XXREAL_3: Basic Operations on Extended Real Numbers

proof end;

cluster ext-real negative non real for set ;

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 for set ;

coherence ;

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

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 ;

proof end;

uniqueness ;
consistency ;
commutativity ;

end;

:: deftheorem Def2 defines + XXREAL_3:def 2 :

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 ;

proof end;

uniqueness ;
consistency ;
involutiveness

proof end;

end;

:: deftheorem Def3 defines - XXREAL_3:def 3 :

definition

let x, y be ext-real number ;

func x - y -> ext-real number equals :: XXREAL_3:def 4
x + (- y);

end;

:: deftheorem defines - XXREAL_3:def 4 :

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 by Def2;

end;

registration

let x be real number ;
let a be complex number ;

identify - x with - a when x = a;

compatibility by Def3;

end;

:: for ext-real numbers

registration

let r be real number ;

cluster - r -> ext-real real ;

end;

:: for ext-real numbers

registration

let r, s be real number ;

cluster r + s -> ext-real real ;

coherence ;

cluster r - s -> ext-real real ;

end;

registration

let x be real number ;
let y be ext-real non real number ;

cluster x + y -> non real for number ;

proof end;

end;

registration

let x, y be ext-real positive non real number ;

cluster x + y -> ext-real non real ;

proof end;

end;

registration

let x, y be ext-real negative non real number ;

cluster x + y -> ext-real non 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 ;

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 ;

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 Th25: :: XXREAL_3:25

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

proof end;

theorem :: XXREAL_3:26

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

proof end;

theorem Th27: :: XXREAL_3:27

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

proof end;

theorem :: XXREAL_3:28

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

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

proof end;

end;

registration

let x, y be ext-real non positive number ;

cluster x + y -> ext-real non 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 by Lm13;

cluster y + x -> ext-real 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 by Lm14;

cluster y + x -> ext-real negative ;

end;

registration

let x be ext-real non positive number ;

cluster - x -> ext-real non negative ;

proof end;

end;

registration

let x be ext-real non negative number ;

cluster - x -> ext-real non positive ;

proof end;

end;

registration

let x be ext-real positive number ;

cluster - x -> ext-real negative ;

proof end;

end;

registration

let x be ext-real negative number ;

cluster - x -> ext-real 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 ;

cluster y - x -> ext-real non 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 ;

cluster y - x -> ext-real 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 ;

cluster y - x -> ext-real positive ;

end;

Lm15: for x, y being ext-real number st x <= y holds
- y <= - x

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

theorem Th38: :: XXREAL_3:38

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

proof end;

theorem Th39: :: XXREAL_3:39

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

proof end;

theorem :: XXREAL_3:40

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

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

theorem Th46: :: XXREAL_3:46

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

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

theorem :: XXREAL_3:60

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

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

theorem :: XXREAL_3:65

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 ;

proof end;

uniqueness ;
consistency ;
commutativity ;

end;

:: deftheorem Def5 defines * XXREAL_3:def 5 :

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

proof end;

uniqueness ;
consistency ;

end;

:: deftheorem Def6 defines " XXREAL_3:def 6 :

registration

let x be real number ;
let a be complex number ;

identify x " with a " when x = a;

compatibility by Def6;

end;

definition

let x, y be ext-real number ;

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

end;

:: deftheorem defines / XXREAL_3:def 7 :

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

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 ;

proof end;

end;

registration

let x, y be ext-real negative number ;

cluster x * y -> ext-real positive ;

proof end;

end;

registration

let x, y be ext-real positive number ;

cluster x * y -> ext-real 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 ;

proof end;

end;

registration

let x, y be ext-real non positive number ;

cluster x * y -> ext-real non negative ;

proof end;

end;

registration

let x, y be ext-real non negative number ;

cluster x * y -> ext-real non negative ;

proof end;

end;

registration

let x be ext-real non positive number ;

cluster x " -> ext-real non positive ;

proof end;

end;

registration

let x be ext-real non negative number ;

cluster x " -> ext-real non 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 ;

cluster y / x -> ext-real non positive ;

end;

registration

let x, y be ext-real non negative number ;

cluster x / y -> ext-real non negative ;

end;

registration

let x, y be ext-real non positive number ;

cluster x / y -> ext-real non 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 ;

proof end;

end;

registration

let x be zero ext-real number ;
let y be ext-real number ;

cluster x * y -> zero ext-real for ext-real number ;

coherence 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 Th66: :: XXREAL_3:66

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

proof end;

:: for ext-real numbers

registration

let r be real number ;

cluster r " -> ext-real real ;

end;

:: for ext-real numbers

registration

let r, s be real number ;

cluster r * s -> ext-real real ;

coherence ;

cluster r / s -> ext-real real ;