let n, k be natural number ; :: thesis: ( n >= 4 & k >= 1 & n > k & not n is even implies Lucas (n + k) = [\(((tau to_power k) * (Lucas n)) + 1)/] )
assume A0: ( n >= 4 & k >= 1 & n > k & not n is even ) ; :: thesis: Lucas (n + k) = [\(((tau to_power k) * (Lucas n)) + 1)/]
set tb = tau_bar ;
set tk = tau to_power k;
set tn = tau to_power n;
set tbn = tau_bar to_power n;
F: sqrt 5 > 1 by SQUARE_1:83, SQUARE_1:95;
A1: ((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
V1: n = k + m by A0, NAT_1:10;
V0: m is non empty Nat by A0, V1;
then h0: m >= 1 by NAT_1:14;
t1: ((((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 ( k is even or not k is even ) ;

suppose W1: k is even ; :: thesis: ((((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))

then W2: not m is even by A0, V1;
m1: 2 to_power m > 0 by POWER:39;
W3: ((((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 W1, FIB_NUM2:5
.= (((- ((- 1) + (sqrt 5))) to_power m) / (2 to_power m)) + ((2 to_power m) / (2 to_power m)) by m1, XCMPLX_1:60
.= ((((- 1) * ((sqrt 5) - 1)) to_power m) + (2 to_power m)) / (2 to_power m) by XCMPLX_1:63
.= ((((- 1) to_power m) * (((sqrt 5) - 1) to_power m)) + (2 to_power m)) / (2 to_power m) by NEWTON:12
.= ((2 to_power m) + ((- 1) * (((sqrt 5) - 1) to_power m))) / (2 to_power m) by W2, FIB_NUM2:3
.= ((2 to_power m) - (((sqrt 5) - 1) to_power m)) / (2 to_power m) ;
z: ( sqrt (3 ^2 ) > sqrt 5 & sqrt 5 > sqrt 1 ) by SQUARE_1:95;
then ( 3 > sqrt 5 & sqrt 5 > 1 ) by SQUARE_1:83, SQUARE_1:def 4;
then ( 3 - 1 > (sqrt 5) - 1 & (sqrt 5) - 1 > 1 - 1 ) by XREAL_1:11;
then 2 to_power m > ((sqrt 5) - 1) to_power m by V0, POWER:42;
then w4: (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:11;
W5: ((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:12
.= ((- 1) * (((- 1) + (sqrt 5)) to_power ((2 * k) + m))) / (2 to_power ((2 * k) + m)) by W2, FIB_NUM2:3
.= (- 1) * ((((- 1) + (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m))) by XCMPLX_1:75 ;
(sqrt 5) - 1 > 1 - 1 by z, SQUARE_1:83, XREAL_1:11;
then ((- 1) + (sqrt 5)) to_power ((2 * k) + m) > 0 by POWER:39;
then ((1 - (sqrt 5)) to_power ((2 * k) + m)) / (2 to_power ((2 * k) + m)) <= 0 by W5;
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 w4, W3; :: thesis: verum

end;

suppose W1: not k is even ; :: thesis: ((((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))

then W2: m is even by A0, V1;
m1: 2 to_power m > 0 by POWER:39;
m2: 2 to_power (2 * k) > 0 by POWER:39;
m > 1 by W2, h0, POLYFORM:4, XXREAL_0:1;
then V2: m - 1 is non empty Nat by NAT_1:20;
W3: ((((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 W1, FIB_NUM2:3
.= ((((1 - (sqrt 5)) to_power m) * (- 1)) / (2 to_power m)) + ((2 to_power m) / (2 to_power m)) by m1, XCMPLX_1:60
.= (((((- 1) * ((- 1) + (sqrt 5))) to_power m) * (- 1)) + (2 to_power m)) / (2 to_power m) by XCMPLX_1:63
.= (((((- 1) to_power m) * (((- 1) + (sqrt 5)) to_power m)) * (- 1)) + (2 to_power m)) / (2 to_power m) by NEWTON:12
.= (((1 * (((- 1) + (sqrt 5)) to_power m)) * (- 1)) + (2 to_power m)) / (2 to_power m) by W2, FIB_NUM2:5
.= (((- (((- 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 m2, XCMPLX_1:92
.= ((- ((((- 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 JakPower32
.= ((- ((((- 1) + (sqrt 5)) to_power m) * (2 to_power (2 * k)))) + (2 to_power (m + (2 * k)))) / (2 to_power (m + (2 * k))) by JakPower32
.= ((2 to_power (m + (2 * k))) - ((((- 1) + (sqrt 5)) to_power m) * (2 to_power (2 * k)))) / (2 to_power (m + (2 * k))) ;
W4: ((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:12
.= (1 * (((- 1) + (sqrt 5)) to_power ((2 * k) + m))) / (2 to_power ((2 * k) + m)) by W2, FIB_NUM2:5
.= (((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);
S1: (2 to_power (1 + 1)) - (((sqrt 5) - 1) to_power (1 + 1)) = (2 ^2 ) - (((sqrt 5) - 1) to_power 2) by POWER:53
.= 4 - (((sqrt 5) - 1) ^2 ) by POWER:53
.= 4 - ((((sqrt 5) ^2 ) - ((2 * (sqrt 5)) * 1)) + (1 ^2 ))
.= 4 - ((5 - (2 * (sqrt 5))) + 1) by SQUARE_1:def 4
.= (2 * (sqrt 5)) - 2 ;
S2: ((sqrt 5) - 1) to_power (1 + 1) = ((sqrt 5) - 1) ^2 by POWER:53
.= (((sqrt 5) ^2 ) - ((2 * (sqrt 5)) * 1)) + (1 ^2 )
.= (5 - (2 * (sqrt 5))) + 1 by SQUARE_1:def 4
.= 6 - (2 * (sqrt 5)) ;
sqrt 5 >= sqrt (2 ^2 ) by SQUARE_1:95;
then sqrt 5 >= 2 by SQUARE_1:def 4;
then (sqrt 5) * 4 >= 2 * 4 by XREAL_1:66;
then (((sqrt 5) * 2) + ((sqrt 5) * 2)) - 2 >= (6 + 2) - 2 by XREAL_1:11;
then ((((sqrt 5) * 2) + ((sqrt 5) * 2)) - 2) - (2 * (sqrt 5)) >= 6 - (2 * (sqrt 5)) by XREAL_1:11;
then B1: S₁[1] by S1, S2;
B2: for k being non empty Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non empty Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
X1: (sqrt 5) - 1 > 1 - 1 by F, XREAL_1:11;
assume S₁[k] ; :: thesis: S₁[k + 1]
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:8;
then (2 to_power (k + 1)) * ((sqrt 5) - 1) >= (2 * (((sqrt 5) - 1) to_power (k + 1))) * ((sqrt 5) - 1) by X1, XREAL_1:66;
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)) by POWER:30;
then BT: (2 to_power (k + 1)) * ((sqrt 5) - 1) >= 2 * (((sqrt 5) - 1) to_power ((k + 1) + 1)) by JakPower32, X1;
sqrt (3 ^2 ) >= sqrt 5 by SQUARE_1:95;
then 3 >= sqrt 5 by SQUARE_1:def 4;
then 3 - 1 >= (sqrt 5) - 1 by XREAL_1:11;
then 2 * (2 to_power (k + 1)) >= ((sqrt 5) - 1) * (2 to_power (k + 1)) by XREAL_1:66;
then (2 to_power 1) * (2 to_power (k + 1)) >= ((sqrt 5) - 1) * (2 to_power (k + 1)) by POWER:30;
then 2 to_power ((1 + k) + 1) >= ((sqrt 5) - 1) * (2 to_power (k + 1)) by JakPower32;
then 2 to_power ((1 + k) + 1) >= 2 * (((sqrt 5) - 1) to_power ((k + 1) + 1)) by BT, 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:11;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being non empty Nat holds S₁[k] from NAT_1:sch 10(B1, B2);
then (2 to_power ((m - 1) + 1)) - (((sqrt 5) - 1) to_power ((m - 1) + 1)) >= ((sqrt 5) - 1) to_power ((m - 1) + 1) by V2;
hence (2 to_power m) - (((sqrt 5) - 1) to_power m) >= ((sqrt 5) - 1) to_power m ; :: thesis: verum

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:66;
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 JakPower32;
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:74;
then w6: (((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 JakPower32;
X1: (sqrt 5) - 1 > 1 - 1 by F, XREAL_1:11;
( sqrt (3 ^2 ) > sqrt 5 & sqrt 5 > sqrt 1 ) by SQUARE_1:95;
then ( 3 > sqrt 5 & sqrt 5 > 1 ) by SQUARE_1:83, SQUARE_1:def 4;
then M4: ( 3 - 1 > (sqrt 5) - 1 & (sqrt 5) - 1 > 1 - 1 ) by XREAL_1:11;
then m5: ((sqrt 5) - 1) to_power m > 0 by POWER:39;
2 to_power (2 * k) >= ((sqrt 5) - 1) to_power (2 * k) by M4, A0, POWER:42;
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 m5, XREAL_1:66;
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:74;
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 w6, 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 JakPower32, X1;
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 W3, W4, JakPower32; :: thesis: verum

end;

end;

end;

(sqrt 5) - 1 > 1 - 1 by F, XREAL_1:11;
then YX: - ((sqrt 5) - 1) < 0 ;
((1 + (sqrt 5)) * (1 - (sqrt 5))) / (2 to_power 2) = ((1 + (sqrt 5)) * (1 - (sqrt 5))) / (2 ^2 ) by POWER:53
.= ((1 ^2 ) - ((sqrt 5) ^2 )) / 4
.= (1 - 5) / 4 by SQUARE_1:def 4
.= - 1 ;
then (- 1) to_power k = (((1 + (sqrt 5)) * (1 - (sqrt 5))) to_power k) / ((2 to_power 2) to_power k) by JakPower36
.= (((1 + (sqrt 5)) * (1 - (sqrt 5))) to_power k) / (2 to_power (2 * k)) by NEWTON:14 ;
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 t1, XCMPLX_1:75;
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:79;
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 JakPower32;
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:12;
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 JakPower32, YX;
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 V1, JakPower36;
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 JakPower32, V1, 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:77;
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 JakPower36;
hence ((tau to_power k) * (tau_bar to_power n)) + 1 >= tau_bar to_power (n + k) by JakPower36, FIB_NUM:def 1, FIB_NUM:def 2; :: thesis: verum

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:8;
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 JakPower32;
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: verum

end;

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

proof

defpred S₁[ Nat] means (tau to_power $1) * (Lucas n) < Lucas (n + $1);
tau_bar to_power n < 0 by pom2, A0;
then ((tau_bar to_power n) * tau ) - ((tau_bar to_power n) * tau_bar ) < 0 ;
then ((tau_bar to_power n) * tau ) - ((tau_bar to_power n) * (tau_bar to_power 1)) < 0 by POWER:30;
then ((tau_bar to_power n) * tau ) - (tau_bar to_power (n + 1)) < 0 by JakPower32;
then (((tau_bar to_power n) * tau ) - (tau_bar to_power (n + 1))) + ((tau to_power (n + 1)) + (tau_bar to_power (n + 1))) < 0 + ((tau to_power (n + 1)) + (tau_bar to_power (n + 1))) by XREAL_1:8;
then ((tau_bar to_power n) * tau ) + (tau to_power (n + 1)) < Lucas (n + 1) by FIB_NUM3:21;
then ((tau_bar to_power n) * tau ) + ((tau to_power n) * (tau to_power 1)) < Lucas (n + 1) by JakPower32;
then ((tau_bar to_power n) * tau ) + ((tau to_power n) * tau ) < Lucas (n + 1) by POWER:30;
then ((tau_bar to_power n) + (tau to_power n)) * tau < Lucas (n + 1) ;
then (Lucas n) * tau < Lucas (n + 1) by FIB_NUM3:21;
then B1: S₁[1] by POWER:30;
B2: for m being non empty Nat st S₁[m] holds
S₁[m + 1]

proof

let m be non empty Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume S₁[m] ; :: thesis: S₁[m + 1]
K1: (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 13;
(1 - (sqrt 5)) to_power s <= abs ((1 - (sqrt 5)) to_power s) by ABSVALUE:11;
then a1: (1 - (sqrt 5)) to_power s <= (abs (1 - (sqrt 5))) to_power s by SERIES_1:2;
sqrt 5 > sqrt 1 by SQUARE_1:95;
then - (sqrt 5) < - 1 by SQUARE_1:83, XREAL_1:26;
then a2: (- (sqrt 5)) + 1 < (- 1) + 1 by XREAL_1:8;
then A5: abs (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:8;
then (abs (1 - (sqrt 5))) to_power s < (1 + (sqrt 5)) to_power s by A5, a2, POWER:42;
hence (1 - (sqrt 5)) to_power (m + 1) < (1 + (sqrt 5)) to_power (m + 1) by a1, XXREAL_0:2; :: thesis: verum

end;

2 to_power (m + 1) > 0 by POWER:39;
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 K1, XREAL_1:76;
then ((1 - (sqrt 5)) / 2) to_power (m + 1) < ((1 + (sqrt 5)) to_power (m + 1)) / (2 to_power (m + 1)) by JakPower36;
then ( tau_bar to_power (m + 1) < tau to_power (m + 1) & tau_bar to_power n < 0 ) by A0, pom2, JakPower36, 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:71;
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:8;
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 JakPower32;
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 JakPower32;
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: verum

end;

for m being non empty Nat holds S₁[m] from NAT_1:sch 10(B1, B2);
hence (((tau to_power k) * (Lucas n)) + 1) - 1 < Lucas (n + k) by A0; :: thesis: verum

end;

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