:: by Magdalena Jastrz\c{e}bska

::

:: Received November 30, 2009

:: Copyright (c) 2009-2021 Association of Mizar Users

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

proof end;

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

proof end;

theorem Th2: :: FIB_NUM4:2

for a being Real

for b, c being Integer st a <> 0 holds

a to_power (b + c) = (a to_power b) * (a to_power c)

for b, c being Integer st a <> 0 holds

a to_power (b + c) = (a to_power b) * (a to_power c)

proof end;

Lm3: tau * tau_bar = - 1

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

Lm10: for n being Nat holds (|.tau_bar.| to_power n) * (1 / (sqrt 5)) > 0

proof end;

Lm11: for n being Nat holds (|.tau_bar.| to_power n) * (1 / (sqrt 5)) < 1 / 2

proof end;

theorem :: FIB_NUM4:9

for n, m being Nat

for r being Real st m is odd & n >= m & r < 0 & r > - 1 holds

r to_power n >= r to_power m

for r being Real st m is odd & n >= m & r < 0 & r > - 1 holds

r to_power n >= r to_power m

proof end;

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 Th17: :: FIB_NUM4:17

for n being Nat holds

( ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) > 0 & ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) < 1 )

( ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) > 0 & ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) < 1 )

proof end;

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:26

for n being Nat 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 Nat st n >= 2 holds

Fib (n + 1) = [\((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1))) / 2)/]

Fib (n + 1) = [\((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1))) / 2)/]

proof end;

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) ;

Lm22: sqrt 5 > 1

by SQUARE_1:18, SQUARE_1:27;

then Lm23: ( (sqrt 5) - 1 > 1 - 1 & 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 & 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 & sqrt 5 > 0 )

by Lm22, XREAL_1:9;

( (- 1) + (sqrt 5) < 0 + (sqrt 5) & sqrt 5 > 0 )

by SQUARE_1:25, XREAL_1:6;

then ( ((sqrt 5) - 1) / (sqrt 5) < (sqrt 5) / (sqrt 5) & 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 & k > 1 ) or ( k = 1 & n > k ) ) holds

[\(((tau to_power k) * (Fib n)) + (1 / 2))/] = Fib (n + k)

[\(((tau to_power k) * (Fib n)) + (1 / 2))/] = Fib (n + k)

proof end;

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

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 Nat st n >= 4 holds

Lucas (n + 1) = [\((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) / 2)/]

Lucas (n + 1) = [\((((Lucas n) + 1) + (sqrt (((5 * ((Lucas n) ^2)) - (2 * (Lucas n))) + 1))) / 2)/]

proof end;

theorem :: FIB_NUM4:39

for n, k being Nat st n >= 4 & k >= 1 & n > k & n is odd holds

Lucas (n + k) = [\(((tau to_power k) * (Lucas n)) + 1)/]

Lucas (n + k) = [\(((tau to_power k) * (Lucas n)) + 1)/]

proof end;