let n be natural number ; :: thesis: ( n >= 2 implies Fib (n + 1) = [\((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1))) / 2)/] )
assume A0: n >= 2 ; :: thesis: Fib (n + 1) = [\((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1))) / 2)/]
aa: n - 0 is Element of NAT by NAT_1:21;
z1: n - 1 >= 2 - 1 by A0, XREAL_1:11;
((n + 1) -' 1) + 1 = ((n + 1) - 1) + 1 by NAT_D:37
.= ((n - 1) + 1) + 1
.= ((n -' 1) + 1) + 1 by z1, NAT_D:39 ;
then a1: 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 A0, NAT_D:38, XXREAL_0:2
.= (Fib (n -' 1)) + (Fib n) by NAT_D:34 ;
n + 2 >= 2 + 2 by A0, XREAL_1:8;
then reconsider p = (n + 2) - 1 as natural number by NAT_1:21, XXREAL_0:2;
A1: (Lucas n) - (Fib n) = (Lucas ((n + 1) -' 1)) - (Fib n) by NAT_D:34
.= (Lucas ((n -' 1) + 1)) - (Fib n) by A0, 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 A0, NAT_D:38, XXREAL_0:2
.= ((Fib (n -' 1)) + (Fib p)) - (Fib n) by NAT_D:37
.= 2 * (Fib (n -' 1)) by a1 ;
A2: ((Lucas n) ^2) - (5 * ((Fib n) ^2)) = ((Lucas n) ^2) - (5 * ((Fib n) to_power 2)) by POWER:53
.= ((Lucas n) to_power 2) - (5 * ((Fib n) |^ 2)) by POWER:53
.= (- 1) * ((5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2))
.= (- 1) * (4 * ((- 1) to_power (n + 1))) by aa, FIB_NUM3:30
.= 4 * ((- 1) * ((- 1) to_power (n + 1)))
.= 4 * (((- 1) to_power 1) * ((- 1) to_power (n + 1))) by POWER:30
.= 4 * ((- 1) to_power (1 + (n + 1))) by JakPower32
.= 4 * ((- 1) to_power (n + 2))
.= 4 * (((- 1) to_power n) * ((- 1) to_power 2)) by JakPower32
.= 4 * (((- 1) to_power n) * ((- 1) ^2)) by POWER:53
.= 4 * ((- 1) to_power n) ;
( n -' 1 >= 2 -' 1 & 2 - 1 >= 1 ) by A0, NAT_D:42;
then n -' 1 >= 2 - 1 by NAT_D:39;
then d1: Fib (n -' 1) >= 1 by FIB_NUM2:47, PRE_FF:1;
1 >= (- 1) to_power n

proof

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

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

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

end;

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

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

end;

end;

end;

then (- 1) to_power n <= Fib (n -' 1) by d1, XXREAL_0:2;
then ((Lucas n) ^2) - (5 * ((Fib n) ^2)) <= (2 * 2) * (Fib (n -' 1)) by A2, XREAL_1:66;
then (((Lucas n) ^2) - (5 * ((Fib n) ^2))) - (2 * (Lucas n)) <= ((2 * (Lucas n)) - (2 * (Fib n))) - (2 * (Lucas n)) by A1, XREAL_1:11;
then ((((Lucas n) ^2) - (5 * ((Fib n) ^2))) - (2 * (Lucas n))) + 1 <= (- (2 * (Fib n))) + 1 by XREAL_1:8;
then a6: (((((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:8;
v1: (n + 2) -' 1 = (n + 2) - 1 by NAT_D:37
.= n + 1 ;
w1: Lucas n = Lucas ((n + 1) -' 1) by NAT_D:34
.= Lucas ((n -' 1) + 1) by A0, 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 A0, NAT_D:38, XXREAL_0:2
.= (2 * (Fib (n + 1))) - (Fib n) by a1, v1 ;
x1: 2 * (Fib (n -' 1)) >= 2 * 0 ;
n >= 1 by A0, XXREAL_0:2;
then pp: Fib n >= 1 by FIB_NUM2:47, PRE_FF:1;
then - (Fib n) <= - 1 by XREAL_1:26;
then (- (Fib n)) + 1 <= (- 1) + 1 by XREAL_1:8;
then (2 * (Fib (n -' 1))) + (Fib n) >= ((- (Fib n)) + 1) + (Fib n) by x1, XREAL_1:8;
then v3: ((2 * (Fib (n -' 1))) + (Fib n)) - 1 >= 1 - 1 by XREAL_1:11;
sqrt ((((2 * (Fib (n + 1))) - (Fib n)) - 1) ^2) <= sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1) by w1, a6, SQUARE_1:94;
then ((2 * (Fib (n + 1))) - (Fib n)) - 1 <= sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1) by a1, v3, SQUARE_1:89;
then (((2 * (Fib (n + 1))) - (Fib n)) - 1) + (Fib n) <= (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1)) + (Fib n) by XREAL_1:8;
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:8;
then a8: (2 * (Fib (n + 1))) / 2 <= (((sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1)) + (Fib n)) + 1) / 2 by XREAL_1:74;
d1: (5 * ((Fib n) ^2)) - (2 * (Fib n)) = ((5 * (Fib n)) - 2) * (Fib n) ;
5 * (Fib n) >= 5 * 1 by pp, XREAL_1:66;
then (5 * (Fib n)) - 2 >= 5 - 2 by XREAL_1:11;
then c1: (5 * (Fib n)) - 2 >= 0 by XXREAL_0:2;
c2: (((Fib (n + 1)) + (Fib (n + 1))) - (Fib n)) + 1 = ((Fib (n + 1)) + (Fib (n -' 1))) + 1 by a1;
((Lucas n) ^2) - (5 * ((Fib n) ^2)) > - (2 * ((Lucas n) + (Fib n)))

proof

q1: Fib n > 0 by A0, FIB_NUM2:23, FIB_NUM2:47;
Lucas n >= n by FIB_NUM3:17;
then Lucas n >= 2 by A0, XXREAL_0:2;
then (Lucas n) + (Fib n) > 0 + 2 by q1, XREAL_1:10;
then ((Lucas n) + (Fib n)) * 2 > 2 * 2 by XREAL_1:70;
then q2: - (((Lucas n) + (Fib n)) * 2) < - 4 by XREAL_1:26;
- 4 <= 4 * ((- 1) to_power n) by tt1;
hence ((Lucas n) ^2) - (5 * ((Fib n) ^2)) > - (2 * ((Lucas n) + (Fib n))) by A2, q2, 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:8;
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:8;
then (((Lucas n) ^2) + ((2 * (Lucas n)) * 1)) + (1 ^2) > ((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + (1 ^2) by XREAL_1:8;
then sqrt ((((2 * (Fib (n + 1))) - (Fib n)) + 1) ^2) > sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1) by c1, d1, w1, SQUARE_1:95;
then ((2 * (Fib (n + 1))) - (Fib n)) + 1 > sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1) by c2, SQUARE_1:89;
then (((2 * (Fib (n + 1))) - (Fib n)) + 1) - 1 > (sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1)) - 1 by XREAL_1:11;
then ((2 * (Fib (n + 1))) - (Fib n)) + (Fib n) > ((sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1)) - 1) + (Fib n) by XREAL_1:8;
then (2 * (Fib (n + 1))) / 2 > (((sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1)) - 1) + (Fib n)) / 2 by XREAL_1:76;
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 a8, INT_1:def 4; :: thesis: verum