let n be Nat; ( n >= 2 implies Fib (n + 1) = [\((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1))) / 2)/] )
assume A1:
n >= 2
; Fib (n + 1) = [\((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1))) / 2)/]
A2:
n - 0 is Element of NAT
by NAT_1:21;
A3:
n - 1 >= 2 - 1
by A1, XREAL_1:9;
((n + 1) -' 1) + 1 =
((n + 1) - 1) + 1
by NAT_D:37
.=
((n - 1) + 1) + 1
.=
((n -' 1) + 1) + 1
by A3, NAT_D:39
;
then A4: Fib (n + 1) =
Fib (((n -' 1) + 1) + 1)
by NAT_D:34
.=
(Fib (n -' 1)) + (Fib ((n -' 1) + 1))
by PRE_FF:1
.=
(Fib (n -' 1)) + (Fib ((n + 1) -' 1))
by A1, NAT_D:38, XXREAL_0:2
.=
(Fib (n -' 1)) + (Fib n)
by NAT_D:34
;
n + 2 >= 2 + 2
by A1, XREAL_1:6;
then reconsider p = (n + 2) - 1 as Nat by NAT_1:21, XXREAL_0:2;
A5: (Lucas n) - (Fib n) =
(Lucas ((n + 1) -' 1)) - (Fib n)
by NAT_D:34
.=
(Lucas ((n -' 1) + 1)) - (Fib n)
by A1, NAT_D:38, XXREAL_0:2
.=
((Fib (n -' 1)) + (Fib ((n -' 1) + 2))) - (Fib n)
by FIB_NUM3:20
.=
((Fib (n -' 1)) + (Fib ((n + 2) -' 1))) - (Fib n)
by A1, NAT_D:38, XXREAL_0:2
.=
((Fib (n -' 1)) + (Fib p)) - (Fib n)
by NAT_D:37
.=
2 * (Fib (n -' 1))
by A4
;
A6: ((Lucas n) ^2) - (5 * ((Fib n) ^2)) =
((Lucas n) ^2) - (5 * ((Fib n) to_power 2))
by POWER:46
.=
((Lucas n) to_power 2) - (5 * ((Fib n) |^ 2))
by POWER:46
.=
(- 1) * ((5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2))
.=
(- 1) * (4 * ((- 1) to_power (n + 1)))
by A2, FIB_NUM3:30
.=
4 * ((- 1) * ((- 1) to_power (n + 1)))
.=
4 * (((- 1) to_power 1) * ((- 1) to_power (n + 1)))
.=
4 * ((- 1) to_power (1 + (n + 1)))
by Th2
.=
4 * ((- 1) to_power (n + 2))
.=
4 * (((- 1) to_power n) * ((- 1) to_power 2))
by Th2
.=
4 * (((- 1) to_power n) * ((- 1) ^2))
by POWER:46
.=
4 * ((- 1) to_power n)
;
( n -' 1 >= 2 -' 1 & 2 - 1 >= 1 )
by A1, NAT_D:42;
then
n -' 1 >= 2 - 1
by NAT_D:39;
then A7:
Fib (n -' 1) >= 1
by FIB_NUM2:45, PRE_FF:1;
1 >= (- 1) to_power n
then
(- 1) to_power n <= Fib (n -' 1)
by A7, XXREAL_0:2;
then
((Lucas n) ^2) - (5 * ((Fib n) ^2)) <= (2 * 2) * (Fib (n -' 1))
by A6, XREAL_1:64;
then
(((Lucas n) ^2) - (5 * ((Fib n) ^2))) - (2 * (Lucas n)) <= ((2 * (Lucas n)) - (2 * (Fib n))) - (2 * (Lucas n))
by A5, XREAL_1:9;
then
((((Lucas n) ^2) - (5 * ((Fib n) ^2))) - (2 * (Lucas n))) + 1 <= (- (2 * (Fib n))) + 1
by XREAL_1:6;
then A8:
(((((Lucas n) ^2) - (5 * ((Fib n) ^2))) - (2 * (Lucas n))) + 1) + (5 * ((Fib n) ^2)) <= ((- (2 * (Fib n))) + 1) + (5 * ((Fib n) ^2))
by XREAL_1:6;
A9: (n + 2) -' 1 =
(n + 2) - 1
by NAT_D:37
.=
n + 1
;
A10: Lucas n =
Lucas ((n + 1) -' 1)
by NAT_D:34
.=
Lucas ((n -' 1) + 1)
by A1, NAT_D:38, XXREAL_0:2
.=
(Fib (n -' 1)) + (Fib ((n -' 1) + 2))
by FIB_NUM3:20
.=
(Fib (n -' 1)) + (Fib ((n + 2) -' 1))
by A1, NAT_D:38, XXREAL_0:2
.=
(2 * (Fib (n + 1))) - (Fib n)
by A4, A9
;
A11:
2 * (Fib (n -' 1)) >= 2 * 0
;
n >= 1
by A1, XXREAL_0:2;
then A12:
Fib n >= 1
by FIB_NUM2:45, PRE_FF:1;
then
- (Fib n) <= - 1
by XREAL_1:24;
then
(- (Fib n)) + 1 <= (- 1) + 1
by XREAL_1:6;
then
(2 * (Fib (n -' 1))) + (Fib n) >= ((- (Fib n)) + 1) + (Fib n)
by A11, XREAL_1:6;
then A13:
((2 * (Fib (n -' 1))) + (Fib n)) - 1 >= 1 - 1
by XREAL_1:9;
sqrt ((((2 * (Fib (n + 1))) - (Fib n)) - 1) ^2) <= sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1)
by A10, A8, SQUARE_1:26;
then
((2 * (Fib (n + 1))) - (Fib n)) - 1 <= sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1)
by A4, A13, SQUARE_1:22;
then
(((2 * (Fib (n + 1))) - (Fib n)) - 1) + (Fib n) <= (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1)) + (Fib n)
by XREAL_1:6;
then
((((2 * (Fib (n + 1))) - (Fib n)) - 1) + (Fib n)) + 1 <= ((sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1)) + (Fib n)) + 1
by XREAL_1:6;
then A14:
(2 * (Fib (n + 1))) / 2 <= (((sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1)) + (Fib n)) + 1) / 2
by XREAL_1:72;
A15:
(5 * ((Fib n) ^2)) - (2 * (Fib n)) = ((5 * (Fib n)) - 2) * (Fib n)
;
5 * (Fib n) >= 5 * 1
by A12, XREAL_1:64;
then
(5 * (Fib n)) - 2 >= 5 - 2
by XREAL_1:9;
then A16:
(5 * (Fib n)) - 2 >= 0
by XXREAL_0:2;
A17:
(((Fib (n + 1)) + (Fib (n + 1))) - (Fib n)) + 1 = ((Fib (n + 1)) + (Fib (n -' 1))) + 1
by A4;
((Lucas n) ^2) - (5 * ((Fib n) ^2)) > - (2 * ((Lucas n) + (Fib n)))
then
(((Lucas n) ^2) - (5 * ((Fib n) ^2))) + (2 * (Lucas n)) > (- (2 * ((Lucas n) + (Fib n)))) + (2 * (Lucas n))
by XREAL_1:6;
then
((((Lucas n) ^2) - (5 * ((Fib n) ^2))) + (2 * (Lucas n))) + (5 * ((Fib n) ^2)) > (- (2 * (Fib n))) + (5 * ((Fib n) ^2))
by XREAL_1:6;
then
(((Lucas n) ^2) + ((2 * (Lucas n)) * 1)) + (1 ^2) > ((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + (1 ^2)
by XREAL_1:6;
then
sqrt ((((2 * (Fib (n + 1))) - (Fib n)) + 1) ^2) > sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1)
by A16, A15, A10, SQUARE_1:27;
then
((2 * (Fib (n + 1))) - (Fib n)) + 1 > sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1)
by A17, SQUARE_1:22;
then
(((2 * (Fib (n + 1))) - (Fib n)) + 1) - 1 > (sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1)) - 1
by XREAL_1:9;
then
((2 * (Fib (n + 1))) - (Fib n)) + (Fib n) > ((sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1)) - 1) + (Fib n)
by XREAL_1:6;
then
(2 * (Fib (n + 1))) / 2 > (((sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1)) - 1) + (Fib n)) / 2
by XREAL_1:74;
then
((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1))) / 2) - 1 < Fib (n + 1)
;
hence
Fib (n + 1) = [\((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1))) / 2)/]
by A14, INT_1:def 6; verum