defpred S1[ set , set ] means for r being real number st $1 = r holds
ex Catal being Real_Sequence st
( ( for n being Nat holds Catal . n = (Catalan (n + 1)) * (r |^ n) ) & ( abs r < 1 / 4 implies ( Catal is absolutely_summable & Sum Catal = 1 + (r * ((Sum Catal) |^ 2)) & $2 = Sum Catal ) ) );
A1: for x being set st x in REAL holds
ex y being set st
( y in REAL & S1[x,y] )
proof
let x be set ; :: thesis: ( x in REAL implies ex y being set st
( y in REAL & S1[x,y] ) )
A2: abs 1 = 1 by ABSVALUE:def 1;
assume x in REAL ; :: thesis: ex y being set st
( y in REAL & S1[x,y] )
then reconsider r = x as Real ;
set a = 4 * (abs r);
deffunc H1( Element of NAT ) -> Element of REAL = (Catalan ($1 + 1)) * (r |^ $1);
consider Cat being Real_Sequence such that
A3: for n being Element of NAT holds Cat . n = H1(n) from FUNCT_2:sch 4();
 set G = (4 * (abs r)) GeoSeq ;
defpred S2[ Nat] means (abs Cat) . $1 <= ((4 * (abs r)) GeoSeq) . $1;
A4: for n being Nat st S2[n] holds
S2[n + 1]
proof
A5: abs r >= 0 by COMPLEX1:46;
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume S2[n] ; :: thesis: S2[n + 1]
then A6: (4 * (abs r)) * ((abs Cat) . n) <= (4 * (abs r)) * (((4 * (abs r)) GeoSeq) . n) by A5, XREAL_1:64;
set n1 = n + 1;
A7: ( n in NAT & n + 1 in NAT ) by ORDINAL1:def 12;
A8: ( abs (r |^ (n + 1)) >= 0 & r |^ (n + 1) = r * (r |^ n) ) by COMPLEX1:46, NEWTON:6;
Catalan ((n + 1) + 1) >= 0 by CATALAN1:17;
then A9: abs (Catalan ((n + 1) + 1)) = Catalan ((n + 1) + 1) by ABSVALUE:def 1;
Catalan (n + 1) >= 0 by CATALAN1:17;
then abs (Catalan (n + 1)) = Catalan (n + 1) by ABSVALUE:def 1;
then abs (Catalan ((n + 1) + 1)) < 4 * (abs (Catalan (n + 1))) by A9, CATALAN1:21;
then A10: (abs (r |^ (n + 1))) * (abs (Catalan ((n + 1) + 1))) <= (4 * (abs (Catalan (n + 1)))) * (abs (r * (r |^ n))) by A8, XREAL_1:64;
abs (r * (r |^ n)) = (abs r) * (abs (r |^ n)) by COMPLEX1:65;
then abs ((r |^ (n + 1)) * (Catalan ((n + 1) + 1))) <= (4 * (abs r)) * ((abs (Catalan (n + 1))) * (abs (r |^ n))) by A10, COMPLEX1:65;
then abs (Cat . (n + 1)) <= (4 * (abs r)) * ((abs (Catalan (n + 1))) * (abs (r |^ n))) by A3;
then ( abs (Cat . (n + 1)) <= (4 * (abs r)) * (abs ((Catalan (n + 1)) * (r |^ n))) & n in NAT ) by COMPLEX1:65, ORDINAL1:def 12;
then A11: abs (Cat . (n + 1)) <= (4 * (abs r)) * (abs (Cat . n)) by A3;
abs (Cat . n) = (abs Cat) . n by A7, SEQ_1:12;
then (abs Cat) . (n + 1) <= (4 * (abs r)) * ((abs Cat) . n) by A11, SEQ_1:12;
then (abs Cat) . (n + 1) <= (4 * (abs r)) * (((4 * (abs r)) GeoSeq) . n) by A6, XXREAL_0:2;
hence S2[n + 1] by A7, PREPOWER:3; :: thesis: verum
end;
Cat . 0 = (Catalan (0 + 1)) * (r |^ 0) by A3;
then A12: (abs Cat) . 0 = abs (r |^ 0) by CATALAN1:11, SEQ_1:12;
( r |^ 0 = 1 & (4 * (abs r)) |^ 0 = 1 ) by NEWTON:4;
then A13: S2[ 0 ] by A12, A2, PREPOWER:def 1;
for n being Nat holds S2[n] from NAT_1:sch 2(A13, A4);
 then A14: for n being Element of NAT holds S2[n] ;
A15: now
let n be Element of NAT ; :: thesis: (abs Cat) . n >= 0
(abs Cat) . n = abs (Cat . n) by SEQ_1:12;
hence (abs Cat) . n >= 0 by COMPLEX1:46; :: thesis: verum
end;
take Sum Cat ; :: thesis: ( Sum Cat in REAL & S1[x, Sum Cat] )
thus Sum Cat in REAL ; :: thesis: S1[x, Sum Cat]
let s be real number ; :: thesis: ( x = s implies ex Catal being Real_Sequence st
( ( for n being Nat holds Catal . n = (Catalan (n + 1)) * (s |^ n) ) & ( abs s < 1 / 4 implies ( Catal is absolutely_summable & Sum Catal = 1 + (s * ((Sum Catal) |^ 2)) & Sum Cat = Sum Catal ) ) ) )
assume A16: x = s ; :: thesis: ex Catal being Real_Sequence st
( ( for n being Nat holds Catal . n = (Catalan (n + 1)) * (s |^ n) ) & ( abs s < 1 / 4 implies ( Catal is absolutely_summable & Sum Catal = 1 + (s * ((Sum Catal) |^ 2)) & Sum Cat = Sum Catal ) ) )
for y being set st y in NAT holds
(Cat ^\ 1) . y = (Cat (##) (r (#) Cat)) . y
proof
let y be set ; :: thesis: ( y in NAT implies (Cat ^\ 1) . y = (Cat (##) (r (#) Cat)) . y )
assume y in NAT ; :: thesis: (Cat ^\ 1) . y = (Cat (##) (r (#) Cat)) . y
then reconsider n = y as Element of NAT ;
set n1 = n + 1;
consider Fr1 being XFinSequence of such that
A17: dom Fr1 = n + 1 and
A18: for i being Nat st i in n + 1 holds
Fr1 . i = (Cat . i) * ((r (#) Cat) . (n -' i)) and
A19: Sum Fr1 = (Cat (##) (r (#) Cat)) . n by Def5;
consider Catal being XFinSequence of such that
A20: Sum Catal = Catalan ((n + 1) + 1) and
A21: dom Catal = n + 1 and
A22: for j being Nat st j < n + 1 holds
Catal . j = (Catalan (j + 1)) * (Catalan ((n + 1) -' j)) by Th43;
rng Catal c= NAT by RELAT_1:def 19;
then rng Catal c= REAL by XBOOLE_1:1;
then reconsider CatalR = Catal as XFinSequence of by RELAT_1:def 19;
defpred S3[ set , set ] means for k being Nat st k = $1 holds
$2 = (r |^ (n + 1)) * (Catal . k);
A23: for k being Nat st k in n + 1 holds
ex x being Element of REAL st S3[k,x]
proof
let k be Nat; :: thesis: ( k in n + 1 implies ex x being Element of REAL st S3[k,x] )
assume k in n + 1 ; :: thesis: ex x being Element of REAL st S3[k,x]
take (r |^ (n + 1)) * (Catal . k) ; :: thesis: S3[k,(r |^ (n + 1)) * (Catal . k)]
thus S3[k,(r |^ (n + 1)) * (Catal . k)] ; :: thesis: verum
end;
consider Fr2 being XFinSequence of such that
A24: dom Fr2 = n + 1 and
A25: for k being Nat st k in n + 1 holds
S3[k,Fr2 . k] from STIRL2_1:sch 5(A23);
A26: now
let k be Nat; :: thesis: ( k in dom Fr2 implies Fr1 . k = Fr2 . k )
assume A27: k in dom Fr2 ; :: thesis: Fr1 . k = Fr2 . k
A28: k in NAT by ORDINAL1:def 12;
A29: k < n + 1 by A24, A27, NAT_1:44;
then A30: (n + 1) -' k = (n + 1) - k by XREAL_1:233;
A31: n = k + (n - k) ;
k <= n by A29, NAT_1:13;
then A32: n -' k = n - k by XREAL_1:233;
then Fr1 . k = (Cat . k) * ((r (#) Cat) . (n - k)) by A18, A24, A27
.= ((Catalan (k + 1)) * (r |^ k)) * ((r (#) Cat) . (n - k)) by A3, A28
.= ((Catalan (k + 1)) * (r |^ k)) * (r * (Cat . (n - k))) by A32, SEQ_1:9
.= ((Catalan (k + 1)) * (r |^ k)) * (r * ((Catalan ((n -' k) + 1)) * (r |^ (n -' k)))) by A3, A32
.= (((Catalan (k + 1)) * (Catalan ((n + 1) -' k))) * r) * ((r |^ k) * (r |^ (n -' k))) by A32, A30
.= (((Catalan (k + 1)) * (Catalan ((n + 1) -' k))) * r) * (r |^ n) by A32, A31, NEWTON:8
.= ((Catal . k) * r) * (r |^ n) by A22, A29
.= (Catal . k) * (r * (r |^ n))
.= (Catal . k) * (r |^ (n + 1)) by NEWTON:6
.= Fr2 . k by A24, A25, A27 ;
hence Fr1 . k = Fr2 . k ; :: thesis: verum
end;
for k being Nat st k in len Fr2 holds
Fr2 . k = (r |^ (n + 1)) * (CatalR . k) by A24, A25;
then Sum Fr2 = (r |^ (n + 1)) * (Sum CatalR) by A21, A24, Th49
.= Cat . (n + 1) by A3, A20
.= (Cat ^\ 1) . n by NAT_1:def 3 ;
hence (Cat ^\ 1) . y = (Cat (##) (r (#) Cat)) . y by A17, A19, A24, A26, AFINSQ_1:8; :: thesis: verum
end;
then A33: Cat ^\ 1 = Cat (##) (r (#) Cat) by FUNCT_2:12;
abs r >= 0 by COMPLEX1:46;
then A34: abs (4 * (abs r)) = 4 * (abs r) by ABSVALUE:def 1;
take Cat ; :: thesis: ( ( for n being Nat holds Cat . n = (Catalan (n + 1)) * (s |^ n) ) & ( abs s < 1 / 4 implies ( Cat is absolutely_summable & Sum Cat = 1 + (s * ((Sum Cat) |^ 2)) & Sum Cat = Sum Cat ) ) )
hereby :: thesis: ( abs s < 1 / 4 implies ( Cat is absolutely_summable & Sum Cat = 1 + (s * ((Sum Cat) |^ 2)) & Sum Cat = Sum Cat ) )
let n be Nat; :: thesis: Cat . n = (Catalan (n + 1)) * (s |^ n)
n in NAT by ORDINAL1:def 12;
hence Cat . n = (Catalan (n + 1)) * (s |^ n) by A3, A16; :: thesis: verum
end;
A35: r |^ 0 = 1 by NEWTON:4;
Cat . 0 = (Catalan (0 + 1)) * (r |^ 0) by A3;
then A36: (Partial_Sums Cat) . 0 = 1 by A35, CATALAN1:11, SERIES_1:def 1;
assume abs s < 1 / 4 ; :: thesis: ( Cat is absolutely_summable & Sum Cat = 1 + (s * ((Sum Cat) |^ 2)) & Sum Cat = Sum Cat )
then 4 * (abs r) < 4 * (1 / 4) by A16, XREAL_1:68;
then (4 * (abs r)) GeoSeq is summable by A34, SERIES_1:24;
then abs Cat is summable by A15, A14, SERIES_1:20;
hence A37: Cat is absolutely_summable by SERIES_1:def 4; :: thesis: ( Sum Cat = 1 + (s * ((Sum Cat) |^ 2)) & Sum Cat = Sum Cat )
then Cat is summable by SERIES_1:35;
then ( r (#) Cat is summable & Sum (r (#) Cat) = r * (Sum Cat) ) by SERIES_1:10;
then Sum (Cat ^\ (0 + 1)) = (Sum Cat) * (r * (Sum Cat)) by A37, A33, Th58;
then Sum Cat = 1 + (r * ((Sum Cat) * (Sum Cat))) by A37, A36, SERIES_1:15, SERIES_1:35;
hence ( Sum Cat = 1 + (s * ((Sum Cat) |^ 2)) & Sum Cat = Sum Cat ) by A16, WSIERP_1:1; :: thesis: verum
end;
consider SumC being Function of REAL,REAL such that
A38: for x being set st x in REAL holds
S1[x,SumC . x] from FUNCT_2:sch 1(A1);
 A39: for r, s being real number st 0 < s & s <= r & r < 1 / 4 holds
SumC . s <= SumC . r
proof
let r, s be real number ; :: thesis: ( 0 < s & s <= r & r < 1 / 4 implies SumC . s <= SumC . r )
assume that
A40: 0 < s and
A41: s <= r and
A42: r < 1 / 4 ; :: thesis: SumC . s <= SumC . r
r is Real by XREAL_0:def 1;
then consider Cr being Real_Sequence such that
A43: for n being Nat holds Cr . n = (Catalan (n + 1)) * (r |^ n) and
A44: ( abs r < 1 / 4 implies ( Cr is absolutely_summable & Sum Cr = 1 + (r * ((Sum Cr) |^ 2)) & SumC . r = Sum Cr ) ) by A38;
A45: Cr is summable by A40, A41, A42, A44, ABSVALUE:def 1, SERIES_1:35;
s is Real by XREAL_0:def 1;
then consider Cs being Real_Sequence such that
A46: for n being Nat holds Cs . n = (Catalan (n + 1)) * (s |^ n) and
A47: ( abs s < 1 / 4 implies ( Cs is absolutely_summable & Sum Cs = 1 + (s * ((Sum Cs) |^ 2)) & SumC . s = Sum Cs ) ) by A38;
A48: now
let n be Element of NAT ; :: thesis: Cs . n <= Cr . n
( s |^ n <= r |^ n & Catalan (n + 1) >= 0 ) by A40, A41, CATALAN1:17, PREPOWER:9;
then A49: (Catalan (n + 1)) * (s |^ n) <= (Catalan (n + 1)) * (r |^ n) by XREAL_1:64;
(Catalan (n + 1)) * (r |^ n) = Cr . n by A43;
hence Cs . n <= Cr . n by A46, A49; :: thesis: verum
end;
A50: s < 1 / 4 by A41, A42, XXREAL_0:2;
then Cs is summable by A40, A47, ABSVALUE:def 1, SERIES_1:35;
hence SumC . s <= SumC . r by A40, A41, A42, A50, A47, A44, A48, A45, ABSVALUE:def 1, TIETZE:5; :: thesis: verum
end;
set R = { r where r is Real : ( 0 < r & r < 1 / 4 & SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) ) } ;
A51: for r being real number st r <> 0 & abs r < 1 / 4 & not SumC . r = (1 - (sqrt (1 - (4 * r)))) / (2 * r) holds
SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r)
proof
let r be real number ; :: thesis: ( r <> 0 & abs r < 1 / 4 & not SumC . r = (1 - (sqrt (1 - (4 * r)))) / (2 * r) implies SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) )
assume that
A52: r <> 0 and
A53: abs r < 1 / 4 ; :: thesis: ( SumC . r = (1 - (sqrt (1 - (4 * r)))) / (2 * r) or SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) )
r <= 1 / 4 by A53, ABSVALUE:5;
then 4 * r <= (1 / 4) * 4 by XREAL_1:64;
then A54: (4 * r) - (4 * r) <= 1 - (4 * r) by XREAL_1:9;
r is Real by XREAL_0:def 1;
then consider Catal being Real_Sequence such that
for n being Nat holds Catal . n = (Catalan (n + 1)) * (r |^ n) and
A55: ( abs r < 1 / 4 implies ( Catal is absolutely_summable & Sum Catal = 1 + (r * ((Sum Catal) |^ 2)) & SumC . r = Sum Catal ) ) by A38;
set S = Sum Catal;
Sum Catal = 1 + (r * ((Sum Catal) ^2)) by A53, A55, WSIERP_1:1;
then A56: ((r * ((Sum Catal) ^2)) + ((- 1) * (Sum Catal))) + 1 = 0 ;
( delta (r,(- 1),1) = 1 - (4 * r) & - (- 1) = 1 ) ;
hence ( SumC . r = (1 - (sqrt (1 - (4 * r)))) / (2 * r) or SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) ) by A52, A53, A55, A56, A54, FIB_NUM:6; :: thesis: verum
end;
A57: for r, s being real number st 0 < r & r < s & s < 1 / 4 holds
(1 + (sqrt (1 - (4 * r)))) / (2 * r) > (1 + (sqrt (1 - (4 * s)))) / (2 * s)
proof
let r, s be real number ; :: thesis: ( 0 < r & r < s & s < 1 / 4 implies (1 + (sqrt (1 - (4 * r)))) / (2 * r) > (1 + (sqrt (1 - (4 * s)))) / (2 * s) )
assume that
A58: 0 < r and
A59: r < s and
A60: s < 1 / 4 ; :: thesis: (1 + (sqrt (1 - (4 * r)))) / (2 * r) > (1 + (sqrt (1 - (4 * s)))) / (2 * s)
4 * s < 4 * (1 / 4) by A60, XREAL_1:68;
then A61: (4 * s) - (4 * s) < 1 - (4 * s) by XREAL_1:9;
then A62: sqrt (1 - (4 * s)) > 0 by SQUARE_1:25;
4 * r < 4 * s by A59, XREAL_1:68;
then 1 - (4 * r) >= 1 - (4 * s) by XREAL_1:10;
then sqrt (1 - (4 * r)) >= sqrt (1 - (4 * s)) by A61, SQUARE_1:26;
then 1 + (sqrt (1 - (4 * r))) >= 1 + (sqrt (1 - (4 * s))) by XREAL_1:7;
then A63: (1 + (sqrt (1 - (4 * r)))) / (2 * r) >= (1 + (sqrt (1 - (4 * s)))) / (2 * r) by A58, XREAL_1:72;
( 2 * r > 2 * 0 & 2 * r < 2 * s ) by A58, A59, XREAL_1:68;
then (1 + (sqrt (1 - (4 * s)))) / (2 * r) > (1 + (sqrt (1 - (4 * s)))) / (2 * s) by A62, XREAL_1:76;
hence (1 + (sqrt (1 - (4 * r)))) / (2 * r) > (1 + (sqrt (1 - (4 * s)))) / (2 * s) by A63, XXREAL_0:2; :: thesis: verum
end;
A64: { r where r is Real : ( 0 < r & r < 1 / 4 & SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) ) } = {}
proof
assume { r where r is Real : ( 0 < r & r < 1 / 4 & SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) ) } <> {} ; :: thesis: contradiction
then consider x being set such that
A65: x in { r where r is Real : ( 0 < r & r < 1 / 4 & SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) ) } by XBOOLE_0:def 1;
consider r being Real such that
x = r and
A66: 0 < r and
A67: r < 1 / 4 and
A68: SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) by A65;
consider s being real number such that
A69: r < s and
A70: s < 1 / 4 by A67, XREAL_1:5;
A71: abs s = s by A66, A69, ABSVALUE:def 1;
4 * s < 4 * (1 / 4) by A70, XREAL_1:68;
then (4 * s) - (4 * s) < 1 - (4 * s) by XREAL_1:9;
then sqrt (1 - (4 * s)) > 0 by SQUARE_1:25;
then 1 - (sqrt (1 - (4 * s))) <= 1 - 0 by XREAL_1:10;
then A72: (1 - (sqrt (1 - (4 * s)))) / (2 * s) <= 1 / (2 * s) by A66, A69, XREAL_1:72;
A73: 2 * r > 2 * 0 by A66, XREAL_1:68;
A74: s is Real by XREAL_0:def 1;
{ r where r is Real : ( 0 < r & r < 1 / 4 & SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) ) } c= {r}
proof
assume not { r where r is Real : ( 0 < r & r < 1 / 4 & SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) ) } c= {r} ; :: thesis: contradiction
then { r where r is Real : ( 0 < r & r < 1 / 4 & SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) ) } \ {r} <> {} by XBOOLE_1:37;
then consider y being set such that
A75: y in { r where r is Real : ( 0 < r & r < 1 / 4 & SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) ) } \ {r} by XBOOLE_0:def 1;
y in { r where r is Real : ( 0 < r & r < 1 / 4 & SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) ) } by A75;
then consider s being Real such that
A76: y = s and
A77: 0 < s and
A78: s < 1 / 4 and
A79: SumC . s = (1 + (sqrt (1 - (4 * s)))) / (2 * s) ;
A80: r <> s by A75, A76, ZFMISC_1:56;
now
per cases ( r > s or r < s ) by A80, XXREAL_0:1;
suppose A81: r > s ; :: thesis: contradiction
then SumC . s > SumC . r by A57, A67, A68, A77, A79;
hence contradiction by A39, A67, A77, A81; :: thesis: verum
end;
suppose A82: r < s ; :: thesis: contradiction
then SumC . r > SumC . s by A57, A66, A68, A78, A79;
hence contradiction by A39, A66, A78, A82; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
then not s in { r where r is Real : ( 0 < r & r < 1 / 4 & SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) ) } by A69, TARSKI:def 1;
then SumC . s <> (1 + (sqrt (1 - (4 * s)))) / (2 * s) by A66, A69, A70, A74;
then A83: SumC . s = (1 - (sqrt (1 - (4 * s)))) / (2 * s) by A51, A66, A69, A70, A71;
4 * r < 4 * (1 / 4) by A67, XREAL_1:68;
then (4 * r) - (4 * r) < 1 - (4 * r) by XREAL_1:9;
then sqrt (1 - (4 * r)) > 0 by SQUARE_1:25;
then 1 + 0 < 1 + (sqrt (1 - (4 * r))) by XREAL_1:8;
then A84: 1 / (2 * r) < SumC . r by A68, A73, XREAL_1:74;
2 * r < 2 * s by A69, XREAL_1:68;
then 1 / (2 * s) < 1 / (2 * r) by A73, XREAL_1:76;
then SumC . s < 1 / (2 * r) by A83, A72, XXREAL_0:2;
then SumC . s < SumC . r by A84, XXREAL_0:2;
hence contradiction by A39, A66, A69, A70; :: thesis: verum
end;
A85: for r being real number st 0 < r & abs r < 1 / 4 holds
SumC . r = (1 - (sqrt (1 - (4 * r)))) / (2 * r)
proof
let r be real number ; :: thesis: ( 0 < r & abs r < 1 / 4 implies SumC . r = (1 - (sqrt (1 - (4 * r)))) / (2 * r) )
assume that
A86: 0 < r and
A87: abs r < 1 / 4 ; :: thesis: SumC . r = (1 - (sqrt (1 - (4 * r)))) / (2 * r)
assume SumC . r <> (1 - (sqrt (1 - (4 * r)))) / (2 * r) ; :: thesis: contradiction
then A88: SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) by A51, A86, A87;
abs r = r by A86, ABSVALUE:def 1;
then r in { r where r is Real : ( 0 < r & r < 1 / 4 & SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) ) } by A86, A87, A88;
hence contradiction by A64; :: thesis: verum
end;
A89: for r being real number st r < 0 & abs r < 1 / 4 holds
SumC . r = (1 - (sqrt (1 - (4 * r)))) / (2 * r)
proof
let r be real number ; :: thesis: ( r < 0 & abs r < 1 / 4 implies SumC . r = (1 - (sqrt (1 - (4 * r)))) / (2 * r) )
assume that
A90: r < 0 and
A91: abs r < 1 / 4 ; :: thesis: SumC . r = (1 - (sqrt (1 - (4 * r)))) / (2 * r)
2 * r < 2 * 0 by A90, XREAL_1:68;
then A92: ( abs (2 * r) = - (2 * r) & 0 - (2 * r) > 0 - 0 ) by ABSVALUE:def 1;
A93: abs (- r) < 1 / 4 by A91, COMPLEX1:52;
then 1 / 4 >= - r by ABSVALUE:5;
then 4 * (1 / 4) >= 4 * (- r) by XREAL_1:64;
then 1 - (4 * (- r)) >= (4 * (- r)) - (4 * (- r)) by XREAL_1:9;
then sqrt (1 - (4 * (- r))) >= 0 by SQUARE_1:def 2;
then A94: 1 - (sqrt (1 - (4 * (- r)))) <= 1 - 0 by XREAL_1:10;
A95: sqrt (1 - (4 * r)) > 0 by A90, SQUARE_1:25;
then 1 + (sqrt (1 - (4 * r))) > 1 + 0 by XREAL_1:8;
then A96: 1 - (sqrt (1 - (4 * (- r)))) < 1 + (sqrt (1 - (4 * r))) by A94, XXREAL_0:2;
1 + (sqrt (1 - (4 * r))) = abs (1 + (sqrt (1 - (4 * r)))) by A95, ABSVALUE:def 1;
then A97: (1 - (sqrt (1 - (4 * (- r))))) / (2 * (- r)) < (abs (1 + (sqrt (1 - (4 * r))))) / (abs (2 * r)) by A96, A92, XREAL_1:74;
consider CR being Real_Sequence such that
A98: for n being Nat holds CR . n = (Catalan (n + 1)) * ((- r) |^ n) and
A99: ( abs (- r) < 1 / 4 implies ( CR is absolutely_summable & Sum CR = 1 + ((- r) * ((Sum CR) |^ 2)) & SumC . (- r) = Sum CR ) ) by A38;
assume A100: SumC . r <> (1 - (sqrt (1 - (4 * r)))) / (2 * r) ; :: thesis: contradiction
r is Real by XREAL_0:def 1;
then consider Cr being Real_Sequence such that
A101: for n being Nat holds Cr . n = (Catalan (n + 1)) * (r |^ n) and
A102: ( abs r < 1 / 4 implies ( Cr is absolutely_summable & Sum Cr = 1 + (r * ((Sum Cr) |^ 2)) & SumC . r = Sum Cr ) ) by A38;
now
let x be set ; :: thesis: ( x in NAT implies (abs Cr) . x = CR . x )
assume x in NAT ; :: thesis: (abs Cr) . x = CR . x
then reconsider n = x as Element of NAT ;
(- r) |^ n = ((- 1) * r) |^ n
.= ((- 1) |^ n) * (r |^ n) by NEWTON:7 ;
then A103: abs ((- r) |^ n) = (abs ((- 1) |^ n)) * (abs (r |^ n)) by COMPLEX1:65
.= 1 * (abs (r |^ n)) by SERIES_2:1 ;
Catalan (n + 1) >= 0 by CATALAN1:17;
then A104: abs (Catalan (n + 1)) = Catalan (n + 1) by ABSVALUE:def 1;
(- r) |^ n >= 0 by A90, POWER:3;
then abs ((- r) |^ n) = (- r) |^ n by ABSVALUE:def 1;
then CR . n = (abs (r |^ n)) * (abs (Catalan (n + 1))) by A98, A103, A104
.= abs ((r |^ n) * (Catalan (n + 1))) by COMPLEX1:65
.= abs (Cr . n) by A101
.= (abs Cr) . n by SEQ_1:12 ;
hence (abs Cr) . x = CR . x ; :: thesis: verum
end;
then A105: abs Cr = CR by FUNCT_2:12;
0 - r > 0 - 0 by A90;
then A106: Sum CR = (1 - (sqrt (1 - (4 * (- r))))) / (2 * (- r)) by A85, A99, A93;
abs (Sum Cr) <= Sum (abs Cr) by A91, A102, TIETZE:6;
then abs ((1 + (sqrt (1 - (4 * r)))) / (2 * r)) <= Sum CR by A51, A90, A91, A102, A105, A100;
hence contradiction by A106, A97, COMPLEX1:67; :: thesis: verum
end;
let r be real number ; :: thesis: ex Catal being Real_Sequence st
( ( for n being Nat holds Catal . n = (Catalan (n + 1)) * (r |^ n) ) & ( abs r < 1 / 4 implies ( Catal is absolutely_summable & Sum Catal = 1 + (r * ((Sum Catal) |^ 2)) & Sum Catal = 2 / (1 + (sqrt (1 - (4 * r)))) & ( r <> 0 implies Sum Catal = (1 - (sqrt (1 - (4 * r)))) / (2 * r) ) ) ) )
r is Real by XREAL_0:def 1;
then consider Cat being Real_Sequence such that
A107: for n being Nat holds Cat . n = (Catalan (n + 1)) * (r |^ n) and
A108: ( abs r < 1 / 4 implies ( Cat is absolutely_summable & Sum Cat = 1 + (r * ((Sum Cat) |^ 2)) & SumC . r = Sum Cat ) ) by A38;
set s = sqrt (1 - (4 * r));
take Cat ; :: thesis: ( ( for n being Nat holds Cat . n = (Catalan (n + 1)) * (r |^ n) ) & ( abs r < 1 / 4 implies ( Cat is absolutely_summable & Sum Cat = 1 + (r * ((Sum Cat) |^ 2)) & Sum Cat = 2 / (1 + (sqrt (1 - (4 * r)))) & ( r <> 0 implies Sum Cat = (1 - (sqrt (1 - (4 * r)))) / (2 * r) ) ) ) )
thus for n being Nat holds Cat . n = (Catalan (n + 1)) * (r |^ n) by A107; :: thesis: ( abs r < 1 / 4 implies ( Cat is absolutely_summable & Sum Cat = 1 + (r * ((Sum Cat) |^ 2)) & Sum Cat = 2 / (1 + (sqrt (1 - (4 * r)))) & ( r <> 0 implies Sum Cat = (1 - (sqrt (1 - (4 * r)))) / (2 * r) ) ) )
assume A109: abs r < 1 / 4 ; :: thesis: ( Cat is absolutely_summable & Sum Cat = 1 + (r * ((Sum Cat) |^ 2)) & Sum Cat = 2 / (1 + (sqrt (1 - (4 * r)))) & ( r <> 0 implies Sum Cat = (1 - (sqrt (1 - (4 * r)))) / (2 * r) ) )
hence ( Cat is absolutely_summable & Sum Cat = 1 + (r * ((Sum Cat) |^ 2)) ) by A108; :: thesis: ( Sum Cat = 2 / (1 + (sqrt (1 - (4 * r)))) & ( r <> 0 implies Sum Cat = (1 - (sqrt (1 - (4 * r)))) / (2 * r) ) )
A110: ( r <> 0 implies Sum Cat = (1 - (sqrt (1 - (4 * r)))) / (2 * r) )
proof
assume r <> 0 ; :: thesis: Sum Cat = (1 - (sqrt (1 - (4 * r)))) / (2 * r)
then ( r > 0 or r < 0 ) ;
hence Sum Cat = (1 - (sqrt (1 - (4 * r)))) / (2 * r) by A85, A89, A108, A109; :: thesis: verum
end;
now
per cases ( r = 0 or r <> 0 ) ;
suppose r = 0 ; :: thesis: 2 / (1 + (sqrt (1 - (4 * r)))) = Sum Cat
hence 2 / (1 + (sqrt (1 - (4 * r)))) = Sum Cat by A108, A109, SQUARE_1:18; :: thesis: verum
end;
suppose A111: r <> 0 ; :: thesis: Sum Cat = 2 / (1 + (sqrt (1 - (4 * r))))
then A112: 2 * r <> 0 ;
r <= 1 / 4 by A109, ABSVALUE:5;
then 4 * r <= 4 * (1 / 4) by XREAL_1:64;
then A113: 1 - (4 * r) >= (4 * r) - (4 * r) by XREAL_1:9;
then sqrt (1 - (4 * r)) >= 0 by SQUARE_1:def 2;
then (1 + (sqrt (1 - (4 * r)))) / (1 + (sqrt (1 - (4 * r)))) = 1 by XCMPLX_1:60;
then (1 - (sqrt (1 - (4 * r)))) / (2 * r) = ((1 - (sqrt (1 - (4 * r)))) / (2 * r)) * ((1 + (sqrt (1 - (4 * r)))) / (1 + (sqrt (1 - (4 * r)))))
.= ((1 - (sqrt (1 - (4 * r)))) * (1 + (sqrt (1 - (4 * r))))) / ((2 * r) * (1 + (sqrt (1 - (4 * r))))) by XCMPLX_1:76
.= ((1 ^2) - ((sqrt (1 - (4 * r))) ^2)) / ((2 * r) * (1 + (sqrt (1 - (4 * r)))))
.= (1 - (1 - (4 * r))) / ((2 * r) * (1 + (sqrt (1 - (4 * r))))) by A113, SQUARE_1:def 2
.= ((2 * r) * 2) / ((2 * r) * (1 + (sqrt (1 - (4 * r)))))
.= ((2 * r) / (2 * r)) * (2 / (1 + (sqrt (1 - (4 * r))))) by XCMPLX_1:76
.= 1 * (2 / (1 + (sqrt (1 - (4 * r))))) by A112, XCMPLX_1:60 ;
hence Sum Cat = 2 / (1 + (sqrt (1 - (4 * r)))) by A110, A111; :: thesis: verum
end;
end;
end;
hence ( Sum Cat = 2 / (1 + (sqrt (1 - (4 * r)))) & ( r <> 0 implies Sum Cat = (1 - (sqrt (1 - (4 * r)))) / (2 * r) ) ) by A110; :: thesis: verum