:: Basic Properties of Extended Real Numbers
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received September 7, 2000
:: Copyright (c) 2000 Association of Mizar Users

theorem :: EXTREAL1:1

canceled;

theorem :: EXTREAL1:2

canceled;

theorem :: EXTREAL1:3

canceled;

theorem Th4: :: EXTREAL1:4

for x being R_eal holds
( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) )

proof end;

Lm1: for x, y being R_eal st x in REAL & y in REAL holds
x + y in REAL

proof end;

theorem :: EXTREAL1:5

canceled;

theorem :: EXTREAL1:6

canceled;

theorem :: EXTREAL1:7

canceled;

theorem Th8: :: EXTREAL1:8

for x, y, z being R_eal st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & not ( y = +infty & z = -infty ) & not ( y = -infty & z = +infty ) & not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) holds
(x + y) + z = x + (y + z)

proof end;

theorem Th9: :: EXTREAL1:9

for x being R_eal holds x + (- x) = 0.

proof end;

theorem :: EXTREAL1:10

canceled;

theorem :: EXTREAL1:11

for x, y, z being R_eal st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) & ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) holds
(x + y) - z = x + (y - z)

proof end;

definition

let x, y be R_eal;
:: original: *
redefine func x * y -> R_eal means :Def1: :: EXTREAL1:def 1
( ex a, b being Real st
( x = a & y = b & it = a * b ) or ( ( ( 0. < x & y = +infty ) or ( 0. < y & x = +infty ) or ( x < 0. & y = -infty ) or ( y < 0. & x = -infty ) ) & it = +infty ) or ( ( ( x < 0. & y = +infty ) or ( y < 0. & x = +infty ) or ( 0. < x & y = -infty ) or ( 0. < y & x = -infty ) ) & it = -infty ) or ( ( x = 0. or y = 0. ) & it = 0. ) );
coherence
x * y is R_eal by XXREAL_0:def 1;
compatibility
for b₁ being R_eal holds
( b₁ = x * y iff ( ex a, b being Real st
( x = a & y = b & b₁ = a * b ) or ( ( ( 0. < x & y = +infty ) or ( 0. < y & x = +infty ) or ( x < 0. & y = -infty ) or ( y < 0. & x = -infty ) ) & b₁ = +infty ) or ( ( ( x < 0. & y = +infty ) or ( y < 0. & x = +infty ) or ( 0. < x & y = -infty ) or ( 0. < y & x = -infty ) ) & b₁ = -infty ) or ( ( x = 0. or y = 0. ) & b₁ = 0. ) ) )

proof end;

end;

:: deftheorem Def1 defines * EXTREAL1:def 1 :

for x, y, b₃ being R_eal holds
( b₃ = x * y iff ( ex a, b being Real st
( x = a & y = b & b₃ = a * b ) or ( ( ( 0. < x & y = +infty ) or ( 0. < y & x = +infty ) or ( x < 0. & y = -infty ) or ( y < 0. & x = -infty ) ) & b₃ = +infty ) or ( ( ( x < 0. & y = +infty ) or ( y < 0. & x = +infty ) or ( 0. < x & y = -infty ) or ( 0. < y & x = -infty ) ) & b₃ = -infty ) or ( ( x = 0. or y = 0. ) & b₃ = 0. ) ) );

theorem :: EXTREAL1:12

canceled;

theorem Th13: :: EXTREAL1:13

for x, y being R_eal
for a, b being Real st x = a & y = b holds
x * y = a * b

proof end;

theorem Th14: :: EXTREAL1:14

for x, y being R_eal st ( ( 0. <= x & 0. < y ) or ( 0. < x & 0. <= y ) ) holds
0. < x + y

proof end;

theorem Th15: :: EXTREAL1:15

for x, y being R_eal st ( ( x <= 0. & y < 0. ) or ( x < 0. & y <= 0. ) ) holds
x + y < 0.

proof end;

theorem :: EXTREAL1:16

canceled;

theorem :: EXTREAL1:17

canceled;

theorem :: EXTREAL1:18

canceled;

theorem :: EXTREAL1:19

canceled;

theorem Th20: :: EXTREAL1:20

for x, y being R_eal st ( ( 0. < x & 0. < y ) or ( x < 0. & y < 0. ) ) holds
0. < x * y

proof end;

theorem Th21: :: EXTREAL1:21

for x, y being R_eal st ( ( 0. < x & y < 0. ) or ( x < 0. & 0. < y ) ) holds
x * y < 0.

proof end;

theorem :: EXTREAL1:22

for x, y being R_eal holds
( x * y = 0. iff ( x = 0. or y = 0. ) )

proof end;

theorem :: EXTREAL1:23

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

proof end;

theorem Th24: :: EXTREAL1:24

- 0. = 0.

proof end;

theorem :: EXTREAL1:25

for x being R_eal holds
( ( 0. < x implies - x < 0. ) & ( - x < 0. implies 0. < x ) & ( x < 0. implies 0. < - x ) & ( 0. < - x implies x < 0. ) ) by Th24, SUPINF_2:17;

theorem Th26: :: EXTREAL1:26

for x, y being R_eal holds
( - (x * y) = x * (- y) & - (x * y) = (- x) * y )

proof end;

theorem :: EXTREAL1:27

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

proof end;

theorem :: EXTREAL1:28

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

proof end;

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

proof end;

theorem :: EXTREAL1:29

for x, y, z being R_eal st ( ( x <> +infty & x <> -infty ) or ( y = -infty & z = +infty ) or ( y < 0. & z < 0. ) or y = 0. or z = 0. or ( 0. < y & 0. < z ) or ( y = +infty & z = -infty ) ) holds
x * (y + z) = (x * y) + (x * z)

proof end;

theorem :: EXTREAL1:30

for y, z, x being R_eal holds
( ( y = +infty & z = +infty ) or ( y = -infty & z = -infty ) or not x <> +infty or not x <> -infty or x * (y - z) = (x * y) - (x * z) )

proof end;

definition

let x, y be R_eal;
assume A1: ( ( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) ) & y <> 0. ) ;
:: original: /
redefine func x / y -> R_eal means :Def2: :: EXTREAL1:def 2
( ex a, b being Real st
( x = a & y = b & it = a / b ) or ( ( ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) ) & it = +infty ) or ( ( ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) ) & it = -infty ) or ( ( y = -infty or y = +infty ) & it = 0. ) );
coherence
x / y is R_eal by XXREAL_0:def 1;
compatibility
for b₁ being R_eal holds
( b₁ = x / y iff ( ex a, b being Real st
( x = a & y = b & b₁ = a / b ) or ( ( ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) ) & b₁ = +infty ) or ( ( ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) ) & b₁ = -infty ) or ( ( y = -infty or y = +infty ) & b₁ = 0. ) ) )

proof end;

end;

:: deftheorem Def2 defines / EXTREAL1:def 2 :

for x, y being R_eal st ( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) ) & y <> 0. holds
for b₃ being R_eal holds
( b₃ = x / y iff ( ex a, b being Real st
( x = a & y = b & b₃ = a / b ) or ( ( ( x = +infty & 0. < y ) or ( x = -infty & y < 0. ) ) & b₃ = +infty ) or ( ( ( x = -infty & 0. < y ) or ( x = +infty & y < 0. ) ) & b₃ = -infty ) or ( ( y = -infty or y = +infty ) & b₃ = 0. ) ) );

theorem :: EXTREAL1:31

canceled;

theorem Th32: :: EXTREAL1:32

for x, y being R_eal st y <> 0. holds
for a, b being Real st x = a & y = b holds
x / y = a / b

proof end;

theorem :: EXTREAL1:33

for x, y being R_eal st x <> -infty & x <> +infty & ( y = -infty or y = +infty ) holds
x / y = 0. by Def2;

theorem :: EXTREAL1:34

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

proof end;

definition

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

end;

:: deftheorem Def3 defines |. EXTREAL1:def 3 :

for x being R_eal holds
( ( 0. <= x implies |.x.| = x ) & ( not 0. <= x implies |.x.| = - x ) );

theorem :: EXTREAL1:35

canceled;

theorem :: EXTREAL1:36

for x being R_eal st 0. < x holds
|.x.| = x by Def3;

theorem :: EXTREAL1:37

for x being R_eal st x < 0. holds
|.x.| = - x by Def3;

theorem :: EXTREAL1:38

for a, b being Real holds a * b = (R_EAL a) * (R_EAL b)

proof end;

theorem :: EXTREAL1:39

for a, b being Real st b <> 0 holds
a / b = (R_EAL a) / (R_EAL b)

proof end;

theorem :: EXTREAL1:40

canceled;

theorem :: EXTREAL1:41

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

proof end;

theorem :: EXTREAL1:42

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

proof end;

theorem :: EXTREAL1:43

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

proof end;

theorem :: EXTREAL1:44

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

proof end;

theorem :: EXTREAL1:45

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

proof end;

theorem :: EXTREAL1:46

for x, y being R_eal st x is Real & y is Real holds
( x < y iff ex p, q being Real st
( p = x & q = y & p < q ) ) ;

theorem :: EXTREAL1:47

for x, y, z being R_eal st x <> -infty & y <> +infty & x <= y & 0. < z holds
x / z <= y / z

proof end;

theorem :: EXTREAL1:48

for x, y, z being R_eal st x <= y & 0. < z & z <> +infty holds
x / z <= y / z

proof end;

theorem :: EXTREAL1:49

for x, y, z being R_eal st x <> -infty & y <> +infty & x <= y & z < 0. holds
y / z <= x / z

proof end;

theorem :: EXTREAL1:50

for x, y, z being R_eal st x <= y & z < 0. & z <> -infty holds
y / z <= x / z

proof end;

theorem :: EXTREAL1:51

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

proof end;

theorem :: EXTREAL1:52

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

proof end;