:: Representation of the {F}ibonacci and {L}ucas Numbers in Terms of the Floor and Ceiling Functor
:: by Magdalena Jastrz\c{e}bska
::
:: Received November 30, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users


begin

Lm1:  for m, n being Nat holds - m <= m * ((- 1) to_power n)
proofend;

Lm2:  for m, n being Nat holds - (m * ((- 1) to_power n)) >= - m
proofend;

theorem Th1: :: FIB_NUM4:1
for a, b being real number
for c being Nat holds (a / b) to_power c = (a to_power c) / (b to_power c)
proofend;

theorem Th2: :: FIB_NUM4:2
for a being real number
for b, c being integer number st a <> 0 holds
a to_power (b + c) = (a to_power b) * (a to_power c)
proofend;

theorem Th3: :: FIB_NUM4:3
for n being Nat
for a being real number st n is even &amp; a <> 0 holds
(- a) to_power n = a to_power n by POWER:47;

theorem Th4: :: FIB_NUM4:4
for n being Nat
for a being real number st n is odd &amp; a <> 0 holds
(- a) to_power n = - (a to_power n) by POWER:48;

Lm3:  tau * tau_bar = - 1
proofend;

Lm4:  tau_bar / tau = ((sqrt 5) - 3) / 2
proofend;

Lm5:  tau / tau_bar = ((- 3) - (sqrt 5)) / 2
proofend;

Lm6:  tau to_power 2 = (3 + (sqrt 5)) / 2
proofend;

Lm7:  tau_bar to_power 2 = (3 - (sqrt 5)) / 2
proofend;

Lm8:  tau_bar to_power 3 = 2 - (sqrt 5)
proofend;

Lm9:  tau_bar to_power 6 = 9 - (4 * (sqrt 5))
proofend;

theorem Th5: :: FIB_NUM4:5
abs tau_bar < 1
proofend;

Lm10:  for n being Nat holds ((abs tau_bar) to_power n) * (1 / (sqrt 5)) > 0
proofend;

Lm11:  for n being Nat holds ((abs tau_bar) to_power n) * (1 / (sqrt 5)) < 1 / 2
proofend;

theorem Th6: :: FIB_NUM4:6
for n being Nat
for r being non empty real number st n is even holds
r to_power n > 0
proofend;

theorem Th7: :: FIB_NUM4:7
for n being Nat
for r being real number st n is odd &amp; r < 0 holds
r to_power n < 0
proofend;

theorem Th8: :: FIB_NUM4:8
for n being Nat st n <> 0 holds
tau_bar to_power n < 1 / 2
proofend;

theorem :: FIB_NUM4:9
for n, m being Nat
for r being real number st m is odd &amp; n >= m &amp; r < 0 &amp; r > - 1 holds
r to_power n >= r to_power m
proofend;

theorem Th10: :: FIB_NUM4:10
for n, m being Nat st m is odd &amp; n >= m holds
tau_bar to_power n >= tau_bar to_power m
proofend;

theorem Th11: :: FIB_NUM4:11
for n, m being Nat st n is even &amp; m is even &amp; n >= m holds
tau_bar to_power n <= tau_bar to_power m
proofend;

theorem Th12: :: FIB_NUM4:12
for m, n being non empty Nat st m >= n holds
Lucas m >= Lucas n
proofend;

Lm12:  tau_bar ^2 = (3 - (sqrt 5)) / 2
by Lm7, POWER:46;

Lm13:  sqrt 5 > 0
by SQUARE_1:25;

then  (sqrt 5) + 3 > (- (sqrt 5)) + 3
by XREAL_1:6;

then  ((sqrt 5) + 3) / 2 > ((- (sqrt 5)) + 3) / 2
by XREAL_1:74;

then Lm14:  tau ^2 > tau_bar ^2
by Lm6, Lm12, POWER:46;

 sqrt 5 < sqrt (3 ^2)
by SQUARE_1:27;

then  sqrt 5 < 3
by SQUARE_1:def_2;

then  (sqrt 5) - 3 < 3 - 3
by XREAL_1:9;

then Lm15:  ((sqrt 5) - 3) / 2 < 0
;

theorem :: FIB_NUM4:13
for n being non empty Nat holds tau to_power n > tau_bar to_power n
proofend;

theorem Th14: :: FIB_NUM4:14
for n being Nat st n > 1 holds
- (1 / 2) < tau_bar to_power n
proofend;

theorem Th15: :: FIB_NUM4:15
for n being Nat st n > 2 holds
tau_bar to_power n >= - (1 / (sqrt 5))
proofend;

theorem Th16: :: FIB_NUM4:16
for n being Nat st n >= 2 holds
tau_bar to_power n <= 1 / (sqrt 5)
proofend;

theorem Th17: :: FIB_NUM4:17
for n being Nat holds
( ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) > 0 &amp; ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) < 1 )
proofend;

begin

theorem :: FIB_NUM4:18
for n being Nat holds [\(((tau to_power n) / (sqrt 5)) + (1 / 2))/] = Fib n
proofend;

theorem :: FIB_NUM4:19
for n being Nat st n <> 0 holds
[/(((tau to_power n) / (sqrt 5)) - (1 / 2))\] = Fib n
proofend;

set s5 = sqrt 5;

Lm16:  1 < sqrt 5
by SQUARE_1:18, SQUARE_1:27;

 1 - (sqrt 5) <> 0
by SQUARE_1:18, SQUARE_1:27;

then  (1 - (sqrt 5)) ^2 > 0
by SQUARE_1:12;

then Lm17:  (1 - (sqrt 5)) to_power 2 > 0
by POWER:46;

Lm18:  sqrt 5 > 0
by SQUARE_1:25;

 2 * 1 < 2 * (sqrt 5)
by Lm16, XREAL_1:68;

then  - (2 * (sqrt 5)) < - 2
by XREAL_1:24;

then  (- (2 * (sqrt 5))) + 6 < (- 2) + 6
by XREAL_1:8;

then  (1 - (2 * (sqrt 5))) + 5 < 4
;

then  ((1 ^2) - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2) < 4
by SQUARE_1:def_2;

then  (1 - (sqrt 5)) ^2 < 2 ^2
;

then  (1 - (sqrt 5)) ^2 < 2 to_power 2
by POWER:46;

then Lm19:  (1 - (sqrt 5)) to_power 2 < 2 to_power 2
by POWER:46;

theorem :: FIB_NUM4:20
for n being Nat st n <> 0 holds
[\((tau to_power (2 * n)) / (sqrt 5))/] = Fib (2 * n)
proofend;

theorem :: FIB_NUM4:21
for n being Nat holds [/((tau to_power ((2 * n) + 1)) / (sqrt 5))\] = Fib ((2 * n) + 1)
proofend;

theorem Th22: :: FIB_NUM4:22
for n being Nat st n >= 2 &amp; n is even holds
Fib (n + 1) = [\((tau * (Fib n)) + 1)/]
proofend;

theorem Th23: :: FIB_NUM4:23
for n being Nat st n >= 2 &amp; n is odd holds
Fib (n + 1) = [/((tau * (Fib n)) - 1)\]
proofend;

theorem Th24: :: FIB_NUM4:24
for n being Nat st n >= 2 holds
Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/]
proofend;

theorem :: FIB_NUM4:25
for n being Nat st n >= 2 holds
Fib (n + 1) = [/((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2)\]
proofend;

theorem :: FIB_NUM4:26
for n being Nat holds Fib (n + 1) = ((Fib n) + (sqrt ((5 * ((Fib n) ^2)) + (4 * ((- 1) to_power n))))) / 2
proofend;

theorem :: FIB_NUM4:27
for n being Nat st n >= 2 holds
Fib (n + 1) = [\((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1))) / 2)/]
proofend;

Lm20:  sqrt 5 > 0
by SQUARE_1:25;

Lm21: (sqrt 5) / (((sqrt 5) - 5) * tau) = (sqrt 5) / (((sqrt 5) - ((sqrt 5) ^2)) * tau) by SQUARE_1:def_2
.= (sqrt 5) / ((sqrt 5) * ((1 - (sqrt 5)) * tau))
.= ((sqrt 5) / (sqrt 5)) / ((1 - (sqrt 5)) * tau) by XCMPLX_1:78
.= 1 / (((1 - (sqrt 5)) * (1 + (sqrt 5))) / 2) by Lm20, FIB_NUM:def_1, XCMPLX_1:60
.= (1 * 2) / ((1 - (sqrt 5)) * (1 + (sqrt 5))) by XCMPLX_1:77
.= 2 / ((1 ^2) - ((sqrt 5) ^2))
.= 2 / ((1 ^2) - 5) by SQUARE_1:def_2
.= - (1 / 2) ;

theorem :: FIB_NUM4:28
for n being Nat st n >= 2 holds
Fib n = [\((1 / tau) * ((Fib (n + 1)) + (1 / 2)))/]
proofend;

Lm22:  sqrt 5 > 1
by SQUARE_1:18, SQUARE_1:27;

then Lm23:  ( (sqrt 5) - 1 > 1 - 1 &amp; sqrt 5 > 0 )
by XREAL_1:9;

 sqrt 5 > 2
by SQUARE_1:20, SQUARE_1:27;

then  - (sqrt 5) < - 2
by XREAL_1:24;

then  (- (sqrt 5)) + 5 < (- 2) + 5
by XREAL_1:6;

then  (- (sqrt 5)) + ((sqrt 5) ^2) < 3
by SQUARE_1:def_2;

then  ((sqrt 5) * ((sqrt 5) - 1)) / 5 < 3 / 5
by XREAL_1:74;

then  ((sqrt 5) - 1) * ((sqrt 5) / 5) < 6 / 10
;

then  ((sqrt 5) - 1) * ((sqrt 5) / ((sqrt 5) ^2)) < 6 / 10
by SQUARE_1:def_2;

then  ( ((sqrt 5) - 1) * ((1 * (sqrt 5)) / ((sqrt 5) * (sqrt 5))) < 6 / 10 &amp; sqrt 5 > 0 )
by SQUARE_1:25;

then  ((sqrt 5) - 1) * (1 / (sqrt 5)) < 6 / 10
by XCMPLX_1:91;

then Lm24:  ((sqrt 5) - 1) / (sqrt 5) < 6 / 10
by XCMPLX_1:99;

 sqrt ((3 / 2) ^2) <= sqrt 5
by SQUARE_1:26;

then  3 / 2 <= sqrt 5
by SQUARE_1:def_2;

then  (3 / 2) * 2 <= (sqrt 5) * 2
by XREAL_1:64;

then Lm25:  3 / 4 <= (2 * (sqrt 5)) / (2 * 2)
by XREAL_1:72;

Lm26:  ( (sqrt 5) - 1 > 1 - 1 &amp; sqrt 5 > 0 )
by Lm22, XREAL_1:9;

 ( (- 1) + (sqrt 5) < 0 + (sqrt 5) &amp; sqrt 5 > 0 )
by SQUARE_1:25, XREAL_1:6;

then  ( ((sqrt 5) - 1) / (sqrt 5) < (sqrt 5) / (sqrt 5) &amp; sqrt 5 > 0 )
by XREAL_1:74;

then Lm27:  ((sqrt 5) - 1) / (sqrt 5) < 1
by XCMPLX_1:60;

 sqrt 5 < sqrt (3 ^2)
by SQUARE_1:27;

then  sqrt 5 < 3
by SQUARE_1:def_2;

then  - (sqrt 5) > - 3
by XREAL_1:24;

then Lm28:  (- (sqrt 5)) + 3 > (- 3) + 3
by XREAL_1:6;

 - (sqrt 5) < - 1
by Lm22, XREAL_1:24;

then  (- (sqrt 5)) + 3 < (- 1) + 3
by XREAL_1:6;

then Lm29:  (3 - (sqrt 5)) / 2 < 2 / 2
by XREAL_1:74;

theorem :: FIB_NUM4:29
for n, k being Nat st ( ( n >= k &amp; k > 1 ) or ( k = 1 &amp; n > k ) ) holds
[\(((tau to_power k) * (Fib n)) + (1 / 2))/] = Fib (n + k)
proofend;

begin

theorem :: FIB_NUM4:30
for n being Nat st n >= 2 holds
Lucas n = [\((tau to_power n) + (1 / 2))/]
proofend;

theorem :: FIB_NUM4:31
for n being Nat st n >= 2 holds
Lucas n = [/((tau to_power n) - (1 / 2))\]
proofend;

theorem :: FIB_NUM4:32
for n being Nat st n >= 2 holds
Lucas (2 * n) = [/(tau to_power (2 * n))\]
proofend;

theorem :: FIB_NUM4:33
for n being Nat st n >= 2 holds
Lucas ((2 * n) + 1) = [\(tau to_power ((2 * n) + 1))/]
proofend;

theorem :: FIB_NUM4:34
for n being Nat st n >= 2 &amp; n is odd holds
Lucas (n + 1) = [\((tau * (Lucas n)) + 1)/]
proofend;

theorem :: FIB_NUM4:35
for n being Nat st n >= 2 &amp; n is even holds
Lucas (n + 1) = [/((tau * (Lucas n)) - 1)\]
proofend;

theorem :: FIB_NUM4:36
for n being Nat st n <> 1 holds
Lucas (n + 1) = ((Lucas n) + (sqrt (5 * (((Lucas n) ^2) - (4 * ((- 1) to_power n)))))) / 2
proofend;

theorem :: FIB_NUM4:37
for n being Nat st n >= 4 holds
Lucas (n + 1) = [\((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) / 2)/]
proofend;

theorem :: FIB_NUM4:38
for n being Nat st n > 2 holds
Lucas n = [\((1 / tau) * ((Lucas (n + 1)) + (1 / 2)))/]
proofend;

theorem :: FIB_NUM4:39
for n, k being Nat st n >= 4 &amp; k >= 1 &amp; n > k &amp; n is odd holds
Lucas (n + k) = [\(((tau to_power k) * (Lucas n)) + 1)/]
proofend;