:: Basic Properties of Extended Real Numbers
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received September 7, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users

definition

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

end;

theorem :: EXTREAL1:1

for x, y being ExtReal
for a, b being Real st x = a & y = b holds
x * y = a * b by XXREAL_3:def 5;

definition

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

end;

theorem :: EXTREAL1:2

for x, y being ExtReal
for a, b being Real st x = a & y = b holds
x / y = a / b ;

definition

let x be ExtReal;

func |.x.| -> R_eal equals :Def1: :: EXTREAL1:def 1
x if 0 <= x
otherwise - x;

coherence
( ( 0 <= x implies x is R_eal ) & ( not 0 <= x implies - x is R_eal ) ) by XXREAL_0:def 1;
consistency
for b₁ being R_eal holds verum ;
projectivity
for b₁ being R_eal
for b₂ being ExtReal st ( 0 <= b₂ implies b₁ = b₂ ) & ( not 0 <= b₂ implies b₁ = - b₂ ) holds
( ( 0 <= b₁ implies b₁ = b₁ ) & ( not 0 <= b₁ implies b₁ = - b₁ ) ) ;

end;

:: deftheorem Def1 defines |. EXTREAL1:def 1 :
for x being ExtReal holds
( ( 0 <= x implies |.x.| = x ) & ( not 0 <= x implies |.x.| = - x ) );

registration

let x be Real;
let a be Complex;

identify |.x.| with |.a.| when x = a;

compatibility
( x = a implies |.x.| = |.a.| )

proof end;

end;

theorem :: EXTREAL1:3

for x being R_eal st 0 <= x holds
|.x.| = x by Def1;

theorem :: EXTREAL1:4

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

registration

let x be R_eal;

cluster |.x.| -> non negative ;

coherence
not |.x.| is negative

proof end;

end;

theorem :: EXTREAL1:5

canceled;

theorem :: EXTREAL1:6

canceled;

:: from CONVFUN1, 2010.02.13, A.T.

definition

let F be FinSequence of ExtREAL ;

func Sum F -> R_eal means :Def2: :: EXTREAL1:def 2
ex f being sequence of ExtREAL st
( it = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) );

existence
ex b₁ being R_eal ex f being sequence of ExtREAL st
( b₁ = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being R_eal st ex f being sequence of ExtREAL st
( b₁ = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) & ex f being sequence of ExtREAL st
( b₂ = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Sum EXTREAL1:def 2 :
for F being FinSequence of ExtREAL
for b₂ being R_eal holds
( b₂ = Sum F iff ex f being sequence of ExtREAL st
( b₂ = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) );

theorem Th5: :: EXTREAL1:7

Sum (<*> ExtREAL) = 0.

proof end;

theorem Th6: :: EXTREAL1:8

for a being R_eal holds Sum <*a*> = a

proof end;

Lm1: for F being FinSequence of ExtREAL
for x being Element of ExtREAL holds Sum (F ^ <*x*>) = (Sum F) + x

proof end;

theorem :: EXTREAL1:9

for a, b being R_eal holds Sum <*a,b*> = a + b

proof end;

Lm2: for F being FinSequence of ExtREAL st not -infty in rng F holds
Sum F <> -infty

proof end;

theorem Th8: :: EXTREAL1:10

for F, G being FinSequence of ExtREAL st not -infty in rng F & not -infty in rng G holds
Sum (F ^ G) = (Sum F) + (Sum G)

proof end;

Lm3: for n, q being Nat st q in Seg (n + 1) holds
ex p being Permutation of (Seg (n + 1)) st
for i being Element of NAT st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )

proof end;

Lm4: for n, q being Nat
for s, p being Permutation of (Seg (n + 1))
for s9 being FinSequence of Seg (n + 1) st s9 = s & q = s . (n + 1) & ( for i being Element of NAT st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ) holds
p * (s9 | n) is Permutation of (Seg n)

proof end;

Lm5: for n, q being Nat
for p being Permutation of (Seg (n + 1))
for F, H being FinSequence of ExtREAL st F = H * p & q in Seg (n + 1) & len H = n + 1 & not -infty in rng H & ( for i being Element of NAT st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ) holds
Sum F = Sum H

proof end;

theorem :: EXTREAL1:11

for F, G being FinSequence of ExtREAL
for s being Permutation of (dom F) st G = F * s & not -infty in rng F holds
Sum F = Sum G

proof end;

theorem Th1: :: EXTREAL1:12

for x being ExtReal
for a being Real st x = a holds
|.x.| = |.a.|

proof end;

theorem :: EXTREAL1:13

for x being ExtReal holds
( |.x.| = x or |.x.| = - x ) by Def1;

theorem :: EXTREAL1:14

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

proof end;

theorem Th4: :: EXTREAL1:15

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

proof end;

theorem :: EXTREAL1:16

for x being ExtReal holds
( x = 0 iff |.x.| = 0 ) by Th4, Def1;

theorem :: EXTREAL1:17

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

proof end;

theorem Th7: :: EXTREAL1:18

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

proof end;

theorem :: EXTREAL1:19

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

proof end;

theorem Th9: :: EXTREAL1:20

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

proof end;

theorem Th10: :: EXTREAL1:21

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

proof end;

theorem Th11: :: EXTREAL1:22

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

proof end;

theorem Th12: :: EXTREAL1:23

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

proof end;

theorem Th13: :: EXTREAL1:24

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

proof end;

theorem Th14: :: EXTREAL1:25

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

proof end;

theorem :: EXTREAL1:26

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

proof end;

theorem :: EXTREAL1:27

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

proof end;

theorem :: EXTREAL1:28

for x, y being ExtReal 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: :: EXTREAL1:29

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

proof end;

theorem Th19: :: EXTREAL1:30

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

proof end;

theorem Th20: :: EXTREAL1:31

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

proof end;

theorem :: EXTREAL1:32

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

proof end;

theorem :: EXTREAL1:33

canceled;

::$CT

theorem :: EXTREAL1:34

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

proof end;

theorem :: EXTREAL1:35

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

proof end;

theorem :: EXTREAL1:36

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

proof end;

theorem :: EXTREAL1:37

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

proof end;

theorem :: EXTREAL1:38

for x, y being ExtReal st x <> -infty & y <> -infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) holds
max (x,y) = ((x + y) + |.(x - y).|) / 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 :: EXTREAL1:39

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

proof end;

:: missing, 2007.07.20, A.T.

theorem Th28: :: EXTREAL1:40

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

proof end;

theorem :: EXTREAL1:41

for x being ExtReal holds
( |.x.| < +infty iff x in REAL ) by Th19, Th28, XXREAL_0:4, XXREAL_0:14;