let r be real number ; :: thesis: ( ( for n being Nat holds (scf r) . n <> 0 ) implies for n being Nat holds (c_d r) . (n + 1) >= tau |^ n )
assume A1:
for n being Nat holds (scf r) . n <> 0
; :: thesis: for n being Nat holds (c_d r) . (n + 1) >= tau |^ n
set s2 = c_d r;
set s = scf r;
defpred S2[ Nat] means (c_d r) . ($1 + 1) >= tau |^ $1;
A2:
(scf r) . 1 >= 1
by A1, Th40;
then
(c_d r) . (0 + 1) >= 1
by Def7;
then A3:
S2[ 0 ]
by NEWTON:9;
A4: (c_d r) . (1 + 1) =
(((scf r) . (0 + 2)) * ((c_d r) . (0 + 1))) + ((c_d r) . 0 )
by Def7
.=
(((scf r) . 2) * ((c_d r) . 1)) + 1
by Def7
.=
(((scf r) . 2) * ((scf r) . 1)) + 1
by Def7
;
(scf r) . 2 >= 1
by A1, Th40;
then
((scf r) . 2) * ((scf r) . 1) >= 1
by A2, XREAL_1:161;
then A5:
(((scf r) . 2) * ((scf r) . 1)) + 1 >= 1 + 1
by XREAL_1:8;
A6:
((1 + (sqrt 5)) / 2) |^ 1 = (1 + (sqrt 5)) / 2
by NEWTON:10;
sqrt 5 < sqrt (3 ^2 )
by SQUARE_1:95;
then
sqrt 5 < 3
by SQUARE_1:89;
then
1 + (sqrt 5) < 1 + 3
by XREAL_1:10;
then
(1 + (sqrt 5)) / 2 < 4 / 2
by XREAL_1:76;
then A7:
S2[1]
by A4, A5, A6, FIB_NUM:def 1, XXREAL_0:2;
A8:
for n being Nat st S2[n] & S2[n + 1] holds
S2[n + 2]
proof
let n be
Nat;
:: thesis: ( S2[n] & S2[n + 1] implies S2[n + 2] )
assume that A9:
(c_d r) . (n + 1) >= tau |^ n
and A10:
(c_d r) . ((n + 1) + 1) >= tau |^ (n + 1)
;
:: thesis: S2[n + 2]
sqrt 5
>= 0
by SQUARE_1:def 4;
then
1
+ (sqrt 5) > 0 + 0
;
then
(1 + (sqrt 5)) / 2
> 0
by XREAL_1:141;
then A11:
tau |^ (n + 1) > 0
by FIB_NUM:def 1, PREPOWER:13;
A12:
(c_d r) . ((n + 2) + 1) =
(((scf r) . ((n + 1) + 2)) * ((c_d r) . ((n + 1) + 1))) + ((c_d r) . (n + 1))
by Def7
.=
(((scf r) . (n + 3)) * ((c_d r) . ((n + 1) + 1))) + ((c_d r) . (n + 1))
;
n + 3
>= 0 + 1
by XREAL_1:9;
then
(scf r) . (n + 3) >= 1
by A1, Th40;
then A13:
((scf r) . (n + 3)) * ((c_d r) . ((n + 1) + 1)) >= 1
* (tau |^ (n + 1))
by A10, A11, XREAL_1:68;
A14:
(tau |^ (n + 1)) + (tau |^ n) =
((((1 + (sqrt 5)) / 2) |^ n) * ((1 + (sqrt 5)) / 2)) + (((1 + (sqrt 5)) / 2) |^ n)
by FIB_NUM:def 1, NEWTON:11
.=
(((1 + (sqrt 5)) / 2) |^ n) * ((6 + (2 * (sqrt 5))) / 4)
;
tau |^ (n + 2) =
(((1 + (sqrt 5)) / 2) |^ n) * (((1 + (sqrt 5)) / 2) |^ 2)
by FIB_NUM:def 1, NEWTON:13
.=
(((1 + (sqrt 5)) / 2) |^ n) * (((1 + (sqrt 5)) / 2) ^2 )
by WSIERP_1:2
.=
(((1 + (sqrt 5)) / 2) |^ n) * ((((1 ^2 ) + ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2 )) / 4)
.=
(((1 + (sqrt 5)) / 2) |^ n) * (((1 + (2 * (sqrt 5))) + 5) / 4)
by SQUARE_1:def 4
.=
(((1 + (sqrt 5)) / 2) |^ n) * ((6 + (2 * (sqrt 5))) / 4)
;
hence
S2[
n + 2]
by A9, A12, A13, A14, XREAL_1:9;
:: thesis: verum
end;
A15:
for n being Nat holds S2[n]
from FIB_NUM:sch 1(A3, A7, A8);
let n be Nat; :: thesis: (c_d r) . (n + 1) >= tau |^ n
thus
(c_d r) . (n + 1) >= tau |^ n
by A15; :: thesis: verum