let n be Nat; :: thesis: ( n >= 2 implies Lucas ((2 * n) + 1) = [\(tau to_power ((2 * n) + 1))/] )
assume n >= 2 ; :: thesis: Lucas ((2 * n) + 1) = [\(tau to_power ((2 * n) + 1))/]
then 2 * n >= 2 * 2 by XREAL_1:64;
then (2 * n) + 1 >= 4 + 1 by XREAL_1:6;
then A1: (2 * n) + 1 > 1 by XXREAL_0:2;
tau_bar to_power ((2 * n) + 1) <= 0 by Th7;
then (tau to_power ((2 * n) + 1)) + 0 >= (tau to_power ((2 * n) + 1)) + (tau_bar to_power ((2 * n) + 1)) by XREAL_1:6;
then A2: tau to_power ((2 * n) + 1) >= Lucas ((2 * n) + 1) by FIB_NUM3:21;
- (1 / 2) <= tau_bar to_power ((2 * n) + 1) by Th14, A1;
then tau_bar to_power ((2 * n) + 1) > - 1 by XXREAL_0:2;
then (- 1) + (tau to_power ((2 * n) + 1)) < (tau to_power ((2 * n) + 1)) + (tau_bar to_power ((2 * n) + 1)) by XREAL_1:6;
then (tau to_power ((2 * n) + 1)) - 1 < Lucas ((2 * n) + 1) by FIB_NUM3:21;
hence Lucas ((2 * n) + 1) = [\(tau to_power ((2 * n) + 1))/] by A2, INT_1:def 6; :: thesis: verum