:: Basic Operations on Extended Real Numbers
:: by Andrzej Trybulec
::
:: Received September 23, 2008
:: Copyright (c) 2008-2011 Association of Mizar Users

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 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 set ;
existence
ex b₁ being ext-real number st
( not b₁ is real & b₁ is positive )

proof end;

cluster ext-real negative non real set ;
existence
ex b₁ being ext-real number st
( not b₁ is real & b₁ is negative )

proof end;

end;

theorem Th1: :: XXREAL_3:1

for x being ext-real positive non real number holds x = +infty

proof end;

theorem Th2: :: XXREAL_3:2

for x being ext-real negative non real number holds x = -infty

proof end;

registration

cluster ext-real non negative non real -> ext-real positive set ;
coherence
for b₁ being ext-real number st not b₁ is real & not b₁ is negative holds
b₁ is positive ;
cluster ext-real non positive non real -> ext-real negative set ;
coherence
for b₁ being ext-real number st not b₁ is real & not b₁ is positive holds
b₁ 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 end;

begin

definition

let x, y be ext-real number ;
func x + 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 b₁ being ext-real number ex a, b being complex number st
( x = a & y = b & b₁ = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b₁ being ext-real number st b₁ = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b₁ being ext-real number st b₁ = -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 b₁ being ext-real number st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being ext-real number holds
( ( x is real & y is real & ex a, b being complex number st
( x = a & y = b & b₁ = a + b ) & ex a, b being complex number st
( x = a & y = b & b₂ = a + b ) implies b₁ = b₂ ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) & b₁ = +infty & b₂ = +infty implies b₁ = b₂ ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) & b₁ = -infty & b₂ = -infty implies b₁ = b₂ ) & ( ( 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 b₁ = 0 or not b₂ = 0 or b₁ = b₂ ) ) ;
consistency
for b₁ 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 & b₁ = a + b ) iff b₁ = +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 & b₁ = a + b ) iff b₁ = -infty ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) & ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b₁ = +infty iff b₁ = -infty ) ) ) ;
commutativity
for b₁, 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 & b₁ = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies b₁ = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies b₁ = -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 b₁ = 0 ) holds
( ( y is real & x is real implies ex a, b being complex number st
( y = a & x = b & b₁ = a + b ) ) & ( ( ( y = +infty & x <> -infty ) or ( x = +infty & y <> -infty ) ) implies b₁ = +infty ) & ( ( ( y = -infty & x <> +infty ) or ( x = -infty & y <> +infty ) ) implies b₁ = -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 b₁ = 0 ) ) ;

end;

:: deftheorem Def2 defines + XXREAL_3:def 2 :
for x, y, b₃ being ext-real number holds
( ( x is real & y is real implies ( b₃ = x + y iff ex a, b being complex number st
( x = a & y = b & b₃ = a + b ) ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( b₃ = x + y iff b₃ = +infty ) ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b₃ = x + y iff b₃ = -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 ( b₃ = x + y iff b₃ = 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 b₁ being ext-real number ex a being complex number st
( x = a & b₁ = - a ) ) & ( x = +infty implies ex b₁ being ext-real number st b₁ = -infty ) & ( not x is real & not x = +infty implies ex b₁ being ext-real number st b₁ = +infty ) )

proof end;

uniqueness
for b₁, b₂ being ext-real number holds
( ( x is real & ex a being complex number st
( x = a & b₁ = - a ) & ex a being complex number st
( x = a & b₂ = - a ) implies b₁ = b₂ ) & ( x = +infty & b₁ = -infty & b₂ = -infty implies b₁ = b₂ ) & ( not x is real & not x = +infty & b₁ = +infty & b₂ = +infty implies b₁ = b₂ ) ) ;
consistency
for b₁ being ext-real number st x is real & x = +infty holds
( ex a being complex number st
( x = a & b₁ = - a ) iff b₁ = -infty ) ;
involutiveness
for b₁, b₂ being ext-real number st ( b₂ is real implies ex a being complex number st
( b₂ = a & b₁ = - a ) ) & ( b₂ = +infty implies b₁ = -infty ) & ( not b₂ is real & not b₂ = +infty implies b₁ = +infty ) holds
( ( b₁ is real implies ex a being complex number st
( b₁ = a & b₂ = - a ) ) & ( b₁ = +infty implies b₂ = -infty ) & ( not b₁ is real & not b₁ = +infty implies b₂ = +infty ) )

proof end;

end;

:: deftheorem Def3 defines - XXREAL_3:def 3 :
for x, b₂ being ext-real number holds
( ( x is real implies ( b₂ = - x iff ex a being complex number st
( x = a & b₂ = - a ) ) ) & ( x = +infty implies ( b₂ = - x iff b₂ = -infty ) ) & ( not x is real & not x = +infty implies ( b₂ = - x iff b₂ = +infty ) ) );

definition

let x, y be ext-real number ;
func x - 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 ;
identify x + 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 ;
cluster r + s -> ext-real real ;
coherence
r + s is real ;
cluster r - s -> ext-real real ;
coherence
r - s is real ;

end;

registration

let x be real number ;
let y be ext-real non real number ;
cluster x + y -> non real number ;
coherence
for b₁ being number st b₁ = x + y holds
not b₁ is real

proof end;

end;

registration

let x, y be ext-real positive non real number ;
cluster x + y -> ext-real non real ;
coherence
not x + y is real

proof end;

end;

registration

let x, y be ext-real negative non real number ;
cluster x + y -> ext-real non real ;
coherence
not x + y is real

proof end;

end;

registration

let x be ext-real negative non real number ;
let y be ext-real positive non real number ;
cluster x + y -> zero ext-real ;
coherence
x + y is zero

proof end;

end;

registration

let x, y be real number ;
let a, b be complex number ;
identify x - 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 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 end;

theorem :: XXREAL_3:8

for x, y being ext-real number st x + y = 0 holds
x = - y

proof end;

Lm3: for x being ext-real number holds
( - x in REAL iff x in REAL )

proof 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 end;

Lm7: for x being ext-real number st x in REAL holds
- (x + -infty) = (- -infty) + (- x)

proof end;

theorem Th9: :: XXREAL_3:9

for x, y being ext-real number holds - (x + y) = (- x) + (- y)

proof end;

theorem Th10: :: XXREAL_3:10

for f, g being ext-real number st - f = - g holds
f = g

proof end;

Lm8: for x, y being ext-real number holds
( not x + y = +infty or x = +infty or y = +infty )

proof end;

Lm9: for x, y being ext-real number holds
( not x + y = -infty or x = -infty or y = -infty )

proof 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 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 end;

theorem Th13: :: XXREAL_3:13

for x being ext-real number st x <> +infty holds
( +infty - x = +infty & x - +infty = -infty )

proof end;

theorem Th14: :: XXREAL_3:14

for x being ext-real number st x <> -infty holds
( -infty - x = -infty & x - -infty = +infty )

proof end;

theorem Th15: :: XXREAL_3:15

for x being ext-real number holds x - 0 = x

proof 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 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 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 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 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 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 end;

theorem :: XXREAL_3:24

for z, x being ext-real number st z is real holds
x = (x + z) - z

proof end;

Lm10: - +infty = -infty
by Def3;

Lm11: for x being ext-real number st x in REAL holds
- (x + -infty) = (- -infty) + (- x)

proof end;

theorem :: XXREAL_3:25

canceled;

theorem Th26: :: XXREAL_3:26

for x, y being ext-real number holds - (x + y) = (- y) - x

proof end;

theorem :: XXREAL_3:27

for x, y being ext-real number holds
( - (x - y) = (- x) + y & - (x - y) = y - x )

proof end;

theorem Th28: :: XXREAL_3:28

for x, y being ext-real number holds
( - ((- x) + y) = x - y & - ((- x) + y) = x + (- y) )

proof end;

theorem :: XXREAL_3:29

for y, z being ext-real number st 0 <= y & y < +infty holds
z = (z + y) - y

proof 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 & z = -infty ) & not ( y = -infty & z = +infty ) & not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) holds
(x + y) + z = x + (y + z)

proof end;

theorem Th31: :: 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 end;

theorem :: 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 end;

theorem Th33: :: XXREAL_3:33

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 end;

theorem Th34: :: XXREAL_3:34

for z, x, y being ext-real number st z is real holds
(z + x) - (z + y) = x - y

proof end;

theorem :: XXREAL_3:35

for y, z, x being ext-real number st y is real holds
(z - y) + (y - x) = z - x

proof end;

begin

Lm12: for x, y, z being ext-real number st x <= y holds
x + z <= y + z

proof end;

Lm13: for x, y being ext-real number st x >= 0 & y > 0 holds
x + y > 0

proof end;

Lm14: for x, y being ext-real number st x <= 0 & y < 0 holds
x + y < 0

proof end;

registration

let x, y be ext-real non negative number ;
cluster x + y -> ext-real non negative ;
coherence
not x + y is negative

proof end;

end;

registration

let x, y be ext-real non positive number ;
cluster x + y -> ext-real non positive ;
coherence
not x + y is positive

proof end;

end;

registration

let x be ext-real positive number ;
let y be ext-real non negative number ;
cluster x + y -> ext-real positive ;
coherence
x + y is positive by Lm13;
cluster y + 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 ;
cluster x + y -> ext-real negative ;
coherence
x + y is negative by Lm14;
cluster y + 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 end;

end;

registration

let x be ext-real non negative number ;
cluster - x -> ext-real non positive ;
coherence
not - x is positive

proof end;

end;

registration

let x be ext-real positive number ;
cluster - x -> ext-real negative ;
coherence
- x is negative

proof end;

end;

registration

let x be ext-real negative number ;
cluster - x -> ext-real positive ;
coherence
- x is positive

proof end;

end;

registration

let x be ext-real non negative number ;
let y be ext-real non positive number ;
cluster x - y -> ext-real non negative ;
coherence
not x - y is negative ;
cluster y - 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 ;
cluster x - y -> ext-real positive ;
coherence
x - y is positive ;
cluster y - 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 ;
cluster x - y -> ext-real negative ;
coherence
x - y is negative ;
cluster y - 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 end;

theorem :: XXREAL_3:36

for x, y, z being ext-real number st x <= y holds
x + z <= y + z by Lm12;

theorem :: XXREAL_3:37

canceled;

theorem Th38: :: XXREAL_3:38

for x, y, z, w being ext-real number st x <= y & z <= w holds
x + z <= y + w

proof end;

theorem Th39: :: XXREAL_3:39

for x, y, z, w being ext-real number st x <= y & z <= w holds
x - w <= y - z

proof end;

theorem Th40: :: XXREAL_3:40

for x, y being ext-real number holds
( x <= y iff - y <= - x )

proof end;

theorem :: XXREAL_3:41

canceled;

theorem Th42: :: XXREAL_3:42

for z, x being ext-real number st 0 <= z holds
x <= x + z

proof end;

theorem :: XXREAL_3:43

for x, y being ext-real number st x <= y holds
y - x >= 0

proof end;

theorem :: XXREAL_3:44

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 end;

theorem :: XXREAL_3:45

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 end;

theorem :: XXREAL_3:46

canceled;

theorem Th47: :: XXREAL_3:47

for z, x, y being ext-real number st z in REAL & x < y holds
( x + z < y + z & x - z < y - z )

proof end;

theorem :: XXREAL_3:48

for x, y, z being ext-real number st 0 <= x & 0 <= y & 0 <= z holds
(x + y) + z = x + (y + z)

proof end;

theorem Th49: :: XXREAL_3:49

for x, y, z being ext-real number st x is real holds
( y + x <= z iff y <= z - x )

proof end;

theorem Th50: :: XXREAL_3:50

for x, y being ext-real number st 0 < x & x < y holds
0 < y - x

proof end;

theorem :: XXREAL_3:51

for x, z, y being ext-real number st 0 <= x & 0 <= z & z + x < y holds
z < y - x

proof end;

theorem :: XXREAL_3:52

canceled;

theorem :: XXREAL_3:53

for x, z, y being ext-real number st 0 <= x & 0 <= z & z + x < y holds
z <= y

proof end;

theorem :: XXREAL_3:54

canceled;

theorem Th55: :: XXREAL_3:55

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 end;

theorem :: XXREAL_3:56

for x being ext-real number st 0 < x holds
ex y being real number st
( 0 < y & y + y < x )

proof end;

theorem Th57: :: XXREAL_3:57

for x, y being ext-real number st x < y & x < +infty & -infty < y holds
0 < y - x

proof end;

theorem :: XXREAL_3:58

canceled;

theorem :: XXREAL_3:59

canceled;

theorem :: XXREAL_3:60

canceled;

theorem :: XXREAL_3:61

canceled;

theorem :: XXREAL_3:62

canceled;

theorem :: XXREAL_3:63

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 end;

theorem :: XXREAL_3:64

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 end;

theorem :: XXREAL_3:65

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 end;

theorem :: XXREAL_3:66

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 end;

theorem :: XXREAL_3:67

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 end;

theorem :: XXREAL_3:68

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 end;

theorem :: XXREAL_3:69

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 end;

theorem :: XXREAL_3:70

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 end;

theorem :: XXREAL_3:71

for x, y being ext-real number holds
( ( x <= - y implies y <= - x ) & ( - x <= y implies - y <= x ) )

proof end;

theorem :: XXREAL_3:72

for x, y being ext-real number st ( for e being real number st 0 < e holds
x < y + e ) holds
x <= y

proof end;

theorem :: XXREAL_3:73

for x, y, t being ext-real number st t <> -infty & t <> +infty & x < y holds
x + t < y + t

proof end;

theorem :: XXREAL_3:74

for x, y, t being ext-real number st t <> -infty & t <> +infty & x < y holds
x - t < y - t

proof end;

theorem :: XXREAL_3:75

for w, x, y, z being ext-real number st -infty < w & x < y & w < z holds
x + w < y + z

proof end;

theorem :: XXREAL_3:76

for x, z, y being ext-real number st 0 <= x & z + x <= y holds
z <= y

proof end;

begin

definition

let x, y be ext-real number ;
func x * 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 b₁ being ext-real number ex a, b being complex number st
( x = a & y = b & b₁ = 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 b₁ being ext-real number st b₁ = +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 b₁ being ext-real number st b₁ = -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 b₁ being ext-real number st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being ext-real number holds
( ( x is real & y is real & ex a, b being complex number st
( x = a & y = b & b₁ = a * b ) & ex a, b being complex number st
( x = a & y = b & b₂ = a * b ) implies b₁ = b₂ ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) & b₁ = +infty & b₂ = +infty implies b₁ = b₂ ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) & b₁ = -infty & b₂ = -infty implies b₁ = b₂ ) & ( ( 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 ) ) ) & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) ) ;
consistency
for b₁ 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 & b₁ = a * b ) iff b₁ = +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 & b₁ = a * b ) iff b₁ = -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 ( b₁ = +infty iff b₁ = -infty ) ) ) ;
commutativity
for b₁, 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 & b₁ = 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 b₁ = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies b₁ = -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 b₁ = 0 ) holds
( ( y is real & x is real implies ex a, b being complex number st
( y = a & x = b & b₁ = 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 b₁ = +infty ) & ( ( not y is real or not x is real ) & ( ( y is positive & x is negative ) or ( y is negative & x is positive ) ) implies b₁ = -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 b₁ = 0 ) ) ;

end;

:: deftheorem Def5 defines * XXREAL_3:def 5 :
for x, y, b₃ being ext-real number holds
( ( x is real & y is real implies ( b₃ = x * y iff ex a, b being complex number st
( x = a & y = b & b₃ = 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 ( b₃ = x * y iff b₃ = +infty ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( b₃ = x * y iff b₃ = -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 ( b₃ = x * y iff b₃ = 0 ) ) );

registration

let x, y be real number ;
let a, b be complex number ;
identify x * 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 ;
func x " -> 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 b₁ being ext-real number ex a being complex number st
( x = a & b₁ = a " ) ) & ( not x is real implies ex b₁ being ext-real number st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being ext-real number holds
( ( x is real & ex a being complex number st
( x = a & b₁ = a " ) & ex a being complex number st
( x = a & b₂ = a " ) implies b₁ = b₂ ) & ( not x is real & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) ) ;
consistency
for b₁ being ext-real number holds verum ;

end;

:: deftheorem Def6 defines " XXREAL_3:def 6 :
for x, b₂ being ext-real number holds
( ( x is real implies ( b₂ = x " iff ex a being complex number st
( x = a & b₂ = a " ) ) ) & ( not x is real implies ( b₂ = x " iff b₂ = 0 ) ) );

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 Def6;

end;

definition

let x, y be ext-real number ;
func x / 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 ;
identify x / y with a / b when x = a, y = b;
compatibility
( x = a & y = b implies x / y = a / b )

proof end;

end;

Lm16: for x being ext-real number holds x * 0 = 0

proof end;

registration

let x be ext-real positive number ;
let y be ext-real negative number ;
cluster x * y -> ext-real negative ;
coherence
x * y is negative

proof end;

end;

registration

let x, y be ext-real negative number ;
cluster x * y -> ext-real positive ;
coherence
x * y is positive

proof end;

end;

registration

let x, y be ext-real positive number ;
cluster x * y -> ext-real positive ;
coherence
x * y is positive

proof end;

end;

registration

let x be ext-real non positive number ;
let y be ext-real non negative number ;
cluster x * y -> ext-real non positive ;
coherence
not x * y is positive

proof end;

end;

registration

let x, y be ext-real non positive number ;
cluster x * y -> ext-real non negative ;
coherence
not x * y is negative

proof end;

end;

registration

let x, y be ext-real non negative number ;
cluster x * y -> ext-real non negative ;
coherence
not x * y is negative

proof end;

end;

registration

let x be ext-real non positive number ;
cluster x " -> ext-real non positive ;
coherence
not x " is positive

proof end;

end;

registration

let x be ext-real non negative number ;
cluster x " -> ext-real non negative ;
coherence
not x " is negative

proof end;

end;

registration

let x be ext-real non negative number ;
let y be ext-real non positive number ;
cluster x / y -> ext-real non positive ;
coherence
not x / y is positive ;
cluster y / x -> ext-real non positive ;
coherence
not y / x is positive ;

end;

registration

let x, y be ext-real non negative number ;
cluster x / y -> ext-real non negative ;
coherence
not x / y is negative ;

end;

registration

let x, y be ext-real non positive number ;
cluster x / 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 end;

registration

let x, y be non zero ext-real number ;
cluster x * y -> non zero ext-real ;
coherence
not x * y is zero

proof end;

end;

registration

let x be zero ext-real number ;
let y be ext-real number ;
cluster x * y -> zero ext-real ext-real number ;
coherence
for b₁ being ext-real number st b₁ = x * y holds
b₁ 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 end;

Lm19: for y, x, z being ext-real number st y = 0 holds
x * (y * z) = (x * y) * z

proof end;

Lm20: for y, x, z being ext-real number st not y is real holds
x * (y * z) = (x * y) * z

proof end;

Lm21: for x, y, z being ext-real number st not x is real holds
x * (y * z) = (x * y) * z

proof end;

theorem Th77: :: XXREAL_3:77

for x, y, z being ext-real number holds x * (y * z) = (x * y) * z

proof end;

registration

let r be real number ;
cluster r " -> ext-real real ;
coherence
r " is real ;

end;

registration

let r, s be real number ;
cluster r * s -> ext-real real ;
coherence
r * s is real ;
cluster r / 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:78

for f, g being ext-real number holds (f * g) " = (f ") * (g ")

proof end;

theorem :: XXREAL_3:79

for r being real number
for f, g being ext-real number st r <> 0 & r * f = r * g holds
f = g

proof end;

theorem Th80: :: XXREAL_3:80

for x, y being ext-real number st x <> +infty & x <> -infty & x * y = +infty & not y = +infty holds
y = -infty

proof end;

theorem Th81: :: XXREAL_3:81

for x, y being ext-real number st x <> +infty & x <> -infty & x * y = -infty & not y = +infty holds
y = -infty

proof 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 end;

theorem Th82: :: XXREAL_3:82

for x, y, z being ext-real number st x <= y & 0 <= z holds
x * z <= y * z

proof end;

theorem Th83: :: XXREAL_3:83

for x, y, z being ext-real number st x < y & 0 < z & z <> +infty holds
x * z < y * z

proof end;

theorem :: XXREAL_3:84

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:85

+infty " = 0 ;

theorem :: XXREAL_3:86

-infty " = 0 ;

theorem :: XXREAL_3:87

for x being ext-real number holds x / +infty = 0 ;

theorem :: XXREAL_3:88

for x being ext-real number holds x / -infty = 0 ;

theorem Th89: :: XXREAL_3:89

for x being ext-real number st x <> -infty & x <> +infty & x <> 0 holds
x / x = 1

proof end;

theorem :: XXREAL_3:90

for x, y, z being ext-real number st x <= y & 0 < z holds
x / z <= y / z by Th82;

theorem :: XXREAL_3:91

for x, y, z being ext-real number st x < y & 0 < z & z <> +infty holds
x / z < y / z

proof end;

theorem Th92: :: XXREAL_3:92

for x being ext-real number holds 1 * x = x

proof end;

theorem Th93: :: XXREAL_3:93

for y being ext-real number holds
( not y " = 0 or y = +infty or y = -infty or y = 0 )

proof end;

theorem Th94: :: XXREAL_3:94

for y being ext-real number st 0 < y & y <> +infty holds
+infty / y = +infty

proof end;

theorem Th95: :: XXREAL_3:95

for y being ext-real number st y < 0 & -infty <> y holds
-infty / y = +infty

proof end;

theorem Th96: :: XXREAL_3:96

for y being ext-real number st y < 0 & -infty <> y holds
+infty / y = -infty

proof end;

theorem Th97: :: XXREAL_3:97

for y being ext-real number st 0 < y & y <> +infty holds
-infty / y = -infty

proof end;

theorem :: XXREAL_3:98

for x being ext-real number st x <> +infty & x <> -infty & x <> 0 holds
( x * (1 / x) = 1 & (1 / x) * x = 1 )

proof end;

theorem :: XXREAL_3:99

for y, x being ext-real number st -infty <> y & y <> +infty & y <> 0 holds
( (x * y) / y = x & x * (y / y) = x )

proof end;

theorem :: XXREAL_3:100

for y being ext-real number holds
( +infty * y <> 1 & -infty * y <> 1 )

proof end;

theorem :: XXREAL_3:101

for x, y being ext-real number st x * y <> +infty & x * y <> -infty & not x in REAL holds
y in REAL

proof end;

begin

theorem Th102: :: XXREAL_3:102

for x being ext-real number holds (- 1) * x = - x

proof end;

theorem Th103: :: XXREAL_3:103

for x, y being ext-real number holds - (x * y) = (- x) * y

proof end;

theorem Th104: :: XXREAL_3:104

for y, z, x being ext-real number st y = - z holds
x * (y + z) = (x * y) + (x * z)

proof end;

theorem Th105: :: XXREAL_3:105

for x being ext-real number holds 2 * x = x + x

proof end;

Lm23: for x, y being ext-real number holds x * (y + y) = (x * y) + (x * y)

proof end;

Lm24: for x, z being ext-real number holds x * (0 + z) = (x * 0) + (x * z)

proof 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 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 end;

theorem Th106: :: XXREAL_3:106

for x, y, z being ext-real number st x is real holds
x * (y + z) = (x * y) + (x * z)

proof end;

theorem Th107: :: XXREAL_3:107

for y, z, x being ext-real number st y >= 0 & z >= 0 holds
x * (y + z) = (x * y) + (x * z)

proof end;

theorem :: XXREAL_3:108

canceled;

theorem :: XXREAL_3:109

for y, z, x being ext-real number st y <= 0 & z <= 0 holds
x * (y + z) = (x * y) + (x * z)

proof end;

theorem :: XXREAL_3:110

for x, z being ext-real number holds x * (0 + z) = (x * 0) + (x * z) by Lm24;

theorem :: XXREAL_3:111

for f being ext-real number holds (- f) " = - (f ")

proof end;

theorem :: XXREAL_3:112

for x, y, z being ext-real number st x is real holds
x * (y - z) = (x * y) - (x * z)

proof end;

theorem Th113: :: XXREAL_3:113

for x, y, z being ext-real number st x <= y & z <= 0 holds
y * z <= x * z

proof end;

theorem Th114: :: XXREAL_3:114

for x, y, z being ext-real number st x < y & z < 0 & z <> -infty holds
y * z < x * z

proof end;

theorem :: XXREAL_3:115

for x, y, z being ext-real number st x <= y & z < 0 holds
y / z <= x / z by Th113;

theorem :: XXREAL_3:116

for x, y, z being ext-real number st x < y & z < 0 & z <> -infty holds
y / z < x / z

proof end;

theorem :: XXREAL_3:117

for x being ext-real number holds (x / 2) + (x / 2) = x

proof end;