let n be Nat; :: thesis: ( n <> 1 implies Lucas (n + 1) = ((Lucas n) + (sqrt (5 * (((Lucas n) ^2) - (4 * ((- 1) to_power n)))))) / 2 )
assume A1: n <> 1 ; :: thesis: Lucas (n + 1) = ((Lucas n) + (sqrt (5 * (((Lucas n) ^2) - (4 * ((- 1) to_power n)))))) / 2
A2: ((Lucas n) ^2) - (((- 1) to_power n) * 4) >= 0
proof
per cases ( n = 0 or n > 1 ) by A1, NAT_1:25;
suppose n = 0 ; :: thesis: ((Lucas n) ^2) - (((- 1) to_power n) * 4) >= 0
then ((Lucas n) ^2) - (((- 1) to_power n) * 4) = (2 * 2) - (1 * 4) by FIB_NUM3:11, POWER:24;
hence ((Lucas n) ^2) - (((- 1) to_power n) * 4) >= 0 ; :: thesis: verum
end;
suppose n > 1 ; :: thesis: ((Lucas n) ^2) - (((- 1) to_power n) * 4) >= 0
then n + 1 > 1 + 1 by XREAL_1:8;
then ( n >= 2 & Lucas n >= n ) by FIB_NUM3:17, NAT_1:13;
then Lucas n >= 2 by XXREAL_0:2;
then (Lucas n) ^2 >= 2 ^2 by SQUARE_1:15;
then ( (Lucas n) ^2 >= 2 * 2 & - (4 * ((- 1) to_power n)) >= - 4 ) by Lm2;
then ((Lucas n) ^2) + (- (4 * ((- 1) to_power n))) >= (2 * 2) + (- 4) by XREAL_1:7;
hence ((Lucas n) ^2) - (((- 1) to_power n) * 4) >= 0 ; :: thesis: verum
end;
end;
end;
A3: n - 0 is Element of NAT by NAT_1:21;
then 2 * (Lucas (n + 1)) = ((Lucas n) * 1) + ((5 * (Fib n)) * 1) by FIB_NUM3:11, FIB_NUM3:26, PRE_FF:1;
then A4: Lucas (n + 1) = ((5 * (Fib n)) + (Lucas n)) / 2 ;
((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 A3, 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 ;
then Fib n = sqrt ((((Lucas n) ^2) - (((- 1) to_power n) * 4)) / 5) by SQUARE_1:def 2;
then Lucas (n + 1) = ((5 * ((sqrt (((Lucas n) ^2) - (((- 1) to_power n) * 4))) / (sqrt 5))) + (Lucas n)) / 2 by A2, A4, SQUARE_1:30
.= ((((sqrt (((Lucas n) ^2) - (((- 1) to_power n) * 4))) * 5) / (sqrt 5)) + (Lucas n)) / 2 by XCMPLX_1:74
.= (((sqrt (((Lucas n) ^2) - (((- 1) to_power n) * 4))) * (5 / (sqrt 5))) + (Lucas n)) / 2 by XCMPLX_1:74
.= (((sqrt (((Lucas n) ^2) - (((- 1) to_power n) * 4))) * (sqrt 5)) + (Lucas n)) / 2 by SQUARE_1:34
.= ((sqrt ((((Lucas n) ^2) - (((- 1) to_power n) * 4)) * 5)) + (Lucas n)) / 2 by A2, SQUARE_1:29 ;
hence Lucas (n + 1) = ((Lucas n) + (sqrt (5 * (((Lucas n) ^2) - (4 * ((- 1) to_power n)))))) / 2 ; :: thesis: verum