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

begin

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

canceled;

theorem :: EXTREAL1:2

canceled;

theorem :: EXTREAL1:3

canceled;

theorem :: EXTREAL1:4

canceled;

theorem :: EXTREAL1:5

canceled;

theorem :: EXTREAL1:6

canceled;

theorem :: EXTREAL1:7

canceled;

theorem :: EXTREAL1:8

canceled;

theorem :: EXTREAL1:9

canceled;

theorem :: EXTREAL1:10

canceled;

theorem :: EXTREAL1:11

canceled;

theorem :: EXTREAL1:12

canceled;

theorem Th13: :: EXTREAL1:13

for x, y being R_eal
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 R_eal;
:: original: /
redefine func x / y -> R_eal;
coherence
x / y is R_eal by XXREAL_0:def 1;

end;

theorem :: EXTREAL1:14

canceled;

theorem :: EXTREAL1:15

canceled;

theorem :: EXTREAL1:16

canceled;

theorem :: EXTREAL1:17

canceled;

theorem :: EXTREAL1:18

canceled;

theorem :: EXTREAL1:19

canceled;

theorem :: EXTREAL1:20

canceled;

theorem :: EXTREAL1:21

canceled;

theorem :: EXTREAL1:22

canceled;

theorem :: EXTREAL1:23

canceled;

theorem :: EXTREAL1:24

canceled;

theorem :: EXTREAL1:25

canceled;

theorem :: EXTREAL1:26

canceled;

theorem :: EXTREAL1:27

canceled;

theorem :: EXTREAL1:28

canceled;

theorem :: EXTREAL1:29

canceled;

theorem :: EXTREAL1:30

canceled;

theorem :: EXTREAL1:31

canceled;

theorem Th32: :: EXTREAL1:32

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

proof end;

definition

canceled;
canceled;
let x be R_eal;
func |.x.| -> R_eal equals :Def3: :: EXTREAL1:def 3
x if 0 <= x
otherwise - x;
coherence
( ( 0 <= x implies x is R_eal ) & ( not 0 <= x implies - x is R_eal ) ) ;
consistency
for b₁ being R_eal holds verum ;

end;

:: deftheorem EXTREAL1:def 1 :
canceled;

:: deftheorem EXTREAL1:def 2 :
canceled;

:: deftheorem Def3 defines |. EXTREAL1:def 3 :
for x being R_eal holds
( ( 0 <= x implies |.x.| = x ) & ( not 0 <= x implies |.x.| = - x ) );

theorem :: EXTREAL1:33

canceled;

theorem :: EXTREAL1:34

canceled;

theorem :: EXTREAL1:35

canceled;

theorem :: EXTREAL1:36

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

theorem :: EXTREAL1:37

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

theorem :: EXTREAL1:38

for a, b being Real holds a * b = (R_EAL a) * (R_EAL b)

proof end;

theorem :: EXTREAL1:39

for a, b being Real holds a / b = (R_EAL a) / (R_EAL b)

proof end;

begin

definition

let F be FinSequence of ExtREAL ;
func Sum F -> R_eal means :Def4: :: EXTREAL1:def 4
ex f being Function of NAT,ExtREAL st
( it = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) );
existence
ex b₁ being R_eal ex f being Function of NAT,ExtREAL st
( b₁ = f . (len F) & f . 0 = 0. & ( for i being Element of 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 Function of NAT,ExtREAL st
( b₁ = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) & ex f being Function of NAT,ExtREAL st
( b₂ = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Sum EXTREAL1:def 4 :
for F being FinSequence of ExtREAL
for b₂ being R_eal holds
( b₂ = Sum F iff ex f being Function of NAT,ExtREAL st
( b₂ = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) );

theorem Th40: :: EXTREAL1:40

Sum (<*> ExtREAL) = 0.

proof end;

theorem Th41: :: EXTREAL1:41

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

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 Th43: :: EXTREAL1:43

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

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;