deffunc H1( Nat) -> set = () / (sqrt 5);
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 ) )
consider f being Real_Sequence such that
A1: for n being Nat holds f . n = Fib n from SEQ_1:sch 1();
set f2 = f ^\ 2;
set f1 = f ^\ 1;
A2: (f ^\ 1) ^\ 1 = f ^\ (1 + 1) by NAT_1:48
.= f ^\ 2 ;
A3: 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 A1 ;
hence (f ^\ 2) . n <> 0 by Lm3; :: thesis: verum
end;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
A4: for n being Nat holds ((f ^\ 2) /" (f ^\ 2)) . n = jj
proof
let n be Nat; :: thesis: ((f ^\ 2) /" (f ^\ 2)) . n = jj
A5: n in NAT by ORDINAL1:def 12;
then ((f ^\ 2) /" (f ^\ 2)) . n = ((f ^\ 2) . n) * (((f ^\ 2) . n) ") by Th10
.= ((f ^\ 2) . n) * (1 / ((f ^\ 2) . n))
.= 1 by ;
hence ((f ^\ 2) /" (f ^\ 2)) . n = jj ; :: thesis: verum
end;
then A6: (f ^\ 2) /" (f ^\ 2) is constant by VALUED_0:def 18;
A7: (f /" f) ^\ 2 = (f ^\ 2) /" (f ^\ 2) by SEQM_3:20;
then A8: f /" f is convergent by ;
((f ^\ 2) /" (f ^\ 2)) . 0 = 1 by A4;
then lim ((f ^\ 2) /" (f ^\ 2)) = 1 by ;
then A9: lim (f /" f) = 1 by ;
ex g being Real_Sequence st
for n being Nat holds g . n = H1(n) from SEQ_1:sch 1();
then consider g being Real_Sequence such that
A10: for n being Nat holds g . n = H1(n) ;
set g1 = g ^\ 1;
A11: for n being Nat holds g . n <> 0
proof
let n be Nat; :: thesis: g . n <> 0
A12: (sqrt 5) " <> 0 by ;
A13: tau |^ n <> 0 by ;
g . n = () / (sqrt 5) by A10
.= () * ((sqrt 5) ")
.= () * ((sqrt 5) ") by POWER:41 ;
hence g . n <> 0 by ; :: thesis: verum
end;
then A14: g is non-zero by SEQ_1:5;
A15: (f ^\ 2) /" (f ^\ 1) = ((f ^\ 2) /" (g ^\ 1)) (#) ((g ^\ 1) /" (f ^\ 1)) by ;
set g2 = (g ^\ 1) ^\ 1;
for n being Nat holds (f ^\ 1) . n <> 0
proof
let n be Nat; :: thesis: (f ^\ 1) . n <> 0
A16: n in NAT by ORDINAL1:def 12;
(f ^\ 1) . n = f . (n + 1) by NAT_1:def 3
.= Fib (n + 1) by A1 ;
hence (f ^\ 1) . n <> 0 by ; :: thesis: verum
end;
then A17: f ^\ 1 is non-zero by SEQ_1:5;
for n being Nat holds (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0
proof
let n be Nat; :: thesis: (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0
A18: n in NAT by ORDINAL1:def 12;
A19: ((g ^\ 1) ^\ 1) . n <> 0 by ;
A20: (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n = (((g ^\ 1) ^\ 1) . n) * (((f ^\ 2) . n) ") by ;
((f ^\ 2) . n) " <> 0 by ;
hence (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0 by ; :: thesis: verum
end;
then A21: ((g ^\ 1) ^\ 1) /" (f ^\ 2) is non-zero by SEQ_1:5;
(g ^\ 1) ^\ 1 = g ^\ (1 + 1) by NAT_1:48;
then A22: ((g ^\ 1) ^\ 1) /" (f ^\ 2) = (g /" f) ^\ 2 by SEQM_3:20;
A23: 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 A1 ;
hence (f ^\ 1) . n = Fib (n + 1) ; :: thesis: verum
end;
assume A24: for n being Element of NAT holds F . n = (Fib (n + 1)) / (Fib n) ; :: thesis: ( F is convergent & lim F = tau )
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 Th10
.= (Fib (n + 1)) / (f . n) by A23
.= (Fib (n + 1)) / (Fib n) by A1 ;
hence F . n = ((f ^\ 1) /" f) . n by A24; :: thesis: verum
end;
then F = (f ^\ 1) /" f by FUNCT_2:63;
then A25: (f ^\ 2) /" (f ^\ 1) = F ^\ 1 by ;
A26: ((g ^\ 1) ^\ 1) /" (g ^\ 1) = ((g ^\ 1) /" g) ^\ 1 by SEQM_3:20;
A27: for n being Nat holds ((g ^\ 1) /" g) . n = tau
proof
let n be Nat; :: thesis: ((g ^\ 1) /" g) . n = tau
A28: n in NAT by ORDINAL1:def 12;
A29: g . n = () / (sqrt 5) by A10
.= () * ((sqrt 5) ")
.= () * ((sqrt 5) ") by POWER:41 ;
A30: g . n <> 0 by A11;
(g ^\ 1) . n = g . (n + 1) by NAT_1:def 3
.= (tau to_power (n + 1)) / (sqrt 5) by A10
.= (tau to_power (n + 1)) * ((sqrt 5) ")
.= (tau |^ (n + 1)) * ((sqrt 5) ") by POWER:41
.= (tau * ()) * ((sqrt 5) ") by NEWTON:6
.= tau * (g . n) by A29 ;
then ((g ^\ 1) /" g) . n = (tau * (g . n)) * ((g . n) ") by
.= tau * ((g . n) * ((g . n) "))
.= tau * 1 by
.= tau ;
hence ((g ^\ 1) /" g) . n = tau ; :: thesis: verum
end;
tau in REAL by XREAL_0:def 1;
then A31: (g ^\ 1) /" g is constant by ;
A32: for x being Real st 0 < x holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((f ") . m) - 0).| < x
proof
let x be Real; :: thesis: ( 0 < x implies ex n being Nat st
for m being Nat st n <= m holds
|.(((f ") . m) - 0).| < x )

assume 0 < x ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((f ") . m) - 0).| < x

then consider k being Element of NAT such that
A33: k > 0 and
0 < 1 / k and
A34: 1 / k <= x by Th3;
for m being Nat st k + 2 <= m holds
|.(((f ") . m) - 0).| < x
proof
let m be Nat; :: thesis: ( k + 2 <= m implies |.(((f ") . m) - 0).| < x )
A35: m in NAT by ORDINAL1:def 12;
k + 2 = (k + 1) + 1 ;
then A36: Fib (k + 2) >= k + 1 by Lm3;
assume k + 2 <= m ; :: thesis: |.(((f ") . m) - 0).| < x
then Fib (k + 2) <= Fib m by ;
then k + 1 <= Fib m by ;
then A37: k + 1 <= f . m by A1;
then 0 < f . m ;
then A38: 0 <= (f . m) " ;
k + 0 < k + 1 by XREAL_1:6;
then A39: 1 / (k + 1) < 1 / k by ;
A40: |.(((f ") . m) - 0).| = |.((f . m) ").| by VALUED_1:10
.= (f . m) " by
.= 1 / (f . m) ;
1 / (f . m) <= 1 / (k + 1) by ;
then 1 / (f . m) < 1 / k by ;
hence |.(((f ") . m) - 0).| < x by ; :: thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
|.(((f ") . m) - 0).| < x ; :: thesis: verum
end;
then A41: f " is convergent by SEQ_2:def 6;
then A42: lim (f ") = 0 by ;
deffunc H2( Nat) -> set = () / (sqrt 5);
ex h being Real_Sequence st
for n being Nat holds h . n = H2(n) from SEQ_1:sch 1();
then consider h being Real_Sequence such that
A43: for n being Nat holds h . n = H2(n) ;
A44: 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 A1
.= (() - ()) / (sqrt 5) by Th7
.= (() / (sqrt 5)) - (() / (sqrt 5))
.= (g . n) - (() / (sqrt 5)) by A10
.= (g . n) - (h . n) by A43 ;
hence f . n = (g . n) - (h . n) ; :: thesis: verum
end;
for n being Nat holds g . n = (f . n) + (h . n)
proof
let n be Nat; :: thesis: g . n = (f . n) + (h . n)
A45: n in NAT by ORDINAL1:def 12;
f . n = (g . n) - (h . n) by ;
hence g . n = (f . n) + (h . n) ; :: thesis: verum
end;
then g = f + h by SEQ_1:7;
then A46: g /" f = (f /" f) + (h /" f) by SEQ_1:49;
for n being Nat holds |.(h . n).| < 1
proof
let n be Nat; :: thesis: |.(h . n).| < 1
A47: n in NAT by ORDINAL1:def 12;
h . n = () / (sqrt 5) by A43;
hence |.(h . n).| < 1 by ; :: thesis: verum
end;
then A48: h is bounded by SEQ_2:3;
f " is convergent by ;
then A49: h /" f is convergent by ;
then A50: g /" f is convergent by ;
((g ^\ 1) /" g) . 0 = tau by A27;
then lim ((g ^\ 1) /" g) = tau by ;
then A51: lim (((g ^\ 1) ^\ 1) /" (g ^\ 1)) = tau by ;
A52: (g ^\ 1) /" (f ^\ 1) = (g /" f) ^\ 1 by SEQM_3:20;
lim (h /" f) = 0 by ;
then A53: lim (g /" f) = 1 + 0 by
.= 1 ;
then A54: lim (((g ^\ 1) ^\ 1) /" (f ^\ 2)) = 1 by ;
then (((g ^\ 1) ^\ 1) /" (f ^\ 2)) " is convergent by ;
then A55: (f ^\ 2) /" ((g ^\ 1) ^\ 1) is convergent by SEQ_1:40;
A56: (f ^\ 2) /" (g ^\ 1) = ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) (#) (((g ^\ 1) ^\ 1) /" (g ^\ 1)) by ;
then A57: (f ^\ 2) /" (g ^\ 1) is convergent by ;
then A58: (f ^\ 2) /" (f ^\ 1) is convergent by ;
hence F is convergent by ; :: thesis:
lim ((((g ^\ 1) ^\ 1) /" (f ^\ 2)) ") = 1 " by
.= 1 ;
then lim ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) = 1 by SEQ_1:40;
then A59: lim ((f ^\ 2) /" (g ^\ 1)) = 1 * tau by
.= tau ;
lim ((g ^\ 1) /" (f ^\ 1)) = 1 by ;
then lim ((f ^\ 2) /" (f ^\ 1)) = tau * 1 by ;
hence lim F = tau by ; :: thesis: verum