let n be Nat; :: thesis: Fib (n + 1) = ((Fib n) + (sqrt ((5 * ((Fib n) ^2)) + (4 * ((- 1) to_power n))))) / 2
A1: n - 0 is Element of NAT by NAT_1:21;
A2: 2 * (Fib (n + 1)) = (Fib n) + (Lucas n) by FIB_NUM3:24;
A3: ((Lucas n) ^2) - (5 * ((Fib n) ^2)) = ((Lucas n) to_power 2) - (5 * ((Fib n) ^2)) by POWER:46
.= ((Lucas n) to_power 2) - (5 * ((Fib n) to_power 2)) by POWER:46
.= - ((5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2))
.= - (4 * ((- 1) to_power (n + 1))) by A1, FIB_NUM3:30
.= (- 1) * (((- 1) to_power (n + 1)) * 4)
.= ((- 1) to_power 1) * (((- 1) to_power (n + 1)) * 4)
.= (((- 1) to_power 1) * ((- 1) to_power (n + 1))) * 4
.= ((- 1) to_power ((n + 1) + 1)) * 4 by Th2
.= ((- 1) to_power (n + 2)) * 4
.= (((- 1) to_power n) * ((- 1) to_power 2)) * 4 by Th2
.= (((- 1) to_power n) * 1) * 4 by FIB_NUM2:3, POLYFORM:5 ;
Fib (n + 1) = ((Fib n) + (Lucas n)) / 2 by A2;
hence Fib (n + 1) = ((Fib n) + (sqrt ((5 * ((Fib n) ^2)) + (4 * ((- 1) to_power n))))) / 2 by A3, SQUARE_1:def 2; :: thesis: verum