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