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

begin

begin

theorem :: EXTREAL2:1

canceled;

theorem :: EXTREAL2:2

canceled;

theorem :: EXTREAL2:3

canceled;

theorem :: EXTREAL2:4

canceled;

theorem :: EXTREAL2:5

canceled;

theorem :: EXTREAL2:6

canceled;

theorem :: EXTREAL2:7

canceled;

theorem :: EXTREAL2:8

canceled;

theorem :: EXTREAL2:9

canceled;

theorem :: EXTREAL2:10

canceled;

theorem :: EXTREAL2:11

canceled;

theorem :: EXTREAL2:12

canceled;

theorem :: EXTREAL2:13

canceled;

theorem :: EXTREAL2:14

canceled;

theorem :: EXTREAL2:15

canceled;

theorem :: EXTREAL2:16

canceled;

theorem :: EXTREAL2:17

canceled;

theorem :: EXTREAL2:18

canceled;

theorem :: EXTREAL2:19

canceled;

theorem :: EXTREAL2:20

canceled;

theorem :: EXTREAL2:21

canceled;

theorem :: EXTREAL2:22

canceled;

theorem :: EXTREAL2:23

canceled;

theorem :: EXTREAL2:24

canceled;

theorem :: EXTREAL2:25

canceled;

theorem :: EXTREAL2:26

canceled;

theorem :: EXTREAL2:27

canceled;

theorem :: EXTREAL2:28

canceled;

theorem :: EXTREAL2:29

canceled;

theorem :: EXTREAL2:30

canceled;

theorem :: EXTREAL2:31

canceled;

theorem :: EXTREAL2:32

canceled;

theorem :: EXTREAL2:33

canceled;

theorem :: EXTREAL2:34

canceled;

theorem :: EXTREAL2:35

canceled;

theorem :: EXTREAL2:36

canceled;

theorem :: EXTREAL2:37

canceled;

theorem :: EXTREAL2:38

canceled;

theorem :: EXTREAL2:39

canceled;

theorem :: EXTREAL2:40

canceled;

theorem :: EXTREAL2:41

canceled;

theorem :: EXTREAL2:42

canceled;

theorem :: EXTREAL2:43

canceled;

theorem :: EXTREAL2:44

canceled;

theorem :: EXTREAL2:45

canceled;

theorem :: EXTREAL2:46

canceled;

theorem :: EXTREAL2:47

canceled;

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 by EXTREAL1:def 3;

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 + 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;

begin

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;

begin

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;