:: Some Properties of Extended Real Numbers Operations: absolutevalue, min and max
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received September 15, 2000
:: Copyright (c) 2000 Association of Mizar Users

theorem :: EXTREAL2:1

canceled;

theorem :: EXTREAL2:2

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

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

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

proof end;

theorem :: EXTREAL2:5

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

proof end;

theorem :: EXTREAL2:6

canceled;

theorem Th7: :: EXTREAL2:7

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

proof end;

theorem :: EXTREAL2:8

canceled;

theorem Th9: :: EXTREAL2:9

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

proof end;

theorem :: EXTREAL2:10

canceled;

theorem :: EXTREAL2:11

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

proof end;

theorem :: EXTREAL2:12

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

proof end;

Lm1: +infty + -infty = 0.
by SUPINF_2:def 2, XXREAL_0:8;

0. = 0
;

then Lm2: ex a being Real st
( 0. = a & - 0. = - a )
by SUPINF_2:def 3;

Lm3: - +infty = -infty
by SUPINF_2:def 3;

theorem :: EXTREAL2:13

for x being R_eal holds x - x = 0

proof end;

Lm4: - (+infty + -infty ) = +infty - +infty by Lm1, Lm2, SUPINF_2:def 3
.= (- -infty ) - +infty by SUPINF_2:def 3, XXREAL_0:11 ;

Lm5: for x being R_eal st x in REAL holds
- (x + +infty ) = (- +infty ) + (- x)

proof end;

Lm6: for x being R_eal st x in REAL holds
- (x + -infty ) = (- -infty ) + (- x)

proof end;

theorem Th14: :: EXTREAL2:14

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

proof end;

theorem Th15: :: EXTREAL2:15

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

proof end;

theorem :: EXTREAL2:16

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

proof end;

theorem Th17: :: EXTREAL2:17

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

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

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 :: EXTREAL2:20

( 1. < +infty & -infty < 1. ) by MESFUNC1:def 8, XXREAL_0:9;

theorem :: EXTREAL2:21

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

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

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

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

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

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

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

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

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

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

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

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

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 )

proof end;

theorem :: EXTREAL2:34

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

proof end;

theorem :: EXTREAL2:35

canceled;

theorem :: EXTREAL2:36

canceled;

theorem :: EXTREAL2:37

canceled;

theorem :: EXTREAL2:38

canceled;

theorem :: EXTREAL2:39

canceled;

theorem :: EXTREAL2:40

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

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

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

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

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

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

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

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

proof end;

theorem :: EXTREAL2:48

canceled;

theorem Th49: :: EXTREAL2:49

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

proof end;

theorem :: EXTREAL2:50

for x being R_eal holds
( |.x.| = x or |.x.| = - x ) by EXTREAL1:def 3;

theorem Th51: :: EXTREAL2:51

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

proof end;

theorem Th52: :: EXTREAL2:52

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

proof end;

theorem :: EXTREAL2:53

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

theorem :: EXTREAL2:54

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

proof end;

theorem Th55: :: EXTREAL2:55

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

proof end;

theorem :: EXTREAL2:56

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

proof end;

theorem Th57: :: EXTREAL2:57

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

proof end;

theorem Th58: :: EXTREAL2:58

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

proof end;

theorem Th59: :: EXTREAL2:59

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

proof end;

theorem Th60: :: EXTREAL2:60

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

proof end;

theorem Th61: :: EXTREAL2:61

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

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

proof end;

theorem :: EXTREAL2:63

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

proof end;

theorem :: EXTREAL2:64

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

proof end;

theorem :: EXTREAL2:65

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

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

proof end;

theorem Th67: :: EXTREAL2:67

( |.+infty .| = +infty & |.-infty .| = +infty )

proof end;

theorem Th68: :: EXTREAL2:68

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

proof end;

theorem :: EXTREAL2:69

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

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

proof end;

theorem :: EXTREAL2:71

for x, z, y, w being R_eal st |.x.| <= z & |.y.| <= w holds
|.(x + y).| <= z + w

proof end;

theorem :: EXTREAL2:72

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

proof end;

theorem :: EXTREAL2:73

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

proof end;

theorem :: EXTREAL2:74

canceled;

theorem :: EXTREAL2:75

canceled;

theorem :: EXTREAL2:76

canceled;

theorem :: EXTREAL2:77

canceled;

theorem :: EXTREAL2:78

canceled;

theorem :: EXTREAL2:79

canceled;

theorem :: EXTREAL2:80

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 :: EXTREAL2:81

canceled;

theorem :: EXTREAL2:82

canceled;

theorem :: EXTREAL2:83

canceled;

theorem :: EXTREAL2:84

canceled;

theorem :: EXTREAL2:85

canceled;

theorem :: EXTREAL2:86

canceled;

theorem :: EXTREAL2:87

canceled;

theorem :: EXTREAL2:88

canceled;

theorem :: EXTREAL2:89

canceled;

theorem :: EXTREAL2:90

canceled;

theorem :: EXTREAL2:91

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;

definition

let x, y be R_eal;
:: original: max
redefine func max x,y -> R_eal;
coherence
max x,y is R_eal by XXREAL_0:def 1;
:: original: min
redefine func min x,y -> R_eal;
coherence
min x,y is R_eal by XXREAL_0:def 1;

end;

theorem :: EXTREAL2:92

canceled;

theorem :: EXTREAL2:93

canceled;

theorem :: EXTREAL2:94

canceled;

theorem :: EXTREAL2:95

canceled;

theorem :: EXTREAL2:96

canceled;

theorem :: EXTREAL2:97

canceled;

theorem :: EXTREAL2:98

canceled;

theorem :: EXTREAL2:99

canceled;

theorem :: EXTREAL2:100

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

proof end;

theorem Th101: :: EXTREAL2:101

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

proof end;

theorem :: EXTREAL2:102

for x being R_eal holds
( |.x.| < +infty iff x in REAL )

proof end;