let n be Element of NAT ; (5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2) = 4 * ((- 1) to_power (n + 1))
set a = tau to_power n;
set b = tau_bar to_power n;
A1: (Fib n) |^ 2 =
(Fib n) * (Fib n)
by WSIERP_1:1
.=
(((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (Fib n)
by FIB_NUM:7
.=
(((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))
by FIB_NUM:7
.=
(((tau to_power n) - (tau_bar to_power n)) * ((tau to_power n) - (tau_bar to_power n))) / ((sqrt 5) * (sqrt 5))
by XCMPLX_1:76
.=
((((tau to_power n) * (tau to_power n)) - ((2 * (tau to_power n)) * (tau_bar to_power n))) + ((tau_bar to_power n) * (tau_bar to_power n))) / 5
by Th2
;
A2: (tau to_power n) * (tau_bar to_power n) =
(tau * tau_bar) to_power n
by Th8
.=
(((1 * 1) - ((sqrt 5) * (sqrt 5))) / 4) to_power n
by FIB_NUM:def 1, FIB_NUM:def 2
.=
((1 - 5) / 4) to_power n
by Th2
.=
(- 1) to_power n
;
(Lucas n) |^ 2 =
(Lucas n) * (Lucas n)
by WSIERP_1:1
.=
((tau to_power n) + (tau_bar to_power n)) * (Lucas n)
by Th21
.=
((tau to_power n) + (tau_bar to_power n)) * ((tau to_power n) + (tau_bar to_power n))
by Th21
.=
(((tau to_power n) * (tau to_power n)) + ((2 * (tau to_power n)) * (tau_bar to_power n))) + ((tau_bar to_power n) * (tau_bar to_power n))
;
then (5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2) =
(4 * (- 1)) * ((- 1) to_power n)
by A1, A2
.=
(4 * ((- 1) to_power 1)) * ((- 1) to_power n)
by POWER:25
.=
4 * (((- 1) to_power 1) * ((- 1) to_power n))
.=
4 * ((- 1) to_power (n + 1))
by FIB_NUM2:5
;
hence
(5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2) = 4 * ((- 1) to_power (n + 1))
; verum