EXTREAL2: Some Properties of Extended Real Numbers Operations: absolute value, min and max

:: 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-2012 Association of Mizar Users

begin

begin

theorem Th1: :: EXTREAL2:1

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

proof end;

theorem :: EXTREAL2:2

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

theorem :: EXTREAL2:3

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

theorem Th4: :: EXTREAL2:4

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

proof end;

theorem :: EXTREAL2:5

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

theorem :: EXTREAL2:6

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

theorem Th7: :: EXTREAL2:7

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

proof end;

theorem :: EXTREAL2:8

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

proof end;

theorem Th9: :: EXTREAL2:9

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

proof end;

theorem Th10: :: EXTREAL2:10

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

proof end;

theorem Th11: :: EXTREAL2:11

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

proof end;

theorem Th12: :: EXTREAL2:12

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

proof end;

theorem Th13: :: EXTREAL2:13

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

proof end;

theorem Th14: :: EXTREAL2:14

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

proof end;

theorem :: EXTREAL2:15

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

proof end;

theorem :: EXTREAL2:16

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

proof end;

theorem :: EXTREAL2:17

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 Th18: :: EXTREAL2:18

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

proof end;

theorem Th19: :: EXTREAL2:19

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

proof end;

theorem Th20: :: EXTREAL2:20

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

proof end;

theorem :: EXTREAL2:21

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

proof end;

theorem :: EXTREAL2:22

canceled;

theorem :: EXTREAL2:23

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

proof end;

theorem :: EXTREAL2:24

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

proof end;

theorem :: EXTREAL2:25

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

proof end;

begin

theorem :: EXTREAL2:26

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:27

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 by XXREAL_0:def 1;
:: original: min
redefine func min (x,y) -> R_eal;
coherence by XXREAL_0:def 1;

end;

theorem :: EXTREAL2:28

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

proof end;

begin

:: missing, 2007.07.20, A.T.

theorem Th29: :: EXTREAL2:29

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

proof end;

theorem :: EXTREAL2:30

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

proof end;