let n be Nat; ( 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
; 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
;
(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;
verum 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)
;
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
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
((((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)
;
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; verum