let a be Nat; for r being Real st a > 0 & ( for n being Nat holds (scf r) . n >= a ) holds
for n being Nat holds (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n
let r be Real; ( a > 0 & ( for n being Nat holds (scf r) . n >= a ) implies for n being Nat holds (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n )
assume that
A1:
a > 0
and
A2:
for n being Nat holds (scf r) . n >= a
; for n being Nat holds (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n
set s = scf r;
set s2 = c_d r;
defpred S2[ Nat] means (c_d r) . ($1 + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ $1;
A3:
(scf r) . 1 > 0
by A1, A2;
then
(scf r) . 1 >= 1
by Th40;
then
(c_d r) . (0 + 1) >= 1
by Def6;
then A4:
S2[ 0 ]
by NEWTON:4;
(scf r) . 2 > 0
by A1, A2;
then
((scf r) . 2) * ((scf r) . 1) >= 1 * ((scf r) . 1)
by A3, Th40, XREAL_1:64;
then A5:
(((scf r) . 2) * ((scf r) . 1)) + 1 >= ((scf r) . 1) + 1
by XREAL_1:6;
(scf r) . 1 >= a
by A2;
then
((scf r) . 1) + 1 >= a + 1
by XREAL_1:6;
then A6:
(((scf r) . 2) * ((scf r) . 1)) + 1 >= a + 1
by A5, XXREAL_0:2;
4 * a > 0
by A1, XREAL_1:129;
then
(a ^2) + 4 < ((a ^2) + 4) + (4 * a)
by XREAL_1:39;
then
sqrt ((a ^2) + 4) < sqrt ((a + 2) ^2)
by SQUARE_1:27;
then
sqrt ((a ^2) + 4) < a + 2
by SQUARE_1:22;
then
a + (sqrt ((a ^2) + 4)) < a + (a + 2)
by XREAL_1:8;
then A7:
( ((a + (sqrt ((a ^2) + 4))) / 2) |^ 1 = (a + (sqrt ((a ^2) + 4))) / 2 & (a + (sqrt ((a ^2) + 4))) / 2 < ((2 * a) + (2 * 1)) / 2 )
by XREAL_1:74;
let n be Nat; (c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n
A8:
for n being Nat st S2[n] & S2[n + 1] holds
S2[n + 2]
(c_d r) . (1 + 1) =
(((scf r) . (0 + 2)) * ((c_d r) . (0 + 1))) + ((c_d r) . 0)
by Def6
.=
(((scf r) . 2) * ((c_d r) . 1)) + 1
by Def6
.=
(((scf r) . 2) * ((scf r) . 1)) + 1
by Def6
;
then A15:
S2[1]
by A6, A7, XXREAL_0:2;
for n being Nat holds S2[n]
from FIB_NUM:sch 1(A4, A15, A8);
hence
(c_d r) . (n + 1) >= ((a + (sqrt ((a ^2) + 4))) / 2) |^ n
; verum