:: EXTREAL2 semantic presentation

theorem Th1: :: EXTREAL2:1

canceled;

theorem Th2: :: EXTREAL2:2

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

proof end;

theorem Th3: :: EXTREAL2:3

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

proof end;

theorem Th4: :: EXTREAL2:4

for b₁ being R_eal holds
( 1. * b₁ = b₁ & b₁ * 1. = b₁ & (R_EAL 1) * b₁ = b₁ & b₁ * (R_EAL 1) = b₁ )

proof end;

theorem Th5: :: EXTREAL2:5

for b₁ being R_eal holds 0. - b₁ = - b₁

proof end;

theorem Th6: :: EXTREAL2:6

canceled;

theorem Th7: :: EXTREAL2:7

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

proof end;

theorem Th8: :: EXTREAL2:8

canceled;

theorem Th9: :: EXTREAL2:9

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

proof end;

theorem Th10: :: EXTREAL2:10

canceled;

theorem Th11: :: EXTREAL2:11

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

proof end;

theorem Th12: :: EXTREAL2:12

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

proof end;

theorem Th13: :: EXTREAL2:13

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

proof end;

theorem Th14: :: EXTREAL2:14

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

proof end;

theorem Th15: :: EXTREAL2:15

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

proof end;

theorem Th16: :: EXTREAL2:16

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

proof end;

theorem Th17: :: EXTREAL2:17

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

proof end;

theorem Th18: :: EXTREAL2:18

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

proof end;

theorem Th19: :: EXTREAL2:19

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

proof end;

theorem Th20: :: EXTREAL2:20

( 1. <' +infty & -infty <' 1. ) by MESFUNC1:def 8, SUPINF_1:31;

theorem Th21: :: EXTREAL2:21

for b₁ being R_eal st ( b₁ = +infty or b₁ = -infty ) holds
for b₂ being R_eal st b₂ in REAL holds
b₁ + b₂ <> 0.

proof end;

theorem Th22: :: EXTREAL2:22

for b₁ being R_eal st ( b₁ = +infty or b₁ = -infty ) holds
for b₂ being R_eal holds b₁ * b₂ <> 1.

proof end;

theorem Th23: :: EXTREAL2:23

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

proof end;

theorem Th24: :: EXTREAL2:24

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

proof end;

theorem Th25: :: EXTREAL2:25

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

proof end;

theorem Th26: :: EXTREAL2:26

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

proof end;

theorem Th27: :: EXTREAL2:27

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

proof end;

theorem Th28: :: EXTREAL2:28

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

proof end;

theorem Th29: :: EXTREAL2:29

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

proof end;

theorem Th30: :: EXTREAL2:30

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

proof end;

theorem Th31: :: EXTREAL2:31

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

proof end;

theorem Th32: :: EXTREAL2:32

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 ) & b₁ <=' b₃ - b₂ holds
( b₂ <> +infty & b₁ + b₂ <=' b₃ )

proof end;

theorem Th33: :: EXTREAL2:33

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

proof end;

theorem Th34: :: EXTREAL2:34

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 ) & b₁ <=' b₃ + b₂ holds
( b₂ <> -infty & b₁ - b₂ <=' b₃ )

proof end;

theorem Th35: :: EXTREAL2:35

canceled;

theorem Th36: :: EXTREAL2:36

canceled;

theorem Th37: :: EXTREAL2:37

canceled;

theorem Th38: :: EXTREAL2:38

canceled;

theorem Th39: :: EXTREAL2:39

canceled;

theorem Th40: :: EXTREAL2:40

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;

theorem Th41: :: EXTREAL2:41

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;

theorem Th42: :: EXTREAL2:42

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

proof end;

theorem Th43: :: EXTREAL2:43

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

proof end;

theorem Th44: :: EXTREAL2:44

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

proof end;

theorem Th45: :: EXTREAL2:45

for b₁, b₂ being R_eal holds
( ( ( ( 0. <=' b₁ or 0. <' b₁ ) & ( 0. <=' b₂ or 0. <' b₂ ) ) or ( ( b₁ <=' 0. or b₁ <' 0. ) & ( b₂ <=' 0. or b₂ <' 0. ) ) ) iff 0. <=' b₁ * b₂ ) by Th44;

theorem Th46: :: EXTREAL2:46

for b₁, b₂ being R_eal holds
( ( ( ( b₁ <=' 0. or b₁ <' 0. ) & ( 0. <=' b₂ or 0. <' b₂ ) ) or ( ( 0. <=' b₁ or 0. <' b₁ ) & ( b₂ <=' 0. or b₂ <' 0. ) ) ) iff b₁ * b₂ <=' 0. ) by Th43;

theorem Th47: :: EXTREAL2:47

for b₁, b₂ being R_eal holds
( ( b₁ <=' - b₂ implies b₂ <=' - b₁ ) & ( b₂ <=' - b₁ implies b₁ <=' - b₂ ) & ( - b₁ <=' b₂ implies - b₂ <=' b₁ ) & ( - b₂ <=' b₁ implies - b₁ <=' b₂ ) )

proof end;

theorem Th48: :: EXTREAL2:48

for b₁, b₂ being R_eal holds
( ( b₁ <' - b₂ implies b₂ <' - b₁ ) & ( b₂ <' - b₁ implies b₁ <' - b₂ ) & ( - b₁ <' b₂ implies - b₂ <' b₁ ) & ( - b₂ <' b₁ implies - b₁ <' b₂ ) )

proof end;

theorem Th49: :: EXTREAL2:49

for b₁ being R_eal
for b₂ being Real st b₁ = b₂ holds
|.b₁.| = abs b₂

proof end;

theorem Th50: :: EXTREAL2:50

for b₁ being R_eal holds
( |.b₁.| = b₁ or |.b₁.| = - b₁ )

proof end;

theorem Th51: :: EXTREAL2:51

for b₁ being R_eal holds 0. <=' |.b₁.|

proof end;

theorem Th52: :: EXTREAL2:52

for b₁ being R_eal st b₁ <> 0. holds
0. <' |.b₁.|

proof end;

theorem Th53: :: EXTREAL2:53

for b₁ being R_eal holds
( b₁ = 0. iff |.b₁.| = 0. ) by Th52, EXTREAL1:def 3;

theorem Th54: :: EXTREAL2:54

for b₁ being R_eal st |.b₁.| = - b₁ & b₁ <> 0. holds
b₁ <' 0.

proof end;

theorem Th55: :: EXTREAL2:55

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

proof end;

theorem Th56: :: EXTREAL2:56

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

proof end;

theorem Th57: :: EXTREAL2:57

for b₁ being R_eal holds
( - |.b₁.| <=' b₁ & b₁ <=' |.b₁.| )

proof end;

theorem Th58: :: EXTREAL2:58

for b₁, b₂ being R_eal st |.b₁.| <' b₂ holds
( - b₂ <' b₁ & b₁ <' b₂ )

proof end;

theorem Th59: :: EXTREAL2:59

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

proof end;

theorem Th60: :: EXTREAL2:60

for b₁, b₂ being R_eal holds
( ( - b₁ <=' b₂ & b₂ <=' b₁ ) iff |.b₂.| <=' b₁ )

proof end;

theorem Th61: :: EXTREAL2:61

for b₁, b₂ being R_eal holds
( ( b₁ = +infty & b₂ = -infty ) or ( b₁ = -infty & b₂ = +infty ) or |.(b₁ + b₂).| <=' |.b₁.| + |.b₂.| )

proof end;

theorem Th62: :: EXTREAL2:62

for b₁ being R_eal st -infty <' b₁ & b₁ <' +infty & b₁ <> 0. holds
|.b₁.| * |.(1. / b₁).| = 1.

proof end;

theorem Th63: :: EXTREAL2:63

for b₁ being R_eal st ( b₁ = +infty or b₁ = -infty ) holds
|.b₁.| * |.(1. / b₁).| = 0.

proof end;

theorem Th64: :: EXTREAL2:64

for b₁ being R_eal st b₁ <> 0. holds
|.(1. / b₁).| = 1. / |.b₁.|

proof end;

theorem Th65: :: EXTREAL2:65

for b₁, b₂ being R_eal st ( ( not b₁ = -infty & not b₁ = +infty ) or ( not b₂ = -infty & not b₂ = +infty ) ) & b₂ <> 0. holds
|.(b₁ / b₂).| = |.b₁.| / |.b₂.|

proof end;

theorem Th66: :: EXTREAL2:66

for b₁ being R_eal holds |.b₁.| = |.(- b₁).|

proof end;

theorem Th67: :: EXTREAL2:67

for b₁ being R_eal st ( b₁ = +infty or b₁ = -infty ) holds
|.b₁.| = +infty

proof end;

theorem Th68: :: EXTREAL2:68

for b₁, b₂ being R_eal st ( b₁ is Real or b₂ is Real ) holds
|.b₁.| - |.b₂.| <=' |.(b₁ - b₂).|

proof end;

theorem Th69: :: EXTREAL2:69

for b₁, b₂ being R_eal holds
( ( b₁ = +infty & b₂ = +infty ) or ( b₁ = -infty & b₂ = -infty ) or |.(b₁ - b₂).| <=' |.b₁.| + |.b₂.| )

proof end;

theorem Th70: :: EXTREAL2:70

for b₁ being R_eal holds |.|.b₁.|.| = |.b₁.|

proof end;

theorem Th71: :: EXTREAL2:71

for b₁, b₂, b₃, b₄ being R_eal holds
( ( b₁ = +infty & b₂ = -infty ) or ( b₁ = -infty & b₂ = +infty ) or not |.b₁.| <=' b₃ or not |.b₂.| <=' b₄ or |.(b₁ + b₂).| <=' b₃ + b₄ )

proof end;

theorem Th72: :: EXTREAL2:72

for b₁, b₂ being R_eal st ( b₁ is Real or b₂ is Real ) holds
|.(|.b₁.| - |.b₂.|).| <=' |.(b₁ - b₂).|

proof end;

theorem Th73: :: EXTREAL2:73

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

proof end;

theorem Th74: :: EXTREAL2:74

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

proof end;

definition

let c₁, c₂ be R_eal;
func min c₁,c₂ -> R_eal equals :Def1: :: EXTREAL2:def 1
a₁ if a₁ <=' a₂
otherwise a₂;
correctness ;
commutativity

proof end;

idempotence ;
func max c₁,c₂ -> R_eal equals :Def2: :: EXTREAL2:def 2
a₁ if a₂ <=' a₁
otherwise a₂;
correctness ;
commutativity

proof end;

idempotence ;

end;

:: deftheorem Def1 defines min EXTREAL2:def 1 :

:: deftheorem Def2 defines max EXTREAL2:def 2 :

theorem Th75: :: EXTREAL2:75

for b₁, b₂ being R_eal st ( b₁ = -infty or b₂ = -infty ) holds
min b₁,b₂ = -infty

proof end;

theorem Th76: :: EXTREAL2:76

for b₁, b₂ being R_eal st ( b₁ = +infty or b₂ = +infty ) holds
max b₁,b₂ = +infty

proof end;

theorem Th77: :: EXTREAL2:77

for b₁, b₂ being R_eal
for b₃, b₄ being Real st b₁ = b₃ & b₂ = b₄ holds
( min b₁,b₂ = min b₃,b₄ & max b₁,b₂ = max b₃,b₄ )

proof end;

theorem Th78: :: EXTREAL2:78

for b₁, b₂ being R_eal st b₁ <=' b₂ holds
min b₂,b₁ = b₁

proof end;

theorem Th79: :: EXTREAL2:79

for b₁, b₂ being R_eal st not b₁ <=' b₂ holds
min b₂,b₁ = b₂ by Def1;

theorem Th80: :: EXTREAL2:80

for b₁, b₂ being R_eal st b₁ <> +infty & b₂ <> +infty & not ( b₁ = +infty & b₂ = +infty ) & not ( b₁ = -infty & b₂ = -infty ) holds
min b₁,b₂ = ((b₁ + b₂) - |.(b₁ - b₂).|) / (R_EAL 2)

proof end;

theorem Th81: :: EXTREAL2:81

for b₁, b₂ being R_eal holds
( min b₁,b₂ <=' b₁ & min b₂,b₁ <=' b₁ )

proof end;

theorem Th82: :: EXTREAL2:82

canceled;

theorem Th83: :: EXTREAL2:83

for b₁, b₂ being R_eal holds min b₁,b₂ = min b₂,b₁ ;

theorem Th84: :: EXTREAL2:84

for b₁, b₂ being R_eal holds
( min b₁,b₂ = b₁ or min b₁,b₂ = b₂ )

proof end;

theorem Th85: :: EXTREAL2:85

for b₁, b₂, b₃ being R_eal holds
( ( b₁ <=' b₂ & b₁ <=' b₃ ) iff b₁ <=' min b₂,b₃ )

proof end;

theorem Th86: :: EXTREAL2:86

canceled;

theorem Th87: :: EXTREAL2:87

for b₁, b₂ being R_eal st min b₁,b₂ = b₂ holds
b₂ <=' b₁ by Def1;

theorem Th88: :: EXTREAL2:88

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

proof end;

theorem Th89: :: EXTREAL2:89

for b₁, b₂ being R_eal st b₁ <=' b₂ holds
max b₁,b₂ = b₂

proof end;

theorem Th90: :: EXTREAL2:90

for b₁, b₂ being R_eal st not b₁ <=' b₂ holds
max b₁,b₂ = b₁ by Def2;

theorem Th91: :: EXTREAL2:91

for b₁, b₂ being R_eal st b₁ <> -infty & b₂ <> -infty & not ( b₁ = +infty & b₂ = +infty ) & not ( b₁ = -infty & b₂ = -infty ) holds
max b₁,b₂ = ((b₁ + b₂) + |.(b₁ - b₂).|) / (R_EAL 2)

proof end;

theorem Th92: :: EXTREAL2:92

for b₁, b₂ being R_eal holds
( b₁ <=' max b₁,b₂ & b₁ <=' max b₂,b₁ )

proof end;

theorem Th93: :: EXTREAL2:93

canceled;

theorem Th94: :: EXTREAL2:94

for b₁, b₂ being R_eal holds max b₁,b₂ = max b₂,b₁ ;

theorem Th95: :: EXTREAL2:95

for b₁, b₂ being R_eal holds
( max b₁,b₂ = b₁ or max b₁,b₂ = b₂ )

proof end;

theorem Th96: :: EXTREAL2:96

for b₁, b₂, b₃ being R_eal holds
( ( b₁ <=' b₂ & b₃ <=' b₂ ) iff max b₁,b₃ <=' b₂ )

proof end;

theorem Th97: :: EXTREAL2:97

canceled;

theorem Th98: :: EXTREAL2:98

for b₁, b₂ being R_eal st max b₁,b₂ = b₂ holds
b₁ <=' b₂ by Def2;

theorem Th99: :: EXTREAL2:99

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

proof end;

theorem Th100: :: EXTREAL2:100

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

proof end;

theorem Th101: :: EXTREAL2:101

for b₁, b₂ being R_eal holds
( max b₁,(min b₁,b₂) = b₁ & max (min b₁,b₂),b₁ = b₁ & max (min b₂,b₁),b₁ = b₁ & max b₁,(min b₂,b₁) = b₁ )

proof end;

theorem Th102: :: EXTREAL2:102

for b₁, b₂ being R_eal holds
( min b₁,(max b₁,b₂) = b₁ & min (max b₁,b₂),b₁ = b₁ & min (max b₂,b₁),b₁ = b₁ & min b₁,(max b₂,b₁) = b₁ )

proof end;

theorem Th103: :: EXTREAL2:103

for b₁, b₂, b₃ being R_eal holds
( min b₁,(max b₂,b₃) = max (min b₁,b₂),(min b₁,b₃) & min (max b₂,b₃),b₁ = max (min b₂,b₁),(min b₃,b₁) )

proof end;

theorem Th104: :: EXTREAL2:104

for b₁, b₂, b₃ being R_eal holds
( max b₁,(min b₂,b₃) = min (max b₁,b₂),(max b₁,b₃) & max (min b₂,b₃),b₁ = min (max b₂,b₁),(max b₃,b₁) )

proof end;