let n be natural number ; :: 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:66;
then (2 * n) + 1 >= 4 + 1 by XREAL_1:8;
then B0: (2 * n) + 1 > 1 by XXREAL_0:2;
tau_bar to_power ((2 * n) + 1) <= 0 by pom2;
then (tau to_power ((2 * n) + 1)) + 0 >= (tau to_power ((2 * n) + 1)) + (tau_bar to_power ((2 * n) + 1)) by XREAL_1:8;
then A1: tau to_power ((2 * n) + 1) >= Lucas ((2 * n) + 1) by FIB_NUM3:21;
- (1 / 2) <= tau_bar to_power ((2 * n) + 1) by hop9, B0;
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:8;
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 A1, INT_1:def 4; :: thesis: verum