let n be natural number ; :: thesis: Fib (n + 1) = ((Fib n) + (sqrt ((5 * ((Fib n) ^2)) + (4 * ((- 1) to_power n))))) / 2
A0: n - 0 is Element of NAT by NAT_1:21;
A1: 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:53
.= ((Lucas n) to_power 2) - (5 * ((Fib n) to_power 2)) by POWER:53
.= - ((5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2))
.= - (4 * ((- 1) to_power (n + 1))) by A0, FIB_NUM3:30
.= (- 1) * (((- 1) to_power (n + 1)) * 4)
.= ((- 1) to_power 1) * (((- 1) to_power (n + 1)) * 4) by POWER:30
.= (((- 1) to_power 1) * ((- 1) to_power (n + 1))) * 4
.= ((- 1) to_power ((n + 1) + 1)) * 4 by JakPower32
.= ((- 1) to_power (n + 2)) * 4
.= (((- 1) to_power n) * ((- 1) to_power 2)) * 4 by JakPower32
.= (((- 1) to_power n) * 1) * 4 by FIB_NUM2:5, POLYFORM:5 ;
Fib (n + 1) = ((Fib n) + (Lucas n)) / 2 by A1;
hence Fib (n + 1) = ((Fib n) + (sqrt ((5 * ((Fib n) ^2)) + (4 * ((- 1) to_power n))))) / 2 by A3, SQUARE_1:def 4; :: thesis: verum