let n be natural number ; :: thesis: ( n >= 2 implies Lucas (2 * n) = [/(tau to_power (2 * n))\] )
assume A0: n >= 2 ; :: thesis: Lucas (2 * n) = [/(tau to_power (2 * n))\]
B0: tau_bar to_power (2 * n) = (tau_bar to_power n) to_power 2 by NEWTON:14
.= (tau_bar to_power n) ^2 by POWER:53 ;
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 B0, SQUARE_1:74;
then 0 + (tau to_power (2 * n)) <= (tau to_power (2 * n)) + (tau_bar to_power (2 * n)) by XREAL_1:8;
then A1: tau to_power (2 * n) <= Lucas (2 * n) by FIB_NUM3:21;
tau_bar to_power (2 * n) < 1 by hop8, A0, XXREAL_0:2;
then (tau_bar to_power (2 * n)) + (tau to_power (2 * n)) < 1 + (tau to_power (2 * n)) by XREAL_1:8;
then (tau to_power (2 * n)) + 1 > Lucas (2 * n) by FIB_NUM3:21;
hence Lucas (2 * n) = [/(tau to_power (2 * n))\] by A1, INT_1:def 5; :: thesis: verum