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

definition

let x, y be ExtReal;

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 ExtReal 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 object ;

existence
ex b₁ being ExtReal st
( not b₁ is real & b₁ is positive )

proof end;

cluster ext-real negative non real for object ;

existence
ex b₁ being ExtReal st
( not b₁ is real & b₁ is negative )

proof end;

end;

theorem Th1: :: XXREAL_3:1

for x being positive non real ExtReal holds x = +infty

proof end;

theorem Th2: :: XXREAL_3:2

for x being negative non real ExtReal holds x = -infty

proof end;

registration

cluster ext-real non negative non real -> positive for object ;

coherence
for b₁ being ExtReal st not b₁ is real & not b₁ is negative holds
b₁ is positive ;

cluster ext-real non positive non real -> negative for object ;

coherence
for b₁ being ExtReal st not b₁ is real & not b₁ is positive holds
b₁ is negative ;

end;

theorem Th3: :: XXREAL_3:3

for x, z being ExtReal st x < z holds
ex y being Real st
( x < y & y < z )

proof end;

definition

let x, y be ExtReal;

func x + y -> ExtReal means :Def2: :: XXREAL_3:def 2
ex a, b being Complex 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 ExtReal ex a, b being Complex st
( x = a & y = b & b₁ = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b₁ being ExtReal st b₁ = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b₁ being ExtReal 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 ExtReal st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being ExtReal holds
( ( x is real & y is real & ex a, b being Complex st
( x = a & y = b & b₁ = a + b ) & ex a, b being Complex 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 ExtReal holds
( ( x is real & y is real & ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( ex a, b being Complex 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 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 ExtReal st ( x is real & y is real implies ex a, b being Complex 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 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 ExtReal holds
( ( x is real & y is real implies ( b₃ = x + y iff ex a, b being Complex 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 ExtReal;

func - x -> ExtReal means :Def3: :: XXREAL_3:def 3
ex a being Complex 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 ExtReal ex a being Complex st
( x = a & b₁ = - a ) ) & ( x = +infty implies ex b₁ being ExtReal st b₁ = -infty ) & ( not x is real & not x = +infty implies ex b₁ being ExtReal st b₁ = +infty ) )

proof end;

uniqueness
for b₁, b₂ being ExtReal holds
( ( x is real & ex a being Complex st
( x = a & b₁ = - a ) & ex a being Complex 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 ExtReal st x is real & x = +infty holds
( ex a being Complex st
( x = a & b₁ = - a ) iff b₁ = -infty ) ;
involutiveness
for b₁, b₂ being ExtReal st ( b₂ is real implies ex a being Complex 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 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 ExtReal holds
( ( x is real implies ( b₂ = - x iff ex a being Complex 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 ExtReal;

func x - y -> ExtReal equals :: XXREAL_3:def 4
x + (- y);

coherence
x + (- y) is ExtReal ;

end;

:: deftheorem defines - XXREAL_3:def 4 :
for x, y being ExtReal holds x - y = x + (- y);

registration

let x, y be Real;
let a, b be Complex;

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;
let a be Complex;

identify - x with - a when x = a;

compatibility
( x = a implies - x = - a ) by Def3;

end;

:: for ExtReals

registration

let r be Real;

cluster - r -> real ;

coherence
- r is real ;

end;

:: for ExtReals

registration

let r, s be Real;

cluster r + s -> real ;

coherence
r + s is real ;

cluster r - s -> real ;

coherence
r - s is real ;

end;

registration

let x be Real;
let y be non real ExtReal;

cluster x + y -> non real for object ;

coherence
for b₁ being object st b₁ = x + y holds
not b₁ is real

proof end;

end;

registration

let x, y be positive non real ExtReal;

cluster x + y -> non real ;

coherence
not x + y is real

proof end;

end;

registration

let x, y be negative non real ExtReal;

cluster x + y -> non real ;

coherence
not x + y is real

proof end;

end;

registration

let x be negative non real ExtReal;
let y be positive non real ExtReal;

cluster x + y -> zero ;

coherence
x + y is zero

proof end;

end;

registration

let x, y be Real;
let a, b be Complex;

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 ExtReal 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 ExtReal holds x + (- x) = 0

proof end;

theorem :: XXREAL_3:8

for x, y being ExtReal st x + y = 0 holds
x = - y

proof end;

Lm3: for x being ExtReal holds
( - x in REAL iff x in REAL )

proof end;

Lm4: - (+infty + -infty) = (- -infty) - +infty

proof end;

Lm5: - +infty = -infty
by Def3;

Lm6: for x being ExtReal st x in REAL holds
- (x + +infty) = (- +infty) + (- x)

proof end;

Lm7: for x being ExtReal st x in REAL holds
- (x + -infty) = (- -infty) + (- x)

proof end;

theorem Th9: :: XXREAL_3:9

for x, y being ExtReal holds - (x + y) = (- x) + (- y)

proof end;

theorem Th10: :: XXREAL_3:10

for f, g being ExtReal st - f = - g holds
f = g

proof end;

Lm8: for x, y being ExtReal holds
( not x + y = +infty or x = +infty or y = +infty )

proof end;

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

proof end;

theorem Th11: :: XXREAL_3:11

for r being Real
for f, g being ExtReal st r + f = r + g holds
f = g

proof end;

theorem :: XXREAL_3:12

for r being Real
for f, g being ExtReal st r - f = r - g holds
f = g

proof end;

theorem Th13: :: XXREAL_3:13

for x being ExtReal st x <> +infty holds
( +infty - x = +infty & x - +infty = -infty )

proof end;

theorem Th14: :: XXREAL_3:14

for x being ExtReal st x <> -infty holds
( -infty - x = -infty & x - -infty = +infty )

proof end;

theorem Th15: :: XXREAL_3:15

for x being ExtReal holds x - 0 = x

proof end;

theorem :: XXREAL_3:16

for x, y being ExtReal holds
( not x + y = +infty or x = +infty or y = +infty ) by Lm8;

theorem :: XXREAL_3:17

for x, y being ExtReal holds
( not x + y = -infty or x = -infty or y = -infty ) by Lm9;

theorem Th18: :: XXREAL_3:18

for x, y being ExtReal holds
( not x - y = +infty or x = +infty or y = -infty )

proof end;

theorem Th19: :: XXREAL_3:19

for x, y being ExtReal holds
( not x - y = -infty or x = -infty or y = +infty )

proof end;

theorem Th20: :: XXREAL_3:20

for x, y being ExtReal 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 ExtReal 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 ExtReal st x is real holds
( (y - x) + x = y & (y + x) - x = y )

proof end;

theorem Th23: :: XXREAL_3:23

for x being ExtReal 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 x, z being ExtReal st z is real holds
x = (x + z) - z

proof end;

Lm10: - +infty = -infty
by Def3;

Lm11: for x being ExtReal st x in REAL holds
- (x + -infty) = (- -infty) + (- x)

proof end;

theorem Th25: :: XXREAL_3:25

for x, y being ExtReal holds - (x + y) = (- y) - x

proof end;

theorem :: XXREAL_3:26

for x, y being ExtReal holds
( - (x - y) = (- x) + y & - (x - y) = y - x )

proof end;

theorem Th27: :: XXREAL_3:27

for x, y being ExtReal holds
( - ((- x) + y) = x - y & - ((- x) + y) = x + (- y) )

proof end;

theorem :: XXREAL_3:28

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

proof end;

theorem Th29: :: XXREAL_3:29

for x, y, z being ExtReal 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 Th30: :: XXREAL_3:30

for x, y, z being ExtReal 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:31

for x, y, z being ExtReal 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 Th32: :: XXREAL_3:32

for x, y, z being ExtReal 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 ExtReal st z is real holds
(z + x) - (z + y) = x - y

proof end;

theorem :: XXREAL_3:34

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

proof end;

Lm12: for x, y, z being ExtReal st x <= y holds
x + z <= y + z

proof end;

Lm13: for x, y being ExtReal st x >= 0 & y > 0 holds
x + y > 0

proof end;

Lm14: for x, y being ExtReal st x <= 0 & y < 0 holds
x + y < 0

proof end;

registration

let x, y be non negative ExtReal;

cluster x + y -> non negative ;

coherence
not x + y is negative

proof end;

end;

registration

let x, y be non positive ExtReal;

cluster x + y -> non positive ;

coherence
not x + y is positive

proof end;

end;

registration

let x be positive ExtReal;
let y be non negative ExtReal;

cluster x + y -> positive ;

coherence
x + y is positive by Lm13;

cluster y + x -> positive ;

coherence
y + x is positive ;

end;

registration

let x be negative ExtReal;
let y be non positive ExtReal;

cluster x + y -> negative ;

coherence
x + y is negative by Lm14;

cluster y + x -> negative ;

coherence
y + x is negative ;

end;

registration

let x be non positive ExtReal;

cluster - x -> non negative ;

coherence
not - x is negative

proof end;

end;

registration

let x be non negative ExtReal;

cluster - x -> non positive ;

coherence
not - x is positive

proof end;

end;

registration

let x be positive ExtReal;

cluster - x -> negative ;

coherence
- x is negative

proof end;

end;

registration

let x be negative ExtReal;

cluster - x -> positive ;

coherence
- x is positive

proof end;

end;

registration

let x be non negative ExtReal;
let y be non positive ExtReal;

cluster x - y -> non negative ;

coherence
not x - y is negative ;

cluster y - x -> non positive ;

coherence
not y - x is positive ;

end;

registration

let x be positive ExtReal;
let y be non positive ExtReal;

cluster x - y -> positive ;

coherence
x - y is positive ;

cluster y - x -> negative ;

coherence
y - x is negative ;

end;

registration

let x be negative ExtReal;
let y be non negative ExtReal;

cluster x - y -> negative ;

coherence
x - y is negative ;

cluster y - x -> positive ;

coherence
y - x is positive ;

end;

Lm15: for x, y being ExtReal st x <= y holds
- y <= - x

proof end;

theorem :: XXREAL_3:35

for x, y, z being ExtReal st x <= y holds
x + z <= y + z by Lm12;

theorem Th36: :: XXREAL_3:36

for x, y, z, w being ExtReal st x <= y & z <= w holds
x + z <= y + w

proof end;

theorem Th37: :: XXREAL_3:37

for x, y, z, w being ExtReal st x <= y & z <= w holds
x - w <= y - z

proof end;

theorem Th38: :: XXREAL_3:38

for x, y being ExtReal holds
( x <= y iff - y <= - x )

proof end;

theorem Th39: :: XXREAL_3:39

for x, z being ExtReal st 0 <= z holds
x <= x + z

proof end;

theorem :: XXREAL_3:40

for x, y being ExtReal st x <= y holds
y - x >= 0

proof end;

theorem :: XXREAL_3:41

for x, y, z being ExtReal 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:42

for x, y, z being ExtReal 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 Th43: :: XXREAL_3:43

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

proof end;

theorem :: XXREAL_3:44

for x, y, z being ExtReal st 0 <= x & 0 <= y & 0 <= z holds
(x + y) + z = x + (y + z)

proof end;

theorem Th45: :: XXREAL_3:45

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

proof end;

theorem Th46: :: XXREAL_3:46

for x, y being ExtReal st 0 < x & x < y holds
0 < y - x

proof end;

Lm16: 0 in REAL
by XREAL_0:def 1;

theorem :: XXREAL_3:47

for x, y, z being ExtReal st 0 <= x & 0 <= z & z + x < y holds
z < y - x

proof end;

theorem :: XXREAL_3:48

for x, y, z being ExtReal st 0 <= x & 0 <= z & z + x < y holds
z <= y

proof end;

theorem Th49: :: XXREAL_3:49

for x, z being ExtReal st 0 <= x & x < z holds
ex y being Real st
( 0 < y & x + y < z )

proof end;

theorem :: XXREAL_3:50

for x being ExtReal st 0 < x holds
ex y being Real st
( 0 < y & y + y < x )

proof end;

theorem Th51: :: XXREAL_3:51

for x, y being ExtReal st x < y & x < +infty & -infty < y holds
0 < y - x

proof end;

theorem :: XXREAL_3:52

for x, y, z being ExtReal 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:53

for x, y, z being ExtReal 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:54

for x, y, z being ExtReal 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:55

for x, y, z being ExtReal 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:56

for x, y, z being ExtReal 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:57

for x, y, z being ExtReal 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:58

for x, y, z being ExtReal 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:59

for x, y, z being ExtReal 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:60

for x, y being ExtReal holds
( ( x <= - y implies y <= - x ) & ( - x <= y implies - y <= x ) )

proof end;

theorem :: XXREAL_3:61

for x, y being ExtReal st ( for e being Real st 0 < e holds
x < y + e ) holds
x <= y

proof end;

theorem :: XXREAL_3:62

for x, y, t being ExtReal st t <> -infty & t <> +infty & x < y holds
x + t < y + t

proof end;

theorem :: XXREAL_3:63

for x, y, t being ExtReal st t <> -infty & t <> +infty & x < y holds
x - t < y - t

proof end;

theorem :: XXREAL_3:64

for x, y, z, w being ExtReal st x < y & w < z holds
x + w < y + z

proof end;

theorem :: XXREAL_3:65

for x, y, z being ExtReal st 0 <= x & z + x <= y holds
z <= y

proof end;

definition

let x, y be ExtReal;

func x * y -> ExtReal means :Def5: :: XXREAL_3:def 5
ex a, b being Complex 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 ExtReal ex a, b being Complex 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 ExtReal 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 ExtReal 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 ExtReal st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being ExtReal holds
( ( x is real & y is real & ex a, b being Complex st
( x = a & y = b & b₁ = a * b ) & ex a, b being Complex 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 ExtReal 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 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 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 ExtReal st ( x is real & y is real implies ex a, b being Complex 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 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 ExtReal holds
( ( x is real & y is real implies ( b₃ = x * y iff ex a, b being Complex 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;
let a, b be Complex;

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

func x " -> ExtReal means :Def6: :: XXREAL_3:def 6
ex a being Complex st
( x = a & it = a " ) if x is real
otherwise it = 0 ;

existence
( ( x is real implies ex b₁ being ExtReal ex a being Complex st
( x = a & b₁ = a " ) ) & ( not x is real implies ex b₁ being ExtReal st b₁ = 0 ) )

proof end;

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

end;

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

registration

let x be Real;
let a be Complex;

identify x " with a " when x = a;

compatibility
( x = a implies x " = a " ) by Def6;

end;

definition

let x, y be ExtReal;

func x / y -> ExtReal equals :: XXREAL_3:def 7
x * (y ");

coherence
x * (y ") is ExtReal ;

end;

:: deftheorem defines / XXREAL_3:def 7 :
for x, y being ExtReal holds x / y = x * (y ");

registration

let x, y be Real;
let a, b be Complex;

identify x / y with a / b when x = a, y = b;

compatibility
( x = a & y = b implies x / y = a / b )

proof end;

end;

Lm17: for x being ExtReal holds x * 0 = 0

proof end;

registration

let x be positive ExtReal;
let y be negative ExtReal;

cluster x * y -> negative ;

coherence
x * y is negative

proof end;

end;

registration

let x, y be negative ExtReal;

cluster x * y -> positive ;

coherence
x * y is positive

proof end;

end;

registration

let x, y be positive ExtReal;

cluster x * y -> positive ;

coherence
x * y is positive

proof end;

end;

registration

let x be non positive ExtReal;
let y be non negative ExtReal;

cluster x * y -> non positive ;

coherence
not x * y is positive

proof end;

end;

registration

let x, y be non positive ExtReal;

cluster x * y -> non negative ;

coherence
not x * y is negative

proof end;

end;

registration

let x, y be non negative ExtReal;

cluster x * y -> non negative ;

coherence
not x * y is negative

proof end;

end;

registration

let x be non positive ExtReal;

cluster x " -> non positive ;

coherence
not x " is positive

proof end;

end;

registration

let x be non negative ExtReal;

cluster x " -> non negative ;

coherence
not x " is negative

proof end;

end;

registration

let x be non negative ExtReal;
let y be non positive ExtReal;

cluster x / y -> non positive ;

coherence
not x / y is positive ;

cluster y / x -> non positive ;

coherence
not y / x is positive ;

end;

registration

let x, y be non negative ExtReal;

cluster x / y -> non negative ;

coherence
not x / y is negative ;

end;

registration

let x, y be non positive ExtReal;

cluster x / y -> non negative ;

coherence
not x / y is negative ;

end;

Lm18: for x, y being ExtReal st not x is real & x * y = 0 holds
y = 0

proof end;

registration

let x, y be non zero ExtReal;

cluster x * y -> non zero ;

coherence
not x * y is zero

proof end;

end;

registration

let x be zero ExtReal;
let y be ExtReal;

cluster x * y -> zero for ExtReal;

coherence
for b₁ being ExtReal st b₁ = x * y holds
b₁ is zero by Lm17;

end;

Lm19: for x, y, z being ExtReal st x = 0 holds
x * (y * z) = (x * y) * z

proof end;

Lm20: for x, y, z being ExtReal st y = 0 holds
x * (y * z) = (x * y) * z

proof end;

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

proof end;

Lm22: for x, y, z being ExtReal st not x is real holds
x * (y * z) = (x * y) * z

proof end;

theorem Th66: :: XXREAL_3:66

for x, y, z being ExtReal holds x * (y * z) = (x * y) * z

proof end;

:: for ExtReals

registration

let r be Real;

cluster r " -> real ;

coherence
r " is real ;

end;

:: for ExtReals

registration

let r, s be Real;

cluster r * s -> real ;

coherence
r * s is real ;

cluster r / s -> real ;

coherence
r / s is real ;

end;

registration

cluster -infty " -> zero ;

coherence
-infty " is zero by Def6;

cluster +infty " -> zero ;

coherence
+infty " is zero by Def6;

end;

theorem :: XXREAL_3:67

for f, g being ExtReal holds (f * g) " = (f ") * (g ")

proof end;

theorem :: XXREAL_3:68

for r being Real
for f, g being ExtReal st r <> 0 & r * f = r * g holds
f = g

proof end;

theorem Th69: :: XXREAL_3:69

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

proof end;

theorem Th70: :: XXREAL_3:70

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

proof end;

Lm23: for x, y being ExtReal holds
( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 )

proof end;

theorem Th71: :: XXREAL_3:71

for x, y, z being ExtReal st x <= y & 0 <= z holds
x * z <= y * z

proof end;

theorem Th72: :: XXREAL_3:72

for x, y, z being ExtReal st x < y & 0 < z & z <> +infty holds
x * z < y * z

proof end;

theorem :: XXREAL_3:73

for x, y being ExtReal holds
( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 ) by Lm23;

theorem :: XXREAL_3:74

+infty " = 0 ;

theorem :: XXREAL_3:75

-infty " = 0 ;

theorem :: XXREAL_3:76

for x being ExtReal holds x / +infty = 0 ;

theorem :: XXREAL_3:77

for x being ExtReal holds x / -infty = 0 ;

theorem Th78: :: XXREAL_3:78

for x being ExtReal st x <> -infty & x <> +infty & x <> 0 holds
x / x = 1

proof end;

theorem :: XXREAL_3:79

for x, y, z being ExtReal st x <= y & 0 < z holds
x / z <= y / z by Th71;

theorem :: XXREAL_3:80

for x, y, z being ExtReal st x < y & 0 < z & z <> +infty holds
x / z < y / z

proof end;

theorem Th81: :: XXREAL_3:81

for x being ExtReal holds 1 * x = x

proof end;

theorem Th82: :: XXREAL_3:82

for y being ExtReal holds
( not y " = 0 or y = +infty or y = -infty or y = 0 )

proof end;

theorem Th83: :: XXREAL_3:83

for y being ExtReal st 0 < y & y <> +infty holds
+infty / y = +infty

proof end;

theorem Th84: :: XXREAL_3:84

for y being ExtReal st y < 0 & -infty <> y holds
-infty / y = +infty

proof end;

theorem Th85: :: XXREAL_3:85

for y being ExtReal st y < 0 & -infty <> y holds
+infty / y = -infty

proof end;

theorem Th86: :: XXREAL_3:86

for y being ExtReal st 0 < y & y <> +infty holds
-infty / y = -infty

proof end;

theorem :: XXREAL_3:87

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

proof end;

theorem :: XXREAL_3:88

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

proof end;

theorem :: XXREAL_3:89

for y being ExtReal holds
( +infty * y <> 1 & -infty * y <> 1 )

proof end;

theorem :: XXREAL_3:90

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

proof end;

theorem Th91: :: XXREAL_3:91

for x being ExtReal holds (- 1) * x = - x

proof end;

theorem Th92: :: XXREAL_3:92

for x, y being ExtReal holds - (x * y) = (- x) * y

proof end;

theorem Th93: :: XXREAL_3:93

for x, y, z being ExtReal st y = - z holds
x * (y + z) = (x * y) + (x * z)

proof end;

theorem Th94: :: XXREAL_3:94

for x being ExtReal holds 2 * x = x + x

proof end;

Lm24: for x, y being ExtReal holds x * (y + y) = (x * y) + (x * y)

proof end;

Lm25: for x, z being ExtReal holds x * (0 + z) = (x * 0) + (x * z)

proof end;

Lm26: for y, z being ExtReal holds 0 * (y + z) = (0 * y) + (0 * z)
;

Lm27: for x, y, z being ExtReal st x is real & y is real holds
x * (y + z) = (x * y) + (x * z)

proof end;

Lm28: for x, y, z being ExtReal st x is real & not y is real holds
x * (y + z) = (x * y) + (x * z)

proof end;

theorem Th95: :: XXREAL_3:95

for x, y, z being ExtReal st x is real holds
x * (y + z) = (x * y) + (x * z)

proof end;

theorem Th96: :: XXREAL_3:96

for x, y, z being ExtReal st y >= 0 & z >= 0 holds
x * (y + z) = (x * y) + (x * z)

proof end;

theorem :: XXREAL_3:97

for x, y, z being ExtReal st y <= 0 & z <= 0 holds
x * (y + z) = (x * y) + (x * z)

proof end;

theorem :: XXREAL_3:98

for x, z being ExtReal holds x * (0 + z) = (x * 0) + (x * z) by Lm25;

theorem :: XXREAL_3:99

for f being ExtReal holds (- f) " = - (f ")

proof end;

theorem :: XXREAL_3:100

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

proof end;

theorem Th101: :: XXREAL_3:101

for x, y, z being ExtReal st x <= y & z <= 0 holds
y * z <= x * z

proof end;

theorem Th102: :: XXREAL_3:102

for x, y, z being ExtReal st x < y & z < 0 & z <> -infty holds
y * z < x * z

proof end;

theorem :: XXREAL_3:103

for x, y, z being ExtReal st x <= y & z < 0 holds
y / z <= x / z by Th101;

theorem :: XXREAL_3:104

for x, y, z being ExtReal st x < y & z < 0 & z <> -infty holds
y / z < x / z

proof end;

theorem :: XXREAL_3:105

for x being ExtReal holds (x / 2) + (x / 2) = x

proof end;

registration

let x, y be Nat;

cluster x + y -> natural ;

coherence
x + y is natural ;

cluster x * y -> natural ;

coherence
x * y is natural ;

end;

registration

cluster - 1 -> dim-like ;

coherence
- 1 is dim-like ;
let n be dim-like number ;

cluster n + 1 -> natural ;

coherence
n + 1 is natural ;

end;