let n be Nat; :: thesis: ( n >= 2 implies Fib (n + 1) = [\((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1))) / 2)/] )
assume A1: n >= 2 ; :: thesis: 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

proof

per cases ( n is even or n is odd ) ;

suppose n is even ; :: thesis: 1 >= (- 1) to_power n

hence 1 >= (- 1) to_power n by FIB_NUM2:3; :: thesis: verum

end;

suppose n is odd ; :: thesis: 1 >= (- 1) to_power n

hence 1 >= (- 1) to_power n by FIB_NUM2:2; :: thesis: verum

end;

end;

end;

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)))

proof

A18: Fib n > 0 by A1, FIB_NUM2:21, FIB_NUM2:45;
Lucas n >= n by FIB_NUM3:17;
then Lucas n >= 2 by A1, XXREAL_0:2;
then (Lucas n) + (Fib n) > 0 + 2 by A18, XREAL_1:8;
then ((Lucas n) + (Fib n)) * 2 > 2 * 2 by XREAL_1:68;
then A19: - (((Lucas n) + (Fib n)) * 2) < - 4 by XREAL_1:24;
- 4 <= 4 * ((- 1) to_power n) by Lm1;
hence ((Lucas n) ^2) - (5 * ((Fib n) ^2)) > - (2 * ((Lucas n) + (Fib n))) by A6, A19, XXREAL_0:2; :: thesis: verum

end;

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; :: thesis: verum