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


begin

definition
let x, y be R_eal;
:: original:*
redefine funcx * y ->  R_eal;
coherence
 x * y is R_eal by XXREAL_0:def_1;
end;

theorem Th1: :: EXTREAL1:1
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 funcx / y ->  R_eal;
coherence
 x / y is R_eal by XXREAL_0:def_1;
end;

theorem Th2: :: EXTREAL1:2
for x, y being R_eal
for a, b being Real st x = a & y = b holds
x / y = a / b
proofend;

definition
let x be R_eal;
func|.x.| ->  R_eal equals :Def1: :: EXTREAL1:def 1
x if  0 <= x
otherwise  - x;
coherence
 ( ( 0 <= x implies x is R_eal ) &amp; ( not 0 <= x implies - x is R_eal ) ) ;
consistency
 for b1 being R_eal holds verum ;
projectivity
 for b1, b2 being R_eal st ( 0 <= b2 implies b1 = b2 ) &amp; ( not 0 <= b2 implies b1 = - b2 ) holds
( ( 0 <= b1 implies b1 = b1 ) &amp; ( not 0 <= b1 implies b1 = - b1 ) ) ;
end;

:: deftheorem Def1 defines |. EXTREAL1:def_1_:_
 for x being R_eal holds
( ( 0 <= x implies |.x.| = x ) &amp; ( not 0 <= x implies |.x.| = - x ) );

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
proofend;
end;

theorem :: EXTREAL1:5
for a, b being Real holds a * b = (R_EAL a) * (R_EAL b)
proofend;

theorem :: EXTREAL1:6
for a, b being Real holds a / b = (R_EAL a) / (R_EAL b)
proofend;

begin

:: 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 Function of NAT,ExtREAL st
( it = f . (len F) &amp; f . 0 = 0. &amp; ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) );
existence
 ex b1 being R_eal ex f being Function of NAT,ExtREAL st
( b1 = f . (len F) &amp; f . 0 = 0. &amp; ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) )
proofend;
uniqueness
 for b1, b2 being R_eal st ex f being Function of NAT,ExtREAL st
( b1 = f . (len F) &amp; f . 0 = 0. &amp; ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) &amp; ex f being Function of NAT,ExtREAL st
( b2 = f . (len F) &amp; f . 0 = 0. &amp; ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Sum EXTREAL1:def_2_:_
 for F being FinSequence of ExtREAL
for b2 being R_eal holds
( b2 = Sum F iff ex f being Function of NAT,ExtREAL st
( b2 = f . (len F) &amp; f . 0 = 0. &amp; ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) );

theorem Th7: :: EXTREAL1:7
Sum (<*> ExtREAL) = 0.
proofend;

theorem Th8: :: EXTREAL1:8
for a being R_eal holds Sum <*a*> = a
proofend;

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

theorem :: EXTREAL1:9
for a, b being R_eal holds Sum <*a,b*> = a + b
proofend;

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

theorem Th10: :: EXTREAL1:10
for F, G being FinSequence of ExtREAL st not -infty in rng F &amp; not -infty in rng G holds
Sum (F ^ G) = (Sum F) + (Sum G)
proofend;

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 ) &amp; ( i = q implies p . i = n + 1 ) &amp; ( i > q implies p . i = i - 1 ) )
proofend;

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 &amp; q = s . (n + 1) &amp; ( for i being Element of NAT st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) &amp; ( i = q implies p . i = n + 1 ) &amp; ( i > q implies p . i = i - 1 ) ) ) holds
p * (s9 | n) is Permutation of (Seg n)
proofend;

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 &amp; q in Seg (n + 1) &amp; len H = n + 1 &amp; not -infty in rng H &amp; ( for i being Element of NAT st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) &amp; ( i = q implies p . i = n + 1 ) &amp; ( i > q implies p . i = i - 1 ) ) ) holds
Sum F = Sum H
proofend;

theorem :: EXTREAL1:11
for F, G being FinSequence of ExtREAL
for s being Permutation of (dom F) st G = F * s &amp; not -infty in rng F holds
Sum F = Sum G
proofend;