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:132;
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:66;
set n1 = n + 1;
B: ( n in NAT & n + 1 in NAT ) by ORDINAL1:def 13;
A7: ( abs (r |^ (n + 1)) >= 0 & r |^ (n + 1) = r * (r |^ n) ) by COMPLEX1:132, NEWTON:11;
Catalan ((n + 1) + 1) >= 0 by CATALAN1:17;
then A8: 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 A8, CATALAN1:21;
then A9: (abs (r |^ (n + 1))) * (abs (Catalan ((n + 1) + 1))) <= (4 * (abs (Catalan (n + 1)))) * (abs (r * (r |^ n))) by A7, XREAL_1:66;
abs (r * (r |^ n)) = (abs r) * (abs (r |^ n)) by COMPLEX1:151;
then abs ((r |^ (n + 1)) * (Catalan ((n + 1) + 1))) <= (4 * (abs r)) * ((abs (Catalan (n + 1))) * (abs (r |^ n))) by A9, COMPLEX1:151;
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:151, ORDINAL1:def 13;
then A10: abs (Cat . (n + 1)) <= (4 * (abs r)) * (abs (Cat . n)) by A3;
abs (Cat . n) = (abs Cat) . n by SEQ_1:16, B;
then (abs Cat) . (n + 1) <= (4 * (abs r)) * ((abs Cat) . n) by A10, SEQ_1:16;
then (abs Cat) . (n + 1) <= (4 * (abs r)) * (((4 * (abs r)) GeoSeq ) . n) by A6, XXREAL_0:2;
hence S2[n + 1] by PREPOWER:4, B; :: thesis: verum
end;
Cat . 0 = (Catalan (0 + 1)) * (r |^ 0 ) by A3;
then A11: (abs Cat) . 0 = abs (r |^ 0 ) by CATALAN1:11, SEQ_1:16;
( r |^ 0 = 1 & (4 * (abs r)) |^ 0 = 1 ) by NEWTON:9;
then A12: S2[ 0 ] by A11, A2, PREPOWER:def 1;
for n being Nat holds S2[n] from NAT_1:sch 2(A12, A4);
 then B13: for n being Element of NAT holds S2[n] ;
A14: now
let n be Element of NAT ; :: thesis: (abs Cat) . n >= 0
(abs Cat) . n = abs (Cat . n) by SEQ_1:16;
hence (abs Cat) . n >= 0 by COMPLEX1:132; :: 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 A15: 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
A16: dom Fr1 = n + 1 and
A17: for i being Nat st i in n + 1 holds
Fr1 . i = (Cat . i) * ((r (#) Cat) . (n -' i)) and
A18: Sum Fr1 = (Cat (##) (r (#) Cat)) . n by Def5;
consider Catal being XFinSequence of such that
A19: Sum Catal = Catalan ((n + 1) + 1) and
A20: dom Catal = n + 1 and
A21: 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);
A22: 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
A23: dom Fr2 = n + 1 and
A24: for k being Nat st k in n + 1 holds
S3[k,Fr2 . k] from STIRL2_1:sch 5(A22);
A25: now
let k be Nat; :: thesis: ( k in dom Fr2 implies Fr1 . k = Fr2 . k )
assume A26: k in dom Fr2 ; :: thesis: Fr1 . k = Fr2 . k
W: k in NAT by ORDINAL1:def 13;
A27: k < n + 1 by A23, A26, NAT_1:45;
then A28: (n + 1) -' k = (n + 1) - k by XREAL_1:235;
A29: n = k + (n - k) ;
k <= n by A27, NAT_1:13;
then A30: n -' k = n - k by XREAL_1:235;
then Fr1 . k = (Cat . k) * ((r (#) Cat) . (n - k)) by A17, A23, A26
.= ((Catalan (k + 1)) * (r |^ k)) * ((r (#) Cat) . (n - k)) by A3, W
.= ((Catalan (k + 1)) * (r |^ k)) * (r * (Cat . (n - k))) by A30, SEQ_1:13
.= ((Catalan (k + 1)) * (r |^ k)) * (r * ((Catalan ((n -' k) + 1)) * (r |^ (n -' k)))) by A3, A30
.= (((Catalan (k + 1)) * (Catalan ((n + 1) -' k))) * r) * ((r |^ k) * (r |^ (n -' k))) by A30, A28
.= (((Catalan (k + 1)) * (Catalan ((n + 1) -' k))) * r) * (r |^ n) by A30, A29, NEWTON:13
.= ((Catal . k) * r) * (r |^ n) by A21, A27
.= (Catal . k) * (r * (r |^ n))
.= (Catal . k) * (r |^ (n + 1)) by NEWTON:11
.= Fr2 . k by A23, A24, A26 ;
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 A23, A24;
then Sum Fr2 = (r |^ (n + 1)) * (Sum CatalR) by A20, A23, Th49
.= Cat . (n + 1) by A3, A19
.= (Cat ^\ 1) . n by NAT_1:def 3 ;
hence (Cat ^\ 1) . y = (Cat (##) (r (#) Cat)) . y by A16, A18, A23, A25, AFINSQ_1:10; :: thesis: verum
end;
then A31: Cat ^\ 1 = Cat (##) (r (#) Cat) by FUNCT_2:18;
abs r >= 0 by COMPLEX1:132;
then A32: 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 13;
hence Cat . n = (Catalan (n + 1)) * (s |^ n) by A3, A15; :: thesis: verum
end;
A33: r |^ 0 = 1 by NEWTON:9;
Cat . 0 = (Catalan (0 + 1)) * (r |^ 0 ) by A3;
then A34: (Partial_Sums Cat) . 0 = 1 by A33, 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 A15, XREAL_1:70;
then (4 * (abs r)) GeoSeq is summable by A32, SERIES_1:28;
then abs Cat is summable by A14, SERIES_1:24, B13;
hence A35: Cat is absolutely_summable by SERIES_1:def 5; :: thesis: ( Sum Cat = 1 + (s * ((Sum Cat) |^ 2)) & Sum Cat = Sum Cat )
then Cat is summable by SERIES_1:40;
then ( r (#) Cat is summable & Sum (r (#) Cat) = r * (Sum Cat) ) by SERIES_1:13;
then Sum (Cat ^\ (0 + 1)) = (Sum Cat) * (r * (Sum Cat)) by A35, A31, Th58;
then Sum Cat = 1 + (r * ((Sum Cat) * (Sum Cat))) by A35, A34, SERIES_1:18, SERIES_1:40;
hence ( Sum Cat = 1 + (s * ((Sum Cat) |^ 2)) & Sum Cat = Sum Cat ) by A15, WSIERP_1:2; :: thesis: verum
end;
consider SumC being Function of REAL ,REAL such that
A36: for x being set st x in REAL holds
S1[x,SumC . x] from FUNCT_2:sch 1(A1);
 A37: 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
A38: 0 < s and
A39: s <= r and
A40: r < 1 / 4 ; :: thesis: SumC . s <= SumC . r
r is Real by XREAL_0:def 1;
then consider Cr being Real_Sequence such that
A41: for n being Nat holds Cr . n = (Catalan (n + 1)) * (r |^ n) and
A42: ( abs r < 1 / 4 implies ( Cr is absolutely_summable & Sum Cr = 1 + (r * ((Sum Cr) |^ 2)) & SumC . r = Sum Cr ) ) by A36;
A43: Cr is summable by A38, A39, A40, A42, ABSVALUE:def 1, SERIES_1:40;
s is Real by XREAL_0:def 1;
then consider Cs being Real_Sequence such that
A44: for n being Nat holds Cs . n = (Catalan (n + 1)) * (s |^ n) and
A45: ( abs s < 1 / 4 implies ( Cs is absolutely_summable & Sum Cs = 1 + (s * ((Sum Cs) |^ 2)) & SumC . s = Sum Cs ) ) by A36;
A46: now
let n be Element of NAT ; :: thesis: Cs . n <= Cr . n
( s |^ n <= r |^ n & Catalan (n + 1) >= 0 ) by A38, A39, CATALAN1:17, PREPOWER:17;
then A47: (Catalan (n + 1)) * (s |^ n) <= (Catalan (n + 1)) * (r |^ n) by XREAL_1:66;
(Catalan (n + 1)) * (r |^ n) = Cr . n by A41;
hence Cs . n <= Cr . n by A44, A47; :: thesis: verum
end;
A48: s < 1 / 4 by A39, A40, XXREAL_0:2;
then Cs is summable by A38, A45, ABSVALUE:def 1, SERIES_1:40;
hence SumC . s <= SumC . r by A38, A39, A40, A48, A45, A42, A46, A43, ABSVALUE:def 1, TIETZE:7; :: thesis: verum
end;
set R = { r where r is Real : ( 0 < r & r < 1 / 4 & SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) ) } ;
A49: 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
A50: r <> 0 and
A51: 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 A51, ABSVALUE:12;
then 4 * r <= (1 / 4) * 4 by XREAL_1:66;
then A52: (4 * r) - (4 * r) <= 1 - (4 * r) by XREAL_1:11;
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
A53: ( abs r < 1 / 4 implies ( Catal is absolutely_summable & Sum Catal = 1 + (r * ((Sum Catal) |^ 2)) & SumC . r = Sum Catal ) ) by A36;
set S = Sum Catal;
Sum Catal = 1 + (r * ((Sum Catal) ^2 )) by A51, A53, WSIERP_1:2;
then A54: ((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 A50, A51, A53, A54, A52, FIB_NUM:6; :: thesis: verum
end;
A55: 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
A56: 0 < r and
A57: r < s and
A58: s < 1 / 4 ; :: thesis: (1 + (sqrt (1 - (4 * r)))) / (2 * r) > (1 + (sqrt (1 - (4 * s)))) / (2 * s)
4 * s < 4 * (1 / 4) by A58, XREAL_1:70;
then A59: (4 * s) - (4 * s) < 1 - (4 * s) by XREAL_1:11;
then A60: sqrt (1 - (4 * s)) > 0 by SQUARE_1:93;
4 * r < 4 * s by A57, XREAL_1:70;
then 1 - (4 * r) >= 1 - (4 * s) by XREAL_1:12;
then sqrt (1 - (4 * r)) >= sqrt (1 - (4 * s)) by A59, SQUARE_1:94;
then 1 + (sqrt (1 - (4 * r))) >= 1 + (sqrt (1 - (4 * s))) by XREAL_1:9;
then A61: (1 + (sqrt (1 - (4 * r)))) / (2 * r) >= (1 + (sqrt (1 - (4 * s)))) / (2 * r) by A56, XREAL_1:74;
( 2 * r > 2 * 0 & 2 * r < 2 * s ) by A56, A57, XREAL_1:70;
then (1 + (sqrt (1 - (4 * s)))) / (2 * r) > (1 + (sqrt (1 - (4 * s)))) / (2 * s) by A60, XREAL_1:78;
hence (1 + (sqrt (1 - (4 * r)))) / (2 * r) > (1 + (sqrt (1 - (4 * s)))) / (2 * s) by A61, XXREAL_0:2; :: thesis: verum
end;
A62: { 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
A63: 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
A64: 0 < r and
A65: r < 1 / 4 and
A66: SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) by A63;
consider s being real number such that
A67: r < s and
A68: s < 1 / 4 by A65, XREAL_1:7;
A69: abs s = s by A64, A67, ABSVALUE:def 1;
4 * s < 4 * (1 / 4) by A68, XREAL_1:70;
then (4 * s) - (4 * s) < 1 - (4 * s) by XREAL_1:11;
then sqrt (1 - (4 * s)) > 0 by SQUARE_1:93;
then 1 - (sqrt (1 - (4 * s))) <= 1 - 0 by XREAL_1:12;
then A70: (1 - (sqrt (1 - (4 * s)))) / (2 * s) <= 1 / (2 * s) by A64, A67, XREAL_1:74;
A71: 2 * r > 2 * 0 by A64, XREAL_1:70;
A72: 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
A73: 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 A73;
then consider s being Real such that
A74: y = s and
A75: 0 < s and
A76: s < 1 / 4 and
A77: SumC . s = (1 + (sqrt (1 - (4 * s)))) / (2 * s) ;
A78: r <> s by A73, A74, ZFMISC_1:64;
now
per cases ( r > s or r < s ) by A78, XXREAL_0:1;
suppose A79: r > s ; :: thesis: contradiction
then SumC . s > SumC . r by A55, A65, A66, A75, A77;
hence contradiction by A37, A65, A75, A79; :: thesis: verum
end;
suppose A80: r < s ; :: thesis: contradiction
then SumC . r > SumC . s by A55, A64, A66, A76, A77;
hence contradiction by A37, A64, A76, A80; :: 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 A67, TARSKI:def 1;
then SumC . s <> (1 + (sqrt (1 - (4 * s)))) / (2 * s) by A64, A67, A68, A72;
then A81: SumC . s = (1 - (sqrt (1 - (4 * s)))) / (2 * s) by A49, A64, A67, A68, A69;
4 * r < 4 * (1 / 4) by A65, XREAL_1:70;
then (4 * r) - (4 * r) < 1 - (4 * r) by XREAL_1:11;
then sqrt (1 - (4 * r)) > 0 by SQUARE_1:93;
then 1 + 0 < 1 + (sqrt (1 - (4 * r))) by XREAL_1:10;
then A82: 1 / (2 * r) < SumC . r by A66, A71, XREAL_1:76;
2 * r < 2 * s by A67, XREAL_1:70;
then 1 / (2 * s) < 1 / (2 * r) by A71, XREAL_1:78;
then SumC . s < 1 / (2 * r) by A81, A70, XXREAL_0:2;
then SumC . s < SumC . r by A82, XXREAL_0:2;
hence contradiction by A37, A64, A67, A68; :: thesis: verum
end;
A83: 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
A84: 0 < r and
A85: 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 A86: SumC . r = (1 + (sqrt (1 - (4 * r)))) / (2 * r) by A49, A84, A85;
abs r = r by A84, 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 A84, A85, A86;
hence contradiction by A62; :: thesis: verum
end;
A87: 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
A88: r < 0 and
A89: abs r < 1 / 4 ; :: thesis: SumC . r = (1 - (sqrt (1 - (4 * r)))) / (2 * r)
2 * r < 2 * 0 by A88, XREAL_1:70;
then A90: ( abs (2 * r) = - (2 * r) & 0 - (2 * r) > 0 - 0 ) by ABSVALUE:def 1;
A91: abs (- r) < 1 / 4 by A89, COMPLEX1:138;
then 1 / 4 >= - r by ABSVALUE:12;
then 4 * (1 / 4) >= 4 * (- r) by XREAL_1:66;
then 1 - (4 * (- r)) >= (4 * (- r)) - (4 * (- r)) by XREAL_1:11;
then sqrt (1 - (4 * (- r))) >= 0 by SQUARE_1:def 4;
then A92: 1 - (sqrt (1 - (4 * (- r)))) <= 1 - 0 by XREAL_1:12;
A93: sqrt (1 - (4 * r)) > 0 by A88, SQUARE_1:93;
then 1 + (sqrt (1 - (4 * r))) > 1 + 0 by XREAL_1:10;
then A94: 1 - (sqrt (1 - (4 * (- r)))) < 1 + (sqrt (1 - (4 * r))) by A92, XXREAL_0:2;
1 + (sqrt (1 - (4 * r))) = abs (1 + (sqrt (1 - (4 * r)))) by A93, ABSVALUE:def 1;
then A95: (1 - (sqrt (1 - (4 * (- r))))) / (2 * (- r)) < (abs (1 + (sqrt (1 - (4 * r))))) / (abs (2 * r)) by A94, A90, XREAL_1:76;
consider CR being Real_Sequence such that
A96: for n being Nat holds CR . n = (Catalan (n + 1)) * ((- r) |^ n) and
A97: ( abs (- r) < 1 / 4 implies ( CR is absolutely_summable & Sum CR = 1 + ((- r) * ((Sum CR) |^ 2)) & SumC . (- r) = Sum CR ) ) by A36;
assume A98: 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
A99: for n being Nat holds Cr . n = (Catalan (n + 1)) * (r |^ n) and
A100: ( abs r < 1 / 4 implies ( Cr is absolutely_summable & Sum Cr = 1 + (r * ((Sum Cr) |^ 2)) & SumC . r = Sum Cr ) ) by A36;
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:12 ;
then A101: abs ((- r) |^ n) = (abs ((- 1) |^ n)) * (abs (r |^ n)) by COMPLEX1:151
.= 1 * (abs (r |^ n)) by SERIES_2:1 ;
Catalan (n + 1) >= 0 by CATALAN1:17;
then A102: abs (Catalan (n + 1)) = Catalan (n + 1) by ABSVALUE:def 1;
(- r) |^ n >= 0 by A88, POWER:3;
then abs ((- r) |^ n) = (- r) |^ n by ABSVALUE:def 1;
then CR . n = (abs (r |^ n)) * (abs (Catalan (n + 1))) by A96, A101, A102
.= abs ((r |^ n) * (Catalan (n + 1))) by COMPLEX1:151
.= abs (Cr . n) by A99
.= (abs Cr) . n by SEQ_1:16 ;
hence (abs Cr) . x = CR . x ; :: thesis: verum
end;
then A103: abs Cr = CR by FUNCT_2:18;
0 - r > 0 - 0 by A88;
then A104: Sum CR = (1 - (sqrt (1 - (4 * (- r))))) / (2 * (- r)) by A83, A97, A91;
abs (Sum Cr) <= Sum (abs Cr) by A89, A100, TIETZE:8;
then abs ((1 + (sqrt (1 - (4 * r)))) / (2 * r)) <= Sum CR by A49, A88, A89, A100, A103, A98;
hence contradiction by A104, A95, COMPLEX1:153; :: 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
A105: for n being Nat holds Cat . n = (Catalan (n + 1)) * (r |^ n) and
A106: ( abs r < 1 / 4 implies ( Cat is absolutely_summable & Sum Cat = 1 + (r * ((Sum Cat) |^ 2)) & SumC . r = Sum Cat ) ) by A36;
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 A105; :: 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 A107: 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 A106; :: thesis: ( Sum Cat = 2 / (1 + (sqrt (1 - (4 * r)))) & ( r <> 0 implies Sum Cat = (1 - (sqrt (1 - (4 * r)))) / (2 * r) ) )
A108: ( 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 A83, A87, A106, A107; :: 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 A106, A107, SQUARE_1:83; :: thesis: verum
end;
suppose A109: r <> 0 ; :: thesis: Sum Cat = 2 / (1 + (sqrt (1 - (4 * r))))
then A110: 2 * r <> 0 ;
r <= 1 / 4 by A107, ABSVALUE:12;
then 4 * r <= 4 * (1 / 4) by XREAL_1:66;
then A111: 1 - (4 * r) >= (4 * r) - (4 * r) by XREAL_1:11;
then sqrt (1 - (4 * r)) >= 0 by SQUARE_1:def 4;
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:77
.= ((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 A111, SQUARE_1:def 4
.= ((2 * r) * 2) / ((2 * r) * (1 + (sqrt (1 - (4 * r)))))
.= ((2 * r) / (2 * r)) * (2 / (1 + (sqrt (1 - (4 * r))))) by XCMPLX_1:77
.= 1 * (2 / (1 + (sqrt (1 - (4 * r))))) by A110, XCMPLX_1:60 ;
hence Sum Cat = 2 / (1 + (sqrt (1 - (4 * r)))) by A108, A109; :: 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 A108; :: thesis: verum