:: EXTREAL2 semantic presentation

Show IDV graph for whole article

theorem :: EXTREAL2:1

Show IDV graph

canceled;

theorem :: EXTREAL2:2

Show IDV graph

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

proof end;

theorem :: EXTREAL2:3

Show IDV graph

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

proof end;

theorem Th4: :: EXTREAL2:4

Show IDV graph

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

proof end;

theorem :: EXTREAL2:5

Show IDV graph

for x being R_eal holds 0. - x = - x

proof end;

theorem :: EXTREAL2:6

Show IDV graph

canceled;

theorem Th7: :: EXTREAL2:7

Show IDV graph

for x, y being R_eal st 0. <=' x & 0. <=' y holds
0. <=' x + y

proof end;

theorem :: EXTREAL2:8

Show IDV graph

canceled;

theorem Th9: :: EXTREAL2:9

Show IDV graph

for x, y being R_eal st x <=' 0. & y <=' 0. holds
x + y <=' 0.

proof end;

theorem :: EXTREAL2:10

Show IDV graph

canceled;

theorem :: EXTREAL2:11

Show IDV graph

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

proof end;

theorem :: EXTREAL2:12

Show IDV graph

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

proof end;

theorem :: EXTREAL2:13

Show IDV graph

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

proof end;

theorem Th14: :: EXTREAL2:14

Show IDV graph

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

proof end;

theorem Th15: :: EXTREAL2:15

Show IDV graph

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

proof end;

theorem :: EXTREAL2:16

Show IDV graph

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

proof end;

theorem Th17: :: EXTREAL2:17

Show IDV graph

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

proof end;

theorem Th18: :: EXTREAL2:18

Show IDV graph

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

proof end;

theorem Th19: :: EXTREAL2:19

Show IDV graph

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

proof end;

theorem Th20: :: EXTREAL2:20

Show IDV graph

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

theorem :: EXTREAL2:21

Show IDV graph

for x being R_eal st ( x = +infty or x = -infty ) holds
for y being R_eal st y in REAL holds
x + y <> 0.

proof end;

theorem :: EXTREAL2:22

Show IDV graph

for x being R_eal st ( x = +infty or x = -infty ) holds
for y being R_eal holds x * y <> 1.

proof end;

theorem Th23: :: EXTREAL2:23

Show IDV graph

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

proof end;

theorem Th24: :: EXTREAL2:24

Show IDV graph

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

proof end;

theorem Th25: :: EXTREAL2:25

Show IDV graph

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

proof end;

theorem Th26: :: EXTREAL2:26

Show IDV graph

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

proof end;

theorem :: EXTREAL2:27

Show IDV graph

for x, y, z being R_eal 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 :: EXTREAL2:28

Show IDV graph

for z, y, x being R_eal 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 :: EXTREAL2:29

Show IDV graph

for x, y, z being R_eal 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 :: EXTREAL2:30

Show IDV graph

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

Show IDV graph

for x, y, z being R_eal 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 :: EXTREAL2:32

Show IDV graph

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 ) & x <=' z - y holds
( y <> +infty & x + y <=' z )

proof end;

theorem :: EXTREAL2:33

Show IDV graph

for x, y, z being R_eal 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 Th34: :: EXTREAL2:34

Show IDV graph

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 ) & x <=' z + y holds
( y <> -infty & x - y <=' z )

proof end;

theorem :: EXTREAL2:35

Show IDV graph

canceled;

theorem :: EXTREAL2:36

Show IDV graph

canceled;

theorem :: EXTREAL2:37

Show IDV graph

canceled;

theorem :: EXTREAL2:38

Show IDV graph

canceled;

theorem :: EXTREAL2:39

Show IDV graph

canceled;

theorem :: EXTREAL2:40

Show IDV graph

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;

theorem :: EXTREAL2:41

Show IDV graph

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;

theorem :: EXTREAL2:42

Show IDV graph

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

proof end;

theorem Th43: :: EXTREAL2:43

Show IDV graph

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

proof end;

theorem Th44: :: EXTREAL2:44

Show IDV graph

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

proof end;

theorem :: EXTREAL2:45

Show IDV graph

for x, y being R_eal holds
( ( ( ( 0. <=' x or 0. <' x ) & ( 0. <=' y or 0. <' y ) ) or ( ( x <=' 0. or x <' 0. ) & ( y <=' 0. or y <' 0. ) ) ) iff 0. <=' x * y ) by Th44;

theorem :: EXTREAL2:46

Show IDV graph

for x, y being R_eal holds
( ( ( ( x <=' 0. or x <' 0. ) & ( 0. <=' y or 0. <' y ) ) or ( ( 0. <=' x or 0. <' x ) & ( y <=' 0. or y <' 0. ) ) ) iff x * y <=' 0. ) by Th43;

theorem Th47: :: EXTREAL2:47

Show IDV graph

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

proof end;

theorem Th48: :: EXTREAL2:48

Show IDV graph

for x, y being R_eal holds
( ( x <' - y implies y <' - x ) & ( y <' - x implies x <' - y ) & ( - x <' y implies - y <' x ) & ( - y <' x implies - x <' y ) )

proof end;

theorem Th49: :: EXTREAL2:49

Show IDV graph

for x being R_eal
for a being Real st x = a holds
|.x.| = abs a

proof end;

theorem Th50: :: EXTREAL2:50

Show IDV graph

for x being R_eal holds
( |.x.| = x or |.x.| = - x )

proof end;

theorem Th51: :: EXTREAL2:51

Show IDV graph

for x being R_eal holds 0. <=' |.x.|

proof end;

theorem Th52: :: EXTREAL2:52

Show IDV graph

for x being R_eal st x <> 0. holds
0. <' |.x.|

proof end;

theorem :: EXTREAL2:53

Show IDV graph

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

theorem :: EXTREAL2:54

Show IDV graph

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

proof end;

theorem Th55: :: EXTREAL2:55

Show IDV graph

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

proof end;

theorem :: EXTREAL2:56

Show IDV graph

for x, y being R_eal holds |.(x * y).| = |.x.| * |.y.|

proof end;

theorem Th57: :: EXTREAL2:57

Show IDV graph

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

proof end;

theorem Th58: :: EXTREAL2:58

Show IDV graph

for x, y being R_eal st |.x.| <' y holds
( - y <' x & x <' y )

proof end;

theorem Th59: :: EXTREAL2:59

Show IDV graph

for y, x being R_eal st - y <' x & x <' y holds
( 0. <' y & |.x.| <' y )

proof end;

theorem Th60: :: EXTREAL2:60

Show IDV graph

for y, x being R_eal holds
( ( - y <=' x & x <=' y ) iff |.x.| <=' y )

proof end;

theorem Th61: :: EXTREAL2:61

Show IDV graph

for x, y being R_eal holds
( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or |.(x + y).| <=' |.x.| + |.y.| )

proof end;

theorem Th62: :: EXTREAL2:62

Show IDV graph

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

proof end;

theorem :: EXTREAL2:63

Show IDV graph

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

proof end;

theorem :: EXTREAL2:64

Show IDV graph

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

proof end;

theorem :: EXTREAL2:65

Show IDV graph

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

proof end;

theorem Th66: :: EXTREAL2:66

Show IDV graph

for x being R_eal holds |.x.| = |.(- x).|

proof end;

theorem Th67: :: EXTREAL2:67

Show IDV graph

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

proof end;

theorem Th68: :: EXTREAL2:68

Show IDV graph

for x, y being R_eal st ( x is Real or y is Real ) holds
|.x.| - |.y.| <=' |.(x - y).|

proof end;

theorem :: EXTREAL2:69

Show IDV graph

for x, y being R_eal holds
( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or |.(x - y).| <=' |.x.| + |.y.| )

proof end;

theorem :: EXTREAL2:70

Show IDV graph

for x being R_eal holds |.|.x.|.| = |.x.|

proof end;

theorem :: EXTREAL2:71

Show IDV graph

for x, y, z, w being R_eal holds
( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not |.x.| <=' z or not |.y.| <=' w or |.(x + y).| <=' z + w )

proof end;

theorem :: EXTREAL2:72

Show IDV graph

for x, y being R_eal st ( x is Real or y is Real ) holds
|.(|.x.| - |.y.|).| <=' |.(x - y).|

proof end;

theorem :: EXTREAL2:73

Show IDV graph

for x, y being R_eal st 0. <=' x * y holds
|.(x + y).| = |.x.| + |.y.|

proof end;

theorem Th74: :: EXTREAL2:74

Show IDV graph

for x, y being R_eal
for a, b being Real st x = a & y = b holds
( ( b < a implies y <' x ) & ( y <' x implies b < a ) & ( b <= a implies y <=' x ) & ( y <=' x implies b <= a ) )

proof end;

definition

let x, y be R_eal;
func min x,y -> R_eal equals :Def1: :: EXTREAL2:def 1
x if x <=' y
otherwise y;
correctness ;
commutativity

proof end;

idempotence ;
func max x,y -> R_eal equals :Def2: :: EXTREAL2:def 2
x if y <=' x
otherwise y;
correctness ;
commutativity

proof end;

idempotence ;

end;

:: deftheorem Def1 defines min EXTREAL2:def 1 :

:: deftheorem Def2 defines max EXTREAL2:def 2 :

theorem Th75: :: EXTREAL2:75

Show IDV graph

for x, y being R_eal st ( x = -infty or y = -infty ) holds
min x,y = -infty

proof end;

theorem Th76: :: EXTREAL2:76

Show IDV graph

for x, y being R_eal st ( x = +infty or y = +infty ) holds
max x,y = +infty

proof end;

theorem Th77: :: EXTREAL2:77

Show IDV graph

for x, y being R_eal
for a, b being Real st x = a & y = b holds
( min x,y = min a,b & max x,y = max a,b )

proof end;

theorem Th78: :: EXTREAL2:78

Show IDV graph

for y, x being R_eal st y <=' x holds
min x,y = y

proof end;

theorem :: EXTREAL2:79

Show IDV graph

for y, x being R_eal st not y <=' x holds
min x,y = x by Def1;

theorem :: EXTREAL2:80

Show IDV graph

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

proof end;

theorem Th81: :: EXTREAL2:81

Show IDV graph

for x, y being R_eal holds
( min x,y <=' x & min y,x <=' x )

proof end;

theorem :: EXTREAL2:82

Show IDV graph

canceled;

theorem :: EXTREAL2:83

Show IDV graph

for x, y being R_eal holds min x,y = min y,x ;

theorem Th84: :: EXTREAL2:84

Show IDV graph

for x, y being R_eal holds
( min x,y = x or min x,y = y )

proof end;

theorem Th85: :: EXTREAL2:85

Show IDV graph

for x, y, z being R_eal holds
( ( x <=' y & x <=' z ) iff x <=' min y,z )

proof end;

theorem :: EXTREAL2:86

Show IDV graph

canceled;

theorem :: EXTREAL2:87

Show IDV graph

for x, y being R_eal st min x,y = y holds
y <=' x by Def1;

theorem :: EXTREAL2:88

Show IDV graph

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

proof end;

theorem Th89: :: EXTREAL2:89

Show IDV graph

for x, y being R_eal st x <=' y holds
max x,y = y

proof end;

theorem :: EXTREAL2:90

Show IDV graph

for x, y being R_eal st not x <=' y holds
max x,y = x by Def2;

theorem :: EXTREAL2:91

Show IDV graph

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

proof end;

theorem Th92: :: EXTREAL2:92

Show IDV graph

for x, y being R_eal holds
( x <=' max x,y & x <=' max y,x )

proof end;

theorem :: EXTREAL2:93

Show IDV graph

canceled;

theorem :: EXTREAL2:94

Show IDV graph

for x, y being R_eal holds max x,y = max y,x ;

theorem Th95: :: EXTREAL2:95

Show IDV graph

for x, y being R_eal holds
( max x,y = x or max x,y = y )

proof end;

theorem Th96: :: EXTREAL2:96

Show IDV graph

for y, x, z being R_eal holds
( ( y <=' x & z <=' x ) iff max y,z <=' x )

proof end;

theorem :: EXTREAL2:97

Show IDV graph

canceled;

theorem :: EXTREAL2:98

Show IDV graph

for x, y being R_eal st max x,y = y holds
x <=' y by Def2;

theorem :: EXTREAL2:99

Show IDV graph

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

proof end;

theorem :: EXTREAL2:100

Show IDV graph

for x, y being R_eal holds (min x,y) + (max x,y) = x + y

proof end;

theorem Th101: :: EXTREAL2:101

Show IDV graph

for x, y being R_eal holds
( max x,(min x,y) = x & max (min x,y),x = x & max (min y,x),x = x & max x,(min y,x) = x )

proof end;

theorem Th102: :: EXTREAL2:102

Show IDV graph

for x, y being R_eal holds
( min x,(max x,y) = x & min (max x,y),x = x & min (max y,x),x = x & min x,(max y,x) = x )

proof end;

theorem :: EXTREAL2:103

Show IDV graph

for x, y, z being R_eal holds
( min x,(max y,z) = max (min x,y),(min x,z) & min (max y,z),x = max (min y,x),(min z,x) )

proof end;

theorem :: EXTREAL2:104

Show IDV graph

for x, y, z being R_eal holds
( max x,(min y,z) = min (max x,y),(max x,z) & max (min y,z),x = min (max y,x),(max z,x) )

proof end;