:: EXTREAL1 semantic presentation

theorem Th1: :: EXTREAL1:1

for b₁ being R_eal st b₁ <> +infty & b₁ <> -infty holds
b₁ is Real

proof end;

theorem Th2: :: EXTREAL1:2

proof end;

theorem Th3: :: EXTREAL1:3

for b₁, b₂ being R_eal st b₁ <' b₂ holds
( b₁ <> +infty & b₂ <> -infty ) by SUPINF_1:20, SUPINF_1:21;

theorem Th4: :: EXTREAL1:4

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

proof end;

theorem Th5: :: EXTREAL1:5

for b₁, b₂ being R_eal holds b₁ - (- b₂) = b₁ + b₂

proof end;

theorem Th6: :: EXTREAL1:6

canceled;

theorem Th7: :: EXTREAL1:7

for b₁, b₂ being R_eal st b₁ <> -infty & b₂ <> +infty & b₁ <=' b₂ holds
( b₁ <> +infty & b₂ <> -infty )

proof end;

Lemma7: for b₁ being R_eal st b₁ in REAL holds
( b₁ + -infty = -infty & b₁ + +infty = +infty )
by SUPINF_1:2, SUPINF_1:6, SUPINF_2:def 2;

Lemma8: for b₁, b₂ being R_eal st b₁ in REAL & b₂ in REAL holds
b₁ + b₂ in REAL

proof end;

theorem Th8: :: EXTREAL1:8

for b₁, b₂, b₃ being R_eal st ( not b₁ = +infty or not b₂ = -infty ) & ( not b₁ = -infty or not b₂ = +infty ) & not ( b₂ = +infty & b₃ = -infty ) & not ( b₂ = -infty & b₃ = +infty ) & not ( b₁ = +infty & b₃ = -infty ) & not ( b₁ = -infty & b₃ = +infty ) holds
(b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

proof end;

theorem Th9: :: EXTREAL1:9

for b₁ being R_eal holds b₁ + (- b₁) = 0.

proof end;

theorem Th10: :: EXTREAL1:10

canceled;

theorem Th11: :: EXTREAL1:11

for b₁, b₂, b₃ being R_eal st ( not b₁ = +infty or not b₂ = -infty ) & ( not b₁ = -infty or not b₂ = +infty ) & ( not b₂ = +infty or not b₃ = +infty ) & ( not b₂ = -infty or not b₃ = -infty ) & ( not b₁ = +infty or not b₃ = +infty ) & ( not b₁ = -infty or not b₃ = -infty ) holds
(b₁ + b₂) - b₃ = b₁ + (b₂ - b₃)

proof end;

definition

let c₁, c₂ be R_eal;
func c₁ * c₂ -> R_eal means :Def1: :: EXTREAL1:def 1
( ex b₁, b₂ being Real st
( a₁ = b₁ & a₂ = b₂ & a₃ = b₁ * b₂ ) or ( ( ( 0. <' a₁ & a₂ = +infty ) or ( 0. <' a₂ & a₁ = +infty ) or ( a₁ <' 0. & a₂ = -infty ) or ( a₂ <' 0. & a₁ = -infty ) ) & a₃ = +infty ) or ( ( ( a₁ <' 0. & a₂ = +infty ) or ( a₂ <' 0. & a₁ = +infty ) or ( 0. <' a₁ & a₂ = -infty ) or ( 0. <' a₂ & a₁ = -infty ) ) & a₃ = -infty ) or ( ( a₁ = 0. or a₂ = 0. ) & a₃ = 0. ) );
existence

proof end;

uniqueness by SUPINF_1:31, SUPINF_2:def 1;

end;

:: deftheorem Def1 defines * EXTREAL1:def 1 :

theorem Th12: :: EXTREAL1:12

canceled;

theorem Th13: :: EXTREAL1:13

for b₁, b₂ being R_eal
for b₃, b₄ being Real st b₁ = b₃ & b₂ = b₄ holds
b₁ * b₂ = b₃ * b₄

proof end;

Lemma13: for b₁ being R_eal
for b₂ being Real st b₁ = b₂ & 0 < b₂ holds
0. <' b₁

proof end;

Lemma14: for b₁ being R_eal
for b₂ being Real st b₁ = b₂ & b₂ < 0 holds
b₁ <' 0.

proof end;

theorem Th14: :: EXTREAL1:14

for b₁, b₂ being R_eal st ( ( 0. <=' b₁ & 0. <' b₂ ) or ( 0. <' b₁ & 0. <=' b₂ ) ) holds
0. <' b₁ + b₂

proof end;

theorem Th15: :: EXTREAL1:15

for b₁, b₂ being R_eal st ( ( b₁ <=' 0. & b₂ <' 0. ) or ( b₁ <' 0. & b₂ <=' 0. ) ) holds
b₁ + b₂ <' 0.

proof end;

theorem Th16: :: EXTREAL1:16

for b₁ being R_eal holds
( not b₁ in REAL or ( -infty <' b₁ & b₁ <' 0. ) or b₁ = 0. or ( 0. <' b₁ & b₁ <' +infty ) )

proof end;

theorem Th17: :: EXTREAL1:17

for b₁, b₂ being R_eal holds b₁ * b₂ = b₂ * b₁

proof end;

definition

let c₁, c₂ be R_eal;
redefine func * as c₁ * c₂ -> R_eal;
commutativity by Th17;

end;

theorem Th18: :: EXTREAL1:18

for b₁ being R_eal
for b₂ being Real st b₁ = b₂ holds
( 0 < b₂ iff 0. <' b₁ ) by Lemma13, SUPINF_1:16, SUPINF_2:def 1;

theorem Th19: :: EXTREAL1:19

for b₁ being R_eal
for b₂ being Real st b₁ = b₂ holds
( b₂ < 0 iff b₁ <' 0. ) by Lemma14, SUPINF_1:16, SUPINF_2:def 1;

theorem Th20: :: EXTREAL1:20

for b₁, b₂ being R_eal st ( ( 0. <' b₁ & 0. <' b₂ ) or ( b₁ <' 0. & b₂ <' 0. ) ) holds
0. <' b₁ * b₂

proof end;

theorem Th21: :: EXTREAL1:21

for b₁, b₂ being R_eal st ( ( 0. <' b₁ & b₂ <' 0. ) or ( b₁ <' 0. & 0. <' b₂ ) ) holds
b₁ * b₂ <' 0.

proof end;

theorem Th22: :: EXTREAL1:22

for b₁, b₂ being R_eal holds
( b₁ * b₂ = 0. iff ( b₁ = 0. or b₂ = 0. ) )

proof end;

theorem Th23: :: EXTREAL1:23

for b₁, b₂, b₃ being R_eal holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃)

proof end;

theorem Th24: :: EXTREAL1:24

- 0. = 0.

proof end;

theorem Th25: :: EXTREAL1:25

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

theorem Th26: :: EXTREAL1:26

for b₁, b₂ being R_eal holds
( - (b₁ * b₂) = b₁ * (- b₂) & - (b₁ * b₂) = (- b₁) * b₂ )

proof end;

theorem Th27: :: EXTREAL1:27

for b₁, b₂ being R_eal st b₁ <> +infty & b₁ <> -infty & b₁ * b₂ = +infty & not b₂ = +infty holds
b₂ = -infty

proof end;

theorem Th28: :: EXTREAL1:28

for b₁, b₂ being R_eal st b₁ <> +infty & b₁ <> -infty & b₁ * b₂ = -infty & not b₂ = +infty holds
b₂ = -infty

proof end;

Lemma23: for b₁, b₂, b₃ being R_eal st b₁ <> +infty & b₁ <> -infty holds
b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃)

proof end;

theorem Th29: :: EXTREAL1:29

for b₁, b₂, b₃ being R_eal st ( ( b₁ <> +infty & b₁ <> -infty ) or ( b₂ = -infty & b₃ = +infty ) or ( b₂ <' 0. & b₃ <' 0. ) or b₂ = 0. or b₃ = 0. or ( 0. <' b₂ & 0. <' b₃ ) or ( b₂ = +infty & b₃ = -infty ) ) holds
b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃)

proof end;

theorem Th30: :: EXTREAL1:30

for b₁, b₂, b₃ being R_eal holds
( ( b₁ = +infty & b₂ = +infty ) or ( b₁ = -infty & b₂ = -infty ) or not b₃ <> +infty or not b₃ <> -infty or b₃ * (b₁ - b₂) = (b₃ * b₁) - (b₃ * b₂) )

proof end;

definition

let c₁, c₂ be R_eal;
assume E24: ( ( ( not c₁ = -infty & not c₁ = +infty ) or ( not c₂ = -infty & not c₂ = +infty ) ) & c₂ <> 0. ) ;
func c₁ / c₂ -> R_eal means :Def2: :: EXTREAL1:def 2
( ex b₁, b₂ being Real st
( a₁ = b₁ & a₂ = b₂ & a₃ = b₁ / b₂ ) or ( ( ( a₁ = +infty & 0. <' a₂ ) or ( a₁ = -infty & a₂ <' 0. ) ) & a₃ = +infty ) or ( ( ( a₁ = -infty & 0. <' a₂ ) or ( a₁ = +infty & a₂ <' 0. ) ) & a₃ = -infty ) or ( ( a₂ = -infty or a₂ = +infty ) & a₃ = 0. ) );
existence

proof end;

uniqueness by E24, SUPINF_1:31;

end;

:: deftheorem Def2 defines / EXTREAL1:def 2 :

theorem Th31: :: EXTREAL1:31

canceled;

theorem Th32: :: EXTREAL1:32

for b₁, b₂ being R_eal st b₂ <> 0. holds
for b₃, b₄ being Real st b₁ = b₃ & b₂ = b₄ holds
b₁ / b₂ = b₃ / b₄

proof end;

theorem Th33: :: EXTREAL1:33

for b₁, b₂ being R_eal st b₁ <> -infty & b₁ <> +infty & ( b₂ = -infty or b₂ = +infty ) holds
b₁ / b₂ = 0. by Def2, SUPINF_2:19;

theorem Th34: :: EXTREAL1:34

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

proof end;

definition

let c₁ be R_eal;
func |.c₁.| -> R_eal equals :Def3: :: EXTREAL1:def 3
a₁ if 0. <=' a₁
otherwise - a₁;
coherence ;
consistency ;

end;

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

theorem Th35: :: EXTREAL1:35

canceled;

theorem Th36: :: EXTREAL1:36

for b₁ being R_eal st 0. <' b₁ holds
|.b₁.| = b₁ by Def3;

theorem Th37: :: EXTREAL1:37

for b₁ being R_eal st b₁ <' 0. holds
|.b₁.| = - b₁ by Def3;

theorem Th38: :: EXTREAL1:38

for b₁, b₂ being Real holds R_EAL (b₁ * b₂) = (R_EAL b₁) * (R_EAL b₂)

proof end;

theorem Th39: :: EXTREAL1:39

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

proof end;

theorem Th40: :: EXTREAL1:40

for b₁, b₂ being R_eal st b₁ <=' b₂ & b₁ <' +infty & -infty <' b₂ holds
0. <=' b₂ - b₁

proof end;

theorem Th41: :: EXTREAL1:41

for b₁, b₂ being R_eal st b₁ <' b₂ & b₁ <' +infty & -infty <' b₂ holds
0. <' b₂ - b₁

proof end;

theorem Th42: :: EXTREAL1:42

for b₁, b₂, b₃ being R_eal st b₁ <=' b₂ & 0. <=' b₃ holds
b₁ * b₃ <=' b₂ * b₃

proof end;

theorem Th43: :: EXTREAL1:43

for b₁, b₂, b₃ being R_eal st b₁ <=' b₂ & b₃ <=' 0. holds
b₂ * b₃ <=' b₁ * b₃

proof end;

theorem Th44: :: EXTREAL1:44

for b₁, b₂, b₃ being R_eal st b₁ <' b₂ & 0. <' b₃ & b₃ <> +infty holds
b₁ * b₃ <' b₂ * b₃

proof end;

theorem Th45: :: EXTREAL1:45

for b₁, b₂, b₃ being R_eal st b₁ <' b₂ & b₃ <' 0. & b₃ <> -infty holds
b₂ * b₃ <' b₁ * b₃

proof end;

theorem Th46: :: EXTREAL1:46

for b₁, b₂ being R_eal st b₁ is Real & b₂ is Real holds
( b₁ <' b₂ iff ex b₃, b₄ being Real st
( b₃ = b₁ & b₄ = b₂ & b₃ < b₄ ) )

proof end;

theorem Th47: :: EXTREAL1:47

for b₁, b₂, b₃ being R_eal st b₁ <> -infty & b₂ <> +infty & b₁ <=' b₂ & 0. <' b₃ holds
b₁ / b₃ <=' b₂ / b₃

proof end;

theorem Th48: :: EXTREAL1:48

for b₁, b₂, b₃ being R_eal st b₁ <=' b₂ & 0. <' b₃ & b₃ <> +infty holds
b₁ / b₃ <=' b₂ / b₃

proof end;

theorem Th49: :: EXTREAL1:49

for b₁, b₂, b₃ being R_eal st b₁ <> -infty & b₂ <> +infty & b₁ <=' b₂ & b₃ <' 0. holds
b₂ / b₃ <=' b₁ / b₃

proof end;

theorem Th50: :: EXTREAL1:50

for b₁, b₂, b₃ being R_eal st b₁ <=' b₂ & b₃ <' 0. & b₃ <> -infty holds
b₂ / b₃ <=' b₁ / b₃

proof end;

theorem Th51: :: EXTREAL1:51

for b₁, b₂, b₃ being R_eal st b₁ <' b₂ & 0. <' b₃ & b₃ <> +infty holds
b₁ / b₃ <' b₂ / b₃

proof end;

theorem Th52: :: EXTREAL1:52

for b₁, b₂, b₃ being R_eal st b₁ <' b₂ & b₃ <' 0. & b₃ <> -infty holds
b₂ / b₃ <' b₁ / b₃

proof end;