:: XXREAL_3 semantic presentation
begin
definition
let x, y be ext-real number ;
redefine pred x <= y means :Def1: :: XXREAL_3:def 1
ex p, q being Element of REAL st
( p = x & q = y & p <= q ) if ( x in REAL & y in REAL )
otherwise ( x = -infty or y = +infty );
consistency
verum ;
compatibility
( ( x in REAL & y in REAL implies ( x <= y iff ex p, q being Element of REAL st
( p = x & q = y & p <= q ) ) ) & ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) )
proof
thus ( x in REAL & y in REAL implies ( x <= y iff ex p, q being Element of REAL st
( p = x & q = y & p <= q ) ) ) ; ::_thesis: ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) )
thus ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) ::_thesis: verum
proof
assume A1: ( not x in REAL or not y in REAL ) ; ::_thesis: ( x <= y iff ( x = -infty or y = +infty ) )
percases ( not x in REAL or not y in REAL ) by A1;
supposeA2: not x in REAL ; ::_thesis: ( x <= y iff ( x = -infty or y = +infty ) )
thus ( not x <= y or x = -infty or y = +infty ) ::_thesis: ( ( x = -infty or y = +infty ) implies x <= y )
proof
assume A3: x <= y ; ::_thesis: ( x = -infty or y = +infty )
assume x <> -infty ; ::_thesis: y = +infty
then x = +infty by A2, XXREAL_0:14;
hence y = +infty by A3, XXREAL_0:4; ::_thesis: verum
end;
thus ( ( x = -infty or y = +infty ) implies x <= y ) by XXREAL_0:3, XXREAL_0:5; ::_thesis: verum
end;
supposeA4: not y in REAL ; ::_thesis: ( x <= y iff ( x = -infty or y = +infty ) )
thus ( not x <= y or x = -infty or y = +infty ) ::_thesis: ( ( x = -infty or y = +infty ) implies x <= y )
proof
assume A5: x <= y ; ::_thesis: ( x = -infty or y = +infty )
assume A6: x <> -infty ; ::_thesis: y = +infty
assume y <> +infty ; ::_thesis: contradiction
then y = -infty by A4, XXREAL_0:14;
hence contradiction by A5, A6, XXREAL_0:6; ::_thesis: verum
end;
thus ( ( x = -infty or y = +infty ) implies x <= y ) by XXREAL_0:3, XXREAL_0:5; ::_thesis: verum
end;
end;
end;
end;
end;
:: deftheorem Def1 defines <= XXREAL_3:def_1_:_
for x, y being ext-real number holds
( ( x in REAL & y in REAL implies ( x <= y iff ex p, q being Element of REAL st
( p = x & q = y & p <= q ) ) ) & ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) );
registration
cluster ext-real positive non real for set ;
existence
ex b1 being ext-real number st
( not b1 is real & b1 is positive )
proof
take +infty ; ::_thesis: ( not +infty is real & +infty is positive )
thus ( not +infty is real & +infty is positive ) ; ::_thesis: verum
end;
cluster ext-real negative non real for set ;
existence
ex b1 being ext-real number st
( not b1 is real & b1 is negative )
proof
take -infty ; ::_thesis: ( not -infty is real & -infty is negative )
thus ( not -infty is real & -infty is negative ) ; ::_thesis: verum
end;
end;
theorem Th1: :: XXREAL_3:1
for x being ext-real positive non real number holds x = +infty
proof
let x be ext-real positive non real number ; ::_thesis: x = +infty
not x in REAL ;
hence x = +infty by XXREAL_0:14; ::_thesis: verum
end;
theorem Th2: :: XXREAL_3:2
for x being ext-real negative non real number holds x = -infty
proof
let x be ext-real negative non real number ; ::_thesis: x = -infty
not x in REAL ;
hence x = -infty by XXREAL_0:14; ::_thesis: verum
end;
registration
cluster ext-real non negative non real -> ext-real positive for set ;
coherence
for b1 being ext-real number st not b1 is real & not b1 is negative holds
b1 is positive ;
cluster ext-real non positive non real -> ext-real negative for set ;
coherence
for b1 being ext-real number st not b1 is real & not b1 is positive holds
b1 is negative ;
end;
theorem Th3: :: XXREAL_3:3
for x, z being ext-real number st x < z holds
ex y being real number st
( x < y & y < z )
proof
let x, z be ext-real number ; ::_thesis: ( x < z implies ex y being real number st
( x < y & y < z ) )
assume A1: x < z ; ::_thesis: ex y being real number st
( x < y & y < z )
percases ( ( x in REAL & z in REAL ) or x = +infty or z = -infty or z = +infty or x = -infty ) by XXREAL_0:14;
suppose ( x in REAL & z in REAL ) ; ::_thesis: ex y being real number st
( x < y & y < z )
hence ex y being real number st
( x < y & y < z ) by A1, XREAL_1:5; ::_thesis: verum
end;
suppose ( x = +infty or z = -infty ) ; ::_thesis: ex y being real number st
( x < y & y < z )
hence ex y being real number st
( x < y & y < z ) by A1, XXREAL_0:4, XXREAL_0:6; ::_thesis: verum
end;
supposeA2: z = +infty ; ::_thesis: ex y being real number st
( x < y & y < z )
percases ( x = -infty or x in REAL ) by A1, A2, XXREAL_0:14;
suppose x = -infty ; ::_thesis: ex y being real number st
( x < y & y < z )
hence ex y being real number st
( x < y & y < z ) by A2; ::_thesis: verum
end;
suppose x in REAL ; ::_thesis: ex y being real number st
( x < y & y < z )
then reconsider x1 = x as real number ;
take x1 + 1 ; ::_thesis: ( x < x1 + 1 & x1 + 1 < z )
A3: x1 + 1 in REAL by XREAL_0:def_1;
x1 + 0 < x1 + 1 by XREAL_1:8;
hence ( x < x1 + 1 & x1 + 1 < z ) by A2, A3, XXREAL_0:9; ::_thesis: verum
end;
end;
end;
supposeA4: x = -infty ; ::_thesis: ex y being real number st
( x < y & y < z )
percases ( z = +infty or z in REAL ) by A1, A4, XXREAL_0:14;
suppose z = +infty ; ::_thesis: ex y being real number st
( x < y & y < z )
hence ex y being real number st
( x < y & y < z ) by A4; ::_thesis: verum
end;
suppose z in REAL ; ::_thesis: ex y being real number st
( x < y & y < z )
then reconsider z1 = z as real number ;
take z1 - 1 ; ::_thesis: ( x < z1 - 1 & z1 - 1 < z )
A5: z1 - 1 in REAL by XREAL_0:def_1;
z1 - 1 < z1 - 0 by XREAL_1:10;
hence ( x < z1 - 1 & z1 - 1 < z ) by A4, A5, XXREAL_0:12; ::_thesis: verum
end;
end;
end;
end;
end;
begin
definition
let x, y be ext-real number ;
funcx + y -> ext-real number means :Def2: :: XXREAL_3:def 2
ex a, b being complex number st
( x = a & y = b & it = a + b ) if ( x is real & y is real )
it = +infty if ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) )
it = -infty if ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) )
otherwise it = 0 ;
existence
( ( x is real & y is real implies ex b1 being ext-real number ex a, b being complex number st
( x = a & y = b & b1 = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b1 being ext-real number st b1 = -infty ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ex b1 being ext-real number st b1 = 0 ) )
proof
thus ( x is real & y is real implies ex c being ext-real number ex a, b being complex number st
( x = a & y = b & c = a + b ) ) ::_thesis: ( ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b1 being ext-real number st b1 = -infty ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ex b1 being ext-real number st b1 = 0 ) )
proof
assume ( x is real & y is real ) ; ::_thesis: ex c being ext-real number ex a, b being complex number st
( x = a & y = b & c = a + b )
then reconsider a = x, b = y as real number ;
take a + b ; ::_thesis: ex a, b being complex number st
( x = a & y = b & a + b = a + b )
take a ; ::_thesis: ex b being complex number st
( x = a & y = b & a + b = a + b )
take b ; ::_thesis: ( x = a & y = b & a + b = a + b )
thus ( x = a & y = b & a + b = a + b ) ; ::_thesis: verum
end;
thus ( ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b1 being ext-real number st b1 = -infty ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ex b1 being ext-real number st b1 = 0 ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being ext-real number holds
( ( x is real & y is real & ex a, b being complex number st
( x = a & y = b & b1 = a + b ) & ex a, b being complex number st
( x = a & y = b & b2 = a + b ) implies b1 = b2 ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) & b1 = +infty & b2 = +infty implies b1 = b2 ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) & b1 = -infty & b2 = -infty implies b1 = b2 ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or not b1 = 0 or not b2 = 0 or b1 = b2 ) ) ;
consistency
for b1 being ext-real number holds
( ( x is real & y is real & ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( ex a, b being complex number st
( x = a & y = b & b1 = a + b ) iff b1 = +infty ) ) & ( x is real & y is real & ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( ex a, b being complex number st
( x = a & y = b & b1 = a + b ) iff b1 = -infty ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) & ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b1 = +infty iff b1 = -infty ) ) ) ;
commutativity
for b1, x, y being ext-real number st ( x is real & y is real implies ex a, b being complex number st
( x = a & y = b & b1 = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies b1 = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies b1 = -infty ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or b1 = 0 ) holds
( ( y is real & x is real implies ex a, b being complex number st
( y = a & x = b & b1 = a + b ) ) & ( ( ( y = +infty & x <> -infty ) or ( x = +infty & y <> -infty ) ) implies b1 = +infty ) & ( ( ( y = -infty & x <> +infty ) or ( x = -infty & y <> +infty ) ) implies b1 = -infty ) & ( ( y is real & x is real ) or ( y = +infty & x <> -infty ) or ( x = +infty & y <> -infty ) or ( y = -infty & x <> +infty ) or ( x = -infty & y <> +infty ) or b1 = 0 ) ) ;
end;
:: deftheorem Def2 defines + XXREAL_3:def_2_:_
for x, y, b3 being ext-real number holds
( ( x is real & y is real implies ( b3 = x + y iff ex a, b being complex number st
( x = a & y = b & b3 = a + b ) ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( b3 = x + y iff b3 = +infty ) ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b3 = x + y iff b3 = -infty ) ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ( b3 = x + y iff b3 = 0 ) ) );
definition
let x be ext-real number ;
func - x -> ext-real number means :Def3: :: XXREAL_3:def 3
ex a being complex number st
( x = a & it = - a ) if x is real
it = -infty if x = +infty
otherwise it = +infty ;
existence
( ( x is real implies ex b1 being ext-real number ex a being complex number st
( x = a & b1 = - a ) ) & ( x = +infty implies ex b1 being ext-real number st b1 = -infty ) & ( not x is real & not x = +infty implies ex b1 being ext-real number st b1 = +infty ) )
proof
thus ( x is real implies ex c being ext-real number ex a being complex number st
( x = a & c = - a ) ) ::_thesis: ( ( x = +infty implies ex b1 being ext-real number st b1 = -infty ) & ( not x is real & not x = +infty implies ex b1 being ext-real number st b1 = +infty ) )
proof
assume x is real ; ::_thesis: ex c being ext-real number ex a being complex number st
( x = a & c = - a )
then reconsider a = x as real number ;
take - a ; ::_thesis: ex a being complex number st
( x = a & - a = - a )
take a ; ::_thesis: ( x = a & - a = - a )
thus ( x = a & - a = - a ) ; ::_thesis: verum
end;
thus ( ( x = +infty implies ex b1 being ext-real number st b1 = -infty ) & ( not x is real & not x = +infty implies ex b1 being ext-real number st b1 = +infty ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being ext-real number holds
( ( x is real & ex a being complex number st
( x = a & b1 = - a ) & ex a being complex number st
( x = a & b2 = - a ) implies b1 = b2 ) & ( x = +infty & b1 = -infty & b2 = -infty implies b1 = b2 ) & ( not x is real & not x = +infty & b1 = +infty & b2 = +infty implies b1 = b2 ) ) ;
consistency
for b1 being ext-real number st x is real & x = +infty holds
( ex a being complex number st
( x = a & b1 = - a ) iff b1 = -infty ) ;
involutiveness
for b1, b2 being ext-real number st ( b2 is real implies ex a being complex number st
( b2 = a & b1 = - a ) ) & ( b2 = +infty implies b1 = -infty ) & ( not b2 is real & not b2 = +infty implies b1 = +infty ) holds
( ( b1 is real implies ex a being complex number st
( b1 = a & b2 = - a ) ) & ( b1 = +infty implies b2 = -infty ) & ( not b1 is real & not b1 = +infty implies b2 = +infty ) )
proof
let y, x be ext-real number ; ::_thesis: ( ( x is real implies ex a being complex number st
( x = a & y = - a ) ) & ( x = +infty implies y = -infty ) & ( not x is real & not x = +infty implies y = +infty ) implies ( ( y is real implies ex a being complex number st
( y = a & x = - a ) ) & ( y = +infty implies x = -infty ) & ( not y is real & not y = +infty implies x = +infty ) ) )
assume that
A1: ( x is real implies ex a being complex number st
( x = a & y = - a ) ) and
A2: ( x = +infty implies y = -infty ) and
A3: ( not x is real & x <> +infty implies y = +infty ) ; ::_thesis: ( ( y is real implies ex a being complex number st
( y = a & x = - a ) ) & ( y = +infty implies x = -infty ) & ( not y is real & not y = +infty implies x = +infty ) )
thus ( y is real implies ex a being complex number st
( y = a & x = - a ) ) ::_thesis: ( ( y = +infty implies x = -infty ) & ( not y is real & not y = +infty implies x = +infty ) )
proof
assume y is real ; ::_thesis: ex a being complex number st
( y = a & x = - a )
then consider a being complex number such that
A4: ( x = a & y = - a ) by A1, A2, A3;
take - a ; ::_thesis: ( y = - a & x = - (- a) )
thus ( y = - a & x = - (- a) ) by A4; ::_thesis: verum
end;
( x in REAL implies x is real ) ;
hence ( y = +infty implies x = -infty ) by A1, A2, XXREAL_0:14; ::_thesis: ( not y is real & not y = +infty implies x = +infty )
thus ( not y is real & not y = +infty implies x = +infty ) by A1, A3; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines - XXREAL_3:def_3_:_
for x, b2 being ext-real number holds
( ( x is real implies ( b2 = - x iff ex a being complex number st
( x = a & b2 = - a ) ) ) & ( x = +infty implies ( b2 = - x iff b2 = -infty ) ) & ( not x is real & not x = +infty implies ( b2 = - x iff b2 = +infty ) ) );
definition
let x, y be ext-real number ;
funcx - y -> ext-real number equals :: XXREAL_3:def 4
x + (- y);
coherence
x + (- y) is ext-real number ;
end;
:: deftheorem defines - XXREAL_3:def_4_:_
for x, y being ext-real number holds x - y = x + (- y);
registration
let x, y be real number ;
let a, b be complex number ;
identifyx + y with a + b when x = a, y = b;
compatibility
( x = a & y = b implies x + y = a + b ) by Def2;
end;
registration
let x be real number ;
let a be complex number ;
identify - x with - a when x = a;
compatibility
( x = a implies - x = - a ) by Def3;
end;
registration
let r be real number ;
cluster - r -> ext-real real ;
coherence
- r is real ;
end;
registration
let r, s be real number ;
clusterr + s -> ext-real real ;
coherence
r + s is real ;
clusterr - s -> ext-real real ;
coherence
r - s is real ;
end;
registration
let x be real number ;
let y be ext-real non real number ;
clusterx + y -> non real for number ;
coherence
for b1 being number st b1 = x + y holds
not b1 is real
proof
not y in REAL ;
then A1: ( y = -infty or y = +infty ) by XXREAL_0:14;
let z be number ; ::_thesis: ( z = x + y implies not z is real )
assume z = x + y ; ::_thesis: not z is real
hence not z is real by A1, Def2; ::_thesis: verum
end;
end;
registration
let x, y be ext-real positive non real number ;
clusterx + y -> ext-real non real ;
coherence
not x + y is real
proof
x = +infty by Th1;
hence not x + y is real by Def2; ::_thesis: verum
end;
end;
registration
let x, y be ext-real negative non real number ;
clusterx + y -> ext-real non real ;
coherence
not x + y is real
proof
x = -infty by Th2;
hence not x + y is real by Def2; ::_thesis: verum
end;
end;
registration
let x be ext-real negative non real number ;
let y be ext-real positive non real number ;
clusterx + y -> zero ext-real ;
coherence
x + y is zero
proof
( x = -infty & y = +infty ) by Th1, Th2;
hence x + y is zero by Def2; ::_thesis: verum
end;
end;
registration
let x, y be real number ;
let a, b be complex number ;
identifyx - y with a - b when x = a, y = b;
compatibility
( x = a & y = b implies x - y = a - b ) ;
end;
theorem Th4: :: XXREAL_3:4
for x being ext-real number holds x + 0 = x
proof
let x be ext-real number ; ::_thesis: x + 0 = x
percases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14;
suppose x in REAL ; ::_thesis: x + 0 = x
then reconsider r = x as real number ;
r + 0 = r ;
hence x + 0 = x ; ::_thesis: verum
end;
suppose ( x = -infty or x = +infty ) ; ::_thesis: x + 0 = x
hence x + 0 = x by Def2; ::_thesis: verum
end;
end;
end;
theorem Th5: :: XXREAL_3:5
- -infty = +infty by Def3;
theorem Th6: :: XXREAL_3:6
- +infty = -infty by Def3;
Lm1: +infty + +infty = +infty
by Def2;
Lm2: -infty + -infty = -infty
by Def2;
theorem Th7: :: XXREAL_3:7
for x being ext-real number holds x + (- x) = 0
proof
let x be ext-real number ; ::_thesis: x + (- x) = 0
percases ( x = -infty or x in REAL or x = +infty ) by XXREAL_0:14;
suppose x = -infty ; ::_thesis: x + (- x) = 0
hence x + (- x) = 0 by Th5; ::_thesis: verum
end;
suppose x in REAL ; ::_thesis: x + (- x) = 0
then reconsider x = x as real number ;
reconsider y = - x as real number ;
x + y = 0 ;
hence x + (- x) = 0 ; ::_thesis: verum
end;
suppose x = +infty ; ::_thesis: x + (- x) = 0
hence x + (- x) = 0 by Th6; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_3:8
for x, y being ext-real number st x + y = 0 holds
x = - y
proof
let x, y be ext-real number ; ::_thesis: ( x + y = 0 implies x = - y )
assume A1: x + y = 0 ; ::_thesis: x = - y
percases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14;
suppose x in REAL ; ::_thesis: x = - y
then reconsider x = x as real number ;
x + y is real by A1;
then reconsider y = y as real number ;
x + y = 0 by A1;
then x = - y ;
hence x = - y ; ::_thesis: verum
end;
supposeA2: x = -infty ; ::_thesis: x = - y
then y = +infty by A1, Def2;
hence x = - y by A2, Def3; ::_thesis: verum
end;
supposeA3: x = +infty ; ::_thesis: x = - y
then y = -infty by A1, Def2;
hence x = - y by A3, Def3; ::_thesis: verum
end;
end;
end;
Lm3: for x being ext-real number holds
( - x in REAL iff x in REAL )
proof
let x be ext-real number ; ::_thesis: ( - x in REAL iff x in REAL )
hereby ::_thesis: ( x in REAL implies - x in REAL )
assume - x in REAL ; ::_thesis: x in REAL
then reconsider a = - x as real number ;
- a in REAL by XREAL_0:def_1;
hence x in REAL ; ::_thesis: verum
end;
assume x in REAL ; ::_thesis: - x in REAL
then reconsider a = x as real number ;
- a is real ;
hence - x in REAL by XREAL_0:def_1; ::_thesis: verum
end;
Lm4: - (+infty + -infty) = +infty - +infty by Def3
.= (- -infty) - +infty by Def3 ;
Lm5: - +infty = -infty
by Def3;
Lm6: for x being ext-real number st x in REAL holds
- (x + +infty) = (- +infty) + (- x)
proof
let x be ext-real number ; ::_thesis: ( x in REAL implies - (x + +infty) = (- +infty) + (- x) )
assume A1: x in REAL ; ::_thesis: - (x + +infty) = (- +infty) + (- x)
then x + +infty = +infty by Def2;
hence - (x + +infty) = (- +infty) + (- x) by A1, Def2, Th6; ::_thesis: verum
end;
Lm7: for x being ext-real number st x in REAL holds
- (x + -infty) = (- -infty) + (- x)
proof
let x be ext-real number ; ::_thesis: ( x in REAL implies - (x + -infty) = (- -infty) + (- x) )
assume A1: x in REAL ; ::_thesis: - (x + -infty) = (- -infty) + (- x)
then x + -infty = -infty by Def2;
hence - (x + -infty) = (- -infty) + (- x) by A1, Def2, Th5; ::_thesis: verum
end;
theorem Th9: :: XXREAL_3:9
for x, y being ext-real number holds - (x + y) = (- x) + (- y)
proof
let x, y be ext-real number ; ::_thesis: - (x + y) = (- x) + (- y)
percases ( ( x = +infty & y = +infty ) or ( x = +infty & y = -infty ) or ( x = +infty & y in REAL ) or ( x = -infty & y = +infty ) or ( x = -infty & y = -infty ) or ( x = -infty & y in REAL ) or ( x in REAL & y = +infty ) or ( x in REAL & y = -infty ) or ( x in REAL & y in REAL ) ) by XXREAL_0:14;
supposeA1: ( x = +infty & y = +infty ) ; ::_thesis: - (x + y) = (- x) + (- y)
hence - (x + y) = - +infty by Def2
.= (- x) + (- y) by A1, Def2, Lm5 ;
::_thesis: verum
end;
suppose ( x = +infty & y = -infty ) ; ::_thesis: - (x + y) = (- x) + (- y)
hence - (x + y) = (- x) + (- y) by Lm4; ::_thesis: verum
end;
suppose ( x = +infty & y in REAL ) ; ::_thesis: - (x + y) = (- x) + (- y)
hence - (x + y) = (- x) + (- y) by Lm6; ::_thesis: verum
end;
suppose ( x = -infty & y = +infty ) ; ::_thesis: - (x + y) = (- x) + (- y)
hence - (x + y) = (- x) + (- y) by Lm4; ::_thesis: verum
end;
supposeA2: ( x = -infty & y = -infty ) ; ::_thesis: - (x + y) = (- x) + (- y)
hence - (x + y) = - -infty by Def2
.= (- x) + (- y) by A2, Def2, Th5 ;
::_thesis: verum
end;
suppose ( x = -infty & y in REAL ) ; ::_thesis: - (x + y) = (- x) + (- y)
hence - (x + y) = (- x) + (- y) by Lm7; ::_thesis: verum
end;
suppose ( x in REAL & y = +infty ) ; ::_thesis: - (x + y) = (- x) + (- y)
hence - (x + y) = (- x) + (- y) by Lm6; ::_thesis: verum
end;
suppose ( x in REAL & y = -infty ) ; ::_thesis: - (x + y) = (- x) + (- y)
hence - (x + y) = (- x) + (- y) by Lm7; ::_thesis: verum
end;
suppose ( x in REAL & y in REAL ) ; ::_thesis: - (x + y) = (- x) + (- y)
then reconsider a = x, b = y as real number ;
- (x + y) = - (a + b)
.= (- a) + (- b) ;
hence - (x + y) = (- x) + (- y) ; ::_thesis: verum
end;
end;
end;
theorem Th10: :: XXREAL_3:10
for f, g being ext-real number st - f = - g holds
f = g
proof
let f, g be ext-real number ; ::_thesis: ( - f = - g implies f = g )
assume A1: - f = - g ; ::_thesis: f = g
percases ( f in REAL or f = +infty or f = -infty ) by XXREAL_0:14;
supposeA2: f in REAL ; ::_thesis: f = g
now__::_thesis:_g_in_REAL
assume not g in REAL ; ::_thesis: contradiction
then ( g = +infty or g = -infty ) by XXREAL_0:14;
hence contradiction by A1, A2, Def3; ::_thesis: verum
end;
then A3: ex a being complex number st
( g = a & - g = - a ) by Def3;
ex a being complex number st
( f = a & - f = - a ) by A2, Def3;
hence f = g by A1, A3; ::_thesis: verum
end;
suppose f = +infty ; ::_thesis: f = g
hence f = g by A1, Th5; ::_thesis: verum
end;
suppose f = -infty ; ::_thesis: f = g
then - (- g) = -infty by A1;
hence f = g by A1; ::_thesis: verum
end;
end;
end;
Lm8: for x, y being ext-real number holds
( not x + y = +infty or x = +infty or y = +infty )
proof
let x, y be ext-real number ; ::_thesis: ( not x + y = +infty or x = +infty or y = +infty )
assume A1: x + y = +infty ; ::_thesis: ( x = +infty or y = +infty )
assume ( not x = +infty & not y = +infty ) ; ::_thesis: contradiction
then ( ( x in REAL & y in REAL ) or ( x in REAL & y = -infty ) or ( x = -infty & y in REAL ) or ( x = -infty & y = -infty ) ) by XXREAL_0:14;
hence contradiction by A1, Def2; ::_thesis: verum
end;
Lm9: for x, y being ext-real number holds
( not x + y = -infty or x = -infty or y = -infty )
proof
let x, y be ext-real number ; ::_thesis: ( not x + y = -infty or x = -infty or y = -infty )
assume A1: x + y = -infty ; ::_thesis: ( x = -infty or y = -infty )
assume ( not x = -infty & not y = -infty ) ; ::_thesis: contradiction
then ( ( x in REAL & y in REAL ) or ( x in REAL & y = +infty ) or ( x = +infty & y in REAL ) or ( x = +infty & y = +infty ) ) by XXREAL_0:14;
hence contradiction by A1, Def2; ::_thesis: verum
end;
theorem Th11: :: XXREAL_3:11
for r being real number
for f, g being ext-real number st r + f = r + g holds
f = g
proof
let r be real number ; ::_thesis: for f, g being ext-real number st r + f = r + g holds
f = g
let f, g be ext-real number ; ::_thesis: ( r + f = r + g implies f = g )
assume A1: r + f = r + g ; ::_thesis: f = g
percases ( f in REAL or f = +infty or f = -infty ) by XXREAL_0:14;
supposeA2: f in REAL ; ::_thesis: f = g
now__::_thesis:_g_in_REAL
assume not g in REAL ; ::_thesis: contradiction
then ( g = +infty or g = -infty ) by XXREAL_0:14;
hence contradiction by A1, A2; ::_thesis: verum
end;
then A3: ex c, d being complex number st
( r = c & g = d & r + g = c + d ) by Def2;
ex a, b being complex number st
( r = a & f = b & r + f = a + b ) by A2, Def2;
hence f = g by A1, A3; ::_thesis: verum
end;
supposeA4: f = +infty ; ::_thesis: f = g
then r + f = +infty by Def2;
hence f = g by A1, A4, Lm8; ::_thesis: verum
end;
supposeA5: f = -infty ; ::_thesis: f = g
then r + f = -infty by Def2;
hence f = g by A1, A5, Lm9; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_3:12
for r being real number
for f, g being ext-real number st r - f = r - g holds
f = g
proof
let r be real number ; ::_thesis: for f, g being ext-real number st r - f = r - g holds
f = g
let f, g be ext-real number ; ::_thesis: ( r - f = r - g implies f = g )
assume r - f = r - g ; ::_thesis: f = g
then - f = - g by Th11;
hence f = g by Th10; ::_thesis: verum
end;
theorem Th13: :: XXREAL_3:13
for x being ext-real number st x <> +infty holds
( +infty - x = +infty & x - +infty = -infty )
proof
let x be ext-real number ; ::_thesis: ( x <> +infty implies ( +infty - x = +infty & x - +infty = -infty ) )
assume A1: x <> +infty ; ::_thesis: ( +infty - x = +infty & x - +infty = -infty )
then - x <> -infty by Th5;
hence +infty - x = +infty by Def2; ::_thesis: x - +infty = -infty
- +infty = -infty by Def3;
hence x - +infty = -infty by A1, Def2; ::_thesis: verum
end;
theorem Th14: :: XXREAL_3:14
for x being ext-real number st x <> -infty holds
( -infty - x = -infty & x - -infty = +infty )
proof
let x be ext-real number ; ::_thesis: ( x <> -infty implies ( -infty - x = -infty & x - -infty = +infty ) )
assume A1: x <> -infty ; ::_thesis: ( -infty - x = -infty & x - -infty = +infty )
now__::_thesis:_not_-_x_=_+infty
assume - x = +infty ; ::_thesis: contradiction
then - (- x) = -infty by Def3;
hence contradiction by A1; ::_thesis: verum
end;
hence -infty - x = -infty by Def2; ::_thesis: x - -infty = +infty
thus x - -infty = +infty by A1, Def2, Th5; ::_thesis: verum
end;
theorem Th15: :: XXREAL_3:15
for x being ext-real number holds x - 0 = x
proof
let x be ext-real number ; ::_thesis: x - 0 = x
percases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14;
suppose x in REAL ; ::_thesis: x - 0 = x
then reconsider a = x as real number ;
x - 0 = a - 0
.= x ;
hence x - 0 = x ; ::_thesis: verum
end;
suppose x = -infty ; ::_thesis: x - 0 = x
hence x - 0 = x by Th14; ::_thesis: verum
end;
suppose x = +infty ; ::_thesis: x - 0 = x
hence x - 0 = x by Th13; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_3:16
for x, y being ext-real number holds
( not x + y = +infty or x = +infty or y = +infty ) by Lm8;
theorem :: XXREAL_3:17
for x, y being ext-real number holds
( not x + y = -infty or x = -infty or y = -infty ) by Lm9;
theorem Th18: :: XXREAL_3:18
for x, y being ext-real number holds
( not x - y = +infty or x = +infty or y = -infty )
proof
let x, y be ext-real number ; ::_thesis: ( not x - y = +infty or x = +infty or y = -infty )
assume A1: x - y = +infty ; ::_thesis: ( x = +infty or y = -infty )
assume ( not x = +infty & not y = -infty ) ; ::_thesis: contradiction
then ( ( x in REAL & y in REAL ) or ( x in REAL & y = +infty ) or ( x = -infty & y in REAL ) or ( x = -infty & y = +infty ) ) by XXREAL_0:14;
hence contradiction by A1, Th13, Th14; ::_thesis: verum
end;
theorem Th19: :: XXREAL_3:19
for x, y being ext-real number holds
( not x - y = -infty or x = -infty or y = +infty )
proof
let x, y be ext-real number ; ::_thesis: ( not x - y = -infty or x = -infty or y = +infty )
assume A1: x - y = -infty ; ::_thesis: ( x = -infty or y = +infty )
assume ( not x = -infty & not y = +infty ) ; ::_thesis: contradiction
then ( ( x in REAL & y in REAL ) or ( x in REAL & y = -infty ) or ( x = +infty & y in REAL ) or ( x = +infty & y = -infty ) ) by XXREAL_0:14;
hence contradiction by A1, Th13, Th14; ::_thesis: verum
end;
theorem Th20: :: XXREAL_3:20
for x, y being ext-real number holds
( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y in REAL or ( x in REAL & y in REAL ) )
proof
let x, y be ext-real number ; ::_thesis: ( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y in REAL or ( x in REAL & y in REAL ) )
assume A1: ( not ( x = +infty & y = -infty ) & not ( x = -infty & y = +infty ) & x + y in REAL ) ; ::_thesis: ( x in REAL & y in REAL )
A2: ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14;
A3: ( y in REAL or y = -infty or y = +infty ) by XXREAL_0:14;
assume ( not x in REAL or not y in REAL ) ; ::_thesis: contradiction
hence contradiction by A1, A2, A3; ::_thesis: verum
end;
theorem Th21: :: XXREAL_3:21
for x, y being ext-real number holds
( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y in REAL or ( x in REAL & y in REAL ) )
proof
let x, y be ext-real number ; ::_thesis: ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y in REAL or ( x in REAL & y in REAL ) )
assume A1: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) & x - y in REAL ) ; ::_thesis: ( x in REAL & y in REAL )
A2: ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14;
A3: ( y in REAL or y = -infty or y = +infty ) by XXREAL_0:14;
assume ( not x in REAL or not y in REAL ) ; ::_thesis: contradiction
hence contradiction by A1, A2, A3, Th13, Th14; ::_thesis: verum
end;
theorem Th22: :: XXREAL_3:22
for x, y being ext-real number st x is real holds
( (y - x) + x = y & (y + x) - x = y )
proof
let x, y be ext-real number ; ::_thesis: ( x is real implies ( (y - x) + x = y & (y + x) - x = y ) )
assume A1: x is real ; ::_thesis: ( (y - x) + x = y & (y + x) - x = y )
percases ( ( x in REAL & y in REAL ) or ( x in REAL & y = -infty ) or ( x in REAL & y = +infty ) ) by A1, XXREAL_0:14;
suppose ( x in REAL & y in REAL ) ; ::_thesis: ( (y - x) + x = y & (y + x) - x = y )
then reconsider a = x, b = y as real number ;
A2: (y + x) - x = (b + a) - a
.= y ;
(y - x) + x = (b - a) + a
.= y ;
hence ( (y - x) + x = y & (y + x) - x = y ) by A2; ::_thesis: verum
end;
supposeA3: ( x in REAL & y = -infty ) ; ::_thesis: ( (y - x) + x = y & (y + x) - x = y )
then y - x = -infty by Def2;
hence ( (y - x) + x = y & (y + x) - x = y ) by A3, Def2; ::_thesis: verum
end;
supposeA4: ( x in REAL & y = +infty ) ; ::_thesis: ( (y - x) + x = y & (y + x) - x = y )
then y - x = +infty by Def2;
hence ( (y - x) + x = y & (y + x) - x = y ) by A4, Def2; ::_thesis: verum
end;
end;
end;
theorem Th23: :: XXREAL_3:23
for x being ext-real number holds
( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) )
proof
let x be ext-real number ; ::_thesis: ( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) )
( - x = +infty implies x = -infty )
proof
assume - x = +infty ; ::_thesis: x = -infty
then - (- x) = -infty by Def3;
hence x = -infty ; ::_thesis: verum
end;
hence ( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) ) by Th5; ::_thesis: verum
end;
theorem :: XXREAL_3:24
for z, x being ext-real number st z is real holds
x = (x + z) - z
proof
let z, x be ext-real number ; ::_thesis: ( z is real implies x = (x + z) - z )
assume A1: z is real ; ::_thesis: x = (x + z) - z
percases ( x = +infty or x = -infty or x is Element of REAL ) by XXREAL_0:14;
supposeA2: x = +infty ; ::_thesis: x = (x + z) - z
then x + z = +infty by A1, Def2;
hence x = (x + z) - z by A1, A2, Th13; ::_thesis: verum
end;
supposeA3: x = -infty ; ::_thesis: x = (x + z) - z
then x + z = -infty by A1, Def2;
hence x = (x + z) - z by A1, A3, Th14; ::_thesis: verum
end;
suppose x is Element of REAL ; ::_thesis: x = (x + z) - z
then reconsider a = x, c = z as real number by A1;
(x + z) - z = (a + c) - c ;
hence x = (x + z) - z ; ::_thesis: verum
end;
end;
end;
Lm10: - +infty = -infty
by Def3;
Lm11: for x being ext-real number st x in REAL holds
- (x + -infty) = (- -infty) + (- x)
proof
let x be ext-real number ; ::_thesis: ( x in REAL implies - (x + -infty) = (- -infty) + (- x) )
A1: - -infty = +infty by Th23;
assume A2: x in REAL ; ::_thesis: - (x + -infty) = (- -infty) + (- x)
then x + -infty = -infty by Def2;
hence - (x + -infty) = (- -infty) + (- x) by A2, A1, Def2; ::_thesis: verum
end;
theorem Th25: :: XXREAL_3:25
for x, y being ext-real number holds - (x + y) = (- y) - x
proof
let x, y be ext-real number ; ::_thesis: - (x + y) = (- y) - x
percases ( ( x = +infty & y = +infty ) or ( x = +infty & y = -infty ) or ( x = +infty & y in REAL ) or ( x = -infty & y = +infty ) or ( x = -infty & y = -infty ) or ( x = -infty & y in REAL ) or ( x in REAL & y = +infty ) or ( x in REAL & y = -infty ) or ( x in REAL & y in REAL ) ) by XXREAL_0:14;
supposeA1: ( x = +infty & y = +infty ) ; ::_thesis: - (x + y) = (- y) - x
hence - (x + y) = - +infty by Def2
.= (- y) - x by A1, Def2, Lm10 ;
::_thesis: verum
end;
suppose ( x = +infty & y = -infty ) ; ::_thesis: - (x + y) = (- y) - x
hence - (x + y) = (- y) - x by Lm4; ::_thesis: verum
end;
suppose ( x = +infty & y in REAL ) ; ::_thesis: - (x + y) = (- y) - x
hence - (x + y) = (- y) - x by Lm6; ::_thesis: verum
end;
suppose ( x = -infty & y = +infty ) ; ::_thesis: - (x + y) = (- y) - x
hence - (x + y) = (- y) - x by Lm4; ::_thesis: verum
end;
supposeA2: ( x = -infty & y = -infty ) ; ::_thesis: - (x + y) = (- y) - x
hence - (x + y) = - -infty by Def2
.= (- y) - x by A2, Def2, Th5 ;
::_thesis: verum
end;
suppose ( x = -infty & y in REAL ) ; ::_thesis: - (x + y) = (- y) - x
hence - (x + y) = (- y) - x by Lm11; ::_thesis: verum
end;
suppose ( x in REAL & y = +infty ) ; ::_thesis: - (x + y) = (- y) - x
hence - (x + y) = (- y) - x by Lm6; ::_thesis: verum
end;
suppose ( x in REAL & y = -infty ) ; ::_thesis: - (x + y) = (- y) - x
hence - (x + y) = (- y) - x by Lm11; ::_thesis: verum
end;
suppose ( x in REAL & y in REAL ) ; ::_thesis: - (x + y) = (- y) - x
then reconsider a = x, b = y as real number ;
- (x + y) = - (a + b)
.= (- a) + (- b) ;
hence - (x + y) = (- y) - x ; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_3:26
for x, y being ext-real number holds
( - (x - y) = (- x) + y & - (x - y) = y - x )
proof
let x, y be ext-real number ; ::_thesis: ( - (x - y) = (- x) + y & - (x - y) = y - x )
- (x - y) = (- (- y)) - x by Th25;
hence ( - (x - y) = (- x) + y & - (x - y) = y - x ) ; ::_thesis: verum
end;
theorem Th27: :: XXREAL_3:27
for x, y being ext-real number holds
( - ((- x) + y) = x - y & - ((- x) + y) = x + (- y) )
proof
let x, y be ext-real number ; ::_thesis: ( - ((- x) + y) = x - y & - ((- x) + y) = x + (- y) )
- ((- x) + y) = (- (- x)) - y by Th25
.= x - y ;
hence ( - ((- x) + y) = x - y & - ((- x) + y) = x + (- y) ) ; ::_thesis: verum
end;
theorem :: XXREAL_3:28
for y, z being ext-real number st 0 <= y & y < +infty holds
z = (z + y) - y
proof
let y, z be ext-real number ; ::_thesis: ( 0 <= y & y < +infty implies z = (z + y) - y )
assume ( 0 <= y & y < +infty ) ; ::_thesis: z = (z + y) - y
then y in REAL by XXREAL_0:14;
hence z = (z + y) - y by Th22; ::_thesis: verum
end;
theorem Th29: :: XXREAL_3:29
for x, y, z being ext-real number 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
let x, y, z be ext-real number ; ::_thesis: ( ( 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 ) implies (x + y) + z = x + (y + z) )
assume A1: ( not ( x = +infty & y = -infty ) & not ( x = -infty & y = +infty ) & not ( y = +infty & z = -infty ) & not ( y = -infty & z = +infty ) & not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) ) ; ::_thesis: (x + y) + z = x + (y + z)
percases ( ( x in REAL & y in REAL & z in REAL ) or ( x in REAL & y = +infty & z in REAL ) or ( x in REAL & y = -infty & z in REAL ) or ( x = -infty & y in REAL & z in REAL ) or ( x = +infty & y in REAL & z in REAL ) or ( x in REAL & y in REAL & z = +infty ) or ( x in REAL & y in REAL & z = -infty ) or ( x = +infty & y = +infty & z in REAL ) or ( x in REAL & y = -infty & z = -infty ) or ( x = -infty & y = -infty & z in REAL ) or ( x = -infty & y in REAL & z = -infty ) or ( x = -infty & y = -infty & z = -infty ) or ( x = +infty & y in REAL & z = +infty ) or ( x = +infty & y = +infty & z = +infty ) or ( x in REAL & y = +infty & z = +infty ) ) by A1, XXREAL_0:14;
suppose ( x in REAL & y in REAL & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z)
then reconsider A = x, B = y, C = z as real number ;
( (A + B) + C = (x + y) + z & A + (B + C) = x + (y + z) ) ;
hence (x + y) + z = x + (y + z) ; ::_thesis: verum
end;
supposeA2: ( x in REAL & y = +infty & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z)
then ( x + y = +infty & y + z = +infty ) by Def2;
hence (x + y) + z = x + (y + z) by A2; ::_thesis: verum
end;
supposeA3: ( x in REAL & y = -infty & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z)
then ( x + y = -infty & y + z = -infty ) by Def2;
hence (x + y) + z = x + (y + z) by A3; ::_thesis: verum
end;
supposeA4: ( x = -infty & y in REAL & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z)
then x + y = -infty by Def2;
then (x + y) + z = -infty by A4, Def2;
hence (x + y) + z = x + (y + z) by A4, Def2; ::_thesis: verum
end;
supposeA5: ( x = +infty & y in REAL & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z)
then x + y = +infty by Def2;
then (x + y) + z = +infty by A5, Def2;
hence (x + y) + z = x + (y + z) by A5, Def2; ::_thesis: verum
end;
supposeA6: ( x in REAL & y in REAL & z = +infty ) ; ::_thesis: (x + y) + z = x + (y + z)
then y + z = +infty by Def2;
then x + (y + z) = +infty by A6, Def2;
hence (x + y) + z = x + (y + z) by A6, Def2; ::_thesis: verum
end;
supposeA7: ( x in REAL & y in REAL & z = -infty ) ; ::_thesis: (x + y) + z = x + (y + z)
then y + z = -infty by Def2;
then x + (y + z) = -infty by A7, Def2;
hence (x + y) + z = x + (y + z) by A7, Def2; ::_thesis: verum
end;
supposeA8: ( x = +infty & y = +infty & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z)
then x + y = +infty by Def2;
then A9: (x + y) + z = +infty by A8, Def2;
y + z <> -infty by A8, Def2;
hence (x + y) + z = x + (y + z) by A8, A9, Def2; ::_thesis: verum
end;
supposeA10: ( x in REAL & y = -infty & z = -infty ) ; ::_thesis: (x + y) + z = x + (y + z)
then A11: x + y = -infty by Def2;
then (x + y) + z = -infty by A10, Def2;
hence (x + y) + z = x + (y + z) by A10, A11; ::_thesis: verum
end;
supposeA12: ( x = -infty & y = -infty & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z)
then A13: x + y = -infty by Def2;
then (x + y) + z = -infty by A12, Def2;
hence (x + y) + z = x + (y + z) by A12, A13; ::_thesis: verum
end;
suppose ( ( x = -infty & y in REAL & z = -infty ) or ( x = -infty & y = -infty & z = -infty ) or ( x = +infty & y in REAL & z = +infty ) or ( x = +infty & y = +infty & z = +infty ) ) ; ::_thesis: (x + y) + z = x + (y + z)
hence (x + y) + z = x + (y + z) ; ::_thesis: verum
end;
supposeA14: ( x in REAL & y = +infty & z = +infty ) ; ::_thesis: (x + y) + z = x + (y + z)
then ( x + y = +infty & y + z = +infty ) by Def2;
hence (x + y) + z = x + (y + z) by A14; ::_thesis: verum
end;
end;
end;
theorem Th30: :: XXREAL_3:30
for x, y, z being ext-real number 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
let x, y, z be ext-real number ; ::_thesis: ( ( 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 ) implies (x + y) - z = x + (y - z) )
assume that
A1: ( ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) ) and
A2: ( ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) ) and
A3: ( ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) ) ; ::_thesis: (x + y) - z = x + (y - z)
A4: ( ( not x = +infty or not - z = -infty ) & ( not x = -infty or not - z = +infty ) ) by A3, Th23;
( ( not y = +infty or not - z = -infty ) & ( not y = -infty or not - z = +infty ) ) by A2, Th23;
hence (x + y) - z = x + (y - z) by A1, A4, Th29; ::_thesis: verum
end;
theorem :: XXREAL_3:31
for x, y, z being ext-real number 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
let x, y, z be ext-real number ; ::_thesis: ( ( 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 ) implies (x - y) - z = x - (y + z) )
assume that
A1: ( not x = +infty or not y = +infty ) and
A2: ( not x = -infty or not y = -infty ) and
A3: ( not y = +infty or not z = -infty ) and
A4: ( not y = -infty or not z = +infty ) and
A5: ( not x = +infty or not z = +infty ) and
A6: ( not x = -infty or not z = -infty ) ; ::_thesis: (x - y) - z = x - (y + z)
percases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ;
supposeA7: x = +infty ; ::_thesis: (x - y) - z = x - (y + z)
then x - y = +infty by A1, Th13;
then A8: (x - y) - z = +infty by A5, A7, Th13;
y + z <> +infty by A1, A5, A7, Lm8;
hence (x - y) - z = x - (y + z) by A7, A8, Th13; ::_thesis: verum
end;
supposeA9: x = -infty ; ::_thesis: (x - y) - z = x - (y + z)
then x - y = -infty by A2, Th14;
then A10: (x - y) - z = -infty by A6, A9, Th14;
y + z <> -infty by A2, A6, A9, Lm9;
hence (x - y) - z = x - (y + z) by A9, A10, Th14; ::_thesis: verum
end;
supposeA11: ( x <> +infty & x <> -infty ) ; ::_thesis: (x - y) - z = x - (y + z)
then x in REAL by XXREAL_0:14;
then reconsider a = x as real number ;
percases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ;
supposeA12: y = +infty ; ::_thesis: (x - y) - z = x - (y + z)
then ( x - y = -infty & y + z = +infty ) by A3, A11, Def2, Th13;
hence (x - y) - z = x - (y + z) by A3, A12, Th14; ::_thesis: verum
end;
supposeA13: y = -infty ; ::_thesis: (x - y) - z = x - (y + z)
then ( x - y = +infty & y + z = -infty ) by A4, A11, Def2, Th14;
hence (x - y) - z = x - (y + z) by A4, A13, Th13; ::_thesis: verum
end;
suppose ( y <> +infty & y <> -infty ) ; ::_thesis: (x - y) - z = x - (y + z)
then y in REAL by XXREAL_0:14;
then reconsider b = y as real number ;
A14: x - y = a - b ;
percases ( z = +infty or z = -infty or ( z <> +infty & z <> -infty ) ) ;
suppose z = +infty ; ::_thesis: (x - y) - z = x - (y + z)
then ( (x - y) - z = -infty & y + z = +infty ) by A14, Def2, Th13;
hence (x - y) - z = x - (y + z) by A11, Th13; ::_thesis: verum
end;
suppose z = -infty ; ::_thesis: (x - y) - z = x - (y + z)
then ( (x - y) - z = +infty & y + z = -infty ) by A14, Def2, Th14;
hence (x - y) - z = x - (y + z) by A11, Th14; ::_thesis: verum
end;
suppose ( z <> +infty & z <> -infty ) ; ::_thesis: (x - y) - z = x - (y + z)
then z in REAL by XXREAL_0:14;
then reconsider c = z as real number ;
( (x - y) - z = (a - b) - c & x - (y + z) = a - (b + c) ) ;
hence (x - y) - z = x - (y + z) ; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
theorem Th32: :: XXREAL_3:32
for x, y, z being ext-real number 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
let x, y, z be ext-real number ; ::_thesis: ( ( 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 ) implies (x - y) + z = x - (y - z) )
assume that
A1: ( not x = +infty or not y = +infty ) and
A2: ( not x = -infty or not y = -infty ) and
A3: ( not y = +infty or not z = +infty ) and
A4: ( not y = -infty or not z = -infty ) and
A5: ( not x = +infty or not z = -infty ) and
A6: ( not x = -infty or not z = +infty ) ; ::_thesis: (x - y) + z = x - (y - z)
percases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ;
supposeA7: x = +infty ; ::_thesis: (x - y) + z = x - (y - z)
then x - y = +infty by A1, Th13;
then A8: (x - y) + z = +infty by A5, A7, Def2;
y - z <> +infty by A1, A5, A7, Th18;
hence (x - y) + z = x - (y - z) by A7, A8, Th13; ::_thesis: verum
end;
supposeA9: x = -infty ; ::_thesis: (x - y) + z = x - (y - z)
then x - y = -infty by A2, Th14;
then A10: (x - y) + z = -infty by A6, A9, Def2;
y - z <> -infty by A2, A6, A9, Th19;
hence (x - y) + z = x - (y - z) by A9, A10, Th14; ::_thesis: verum
end;
supposeA11: ( x <> +infty & x <> -infty ) ; ::_thesis: (x - y) + z = x - (y - z)
then x in REAL by XXREAL_0:14;
then reconsider a = x as real number ;
percases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ;
supposeA12: y = +infty ; ::_thesis: (x - y) + z = x - (y - z)
then ( x - y = -infty & y - z = +infty ) by A3, A11, Th13;
hence (x - y) + z = x - (y - z) by A3, A12, Def2; ::_thesis: verum
end;
supposeA13: y = -infty ; ::_thesis: (x - y) + z = x - (y - z)
then ( x - y = +infty & y - z = -infty ) by A4, A11, Th14;
hence (x - y) + z = x - (y - z) by A4, A13, Def2; ::_thesis: verum
end;
suppose ( y <> +infty & y <> -infty ) ; ::_thesis: (x - y) + z = x - (y - z)
then y in REAL by XXREAL_0:14;
then reconsider b = y as real number ;
A14: x - y = a - b ;
percases ( z = +infty or z = -infty or ( z <> +infty & z <> -infty ) ) ;
suppose z = +infty ; ::_thesis: (x - y) + z = x - (y - z)
then ( (x - y) + z = +infty & y - z = -infty ) by A14, Def2, Th13;
hence (x - y) + z = x - (y - z) by A11, Th14; ::_thesis: verum
end;
suppose z = -infty ; ::_thesis: (x - y) + z = x - (y - z)
then ( (x - y) + z = -infty & y - z = +infty ) by A14, Def2, Th14;
hence (x - y) + z = x - (y - z) by A11, Th13; ::_thesis: verum
end;
suppose ( z <> +infty & z <> -infty ) ; ::_thesis: (x - y) + z = x - (y - z)
then z in REAL by XXREAL_0:14;
then reconsider c = z as real number ;
( (x - y) + z = (a - b) + c & x - (y - z) = a - (b - c) ) ;
hence (x - y) + z = x - (y - z) ; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
theorem Th33: :: XXREAL_3:33
for z, x, y being ext-real number st z is real holds
(z + x) - (z + y) = x - y
proof
let z, x, y be ext-real number ; ::_thesis: ( z is real implies (z + x) - (z + y) = x - y )
assume A1: z is real ; ::_thesis: (z + x) - (z + y) = x - y
percases ( x = -infty or y = +infty or ( x in REAL & y in REAL & z in REAL ) or ( x = +infty & y in REAL & z in REAL ) or ( x in REAL & y = -infty & z in REAL ) or ( x = +infty & y = -infty & z in REAL ) ) by A1, XXREAL_0:14;
supposeA2: x = -infty ; ::_thesis: (z + x) - (z + y) = x - y
percases ( y = -infty or y = +infty or y in REAL ) by XXREAL_0:14;
supposeA3: y = -infty ; ::_thesis: (z + x) - (z + y) = x - y
(z + -infty) - (z + -infty) = -infty - (z + -infty) by A1, Def2
.= -infty - -infty by A1, Def2 ;
hence (z + x) - (z + y) = x - y by A2, A3; ::_thesis: verum
end;
supposeA4: y = +infty ; ::_thesis: (z + x) - (z + y) = x - y
(z + -infty) - (z + +infty) = -infty - (z + +infty) by A1, Def2
.= -infty - +infty by A1, Def2 ;
hence (z + x) - (z + y) = x - y by A2, A4; ::_thesis: verum
end;
supposeA5: y in REAL ; ::_thesis: (z + x) - (z + y) = x - y
then consider a, b being complex number such that
A6: ( z = a & y = b ) and
z + y = a + b by A1, Def2;
reconsider a = a, b = b as real number by A1, A5, A6;
A7: a + b in REAL by XREAL_0:def_1;
(z + -infty) - (z + y) = -infty - (z + y) by A1, Def2
.= -infty by A6, A7, Def2
.= -infty - y by A5, Def2 ;
hence (z + x) - (z + y) = x - y by A2; ::_thesis: verum
end;
end;
end;
supposeA8: y = +infty ; ::_thesis: (z + x) - (z + y) = x - y
percases ( x = -infty or x = +infty or x in REAL ) by XXREAL_0:14;
supposeA9: x = -infty ; ::_thesis: (z + x) - (z + y) = x - y
(z + -infty) - (z + +infty) = (z + -infty) - +infty by A1, Def2
.= -infty - +infty by A1, Def2 ;
hence (z + x) - (z + y) = x - y by A8, A9; ::_thesis: verum
end;
supposeA10: x = +infty ; ::_thesis: (z + x) - (z + y) = x - y
(z + +infty) - (z + +infty) = (z + +infty) - +infty by A1, Def2
.= +infty - +infty by A1, Def2 ;
hence (z + x) - (z + y) = x - y by A8, A10; ::_thesis: verum
end;
supposeA11: x in REAL ; ::_thesis: (z + x) - (z + y) = x - y
then consider a, b being complex number such that
A12: ( z = a & x = b ) and
z + x = a + b by A1, Def2;
reconsider a = a, b = b as real number by A1, A11, A12;
A13: a + b in REAL by XREAL_0:def_1;
A14: - +infty = -infty by Def3;
(z + x) - (z + +infty) = (z + x) - +infty by A1, Def2
.= (z + x) + -infty by Def3
.= -infty by A12, A13, Def2
.= x + (- +infty) by A11, A14, Def2 ;
hence (z + x) - (z + y) = x - y by A8; ::_thesis: verum
end;
end;
end;
suppose ( x in REAL & y in REAL & z in REAL ) ; ::_thesis: (z + x) - (z + y) = x - y
then reconsider a = x, b = y, c = z as real number ;
(z + x) - (z + y) = (a + c) - (c + b)
.= a - b
.= x - y ;
hence (z + x) - (z + y) = x - y ; ::_thesis: verum
end;
supposeA15: ( x = +infty & y in REAL & z in REAL ) ; ::_thesis: (z + x) - (z + y) = x - y
then reconsider c = z, b = y as real number ;
A16: z + y = c + b ;
( z + x = +infty & x - y = +infty ) by A15, Def2;
hence (z + x) - (z + y) = x - y by A16, Th13; ::_thesis: verum
end;
supposeA17: ( x in REAL & y = -infty & z in REAL ) ; ::_thesis: (z + x) - (z + y) = x - y
then reconsider c = z, a = x as real number ;
( z + x = c + a & z + y = -infty ) by A17, Def2;
then (z + x) - (z + y) = +infty by Th14
.= x - y by A17, Th14 ;
hence (z + x) - (z + y) = x - y ; ::_thesis: verum
end;
supposeA18: ( x = +infty & y = -infty & z in REAL ) ; ::_thesis: (z + x) - (z + y) = x - y
then ( z + y = -infty & not z + x = -infty ) by Def2;
then (z + x) - (z + y) = +infty by Th14
.= x - y by A18, Th14 ;
hence (z + x) - (z + y) = x - y ; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_3:34
for y, z, x being ext-real number st y is real holds
(z - y) + (y - x) = z - x
proof
let y, z, x be ext-real number ; ::_thesis: ( y is real implies (z - y) + (y - x) = z - x )
assume A1: y is real ; ::_thesis: (z - y) + (y - x) = z - x
thus (z - y) + (y - x) = (z - y) - (x - y) by Th27
.= z - x by A1, Th33 ; ::_thesis: verum
end;
begin
Lm12: for x, y, z being ext-real number st x <= y holds
x + z <= y + z
proof
let x, y, z be ext-real number ; ::_thesis: ( x <= y implies x + z <= y + z )
assume A1: x <= y ; ::_thesis: x + z <= y + z
percases ( ( x in REAL & y in REAL ) or ( x in REAL & y = +infty ) or ( x = -infty & y in REAL ) or ( x = -infty & y = +infty ) or x = +infty or y = -infty ) by XXREAL_0:14;
supposeA2: ( x in REAL & y in REAL ) ; ::_thesis: x + z <= y + z
percases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14;
supposeA3: z = -infty ; ::_thesis: x + z <= y + z
-infty <= y + z by XXREAL_0:5;
hence x + z <= y + z by A2, A3, Def2; ::_thesis: verum
end;
suppose z in REAL ; ::_thesis: x + z <= y + z
then reconsider x = x, y = y, z = z as real number by A2;
x + z <= y + z by A1, XREAL_1:6;
hence x + z <= y + z ; ::_thesis: verum
end;
supposeA4: z = +infty ; ::_thesis: x + z <= y + z
x + z <= +infty by XXREAL_0:3;
hence x + z <= y + z by A2, A4, Def2; ::_thesis: verum
end;
end;
end;
supposeA5: ( x in REAL & y = +infty ) ; ::_thesis: x + z <= y + z
percases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14;
supposeA6: z = -infty ; ::_thesis: x + z <= y + z
-infty <= y + z by XXREAL_0:5;
hence x + z <= y + z by A5, A6, Def2; ::_thesis: verum
end;
supposeA7: z in REAL ; ::_thesis: x + z <= y + z
x + z <= +infty by XXREAL_0:3;
hence x + z <= y + z by A5, A7, Def2; ::_thesis: verum
end;
suppose z = +infty ; ::_thesis: x + z <= y + z
hence x + z <= y + z by A5, Lm1, XXREAL_0:3; ::_thesis: verum
end;
end;
end;
supposeA8: ( x = -infty & y in REAL ) ; ::_thesis: x + z <= y + z
percases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14;
suppose z = -infty ; ::_thesis: x + z <= y + z
hence x + z <= y + z by A8, Lm2, XXREAL_0:5; ::_thesis: verum
end;
supposeA9: z in REAL ; ::_thesis: x + z <= y + z
-infty <= y + z by XXREAL_0:5;
hence x + z <= y + z by A8, A9, Def2; ::_thesis: verum
end;
supposeA10: z = +infty ; ::_thesis: x + z <= y + z
x + z <= +infty by XXREAL_0:3;
hence x + z <= y + z by A8, A10, Def2; ::_thesis: verum
end;
end;
end;
supposeA11: ( x = -infty & y = +infty ) ; ::_thesis: x + z <= y + z
percases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14;
suppose z = -infty ; ::_thesis: x + z <= y + z
hence x + z <= y + z by A11, Lm2; ::_thesis: verum
end;
supposeA12: z in REAL ; ::_thesis: x + z <= y + z
-infty <= y + z by XXREAL_0:5;
hence x + z <= y + z by A11, A12, Def2; ::_thesis: verum
end;
suppose z = +infty ; ::_thesis: x + z <= y + z
hence x + z <= y + z by A11, Lm1; ::_thesis: verum
end;
end;
end;
suppose x = +infty ; ::_thesis: x + z <= y + z
hence x + z <= y + z by A1, XXREAL_0:4; ::_thesis: verum
end;
suppose y = -infty ; ::_thesis: x + z <= y + z
hence x + z <= y + z by A1, XXREAL_0:6; ::_thesis: verum
end;
end;
end;
Lm13: for x, y being ext-real number st x >= 0 & y > 0 holds
x + y > 0
proof
let x, y be ext-real number ; ::_thesis: ( x >= 0 & y > 0 implies x + y > 0 )
assume x >= 0 ; ::_thesis: ( not y > 0 or x + y > 0 )
then x + y >= 0 + y by Lm12;
hence ( not y > 0 or x + y > 0 ) by Th4; ::_thesis: verum
end;
Lm14: for x, y being ext-real number st x <= 0 & y < 0 holds
x + y < 0
proof
let x, y be ext-real number ; ::_thesis: ( x <= 0 & y < 0 implies x + y < 0 )
assume x <= 0 ; ::_thesis: ( not y < 0 or x + y < 0 )
then x + y <= 0 + y by Lm12;
hence ( not y < 0 or x + y < 0 ) by Th4; ::_thesis: verum
end;
registration
let x, y be ext-real non negative number ;
clusterx + y -> ext-real non negative ;
coherence
not x + y is negative
proof
percases ( x = 0 or x > 0 ) ;
suppose x = 0 ; ::_thesis: not x + y is negative
hence x + y >= 0 by Th4; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
suppose x > 0 ; ::_thesis: not x + y is negative
hence x + y >= 0 by Lm13; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
end;
end;
end;
registration
let x, y be ext-real non positive number ;
clusterx + y -> ext-real non positive ;
coherence
not x + y is positive
proof
percases ( x = 0 or x < 0 ) ;
suppose x = 0 ; ::_thesis: not x + y is positive
hence x + y <= 0 by Th4; :: according to XXREAL_0:def_6 ::_thesis: verum
end;
suppose x < 0 ; ::_thesis: not x + y is positive
hence x + y <= 0 by Lm14; :: according to XXREAL_0:def_6 ::_thesis: verum
end;
end;
end;
end;
registration
let x be ext-real positive number ;
let y be ext-real non negative number ;
clusterx + y -> ext-real positive ;
coherence
x + y is positive by Lm13;
clustery + x -> ext-real positive ;
coherence
y + x is positive ;
end;
registration
let x be ext-real negative number ;
let y be ext-real non positive number ;
clusterx + y -> ext-real negative ;
coherence
x + y is negative by Lm14;
clustery + x -> ext-real negative ;
coherence
y + x is negative ;
end;
registration
let x be ext-real non positive number ;
cluster - x -> ext-real non negative ;
coherence
not - x is negative
proof
assume - x < 0 ; :: according to XXREAL_0:def_7 ::_thesis: contradiction
then (- x) - (- x) < 0 ;
hence contradiction by Th7; ::_thesis: verum
end;
end;
registration
let x be ext-real non negative number ;
cluster - x -> ext-real non positive ;
coherence
not - x is positive
proof
assume - x > 0 ; :: according to XXREAL_0:def_6 ::_thesis: contradiction
then (- x) - (- x) > 0 ;
hence contradiction by Th7; ::_thesis: verum
end;
end;
registration
let x be ext-real positive number ;
cluster - x -> ext-real negative ;
coherence
- x is negative
proof
assume - x >= 0 ; :: according to XXREAL_0:def_7 ::_thesis: contradiction
then (- x) - (- x) > 0 ;
hence contradiction by Th7; ::_thesis: verum
end;
end;
registration
let x be ext-real negative number ;
cluster - x -> ext-real positive ;
coherence
- x is positive
proof
assume - x <= 0 ; :: according to XXREAL_0:def_6 ::_thesis: contradiction
then (- x) - (- x) < 0 ;
hence contradiction by Th7; ::_thesis: verum
end;
end;
registration
let x be ext-real non negative number ;
let y be ext-real non positive number ;
clusterx - y -> ext-real non negative ;
coherence
not x - y is negative ;
clustery - x -> ext-real non positive ;
coherence
not y - x is positive ;
end;
registration
let x be ext-real positive number ;
let y be ext-real non positive number ;
clusterx - y -> ext-real positive ;
coherence
x - y is positive ;
clustery - x -> ext-real negative ;
coherence
y - x is negative ;
end;
registration
let x be ext-real negative number ;
let y be ext-real non negative number ;
clusterx - y -> ext-real negative ;
coherence
x - y is negative ;
clustery - x -> ext-real positive ;
coherence
y - x is positive ;
end;
Lm15: for x, y being ext-real number st x <= y holds
- y <= - x
proof
let x, y be ext-real number ; ::_thesis: ( x <= y implies - y <= - x )
assume A1: x <= y ; ::_thesis: - y <= - x
percases ( ( - y in REAL & - x in REAL ) or not - y in REAL or not - x in REAL ) ;
:: according to XXREAL_3:def_1
casethat A2: - y in REAL and
A3: - x in REAL ; ::_thesis: ex p, q being Element of REAL st
( p = - y & q = - x & p <= q )
x in REAL by A3, Lm3;
then consider a being complex number such that
A4: x = a and
A5: - x = - a by Def3;
y in REAL by A2, Lm3;
then consider b being complex number such that
A6: y = b and
A7: - y = - b by Def3;
( x in REAL & y in REAL ) by A2, A3, Lm3;
then reconsider a = a, b = b as real number by A6, A4;
reconsider mb = - b, ma = - a as Element of REAL by XREAL_0:def_1;
take mb ; ::_thesis: ex q being Element of REAL st
( mb = - y & q = - x & mb <= q )
take ma ; ::_thesis: ( mb = - y & ma = - x & mb <= ma )
thus ( mb = - y & ma = - x ) by A7, A5; ::_thesis: mb <= ma
thus mb <= ma by A1, A6, A4, XREAL_1:24; ::_thesis: verum
end;
case ( not - y in REAL or not - x in REAL ) ; ::_thesis: ( - y = -infty or - x = +infty )
then ( not y in REAL or not x in REAL ) by Lm3;
then ( x = -infty or y = +infty ) by A1, Def1;
hence ( - y = -infty or - x = +infty ) by Def3; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_3:35
for x, y, z being ext-real number st x <= y holds
x + z <= y + z by Lm12;
theorem Th36: :: XXREAL_3:36
for x, y, z, w being ext-real number st x <= y & z <= w holds
x + z <= y + w
proof
let x, y, z, w be ext-real number ; ::_thesis: ( x <= y & z <= w implies x + z <= y + w )
assume that
A1: x <= y and
A2: z <= w ; ::_thesis: x + z <= y + w
percases ( ( x = +infty & z = -infty ) or ( x = -infty & z = +infty ) or ( y = +infty & w = -infty ) or ( y = -infty & w = +infty ) or ( not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) & not ( y = +infty & w = -infty ) & not ( y = -infty & w = +infty ) ) ) ;
supposeA3: ( x = +infty & z = -infty ) ; ::_thesis: x + z <= y + w
A4: ( w <> -infty implies +infty + w = +infty ) by Def2;
y = +infty by A1, A3, XXREAL_0:4;
hence x + z <= y + w by A3, A4; ::_thesis: verum
end;
supposeA5: ( x = -infty & z = +infty ) ; ::_thesis: x + z <= y + w
A6: ( y <> -infty implies +infty + y = +infty ) by Def2;
w = +infty by A2, A5, XXREAL_0:4;
hence x + z <= y + w by A5, A6; ::_thesis: verum
end;
supposeA7: ( y = +infty & w = -infty ) ; ::_thesis: x + z <= y + w
A8: ( x <> +infty implies -infty + x = -infty ) by Def2;
z = -infty by A2, A7, XXREAL_0:6;
hence x + z <= y + w by A7, A8; ::_thesis: verum
end;
supposeA9: ( y = -infty & w = +infty ) ; ::_thesis: x + z <= y + w
A10: ( z <> +infty implies -infty + z = -infty ) by Def2;
x = -infty by A1, A9, XXREAL_0:6;
hence x + z <= y + w by A9, A10; ::_thesis: verum
end;
supposeA11: ( not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) & not ( y = +infty & w = -infty ) & not ( y = -infty & w = +infty ) ) ; ::_thesis: x + z <= y + w
reconsider a = x + z, b = y + w as Element of ExtREAL by XXREAL_0:def_1;
A12: ( not a = +infty or not b = -infty )
proof
assume that
A13: a = +infty and
A14: b = -infty ; ::_thesis: contradiction
( x = +infty or z = +infty ) by A13, Lm8;
hence contradiction by A1, A2, A11, A14, Lm9, XXREAL_0:4; ::_thesis: verum
end;
A15: ( a in REAL & b in REAL implies a <= b )
proof
assume A16: ( a in REAL & b in REAL ) ; ::_thesis: a <= b
then A17: ( z in REAL & w in REAL ) by A11, Th20;
( x in REAL & y in REAL ) by A11, A16, Th20;
then consider Ox, Oy, Os, Ot being real number such that
A18: ( Ox = x & Oy = y & Os = z & Ot = w ) and
A19: ( Ox <= Oy & Os <= Ot ) by A1, A2, A17;
( Ox + Os <= Os + Oy & Os + Oy <= Ot + Oy ) by A19, XREAL_1:6;
hence a <= b by A18, XXREAL_0:2; ::_thesis: verum
end;
A20: ( a = +infty & b in REAL implies a <= b )
proof
assume that
A21: a = +infty and
b in REAL ; ::_thesis: a <= b
( x = +infty or z = +infty ) by A21, Lm8;
then ( y = +infty or w = +infty ) by A1, A2, XXREAL_0:4;
then b = +infty by A11, Def2;
hence a <= b by XXREAL_0:4; ::_thesis: verum
end;
A22: ( a in REAL & b = -infty implies a <= b )
proof
assume that
a in REAL and
A23: b = -infty ; ::_thesis: a <= b
( y = -infty or w = -infty ) by A23, Lm9;
then ( x = -infty or z = -infty ) by A1, A2, XXREAL_0:6;
then a = -infty by A11, Def2;
hence a <= b by XXREAL_0:5; ::_thesis: verum
end;
( ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a in REAL & b = -infty ) or ( a = +infty & b in REAL ) or ( a = +infty & b = +infty ) or ( a = +infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a = -infty & b = -infty ) ) by XXREAL_0:14;
hence x + z <= y + w by A15, A22, A20, A12, XXREAL_0:4, XXREAL_0:5; ::_thesis: verum
end;
end;
end;
theorem Th37: :: XXREAL_3:37
for x, y, z, w being ext-real number st x <= y & z <= w holds
x - w <= y - z
proof
let x, y, z, w be ext-real number ; ::_thesis: ( x <= y & z <= w implies x - w <= y - z )
assume that
A1: x <= y and
A2: z <= w ; ::_thesis: x - w <= y - z
- w <= - z by A2, Lm15;
hence x - w <= y - z by A1, Th36; ::_thesis: verum
end;
theorem Th38: :: XXREAL_3:38
for x, y being ext-real number holds
( x <= y iff - y <= - x )
proof
let x, y be ext-real number ; ::_thesis: ( x <= y iff - y <= - x )
thus ( x <= y implies - y <= - x ) by Lm15; ::_thesis: ( - y <= - x implies x <= y )
( - y <= - x implies - (- x) <= - (- y) ) by Lm15;
hence ( - y <= - x implies x <= y ) ; ::_thesis: verum
end;
theorem Th39: :: XXREAL_3:39
for z, x being ext-real number st 0 <= z holds
x <= x + z
proof
let z, x be ext-real number ; ::_thesis: ( 0 <= z implies x <= x + z )
assume 0 <= z ; ::_thesis: x <= x + z
then x + 0 <= x + z by Th36;
hence x <= x + z by Th4; ::_thesis: verum
end;
theorem :: XXREAL_3:40
for x, y being ext-real number st x <= y holds
y - x >= 0
proof
let x, y be ext-real number ; ::_thesis: ( x <= y implies y - x >= 0 )
assume x <= y ; ::_thesis: y - x >= 0
then - y <= - x by Lm15;
then (- y) + y <= y + (- x) by Th36;
hence y - x >= 0 by Th7; ::_thesis: verum
end;
theorem :: XXREAL_3:41
for z, y, x being ext-real number st ( z = -infty & y = +infty implies x <= 0 ) & ( z = +infty & y = -infty implies x <= 0 ) & x - y <= z holds
x <= z + y
proof
let z, y, x be ext-real number ; ::_thesis: ( ( z = -infty & y = +infty implies x <= 0 ) & ( z = +infty & y = -infty implies x <= 0 ) & x - y <= z implies x <= z + y )
assume that
A1: ( z = -infty & y = +infty implies x <= 0 ) and
A2: ( z = +infty & y = -infty implies x <= 0 ) and
A3: x - y <= z ; ::_thesis: x <= z + y
percases ( z = -infty or z = +infty or z in REAL ) by XXREAL_0:14;
supposeA4: z = -infty ; ::_thesis: x <= z + y
percases ( x = -infty or y = +infty ) by A3, A4, Th19, XXREAL_0:6;
suppose x = -infty ; ::_thesis: x <= z + y
hence x <= z + y by XXREAL_0:5; ::_thesis: verum
end;
suppose y = +infty ; ::_thesis: x <= z + y
hence x <= z + y by A1, A4; ::_thesis: verum
end;
end;
end;
supposeA5: z = +infty ; ::_thesis: x <= z + y
percases ( y = -infty or y <> -infty ) ;
suppose y = -infty ; ::_thesis: x <= z + y
hence x <= z + y by A2, A5; ::_thesis: verum
end;
suppose y <> -infty ; ::_thesis: x <= z + y
then z + y = +infty by A5, Def2;
hence x <= z + y by XXREAL_0:3; ::_thesis: verum
end;
end;
end;
supposeA6: z in REAL ; ::_thesis: x <= z + y
percases ( x - y in REAL or x - y = -infty ) by A3, A6, XXREAL_0:13;
supposeA7: x - y in REAL ; ::_thesis: x <= z + y
percases ( y = +infty or x = -infty or ( x in REAL & y in REAL ) ) by A7, Th21;
suppose y = +infty ; ::_thesis: x <= z + y
then z + y = +infty by A6, Def2;
hence x <= z + y by XXREAL_0:3; ::_thesis: verum
end;
suppose x = -infty ; ::_thesis: x <= z + y
hence x <= z + y by XXREAL_0:5; ::_thesis: verum
end;
suppose ( x in REAL & y in REAL ) ; ::_thesis: x <= z + y
then reconsider a = x, b = y, c = z as Element of REAL by A6;
a - b <= c by A3;
then a <= b + c by XREAL_1:20;
hence x <= z + y ; ::_thesis: verum
end;
end;
end;
supposeA8: x - y = -infty ; ::_thesis: x <= z + y
percases ( x = -infty or y = +infty ) by A8, Th19;
suppose x = -infty ; ::_thesis: x <= z + y
hence x <= z + y by XXREAL_0:5; ::_thesis: verum
end;
suppose y = +infty ; ::_thesis: x <= z + y
then z + y = +infty by A6, Def2;
hence x <= z + y by XXREAL_0:3; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
theorem :: XXREAL_3:42
for x, y, z being ext-real number st ( x = +infty & y = +infty implies 0 <= z ) & ( x = -infty & y = -infty implies 0 <= z ) & x <= z + y holds
x - y <= z
proof
let x, y, z be ext-real number ; ::_thesis: ( ( x = +infty & y = +infty implies 0 <= z ) & ( x = -infty & y = -infty implies 0 <= z ) & x <= z + y implies x - y <= z )
assume that
A1: ( x = +infty & y = +infty implies 0 <= z ) and
A2: ( x = -infty & y = -infty implies 0 <= z ) and
A3: x <= z + y ; ::_thesis: x - y <= z
percases ( x = +infty or x = -infty or x in REAL ) by XXREAL_0:14;
supposeA4: x = +infty ; ::_thesis: x - y <= z
percases ( z = +infty or y = +infty ) by A3, A4, Lm8, XXREAL_0:4;
suppose z = +infty ; ::_thesis: x - y <= z
hence x - y <= z by XXREAL_0:3; ::_thesis: verum
end;
suppose y = +infty ; ::_thesis: x - y <= z
hence x - y <= z by A1, A4, Th7; ::_thesis: verum
end;
end;
end;
supposeA5: x = -infty ; ::_thesis: x - y <= z
percases ( y = -infty or - (- y) <> -infty ) ;
suppose y = -infty ; ::_thesis: x - y <= z
hence x - y <= z by A2, A5, Th7; ::_thesis: verum
end;
suppose - (- y) <> -infty ; ::_thesis: x - y <= z
then - y <> +infty by Def3;
then x - y = -infty by A5, Def2;
hence x - y <= z by XXREAL_0:5; ::_thesis: verum
end;
end;
end;
supposeA6: x in REAL ; ::_thesis: x - y <= z
percases ( z + y in REAL or z + y = +infty ) by A3, A6, XXREAL_0:10;
supposeA7: z + y in REAL ; ::_thesis: x - y <= z
percases ( y = +infty or z = +infty or ( z in REAL & y in REAL ) ) by A7, Th20;
suppose y = +infty ; ::_thesis: x - y <= z
then x - y = -infty by A6, Def2, Th5;
hence x - y <= z by XXREAL_0:5; ::_thesis: verum
end;
suppose z = +infty ; ::_thesis: x - y <= z
hence x - y <= z by XXREAL_0:3; ::_thesis: verum
end;
suppose ( z in REAL & y in REAL ) ; ::_thesis: x - y <= z
then reconsider a = x, b = y, c = z as Element of REAL by A6;
a <= b + c by A3;
then a - b <= c by XREAL_1:20;
hence x - y <= z ; ::_thesis: verum
end;
end;
end;
supposeA8: z + y = +infty ; ::_thesis: x - y <= z
percases ( z = +infty or y = +infty ) by A8, Lm8;
suppose z = +infty ; ::_thesis: x - y <= z
hence x - y <= z by XXREAL_0:3; ::_thesis: verum
end;
suppose y = +infty ; ::_thesis: x - y <= z
then x - y = -infty by A6, Def2, Th5;
hence x - y <= z by XXREAL_0:5; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
theorem Th43: :: XXREAL_3:43
for z, x, y being ext-real number st z in REAL & x < y holds
( x + z < y + z & x - z < y - z )
proof
let z, x, y be ext-real number ; ::_thesis: ( z in REAL & x < y implies ( x + z < y + z & x - z < y - z ) )
assume that
A1: z in REAL and
A2: x < y ; ::_thesis: ( x + z < y + z & x - z < y - z )
A3: x + z <> y + z
proof
assume x + z = y + z ; ::_thesis: contradiction
then x = (y + z) - z by A1, Th22
.= y by A1, Th22 ;
hence contradiction by A2; ::_thesis: verum
end;
A4: x - z <> y - z
proof
assume x - z = y - z ; ::_thesis: contradiction
then x = (y - z) + z by A1, Th22
.= y by A1, Th22 ;
hence contradiction by A2; ::_thesis: verum
end;
( x + z <= y + z & x - z <= y - z ) by A2, Th36;
hence ( x + z < y + z & x - z < y - z ) by A3, A4, XXREAL_0:1; ::_thesis: verum
end;
theorem :: XXREAL_3:44
for x, y, z being ext-real number st 0 <= x & 0 <= y & 0 <= z holds
(x + y) + z = x + (y + z)
proof
let x, y, z be ext-real number ; ::_thesis: ( 0 <= x & 0 <= y & 0 <= z implies (x + y) + z = x + (y + z) )
assume that
A1: 0 <= x and
A2: 0 <= y and
A3: 0 <= z ; ::_thesis: (x + y) + z = x + (y + z)
percases ( ( x in REAL & y in REAL & z in REAL ) or x = +infty or y = +infty or z = +infty ) by A1, A2, A3, XXREAL_0:14;
suppose ( x in REAL & y in REAL & z in REAL ) ; ::_thesis: (x + y) + z = x + (y + z)
then consider a, b, c, d, e being real number such that
A4: ( x = a & y = b & z = c ) and
x + y = d and
y + z = e ;
(x + y) + z = (a + b) + c by A4
.= a + (b + c)
.= x + (y + z) by A4 ;
hence (x + y) + z = x + (y + z) ; ::_thesis: verum
end;
supposeA5: x = +infty ; ::_thesis: (x + y) + z = x + (y + z)
then (x + y) + z = +infty + z by A2, Def2
.= +infty by A3, Def2
.= +infty + (y + z) by A2, A3, Def2 ;
hence (x + y) + z = x + (y + z) by A5; ::_thesis: verum
end;
supposeA6: y = +infty ; ::_thesis: (x + y) + z = x + (y + z)
then (x + y) + z = +infty + z by A1, Def2
.= +infty by A3, Def2
.= x + +infty by A1, Def2
.= x + (+infty + z) by A3, Def2 ;
hence (x + y) + z = x + (y + z) by A6; ::_thesis: verum
end;
supposeA7: z = +infty ; ::_thesis: (x + y) + z = x + (y + z)
then (x + y) + z = +infty by A1, A2, Def2
.= x + +infty by A1, Def2
.= x + (y + +infty) by A2, Def2 ;
hence (x + y) + z = x + (y + z) by A7; ::_thesis: verum
end;
end;
end;
theorem Th45: :: XXREAL_3:45
for x, y, z being ext-real number st x is real holds
( y + x <= z iff y <= z - x )
proof
let x, y, z be ext-real number ; ::_thesis: ( x is real implies ( y + x <= z iff y <= z - x ) )
assume A1: x is real ; ::_thesis: ( y + x <= z iff y <= z - x )
A2: (z - x) + x = z
proof
percases ( z in REAL or z = -infty or z = +infty ) by XXREAL_0:14;
suppose z in REAL ; ::_thesis: (z - x) + x = z
then reconsider a = x, b = z as real number by A1;
thus (z - x) + x = (b - a) + a
.= z ; ::_thesis: verum
end;
supposeA3: z = -infty ; ::_thesis: (z - x) + x = z
hence (z - x) + x = -infty + x by A1, Th14
.= z by A1, A3, Def2 ;
::_thesis: verum
end;
supposeA4: z = +infty ; ::_thesis: (z - x) + x = z
hence (z - x) + x = +infty + x by A1, Th13
.= z by A1, A4, Def2 ;
::_thesis: verum
end;
end;
end;
hereby ::_thesis: ( y <= z - x implies y + x <= z )
A5: (y + x) - x = y
proof
percases ( y in REAL or y = -infty or y = +infty ) by XXREAL_0:14;
suppose y in REAL ; ::_thesis: (y + x) - x = y
then reconsider a = x, b = y as Element of REAL by A1, XXREAL_0:14;
(y + x) - x = (b + a) - a
.= y ;
hence (y + x) - x = y ; ::_thesis: verum
end;
supposeA6: ( y = -infty or y = +infty ) ; ::_thesis: (y + x) - x = y
percases ( y = -infty or y = +infty ) by A6;
supposeA7: y = -infty ; ::_thesis: (y + x) - x = y
hence (y + x) - x = -infty - x by A1, Def2
.= y by A1, A7, Th14 ;
::_thesis: verum
end;
supposeA8: y = +infty ; ::_thesis: (y + x) - x = y
hence (y + x) - x = +infty - x by A1, Def2
.= y by A1, A8, Th13 ;
::_thesis: verum
end;
end;
end;
end;
end;
assume y + x <= z ; ::_thesis: y <= z - x
hence y <= z - x by A5, Th37; ::_thesis: verum
end;
assume y <= z - x ; ::_thesis: y + x <= z
hence y + x <= z by A2, Th36; ::_thesis: verum
end;
theorem Th46: :: XXREAL_3:46
for x, y being ext-real number st 0 < x & x < y holds
0 < y - x
proof
let x, y be ext-real number ; ::_thesis: ( 0 < x & x < y implies 0 < y - x )
assume that
A1: 0 < x and
A2: x < y ; ::_thesis: 0 < y - x
A3: x in REAL by A1, A2, XXREAL_0:48;
A4: 0 <> y - x
proof
assume 0 = y - x ; ::_thesis: contradiction
then x = (y - x) + x by Th4
.= y by A3, Th22 ;
hence contradiction by A2; ::_thesis: verum
end;
0 + x < y by A2, Th4;
hence 0 < y - x by A3, A4, Th45; ::_thesis: verum
end;
theorem :: XXREAL_3:47
for x, z, y being ext-real number st 0 <= x & 0 <= z & z + x < y holds
z < y - x
proof
let x, z, y be ext-real number ; ::_thesis: ( 0 <= x & 0 <= z & z + x < y implies z < y - x )
assume that
A1: 0 <= x and
A2: 0 <= z and
A3: z + x < y ; ::_thesis: z < y - x
x in REAL
proof
A4: x <> +infty
proof
assume x = +infty ; ::_thesis: contradiction
then +infty < y by A2, A3, Def2;
hence contradiction by XXREAL_0:4; ::_thesis: verum
end;
assume not x in REAL ; ::_thesis: contradiction
hence contradiction by A1, A4, XXREAL_0:10; ::_thesis: verum
end;
then ( z <= y - x & z <> y - x ) by A3, Th22, Th45;
hence z < y - x by XXREAL_0:1; ::_thesis: verum
end;
theorem :: XXREAL_3:48
for x, z, y being ext-real number st 0 <= x & 0 <= z & z + x < y holds
z <= y
proof
let x, z, y be ext-real number ; ::_thesis: ( 0 <= x & 0 <= z & z + x < y implies z <= y )
assume that
A1: 0 <= x and
A2: 0 <= z and
A3: z + x < y ; ::_thesis: z <= y
x in REAL
proof
A4: x <> +infty
proof
assume x = +infty ; ::_thesis: contradiction
then +infty < y by A2, A3, Def2;
hence contradiction by XXREAL_0:4; ::_thesis: verum
end;
assume not x in REAL ; ::_thesis: contradiction
hence contradiction by A1, A4, XXREAL_0:10; ::_thesis: verum
end;
then A5: (z + x) - x = z by Th22;
y - 0 = y by Th15;
hence z <= y by A1, A3, A5, Th37; ::_thesis: verum
end;
theorem Th49: :: XXREAL_3:49
for x, z being ext-real number st 0 <= x & x < z holds
ex y being real number st
( 0 < y & x + y < z )
proof
let x, z be ext-real number ; ::_thesis: ( 0 <= x & x < z implies ex y being real number st
( 0 < y & x + y < z ) )
assume that
A1: 0 <= x and
A2: x < z ; ::_thesis: ex y being real number st
( 0 < y & x + y < z )
percases ( 0 < x or 0 = x ) by A1;
supposeA3: 0 < x ; ::_thesis: ex y being real number st
( 0 < y & x + y < z )
then 0 < z - x by A2, Th46;
then consider y being real number such that
A4: 0 < y and
A5: y < z - x by Th3;
take y ; ::_thesis: ( 0 < y & x + y < z )
A6: x + y <= x + (z - x) by A5, Th36;
A7: x in REAL by A2, A3, XXREAL_0:48;
then A8: x + (z - x) = z by Th22;
x + y <> z by A7, A5, Th22;
hence ( 0 < y & x + y < z ) by A4, A6, A8, XXREAL_0:1; ::_thesis: verum
end;
supposeA9: 0 = x ; ::_thesis: ex y being real number st
( 0 < y & x + y < z )
consider y being real number such that
A10: ( 0 < y & y < z ) by A1, A2, Th3;
take y ; ::_thesis: ( 0 < y & x + y < z )
thus ( 0 < y & x + y < z ) by A9, A10, Th4; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_3:50
for x being ext-real number st 0 < x holds
ex y being real number st
( 0 < y & y + y < x )
proof
let x be ext-real number ; ::_thesis: ( 0 < x implies ex y being real number st
( 0 < y & y + y < x ) )
assume 0 < x ; ::_thesis: ex y being real number st
( 0 < y & y + y < x )
then consider x1 being real number such that
A1: 0 < x1 and
A2: x1 < x by Th3;
consider x2 being real number such that
A3: 0 < x2 and
A4: x1 + x2 < x by A1, A2, Th49;
take y = min (x1,x2); ::_thesis: ( 0 < y & y + y < x )
percases ( x1 <= x2 or x2 <= x1 ) ;
supposeA5: x1 <= x2 ; ::_thesis: ( 0 < y & y + y < x )
hence 0 < y by A1, XXREAL_0:def_9; ::_thesis: y + y < x
y = x1 by A5, XXREAL_0:def_9;
then y + y <= x1 + x2 by A5, Th36;
hence y + y < x by A4, XXREAL_0:2; ::_thesis: verum
end;
supposeA6: x2 <= x1 ; ::_thesis: ( 0 < y & y + y < x )
hence 0 < y by A3, XXREAL_0:def_9; ::_thesis: y + y < x
y = x2 by A6, XXREAL_0:def_9;
then y + y <= x1 + x2 by A6, Th36;
hence y + y < x by A4, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
theorem Th51: :: XXREAL_3:51
for x, y being ext-real number st x < y & x < +infty & -infty < y holds
0 < y - x
proof
let x, y be ext-real number ; ::_thesis: ( x < y & x < +infty & -infty < y implies 0 < y - x )
assume that
A1: x < y and
A2: x < +infty and
A3: -infty < y ; ::_thesis: 0 < y - x
percases ( y = +infty or y <> +infty ) ;
suppose y = +infty ; ::_thesis: 0 < y - x
hence 0 < y - x by A2, Th13; ::_thesis: verum
end;
supposeA4: y <> +infty ; ::_thesis: 0 < y - x
percases ( x = -infty or x <> -infty ) ;
suppose x = -infty ; ::_thesis: 0 < y - x
hence 0 < y - x by A3, Th14; ::_thesis: verum
end;
supposeA5: x <> -infty ; ::_thesis: 0 < y - x
A6: y in REAL by A3, A4, XXREAL_0:14;
x in REAL by A2, A5, XXREAL_0:14;
then reconsider a = x, b = y as real number by A6;
b - a > 0 by A1, XREAL_1:50;
hence 0 < y - x ; ::_thesis: verum
end;
end;
end;
end;
end;
theorem :: XXREAL_3:52
for x, y, z being ext-real number holds
( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y < z or ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) )
proof
let x, y, z be ext-real number ; ::_thesis: ( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y < z or ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) )
assume that
A1: ( not ( x = +infty & y = -infty ) & not ( x = -infty & y = +infty ) ) and
A2: x + y < z ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x < z - y )
percases ( z = +infty or z <> +infty ) ;
supposeA3: z = +infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x < z - y )
then x <> +infty by A1, A2, Def2;
then A4: x < +infty by XXREAL_0:4;
y <> +infty by A1, A2, A3, Def2;
hence ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) by A3, A4, Th13; ::_thesis: verum
end;
supposeA5: z <> +infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x < z - y )
A6: -infty <= x + y by XXREAL_0:5;
then z in REAL by A2, A5, XXREAL_0:14;
then reconsider c = z as real number ;
A7: x + y < +infty by A2, XXREAL_0:2, XXREAL_0:4;
then A8: x <> +infty by A1, Def2;
A9: y <> +infty by A1, A7, Def2;
percases ( y = -infty or y <> -infty ) ;
supposeA10: y = -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x < z - y )
then x < +infty by A1, XXREAL_0:4;
hence ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) by A2, A6, A10, Th14; ::_thesis: verum
end;
suppose y <> -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x < z - y )
then y in REAL by A9, XXREAL_0:14;
then reconsider b = y as real number ;
percases ( x = -infty or x <> -infty ) ;
supposeA11: x = -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x < z - y )
hence x <> +infty ; ::_thesis: ( y <> +infty & z <> -infty & x < z - y )
A12: z - y = c - b ;
hence y <> +infty ; ::_thesis: ( z <> -infty & x < z - y )
thus z <> -infty by A12; ::_thesis: x < z - y
c - b in REAL by XREAL_0:def_1;
hence x < z - y by A11, XXREAL_0:12; ::_thesis: verum
end;
suppose x <> -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x < z - y )
then x in REAL by A8, XXREAL_0:14;
then reconsider a = x as real number ;
x + y = a + b ;
then a < c - b by A2, XREAL_1:20;
hence ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) ; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
theorem :: XXREAL_3:53
for z, y, x being ext-real number holds
( ( z = +infty & y = +infty ) or ( z = -infty & y = -infty ) or not x < z - y or ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) )
proof
let z, y, x be ext-real number ; ::_thesis: ( ( z = +infty & y = +infty ) or ( z = -infty & y = -infty ) or not x < z - y or ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) )
assume that
A1: ( not ( z = +infty & y = +infty ) & not ( z = -infty & y = -infty ) ) and
A2: x < z - y ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z )
percases ( x = -infty or x <> -infty ) ;
supposeA3: x = -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z )
A4: -infty <= z by XXREAL_0:5;
z <> -infty by A1, A2, A3, Th14;
then A5: -infty < z by A4, XXREAL_0:1;
y <> +infty by A1, A2, A3, Th13;
hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) by A3, A5, Def2; ::_thesis: verum
end;
supposeA6: x <> -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z )
A7: z - y <= +infty by XXREAL_0:4;
then x in REAL by A2, A6, XXREAL_0:14;
then reconsider a = x as real number ;
A8: -infty <= x by XXREAL_0:5;
then A9: z <> -infty by A1, A2, Th14;
A10: y <> +infty by A1, A2, A8, Th13;
percases ( y = -infty or y <> -infty ) ;
supposeA11: y = -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z )
-infty <= z by XXREAL_0:5;
then -infty < z by A1, A11, XXREAL_0:1;
hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) by A2, A7, A11, Def2; ::_thesis: verum
end;
suppose y <> -infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z )
then y in REAL by A10, XXREAL_0:14;
then reconsider b = y as real number ;
percases ( z = +infty or z <> +infty ) ;
supposeA12: z = +infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z )
a + b in REAL by XREAL_0:def_1;
hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) by A12, XXREAL_0:9; ::_thesis: verum
end;
suppose z <> +infty ; ::_thesis: ( x <> +infty & y <> +infty & z <> -infty & x + y < z )
then z in REAL by A9, XXREAL_0:14;
then reconsider c = z as real number ;
z - y = c - b ;
then a + b < c by A2, XREAL_1:20;
hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) ; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
theorem :: XXREAL_3:54
for x, y, z being ext-real number holds
( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y < z or ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) )
proof
let x, y, z be ext-real number ; ::_thesis: ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y < z or ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) )
assume that
A1: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) ) and
A2: x - y < z ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y )
percases ( z = +infty or z <> +infty ) ;
supposeA3: z = +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y )
then x <> +infty by A1, A2, Th13;
then A4: x < +infty by XXREAL_0:4;
y <> -infty by A1, A2, A3, Th14;
hence ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) by A3, A4, Def2; ::_thesis: verum
end;
supposeA5: z <> +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y )
A6: -infty <= x - y by XXREAL_0:5;
then z in REAL by A2, A5, XXREAL_0:14;
then reconsider c = z as real number ;
A7: x - y < +infty by A2, XXREAL_0:2, XXREAL_0:4;
then A8: x <> +infty by A1, Th13;
A9: y <> -infty by A1, A7, Th14;
percases ( y = +infty or y <> +infty ) ;
supposeA10: y = +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y )
then x < +infty by A1, XXREAL_0:4;
hence ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) by A2, A6, A10, Def2; ::_thesis: verum
end;
suppose y <> +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y )
then y in REAL by A9, XXREAL_0:14;
then reconsider b = y as real number ;
percases ( x = -infty or x <> -infty ) ;
supposeA11: x = -infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y )
c + b in REAL by XREAL_0:def_1;
hence ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) by A11, XXREAL_0:12; ::_thesis: verum
end;
suppose x <> -infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y )
then x in REAL by A8, XXREAL_0:14;
then reconsider a = x as real number ;
x - y = a - b ;
then a < c + b by A2, XREAL_1:19;
hence ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) ; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
theorem :: XXREAL_3:55
for z, y, x being ext-real number holds
( ( z = +infty & y = -infty ) or ( z = -infty & y = +infty ) or not x < z + y or ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) )
proof
let z, y, x be ext-real number ; ::_thesis: ( ( z = +infty & y = -infty ) or ( z = -infty & y = +infty ) or not x < z + y or ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) )
assume that
A1: ( not ( z = +infty & y = -infty ) & not ( z = -infty & y = +infty ) ) and
A2: x < z + y ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z )
percases ( x = -infty or x <> -infty ) ;
supposeA3: x = -infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z )
A4: -infty <= z by XXREAL_0:5;
z <> -infty by A1, A2, A3, Def2;
then A5: -infty < z by A4, XXREAL_0:1;
y <> -infty by A1, A2, A3, Def2;
hence ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) by A3, A5, Th14; ::_thesis: verum
end;
supposeA6: x <> -infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z )
A7: z + y <= +infty by XXREAL_0:4;
then x in REAL by A2, A6, XXREAL_0:14;
then reconsider a = x as real number ;
A8: -infty <= x by XXREAL_0:5;
then A9: z <> -infty by A1, A2, Def2;
A10: y <> -infty by A1, A2, A8, Def2;
percases ( y = +infty or y <> +infty ) ;
supposeA11: y = +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z )
-infty <= z by XXREAL_0:5;
then -infty < z by A1, A11, XXREAL_0:1;
hence ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) by A2, A7, A11, Th13; ::_thesis: verum
end;
suppose y <> +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z )
then y in REAL by A10, XXREAL_0:14;
then reconsider b = y as real number ;
percases ( z = +infty or z <> +infty ) ;
supposeA12: z = +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z )
a - b in REAL by XREAL_0:def_1;
hence ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) by A12, XXREAL_0:9; ::_thesis: verum
end;
suppose z <> +infty ; ::_thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z )
then z in REAL by A9, XXREAL_0:14;
then reconsider c = z as real number ;
z + y = c + b ;
then a - b < c by A2, XREAL_1:19;
hence ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) ; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
theorem :: XXREAL_3:56
for x, y, z being ext-real number holds
( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or ( y = +infty & z = +infty ) or ( y = -infty & z = -infty ) or not x + y <= z or ( y <> +infty & x <= z - y ) )
proof
let x, y, z be ext-real number ; ::_thesis: ( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or ( y = +infty & z = +infty ) or ( y = -infty & z = -infty ) or not x + y <= z or ( y <> +infty & x <= z - y ) )
assume that
A1: ( not ( x = +infty & y = -infty ) & not ( x = -infty & y = +infty ) & not ( y = +infty & z = +infty ) & not ( y = -infty & z = -infty ) ) and
A2: x + y <= z ; ::_thesis: ( y <> +infty & x <= z - y )
thus y <> +infty ::_thesis: x <= z - y
proof
assume A3: y = +infty ; ::_thesis: contradiction
then x + y = +infty by A1, Def2;
hence contradiction by A1, A2, A3, XXREAL_0:4; ::_thesis: verum
end;
percases ( z = +infty or z <> +infty ) ;
suppose z = +infty ; ::_thesis: x <= z - y
then z - y = +infty by A1, Th13;
hence x <= z - y by XXREAL_0:4; ::_thesis: verum
end;
supposeA4: z <> +infty ; ::_thesis: x <= z - y
then A5: x + y < +infty by A2, XXREAL_0:2, XXREAL_0:4;
then A6: x <> +infty by A1, Def2;
A7: y <> +infty by A1, A5, Def2;
percases ( x = -infty or x <> -infty ) ;
suppose x = -infty ; ::_thesis: x <= z - y
hence x <= z - y by XXREAL_0:5; ::_thesis: verum
end;
suppose x <> -infty ; ::_thesis: x <= z - y
then x in REAL by A6, XXREAL_0:14;
then reconsider a = x as real number ;
percases ( y = -infty or y <> -infty ) ;
suppose y = -infty ; ::_thesis: x <= z - y
then z - y = +infty by A1, Th14;
hence x <= z - y by XXREAL_0:4; ::_thesis: verum
end;
suppose y <> -infty ; ::_thesis: x <= z - y
then y in REAL by A7, XXREAL_0:14;
then reconsider b = y as real number ;
a + b in REAL by XREAL_0:def_1;
then z <> -infty by A2, XXREAL_0:12;
then z in REAL by A4, XXREAL_0:14;
then reconsider c = z as real number ;
x + y = a + b ;
then a <= c - b by A2, XREAL_1:19;
hence x <= z - y ; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
theorem :: XXREAL_3:57
for x, y, z being ext-real number st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & x <= z - y holds
( y <> +infty & x + y <= z )
proof
let x, y, z be ext-real number ; ::_thesis: ( ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & x <= z - y implies ( y <> +infty & x + y <= z ) )
assume that
A1: ( not x = +infty or not y = -infty ) and
A2: ( not x = -infty or not y = +infty ) and
A3: ( not y = +infty or not z = +infty ) and
A4: x <= z - y ; ::_thesis: ( y <> +infty & x + y <= z )
thus A5: y <> +infty ::_thesis: x + y <= z
proof
assume A6: y = +infty ; ::_thesis: contradiction
then z - y = -infty by A3, Th13;
hence contradiction by A2, A4, A6, XXREAL_0:6; ::_thesis: verum
end;
percases ( y = -infty or ( y <> +infty & y <> -infty ) ) by A5;
suppose y = -infty ; ::_thesis: x + y <= z
then x + y = -infty by A1, Def2;
hence x + y <= z by XXREAL_0:5; ::_thesis: verum
end;
supposeA7: ( y <> +infty & y <> -infty ) ; ::_thesis: x + y <= z
- -infty = +infty by Def3;
then A8: - y <> -infty by A7;
- +infty = -infty by Def3;
then - y <> +infty by A7;
then (z - y) + y = z + ((- y) + y) by A7, A8, Th29
.= z + 0 by Th7
.= z by Th4 ;
hence x + y <= z by A4, Th36; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_3:58
for x, y, z being ext-real number holds
( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or ( y = +infty & z = -infty ) or ( y = -infty & z = +infty ) or not x - y <= z or y <> -infty )
proof
let x, y, z be ext-real number ; ::_thesis: ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or ( y = +infty & z = -infty ) or ( y = -infty & z = +infty ) or not x - y <= z or y <> -infty )
assume that
A1: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) & not ( y = +infty & z = -infty ) & not ( y = -infty & z = +infty ) ) and
A2: x - y <= z ; ::_thesis: y <> -infty
assume A3: y = -infty ; ::_thesis: contradiction
then x - y = +infty by A1, Th14;
hence contradiction by A1, A2, A3, XXREAL_0:4; ::_thesis: verum
end;
theorem :: XXREAL_3:59
for x, y, z being ext-real number st ( not x = -infty or not y = -infty ) & ( not y = -infty or not z = +infty ) & x <= z + y holds
y <> -infty
proof
let x, y, z be ext-real number ; ::_thesis: ( ( not x = -infty or not y = -infty ) & ( not y = -infty or not z = +infty ) & x <= z + y implies y <> -infty )
assume that
A1: ( not x = -infty or not y = -infty ) and
A2: ( not y = -infty or not z = +infty ) and
A3: x <= z + y ; ::_thesis: y <> -infty
assume A4: y = -infty ; ::_thesis: contradiction
then z + y = -infty by A2, Def2;
hence contradiction by A1, A3, A4, XXREAL_0:6; ::_thesis: verum
end;
theorem :: XXREAL_3:60
for x, y being ext-real number holds
( ( x <= - y implies y <= - x ) & ( - x <= y implies - y <= x ) )
proof
let x, y be ext-real number ; ::_thesis: ( ( x <= - y implies y <= - x ) & ( - x <= y implies - y <= x ) )
( x <= - y implies - (- y) <= - x ) by Th38;
hence ( x <= - y implies y <= - x ) ; ::_thesis: ( - x <= y implies - y <= x )
( - x <= y implies - y <= - (- x) ) by Th38;
hence ( - x <= y implies - y <= x ) ; ::_thesis: verum
end;
theorem :: XXREAL_3:61
for x, y being ext-real number st ( for e being real number st 0 < e holds
x < y + e ) holds
x <= y
proof
let x, y be ext-real number ; ::_thesis: ( ( for e being real number st 0 < e holds
x < y + e ) implies x <= y )
assume A1: for e being real number st 0 < e holds
x < y + e ; ::_thesis: x <= y
percases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ;
supposeA2: ( y = +infty or y = -infty ) ; ::_thesis: x <= y
percases ( y = +infty or y = -infty ) by A2;
suppose y = +infty ; ::_thesis: x <= y
hence x <= y by XXREAL_0:4; ::_thesis: verum
end;
supposeA3: y = -infty ; ::_thesis: x <= y
x < y + 1 by A1;
hence x <= y by A3, Def2; ::_thesis: verum
end;
end;
end;
supposeA4: ( y <> +infty & y <> -infty ) ; ::_thesis: x <= y
percases ( x = +infty or x <> +infty ) ;
supposeA5: x = +infty ; ::_thesis: x <= y
x < y + 1 by A1;
hence x <= y by A5, XXREAL_0:4; ::_thesis: verum
end;
supposeA6: x <> +infty ; ::_thesis: x <= y
now__::_thesis:_(_x_<>_-infty_implies_x_<=_y_)
assume A7: x <> -infty ; ::_thesis: x <= y
then x in REAL by A6, XXREAL_0:14;
then reconsider x1 = x as real number ;
-infty <= x by XXREAL_0:5;
then A8: -infty < x by A7, XXREAL_0:1;
y in REAL by A4, XXREAL_0:14;
then reconsider y1 = y as real number ;
assume A9: not x <= y ; ::_thesis: contradiction
y < +infty by A4, XXREAL_0:4;
then 0 < x - y by A9, A8, Th51;
then x < y + (x1 - y1) by A1;
then x < (y + x) - y by Th30;
then x < x + (y - y) by A4, Th30;
then x < x + 0 by Th7;
hence contradiction by Th4; ::_thesis: verum
end;
hence x <= y by XXREAL_0:5; ::_thesis: verum
end;
end;
end;
end;
end;
theorem :: XXREAL_3:62
for x, y, t being ext-real number st t <> -infty & t <> +infty & x < y holds
x + t < y + t
proof
let x, y, t be ext-real number ; ::_thesis: ( t <> -infty & t <> +infty & x < y implies x + t < y + t )
assume that
A1: ( t <> -infty & t <> +infty ) and
A2: x < y ; ::_thesis: x + t < y + t
A3: t - t = 0 by Th7;
A4: now__::_thesis:_not_x_+_t_=_y_+_t
assume x + t = y + t ; ::_thesis: contradiction
then x + (t - t) = (y + t) - t by A1, Th30;
then x + 0 = y + (t - t) by A1, A3, Th30;
then x = y + 0 by A3, Th4;
hence contradiction by A2, Th4; ::_thesis: verum
end;
x + t <= y + t by A2, Th36;
hence x + t < y + t by A4, XXREAL_0:1; ::_thesis: verum
end;
theorem :: XXREAL_3:63
for x, y, t being ext-real number st t <> -infty & t <> +infty & x < y holds
x - t < y - t
proof
let x, y, t be ext-real number ; ::_thesis: ( t <> -infty & t <> +infty & x < y implies x - t < y - t )
assume that
A1: ( t <> -infty & t <> +infty ) and
A2: x < y ; ::_thesis: x - t < y - t
A3: t - t = 0 by Th7;
A4: now__::_thesis:_not_x_-_t_=_y_-_t
assume x - t = y - t ; ::_thesis: contradiction
then x - (t - t) = (y - t) + t by A1, Th32;
then x - 0 = y - (t - t) by A1, A3, Th32;
then x = y + 0 by A3, Th4;
hence contradiction by A2, Th4; ::_thesis: verum
end;
x - t <= y - t by A2, Th37;
hence x - t < y - t by A4, XXREAL_0:1; ::_thesis: verum
end;
theorem :: XXREAL_3:64
for x, y, w, z being ext-real number st x < y & w < z holds
x + w < y + z
proof
let x, y, w, z be ext-real number ; ::_thesis: ( x < y & w < z implies x + w < y + z )
assume that
A2: x < y and
A3: w < z ; ::_thesis: x + w < y + z
-infty <= w by XXREAL_0:5;
percasesthen ( w = -infty or -infty < w ) by XXREAL_0:1;
supposeB2: w = -infty ; ::_thesis: x + w < y + z
B3: ( y <> -infty & z <> -infty ) by A2, A3, XXREAL_0:5;
x <> +infty by A2, XXREAL_0:3;
then x + w = -infty by B2, Def2;
hence x + w < y + z by B3, Lm9, XXREAL_0:6; ::_thesis: verum
end;
supposeA1: -infty < w ; ::_thesis: x + w < y + z
percases ( y = +infty or y <> +infty ) ;
supposeA4: y = +infty ; ::_thesis: x + w < y + z
A5: z <= +infty by XXREAL_0:4;
y + z = +infty by A1, A3, A4, Def2;
hence x + w < y + z by A2, A3, A4, A5, Lm8, XXREAL_0:4; ::_thesis: verum
end;
supposeA6: y <> +infty ; ::_thesis: x + w < y + z
-infty <= x by XXREAL_0:5;
then y in REAL by A2, A6, XXREAL_0:14;
then A7: y + w < y + z by A3, Th43;
z <= +infty by XXREAL_0:4;
then w in REAL by A1, A3, XXREAL_0:14;
then x + w < y + w by A2, Th43;
hence x + w < y + z by A7, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
end;
end;
theorem :: XXREAL_3:65
for x, z, y being ext-real number st 0 <= x & z + x <= y holds
z <= y
proof
let x, z, y be ext-real number ; ::_thesis: ( 0 <= x & z + x <= y implies z <= y )
assume 0 <= x ; ::_thesis: ( not z + x <= y or z <= y )
then z <= z + x by Th39;
hence ( not z + x <= y or z <= y ) by XXREAL_0:2; ::_thesis: verum
end;
begin
definition
let x, y be ext-real number ;
funcx * y -> ext-real number means :Def5: :: XXREAL_3:def 5
ex a, b being complex number st
( x = a & y = b & it = a * b ) if ( x is real & y is real )
it = +infty if ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) )
it = -infty if ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) )
otherwise it = 0 ;
existence
( ( x is real & y is real implies ex b1 being ext-real number ex a, b being complex number st
( x = a & y = b & b1 = a * b ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ex b1 being ext-real number st b1 = -infty ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies ex b1 being ext-real number st b1 = 0 ) )
proof
thus ( x is real & y is real implies ex c being ext-real number ex a, b being complex number st
( x = a & y = b & c = a * b ) ) ::_thesis: ( ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ex b1 being ext-real number st b1 = -infty ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies ex b1 being ext-real number st b1 = 0 ) )
proof
assume ( x is real & y is real ) ; ::_thesis: ex c being ext-real number ex a, b being complex number st
( x = a & y = b & c = a * b )
then reconsider a = x, b = y as real number ;
take a * b ; ::_thesis: ex a, b being complex number st
( x = a & y = b & a * b = a * b )
take a ; ::_thesis: ex b being complex number st
( x = a & y = b & a * b = a * b )
take b ; ::_thesis: ( x = a & y = b & a * b = a * b )
thus ( x = a & y = b & a * b = a * b ) ; ::_thesis: verum
end;
thus ( ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ex b1 being ext-real number st b1 = -infty ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies ex b1 being ext-real number st b1 = 0 ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being ext-real number holds
( ( x is real & y is real & ex a, b being complex number st
( x = a & y = b & b1 = a * b ) & ex a, b being complex number st
( x = a & y = b & b2 = a * b ) implies b1 = b2 ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) & b1 = +infty & b2 = +infty implies b1 = b2 ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) & b1 = -infty & b2 = -infty implies b1 = b2 ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) & b1 = 0 & b2 = 0 implies b1 = b2 ) ) ;
consistency
for b1 being ext-real number holds
( ( x is real & y is real & ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ( ex a, b being complex number st
( x = a & y = b & b1 = a * b ) iff b1 = +infty ) ) & ( x is real & y is real & ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( ex a, b being complex number st
( x = a & y = b & b1 = a * b ) iff b1 = -infty ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) & ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( b1 = +infty iff b1 = -infty ) ) ) ;
commutativity
for b1, x, y being ext-real number st ( x is real & y is real implies ex a, b being complex number st
( x = a & y = b & b1 = a * b ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies b1 = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies b1 = -infty ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies b1 = 0 ) holds
( ( y is real & x is real implies ex a, b being complex number st
( y = a & x = b & b1 = a * b ) ) & ( ( not y is real or not x is real ) & ( ( y is positive & x is positive ) or ( y is negative & x is negative ) ) implies b1 = +infty ) & ( ( not y is real or not x is real ) & ( ( y is positive & x is negative ) or ( y is negative & x is positive ) ) implies b1 = -infty ) & ( ( not y is real or not x is real ) & ( ( y is real & x is real ) or ( not ( y is positive & x is positive ) & not ( y is negative & x is negative ) ) ) & ( ( y is real & x is real ) or ( not ( y is positive & x is negative ) & not ( y is negative & x is positive ) ) ) implies b1 = 0 ) ) ;
end;
:: deftheorem Def5 defines * XXREAL_3:def_5_:_
for x, y, b3 being ext-real number holds
( ( x is real & y is real implies ( b3 = x * y iff ex a, b being complex number st
( x = a & y = b & b3 = a * b ) ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ( b3 = x * y iff b3 = +infty ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( b3 = x * y iff b3 = -infty ) ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies ( b3 = x * y iff b3 = 0 ) ) );
registration
let x, y be real number ;
let a, b be complex number ;
identifyx * y with a * b when x = a, y = b;
compatibility
( x = a & y = b implies x * y = a * b ) by Def5;
end;
definition
let x be ext-real number ;
funcx " -> ext-real number means :Def6: :: XXREAL_3:def 6
ex a being complex number st
( x = a & it = a " ) if x is real
otherwise it = 0 ;
existence
( ( x is real implies ex b1 being ext-real number ex a being complex number st
( x = a & b1 = a " ) ) & ( not x is real implies ex b1 being ext-real number st b1 = 0 ) )
proof
thus ( x is real implies ex c being ext-real number ex a being complex number st
( x = a & c = a " ) ) ::_thesis: ( not x is real implies ex b1 being ext-real number st b1 = 0 )
proof
assume x is real ; ::_thesis: ex c being ext-real number ex a being complex number st
( x = a & c = a " )
then reconsider a = x as real number ;
take a " ; ::_thesis: ex a being complex number st
( x = a & a " = a " )
take a ; ::_thesis: ( x = a & a " = a " )
thus ( x = a & a " = a " ) ; ::_thesis: verum
end;
thus ( not x is real implies ex b1 being ext-real number st b1 = 0 ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being ext-real number holds
( ( x is real & ex a being complex number st
( x = a & b1 = a " ) & ex a being complex number st
( x = a & b2 = a " ) implies b1 = b2 ) & ( not x is real & b1 = 0 & b2 = 0 implies b1 = b2 ) ) ;
consistency
for b1 being ext-real number holds verum ;
end;
:: deftheorem Def6 defines " XXREAL_3:def_6_:_
for x, b2 being ext-real number holds
( ( x is real implies ( b2 = x " iff ex a being complex number st
( x = a & b2 = a " ) ) ) & ( not x is real implies ( b2 = x " iff b2 = 0 ) ) );
registration
let x be real number ;
let a be complex number ;
identifyx " with a " when x = a;
compatibility
( x = a implies x " = a " ) by Def6;
end;
definition
let x, y be ext-real number ;
funcx / y -> ext-real number equals :: XXREAL_3:def 7
x * (y ");
coherence
x * (y ") is ext-real number ;
end;
:: deftheorem defines / XXREAL_3:def_7_:_
for x, y being ext-real number holds x / y = x * (y ");
registration
let x, y be real number ;
let a, b be complex number ;
identifyx / y with a / b when x = a, y = b;
compatibility
( x = a & y = b implies x / y = a / b )
proof
reconsider y1 = y " as real number ;
assume ( x = a & y = b ) ; ::_thesis: x / y = a / b
hence a / b = x * y1
.= x / y ;
::_thesis: verum
end;
end;
Lm16: for x being ext-real number holds x * 0 = 0
proof
let x be ext-real number ; ::_thesis: x * 0 = 0
percases ( x in REAL or x = +infty or x = -infty ) by XXREAL_0:14;
suppose x in REAL ; ::_thesis: x * 0 = 0
then ex a, b being complex number st
( x = a & 0 = b & x * 0 = a * b ) by Def5;
hence x * 0 = 0 ; ::_thesis: verum
end;
suppose x = +infty ; ::_thesis: x * 0 = 0
hence x * 0 = 0 by Def5; ::_thesis: verum
end;
suppose x = -infty ; ::_thesis: x * 0 = 0
hence x * 0 = 0 by Def5; ::_thesis: verum
end;
end;
end;
registration
let x be ext-real positive number ;
let y be ext-real negative number ;
clusterx * y -> ext-real negative ;
coherence
x * y is negative
proof
percases ( ( x in REAL & y in REAL ) or not x in REAL or not y in REAL ) ;
suppose ( x in REAL & y in REAL ) ; ::_thesis: x * y is negative
then reconsider x = x, y = y as real number ;
x * y < 0 ;
hence x * y is negative ; ::_thesis: verum
end;
suppose ( not x in REAL or not y in REAL ) ; ::_thesis: x * y is negative
then ( not x is real or not y is real ) by XREAL_0:def_1;
hence x * y is negative by Def5; ::_thesis: verum
end;
end;
end;
end;
registration
let x, y be ext-real negative number ;
clusterx * y -> ext-real positive ;
coherence
x * y is positive
proof
percases ( ( x in REAL & y in REAL ) or not x in REAL or not y in REAL ) ;
suppose ( x in REAL & y in REAL ) ; ::_thesis: x * y is positive
then reconsider x = x, y = y as real number ;
x * y > 0 ;
hence x * y is positive ; ::_thesis: verum
end;
suppose ( not x in REAL or not y in REAL ) ; ::_thesis: x * y is positive
then ( not x is real or not y is real ) by XREAL_0:def_1;
hence x * y is positive by Def5; ::_thesis: verum
end;
end;
end;
end;
registration
let x, y be ext-real positive number ;
clusterx * y -> ext-real positive ;
coherence
x * y is positive
proof
percases ( ( x in REAL & y in REAL ) or not x in REAL or not y in REAL ) ;
suppose ( x in REAL & y in REAL ) ; ::_thesis: x * y is positive
then reconsider x = x, y = y as real number ;
x * y > 0 ;
hence x * y is positive ; ::_thesis: verum
end;
suppose ( not x in REAL or not y in REAL ) ; ::_thesis: x * y is positive
then ( not x is real or not y is real ) by XREAL_0:def_1;
hence x * y is positive by Def5; ::_thesis: verum
end;
end;
end;
end;
registration
let x be ext-real non positive number ;
let y be ext-real non negative number ;
clusterx * y -> ext-real non positive ;
coherence
not x * y is positive
proof
percases ( x = 0 or y = 0 or ( x < 0 & y > 0 ) ) ;
suppose ( x = 0 or y = 0 ) ; ::_thesis: not x * y is positive
hence x * y <= 0 by Lm16; :: according to XXREAL_0:def_6 ::_thesis: verum
end;
suppose ( x < 0 & y > 0 ) ; ::_thesis: not x * y is positive
hence x * y <= 0 ; :: according to XXREAL_0:def_6 ::_thesis: verum
end;
end;
end;
end;
registration
let x, y be ext-real non positive number ;
clusterx * y -> ext-real non negative ;
coherence
not x * y is negative
proof
percases ( x = 0 or y = 0 or ( x < 0 & y < 0 ) ) ;
suppose ( x = 0 or y = 0 ) ; ::_thesis: not x * y is negative
hence x * y >= 0 by Lm16; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
suppose ( x < 0 & y < 0 ) ; ::_thesis: not x * y is negative
hence x * y >= 0 ; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
end;
end;
end;
registration
let x, y be ext-real non negative number ;
clusterx * y -> ext-real non negative ;
coherence
not x * y is negative
proof
percases ( x = 0 or y = 0 or ( x > 0 & y > 0 ) ) ;
suppose ( x = 0 or y = 0 ) ; ::_thesis: not x * y is negative
hence x * y >= 0 by Lm16; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
suppose ( x > 0 & y > 0 ) ; ::_thesis: not x * y is negative
hence x * y >= 0 ; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
end;
end;
end;
registration
let x be ext-real non positive number ;
clusterx " -> ext-real non positive ;
coherence
not x " is positive
proof
percases ( x is real or not x is real ) ;
suppose x is real ; ::_thesis: not x " is positive
then reconsider x = x as real number ;
not x " is positive ;
hence not x " is positive ; ::_thesis: verum
end;
suppose not x is real ; ::_thesis: not x " is positive
hence not x " is positive by Def6; ::_thesis: verum
end;
end;
end;
end;
registration
let x be ext-real non negative number ;
clusterx " -> ext-real non negative ;
coherence
not x " is negative
proof
percases ( x is real or not x is real ) ;
suppose x is real ; ::_thesis: not x " is negative
then reconsider x = x as real number ;
not x " is negative ;
hence not x " is negative ; ::_thesis: verum
end;
suppose not x is real ; ::_thesis: not x " is negative
hence not x " is negative by Def6; ::_thesis: verum
end;
end;
end;
end;
registration
let x be ext-real non negative number ;
let y be ext-real non positive number ;
clusterx / y -> ext-real non positive ;
coherence
not x / y is positive ;
clustery / x -> ext-real non positive ;
coherence
not y / x is positive ;
end;
registration
let x, y be ext-real non negative number ;
clusterx / y -> ext-real non negative ;
coherence
not x / y is negative ;
end;
registration
let x, y be ext-real non positive number ;
clusterx / y -> ext-real non negative ;
coherence
not x / y is negative ;
end;
Lm17: for x, y being ext-real number st not x is real & x * y = 0 holds
y = 0
proof
let x, y be ext-real number ; ::_thesis: ( not x is real & x * y = 0 implies y = 0 )
assume that
A1: not x is real and
A2: x * y = 0 ; ::_thesis: y = 0
( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) by A2;
hence y = 0 by A1, A2; ::_thesis: verum
end;
registration
let x, y be non zero ext-real number ;
clusterx * y -> non zero ext-real ;
coherence
not x * y is zero
proof
percases ( ( x is real & y is real ) or not x is real or not y is real ) ;
suppose ( x is real & y is real ) ; ::_thesis: not x * y is zero
then reconsider r = x, s = y as real number ;
assume x * y is zero ; ::_thesis: contradiction
then r * s = 0 ;
hence contradiction ; ::_thesis: verum
end;
suppose ( not x is real or not y is real ) ; ::_thesis: not x * y is zero
hence not x * y is zero by Lm17; ::_thesis: verum
end;
end;
end;
end;
registration
let x be zero ext-real number ;
let y be ext-real number ;
clusterx * y -> zero ext-real for ext-real number ;
coherence
for b1 being ext-real number st b1 = x * y holds
b1 is zero by Lm16;
end;
Lm18: for x, y, z being ext-real number st x = 0 holds
x * (y * z) = (x * y) * z
proof
let x, y, z be ext-real number ; ::_thesis: ( x = 0 implies x * (y * z) = (x * y) * z )
assume A1: x = 0 ; ::_thesis: x * (y * z) = (x * y) * z
hence x * (y * z) = 0
.= (x * y) * z by A1 ;
::_thesis: verum
end;
Lm19: for y, x, z being ext-real number st y = 0 holds
x * (y * z) = (x * y) * z
proof
let y, x, z be ext-real number ; ::_thesis: ( y = 0 implies x * (y * z) = (x * y) * z )
assume A1: y = 0 ; ::_thesis: x * (y * z) = (x * y) * z
hence x * (y * z) = 0
.= (x * y) * z by A1 ;
::_thesis: verum
end;
Lm20: for y, x, z being ext-real number st not y is real holds
x * (y * z) = (x * y) * z
proof
let y, x, z be ext-real number ; ::_thesis: ( not y is real implies x * (y * z) = (x * y) * z )
assume not y is real ; ::_thesis: x * (y * z) = (x * y) * z
then A1: not y in REAL ;
assume A2: not x * (y * z) = (x * y) * z ; ::_thesis: contradiction
then A3: ( x <> 0 & z <> 0 ) by Lm18;
percases ( y = -infty or y = +infty ) by A1, XXREAL_0:14;
supposeA4: y = -infty ; ::_thesis: contradiction
percases ( ( x is positive & z is positive ) or ( x is positive & z is negative ) or ( x is negative & z is positive ) or ( x is negative & z is negative ) ) by A3;
supposeA5: ( x is positive & z is positive ) ; ::_thesis: contradiction
then x * (-infty * z) = x * -infty by Def5
.= -infty by A5, Def5
.= -infty * z by A5, Def5
.= (x * -infty) * z by A5, Def5 ;
hence contradiction by A2, A4; ::_thesis: verum
end;
supposeA6: ( x is positive & z is negative ) ; ::_thesis: contradiction
then x * (-infty * z) = x * +infty by Def5
.= +infty by A6, Def5
.= -infty * z by A6, Def5
.= (x * -infty) * z by A6, Def5 ;
hence contradiction by A2, A4; ::_thesis: verum
end;
supposeA7: ( x is negative & z is positive ) ; ::_thesis: contradiction
then x * (-infty * z) = x * -infty by Def5
.= +infty by A7, Def5
.= +infty * z by A7, Def5
.= (x * -infty) * z by A7, Def5 ;
hence contradiction by A2, A4; ::_thesis: verum
end;
supposeA8: ( x is negative & z is negative ) ; ::_thesis: contradiction
then x * (-infty * z) = x * +infty by Def5
.= -infty by A8, Def5
.= +infty * z by A8, Def5
.= (x * -infty) * z by A8, Def5 ;
hence contradiction by A2, A4; ::_thesis: verum
end;
end;
end;
supposeA9: y = +infty ; ::_thesis: contradiction
percases ( ( x is positive & z is positive ) or ( x is positive & z is negative ) or ( x is negative & z is positive ) or ( x is negative & z is negative ) ) by A3;
supposeA10: ( x is positive & z is positive ) ; ::_thesis: contradiction
then x * (+infty * z) = x * +infty by Def5
.= +infty by A10, Def5
.= +infty * z by A10, Def5
.= (x * +infty) * z by A10, Def5 ;
hence contradiction by A2, A9; ::_thesis: verum
end;
supposeA11: ( x is positive & z is negative ) ; ::_thesis: contradiction
then x * (+infty * z) = x * -infty by Def5
.= -infty by A11, Def5
.= +infty * z by A11, Def5
.= (x * +infty) * z by A11, Def5 ;
hence contradiction by A2, A9; ::_thesis: verum
end;
supposeA12: ( x is negative & z is positive ) ; ::_thesis: contradiction
then x * (+infty * z) = x * +infty by Def5
.= -infty by A12, Def5
.= -infty * z by A12, Def5
.= (x * +infty) * z by A12, Def5 ;
hence contradiction by A2, A9; ::_thesis: verum
end;
supposeA13: ( x is negative & z is negative ) ; ::_thesis: contradiction
then x * (+infty * z) = x * -infty by Def5
.= +infty by A13, Def5
.= -infty * z by A13, Def5
.= (x * +infty) * z by A13, Def5 ;
hence contradiction by A2, A9; ::_thesis: verum
end;
end;
end;
end;
end;
Lm21: for x, y, z being ext-real number st not x is real holds
x * (y * z) = (x * y) * z
proof
let x, y, z be ext-real number ; ::_thesis: ( not x is real implies x * (y * z) = (x * y) * z )
assume not x is real ; ::_thesis: x * (y * z) = (x * y) * z
then A1: not x in REAL ;
assume A2: not x * (y * z) = (x * y) * z ; ::_thesis: contradiction
then A3: ( y <> 0 & z <> 0 ) by Lm18, Lm19;
percases ( x = -infty or x = +infty ) by A1, XXREAL_0:14;
supposeA4: x = -infty ; ::_thesis: contradiction
percases ( ( y is positive & z is positive ) or ( y is positive & z is negative ) or ( y is negative & z is positive ) or ( y is negative & z is negative ) ) by A3;
supposeA5: ( y is positive & z is positive ) ; ::_thesis: contradiction
then -infty * (y * z) = -infty by Def5
.= -infty * z by A5, Def5
.= (-infty * y) * z by A5, Def5 ;
hence contradiction by A2, A4; ::_thesis: verum
end;
supposeA6: ( y is positive & z is negative ) ; ::_thesis: contradiction
then -infty * (y * z) = +infty by Def5
.= -infty * z by A6, Def5
.= (-infty * y) * z by A6, Def5 ;
hence contradiction by A2, A4; ::_thesis: verum
end;
supposeA7: ( y is negative & z is positive ) ; ::_thesis: contradiction
then -infty * (y * z) = +infty by Def5
.= +infty * z by A7, Def5
.= (-infty * y) * z by A7, Def5 ;
hence contradiction by A2, A4; ::_thesis: verum
end;
supposeA8: ( y is negative & z is negative ) ; ::_thesis: contradiction
then -infty * (y * z) = -infty by Def5
.= +infty * z by A8, Def5
.= (-infty * y) * z by A8, Def5 ;
hence contradiction by A2, A4; ::_thesis: verum
end;
end;
end;
supposeA9: x = +infty ; ::_thesis: contradiction
percases ( ( y is positive & z is positive ) or ( y is positive & z is negative ) or ( y is negative & z is positive ) or ( y is negative & z is negative ) ) by A3;
supposeA10: ( y is positive & z is positive ) ; ::_thesis: contradiction
then +infty * (y * z) = +infty by Def5
.= +infty * z by A10, Def5
.= (+infty * y) * z by A10, Def5 ;
hence contradiction by A2, A9; ::_thesis: verum
end;
supposeA11: ( y is positive & z is negative ) ; ::_thesis: contradiction
then +infty * (y * z) = -infty by Def5
.= +infty * z by A11, Def5
.= (+infty * y) * z by A11, Def5 ;
hence contradiction by A2, A9; ::_thesis: verum
end;
supposeA12: ( y is negative & z is positive ) ; ::_thesis: contradiction
then +infty * (y * z) = -infty by Def5
.= -infty * z by A12, Def5
.= (+infty * y) * z by A12, Def5 ;
hence contradiction by A2, A9; ::_thesis: verum
end;
supposeA13: ( y is negative & z is negative ) ; ::_thesis: contradiction
then +infty * (y * z) = +infty by Def5
.= -infty * z by A13, Def5
.= (+infty * y) * z by A13, Def5 ;
hence contradiction by A2, A9; ::_thesis: verum
end;
end;
end;
end;
end;
theorem Th66: :: XXREAL_3:66
for x, y, z being ext-real number holds x * (y * z) = (x * y) * z
proof
let x, y, z be ext-real number ; ::_thesis: x * (y * z) = (x * y) * z
percases ( ( x is real & y is real & z is real ) or not x is real or not z is real or not y is real ) ;
suppose ( x is real & y is real & z is real ) ; ::_thesis: x * (y * z) = (x * y) * z
then reconsider r = x, s = y, t = z as real number ;
reconsider rs = r * s, sx = s * t as real number ;
thus x * (y * z) = r * sx
.= rs * t
.= (x * y) * z ; ::_thesis: verum
end;
suppose ( not x is real or not z is real ) ; ::_thesis: x * (y * z) = (x * y) * z
hence x * (y * z) = (x * y) * z by Lm21; ::_thesis: verum
end;
suppose not y is real ; ::_thesis: x * (y * z) = (x * y) * z
hence x * (y * z) = (x * y) * z by Lm20; ::_thesis: verum
end;
end;
end;
registration
let r be real number ;
clusterr " -> ext-real real ;
coherence
r " is real ;
end;
registration
let r, s be real number ;
clusterr * s -> ext-real real ;
coherence
r * s is real ;
clusterr / s -> ext-real real ;
coherence
r / s is real ;
end;
registration
cluster-infty " -> zero ext-real ;
coherence
-infty " is zero by Def6;
cluster+infty " -> zero ext-real ;
coherence
+infty " is zero by Def6;
end;
theorem :: XXREAL_3:67
for f, g being ext-real number holds (f * g) " = (f ") * (g ")
proof
let f, g be ext-real number ; ::_thesis: (f * g) " = (f ") * (g ")
percases ( ( f in REAL & g in REAL ) or f = +infty or f = -infty or g = +infty or g = -infty ) by XXREAL_0:14;
suppose ( f in REAL & g in REAL ) ; ::_thesis: (f * g) " = (f ") * (g ")
then reconsider f1 = f, g1 = g as real number ;
A1: ( ex a being complex number st
( f1 = a & f " = a " ) & ex b being complex number st
( g1 = b & g " = b " ) ) by Def6;
then ex a, b being complex number st
( f " = a & g " = b & (f ") * (g ") = a * b ) by Def5;
then (f ") * (g ") = (f1 * g1) " by A1, XCMPLX_1:204;
hence (f * g) " = (f ") * (g ") ; ::_thesis: verum
end;
supposeA2: f = +infty ; ::_thesis: (f * g) " = (f ") * (g ")
( g is positive or g is negative or g = 0 ) ;
then ( (f * g) " = +infty " or (f * g) " = -infty " or (f * g) " = 0 " ) by A2, Def5;
hence (f * g) " = (f ") * (g ") by A2; ::_thesis: verum
end;
supposeA3: f = -infty ; ::_thesis: (f * g) " = (f ") * (g ")
( g is positive or g is negative or g = 0 ) ;
then ( (f * g) " = +infty " or (f * g) " = -infty " or (f * g) " = 0 " ) by A3, Def5;
hence (f * g) " = (f ") * (g ") by A3; ::_thesis: verum
end;
supposeA4: g = +infty ; ::_thesis: (f * g) " = (f ") * (g ")
( f is positive or f is negative or f = 0 ) ;
then ( (f * g) " = +infty " or (f * g) " = -infty " or (f * g) " = 0 " ) by A4, Def5;
hence (f * g) " = (f ") * (g ") by A4; ::_thesis: verum
end;
supposeA5: g = -infty ; ::_thesis: (f * g) " = (f ") * (g ")
( f is positive or f is negative or f = 0 ) ;
then ( (f * g) " = +infty " or (f * g) " = -infty " or (f * g) " = 0 " ) by A5, Def5;
hence (f * g) " = (f ") * (g ") by A5; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_3:68
for r being real number
for f, g being ext-real number st r <> 0 & r * f = r * g holds
f = g
proof
let r be real number ; ::_thesis: for f, g being ext-real number st r <> 0 & r * f = r * g holds
f = g
let f, g be ext-real number ; ::_thesis: ( r <> 0 & r * f = r * g implies f = g )
assume that
A1: r <> 0 and
A2: r * f = r * g ; ::_thesis: f = g
A3: ( r is positive or r is negative ) by A1;
percases ( f in REAL or f = +infty or f = -infty ) by XXREAL_0:14;
supposeA4: f in REAL ; ::_thesis: f = g
now__::_thesis:_g_in_REAL
assume not g in REAL ; ::_thesis: contradiction
then ( g = +infty or g = -infty ) by XXREAL_0:14;
hence contradiction by A2, A3, A4, Def5; ::_thesis: verum
end;
then A5: ex c, d being complex number st
( r = c & g = d & r * g = c * d ) by Def5;
ex a, b being complex number st
( r = a & f = b & r * f = a * b ) by A4, Def5;
hence f = g by A1, A2, A5, XCMPLX_1:5; ::_thesis: verum
end;
supposeA6: f = +infty ; ::_thesis: f = g
assume f <> g ; ::_thesis: contradiction
then ( g in REAL or g = -infty ) by A6, XXREAL_0:14;
hence contradiction by A2, A3, A6, Def5; ::_thesis: verum
end;
supposeA7: f = -infty ; ::_thesis: f = g
assume f <> g ; ::_thesis: contradiction
then ( g in REAL or g = +infty ) by A7, XXREAL_0:14;
hence contradiction by A2, A3, A7, Def5; ::_thesis: verum
end;
end;
end;
theorem Th69: :: XXREAL_3:69
for x, y being ext-real number st x <> +infty & x <> -infty & x * y = +infty & not y = +infty holds
y = -infty
proof
let x, y be ext-real number ; ::_thesis: ( x <> +infty & x <> -infty & x * y = +infty & not y = +infty implies y = -infty )
assume that
A1: ( x <> +infty & x <> -infty ) and
A2: x * y = +infty ; ::_thesis: ( y = +infty or y = -infty )
assume ( y <> +infty & y <> -infty ) ; ::_thesis: contradiction
then A3: y in REAL by XXREAL_0:14;
x in REAL by A1, XXREAL_0:14;
then reconsider a = x, b = y as real number by A3;
x * y = a * b ;
hence contradiction by A2; ::_thesis: verum
end;
theorem Th70: :: XXREAL_3:70
for x, y being ext-real number st x <> +infty & x <> -infty & x * y = -infty & not y = +infty holds
y = -infty
proof
let x, y be ext-real number ; ::_thesis: ( x <> +infty & x <> -infty & x * y = -infty & not y = +infty implies y = -infty )
assume that
A1: ( x <> +infty & x <> -infty ) and
A2: x * y = -infty ; ::_thesis: ( y = +infty or y = -infty )
assume ( y <> +infty & y <> -infty ) ; ::_thesis: contradiction
then A3: y in REAL by XXREAL_0:14;
x in REAL by A1, XXREAL_0:14;
then reconsider a = x, b = y as real number by A3;
x * y = a * b ;
hence contradiction by A2; ::_thesis: verum
end;
Lm22: for x, y being ext-real number holds
( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 )
proof
let x, y be ext-real number ; ::_thesis: ( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 )
assume A1: x * y in REAL ; ::_thesis: ( ( x in REAL & y in REAL ) or x * y = 0 )
assume ( not x in REAL or not y in REAL ) ; ::_thesis: x * y = 0
then A2: ( not x is real or not y is real ) by XREAL_0:def_1;
assume A3: x * y <> 0 ; ::_thesis: contradiction
percases ( ( x is positive & y is positive ) or ( x is negative & y is negative ) or ( x is positive & y is negative ) or ( x is negative & y is positive ) ) by A3;
suppose ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) ; ::_thesis: contradiction
hence contradiction by A1, A2, Def5; ::_thesis: verum
end;
suppose ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) ; ::_thesis: contradiction
hence contradiction by A1, A2, Def5; ::_thesis: verum
end;
end;
end;
theorem Th71: :: XXREAL_3:71
for x, y, z being ext-real number st x <= y & 0 <= z holds
x * z <= y * z
proof
let x, y, z be ext-real number ; ::_thesis: ( x <= y & 0 <= z implies x * z <= y * z )
assume that
A1: x <= y and
A2: 0 <= z ; ::_thesis: x * z <= y * z
percases ( z = 0 or z > 0 ) by A2;
suppose z = 0 ; ::_thesis: x * z <= y * z
hence x * z <= y * z ; ::_thesis: verum
end;
supposeA3: z > 0 ; ::_thesis: x * z <= y * z
percases ( x = 0 or x <> 0 ) ;
supposeA4: x = 0 ; ::_thesis: x * z <= y * z
then z * y >= 0 by A1, A2;
hence x * z <= y * z by A4; ::_thesis: verum
end;
supposeA5: x <> 0 ; ::_thesis: x * z <= y * z
percases ( ( x * z in REAL & y * z in REAL ) or not x * z in REAL or not y * z in REAL ) ;
:: according to XXREAL_3:def_1
caseA6: ( x * z in REAL & y * z in REAL ) ; ::_thesis: ex p, q being Element of REAL st
( p = x * z & q = y * z & p <= q )
( y * z = 0 implies y = 0 ) by A3;
then reconsider x = x, y = y, z = z as Element of REAL by A3, A5, A6, Lm22;
reconsider p = x * z, q = y * z as Element of REAL by XREAL_0:def_1;
take p ; ::_thesis: ex q being Element of REAL st
( p = x * z & q = y * z & p <= q )
take q ; ::_thesis: ( p = x * z & q = y * z & p <= q )
thus ( p = x * z & q = y * z & p <= q ) by A1, A2, XREAL_1:64; ::_thesis: verum
end;
caseA7: ( not x * z in REAL or not y * z in REAL ) ; ::_thesis: ( x * z = -infty or y * z = +infty )
percases ( not x * z in REAL or not y * z in REAL ) by A7;
supposeA8: not x * z in REAL ; ::_thesis: ( x * z = -infty or y * z = +infty )
percases ( x * z = -infty or x * z = +infty ) by A8, XXREAL_0:14;
suppose x * z = -infty ; ::_thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) ; ::_thesis: verum
end;
suppose x * z = +infty ; ::_thesis: ( x * z = -infty or y * z = +infty )
then A9: x <> -infty by A3;
A10: ( not x in REAL or not y in REAL or not z in REAL ) by A8, XREAL_0:def_1;
percases ( y = +infty or x = +infty or y = -infty or ( not z in REAL & x in REAL & y in REAL ) ) by A9, A10, XXREAL_0:14;
suppose y = +infty ; ::_thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A3, Def5; ::_thesis: verum
end;
suppose x = +infty ; ::_thesis: ( x * z = -infty or y * z = +infty )
then y = +infty by A1, XXREAL_0:4;
hence ( x * z = -infty or y * z = +infty ) by A3, Def5; ::_thesis: verum
end;
suppose y = -infty ; ::_thesis: ( x * z = -infty or y * z = +infty )
then x = -infty by A1, XXREAL_0:6;
hence ( x * z = -infty or y * z = +infty ) by A3, Def5; ::_thesis: verum
end;
supposethat A11: not z in REAL and
( x in REAL & y in REAL ) ; ::_thesis: ( x * z = -infty or y * z = +infty )
A12: z = +infty by A3, A11, XXREAL_0:14;
percases ( x < 0 or 0 < x ) by A5;
suppose x < 0 ; ::_thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A12, Def5; ::_thesis: verum
end;
suppose 0 < x ; ::_thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A1, A12, Def5; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
suppose not y * z in REAL ; ::_thesis: ( x * z = -infty or y * z = +infty )
then A13: ( not x in REAL or not y in REAL or not z in REAL ) by XREAL_0:def_1;
percases ( x = -infty or y = +infty or x = +infty or y = -infty or ( not z in REAL & x in REAL & y in REAL ) ) by A13, XXREAL_0:14;
suppose x = -infty ; ::_thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A3, Def5; ::_thesis: verum
end;
suppose y = +infty ; ::_thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A3, Def5; ::_thesis: verum
end;
suppose x = +infty ; ::_thesis: ( x * z = -infty or y * z = +infty )
then y = +infty by A1, XXREAL_0:4;
hence ( x * z = -infty or y * z = +infty ) by A3, Def5; ::_thesis: verum
end;
suppose y = -infty ; ::_thesis: ( x * z = -infty or y * z = +infty )
then x = -infty by A1, XXREAL_0:6;
hence ( x * z = -infty or y * z = +infty ) by A3, Def5; ::_thesis: verum
end;
supposethat A14: not z in REAL and
( x in REAL & y in REAL ) ; ::_thesis: ( x * z = -infty or y * z = +infty )
A15: z = +infty by A3, A14, XXREAL_0:14;
percases ( x < 0 or 0 < x ) by A5;
suppose x < 0 ; ::_thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A15, Def5; ::_thesis: verum
end;
suppose 0 < x ; ::_thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A1, A15, Def5; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;
theorem Th72: :: XXREAL_3:72
for x, y, z being ext-real number st x < y & 0 < z & z <> +infty holds
x * z < y * z
proof
let x, y, z be ext-real number ; ::_thesis: ( x < y & 0 < z & z <> +infty implies x * z < y * z )
assume that
A1: x < y and
A2: 0 < z and
A3: z <> +infty ; ::_thesis: x * z < y * z
A4: now__::_thesis:_not_x_*_z_=_y_*_z
A5: ( x <> +infty & y <> -infty ) by A1, XXREAL_0:3, XXREAL_0:5;
assume A6: x * z = y * z ; ::_thesis: contradiction
percases ( ( x in REAL & y in REAL ) or y = +infty or x = -infty ) by A5, XXREAL_0:14;
supposeA7: ( x in REAL & y in REAL ) ; ::_thesis: contradiction
z in REAL by A2, A3, XXREAL_0:14;
then reconsider x = x, y = y, z = z as real number by A7;
x * z < y * z by A1, A2, XREAL_1:68;
hence contradiction by A6; ::_thesis: verum
end;
supposeA8: y = +infty ; ::_thesis: contradiction
then y * z = +infty by A2, Def5;
then ( x = +infty or x = -infty ) by A2, A3, A6, Th69;
hence contradiction by A1, A2, A6, A8; ::_thesis: verum
end;
supposeA9: x = -infty ; ::_thesis: contradiction
then x * z = -infty by A2, Def5;
then ( y = +infty or y = -infty ) by A2, A3, A6, Th70;
hence contradiction by A1, A2, A6, A9; ::_thesis: verum
end;
end;
end;
x * z <= y * z by A1, A2, Th71;
hence x * z < y * z by A4, XXREAL_0:1; ::_thesis: verum
end;
theorem :: XXREAL_3:73
for x, y being ext-real number holds
( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 ) by Lm22;
theorem :: XXREAL_3:74
+infty " = 0 ;
theorem :: XXREAL_3:75
-infty " = 0 ;
theorem :: XXREAL_3:76
for x being ext-real number holds x / +infty = 0 ;
theorem :: XXREAL_3:77
for x being ext-real number holds x / -infty = 0 ;
theorem Th78: :: XXREAL_3:78
for x being ext-real number st x <> -infty & x <> +infty & x <> 0 holds
x / x = 1
proof
let x be ext-real number ; ::_thesis: ( x <> -infty & x <> +infty & x <> 0 implies x / x = 1 )
assume ( x <> -infty & x <> +infty ) ; ::_thesis: ( not x <> 0 or x / x = 1 )
then x in REAL by XXREAL_0:14;
then reconsider a = x as real number ;
assume x <> 0 ; ::_thesis: x / x = 1
then a / a = 1 by XCMPLX_1:60;
hence x / x = 1 ; ::_thesis: verum
end;
theorem :: XXREAL_3:79
for x, y, z being ext-real number st x <= y & 0 < z holds
x / z <= y / z by Th71;
theorem :: XXREAL_3:80
for x, y, z being ext-real number st x < y & 0 < z & z <> +infty holds
x / z < y / z
proof
let x, y, z be ext-real number ; ::_thesis: ( x < y & 0 < z & z <> +infty implies x / z < y / z )
assume that
A1: x < y and
A2: 0 < z and
A3: z <> +infty ; ::_thesis: x / z < y / z
percases ( z = -infty or z in REAL ) by A3, XXREAL_0:14;
suppose z = -infty ; ::_thesis: x / z < y / z
hence x / z < y / z by A2; ::_thesis: verum
end;
suppose z in REAL ; ::_thesis: x / z < y / z
then reconsider z = z as real number ;
z " > 0 by A2;
hence x / z < y / z by A1, Th72; ::_thesis: verum
end;
end;
end;
theorem Th81: :: XXREAL_3:81
for x being ext-real number holds 1 * x = x
proof
let x be ext-real number ; ::_thesis: 1 * x = x
percases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14;
suppose x in REAL ; ::_thesis: 1 * x = x
then reconsider x = x, y = 1 as real number ;
y * x = x ;
hence 1 * x = x ; ::_thesis: verum
end;
suppose ( x = -infty or x = +infty ) ; ::_thesis: 1 * x = x
hence 1 * x = x by Def5; ::_thesis: verum
end;
end;
end;
theorem Th82: :: XXREAL_3:82
for y being ext-real number holds
( not y " = 0 or y = +infty or y = -infty or y = 0 )
proof
let y be ext-real number ; ::_thesis: ( not y " = 0 or y = +infty or y = -infty or y = 0 )
assume A1: y " = 0 ; ::_thesis: ( y = +infty or y = -infty or y = 0 )
assume ( y <> +infty & y <> -infty ) ; ::_thesis: y = 0
then y in REAL by XXREAL_0:14;
then reconsider y = y as real number ;
(y ") " = 0 by A1;
hence y = 0 ; ::_thesis: verum
end;
theorem Th83: :: XXREAL_3:83
for y being ext-real number st 0 < y & y <> +infty holds
+infty / y = +infty
proof
let y be ext-real number ; ::_thesis: ( 0 < y & y <> +infty implies +infty / y = +infty )
assume that
A1: 0 < y and
A2: y <> +infty ; ::_thesis: +infty / y = +infty
y " <> 0 by A1, A2, Th82;
hence +infty / y = +infty by A1, Def5; ::_thesis: verum
end;
theorem Th84: :: XXREAL_3:84
for y being ext-real number st y < 0 & -infty <> y holds
-infty / y = +infty
proof
let y be ext-real number ; ::_thesis: ( y < 0 & -infty <> y implies -infty / y = +infty )
assume that
A1: y < 0 and
A2: -infty <> y ; ::_thesis: -infty / y = +infty
y " <> 0 by A1, A2, Th82;
hence -infty / y = +infty by A1, Def5; ::_thesis: verum
end;
theorem Th85: :: XXREAL_3:85
for y being ext-real number st y < 0 & -infty <> y holds
+infty / y = -infty
proof
let y be ext-real number ; ::_thesis: ( y < 0 & -infty <> y implies +infty / y = -infty )
assume that
A1: y < 0 and
A2: -infty <> y ; ::_thesis: +infty / y = -infty
y " <> 0 by A1, A2, Th82;
hence +infty / y = -infty by A1, Def5; ::_thesis: verum
end;
theorem Th86: :: XXREAL_3:86
for y being ext-real number st 0 < y & y <> +infty holds
-infty / y = -infty
proof
let y be ext-real number ; ::_thesis: ( 0 < y & y <> +infty implies -infty / y = -infty )
assume that
A1: 0 < y and
A2: y <> +infty ; ::_thesis: -infty / y = -infty
y " <> 0 by A1, A2, Th82;
hence -infty / y = -infty by A1, Def5; ::_thesis: verum
end;
theorem :: XXREAL_3:87
for x being ext-real number st x <> +infty & x <> -infty & x <> 0 holds
( x * (1 / x) = 1 & (1 / x) * x = 1 )
proof
let x be ext-real number ; ::_thesis: ( x <> +infty & x <> -infty & x <> 0 implies ( x * (1 / x) = 1 & (1 / x) * x = 1 ) )
assume that
A1: ( x <> +infty & x <> -infty ) and
A2: x <> 0 ; ::_thesis: ( x * (1 / x) = 1 & (1 / x) * x = 1 )
x in REAL by A1, XXREAL_0:14;
then reconsider a = x as real number ;
x * (1 / x) = a * (1 / a)
.= 1 by A2, XCMPLX_1:106 ;
hence ( x * (1 / x) = 1 & (1 / x) * x = 1 ) ; ::_thesis: verum
end;
theorem :: XXREAL_3:88
for y, x being ext-real number st -infty <> y & y <> +infty & y <> 0 holds
( (x * y) / y = x & x * (y / y) = x )
proof
let y, x be ext-real number ; ::_thesis: ( -infty <> y & y <> +infty & y <> 0 implies ( (x * y) / y = x & x * (y / y) = x ) )
assume that
A1: -infty <> y and
A2: y <> +infty and
A3: y <> 0 ; ::_thesis: ( (x * y) / y = x & x * (y / y) = x )
reconsider b = y as Element of REAL by A1, A2, XXREAL_0:14;
A4: (x * y) / y = x
proof
percases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ;
supposeA5: x = +infty ; ::_thesis: (x * y) / y = x
percases ( 0 < y or y < 0 ) by A3;
supposeA6: 0 < y ; ::_thesis: (x * y) / y = x
then x * y = +infty by A5, Def5;
hence (x * y) / y = x by A2, A5, A6, Th83; ::_thesis: verum
end;
supposeA7: y < 0 ; ::_thesis: (x * y) / y = x
then x * y = -infty by A5, Def5;
hence (x * y) / y = x by A1, A5, A7, Th84; ::_thesis: verum
end;
end;
end;
supposeA8: x = -infty ; ::_thesis: (x * y) / y = x
percases ( 0 < y or y < 0 ) by A3;
supposeA9: 0 < y ; ::_thesis: (x * y) / y = x
then x * y = -infty by A8, Def5;
hence (x * y) / y = x by A2, A8, A9, Th86; ::_thesis: verum
end;
supposeA10: y < 0 ; ::_thesis: (x * y) / y = x
then x * y = +infty by A8, Def5;
hence (x * y) / y = x by A1, A8, A10, Th85; ::_thesis: verum
end;
end;
end;
suppose ( x <> +infty & x <> -infty ) ; ::_thesis: (x * y) / y = x
then x in REAL by XXREAL_0:14;
then reconsider a = x as real number ;
(x * y) / y = (a * b) / b
.= a by A3, XCMPLX_1:89 ;
hence (x * y) / y = x ; ::_thesis: verum
end;
end;
end;
y / y = 1 by A1, A2, A3, Th78;
hence ( (x * y) / y = x & x * (y / y) = x ) by A4, Th81; ::_thesis: verum
end;
theorem :: XXREAL_3:89
for y being ext-real number holds
( +infty * y <> 1 & -infty * y <> 1 )
proof
let y be ext-real number ; ::_thesis: ( +infty * y <> 1 & -infty * y <> 1 )
( y = 0 or 0 < y or y < 0 ) ;
hence ( +infty * y <> 1 & -infty * y <> 1 ) by Def5; ::_thesis: verum
end;
theorem :: XXREAL_3:90
for x, y being ext-real number st x * y <> +infty & x * y <> -infty & not x in REAL holds
y in REAL
proof
let x, y be ext-real number ; ::_thesis: ( x * y <> +infty & x * y <> -infty & not x in REAL implies y in REAL )
assume that
A1: x * y <> +infty and
A2: x * y <> -infty ; ::_thesis: ( x in REAL or y in REAL )
assume A3: ( not x in REAL & not y in REAL ) ; ::_thesis: contradiction
percases ( ( x = +infty & y = +infty ) or ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or ( x = -infty & y = -infty ) ) by A3, XXREAL_0:14;
suppose ( x = +infty & y = +infty ) ; ::_thesis: contradiction
hence contradiction by A1, Def5; ::_thesis: verum
end;
suppose ( x = +infty & y = -infty ) ; ::_thesis: contradiction
hence contradiction by A2, Def5; ::_thesis: verum
end;
suppose ( x = -infty & y = +infty ) ; ::_thesis: contradiction
hence contradiction by A2, Def5; ::_thesis: verum
end;
suppose ( x = -infty & y = -infty ) ; ::_thesis: contradiction
hence contradiction by A1, Def5; ::_thesis: verum
end;
end;
end;
begin
theorem Th91: :: XXREAL_3:91
for x being ext-real number holds (- 1) * x = - x
proof
let x be ext-real number ; ::_thesis: (- 1) * x = - x
percases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14;
suppose x in REAL ; ::_thesis: (- 1) * x = - x
then reconsider x = x, y = - 1 as real number ;
y * x = - x ;
hence (- 1) * x = - x ; ::_thesis: verum
end;
supposeA1: x = -infty ; ::_thesis: (- 1) * x = - x
hence (- 1) * x = +infty by Def5
.= - x by A1, Def3 ;
::_thesis: verum
end;
supposeA2: x = +infty ; ::_thesis: (- 1) * x = - x
hence (- 1) * x = -infty by Def5
.= - x by A2, Def3 ;
::_thesis: verum
end;
end;
end;
theorem Th92: :: XXREAL_3:92
for x, y being ext-real number holds - (x * y) = (- x) * y
proof
let x, y be ext-real number ; ::_thesis: - (x * y) = (- x) * y
thus - (x * y) = (- 1) * (x * y) by Th91
.= ((- 1) * x) * y by Th66
.= (- x) * y by Th91 ; ::_thesis: verum
end;
theorem Th93: :: XXREAL_3:93
for y, z, x being ext-real number st y = - z holds
x * (y + z) = (x * y) + (x * z)
proof
let y, z, x be ext-real number ; ::_thesis: ( y = - z implies x * (y + z) = (x * y) + (x * z) )
assume A1: y = - z ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = x * 0 by Th7
.= (x * y) - (x * y) by Th7
.= (x * y) + (x * (- y)) by Th92
.= (x * y) + (x * z) by A1 ;
::_thesis: verum
end;
theorem Th94: :: XXREAL_3:94
for x being ext-real number holds 2 * x = x + x
proof
let x be ext-real number ; ::_thesis: 2 * x = x + x
percases ( x in REAL or x = -infty or x = +infty ) by XXREAL_0:14;
suppose x in REAL ; ::_thesis: 2 * x = x + x
then reconsider x = x as real number ;
2 * x = x + x ;
hence 2 * x = x + x ; ::_thesis: verum
end;
supposeA1: x = -infty ; ::_thesis: 2 * x = x + x
hence 2 * x = -infty by Def5
.= x + x by A1, Def2 ;
::_thesis: verum
end;
supposeA2: x = +infty ; ::_thesis: 2 * x = x + x
hence 2 * x = +infty by Def5
.= x + x by A2, Def2 ;
::_thesis: verum
end;
end;
end;
Lm23: for x, y being ext-real number holds x * (y + y) = (x * y) + (x * y)
proof
let x, y be ext-real number ; ::_thesis: x * (y + y) = (x * y) + (x * y)
thus x * (y + y) = x * (2 * y) by Th94
.= 2 * (x * y) by Th66
.= (x * y) + (x * y) by Th94 ; ::_thesis: verum
end;
Lm24: for x, z being ext-real number holds x * (0 + z) = (x * 0) + (x * z)
proof
let x, z be ext-real number ; ::_thesis: x * (0 + z) = (x * 0) + (x * z)
thus x * (0 + z) = x * z by Th4
.= (x * 0) + (x * z) by Th4 ; ::_thesis: verum
end;
Lm25: for y, z being ext-real number holds 0 * (y + z) = (0 * y) + (0 * z)
;
Lm26: for x, y, z being ext-real number st x is real & y is real holds
x * (y + z) = (x * y) + (x * z)
proof
let x, y, z be ext-real number ; ::_thesis: ( x is real & y is real implies x * (y + z) = (x * y) + (x * z) )
assume that
A1: x is real and
A2: y is real ; ::_thesis: x * (y + z) = (x * y) + (x * z)
reconsider r = x, s = y as real number by A1, A2;
A3: x * y = r * s ;
percases ( z in REAL or z = -infty or z = +infty ) by XXREAL_0:14;
suppose z in REAL ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then reconsider t = z as real number ;
reconsider u = s + t, v = r * s, w = r * t as real number ;
r * u = v + w ;
hence x * (y + z) = (x * y) + (x * z) ; ::_thesis: verum
end;
supposeA4: z = -infty ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then A5: y + z = -infty by A2, Def2;
percases ( x is zero or x is positive or x is negative ) ;
suppose x is zero ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by Lm25; ::_thesis: verum
end;
supposeA6: x is positive ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = -infty by A5, Def5
.= (x * y) + -infty by A3, Def2
.= (x * y) + (x * z) by A4, A6, Def5 ;
::_thesis: verum
end;
supposeA7: x is negative ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = +infty by A5, Def5
.= (x * y) + +infty by A3, Def2
.= (x * y) + (x * z) by A4, A7, Def5 ;
::_thesis: verum
end;
end;
end;
supposeA8: z = +infty ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then A9: y + z = +infty by A2, Def2;
percases ( x is zero or x is positive or x is negative ) ;
suppose x is zero ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by Lm25; ::_thesis: verum
end;
supposeA10: x is positive ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = +infty by A9, Def5
.= (x * y) + +infty by A3, Def2
.= (x * y) + (x * z) by A8, A10, Def5 ;
::_thesis: verum
end;
supposeA11: x is negative ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = -infty by A9, Def5
.= (x * y) + -infty by A3, Def2
.= (x * y) + (x * z) by A8, A11, Def5 ;
::_thesis: verum
end;
end;
end;
end;
end;
Lm27: for x, y, z being ext-real number st x is real & not y is real holds
x * (y + z) = (x * y) + (x * z)
proof
let x, y, z be ext-real number ; ::_thesis: ( x is real & not y is real implies x * (y + z) = (x * y) + (x * z) )
assume that
A1: x is real and
A2: not y is real ; ::_thesis: x * (y + z) = (x * y) + (x * z)
percases ( z is real or not z is real ) ;
suppose z is real ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by A1, Lm26; ::_thesis: verum
end;
suppose not z is real ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then A3: not z in REAL ;
A4: not y in REAL by A2;
percases ( ( y = -infty & z = -infty ) or ( y = -infty & z = +infty ) or ( y = +infty & z = -infty ) or ( y = +infty & z = +infty ) ) by A4, A3, XXREAL_0:14;
suppose ( y = -infty & z = -infty ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by Lm23; ::_thesis: verum
end;
suppose ( y = -infty & z = +infty ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by Th5, Th93; ::_thesis: verum
end;
suppose ( y = +infty & z = -infty ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by Th6, Th93; ::_thesis: verum
end;
suppose ( y = +infty & z = +infty ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by Lm23; ::_thesis: verum
end;
end;
end;
end;
end;
theorem Th95: :: XXREAL_3:95
for x, y, z being ext-real number st x is real holds
x * (y + z) = (x * y) + (x * z)
proof
let x, y, z be ext-real number ; ::_thesis: ( x is real implies x * (y + z) = (x * y) + (x * z) )
assume A1: x is real ; ::_thesis: x * (y + z) = (x * y) + (x * z)
percases ( ( y is real & z is real ) or not y is real or not z is real ) ;
suppose ( y is real & z is real ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by A1, Lm26; ::_thesis: verum
end;
suppose ( not y is real or not z is real ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by A1, Lm27; ::_thesis: verum
end;
end;
end;
theorem Th96: :: XXREAL_3:96
for y, z, x being ext-real number st y >= 0 & z >= 0 holds
x * (y + z) = (x * y) + (x * z)
proof
let y, z, x be ext-real number ; ::_thesis: ( y >= 0 & z >= 0 implies x * (y + z) = (x * y) + (x * z) )
assume A1: ( y >= 0 & z >= 0 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
percases ( y = 0 or z = 0 or ( y > 0 & z > 0 ) ) by A1;
suppose ( y = 0 or z = 0 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by Lm24; ::_thesis: verum
end;
supposeA2: ( y > 0 & z > 0 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
percases ( x is real or not x is real ) ;
suppose x is real ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = (x * y) + (x * z) by Th95; ::_thesis: verum
end;
suppose not x is real ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then A3: not x in REAL ;
percases ( x = -infty or x = +infty ) by A3, XXREAL_0:14;
supposeA4: x = -infty ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = -infty by A2, Def5
.= -infty + (x * z) by A2, A4, Def2
.= (x * y) + (x * z) by A2, A4, Def5 ;
::_thesis: verum
end;
supposeA5: x = +infty ; ::_thesis: x * (y + z) = (x * y) + (x * z)
hence x * (y + z) = +infty by A2, Def5
.= +infty + (x * z) by A2, A5, Def2
.= (x * y) + (x * z) by A2, A5, Def5 ;
::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
theorem :: XXREAL_3:97
for y, z, x being ext-real number st y <= 0 & z <= 0 holds
x * (y + z) = (x * y) + (x * z)
proof
let y, z, x be ext-real number ; ::_thesis: ( y <= 0 & z <= 0 implies x * (y + z) = (x * y) + (x * z) )
assume A1: ( y <= 0 & z <= 0 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
thus x * (y + z) = - (- (x * (y + z)))
.= - (x * (- (y + z))) by Th92
.= - (x * ((- y) + (- z))) by Th9
.= - ((x * (- y)) + (x * (- z))) by A1, Th96
.= - ((- (x * y)) + (x * (- z))) by Th92
.= - ((- (x * y)) + (- (x * z))) by Th92
.= - (- ((x * y) + (x * z))) by Th9
.= (x * y) + (x * z) ; ::_thesis: verum
end;
theorem :: XXREAL_3:98
for x, z being ext-real number holds x * (0 + z) = (x * 0) + (x * z) by Lm24;
theorem :: XXREAL_3:99
for f being ext-real number holds (- f) " = - (f ")
proof
let f be ext-real number ; ::_thesis: (- f) " = - (f ")
percases ( f in REAL or f = +infty or f = -infty ) by XXREAL_0:14;
supposeA1: f in REAL ; ::_thesis: (- f) " = - (f ")
then reconsider g = f as real number ;
A2: - f = - g ;
consider a being complex number such that
A3: f = a and
A4: f " = a " by A1, Def6;
A5: (- a) " = - (a ") by XCMPLX_1:222;
ex m being complex number st
( - f = m & - (f ") = m " )
proof
take - a ; ::_thesis: ( - f = - a & - (f ") = (- a) " )
thus - f = - a by A3, A2; ::_thesis: - (f ") = (- a) "
thus - (f ") = (- a) " by A4, A5, A2, Def3; ::_thesis: verum
end;
hence (- f) " = - (f ") by A2, Def6; ::_thesis: verum
end;
supposeA6: f = +infty ; ::_thesis: (- f) " = - (f ")
hence (- f) " = -infty " by Def3
.= - (f ") by A6 ;
::_thesis: verum
end;
supposeA7: f = -infty ; ::_thesis: (- f) " = - (f ")
hence (- f) " = +infty " by Def3
.= - (f ") by A7 ;
::_thesis: verum
end;
end;
end;
theorem :: XXREAL_3:100
for x, y, z being ext-real number st x is real holds
x * (y - z) = (x * y) - (x * z)
proof
let x, y, z be ext-real number ; ::_thesis: ( x is real implies x * (y - z) = (x * y) - (x * z) )
assume x is real ; ::_thesis: x * (y - z) = (x * y) - (x * z)
then x * (y - z) = (x * y) + (x * (- z)) by Th95
.= (x * y) + (- (x * z)) by Th92 ;
hence x * (y - z) = (x * y) - (x * z) ; ::_thesis: verum
end;
theorem Th101: :: XXREAL_3:101
for x, y, z being ext-real number st x <= y & z <= 0 holds
y * z <= x * z
proof
let x, y, z be ext-real number ; ::_thesis: ( x <= y & z <= 0 implies y * z <= x * z )
assume ( x <= y & z <= 0 ) ; ::_thesis: y * z <= x * z
then A1: x * (- z) <= y * (- z) by Th71;
( - (x * z) = x * (- z) & - (y * z) = y * (- z) ) by Th92;
hence y * z <= x * z by A1, Th38; ::_thesis: verum
end;
theorem Th102: :: XXREAL_3:102
for x, y, z being ext-real number st x < y & z < 0 & z <> -infty holds
y * z < x * z
proof
let x, y, z be ext-real number ; ::_thesis: ( x < y & z < 0 & z <> -infty implies y * z < x * z )
assume ( x < y & z < 0 & z <> -infty ) ; ::_thesis: y * z < x * z
then A1: x * (- z) < y * (- z) by Th5, Th10, Th72;
( - (x * z) = x * (- z) & - (y * z) = y * (- z) ) by Th92;
hence y * z < x * z by A1, Th38; ::_thesis: verum
end;
theorem :: XXREAL_3:103
for x, y, z being ext-real number st x <= y & z < 0 holds
y / z <= x / z by Th101;
theorem :: XXREAL_3:104
for x, y, z being ext-real number st x < y & z < 0 & z <> -infty holds
y / z < x / z
proof
let x, y, z be ext-real number ; ::_thesis: ( x < y & z < 0 & z <> -infty implies y / z < x / z )
assume that
A1: x < y and
A2: 0 > z and
A3: z <> -infty ; ::_thesis: y / z < x / z
percases ( z = +infty or z in REAL ) by A3, XXREAL_0:14;
suppose z = +infty ; ::_thesis: y / z < x / z
hence y / z < x / z by A2; ::_thesis: verum
end;
suppose z in REAL ; ::_thesis: y / z < x / z
then reconsider z = z as real number ;
z " < 0 by A2;
hence y / z < x / z by A1, Th102; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_3:105
for x being ext-real number holds (x / 2) + (x / 2) = x
proof
let x be ext-real number ; ::_thesis: (x / 2) + (x / 2) = x
(x / 2) + (x / 2) = (x + x) / 2 by Th95
.= (2 * x) / 2 by Th94
.= x * (2 / 2) by Th66
.= x by Th81 ;
hence (x / 2) + (x / 2) = x ; ::_thesis: verum
end;