let n be natural number ; :: 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 A0: n >= 4 ; :: thesis: Lucas (n + 1) = [\((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2 )) - (2 * (Lucas n))) + 1))) / 2)/]
C0: sqrt 5 > 0 by SQUARE_1:93;
A1: (((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2 )) - (2 * (Lucas n))) + 1))) / 2 >= Lucas (n + 1)

proof

ZX: n - 0 is non empty Element of NAT by NAT_1:21, A0;
( Lucas (n + 1) >= n + 1 & n + 1 >= 0 + 1 ) by FIB_NUM3:17, XREAL_1:8;
then ( Lucas (n + 1) >= Lucas n & Lucas (n + 1) >= 1 ) by FIB_NUM3:18, XXREAL_0:2, ZX;
then (Lucas (n + 1)) + (Lucas (n + 1)) >= (Lucas n) + 1 by XREAL_1:9;
then ((Lucas (n + 1)) + (Lucas (n + 1))) - (Lucas n) >= ((Lucas n) + 1) - (Lucas n) by XREAL_1:11;
then F0: ((2 * (Lucas (n + 1))) - (Lucas n)) - 1 >= 1 - 1 by XREAL_1:11;
((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 JakPower32
.= ((2 * (((tau to_power n) * tau ) + (tau_bar to_power (n + 1)))) - ((tau to_power n) + (tau_bar to_power n))) - 1 by POWER:30
.= ((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 JakPower32
.= ((2 * (((tau to_power n) * tau ) + ((tau_bar to_power n) * tau_bar ))) - ((tau to_power n) + (tau_bar to_power n))) - 1 by POWER:30
.= (((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 C0, XCMPLX_1:88
.= (((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 4 ;
then G1: (((2 * (Lucas (n + 1))) - (Lucas n)) - 1) ^2 = (((5 * (Fib n)) ^2 ) - ((2 * (5 * (Fib n))) * 1)) + (1 ^2 ) by SQUARE_1:64
.= ((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 A0, 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_NUM3:16, FIB_NUM2:25; :: thesis: verum

end;

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

then K1: n >= 4 + 1 by NAT_1:13;
set s5 = sqrt 5;
LW: (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)) ;
PR: (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:77
.= (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 4
.= (((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 XCMPLX_1:92, C0
.= (((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 4
.= ((((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)) ;
K2: (n -' 1) + 1 = (n + 1) -' 1 by NAT_D:38, A0, XXREAL_0:2
.= n by NAT_D:34 ;
aa: - 10 <= 10 * ((- 1) to_power n) by tt1;
n -' 1 >= 5 -' 1 by K1, NAT_D:42;
then n -' 1 >= 5 - 1 by NAT_D:39;
then Lucas (n -' 1) >= 7 by FIB_NUM3:16, luc1;
then Lucas (n -' 1) >= 5 by XXREAL_0:2;
then (Lucas (n -' 1)) * (- 2) <= 5 * (- 2) by XREAL_1:67;
then (Lucas ((n -' 1) + 1)) - ((2 * (Lucas (n -' 1))) + (Lucas ((n -' 1) + 1))) <= - 10 ;
then (Lucas n) - (5 * (Fib n)) <= - 10 by K2, 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:100;
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 4;
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:100;
then ((tau to_power n) + (tau_bar to_power n)) - (((sqrt 5) * 1) * ((tau to_power n) - (tau_bar to_power n))) <= - 10 by XCMPLX_1:60, C0;
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 albet3, aa, 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:11;
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:8;
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:12;
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:66;
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:26;
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:11;
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:8;
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:8;
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:8;
hence (5 * ((Lucas n) ^2 )) - (2 * (Lucas n)) >= (25 * ((Fib n) ^2 )) - (10 * (Fib n)) by LW, PR; :: thesis: verum

end;

end;

end;

then ((5 * ((Lucas n) ^2 )) - (2 * (Lucas n))) + 1 >= (((2 * (Lucas (n + 1))) - (Lucas n)) - 1) ^2 by G1, XREAL_1:8;
then sqrt (((5 * ((Lucas n) ^2 )) - (2 * (Lucas n))) + 1) >= sqrt ((((2 * (Lucas (n + 1))) - (Lucas n)) - 1) ^2 ) by SQUARE_1:94;
then sqrt (((5 * ((Lucas n) ^2 )) - (2 * (Lucas n))) + 1) >= ((2 * (Lucas (n + 1))) - (Lucas n)) - 1 by F0, SQUARE_1:def 4;
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:8;
then (((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2 )) - (2 * (Lucas n))) + 1))) / 2 >= (2 * (Lucas (n + 1))) / 2 by XREAL_1:74;
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 BB: Lucas n >= 4 by A0, XXREAL_0:2;
then B0: (Lucas n) / 5 >= 4 / 5 by XREAL_1:74;
Fib n >= 3 by FIB_NUM2:25, FIB_NUM2:47, A0;
then (Fib n) + ((Lucas n) / 5) >= 3 + (4 / 5) by B0, XREAL_1:9;
then B1: 2 < (Fib n) + ((Lucas n) / 5) by XXREAL_0:2;
( n is even or not n is even ) ;
then (- 1) to_power n <= 1 by FIB_NUM2:3, FIB_NUM2:5;
then 2 * ((- 1) to_power n) <= 2 * 1 by XREAL_1:66;
then 2 * ((- 1) to_power n) < (Fib n) + ((Lucas n) / 5) by B1, 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:70;
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 4;
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 XCMPLX_1:88, C0;
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:8;
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:11;
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:11;
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 albet3;
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:12;
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 albet3;
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:12;
then E1: ((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 ;
E2: ((5 * ((Lucas n) ^2 )) + 1) - (2 * (Lucas n)) >= 0

proof

5 * (Lucas n) >= 5 * 4 by BB, XREAL_1:68;
then (5 * (Lucas n)) - 2 >= 20 - 2 by XREAL_1:11;
then (Lucas n) * ((5 * (Lucas n)) - 2) >= 4 * 18 by BB, XREAL_1:68;
then ((Lucas n) * ((5 * (Lucas n)) - 2)) + 1 >= (4 * 18) + 1 by XREAL_1:8;
hence ((5 * ((Lucas n) ^2 )) + 1) - (2 * (Lucas n)) >= 0 ; :: thesis: verum

end;

E3: ((((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 JakPower32
.= ((((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 JakPower32
.= ((((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 by POWER:30
.= ((((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, POWER:30
.= (((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 XCMPLX_1:60, C0
.= (((sqrt 5) * ((tau to_power n) - (tau_bar to_power n))) * ((sqrt 5) * (1 / (sqrt 5)))) + 1 by XCMPLX_1:100
.= (((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:100
.= (((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 4 ;
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 4
.= ((((((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 by POWER:30
.= (((((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 by POWER:30
.= (((((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 JakPower32
.= (((((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 JakPower32 ;
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 E1, 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 SQUARE_1:95, E2;
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 SQUARE_1:89, E3;
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:8;
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:11;
then ((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2 )) - (2 * (Lucas n))) + 1))) - 2) + 2 < (2 * (Lucas (n + 1))) + 2 by XREAL_1:11;
then (((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2 )) - (2 * (Lucas n))) + 1))) - 2 < 2 * (Lucas (n + 1)) by XREAL_1:8;
then ((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2 )) - (2 * (Lucas n))) + 1))) - 2) / 2 < (2 * (Lucas (n + 1))) / 2 by XREAL_1:76;
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 A1, INT_1:def 4; :: thesis: verum