let n be Nat; :: thesis: ( n >= 2 implies Lucas (2 * n) = [/(tau to_power (2 * n))\] )
assume A1: n >= 2 ; :: thesis: Lucas (2 * n) = [/(tau to_power (2 * n))\]
A2: tau_bar to_power (2 * n) = (tau_bar to_power n) to_power 2 by NEWTON:9
.= (tau_bar to_power n) ^2 by POWER:46 ;
n - 0 is Element of NAT by NAT_1:21;
then tau_bar to_power n <> 0 by FIB_NUM3:1;
then tau_bar to_power (2 * n) > 0 by A2, SQUARE_1:12;
then 0 + (tau to_power (2 * n)) <= (tau to_power (2 * n)) + (tau_bar to_power (2 * n)) by XREAL_1:6;
then A3: tau to_power (2 * n) <= Lucas (2 * n) by FIB_NUM3:21;
tau_bar to_power (2 * n) < 1 by Th8, A1, XXREAL_0:2;
then (tau_bar to_power (2 * n)) + (tau to_power (2 * n)) < 1 + (tau to_power (2 * n)) by XREAL_1:6;
then (tau to_power (2 * n)) + 1 > Lucas (2 * n) by FIB_NUM3:21;
hence Lucas (2 * n) = [/(tau to_power (2 * n))\] by A3, INT_1:def 7; :: thesis: verum