let F be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds F . n = (Fib (n + 1)) / (Fib n) ) implies ( F is convergent & lim F = tau ) )
assume A1: for n being Element of NAT holds F . n = (Fib (n + 1)) / (Fib n) ; :: thesis: ( F is convergent & lim F = tau )
consider f being Real_Sequence such that
A2: for n being Element of NAT holds f . n = Fib n from SEQ_1:sch 1();
 set f1 = f ^\ 1;
A3: for n being Element of NAT holds (f ^\ 1) . n = Fib (n + 1)
proof
let n be Element of NAT ; :: thesis: (f ^\ 1) . n = Fib (n + 1)
(f ^\ 1) . n = f . (n + 1) by NAT_1:def 3
.= Fib (n + 1) by A2 ;
hence (f ^\ 1) . n = Fib (n + 1) ; :: thesis: verum
end;
A4: F = (f ^\ 1) /" f
proof
for n being Element of NAT holds F . n = ((f ^\ 1) /" f) . n
proof
let n be Element of NAT ; :: thesis: F . n = ((f ^\ 1) /" f) . n
((f ^\ 1) /" f) . n = ((f ^\ 1) . n) / (f . n) by Th11
.= (Fib (n + 1)) / (f . n) by A3
.= (Fib (n + 1)) / (Fib n) by A2 ;
hence F . n = ((f ^\ 1) /" f) . n by A1; :: thesis: verum
end;
hence F = (f ^\ 1) /" f by FUNCT_2:113; :: thesis: verum
end;
deffunc H1( Element of NAT ) -> Element of K45() = (tau to_power $1) / (sqrt 5);
ex g being Real_Sequence st
for n being Element of NAT holds g . n = H1(n) from SEQ_1:sch 1();
 then consider g being Real_Sequence such that
A5: for n being Element of NAT holds g . n = H1(n) ;
deffunc H2( Element of NAT ) -> Element of K45() = (tau_bar to_power $1) / (sqrt 5);
ex h being Real_Sequence st
for n being Element of NAT holds h . n = H2(n) from SEQ_1:sch 1();
 then consider h being Real_Sequence such that
A6: for n being Element of NAT holds h . n = H2(n) ;
A7: g = f + h
proof
A8: for n being Element of NAT holds f . n = (g . n) - (h . n)
proof
let n be Element of NAT ; :: thesis: f . n = (g . n) - (h . n)
f . n = Fib n by A2
.= ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) by Th7
.= ((tau to_power n) / (sqrt 5)) - ((tau_bar to_power n) / (sqrt 5))
.= (g . n) - ((tau_bar to_power n) / (sqrt 5)) by A5
.= (g . n) - (h . n) by A6 ;
hence f . n = (g . n) - (h . n) ; :: thesis: verum
end;
for n being Element of NAT holds g . n = (f . n) + (h . n)
proof
let n be Element of NAT ; :: thesis: g . n = (f . n) + (h . n)
f . n = (g . n) - (h . n) by A8;
hence g . n = (f . n) + (h . n) ; :: thesis: verum
end;
hence g = f + h by SEQ_1:11; :: thesis: verum
end;
A9: ( h /" f is convergent & lim (h /" f) = 0 )
proof
A10: h is bounded
proof
for n being Element of NAT holds abs (h . n) < 1
proof
let n be Element of NAT ; :: thesis: abs (h . n) < 1
h . n = (tau_bar to_power n) / (sqrt 5) by A6;
hence abs (h . n) < 1 by Lm16; :: thesis: verum
end;
hence h is bounded by SEQ_2:15; :: thesis: verum
end;
A11: ( f " is convergent & lim (f " ) = 0 )
proof
A12: for x being real number st 0 < x holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f " ) . m) - 0 ) < x
proof
let x be real number ; :: thesis: ( 0 < x implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f " ) . m) - 0 ) < x )
assume 0 < x ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f " ) . m) - 0 ) < x
then consider k being Element of NAT such that
A13: k > 0 and
0 < 1 / k and
A14: 1 / k <= x by Th3;
for m being Element of NAT st k + 2 <= m holds
abs (((f " ) . m) - 0 ) < x
proof
let m be Element of NAT ; :: thesis: ( k + 2 <= m implies abs (((f " ) . m) - 0 ) < x )
assume k + 2 <= m ; :: thesis: abs (((f " ) . m) - 0 ) < x
then A15: Fib (k + 2) <= Fib m by Lm5;
k + 2 = (k + 1) + 1 ;
then Fib (k + 2) >= k + 1 by Lm3;
then k + 1 <= Fib m by A15, XXREAL_0:2;
then A16: k + 1 <= f . m by A2;
0 < k + 1 by NAT_1:5;
then A17: 1 / (f . m) <= 1 / (k + 1) by A16, XREAL_1:87;
k + 0 < k + 1 by XREAL_1:8;
then A18: 1 / (k + 1) < 1 / k by A13, XREAL_1:90;
0 < f . m by A16, NAT_1:5, XXREAL_0:2;
then A19: 0 <= (f . m) " by XREAL_1:124;
A20: abs (((f " ) . m) - 0 ) = abs ((f . m) " ) by VALUED_1:10
.= (f . m) " by A19, ABSVALUE:def 1
.= 1 / (f . m) ;
1 / (f . m) < 1 / k by A17, A18, XXREAL_0:2;
hence abs (((f " ) . m) - 0 ) < x by A14, A20, XXREAL_0:2; :: thesis: verum
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f " ) . m) - 0 ) < x ; :: thesis: verum
end;
hence f " is convergent by SEQ_2:def 6; :: thesis: lim (f " ) = 0
hence lim (f " ) = 0 by A12, SEQ_2:def 7; :: thesis: verum
end;
hence h /" f is convergent by A10, SEQ_2:39; :: thesis: lim (h /" f) = 0
thus lim (h /" f) = 0 by A10, A11, SEQ_2:40; :: thesis: verum
end;
set f2 = f ^\ 2;
A21: ( f /" f is convergent & lim (f /" f) = 1 )
proof
A22: for n being Element of NAT holds (f ^\ 2) . n <> 0
proof
let n be Element of NAT ; :: thesis: (f ^\ 2) . n <> 0
(f ^\ 2) . n = f . (n + 2) by NAT_1:def 3
.= Fib ((n + 1) + 1) by A2 ;
hence (f ^\ 2) . n <> 0 by Lm3, NAT_1:5; :: thesis: verum
end;
A23: for n being Nat holds ((f ^\ 2) /" (f ^\ 2)) . n = 1
proof
let n be Nat; :: thesis: ((f ^\ 2) /" (f ^\ 2)) . n = 1
X: n in NAT by ORDINAL1:def 13;
then ((f ^\ 2) /" (f ^\ 2)) . n = ((f ^\ 2) . n) * (((f ^\ 2) . n) " ) by Th11
.= ((f ^\ 2) . n) * (1 / ((f ^\ 2) . n))
.= 1 by A22, X, XCMPLX_1:107 ;
hence ((f ^\ 2) /" (f ^\ 2)) . n = 1 ; :: thesis: verum
end;
then A24: (f ^\ 2) /" (f ^\ 2) is V8() by VALUED_0:def 18;
((f ^\ 2) /" (f ^\ 2)) . 0 = 1 by A23;
then A25: lim ((f ^\ 2) /" (f ^\ 2)) = 1 by A24, SEQ_4:40;
A26: (f /" f) ^\ 2 = (f ^\ 2) /" (f ^\ 2) by SEQM_3:43;
hence f /" f is convergent by A24, SEQ_4:35; :: thesis: lim (f /" f) = 1
thus lim (f /" f) = 1 by A24, A25, A26, SEQ_4:36; :: thesis: verum
end;
A27: g /" f = (f /" f) + (h /" f) by A7, SEQ_1:57;
then A28: g /" f is convergent by A9, A21, SEQ_2:19;
A29: lim (g /" f) = 1 + 0 by A9, A21, A27, SEQ_2:20
.= 1 ;
set g1 = g ^\ 1;
A30: g is non-zero
proof
for n being Element of NAT holds g . n <> 0
proof
let n be Element of NAT ; :: thesis: g . n <> 0
A31: g . n = (tau to_power n) / (sqrt 5) by A5
.= (tau to_power n) * ((sqrt 5) " )
.= (tau |^ n) * ((sqrt 5) " ) by POWER:46 ;
A32: tau |^ n <> 0 by Lm12, PREPOWER:12;
(sqrt 5) " <> 0 by SQUARE_1:85, SQUARE_1:95, XCMPLX_1:203;
hence g . n <> 0 by A31, A32, XCMPLX_1:6; :: thesis: verum
end;
hence g is non-zero by SEQ_1:7; :: thesis: verum
end;
A33: ( (g ^\ 1) /" g is convergent & lim ((g ^\ 1) /" g) = tau )
proof
Y: tau in REAL by XREAL_0:def 1;
A34: for n being Nat holds ((g ^\ 1) /" g) . n = tau
proof
let n be Nat; :: thesis: ((g ^\ 1) /" g) . n = tau
X: n in NAT by ORDINAL1:def 13;
then A35: g . n = (tau to_power n) / (sqrt 5) by A5
.= (tau to_power n) * ((sqrt 5) " )
.= (tau |^ n) * ((sqrt 5) " ) by POWER:46 ;
A36: (g ^\ 1) . n = g . (n + 1) by NAT_1:def 3
.= (tau to_power (n + 1)) / (sqrt 5) by A5
.= (tau to_power (n + 1)) * ((sqrt 5) " )
.= (tau |^ (n + 1)) * ((sqrt 5) " ) by POWER:46
.= (tau * (tau |^ n)) * ((sqrt 5) " ) by NEWTON:11
.= tau * (g . n) by A35 ;
A37: g . n <> 0 by A30, X, SEQ_1:7;
((g ^\ 1) /" g) . n = (tau * (g . n)) * ((g . n) " ) by A36, Th11, X
.= tau * ((g . n) * ((g . n) " ))
.= tau * 1 by A37, XCMPLX_0:def 7
.= tau ;
hence ((g ^\ 1) /" g) . n = tau ; :: thesis: verum
end;
then A38: (g ^\ 1) /" g is V8() by Y, VALUED_0:def 18;
hence (g ^\ 1) /" g is convergent ; :: thesis: lim ((g ^\ 1) /" g) = tau
((g ^\ 1) /" g) . 0 = tau by A34;
hence lim ((g ^\ 1) /" g) = tau by A38, SEQ_4:40; :: thesis: verum
end;
A39: f ^\ 1 is non-zero
proof
for n being Element of NAT holds (f ^\ 1) . n <> 0
proof
let n be Element of NAT ; :: thesis: (f ^\ 1) . n <> 0
(f ^\ 1) . n = f . (n + 1) by NAT_1:def 3
.= Fib (n + 1) by A2 ;
hence (f ^\ 1) . n <> 0 by Lm6; :: thesis: verum
end;
hence f ^\ 1 is non-zero by SEQ_1:7; :: thesis: verum
end;
A40: (f ^\ 1) ^\ 1 = f ^\ (1 + 1) by NAT_1:49
.= f ^\ 2 ;
set g2 = (g ^\ 1) ^\ 1;
A42: f ^\ 2 is non-zero by A39, A40;
A43: ( (f ^\ 2) /" (g ^\ 1) is convergent & lim ((f ^\ 2) /" (g ^\ 1)) = tau )
proof
A44: (f ^\ 2) /" (g ^\ 1) = ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) (#) (((g ^\ 1) ^\ 1) /" (g ^\ 1)) by A30, Th10;
A45: (g ^\ 1) ^\ 1 = g ^\ (1 + 1) by NAT_1:49;
A46: ( (f ^\ 2) /" ((g ^\ 1) ^\ 1) is convergent & lim ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) = 1 )
proof
A47: ((g ^\ 1) ^\ 1) /" (f ^\ 2) = (g /" f) ^\ 2 by A45, SEQM_3:43;
A49: lim (((g ^\ 1) ^\ 1) /" (f ^\ 2)) = 1 by A28, A29, A47, SEQ_4:33;
for n being Element of NAT holds (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0
proof
let n be Element of NAT ; :: thesis: (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0
A50: ((g ^\ 1) ^\ 1) . n <> 0 by A30, SEQ_1:7;
A51: ((f ^\ 2) . n) " <> 0 by A42, SEQ_1:7, XCMPLX_1:203;
(((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n = (((g ^\ 1) ^\ 1) . n) * (((f ^\ 2) . n) " ) by Th11;
hence (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0 by A50, A51, XCMPLX_1:6; :: thesis: verum
end;
then A52: ((g ^\ 1) ^\ 1) /" (f ^\ 2) is non-zero by SEQ_1:7;
then (((g ^\ 1) ^\ 1) /" (f ^\ 2)) " is convergent by A47, A28, A49, SEQ_2:35;
hence (f ^\ 2) /" ((g ^\ 1) ^\ 1) is convergent by SEQ_1:48; :: thesis: lim ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) = 1
lim ((((g ^\ 1) ^\ 1) /" (f ^\ 2)) " ) = 1 " by A47, A28, A49, A52, SEQ_2:36
.= 1 ;
hence lim ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) = 1 by SEQ_1:48; :: thesis: verum
end;
A53: ( ((g ^\ 1) ^\ 1) /" (g ^\ 1) is convergent & lim (((g ^\ 1) ^\ 1) /" (g ^\ 1)) = tau )
proof
((g ^\ 1) ^\ 1) /" (g ^\ 1) = ((g ^\ 1) /" g) ^\ 1 by SEQM_3:43;
hence ( ((g ^\ 1) ^\ 1) /" (g ^\ 1) is convergent & lim (((g ^\ 1) ^\ 1) /" (g ^\ 1)) = tau ) by A33, SEQ_4:33; :: thesis: verum
end;
hence (f ^\ 2) /" (g ^\ 1) is convergent by A44, A46, SEQ_2:28; :: thesis: lim ((f ^\ 2) /" (g ^\ 1)) = tau
lim ((f ^\ 2) /" (g ^\ 1)) = 1 * tau by A44, A46, A53, SEQ_2:29
.= tau ;
hence lim ((f ^\ 2) /" (g ^\ 1)) = tau ; :: thesis: verum
end;
A54: ( (g ^\ 1) /" (f ^\ 1) is convergent & lim ((g ^\ 1) /" (f ^\ 1)) = 1 )
proof
(g ^\ 1) /" (f ^\ 1) = (g /" f) ^\ 1 by SEQM_3:43;
hence ( (g ^\ 1) /" (f ^\ 1) is convergent & lim ((g ^\ 1) /" (f ^\ 1)) = 1 ) by A28, A29, SEQ_4:33; :: thesis: verum
end;
A55: ( (f ^\ 2) /" (f ^\ 1) is convergent & lim ((f ^\ 2) /" (f ^\ 1)) = tau )
proof
A56: (f ^\ 2) /" (f ^\ 1) = ((f ^\ 2) /" (g ^\ 1)) (#) ((g ^\ 1) /" (f ^\ 1)) by A30, Th10;
hence (f ^\ 2) /" (f ^\ 1) is convergent by A43, A54, SEQ_2:28; :: thesis: lim ((f ^\ 2) /" (f ^\ 1)) = tau
lim ((f ^\ 2) /" (f ^\ 1)) = tau * 1 by A43, A54, A56, SEQ_2:29;
hence lim ((f ^\ 2) /" (f ^\ 1)) = tau ; :: thesis: verum
end;
A57: (f ^\ 2) /" (f ^\ 1) = F ^\ 1 by A4, A40, SEQM_3:43;
hence F is convergent by A55, SEQ_4:35; :: thesis: lim F = tau
thus lim F = tau by A55, A57, SEQ_4:36; :: thesis: verum