deffunc H1( Nat) -> set = (tau to_power $1) / (sqrt 5);
let F be Real_Sequence; ( ( 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
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
A4:
for n being Nat holds ((f ^\ 2) /" (f ^\ 2)) . n = jj
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 A6, SEQ_4:21;
((f ^\ 2) /" (f ^\ 2)) . 0 = 1
by A4;
then
lim ((f ^\ 2) /" (f ^\ 2)) = 1
by A6, SEQ_4:25;
then A9:
lim (f /" f) = 1
by A6, A7, SEQ_4:22;
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
then A14:
g is non-zero
by SEQ_1:5;
A15:
(f ^\ 2) /" (f ^\ 1) = ((f ^\ 2) /" (g ^\ 1)) (#) ((g ^\ 1) /" (f ^\ 1))
by Th9, A14;
set g2 = (g ^\ 1) ^\ 1;
for n being Nat holds (f ^\ 1) . n <> 0
then A17:
f ^\ 1 is non-zero
by SEQ_1:5;
for n being Nat holds (((g ^\ 1) ^\ 1) /" (f ^\ 2)) . n <> 0
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)
assume A24:
for n being Element of NAT holds F . n = (Fib (n + 1)) / (Fib n)
; ( F is convergent & lim F = tau )
for n being Element of NAT holds F . n = ((f ^\ 1) /" f) . n
then
F = (f ^\ 1) /" f
by FUNCT_2:63;
then A25:
(f ^\ 2) /" (f ^\ 1) = F ^\ 1
by A2, SEQM_3:20;
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
tau in REAL
by XREAL_0:def 1;
then A31:
(g ^\ 1) /" g is constant
by A27, VALUED_0:def 18;
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
then A41:
f " is convergent
by SEQ_2:def 6;
then A42:
lim (f ") = 0
by A32, SEQ_2:def 7;
deffunc H2( Nat) -> set = (tau_bar to_power $1) / (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)
for n being Nat holds g . n = (f . n) + (h . n)
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
then A48:
h is bounded
by SEQ_2:3;
f " is convergent
by A32, SEQ_2:def 6;
then A49:
h /" f is convergent
by A48, A42, SEQ_2:25;
then A50:
g /" f is convergent
by A8, A46;
((g ^\ 1) /" g) . 0 = tau
by A27;
then
lim ((g ^\ 1) /" g) = tau
by A31, SEQ_4:25;
then A51:
lim (((g ^\ 1) ^\ 1) /" (g ^\ 1)) = tau
by A31, A26, SEQ_4:20;
A52:
(g ^\ 1) /" (f ^\ 1) = (g /" f) ^\ 1
by SEQM_3:20;
lim (h /" f) = 0
by A48, A41, A42, SEQ_2:26;
then A53: lim (g /" f) =
1 + 0
by A49, A8, A9, A46, SEQ_2:6
.=
1
;
then A54:
lim (((g ^\ 1) ^\ 1) /" (f ^\ 2)) = 1
by A50, A22, SEQ_4:20;
then
(((g ^\ 1) ^\ 1) /" (f ^\ 2)) " is convergent
by A50, A22, A21, SEQ_2:21;
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 A14, Th9;
then A57:
(f ^\ 2) /" (g ^\ 1) is convergent
by A31, A55, A26;
then A58:
(f ^\ 2) /" (f ^\ 1) is convergent
by A50, A52, A15;
hence
F is convergent
by A25, SEQ_4:21; lim F = tau
lim ((((g ^\ 1) ^\ 1) /" (f ^\ 2)) ") =
1 "
by A50, A22, A54, A21, SEQ_2:22
.=
1
;
then
lim ((f ^\ 2) /" ((g ^\ 1) ^\ 1)) = 1
by SEQ_1:40;
then A59: lim ((f ^\ 2) /" (g ^\ 1)) =
1 * tau
by A31, A56, A55, A26, A51, SEQ_2:15
.=
tau
;
lim ((g ^\ 1) /" (f ^\ 1)) = 1
by A50, A53, A52, SEQ_4:20;
then
lim ((f ^\ 2) /" (f ^\ 1)) = tau * 1
by A50, A59, A57, A52, A15, SEQ_2:15;
hence
lim F = tau
by A58, A25, SEQ_4:22; verum