:: 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 Association of Mizar Users

begin

tt1: for m, n being natural number holds - m <= m * ((- 1) to_power n)

proof end;

tt2: for m, n being natural number holds - (m * ((- 1) to_power n)) >= - m

proof end;

theorem JakPower36: :: FIB_NUM4:1

for a, b being real number
for c being natural number holds (a / b) to_power c = (a to_power c) / (b to_power c)

proof end;

theorem JakPower32: :: 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)

proof end;

theorem pomoc1: :: FIB_NUM4:3

for n being natural number
for a being real number st n is even & a <> 0 holds
(- a) to_power n = a to_power n

proof end;

theorem pomoc2: :: FIB_NUM4:4

for n being natural number
for a being real number st not n is even & a <> 0 holds
(- a) to_power n = - (a to_power n)

proof end;

albet3: tau * tau_bar = - 1

proof end;

albet2: tau_bar / tau = ((sqrt 5) - 3) / 2

proof end;

albet4: tau / tau_bar = ((- 3) - (sqrt 5)) / 2

proof end;

alfa2: tau to_power 2 = (3 + (sqrt 5)) / 2

proof end;

beta2: tau_bar to_power 2 = (3 - (sqrt 5)) / 2

proof end;

beta3: tau_bar to_power 3 = 2 - (sqrt 5)

proof end;

beta6: tau_bar to_power 6 = 9 - (4 * (sqrt 5))

proof end;

theorem hop3: :: FIB_NUM4:5

abs tau_bar < 1

proof end;

hop2: for n being natural number holds ((abs tau_bar ) to_power n) * (1 / (sqrt 5)) > 0

proof end;

hop4: for n being natural number holds ((abs tau_bar ) to_power n) * (1 / (sqrt 5)) < 1 / 2

proof end;

theorem pom1: :: FIB_NUM4:6

for n being natural number
for r being non empty real number st n is even holds
r to_power n > 0

proof end;

theorem pom2: :: FIB_NUM4:7

for n being natural number
for r being real number st not n is even & r < 0 holds
r to_power n < 0

proof end;

theorem hop8: :: FIB_NUM4:8

for n being natural number st n <> 0 holds
tau_bar to_power n < 1 / 2

proof end;

theorem :: FIB_NUM4:9

for n, m being natural number
for r being real number st not m is even & n >= m & r < 0 & r > - 1 holds
r to_power n >= r to_power m

proof end;

theorem hopp9: :: FIB_NUM4:10

for n, m being natural number st not m is even & n >= m holds
tau_bar to_power n >= tau_bar to_power m

proof end;

theorem hopp10: :: FIB_NUM4:11

for n, m being natural number st n is even & m is even & n >= m holds
tau_bar to_power n <= tau_bar to_power m

proof end;

theorem luc1: :: FIB_NUM4:12

for m, n being non empty natural number st m >= n holds
Lucas m >= Lucas n

proof end;

C2: tau_bar ^2 = (3 - (sqrt 5)) / 2
by beta2, POWER:53;

d3: sqrt 5 > 0
by SQUARE_1:93;

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

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

then B0: tau ^2 > tau_bar ^2
by alfa2, POWER:53, C2;

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

then sqrt 5 < 3
by SQUARE_1:def 4;

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

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

theorem :: FIB_NUM4:13

for n being non empty natural number holds tau to_power n > tau_bar to_power n

proof end;

theorem hop9: :: FIB_NUM4:14

for n being natural number st n > 1 holds
- (1 / 2) < tau_bar to_power n

proof end;

theorem mag1: :: FIB_NUM4:15

for n being natural number st n > 2 holds
tau_bar to_power n >= - (1 / (sqrt 5))

proof end;

theorem mag2: :: FIB_NUM4:16

for n being natural number st n >= 2 holds
tau_bar to_power n <= 1 / (sqrt 5)

proof end;

theorem Lemat11: :: FIB_NUM4:17

for n being natural number holds
( ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) > 0 & ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) < 1 )

proof end;

begin

theorem :: FIB_NUM4:18

for n being natural number holds [\(((tau to_power n) / (sqrt 5)) + (1 / 2))/] = Fib n

proof end;

theorem :: FIB_NUM4:19

for n being natural number st n <> 0 holds
[/(((tau to_power n) / (sqrt 5)) - (1 / 2))\] = Fib n

proof end;

set s5 = sqrt 5;

d0: 1 < sqrt 5
by SQUARE_1:83, SQUARE_1:95;

1 - (sqrt 5) <> 0
by SQUARE_1:83, SQUARE_1:95;

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

then d1: (1 - (sqrt 5)) to_power 2 > 0
by POWER:53;

d3: sqrt 5 > 0
by SQUARE_1:93;

2 * 1 < 2 * (sqrt 5)
by XREAL_1:70, d0;

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

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

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

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

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

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

then xx: (1 - (sqrt 5)) to_power 2 < 2 to_power 2
by POWER:53;

theorem :: FIB_NUM4:20

for n being natural number st n <> 0 holds
[\((tau to_power (2 * n)) / (sqrt 5))/] = Fib (2 * n)

proof end;

theorem :: FIB_NUM4:21

for n being natural number holds [/((tau to_power ((2 * n) + 1)) / (sqrt 5))\] = Fib ((2 * n) + 1)

proof end;

theorem Tw13a: :: FIB_NUM4:22

for n being natural number st n >= 2 & n is even holds
Fib (n + 1) = [\((tau * (Fib n)) + 1)/]

proof end;

theorem Tw13b: :: FIB_NUM4:23

for n being natural number st n >= 2 & not n is even holds
Fib (n + 1) = [/((tau * (Fib n)) - 1)\]

proof end;

theorem Wn14: :: FIB_NUM4:24

for n being natural number st n >= 2 holds
Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/]

proof end;

theorem :: FIB_NUM4:25

for n being natural number st n >= 2 holds
Fib (n + 1) = [/((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2)\]

proof end;

theorem :: FIB_NUM4:26

for n being natural number holds Fib (n + 1) = ((Fib n) + (sqrt ((5 * ((Fib n) ^2 )) + (4 * ((- 1) to_power n))))) / 2

proof end;

theorem :: FIB_NUM4:27

for n being natural number st n >= 2 holds
Fib (n + 1) = [\((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2 )) - (2 * (Fib n))) + 1))) / 2)/]

proof end;

B2: sqrt 5 > 0
by SQUARE_1:93;

D1: (sqrt 5) / (((sqrt 5) - 5) * tau ) = (sqrt 5) / (((sqrt 5) - ((sqrt 5) ^2 )) * tau ) by SQUARE_1:def 4
.= (sqrt 5) / ((sqrt 5) * ((1 - (sqrt 5)) * tau ))
.= ((sqrt 5) / (sqrt 5)) / ((1 - (sqrt 5)) * tau ) by XCMPLX_1:79
.= 1 / (((1 - (sqrt 5)) * (1 + (sqrt 5))) / 2) by XCMPLX_1:60, B2, FIB_NUM:def 1
.= (1 * 2) / ((1 - (sqrt 5)) * (1 + (sqrt 5))) by XCMPLX_1:78
.= 2 / ((1 ^2 ) - ((sqrt 5) ^2 ))
.= 2 / ((1 ^2 ) - 5) by SQUARE_1:def 4
.= - (1 / 2) ;

theorem :: FIB_NUM4:28

for n being natural number st n >= 2 holds
Fib n = [\((1 / tau ) * ((Fib (n + 1)) + (1 / 2)))/]

proof end;

tt: sqrt 5 > 1
by SQUARE_1:83, SQUARE_1:95;

then y2: ( (sqrt 5) - 1 > 1 - 1 & sqrt 5 > 0 )
by XREAL_1:11;

sqrt 5 > 2
by SQUARE_1:85, SQUARE_1:95;

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

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

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

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

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

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

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

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

then Y3: ((sqrt 5) - 1) / (sqrt 5) < 6 / 10
by XCMPLX_1:100;

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

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

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

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

r2: ( (sqrt 5) - 1 > 1 - 1 & sqrt 5 > 0 )
by XREAL_1:11, tt;

( (- 1) + (sqrt 5) < 0 + (sqrt 5) & sqrt 5 > 0 )
by XREAL_1:8, SQUARE_1:93;

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

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

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

then sqrt 5 < 3
by SQUARE_1:def 4;

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

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

- (sqrt 5) < - 1
by XREAL_1:26, tt;

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

then xx: (3 - (sqrt 5)) / 2 < 2 / 2
by XREAL_1:76;

theorem :: FIB_NUM4:29

for n, k being natural number st ( ( n >= k & k > 1 ) or ( k = 1 & n > k ) ) holds
[\(((tau to_power k) * (Fib n)) + (1 / 2))/] = Fib (n + k)

proof end;

begin

theorem :: FIB_NUM4:30

for n being natural number st n >= 2 holds
Lucas n = [\((tau to_power n) + (1 / 2))/]

proof end;

theorem :: FIB_NUM4:31

for n being natural number st n >= 2 holds
Lucas n = [/((tau to_power n) - (1 / 2))\]

proof end;

theorem :: FIB_NUM4:32

for n being natural number st n >= 2 holds
Lucas (2 * n) = [/(tau to_power (2 * n))\]

proof end;

theorem :: FIB_NUM4:33

for n being natural number st n >= 2 holds
Lucas ((2 * n) + 1) = [\(tau to_power ((2 * n) + 1))/]

proof end;

theorem :: FIB_NUM4:34

for n being natural number st n >= 2 & not n is even holds
Lucas (n + 1) = [\((tau * (Lucas n)) + 1)/]

proof end;

theorem :: FIB_NUM4:35

for n being natural number st n >= 2 & n is even holds
Lucas (n + 1) = [/((tau * (Lucas n)) - 1)\]

proof end;

theorem :: FIB_NUM4:36

for n being natural number st n <> 1 holds
Lucas (n + 1) = ((Lucas n) + (sqrt (5 * (((Lucas n) ^2 ) - (4 * ((- 1) to_power n)))))) / 2

proof end;

theorem :: FIB_NUM4:37

for n being natural number st n >= 4 holds
Lucas (n + 1) = [\((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2 )) - (2 * (Lucas n))) + 1))) / 2)/]

proof end;

theorem :: FIB_NUM4:38

for n being natural number st n > 2 holds
Lucas n = [\((1 / tau ) * ((Lucas (n + 1)) + (1 / 2)))/]

proof end;

theorem :: FIB_NUM4:39

for n, k being natural number st n >= 4 & k >= 1 & n > k & not n is even holds
Lucas (n + k) = [\(((tau to_power k) * (Lucas n)) + 1)/]

proof end;