let n, k be Nat; :: thesis:
assume A1: ( n >= 4 & k >= 1 & n > k & n is odd ) ; :: thesis:
set tb = tau_bar ;
set tk = tau to_power k;
set tn = tau to_power n;
set tbn = tau_bar to_power n;
A2: sqrt 5 > 1 by SQUARE_1:18, SQUARE_1:27;
A3: ((tau to_power k) * (Lucas n)) + 1 >= Lucas (n + k)

proof

((tau to_power k) * (tau_bar to_power n)) + 1 >= tau_bar to_power (n + k)

proof

consider m being Nat such that
A4: n = k + m by A1, NAT_1:10;
A5: m is non zero Nat by A1, A4;
then A6: m >= 1 by NAT_1:14;
A7: ((((1 - (sqrt 5)) to_power m) * ((- 1) to_power k)) / (2 to_power m)) + 1 >= ((1 - (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m))

proof

per cases ;

suppose A8: k is even ; :: thesis:

then A9: m is odd by A1, A4;
A10: 2 to_power m > 0 by POWER:34;
A11: ((((1 - (sqrt 5)) to_power m) * ((- 1) to_power k)) / (2 to_power m)) + 1 = ((((1 - (sqrt 5)) to_power m) * 1) / (2 to_power m)) + 1 by A8, FIB_NUM2:3
.= (((- ((- 1) + (sqrt 5))) to_power m) / (2 to_power m)) + ((2 to_power m) / (2 to_power m)) by A10, XCMPLX_1:60
.= ((((- 1) * ((sqrt 5) - 1)) to_power m) + (2 to_power m)) / (2 to_power m) by XCMPLX_1:62
.= ((((- 1) to_power m) * (((sqrt 5) - 1) to_power m)) + (2 to_power m)) / (2 to_power m) by NEWTON:7
.= ((2 to_power m) + ((- 1) * (((sqrt 5) - 1) to_power m))) / (2 to_power m) by A9, FIB_NUM2:2
.= ((2 to_power m) - (((sqrt 5) - 1) to_power m)) / (2 to_power m) ;
A12: ( sqrt (3 ^2) > sqrt 5 & sqrt 5 > sqrt 1 ) by SQUARE_1:27;
then ( 3 > sqrt 5 & sqrt 5 > 1 ) by SQUARE_1:18, SQUARE_1:def 2;
then ( 3 - 1 > (sqrt 5) - 1 & (sqrt 5) - 1 > 1 - 1 ) by XREAL_1:9;
then 2 to_power m > ((sqrt 5) - 1) to_power m by A5, POWER:37;
then A13: (2 to_power m) - (((sqrt 5) - 1) to_power m) > (((sqrt 5) - 1) to_power m) - (((sqrt 5) - 1) to_power m) by XREAL_1:9;
A14: ((1 - (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)) = (((- 1) * ((- 1) + (sqrt 5))) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m))
.= (((- 1) to_power ((2 * k) + m)) * (((- 1) + (sqrt 5)) to_power ((2 * k) + m))) / (2 to_power ((2 * k) + m)) by NEWTON:7
.= ((- 1) * (((- 1) + (sqrt 5)) to_power ((2 * k) + m))) / (2 to_power ((2 * k) + m)) by A9, FIB_NUM2:2
.= (- 1) * ((((- 1) + (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m))) by XCMPLX_1:74 ;
(sqrt 5) - 1 > 1 - 1 by A12, SQUARE_1:18, XREAL_1:9;
then ((- 1) + (sqrt 5)) to_power ((2 * k) + m) > 0 by POWER:34;
then ((1 - (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)) <= 0 by A14;
hence ((((1 - (sqrt 5)) to_power m) * ((- 1) to_power k)) / (2 to_power m)) + 1 >= ((1 - (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)) by A13, A11; :: thesis:

end;

suppose A15: k is odd ; :: thesis:

then A16: m is even by A1, A4;
A17: 2 to_power m > 0 by POWER:34;
A18: 2 to_power (2 * k) > 0 by POWER:34;
m > 1 by A16, A6, POLYFORM:4, XXREAL_0:1;
then A19: m - 1 is non zero Nat by NAT_1:20;
A20: ((((1 - (sqrt 5)) to_power m) * ((- 1) to_power k)) / (2 to_power m)) + 1 = ((((1 - (sqrt 5)) to_power m) * (- 1)) / (2 to_power m)) + 1 by A15, FIB_NUM2:2
.= ((((1 - (sqrt 5)) to_power m) * (- 1)) / (2 to_power m)) + ((2 to_power m) / (2 to_power m)) by A17, XCMPLX_1:60
.= (((((- 1) * ((- 1) + (sqrt 5))) to_power m) * (- 1)) + (2 to_power m)) / (2 to_power m) by XCMPLX_1:62
.= (((((- 1) to_power m) * (((- 1) + (sqrt 5)) to_power m)) * (- 1)) + (2 to_power m)) / (2 to_power m) by NEWTON:7
.= (((1 * (((- 1) + (sqrt 5)) to_power m)) * (- 1)) + (2 to_power m)) / (2 to_power m) by A16, FIB_NUM2:3
.= (((- (((- 1) + (sqrt 5)) to_power m)) + (2 to_power m)) * (2 to_power (2 * k))) / ((2 to_power m) * (2 to_power (2 * k))) by A18, XCMPLX_1:91
.= ((- ((((- 1) + (sqrt 5)) to_power m) * (2 to_power (2 * k)))) + ((2 to_power m) * (2 to_power (2 * k)))) / (2 to_power (m + (2 * k))) by Th2
.= ((- ((((- 1) + (sqrt 5)) to_power m) * (2 to_power (2 * k)))) + (2 to_power (m + (2 * k)))) / (2 to_power (m + (2 * k))) by Th2
.= ((2 to_power (m + (2 * k))) - ((((- 1) + (sqrt 5)) to_power m) * (2 to_power (2 * k)))) / (2 to_power (m + (2 * k))) ;
A21: ((1 - (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)) = (((- 1) * ((- 1) + (sqrt 5))) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m))
.= (((- 1) to_power ((2 * k) + m)) * (((- 1) + (sqrt 5)) to_power ((2 * k) + m))) / (2 to_power ((2 * k) + m)) by NEWTON:7
.= (1 * (((- 1) + (sqrt 5)) to_power ((2 * k) + m))) / (2 to_power ((2 * k) + m)) by A16, FIB_NUM2:3
.= (((sqrt 5) - 1) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)) ;
(2 to_power m) - (((sqrt 5) - 1) to_power m) >= ((sqrt 5) - 1) to_power m

proof

defpred S₁[ Nat] means (2 to_power ($1 + 1)) - (((sqrt 5) - 1) to_power ($1 + 1)) >= ((sqrt 5) - 1) to_power ($1 + 1);
A22: (2 to_power (1 + 1)) - (((sqrt 5) - 1) to_power (1 + 1)) = (2 ^2) - (((sqrt 5) - 1) to_power 2) by POWER:46
.= 4 - (((sqrt 5) - 1) ^2) by POWER:46
.= 4 - ((((sqrt 5) ^2) - ((2 * (sqrt 5)) * 1)) + (1 ^2))
.= 4 - ((5 - (2 * (sqrt 5))) + 1) by SQUARE_1:def 2
.= (2 * (sqrt 5)) - 2 ;
A23: ((sqrt 5) - 1) to_power (1 + 1) = ((sqrt 5) - 1) ^2 by POWER:46
.= (((sqrt 5) ^2) - ((2 * (sqrt 5)) * 1)) + (1 ^2)
.= (5 - (2 * (sqrt 5))) + 1 by SQUARE_1:def 2
.= 6 - (2 * (sqrt 5)) ;
sqrt 5 >= sqrt (2 ^2) by SQUARE_1:27;
then sqrt 5 >= 2 by SQUARE_1:def 2;
then (sqrt 5) * 4 >= 2 * 4 by XREAL_1:64;
then (((sqrt 5) * 2) + ((sqrt 5) * 2)) - 2 >= (6 + 2) - 2 by XREAL_1:9;
then ((((sqrt 5) * 2) + ((sqrt 5) * 2)) - 2) - (2 * (sqrt 5)) >= 6 - (2 * (sqrt 5)) by XREAL_1:9;
then A24: S₁[1] by A22, A23;
A25: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis:
A26: (sqrt 5) - 1 > 1 - 1 by A2, XREAL_1:9;
assume S₁[k] ; :: thesis:
then ((2 to_power (k + 1)) - (((sqrt 5) - 1) to_power (k + 1))) + (((sqrt 5) - 1) to_power (k + 1)) >= (((sqrt 5) - 1) to_power (k + 1)) + (((sqrt 5) - 1) to_power (k + 1)) by XREAL_1:6;
then (2 to_power (k + 1)) * ((sqrt 5) - 1) >= (2 * (((sqrt 5) - 1) to_power (k + 1))) * ((sqrt 5) - 1) by A26, XREAL_1:64;
then (2 to_power (k + 1)) * ((sqrt 5) - 1) >= 2 * ((((sqrt 5) - 1) to_power (k + 1)) * ((sqrt 5) - 1)) ;
then (2 to_power (k + 1)) * ((sqrt 5) - 1) >= 2 * ((((sqrt 5) - 1) to_power (k + 1)) * (((sqrt 5) - 1) to_power 1)) ;
then A27: (2 to_power (k + 1)) * ((sqrt 5) - 1) >= 2 * (((sqrt 5) - 1) to_power ((k + 1) + 1)) by Th2, A26;
sqrt (3 ^2) >= sqrt 5 by SQUARE_1:27;
then 3 >= sqrt 5 by SQUARE_1:def 2;
then 3 - 1 >= (sqrt 5) - 1 by XREAL_1:9;
then 2 * (2 to_power (k + 1)) >= ((sqrt 5) - 1) * (2 to_power (k + 1)) by XREAL_1:64;
then (2 to_power 1) * (2 to_power (k + 1)) >= ((sqrt 5) - 1) * (2 to_power (k + 1)) ;
then 2 to_power ((1 + k) + 1) >= ((sqrt 5) - 1) * (2 to_power (k + 1)) by Th2;
then 2 to_power ((1 + k) + 1) >= 2 * (((sqrt 5) - 1) to_power ((k + 1) + 1)) by A27, XXREAL_0:2;
then (2 to_power ((1 + k) + 1)) - (((sqrt 5) - 1) to_power ((k + 1) + 1)) >= (2 * (((sqrt 5) - 1) to_power ((k + 1) + 1))) - (((sqrt 5) - 1) to_power ((k + 1) + 1)) by XREAL_1:9;
hence S₁[k + 1] ; :: thesis:

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A24, A25);
then (2 to_power ((m - 1) + 1)) - (((sqrt 5) - 1) to_power ((m - 1) + 1)) >= ((sqrt 5) - 1) to_power ((m - 1) + 1) by A19;
hence (2 to_power m) - (((sqrt 5) - 1) to_power m) >= ((sqrt 5) - 1) to_power m ; :: thesis:

end;

then ((2 to_power m) - (((sqrt 5) - 1) to_power m)) * (2 to_power (2 * k)) >= (((sqrt 5) - 1) to_power m) * (2 to_power (2 * k)) by XREAL_1:64;
then ((2 to_power m) * (2 to_power (2 * k))) - ((((sqrt 5) - 1) to_power m) * (2 to_power (2 * k))) >= (((sqrt 5) - 1) to_power m) * (2 to_power (2 * k)) ;
then (2 to_power (m + (2 * k))) - ((((sqrt 5) - 1) to_power m) * (2 to_power (2 * k))) >= (((sqrt 5) - 1) to_power m) * (2 to_power (2 * k)) by Th2;
then ((2 to_power (m + (2 * k))) - ((((sqrt 5) - 1) to_power m) * (2 to_power (2 * k)))) / (2 to_power (m + (2 * k))) >= ((((sqrt 5) - 1) to_power m) * (2 to_power (2 * k))) / (2 to_power (m + (2 * k))) by XREAL_1:72;
then A28: (((2 to_power m) * (2 to_power (2 * k))) - ((((sqrt 5) - 1) to_power m) * (2 to_power (2 * k)))) / (2 to_power (m + (2 * k))) >= ((((sqrt 5) - 1) to_power m) * (2 to_power (2 * k))) / (2 to_power (m + (2 * k))) by Th2;
A29: (sqrt 5) - 1 > 1 - 1 by A2, XREAL_1:9;
( sqrt (3 ^2) > sqrt 5 & sqrt 5 > sqrt 1 ) by SQUARE_1:27;
then ( 3 > sqrt 5 & sqrt 5 > 1 ) by SQUARE_1:18, SQUARE_1:def 2;
then A30: ( 3 - 1 > (sqrt 5) - 1 & (sqrt 5) - 1 > 1 - 1 ) by XREAL_1:9;
then A31: ((sqrt 5) - 1) to_power m > 0 by POWER:34;
2 to_power (2 * k) >= ((sqrt 5) - 1) to_power (2 * k) by A30, A1, POWER:37;
then (2 to_power (2 * k)) * (((sqrt 5) - 1) to_power m) >= (((sqrt 5) - 1) to_power (2 * k)) * (((sqrt 5) - 1) to_power m) by A31, XREAL_1:64;
then ((2 to_power (2 * k)) * (((sqrt 5) - 1) to_power m)) / (2 to_power ((2 * k) + m)) >= ((((sqrt 5) - 1) to_power (2 * k)) * (((sqrt 5) - 1) to_power m)) / (2 to_power ((2 * k) + m)) by XREAL_1:72;
then (((2 to_power m) - (((sqrt 5) - 1) to_power m)) * (2 to_power (2 * k))) / (2 to_power (m + (2 * k))) >= ((((sqrt 5) - 1) to_power (2 * k)) * (((sqrt 5) - 1) to_power m)) / (2 to_power ((2 * k) + m)) by A28, XXREAL_0:2;
then (((2 to_power m) * (2 to_power (2 * k))) - ((((sqrt 5) - 1) to_power m) * (2 to_power (2 * k)))) / (2 to_power (m + (2 * k))) >= (((sqrt 5) - 1) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)) by Th2, A29;
hence ((((1 - (sqrt 5)) to_power m) * ((- 1) to_power k)) / (2 to_power m)) + 1 >= ((1 - (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)) by A20, A21, Th2; :: thesis:

end;

(sqrt 5) - 1 > 1 - 1 by A2, XREAL_1:9;
then A32: - ((sqrt 5) - 1) < 0 ;
((1 + (sqrt 5)) * (1 - (sqrt 5))) / (2 to_power 2) = ((1 + (sqrt 5)) * (1 - (sqrt 5))) / (2 ^2) by POWER:46
.= ((1 ^2) - ((sqrt 5) ^2)) / 4
.= (1 - 5) / 4 by SQUARE_1:def 2
.= - 1 ;
then (- 1) to_power k = (((1 + (sqrt 5)) * (1 - (sqrt 5))) to_power k) / ((2 to_power 2) to_power k) by Th1
.= (((1 + (sqrt 5)) * (1 - (sqrt 5))) to_power k) / (2 to_power (2 * k)) by NEWTON:9 ;
then (((((1 - (sqrt 5)) to_power m) * (((1 + (sqrt 5)) * (1 - (sqrt 5))) to_power k)) / (2 to_power (2 * k))) / (2 to_power m)) + 1 >= ((1 - (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)) by A7, XCMPLX_1:74;
then ((((1 - (sqrt 5)) to_power m) * (((1 + (sqrt 5)) * (1 - (sqrt 5))) to_power k)) / ((2 to_power (2 * k)) * (2 to_power m))) + 1 >= ((1 - (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)) by XCMPLX_1:78;
then ((((1 - (sqrt 5)) to_power m) * (((1 + (sqrt 5)) * (1 - (sqrt 5))) to_power k)) / (2 to_power ((2 * k) + m))) + 1 >= ((1 - (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)) by Th2;
then ((((1 - (sqrt 5)) to_power m) * (((1 + (sqrt 5)) to_power k) * ((1 - (sqrt 5)) to_power k))) / (2 to_power ((2 * k) + m))) + 1 >= ((1 - (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)) by NEWTON:7;
then (((((1 - (sqrt 5)) to_power m) * ((1 - (sqrt 5)) to_power k)) * ((1 + (sqrt 5)) to_power k)) / (2 to_power ((2 * k) + m))) + 1 >= ((1 - (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)) ;
then ((((1 - (sqrt 5)) to_power (m + k)) * ((1 + (sqrt 5)) to_power k)) / (2 to_power ((k + k) + m))) + 1 >= ((1 - (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)) by Th2, A32;
then ((((1 - (sqrt 5)) to_power n) * ((1 + (sqrt 5)) to_power k)) / (2 to_power (k + n))) + 1 >= ((1 - (sqrt 5)) / 2) to_power ((k + k) + m) by A4, Th1;
then ((((1 - (sqrt 5)) to_power n) * ((1 + (sqrt 5)) to_power k)) / ((2 to_power n) * (2 to_power k))) + 1 >= tau_bar to_power (k + n) by Th2, A4, FIB_NUM:def 2;
then ((((1 - (sqrt 5)) to_power n) / (2 to_power n)) * (((1 + (sqrt 5)) to_power k) / (2 to_power k))) + 1 >= tau_bar to_power (k + n) by XCMPLX_1:76;
then ((((1 - (sqrt 5)) / 2) to_power n) * (((1 + (sqrt 5)) to_power k) / (2 to_power k))) + 1 >= tau_bar to_power (k + n) by Th1;
hence ((tau to_power k) * (tau_bar to_power n)) + 1 >= tau_bar to_power (n + k) by Th1, FIB_NUM:def 1, FIB_NUM:def 2; :: thesis:

end;

then (((tau to_power k) * (tau_bar to_power n)) + 1) + (tau to_power (n + k)) >= (tau_bar to_power (n + k)) + (tau to_power (n + k)) by XREAL_1:6;
then ((tau to_power (n + k)) + ((tau to_power k) * (tau_bar to_power n))) + 1 >= (tau to_power (n + k)) + (tau_bar to_power (n + k)) ;
then (((tau to_power k) * (tau to_power n)) + ((tau to_power k) * (tau_bar to_power n))) + 1 >= (tau to_power (n + k)) + (tau_bar to_power (n + k)) by Th2;
then ((tau to_power k) * ((tau to_power n) + (tau_bar to_power n))) + 1 >= Lucas (n + k) by FIB_NUM3:21;
hence ((tau to_power k) * (Lucas n)) + 1 >= Lucas (n + k) by FIB_NUM3:21; :: thesis:

end;

(((tau to_power k) * (Lucas n)) + 1) - 1 < Lucas (n + k)

proof

proof

let m be non zero Nat; :: thesis:
assume S₁[m] ; :: thesis:
A35: (1 - (sqrt 5)) to_power (m + 1) < (1 + (sqrt 5)) to_power (m + 1)

proof

reconsider s = m + 1 as Element of NAT by ORDINAL1:def 12;
(1 - (sqrt 5)) to_power s <= |.((1 - (sqrt 5)) to_power s).| by ABSVALUE:4;
then A36: (1 - (sqrt 5)) to_power s <= |.(1 - (sqrt 5)).| to_power s by SERIES_1:2;
sqrt 5 > sqrt 1 by SQUARE_1:27;
then - (sqrt 5) < - 1 by SQUARE_1:18, XREAL_1:24;
then A37: (- (sqrt 5)) + 1 < (- 1) + 1 by XREAL_1:6;
then A38: |.(1 - (sqrt 5)).| = - (1 - (sqrt 5)) by ABSVALUE:def 1;
- (1 - (sqrt 5)) = (- 1) + (sqrt 5) ;
then - (1 - (sqrt 5)) < 1 + (sqrt 5) by XREAL_1:6;
then |.(1 - (sqrt 5)).| to_power s < (1 + (sqrt 5)) to_power s by A38, A37, POWER:37;
hence (1 - (sqrt 5)) to_power (m + 1) < (1 + (sqrt 5)) to_power (m + 1) by A36, XXREAL_0:2; :: thesis:

end;

2 to_power (m + 1) > 0 by POWER:34;
then ((1 - (sqrt 5)) to_power (m + 1)) / (2 to_power (m + 1)) < ((1 + (sqrt 5)) to_power (m + 1)) / (2 to_power (m + 1)) by A35, XREAL_1:74;
then ((1 - (sqrt 5)) / 2) to_power (m + 1) < ((1 + (sqrt 5)) to_power (m + 1)) / (2 to_power (m + 1)) by Th1;
then ( tau_bar to_power (m + 1) < tau to_power (m + 1) & tau_bar to_power n < 0 ) by A1, Th7, Th1, FIB_NUM:def 1, FIB_NUM:def 2;
then (tau_bar to_power (m + 1)) * (tau_bar to_power n) > (tau to_power (m + 1)) * (tau_bar to_power n) by XREAL_1:69;
then ((tau_bar to_power (m + 1)) * (tau_bar to_power n)) + (tau to_power ((n + m) + 1)) > ((tau to_power (m + 1)) * (tau_bar to_power n)) + (tau to_power ((n + m) + 1)) by XREAL_1:6;
then (tau_bar to_power ((m + 1) + n)) + (tau to_power ((n + m) + 1)) > ((tau to_power (m + 1)) * (tau_bar to_power n)) + (tau to_power ((n + m) + 1)) by Th2;
then (tau_bar to_power ((m + 1) + n)) + (tau to_power ((n + m) + 1)) > ((tau to_power (m + 1)) * (tau_bar to_power n)) + ((tau to_power n) * (tau to_power (m + 1))) by Th2;
then Lucas ((n + m) + 1) > (tau to_power (m + 1)) * ((tau_bar to_power n) + (tau to_power n)) by FIB_NUM3:21;
hence S₁[m + 1] by FIB_NUM3:21; :: thesis:

end;

for m being non zero Nat holds S₁[m] from NAT_1:sch 10(A33, A34);
hence (((tau to_power k) * (Lucas n)) + 1) - 1 < Lucas (n + k) by A1; :: thesis:

end;

hence Lucas (n + k) = [\(((tau to_power k) * (Lucas n)) + 1)/] by A3, INT_1:def 6; :: thesis: