:: EXTREAL1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: EXTREAL1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being R_eal st x <> +infty & x <> -infty holds
x is Real
proof end;

theorem Th2: :: EXTREAL1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
-infty <' +infty
proof end;

theorem Th3: :: EXTREAL1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st x <' y holds
( x <> +infty & y <> -infty ) by SUPINF_1:20, SUPINF_1:21;

theorem Th4: :: EXTREAL1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being R_eal holds
( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) )
proof end;

theorem Th5: :: EXTREAL1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal holds x - (- y) = x + y
proof end;

theorem :: EXTREAL1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th7: :: EXTREAL1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st x <> -infty & y <> +infty & x <=' y holds
( x <> +infty & y <> -infty )
proof end;

Lm1: for x being R_eal st x in REAL holds
( x + -infty = -infty & x + +infty = +infty )
by SUPINF_1:2, SUPINF_1:6, SUPINF_2:def 2;

Lm2: for x, y being R_eal st x in REAL & y in REAL holds
x + y in REAL
proof end;

theorem Th8: :: EXTREAL1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being R_eal st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & not ( y = +infty & z = -infty ) & not ( y = -infty & z = +infty ) & not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) holds
(x + y) + z = x + (y + z)
proof end;

theorem Th9: :: EXTREAL1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being R_eal holds x + (- x) = 0.
proof end;

theorem :: EXTREAL1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EXTREAL1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being R_eal st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) & ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) holds
(x + y) - z = x + (y - z)
proof end;

definition
let x, y be R_eal;
func x * y -> R_eal means :Def1: :: EXTREAL1:def 1
( ex a, b being Real st
( x = a & y = b & it = a * b ) or ( ( ( 0. <' x & y = +infty ) or ( 0. <' y & x = +infty ) or ( x <' 0. & y = -infty ) or ( y <' 0. & x = -infty ) ) & it = +infty ) or ( ( ( x <' 0. & y = +infty ) or ( y <' 0. & x = +infty ) or ( 0. <' x & y = -infty ) or ( 0. <' y & x = -infty ) ) & it = -infty ) or ( ( x = 0. or y = 0. ) & it = 0. ) );
existence
ex b1 being R_eal st
( ex a, b being Real st
( x = a & y = b & b1 = a * b ) or ( ( ( 0. <' x & y = +infty ) or ( 0. <' y & x = +infty ) or ( x <' 0. & y = -infty ) or ( y <' 0. & x = -infty ) ) & b1 = +infty ) or ( ( ( x <' 0. & y = +infty ) or ( y <' 0. & x = +infty ) or ( 0. <' x & y = -infty ) or ( 0. <' y & x = -infty ) ) & b1 = -infty ) or ( ( x = 0. or y = 0. ) & b1 = 0. ) )
proof end;
uniqueness
for b1, b2 being R_eal st ( ex a, b being Real st
( x = a & y = b & b1 = a * b ) or ( ( ( 0. <' x & y = +infty ) or ( 0. <' y & x = +infty ) or ( x <' 0. & y = -infty ) or ( y <' 0. & x = -infty ) ) & b1 = +infty ) or ( ( ( x <' 0. & y = +infty ) or ( y <' 0. & x = +infty ) or ( 0. <' x & y = -infty ) or ( 0. <' y & x = -infty ) ) & b1 = -infty ) or ( ( x = 0. or y = 0. ) & b1 = 0. ) ) & ( ex a, b being Real st
( x = a & y = b & b2 = a * b ) or ( ( ( 0. <' x & y = +infty ) or ( 0. <' y & x = +infty ) or ( x <' 0. & y = -infty ) or ( y <' 0. & x = -infty ) ) & b2 = +infty ) or ( ( ( x <' 0. & y = +infty ) or ( y <' 0. & x = +infty ) or ( 0. <' x & y = -infty ) or ( 0. <' y & x = -infty ) ) & b2 = -infty ) or ( ( x = 0. or y = 0. ) & b2 = 0. ) ) holds
b1 = b2 by SUPINF_1:31, SUPINF_2:def 1;
end;

:: deftheorem Def1 defines * EXTREAL1:def 1 :
for x, y, b3 being R_eal holds
( b3 = x * y iff ( ex a, b being Real st
( x = a & y = b & b3 = a * b ) or ( ( ( 0. <' x & y = +infty ) or ( 0. <' y & x = +infty ) or ( x <' 0. & y = -infty ) or ( y <' 0. & x = -infty ) ) & b3 = +infty ) or ( ( ( x <' 0. & y = +infty ) or ( y <' 0. & x = +infty ) or ( 0. <' x & y = -infty ) or ( 0. <' y & x = -infty ) ) & b3 = -infty ) or ( ( x = 0. or y = 0. ) & b3 = 0. ) ) );

theorem :: EXTREAL1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th13: :: EXTREAL1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal
for a, b being Real st x = a & y = b holds
x * y = a * b
proof end;

Lm3: for x being R_eal
for a being Real st x = a & 0 < a holds
0. <' x
proof end;

Lm4: for x being R_eal
for a being Real st x = a & a < 0 holds
x <' 0.
proof end;

theorem Th14: :: EXTREAL1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st ( ( 0. <=' x & 0. <' y ) or ( 0. <' x & 0. <=' y ) ) holds
0. <' x + y
proof end;

theorem Th15: :: EXTREAL1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st ( ( x <=' 0. & y <' 0. ) or ( x <' 0. & y <=' 0. ) ) holds
x + y <' 0.
proof end;

theorem Th16: :: EXTREAL1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being R_eal holds
( not x in REAL or ( -infty <' x & x <' 0. ) or x = 0. or ( 0. <' x & x <' +infty ) )
proof end;

theorem Th17: :: EXTREAL1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal holds x * y = y * x
proof end;

definition
let x, y be R_eal;
:: original: *
redefine func x * y -> R_eal;
commutativity
for x, y being R_eal holds x * y = y * x by Th17;
end;

theorem :: EXTREAL1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being R_eal
for a being Real st x = a holds
( 0 < a iff 0. <' x ) by Lm3, SUPINF_1:16, SUPINF_2:def 1;

theorem :: EXTREAL1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being R_eal
for a being Real st x = a holds
( a < 0 iff x <' 0. ) by Lm4, SUPINF_1:16, SUPINF_2:def 1;

theorem Th20: :: EXTREAL1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st ( ( 0. <' x & 0. <' y ) or ( x <' 0. & y <' 0. ) ) holds
0. <' x * y
proof end;

theorem Th21: :: EXTREAL1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st ( ( 0. <' x & y <' 0. ) or ( x <' 0. & 0. <' y ) ) holds
x * y <' 0.
proof end;

theorem :: EXTREAL1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal holds
( x * y = 0. iff ( x = 0. or y = 0. ) )
proof end;

theorem :: EXTREAL1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being R_eal holds (x * y) * z = x * (y * z)
proof end;

theorem Th24: :: EXTREAL1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
- 0. = 0.
proof end;

theorem :: EXTREAL1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being R_eal holds
( ( 0. <' x implies - x <' 0. ) & ( - x <' 0. implies 0. <' x ) & ( x <' 0. implies 0. <' - x ) & ( 0. <' - x implies x <' 0. ) ) by Th24, SUPINF_2:17;

theorem Th26: :: EXTREAL1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal holds
( - (x * y) = x * (- y) & - (x * y) = (- x) * y )
proof end;

theorem :: EXTREAL1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st x <> +infty & x <> -infty & x * y = +infty & not y = +infty holds
y = -infty
proof end;

theorem :: EXTREAL1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st x <> +infty & x <> -infty & x * y = -infty & not y = +infty holds
y = -infty
proof end;

Lm5: for x, y, z being R_eal st x <> +infty & x <> -infty holds
x * (y + z) = (x * y) + (x * z)
proof end;

theorem :: EXTREAL1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being R_eal st ( ( x <> +infty & x <> -infty ) or ( y = -infty & z = +infty ) or ( y <' 0. & z <' 0. ) or y = 0. or z = 0. or ( 0. <' y & 0. <' z ) or ( y = +infty & z = -infty ) ) holds
x * (y + z) = (x * y) + (x * z)
proof end;

theorem :: EXTREAL1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, z, x being R_eal holds
( ( y = +infty & z = +infty ) or ( y = -infty & z = -infty ) or not x <> +infty or not x <> -infty or x * (y - z) = (x * y) - (x * z) )
proof end;

definition
let x, y be R_eal;
assume A1: ( ( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) ) & y <> 0. ) ;
func x / y -> R_eal means :Def2: :: EXTREAL1:def 2
( ex a, b being Real st
( x = a & y = b & it = a / b ) or ( ( ( x = +infty & 0. <' y ) or ( x = -infty & y <' 0. ) ) & it = +infty ) or ( ( ( x = -infty & 0. <' y ) or ( x = +infty & y <' 0. ) ) & it = -infty ) or ( ( y = -infty or y = +infty ) & it = 0. ) );
existence
ex b1 being R_eal st
( ex a, b being Real st
( x = a & y = b & b1 = a / b ) or ( ( ( x = +infty & 0. <' y ) or ( x = -infty & y <' 0. ) ) & b1 = +infty ) or ( ( ( x = -infty & 0. <' y ) or ( x = +infty & y <' 0. ) ) & b1 = -infty ) or ( ( y = -infty or y = +infty ) & b1 = 0. ) )
proof end;
uniqueness
for b1, b2 being R_eal st ( ex a, b being Real st
( x = a & y = b & b1 = a / b ) or ( ( ( x = +infty & 0. <' y ) or ( x = -infty & y <' 0. ) ) & b1 = +infty ) or ( ( ( x = -infty & 0. <' y ) or ( x = +infty & y <' 0. ) ) & b1 = -infty ) or ( ( y = -infty or y = +infty ) & b1 = 0. ) ) & ( ex a, b being Real st
( x = a & y = b & b2 = a / b ) or ( ( ( x = +infty & 0. <' y ) or ( x = -infty & y <' 0. ) ) & b2 = +infty ) or ( ( ( x = -infty & 0. <' y ) or ( x = +infty & y <' 0. ) ) & b2 = -infty ) or ( ( y = -infty or y = +infty ) & b2 = 0. ) ) holds
b1 = b2 by A1, SUPINF_1:31;
end;

:: deftheorem Def2 defines / EXTREAL1:def 2 :
for x, y being R_eal st ( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) ) & y <> 0. holds
for b3 being R_eal holds
( b3 = x / y iff ( ex a, b being Real st
( x = a & y = b & b3 = a / b ) or ( ( ( x = +infty & 0. <' y ) or ( x = -infty & y <' 0. ) ) & b3 = +infty ) or ( ( ( x = -infty & 0. <' y ) or ( x = +infty & y <' 0. ) ) & b3 = -infty ) or ( ( y = -infty or y = +infty ) & b3 = 0. ) ) );

theorem :: EXTREAL1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th32: :: EXTREAL1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st y <> 0. holds
for a, b being Real st x = a & y = b holds
x / y = a / b
proof end;

theorem :: EXTREAL1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st x <> -infty & x <> +infty & ( y = -infty or y = +infty ) holds
x / y = 0. by Def2, SUPINF_2:19;

theorem :: EXTREAL1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being R_eal st x <> -infty & x <> +infty & x <> 0. holds
x / x = 1
proof end;

definition
let x be R_eal;
func |.x.| -> R_eal equals :Def3: :: EXTREAL1:def 3
x if 0. <=' x
otherwise - x;
coherence
( ( 0. <=' x implies x is R_eal ) & ( not 0. <=' x implies - x is R_eal ) ) ;
consistency
for b1 being R_eal holds verum ;
end;

:: deftheorem Def3 defines |. EXTREAL1:def 3 :
for x being R_eal holds
( ( 0. <=' x implies |.x.| = x ) & ( not 0. <=' x implies |.x.| = - x ) );

theorem :: EXTREAL1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EXTREAL1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being R_eal st 0. <' x holds
|.x.| = x by Def3;

theorem :: EXTREAL1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being R_eal st x <' 0. holds
|.x.| = - x by Def3;

theorem :: EXTREAL1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Real holds R_EAL (a * b) = (R_EAL a) * (R_EAL b)
proof end;

theorem :: EXTREAL1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Real st b <> 0 holds
R_EAL (a / b) = (R_EAL a) / (R_EAL b)
proof end;

theorem :: EXTREAL1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st x <=' y & x <' +infty & -infty <' y holds
0. <=' y - x
proof end;

theorem :: EXTREAL1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st x <' y & x <' +infty & -infty <' y holds
0. <' y - x
proof end;

theorem :: EXTREAL1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being R_eal st x <=' y & 0. <=' z holds
x * z <=' y * z
proof end;

theorem :: EXTREAL1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being R_eal st x <=' y & z <=' 0. holds
y * z <=' x * z
proof end;

theorem :: EXTREAL1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being R_eal st x <' y & 0. <' z & z <> +infty holds
x * z <' y * z
proof end;

theorem :: EXTREAL1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being R_eal st x <' y & z <' 0. & z <> -infty holds
y * z <' x * z
proof end;

theorem :: EXTREAL1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being R_eal st x is Real & y is Real holds
( x <' y iff ex p, q being Real st
( p = x & q = y & p < q ) )
proof end;

theorem :: EXTREAL1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being R_eal st x <> -infty & y <> +infty & x <=' y & 0. <' z holds
x / z <=' y / z
proof end;

theorem :: EXTREAL1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being R_eal st x <=' y & 0. <' z & z <> +infty holds
x / z <=' y / z
proof end;

theorem :: EXTREAL1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being R_eal st x <> -infty & y <> +infty & x <=' y & z <' 0. holds
y / z <=' x / z
proof end;

theorem :: EXTREAL1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being R_eal st x <=' y & z <' 0. & z <> -infty holds
y / z <=' x / z
proof end;

theorem :: EXTREAL1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being R_eal st x <' y & 0. <' z & z <> +infty holds
x / z <' y / z
proof end;

theorem :: EXTREAL1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being R_eal st x <' y & z <' 0. & z <> -infty holds
y / z <' x / z
proof end;