let n be Nat; :: thesis: ( n >= 4 implies Lucas (n + 1) = [\((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) / 2)/] )
set tb = tau_bar ;
set tbn = tau_bar to_power n;
set tn = tau to_power n;
assume A1: n >= 4 ; :: thesis: Lucas (n + 1) = [\((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) / 2)/]
A2: sqrt 5 > 0 by SQUARE_1:25;
A3: (((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) / 2 >= Lucas (n + 1)

proof

A4: n - 0 is non zero Element of NAT by A1, NAT_1:21;
( Lucas (n + 1) >= n + 1 & n + 1 >= 0 + 1 ) by FIB_NUM3:17, XREAL_1:6;
then ( Lucas (n + 1) >= Lucas n & Lucas (n + 1) >= 1 ) by A4, FIB_NUM3:18, XXREAL_0:2;
then (Lucas (n + 1)) + (Lucas (n + 1)) >= (Lucas n) + 1 by XREAL_1:7;
then ((Lucas (n + 1)) + (Lucas (n + 1))) - (Lucas n) >= ((Lucas n) + 1) - (Lucas n) by XREAL_1:9;
then A5: ((2 * (Lucas (n + 1))) - (Lucas n)) - 1 >= 1 - 1 by XREAL_1:9;
((2 * (Lucas (n + 1))) - (Lucas n)) - 1 = ((2 * (Lucas (n + 1))) - ((tau to_power n) + (tau_bar to_power n))) - 1 by FIB_NUM3:21
.= ((2 * ((tau to_power (n + 1)) + (tau_bar to_power (n + 1)))) - ((tau to_power n) + (tau_bar to_power n))) - 1 by FIB_NUM3:21
.= ((2 * (((tau to_power n) * (tau to_power 1)) + (tau_bar to_power (n + 1)))) - ((tau to_power n) + (tau_bar to_power n))) - 1 by Th2
.= ((2 * (((tau to_power n) * tau) + (tau_bar to_power (n + 1)))) - ((tau to_power n) + (tau_bar to_power n))) - 1
.= ((2 * (((tau to_power n) * tau) + ((tau_bar to_power n) * (tau_bar to_power 1)))) - ((tau to_power n) + (tau_bar to_power n))) - 1 by Th2
.= ((2 * (((tau to_power n) * tau) + ((tau_bar to_power n) * tau_bar))) - ((tau to_power n) + (tau_bar to_power n))) - 1
.= (((tau to_power n) - (tau_bar to_power n)) * (sqrt 5)) - 1 by FIB_NUM:def 1, FIB_NUM:def 2
.= (((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (sqrt 5)) * (sqrt 5)) - 1 by A2, XCMPLX_1:87
.= (((Fib n) * (sqrt 5)) * (sqrt 5)) - 1 by FIB_NUM:7
.= ((Fib n) * ((sqrt 5) ^2)) - 1
.= (5 * (Fib n)) - 1 by SQUARE_1:def 2 ;
then A6: (((2 * (Lucas (n + 1))) - (Lucas n)) - 1) ^2 = (((5 * (Fib n)) ^2) - ((2 * (5 * (Fib n))) * 1)) + (1 ^2) by SQUARE_1:5
.= ((25 * ((Fib n) ^2)) - (10 * (Fib n))) + 1 ;
(5 * ((Lucas n) ^2)) - (2 * (Lucas n)) >= (25 * ((Fib n) ^2)) - (10 * (Fib n))

proof

per cases ( n = 4 or n > 4 ) by A1, XXREAL_0:1;

suppose n = 4 ; :: thesis: (5 * ((Lucas n) ^2)) - (2 * (Lucas n)) >= (25 * ((Fib n) ^2)) - (10 * (Fib n))

hence (5 * ((Lucas n) ^2)) - (2 * (Lucas n)) >= (25 * ((Fib n) ^2)) - (10 * (Fib n)) by FIB_NUM2:23, FIB_NUM3:16; :: thesis: verum

end;

suppose n > 4 ; :: thesis: (5 * ((Lucas n) ^2)) - (2 * (Lucas n)) >= (25 * ((Fib n) ^2)) - (10 * (Fib n))

then A7: n >= 4 + 1 by NAT_1:13;
set s5 = sqrt 5;
A8: (5 * ((Lucas n) ^2)) - (2 * (Lucas n)) = (5 * ((Lucas n) ^2)) - (2 * ((tau to_power n) + (tau_bar to_power n))) by FIB_NUM3:21
.= (5 * (((tau to_power n) + (tau_bar to_power n)) ^2)) - (2 * ((tau to_power n) + (tau_bar to_power n))) by FIB_NUM3:21
.= ((((5 * ((tau to_power n) ^2)) + (((5 * 2) * (tau to_power n)) * (tau_bar to_power n))) + (5 * ((tau_bar to_power n) ^2))) - (2 * (tau to_power n))) - (2 * (tau_bar to_power n)) ;
A9: (25 * ((Fib n) ^2)) - (10 * (Fib n)) = (25 * ((Fib n) ^2)) - (10 * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) by FIB_NUM:7
.= (25 * ((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) ^2)) - (10 * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) by FIB_NUM:7
.= (25 * ((((tau to_power n) - (tau_bar to_power n)) ^2) / ((sqrt 5) ^2))) - (10 * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) by XCMPLX_1:76
.= (25 * ((((tau to_power n) - (tau_bar to_power n)) ^2) / 5)) - (10 * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) by SQUARE_1:def 2
.= (((5 * ((tau to_power n) ^2)) - (((5 * 2) * (tau to_power n)) * (tau_bar to_power n))) + (5 * ((tau_bar to_power n) ^2))) - (10 * ((((tau to_power n) - (tau_bar to_power n)) * (sqrt 5)) / ((sqrt 5) ^2))) by A2, XCMPLX_1:91
.= (((5 * ((tau to_power n) ^2)) - ((10 * (tau to_power n)) * (tau_bar to_power n))) + (5 * ((tau_bar to_power n) ^2))) - (10 * ((((tau to_power n) - (tau_bar to_power n)) * (sqrt 5)) / 5)) by SQUARE_1:def 2
.= ((((5 * ((tau to_power n) ^2)) - ((10 * (tau to_power n)) * (tau_bar to_power n))) + (5 * ((tau_bar to_power n) ^2))) - ((2 * (tau to_power n)) * (sqrt 5))) + ((2 * (tau_bar to_power n)) * (sqrt 5)) ;
A10: (n -' 1) + 1 = (n + 1) -' 1 by A1, NAT_D:38, XXREAL_0:2
.= n by NAT_D:34 ;
A11: - 10 <= 10 * ((- 1) to_power n) by Lm1;
n -' 1 >= 5 -' 1 by A7, NAT_D:42;
then n -' 1 >= 5 - 1 by NAT_D:39;
then Lucas (n -' 1) >= 7 by Th12, FIB_NUM3:16;
then Lucas (n -' 1) >= 5 by XXREAL_0:2;
then (Lucas (n -' 1)) * (- 2) <= 5 * (- 2) by XREAL_1:65;
then (Lucas ((n -' 1) + 1)) - ((2 * (Lucas (n -' 1))) + (Lucas ((n -' 1) + 1))) <= - 10 ;
then (Lucas n) - (5 * (Fib n)) <= - 10 by A10, FIB_NUM3:22;
then ((tau to_power n) + (tau_bar to_power n)) - (5 * (Fib n)) <= - 10 by FIB_NUM3:21;
then ((tau to_power n) + (tau_bar to_power n)) - (5 * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) <= - 10 by FIB_NUM:7;
then ((tau to_power n) + (tau_bar to_power n)) - (5 * (((tau to_power n) - (tau_bar to_power n)) * (1 / (sqrt 5)))) <= - 10 by XCMPLX_1:99;
then ((tau to_power n) + (tau_bar to_power n)) - ((5 * (1 / (sqrt 5))) * ((tau to_power n) - (tau_bar to_power n))) <= - 10 ;
then ((tau to_power n) + (tau_bar to_power n)) - ((((sqrt 5) ^2) * (1 / (sqrt 5))) * ((tau to_power n) - (tau_bar to_power n))) <= - 10 by SQUARE_1:def 2;
then ((tau to_power n) + (tau_bar to_power n)) - (((sqrt 5) * ((sqrt 5) * (1 / (sqrt 5)))) * ((tau to_power n) - (tau_bar to_power n))) <= - 10 ;
then ((tau to_power n) + (tau_bar to_power n)) - (((sqrt 5) * ((sqrt 5) / (sqrt 5))) * ((tau to_power n) - (tau_bar to_power n))) <= - 10 by XCMPLX_1:99;
then ((tau to_power n) + (tau_bar to_power n)) - (((sqrt 5) * 1) * ((tau to_power n) - (tau_bar to_power n))) <= - 10 by A2, XCMPLX_1:60;
then (((tau to_power n) + (tau_bar to_power n)) - ((sqrt 5) * (tau to_power n))) + ((sqrt 5) * (tau_bar to_power n)) <= 10 * ((tau * tau_bar) to_power n) by Lm3, A11, XXREAL_0:2;
then ((((tau to_power n) + (tau_bar to_power n)) - ((sqrt 5) * (tau to_power n))) + ((sqrt 5) * (tau_bar to_power n))) - (10 * ((tau * tau_bar) to_power n)) <= (10 * ((tau * tau_bar) to_power n)) - (10 * ((tau * tau_bar) to_power n)) by XREAL_1:9;
then (((((tau to_power n) + (tau_bar to_power n)) - ((sqrt 5) * (tau to_power n))) + ((sqrt 5) * (tau_bar to_power n))) - (10 * ((tau * tau_bar) to_power n))) + ((sqrt 5) * (tau to_power n)) <= 0 + ((sqrt 5) * (tau to_power n)) by XREAL_1:6;
then (((tau to_power n) + (tau_bar to_power n)) + ((sqrt 5) * (tau_bar to_power n))) - (10 * ((tau * tau_bar) to_power n)) <= (sqrt 5) * (tau to_power n) ;
then (((tau to_power n) + (tau_bar to_power n)) + ((sqrt 5) * (tau_bar to_power n))) - (10 * ((tau to_power n) * (tau_bar to_power n))) <= (sqrt 5) * (tau to_power n) by NEWTON:7;
then ((((- ((10 * (tau to_power n)) * (tau_bar to_power n))) + (tau to_power n)) + (tau_bar to_power n)) + ((tau_bar to_power n) * (sqrt 5))) * 2 <= ((tau to_power n) * (sqrt 5)) * 2 by XREAL_1:64;
then - ((((- ((20 * (tau to_power n)) * (tau_bar to_power n))) + (2 * (tau to_power n))) + (2 * (tau_bar to_power n))) + ((2 * (tau_bar to_power n)) * (sqrt 5))) >= - ((2 * (tau to_power n)) * (sqrt 5)) by XREAL_1:24;
then ((((((10 * (tau to_power n)) * (tau_bar to_power n)) - (2 * (tau to_power n))) - (2 * (tau_bar to_power n))) - ((2 * (tau_bar to_power n)) * (sqrt 5))) + ((10 * (tau to_power n)) * (tau_bar to_power n))) - ((10 * (tau to_power n)) * (tau_bar to_power n)) >= (- ((2 * (tau to_power n)) * (sqrt 5))) - ((10 * (tau to_power n)) * (tau_bar to_power n)) by XREAL_1:9;
then (((((10 * (tau to_power n)) * (tau_bar to_power n)) - (2 * (tau to_power n))) - (2 * (tau_bar to_power n))) - ((2 * (tau_bar to_power n)) * (sqrt 5))) + ((2 * (tau_bar to_power n)) * (sqrt 5)) >= ((- ((10 * (tau to_power n)) * (tau_bar to_power n))) - ((2 * (tau to_power n)) * (sqrt 5))) + ((2 * (tau_bar to_power n)) * (sqrt 5)) by XREAL_1:6;
then ((((10 * (tau to_power n)) * (tau_bar to_power n)) - (2 * (tau to_power n))) - (2 * (tau_bar to_power n))) + (5 * ((tau_bar to_power n) ^2)) >= (((- ((10 * (tau to_power n)) * (tau_bar to_power n))) - ((2 * (tau to_power n)) * (sqrt 5))) + ((2 * (tau_bar to_power n)) * (sqrt 5))) + (5 * ((tau_bar to_power n) ^2)) by XREAL_1:6;
then (((((10 * (tau to_power n)) * (tau_bar to_power n)) + (5 * ((tau_bar to_power n) ^2))) - (2 * (tau to_power n))) - (2 * (tau_bar to_power n))) + (5 * ((tau to_power n) ^2)) >= ((((- ((10 * (tau to_power n)) * (tau_bar to_power n))) + (5 * ((tau_bar to_power n) ^2))) - ((2 * (tau to_power n)) * (sqrt 5))) + ((2 * (tau_bar to_power n)) * (sqrt 5))) + (5 * ((tau to_power n) ^2)) by XREAL_1:6;
hence (5 * ((Lucas n) ^2)) - (2 * (Lucas n)) >= (25 * ((Fib n) ^2)) - (10 * (Fib n)) by A8, A9; :: thesis: verum

end;

end;

end;

then ((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1 >= (((2 * (Lucas (n + 1))) - (Lucas n)) - 1) ^2 by A6, XREAL_1:6;
then sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1) >= sqrt ((((2 * (Lucas (n + 1))) - (Lucas n)) - 1) ^2) by SQUARE_1:26;
then sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1) >= ((2 * (Lucas (n + 1))) - (Lucas n)) - 1 by A5, SQUARE_1:def 2;
then (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1)) + ((Lucas n) + 1) >= (((2 * (Lucas (n + 1))) - (Lucas n)) - 1) + ((Lucas n) + 1) by XREAL_1:6;
then (((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) / 2 >= (2 * (Lucas (n + 1))) / 2 by XREAL_1:72;
hence (((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) / 2 >= Lucas (n + 1) ; :: thesis: verum

end;

((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) / 2) - 1 < Lucas (n + 1)

proof

Lucas n >= n by FIB_NUM3:17;
then A12: Lucas n >= 4 by A1, XXREAL_0:2;
then A13: (Lucas n) / 5 >= 4 / 5 by XREAL_1:72;
Fib n >= 3 by A1, FIB_NUM2:23, FIB_NUM2:45;
then (Fib n) + ((Lucas n) / 5) >= 3 + (4 / 5) by A13, XREAL_1:7;
then A14: 2 < (Fib n) + ((Lucas n) / 5) by XXREAL_0:2;
( n is even or n is odd ) ;
then (- 1) to_power n <= 1 by FIB_NUM2:2, FIB_NUM2:3;
then 2 * ((- 1) to_power n) <= 2 * 1 by XREAL_1:64;
then 2 * ((- 1) to_power n) < (Fib n) + ((Lucas n) / 5) by A14, XXREAL_0:2;
then 2 * ((- 1) to_power n) < (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) + ((Lucas n) / 5) by FIB_NUM:7;
then 2 * ((- 1) to_power n) < (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) + (((tau to_power n) + (tau_bar to_power n)) / 5) by FIB_NUM3:21;
then (2 * ((- 1) to_power n)) * 10 < ((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) + (((tau to_power n) + (tau_bar to_power n)) / 5)) * 10 by XREAL_1:68;
then 20 * ((- 1) to_power n) < ((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (2 * 5)) + (((tau to_power n) + (tau_bar to_power n)) * 2) ;
then 20 * ((- 1) to_power n) < ((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (2 * ((sqrt 5) ^2))) + (((tau to_power n) + (tau_bar to_power n)) * 2) by SQUARE_1:def 2;
then 20 * ((- 1) to_power n) < (((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (sqrt 5)) * ((sqrt 5) * 2)) + (((tau to_power n) + (tau_bar to_power n)) * 2) ;
then 20 * ((- 1) to_power n) < (((tau to_power n) - (tau_bar to_power n)) * (2 * (sqrt 5))) + (((tau to_power n) + (tau_bar to_power n)) * 2) by A2, XCMPLX_1:87;
then (20 * ((- 1) to_power n)) + (((5 * ((tau to_power n) ^2)) + (5 * ((tau_bar to_power n) ^2))) + 1) < ((((tau to_power n) - (tau_bar to_power n)) * (2 * (sqrt 5))) + (((tau to_power n) + (tau_bar to_power n)) * 2)) + (((5 * ((tau to_power n) ^2)) + (5 * ((tau_bar to_power n) ^2))) + 1) by XREAL_1:6;
then ((20 * ((- 1) to_power n)) + (((5 * ((tau to_power n) ^2)) + (5 * ((tau_bar to_power n) ^2))) + 1)) - (((tau to_power n) + (tau_bar to_power n)) * 2) < (((((tau to_power n) - (tau_bar to_power n)) * (2 * (sqrt 5))) + (((tau to_power n) + (tau_bar to_power n)) * 2)) + (((5 * ((tau to_power n) ^2)) + (5 * ((tau_bar to_power n) ^2))) + 1)) - (((tau to_power n) + (tau_bar to_power n)) * 2) by XREAL_1:9;
then ((((((10 * ((- 1) to_power n)) + (10 * ((- 1) to_power n))) + (5 * ((tau to_power n) ^2))) + (5 * ((tau_bar to_power n) ^2))) + 1) - (((tau to_power n) + (tau_bar to_power n)) * 2)) - (10 * ((- 1) to_power n)) < ((((tau to_power n) - (tau_bar to_power n)) * (2 * (sqrt 5))) + (((5 * ((tau to_power n) ^2)) + (5 * ((tau_bar to_power n) ^2))) + 1)) - (10 * ((- 1) to_power n)) by XREAL_1:9;
then (((5 * (((2 * ((tau * tau_bar) to_power n)) + ((tau to_power n) ^2)) + ((tau_bar to_power n) ^2))) + 1) - (2 * (tau to_power n))) - (2 * (tau_bar to_power n)) < ((((((2 * (sqrt 5)) * (tau to_power n)) - ((2 * (sqrt 5)) * (tau_bar to_power n))) + (5 * ((tau to_power n) ^2))) + (5 * ((tau_bar to_power n) ^2))) - (10 * ((- 1) to_power n))) + 1 by Lm3;
then (((5 * (((2 * ((tau to_power n) * (tau_bar to_power n))) + ((tau to_power n) ^2)) + ((tau_bar to_power n) ^2))) + 1) - (2 * (tau to_power n))) - (2 * (tau_bar to_power n)) < ((((((2 * (sqrt 5)) * (tau to_power n)) - ((2 * (sqrt 5)) * (tau_bar to_power n))) + (5 * ((tau to_power n) ^2))) + (5 * ((tau_bar to_power n) ^2))) - ((5 * 2) * ((- 1) to_power n))) + 1 by NEWTON:7;
then (((5 * (((tau to_power n) + (tau_bar to_power n)) ^2)) + 1) - (2 * (tau to_power n))) - (2 * (tau_bar to_power n)) < ((((2 * (sqrt 5)) * (tau to_power n)) - ((2 * (sqrt 5)) * (tau_bar to_power n))) + (5 * ((((tau to_power n) ^2) + ((tau_bar to_power n) ^2)) - (2 * ((tau * tau_bar) to_power n))))) + 1 by Lm3;
then (((5 * (((tau to_power n) + (tau_bar to_power n)) ^2)) + 1) - (2 * (tau to_power n))) - (2 * (tau_bar to_power n)) < ((((2 * (sqrt 5)) * (tau to_power n)) - ((2 * (sqrt 5)) * (tau_bar to_power n))) + (5 * ((((tau to_power n) ^2) + ((tau_bar to_power n) ^2)) - (2 * ((tau to_power n) * (tau_bar to_power n)))))) + 1 by NEWTON:7;
then A15: ((5 * (((tau to_power n) + (tau_bar to_power n)) ^2)) + 1) - (2 * ((tau to_power n) + (tau_bar to_power n))) < ((((2 * (sqrt 5)) * (tau to_power n)) - ((2 * (sqrt 5)) * (tau_bar to_power n))) + (5 * (((tau to_power n) - (tau_bar to_power n)) ^2))) + 1 ;
A16: ((5 * ((Lucas n) ^2)) + 1) - (2 * (Lucas n)) >= 0

proof

5 * (Lucas n) >= 5 * 4 by A12, XREAL_1:66;
then (5 * (Lucas n)) - 2 >= 20 - 2 by XREAL_1:9;
then (Lucas n) * ((5 * (Lucas n)) - 2) >= 4 * 18 by A12, XREAL_1:66;
then ((Lucas n) * ((5 * (Lucas n)) - 2)) + 1 >= (4 * 18) + 1 by XREAL_1:6;
hence ((5 * ((Lucas n) ^2)) + 1) - (2 * (Lucas n)) >= 0 ; :: thesis: verum

end;

A17: ((((2 * (tau to_power (n + 1))) - (tau to_power n)) + (2 * (tau_bar to_power (n + 1)))) - (tau_bar to_power n)) + 1 > 0

proof

((((2 * (tau to_power (n + 1))) - (tau to_power n)) + (2 * (tau_bar to_power (n + 1)))) - (tau_bar to_power n)) + 1 = ((((2 * ((tau to_power n) * (tau to_power 1))) - (tau to_power n)) + (2 * (tau_bar to_power (n + 1)))) - (tau_bar to_power n)) + 1 by Th2
.= ((((2 * ((tau to_power n) * (tau to_power 1))) - (tau to_power n)) + (2 * ((tau_bar to_power n) * (tau_bar to_power 1)))) - (tau_bar to_power n)) + 1 by Th2
.= ((((2 * ((tau to_power n) * tau)) - (tau to_power n)) + (2 * ((tau_bar to_power n) * (tau_bar to_power 1)))) - (tau_bar to_power n)) + 1
.= ((((tau to_power n) * (sqrt 5)) + (2 * ((tau_bar to_power n) * tau_bar))) - (tau_bar to_power n)) + 1 by FIB_NUM:def 1
.= (((sqrt 5) * ((tau to_power n) - (tau_bar to_power n))) * 1) + 1 by FIB_NUM:def 2
.= (((sqrt 5) * ((tau to_power n) - (tau_bar to_power n))) * ((sqrt 5) / (sqrt 5))) + 1 by A2, XCMPLX_1:60
.= (((sqrt 5) * ((tau to_power n) - (tau_bar to_power n))) * ((sqrt 5) * (1 / (sqrt 5)))) + 1 by XCMPLX_1:99
.= (((sqrt 5) * (((tau to_power n) - (tau_bar to_power n)) * (1 / (sqrt 5)))) * (sqrt 5)) + 1
.= (((sqrt 5) * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) * (sqrt 5)) + 1 by XCMPLX_1:99
.= (((sqrt 5) * (Fib n)) * (sqrt 5)) + 1 by FIB_NUM:7
.= (((sqrt 5) ^2) * (Fib n)) + 1
.= (5 * (Fib n)) + 1 by SQUARE_1:def 2 ;
hence ((((2 * (tau to_power (n + 1))) - (tau to_power n)) + (2 * (tau_bar to_power (n + 1)))) - (tau_bar to_power n)) + 1 > 0 ; :: thesis: verum

end;

((((2 * (sqrt 5)) * (tau to_power n)) - ((2 * (sqrt 5)) * (tau_bar to_power n))) + (5 * (((tau to_power n) - (tau_bar to_power n)) ^2))) + 1 = ((((2 * (sqrt 5)) * (tau to_power n)) - ((2 * (sqrt 5)) * (tau_bar to_power n))) + (((sqrt 5) ^2) * (((tau to_power n) - (tau_bar to_power n)) ^2))) + 1 by SQUARE_1:def 2
.= ((((((2 * tau) * (tau to_power n)) - (1 * (tau to_power n))) + ((2 * tau_bar) * (tau_bar to_power n))) - (1 * (tau_bar to_power n))) + 1) ^2 by FIB_NUM:def 1, FIB_NUM:def 2
.= ((((((2 * (tau to_power 1)) * (tau to_power n)) - (1 * (tau to_power n))) + ((2 * tau_bar) * (tau_bar to_power n))) - (1 * (tau_bar to_power n))) + 1) ^2
.= (((((2 * ((tau to_power 1) * (tau to_power n))) - (1 * (tau to_power n))) + ((2 * (tau_bar to_power 1)) * (tau_bar to_power n))) - (1 * (tau_bar to_power n))) + 1) ^2
.= (((((2 * (tau to_power (n + 1))) - (tau to_power n)) + (2 * ((tau_bar to_power 1) * (tau_bar to_power n)))) - (tau_bar to_power n)) + 1) ^2 by Th2
.= (((((2 * (tau to_power (n + 1))) - (tau to_power n)) + (2 * (tau_bar to_power (n + 1)))) - (tau_bar to_power n)) + 1) ^2 by Th2 ;
then ((5 * ((Lucas n) ^2)) + 1) - (2 * ((tau to_power n) + (tau_bar to_power n))) < (((((2 * (tau to_power (n + 1))) - (tau to_power n)) + (2 * (tau_bar to_power (n + 1)))) - (tau_bar to_power n)) + 1) ^2 by A15, FIB_NUM3:21;
then ((5 * ((Lucas n) ^2)) + 1) - (2 * (Lucas n)) < (((((2 * (tau to_power (n + 1))) - (tau to_power n)) + (2 * (tau_bar to_power (n + 1)))) - (tau_bar to_power n)) + 1) ^2 by FIB_NUM3:21;
then sqrt (((5 * ((Lucas n) ^2)) + 1) - (2 * (Lucas n))) < sqrt ((((((2 * (tau to_power (n + 1))) - (tau to_power n)) + (2 * (tau_bar to_power (n + 1)))) - (tau_bar to_power n)) + 1) ^2) by A16, SQUARE_1:27;
then sqrt (((5 * ((Lucas n) ^2)) + 1) - (2 * (Lucas n))) < (((2 * ((tau to_power (n + 1)) + (tau_bar to_power (n + 1)))) - (tau to_power n)) - (tau_bar to_power n)) + 1 by A17, SQUARE_1:22;
then sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1) < (((2 * (Lucas (n + 1))) - (tau to_power n)) - (tau_bar to_power n)) + 1 by FIB_NUM3:21;
then 1 + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1)) < ((((2 * (Lucas (n + 1))) + 1) - (tau to_power n)) - (tau_bar to_power n)) + 1 by XREAL_1:6;
then (((((tau to_power n) + (tau_bar to_power n)) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) - (tau to_power n)) - (tau_bar to_power n) < (((2 * (Lucas (n + 1))) + 2) - (tau to_power n)) - (tau_bar to_power n) ;
then ((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) - (tau to_power n)) - (tau_bar to_power n) < (((2 * (Lucas (n + 1))) + 2) - (tau to_power n)) - (tau_bar to_power n) by FIB_NUM3:21;
then (((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) - (tau to_power n) < ((2 * (Lucas (n + 1))) + 2) - (tau to_power n) by XREAL_1:9;
then ((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) - 2) + 2 < (2 * (Lucas (n + 1))) + 2 by XREAL_1:9;
then (((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) - 2 < 2 * (Lucas (n + 1)) by XREAL_1:6;
then ((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) - 2) / 2 < (2 * (Lucas (n + 1))) / 2 by XREAL_1:74;
hence ((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) / 2) - 1 < Lucas (n + 1) ; :: thesis: verum

end;

hence Lucas (n + 1) = [\((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) / 2)/] by A3, INT_1:def 6; :: thesis: verum