let n, k be Nat; ( n >= 4 & k >= 1 & n > k & n is odd implies Lucas (n + k) = [\(((tau to_power k) * (Lucas n)) + 1)/] )
assume A1:
( n >= 4 & k >= 1 & n > k & n is odd )
; 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;
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
( k is even or k is odd )
;
suppose A8:
k is
even
;
((((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 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;
verum end; suppose A15:
k is
odd
;
((((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 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
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;
verum end; end;
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;
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: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;
verum
end;
(((tau to_power k) * (Lucas n)) + 1) - 1 < Lucas (n + k)
hence
Lucas (n + k) = [\(((tau to_power k) * (Lucas n)) + 1)/]
by A3, INT_1:def 6; verum