:: FIB_NUM4 semantic presentation begin Lm1: for m, n being Nat holds - m <= m * ((- 1) to_power n) proof let m, n be Nat; ::_thesis: - m <= m * ((- 1) to_power n) ( n is even or n is odd ) ; then ( (- 1) to_power n = 1 or (- 1) to_power n = - 1 ) by FIB_NUM2:2, FIB_NUM2:3; hence - m <= m * ((- 1) to_power n) ; ::_thesis: verum end; Lm2: for m, n being Nat holds - (m * ((- 1) to_power n)) >= - m proof let m, n be Nat; ::_thesis: - (m * ((- 1) to_power n)) >= - m ( n is even or n is odd ) ; then ( (- 1) to_power n = 1 or (- 1) to_power n = - 1 ) by FIB_NUM2:2, FIB_NUM2:3; hence - (m * ((- 1) to_power n)) >= - m ; ::_thesis: verum end; 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) proof let a, b be real number ; ::_thesis: for c being Nat holds (a / b) to_power c = (a to_power c) / (b to_power c) let c be Nat; ::_thesis: (a / b) to_power c = (a to_power c) / (b to_power c) (a / b) to_power c = (a * (1 / b)) |^ c by XCMPLX_1:99 .= (a to_power c) * ((1 / b) |^ c) by NEWTON:7 .= (a to_power c) * (1 / (b |^ c)) by PREPOWER:7 .= (a to_power c) / (b |^ c) by XCMPLX_1:99 ; hence (a / b) to_power c = (a to_power c) / (b to_power c) ; ::_thesis: verum end; 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) proof let a be real number ; ::_thesis: for b, c being integer number st a <> 0 holds a to_power (b + c) = (a to_power b) * (a to_power c) let b, c be integer number ; ::_thesis: ( a <> 0 implies a to_power (b + c) = (a to_power b) * (a to_power c) ) assume A1: a <> 0 ; ::_thesis: a to_power (b + c) = (a to_power b) * (a to_power c) thus (a to_power b) * (a to_power c) = (a #Z b) * (a to_power c) by POWER:43 .= (a #Z b) * (a #Z c) by POWER:43 .= a #Z (b + c) by A1, PREPOWER:44 .= a to_power (b + c) by POWER:43 ; ::_thesis: verum end; theorem Th3: :: FIB_NUM4:3 for n being Nat for a being real number st n is even & 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 & a <> 0 holds (- a) to_power n = - (a to_power n) by POWER:48; Lm3: tau * tau_bar = - 1 proof tau * tau_bar = ((1 ^2) - ((sqrt 5) ^2)) / 4 by FIB_NUM:def_1, FIB_NUM:def_2 .= (1 - 5) / 4 by SQUARE_1:def_2 ; hence tau * tau_bar = - 1 ; ::_thesis: verum end; Lm4: tau_bar / tau = ((sqrt 5) - 3) / 2 proof sqrt 5 > 1 by SQUARE_1:18, SQUARE_1:27; then - (sqrt 5) < - 1 by XREAL_1:24; then A1: (- (sqrt 5)) + 1 < (- 1) + 1 by XREAL_1:6; tau_bar / tau = ((1 - (sqrt 5)) * 2) / ((1 + (sqrt 5)) * 2) by FIB_NUM:def_1, FIB_NUM:def_2, XCMPLX_1:84 .= (1 - (sqrt 5)) / (1 + (sqrt 5)) by XCMPLX_1:91 .= ((1 - (sqrt 5)) * (1 - (sqrt 5))) / ((1 + (sqrt 5)) * (1 - (sqrt 5))) by A1, XCMPLX_1:91 .= ((1 - (2 * (sqrt 5))) + ((sqrt 5) ^2)) / ((1 ^2) - ((sqrt 5) ^2)) .= ((1 - (2 * (sqrt 5))) + 5) / ((1 ^2) - ((sqrt 5) ^2)) by SQUARE_1:def_2 .= (6 - (2 * (sqrt 5))) / ((1 ^2) - 5) by SQUARE_1:def_2 .= (2 * (3 - (sqrt 5))) / ((- 2) * 2) ; hence tau_bar / tau = ((sqrt 5) - 3) / 2 ; ::_thesis: verum end; Lm5: tau / tau_bar = ((- 3) - (sqrt 5)) / 2 proof A1: sqrt 5 > 0 by SQUARE_1:25; tau / tau_bar = ((1 + (sqrt 5)) * 2) / ((1 - (sqrt 5)) * 2) by FIB_NUM:def_1, FIB_NUM:def_2, XCMPLX_1:84 .= (1 + (sqrt 5)) / (1 - (sqrt 5)) by XCMPLX_1:91 .= ((1 + (sqrt 5)) * (1 + (sqrt 5))) / ((1 - (sqrt 5)) * (1 + (sqrt 5))) by A1, XCMPLX_1:91 .= ((1 + (sqrt 5)) * (1 + (sqrt 5))) / (1 - ((sqrt 5) ^2)) .= ((1 + (sqrt 5)) * (1 + (sqrt 5))) / (1 - 5) by SQUARE_1:def_2 .= ((1 + (2 * (sqrt 5))) + ((sqrt 5) ^2)) / (- 4) .= ((1 + (2 * (sqrt 5))) + 5) / (- 4) by SQUARE_1:def_2 ; hence tau / tau_bar = ((- 3) - (sqrt 5)) / 2 ; ::_thesis: verum end; Lm6: tau to_power 2 = (3 + (sqrt 5)) / 2 proof tau to_power 2 = ((1 + (sqrt 5)) / 2) ^2 by FIB_NUM:def_1, POWER:46 .= (((1 ^2) + ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) / 4 .= ((1 + (2 * (sqrt 5))) + 5) / 4 by SQUARE_1:def_2 .= (2 * (3 + (sqrt 5))) / (2 * 2) ; hence tau to_power 2 = (3 + (sqrt 5)) / 2 ; ::_thesis: verum end; Lm7: tau_bar to_power 2 = (3 - (sqrt 5)) / 2 proof tau_bar to_power 2 = ((1 - (sqrt 5)) / 2) ^2 by FIB_NUM:def_2, POWER:46 .= (((1 ^2) - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) / 4 .= ((1 - (2 * (sqrt 5))) + 5) / 4 by SQUARE_1:def_2 .= (2 * (3 - (sqrt 5))) / (2 * 2) ; hence tau_bar to_power 2 = (3 - (sqrt 5)) / 2 ; ::_thesis: verum end; Lm8: tau_bar to_power 3 = 2 - (sqrt 5) proof 1 < sqrt 5 by SQUARE_1:18, SQUARE_1:27; then A1: 1 - (sqrt 5) < (sqrt 5) - (sqrt 5) by XREAL_1:9; thus tau_bar to_power 3 = ((1 - (sqrt 5)) / 2) to_power (2 + 1) by FIB_NUM:def_2 .= (((1 - (sqrt 5)) / 2) to_power 2) * (((1 - (sqrt 5)) / 2) to_power 1) by Th2, A1 .= (((1 - (sqrt 5)) / 2) to_power 2) * ((1 - (sqrt 5)) / 2) by POWER:25 .= (((1 - (sqrt 5)) / 2) ^2) * ((1 - (sqrt 5)) / 2) by POWER:46 .= (((1 - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) * (1 - (sqrt 5))) / 8 .= (((1 - (2 * (sqrt 5))) + 5) * (1 - (sqrt 5))) / 8 by SQUARE_1:def_2 .= ((6 - (8 * (sqrt 5))) + (2 * ((sqrt 5) ^2))) / 8 .= ((6 - (8 * (sqrt 5))) + (2 * 5)) / 8 by SQUARE_1:def_2 .= 2 - (sqrt 5) ; ::_thesis: verum end; Lm9: tau_bar to_power 6 = 9 - (4 * (sqrt 5)) proof thus tau_bar to_power 6 = tau_bar to_power (3 * 2) .= (2 - (sqrt 5)) to_power 2 by Lm8, NEWTON:9 .= (2 - (sqrt 5)) ^2 by POWER:46 .= ((2 ^2) - ((2 * 2) * (sqrt 5))) + ((sqrt 5) ^2) .= (4 - (4 * (sqrt 5))) + 5 by SQUARE_1:def_2 .= 9 - (4 * (sqrt 5)) ; ::_thesis: verum end; theorem Th5: :: FIB_NUM4:5 abs tau_bar < 1 proof sqrt 5 < sqrt (3 ^2) by SQUARE_1:27; then sqrt 5 < 3 by SQUARE_1:def_2; then (sqrt 5) - 1 < (2 + 1) - 1 by XREAL_1:9; then - ((sqrt 5) - 1) > - 2 by XREAL_1:24; then (1 - (sqrt 5)) / 2 > (- 2) / 2 by XREAL_1:74; then A1: abs tau_bar < (abs (- 1)) + (abs 0) by FIB_NUM:def_2, MEASURE6:37; abs (- 1) = - (- 1) by ABSVALUE:def_1; then abs tau_bar < 1 + 0 by A1; hence abs tau_bar < 1 ; ::_thesis: verum end; Lm10: for n being Nat holds ((abs tau_bar) to_power n) * (1 / (sqrt 5)) > 0 proof let n be Nat; ::_thesis: ((abs tau_bar) to_power n) * (1 / (sqrt 5)) > 0 set b = tau_bar ; sqrt 5 > 0 by SQUARE_1:25; then ( (abs tau_bar) to_power n > 0 & 1 / (sqrt 5) > 0 ) by POWER:34; hence ((abs tau_bar) to_power n) * (1 / (sqrt 5)) > 0 ; ::_thesis: verum end; Lm11: for n being Nat holds ((abs tau_bar) to_power n) * (1 / (sqrt 5)) < 1 / 2 proof let n be Nat; ::_thesis: ((abs tau_bar) to_power n) * (1 / (sqrt 5)) < 1 / 2 A1: 2 < sqrt 5 by SQUARE_1:20, SQUARE_1:27; then A2: 2 / 2 < (sqrt 5) / 2 by XREAL_1:74; set b = tau_bar ; A3: sqrt 5 <> 0 by SQUARE_1:17, SQUARE_1:27; A4: sqrt 5 > 0 by SQUARE_1:25; percases ( n <> 0 or n = 0 ) ; supposeA5: n <> 0 ; ::_thesis: ((abs tau_bar) to_power n) * (1 / (sqrt 5)) < 1 / 2 ( abs tau_bar < 1 & abs tau_bar > 0 ) by Th5; then (abs tau_bar) to_power n < 1 to_power n by A5, POWER:37; then (abs tau_bar) to_power n < 1 by POWER:26; then (abs tau_bar) to_power n < (sqrt 5) / 2 by A2, XXREAL_0:2; then ((abs tau_bar) to_power n) / ((sqrt 5) / 1) < ((sqrt 5) / 2) / ((sqrt 5) / 1) by A4, XREAL_1:74; then ((abs tau_bar) to_power n) / (sqrt 5) < (1 * (sqrt 5)) / (2 * (sqrt 5)) by XCMPLX_1:84; then ((abs tau_bar) to_power n) * (1 / (sqrt 5)) < (1 * (sqrt 5)) / (2 * (sqrt 5)) by XCMPLX_1:99; hence ((abs tau_bar) to_power n) * (1 / (sqrt 5)) < 1 / 2 by A3, XCMPLX_1:91; ::_thesis: verum end; suppose n = 0 ; ::_thesis: ((abs tau_bar) to_power n) * (1 / (sqrt 5)) < 1 / 2 then (abs tau_bar) to_power n = 1 by POWER:24; hence ((abs tau_bar) to_power n) * (1 / (sqrt 5)) < 1 / 2 by A1, XREAL_1:76; ::_thesis: verum end; end; end; 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 proof let n be Nat; ::_thesis: for r being non empty real number st n is even holds r to_power n > 0 let r be non empty real number ; ::_thesis: ( n is even implies r to_power n > 0 ) assume A1: n is even ; ::_thesis: r to_power n > 0 percases ( r > 0 or r < 0 ) ; suppose r > 0 ; ::_thesis: r to_power n > 0 hence r to_power n > 0 by POWER:34; ::_thesis: verum end; supposeA2: r < 0 ; ::_thesis: r to_power n > 0 r to_power n = (- r) to_power n by Th3, A1; hence r to_power n > 0 by A2, POWER:34; ::_thesis: verum end; end; end; theorem Th7: :: FIB_NUM4:7 for n being Nat for r being real number st n is odd & r < 0 holds r to_power n < 0 proof let n be Nat; ::_thesis: for r being real number st n is odd & r < 0 holds r to_power n < 0 let r be real number ; ::_thesis: ( n is odd & r < 0 implies r to_power n < 0 ) assume A1: n is odd ; ::_thesis: ( not r < 0 or r to_power n < 0 ) assume A2: r < 0 ; ::_thesis: r to_power n < 0 A3: r to_power n = (- (- r)) to_power n .= - ((- r) to_power n) by Th4, A1, A2 ; (- r) to_power n > 0 by A2, POWER:34; hence r to_power n < 0 by A3; ::_thesis: verum end; theorem Th8: :: FIB_NUM4:8 for n being Nat st n <> 0 holds tau_bar to_power n < 1 / 2 proof let n be Nat; ::_thesis: ( n <> 0 implies tau_bar to_power n < 1 / 2 ) assume n <> 0 ; ::_thesis: tau_bar to_power n < 1 / 2 then n + 1 > 0 + 1 by XREAL_1:8; then n + 1 >= 1 + 1 by NAT_1:13; then A1: ( n + 1 = 2 or n >= 2 ) by NAT_1:8; percases ( n = 1 or n >= 2 ) by A1; suppose n = 1 ; ::_thesis: tau_bar to_power n < 1 / 2 hence tau_bar to_power n < 1 / 2 by POWER:25; ::_thesis: verum end; suppose n >= 2 ; ::_thesis: tau_bar to_power n < 1 / 2 then ( n <> 0 & n <> 1 ) ; then A2: n is non trivial Nat by NAT_2:def_1; tau_bar to_power n < 1 / 2 proof defpred S1[ Nat] means (abs tau_bar) to_power \$1 < 1 / 2; A3: (abs tau_bar) to_power 2 = (- tau_bar) to_power 2 by ABSVALUE:def_1 .= (- tau_bar) ^2 by POWER:46 .= (((1 ^2) - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) / 4 by FIB_NUM:def_2 .= ((1 - (2 * (sqrt 5))) + 5) / 4 by SQUARE_1:def_2 .= (3 - (sqrt 5)) / 2 ; sqrt 5 > 2 by SQUARE_1:20, SQUARE_1:27; then - (sqrt 5) < - 2 by XREAL_1:24; then (- (sqrt 5)) + 3 < (- 2) + 3 by XREAL_1:8; then A4: S1[2] by A3, XREAL_1:74; A5: for k being non trivial Nat st S1[k] holds S1[k + 1] proof let k be non trivial Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then ((abs tau_bar) to_power k) * (abs tau_bar) < (1 / 2) * (abs tau_bar) by XREAL_1:68; then A6: ((abs tau_bar) to_power k) * ((abs tau_bar) to_power 1) < (1 / 2) * (abs tau_bar) by POWER:25; (1 / 2) * (abs tau_bar) < (1 / 2) * 1 by Th5, XREAL_1:68; then ((abs tau_bar) to_power k) * ((abs tau_bar) to_power 1) < 1 / 2 by A6, XXREAL_0:2; hence S1[k + 1] by Th2; ::_thesis: verum end; A7: for n being non trivial Nat holds S1[n] from NAT_2:sch_2(A4, A5); for n being non trivial Nat holds tau_bar to_power n < 1 / 2 proof let n be non trivial Nat; ::_thesis: tau_bar to_power n < 1 / 2 (abs tau_bar) to_power n < 1 / 2 by A7; then ( abs (tau_bar to_power n) < 1 / 2 & tau_bar to_power n <= abs (tau_bar to_power n) ) by ABSVALUE:4, SERIES_1:2; hence tau_bar to_power n < 1 / 2 by XXREAL_0:2; ::_thesis: verum end; hence tau_bar to_power n < 1 / 2 by A2; ::_thesis: verum end; hence tau_bar to_power n < 1 / 2 ; ::_thesis: verum end; end; end; theorem :: FIB_NUM4:9 for n, m being Nat for r being real number st m is odd & n >= m & r < 0 & r > - 1 holds r to_power n >= r to_power m proof let n, m be Nat; ::_thesis: for r being real number st m is odd & n >= m & r < 0 & r > - 1 holds r to_power n >= r to_power m let r be real number ; ::_thesis: ( m is odd & n >= m & r < 0 & r > - 1 implies r to_power n >= r to_power m ) assume A1: m is odd ; ::_thesis: ( not n >= m or not r < 0 or not r > - 1 or r to_power n >= r to_power m ) assume A2: n >= m ; ::_thesis: ( not r < 0 or not r > - 1 or r to_power n >= r to_power m ) assume A3: ( r < 0 & r > - 1 ) ; ::_thesis: r to_power n >= r to_power m A4: n + 1 > m + 0 by A2, XREAL_1:8; percases ( n = m or n > m ) by A4, NAT_1:22; suppose n = m ; ::_thesis: r to_power n >= r to_power m hence r to_power n >= r to_power m ; ::_thesis: verum end; supposeA5: n > m ; ::_thesis: r to_power n >= r to_power m then reconsider t = n - m as Nat by NAT_1:21; A6: (r to_power n) - (r to_power m) = (r to_power (t + m)) - (r to_power m) .= ((r to_power t) * (r to_power m)) - (1 * (r to_power m)) by Th2, A3 .= ((r to_power t) - 1) * (r to_power m) ; A7: r to_power m <= 0 by Th7, A3, A1; A8: t <> 0 by A5; A9: abs r <= 1 by A3, ABSVALUE:5; abs r <> 1 proof assume abs r = 1 ; ::_thesis: contradiction then abs r = abs 1 ; hence contradiction by A3, ABSVALUE:28; ::_thesis: verum end; then A10: abs r < 1 by A9, XXREAL_0:1; ( abs r > 0 & t > 0 ) by A8, A3; then (abs r) to_power t < 1 to_power t by A10, POWER:37; then (abs r) to_power t < 1 by POWER:26; then ( abs (r to_power t) < 1 & r to_power t <= abs (r to_power t) ) by ABSVALUE:4, SERIES_1:2; then r to_power t < 1 by XXREAL_0:2; then (r to_power t) - 1 <= 1 - 1 by XREAL_1:9; then ((r to_power n) - (r to_power m)) + (r to_power m) >= 0 + (r to_power m) by A6, A7, XREAL_1:6; hence r to_power n >= r to_power m ; ::_thesis: verum end; end; end; theorem Th10: :: FIB_NUM4:10 for n, m being Nat st m is odd & n >= m holds tau_bar to_power n >= tau_bar to_power m proof let n, m be Nat; ::_thesis: ( m is odd & n >= m implies tau_bar to_power n >= tau_bar to_power m ) assume A1: m is odd ; ::_thesis: ( not n >= m or tau_bar to_power n >= tau_bar to_power m ) assume n >= m ; ::_thesis: tau_bar to_power n >= tau_bar to_power m then A2: n + 1 > m + 0 by XREAL_1:8; percases ( n = m or n > m ) by A2, NAT_1:22; suppose n = m ; ::_thesis: tau_bar to_power n >= tau_bar to_power m hence tau_bar to_power n >= tau_bar to_power m ; ::_thesis: verum end; supposeA3: n > m ; ::_thesis: tau_bar to_power n >= tau_bar to_power m then reconsider t = n - m as Nat by NAT_1:21; A4: (tau_bar to_power n) - (tau_bar to_power m) = (tau_bar to_power (t + m)) - (tau_bar to_power m) .= ((tau_bar to_power t) * (tau_bar to_power m)) - (1 * (tau_bar to_power m)) by Th2 .= ((tau_bar to_power t) - 1) * (tau_bar to_power m) ; A5: tau_bar to_power m <= 0 by Th7, A1; t <> 0 by A3; then ( abs tau_bar > 0 & t > 0 ) ; then (abs tau_bar) to_power t < 1 to_power t by Th5, POWER:37; then (abs tau_bar) to_power t < 1 by POWER:26; then ( abs (tau_bar to_power t) < 1 & tau_bar to_power t <= abs (tau_bar to_power t) ) by ABSVALUE:4, SERIES_1:2; then tau_bar to_power t < 1 by XXREAL_0:2; then (tau_bar to_power t) - 1 <= 1 - 1 by XREAL_1:9; then ((tau_bar to_power n) - (tau_bar to_power m)) + (tau_bar to_power m) >= 0 + (tau_bar to_power m) by A4, A5, XREAL_1:6; hence tau_bar to_power n >= tau_bar to_power m ; ::_thesis: verum end; end; end; theorem Th11: :: FIB_NUM4:11 for n, m being Nat st n is even & m is even & n >= m holds tau_bar to_power n <= tau_bar to_power m proof let n, m be Nat; ::_thesis: ( n is even & m is even & n >= m implies tau_bar to_power n <= tau_bar to_power m ) assume A1: ( n is even & m is even & n >= m ) ; ::_thesis: tau_bar to_power n <= tau_bar to_power m then A2: n + 1 > m + 0 by XREAL_1:8; percases ( n = m or n > m ) by A2, NAT_1:22; suppose n = m ; ::_thesis: tau_bar to_power n <= tau_bar to_power m hence tau_bar to_power n <= tau_bar to_power m ; ::_thesis: verum end; supposeA3: n > m ; ::_thesis: tau_bar to_power n <= tau_bar to_power m then reconsider t = n - m as Nat by NAT_1:21; A4: (tau_bar to_power n) - (tau_bar to_power m) = (tau_bar to_power (t + m)) - (tau_bar to_power m) .= ((tau_bar to_power t) * (tau_bar to_power m)) - (1 * (tau_bar to_power m)) by Th2 .= ((tau_bar to_power t) - 1) * (tau_bar to_power m) ; A5: tau_bar to_power m > 0 by Th6, A1; n - m > m - m by A3, XREAL_1:9; then tau_bar to_power t < 1 by Th8, XXREAL_0:2; then (tau_bar to_power t) - 1 < 1 - 1 by XREAL_1:9; then ((tau_bar to_power n) - (tau_bar to_power m)) + (tau_bar to_power m) < 0 + (tau_bar to_power m) by A4, A5, XREAL_1:6; hence tau_bar to_power n <= tau_bar to_power m ; ::_thesis: verum end; end; end; theorem Th12: :: FIB_NUM4:12 for m, n being non empty Nat st m >= n holds Lucas m >= Lucas n proof let m, n be non empty Nat; ::_thesis: ( m >= n implies Lucas m >= Lucas n ) assume A1: m >= n ; ::_thesis: Lucas m >= Lucas n percases ( m = n or m > n ) by A1, XXREAL_0:1; suppose m = n ; ::_thesis: Lucas m >= Lucas n hence Lucas m >= Lucas n ; ::_thesis: verum end; supposeA2: m > n ; ::_thesis: Lucas m >= Lucas n then consider k being Nat such that A3: m = n + k by NAT_1:10; A4: for k, n being non empty Nat holds Lucas (n + k) >= Lucas n proof defpred S1[ Nat] means for n being non empty Nat holds Lucas (n + \$1) >= Lucas n; A5: S1[1] proof let n be non empty Nat; ::_thesis: Lucas (n + 1) >= Lucas n ( n - 0 is Element of NAT & n + 1 is Element of NAT ) by ORDINAL1:def_12; hence Lucas (n + 1) >= Lucas n by FIB_NUM3:18; ::_thesis: verum end; A6: for k being non empty Nat st S1[k] holds S1[k + 1] proof let k be non empty Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A7: S1[k] ; ::_thesis: S1[k + 1] for n being non empty Nat holds Lucas (n + (k + 1)) >= Lucas n proof let n be non empty Nat; ::_thesis: Lucas (n + (k + 1)) >= Lucas n reconsider p = n + k as Element of NAT by ORDINAL1:def_12; p is non empty Element of NAT ; then ( Lucas (n + k) >= Lucas n & Lucas ((n + k) + 1) >= Lucas (n + k) ) by A7, FIB_NUM3:18; hence Lucas (n + (k + 1)) >= Lucas n by XXREAL_0:2; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for k being non empty Nat holds S1[k] from NAT_1:sch_10(A5, A6); hence for k, n being non empty Nat holds Lucas (n + k) >= Lucas n ; ::_thesis: verum end; ( k is non empty Nat & n is non empty Nat ) by A3, A2; hence Lucas m >= Lucas n by A3, A4; ::_thesis: verum end; end; 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 :: FIB_NUM4:13 for n being non empty Nat holds tau to_power n > tau_bar to_power n proof let n be non empty Nat; ::_thesis: tau to_power n > tau_bar to_power n set tb = tau_bar ; percases ( n is even or n is odd ) ; supposeA1: n is even ; ::_thesis: tau to_power n > tau_bar to_power n n - 0 is Element of NAT by NAT_1:21; then consider k being Element of NAT such that A2: n = 2 * k by A1, ABIAN:def_2; A3: k > 0 by A2; A4: tau to_power n = (tau to_power 2) to_power k by A2, NEWTON:9 .= (tau ^2) to_power k by POWER:46 ; tau_bar to_power n = (tau_bar to_power 2) to_power k by A2, NEWTON:9 .= (tau_bar ^2) to_power k by POWER:46 ; hence tau to_power n > tau_bar to_power n by A3, A4, Lm14, POWER:37; ::_thesis: verum end; suppose n is odd ; ::_thesis: tau to_power n > tau_bar to_power n then consider k being Element of NAT such that A5: n = (2 * k) + 1 by ABIAN:9; set kk = tau to_power (2 * k); A6: (tau / tau_bar) to_power (2 * k) = ((tau / tau_bar) to_power 2) to_power k by NEWTON:9 .= ((tau / tau_bar) ^2) to_power k by POWER:46 ; tau_bar to_power (2 * k) = (tau_bar to_power 2) to_power k by NEWTON:9 .= (tau_bar ^2) to_power k by POWER:46 ; then A7: tau_bar to_power (2 * k) > 0 by POWER:34; (tau / tau_bar) to_power (2 * k) > ((sqrt 5) - 3) / 2 by A6, Lm15, POWER:34; then ((tau / tau_bar) to_power (2 * k)) * (((- 3) - (sqrt 5)) / 2) < (tau_bar / tau) * (((- 3) - (sqrt 5)) / 2) by Lm13, Lm4, XREAL_1:69; then ((tau / tau_bar) to_power (2 * k)) * (tau / tau_bar) < 1 by Lm5, XCMPLX_1:112; then ((tau to_power (2 * k)) / (tau_bar to_power (2 * k))) * (tau / tau_bar) < 1 by Th1; then ((tau to_power (2 * k)) * (1 / (tau_bar to_power (2 * k)))) * (tau / tau_bar) < 1 by XCMPLX_1:99; then (((tau to_power (2 * k)) * (1 / (tau_bar to_power (2 * k)))) * (tau / tau_bar)) * (tau_bar to_power (2 * k)) < 1 * (tau_bar to_power (2 * k)) by A7, XREAL_1:68; then ((tau to_power (2 * k)) * (tau / tau_bar)) * ((tau_bar to_power (2 * k)) * (1 / (tau_bar to_power (2 * k)))) < 1 * (tau_bar to_power (2 * k)) ; then ((tau to_power (2 * k)) * (tau / tau_bar)) * ((tau_bar to_power (2 * k)) / (tau_bar to_power (2 * k))) < 1 * (tau_bar to_power (2 * k)) by XCMPLX_1:99; then ((tau to_power (2 * k)) * (tau / tau_bar)) * 1 < tau_bar to_power (2 * k) by A7, XCMPLX_1:60; then ((tau to_power (2 * k)) * (tau * (1 / tau_bar))) * 1 < tau_bar to_power (2 * k) by XCMPLX_1:99; then (((tau to_power (2 * k)) * (tau * (1 / tau_bar))) * 1) * tau_bar > (tau_bar to_power (2 * k)) * tau_bar by XREAL_1:69; then ((tau to_power (2 * k)) * tau) * (((1 / tau_bar) * 1) * tau_bar) > (tau_bar to_power (2 * k)) * tau_bar ; then ((tau to_power (2 * k)) * tau) * (tau_bar / tau_bar) > (tau_bar to_power (2 * k)) * tau_bar by XCMPLX_1:99; then ((tau to_power (2 * k)) * tau) * 1 > (tau_bar to_power (2 * k)) * tau_bar by XCMPLX_1:60; then (tau to_power (2 * k)) * tau > (tau_bar to_power (2 * k)) * (tau_bar to_power 1) by POWER:25; then (tau to_power (2 * k)) * tau > tau_bar to_power ((2 * k) + 1) by Th2; then (tau to_power (2 * k)) * (tau to_power 1) > tau_bar to_power ((2 * k) + 1) by POWER:25; hence tau to_power n > tau_bar to_power n by A5, Th2; ::_thesis: verum end; end; end; theorem Th14: :: FIB_NUM4:14 for n being Nat st n > 1 holds - (1 / 2) < tau_bar to_power n proof let n be Nat; ::_thesis: ( n > 1 implies - (1 / 2) < tau_bar to_power n ) assume A1: n > 1 ; ::_thesis: - (1 / 2) < tau_bar to_power n A2: n - 0 is Element of NAT by NAT_1:21; A3: n + 1 > 1 + 1 by A1, XREAL_1:8; percases ( n is even or n is odd ) ; suppose n is even ; ::_thesis: - (1 / 2) < tau_bar to_power n then consider k being Element of NAT such that A4: n = 2 * k by A2, ABIAN:def_2; A5: 0 ^2 = 0 ; tau_bar to_power n = (tau_bar to_power k) to_power 2 by A4, NEWTON:9 .= (tau_bar to_power k) ^2 by POWER:46 ; hence - (1 / 2) < tau_bar to_power n by A5, SQUARE_1:12; ::_thesis: verum end; supposeA6: n is odd ; ::_thesis: - (1 / 2) < tau_bar to_power n n >= 2 by A3, NAT_1:13; then ( n = 2 or n > 2 ) by XXREAL_0:1; then n + 1 > 2 + 1 by A6, POLYFORM:5, XREAL_1:6; then n >= 3 by NAT_1:13; then A7: tau_bar to_power n >= tau_bar to_power 3 by Th10, POLYFORM:6; sqrt 5 < sqrt ((5 / 2) ^2) by SQUARE_1:27; then sqrt 5 < 5 / 2 by SQUARE_1:def_2; then 2 * (sqrt 5) < 2 * (5 / 2) by XREAL_1:68; then - (2 * (sqrt 5)) > - 5 by XREAL_1:24; then (- (2 * (sqrt 5))) + 4 > (- 5) + 4 by XREAL_1:6; then (2 * (2 - (sqrt 5))) / 2 > (- 1) / 2 by XREAL_1:74; hence - (1 / 2) < tau_bar to_power n by A7, Lm8, XXREAL_0:2; ::_thesis: verum end; end; end; theorem Th15: :: FIB_NUM4:15 for n being Nat st n > 2 holds tau_bar to_power n >= - (1 / (sqrt 5)) proof let n be Nat; ::_thesis: ( n > 2 implies tau_bar to_power n >= - (1 / (sqrt 5)) ) assume n > 2 ; ::_thesis: tau_bar to_power n >= - (1 / (sqrt 5)) then n >= 2 + 1 by NAT_1:13; then A1: tau_bar to_power n >= tau_bar to_power 3 by Th10, POLYFORM:6; A2: sqrt 5 > 0 by SQUARE_1:25; sqrt 5 >= 2 by SQUARE_1:20, SQUARE_1:26; then 2 * (sqrt 5) >= 2 * 2 by XREAL_1:64; then (2 * (sqrt 5)) - 5 >= 4 - 5 by XREAL_1:9; then (2 * (sqrt 5)) - ((sqrt 5) ^2) >= - 1 by SQUARE_1:def_2; then ((2 - (sqrt 5)) * (sqrt 5)) / (sqrt 5) >= (- 1) / (sqrt 5) by A2, XREAL_1:72; then ((2 - (sqrt 5)) * (sqrt 5)) / (sqrt 5) >= - (1 / (sqrt 5)) by XCMPLX_1:187; then 2 - (sqrt 5) >= - (1 / (sqrt 5)) by A2, XCMPLX_1:89; hence tau_bar to_power n >= - (1 / (sqrt 5)) by A1, Lm8, XXREAL_0:2; ::_thesis: verum end; theorem Th16: :: FIB_NUM4:16 for n being Nat st n >= 2 holds tau_bar to_power n <= 1 / (sqrt 5) proof let n be Nat; ::_thesis: ( n >= 2 implies tau_bar to_power n <= 1 / (sqrt 5) ) assume A1: n >= 2 ; ::_thesis: tau_bar to_power n <= 1 / (sqrt 5) percases ( n is even or n is odd ) ; supposeA2: n is even ; ::_thesis: tau_bar to_power n <= 1 / (sqrt 5) A3: sqrt 5 > 0 by SQUARE_1:25; A4: tau_bar to_power n <= (3 - (sqrt 5)) / 2 by Lm7, A1, A2, Th11, POLYFORM:5; sqrt 5 <= sqrt ((7 / 3) ^2) by SQUARE_1:26; then sqrt 5 <= 7 / 3 by SQUARE_1:def_2; then 3 * (sqrt 5) <= (7 / 3) * 3 by XREAL_1:64; then (3 * (sqrt 5)) - 5 <= 7 - 5 by XREAL_1:9; then (3 * (sqrt 5)) - ((sqrt 5) ^2) <= 2 by SQUARE_1:def_2; then ((3 * (sqrt 5)) - ((sqrt 5) * (sqrt 5))) / 2 <= 2 / 2 by XREAL_1:72; then (((3 - (sqrt 5)) / 2) * (sqrt 5)) / (sqrt 5) <= 1 / (sqrt 5) by A3, XREAL_1:72; then (3 - (sqrt 5)) / 2 <= 1 / (sqrt 5) by A3, XCMPLX_1:89; hence tau_bar to_power n <= 1 / (sqrt 5) by A4, XXREAL_0:2; ::_thesis: verum end; suppose n is odd ; ::_thesis: tau_bar to_power n <= 1 / (sqrt 5) then A5: tau_bar to_power n < 0 by Th7; sqrt 5 >= sqrt 0 by SQUARE_1:26; hence tau_bar to_power n <= 1 / (sqrt 5) by A5, SQUARE_1:17; ::_thesis: verum end; end; end; 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 ) proof let n be Nat; ::_thesis: ( ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) > 0 & ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) < 1 ) set b = (1 - (sqrt 5)) / 2; A1: abs ((1 - (sqrt 5)) / 2) = - ((1 - (sqrt 5)) / 2) by ABSVALUE:def_1, FIB_NUM:def_2; A2: ((abs ((1 - (sqrt 5)) / 2)) to_power n) * (1 / (sqrt 5)) < 1 / 2 by Lm11, FIB_NUM:def_2; ( ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) > 0 & ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) < 1 ) proof percases ( n is even or n is odd ) ; suppose n is even ; ::_thesis: ( ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) > 0 & ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) < 1 ) then (abs ((1 - (sqrt 5)) / 2)) to_power n = ((1 - (sqrt 5)) / 2) to_power n by Th3, A1, FIB_NUM:def_2; then ( (((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5)) > 0 & (((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5)) < 1 / 2 ) by Lm10, Lm11, FIB_NUM:def_2; then ( (((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5)) > 0 & ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) < (1 / 2) + (1 / 2) ) by XREAL_1:8; hence ( ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) > 0 & ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) < 1 ) ; ::_thesis: verum end; suppose n is odd ; ::_thesis: ( ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) > 0 & ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) < 1 ) then (abs ((1 - (sqrt 5)) / 2)) to_power n = - (((1 - (sqrt 5)) / 2) to_power n) by Th4, A1, FIB_NUM:def_2; then ( (- (((1 - (sqrt 5)) / 2) to_power n)) * (1 / (sqrt 5)) > 0 & - ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) < 1 / 2 ) by Lm10, A2, FIB_NUM:def_2; then ( - ((((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5)) > 0 & - ((((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5)) < 1 / 2 ) by XCMPLX_1:99; then ( (((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5) < 0 & - (- ((((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5))) > - (1 / 2) ) by XREAL_1:24; then ( ((((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5)) + (1 / 2) < 0 + (1 / 2) & ((((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5)) + (1 / 2) > (- (1 / 2)) + (1 / 2) ) by XREAL_1:8; then ( ((((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5)) + (1 / 2) < 1 & ((((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5)) + (1 / 2) > 0 ) by XXREAL_0:2; hence ( ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) > 0 & ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) < 1 ) by XCMPLX_1:99; ::_thesis: verum end; end; end; hence ( ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) > 0 & ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) < 1 ) by FIB_NUM:def_2, XCMPLX_1:99; ::_thesis: verum end; begin theorem :: FIB_NUM4:18 for n being Nat holds [\(((tau to_power n) / (sqrt 5)) + (1 / 2))/] = Fib n proof let n be Nat; ::_thesis: [\(((tau to_power n) / (sqrt 5)) + (1 / 2))/] = Fib n set tn = tau_bar to_power n; A1: Fib n = ((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) + (1 / 2)) - (1 / 2) by FIB_NUM:7 .= ((((tau to_power n) / (sqrt 5)) - ((tau_bar to_power n) / (sqrt 5))) + (1 / 2)) - (1 / 2) by XCMPLX_1:120 .= (((tau to_power n) / (sqrt 5)) + (1 / 2)) - (((tau_bar to_power n) / (sqrt 5)) + (1 / 2)) ; ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) > 0 by Th17; then A2: (((tau_bar to_power n) / (sqrt 5)) + (1 / 2)) + (Fib n) > 0 + (Fib n) by XREAL_1:6; ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) < 1 by Th17; then (((tau_bar to_power n) / (sqrt 5)) + (1 / 2)) - (1 / 2) < 1 - (1 / 2) by XREAL_1:9; then - ((tau_bar to_power n) / (sqrt 5)) > - (1 / 2) by XREAL_1:24; then (- ((tau_bar to_power n) / (sqrt 5))) + ((tau to_power n) / (sqrt 5)) > (- (1 / 2)) + ((tau to_power n) / (sqrt 5)) by XREAL_1:6; then ((tau to_power n) / (sqrt 5)) - ((tau_bar to_power n) / (sqrt 5)) > (- (1 / 2)) + ((tau to_power n) / (sqrt 5)) ; then ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) > (- (1 / 2)) + ((tau to_power n) / (sqrt 5)) by XCMPLX_1:120; then Fib n > (((tau to_power n) / (sqrt 5)) + (1 / 2)) - 1 by FIB_NUM:7; hence [\(((tau to_power n) / (sqrt 5)) + (1 / 2))/] = Fib n by A2, A1, INT_1:def_6; ::_thesis: verum end; theorem :: FIB_NUM4:19 for n being Nat st n <> 0 holds [/(((tau to_power n) / (sqrt 5)) - (1 / 2))\] = Fib n proof let n be Nat; ::_thesis: ( n <> 0 implies [/(((tau to_power n) / (sqrt 5)) - (1 / 2))\] = Fib n ) set tn = tau to_power n; set tbn = tau_bar to_power n; assume A1: n <> 0 ; ::_thesis: [/(((tau to_power n) / (sqrt 5)) - (1 / 2))\] = Fib n A2: sqrt 5 > 0 by SQUARE_1:25; A3: ((tau to_power n) / (sqrt 5)) - (1 / 2) <= Fib n proof 1 <= sqrt 5 by SQUARE_1:18, SQUARE_1:26; then 1 / 2 <= (sqrt 5) / 2 by XREAL_1:72; then tau_bar to_power n <= (sqrt 5) / 2 by A1, Th8, XXREAL_0:2; then (tau_bar to_power n) / (sqrt 5) <= ((sqrt 5) / 2) / (sqrt 5) by A2, XREAL_1:72; then (tau_bar to_power n) / (sqrt 5) <= ((sqrt 5) / (sqrt 5)) / 2 by XCMPLX_1:48; then (tau_bar to_power n) / (sqrt 5) <= 1 / 2 by A2, XCMPLX_1:60; then - ((tau_bar to_power n) / (sqrt 5)) >= - (1 / 2) by XREAL_1:24; then (- ((tau_bar to_power n) / (sqrt 5))) + ((tau to_power n) / (sqrt 5)) >= (- (1 / 2)) + ((tau to_power n) / (sqrt 5)) by XREAL_1:6; then ((tau to_power n) / (sqrt 5)) - ((tau_bar to_power n) / (sqrt 5)) >= (- (1 / 2)) + ((tau to_power n) / (sqrt 5)) ; then ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) >= ((tau to_power n) / (sqrt 5)) - (1 / 2) by XCMPLX_1:120; hence ((tau to_power n) / (sqrt 5)) - (1 / 2) <= Fib n by FIB_NUM:7; ::_thesis: verum end; (((tau to_power n) / (sqrt 5)) - (1 / 2)) + 1 > Fib n proof n + 1 > 0 + 1 by A1, XREAL_1:6; then A4: n >= 1 by NAT_1:13; percases ( n = 1 or n > 1 ) by A4, XXREAL_0:1; supposeA5: n = 1 ; ::_thesis: (((tau to_power n) / (sqrt 5)) - (1 / 2)) + 1 > Fib n then A6: (((tau to_power n) / (sqrt 5)) - (1 / 2)) + 1 = ((tau / (sqrt 5)) - (1 / 2)) + 1 by POWER:25 .= (((1 + (sqrt 5)) / 2) / (sqrt 5)) + (1 - (1 / 2)) by FIB_NUM:def_1 .= (((1 + (sqrt 5)) / (sqrt 5)) / 2) + (1 / 2) by XCMPLX_1:48 .= (((1 + (sqrt 5)) / (sqrt 5)) + 1) / 2 .= (((1 / (sqrt 5)) + ((sqrt 5) / (sqrt 5))) + 1) / 2 by XCMPLX_1:62 .= (((1 / (sqrt 5)) + 1) + 1) / 2 by A2, XCMPLX_1:60 .= ((1 / (sqrt 5)) / 2) + (2 / 2) ; ((1 / (sqrt 5)) / 2) + 1 > 0 + 1 by A2, XREAL_1:6; hence (((tau to_power n) / (sqrt 5)) - (1 / 2)) + 1 > Fib n by A5, A6, PRE_FF:1; ::_thesis: verum end; supposeA7: n > 1 ; ::_thesis: (((tau to_power n) / (sqrt 5)) - (1 / 2)) + 1 > Fib n 1 < sqrt 5 by SQUARE_1:18, SQUARE_1:27; then 1 / 2 < (sqrt 5) / 2 by XREAL_1:74; then A8: - (1 / 2) > - ((sqrt 5) / 2) by XREAL_1:24; tau_bar to_power n > - (1 / 2) by A7, Th14; then tau_bar to_power n > - ((sqrt 5) / 2) by A8, XXREAL_0:2; then (tau_bar to_power n) / (sqrt 5) > (- ((sqrt 5) / 2)) / (sqrt 5) by A2, XREAL_1:74; then (tau_bar to_power n) / (sqrt 5) > - (((sqrt 5) / 2) / (sqrt 5)) by XCMPLX_1:187; then (tau_bar to_power n) / (sqrt 5) > - (((sqrt 5) / (sqrt 5)) / 2) by XCMPLX_1:48; then (tau_bar to_power n) / (sqrt 5) > - (1 / 2) by A2, XCMPLX_1:60; then - ((tau_bar to_power n) / (sqrt 5)) < - (- (1 / 2)) by XREAL_1:24; then (- ((tau_bar to_power n) / (sqrt 5))) + ((tau to_power n) / (sqrt 5)) < (1 / 2) + ((tau to_power n) / (sqrt 5)) by XREAL_1:6; then ((tau to_power n) / (sqrt 5)) - ((tau_bar to_power n) / (sqrt 5)) < (1 / 2) + ((tau to_power n) / (sqrt 5)) ; then ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) < (1 / 2) + ((tau to_power n) / (sqrt 5)) by XCMPLX_1:120; hence (((tau to_power n) / (sqrt 5)) - (1 / 2)) + 1 > Fib n by FIB_NUM:7; ::_thesis: verum end; end; end; hence [/(((tau to_power n) / (sqrt 5)) - (1 / 2))\] = Fib n by A3, INT_1:def_7; ::_thesis: verum 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:20 for n being Nat st n <> 0 holds [\((tau to_power (2 * n)) / (sqrt 5))/] = Fib (2 * n) proof let n be Nat; ::_thesis: ( n <> 0 implies [\((tau to_power (2 * n)) / (sqrt 5))/] = Fib (2 * n) ) assume A1: n <> 0 ; ::_thesis: [\((tau to_power (2 * n)) / (sqrt 5))/] = Fib (2 * n) A2: ((tau to_power (2 * n)) / (sqrt 5)) - 1 < Fib (2 * n) proof A3: 2 to_power (2 * n) > 0 by POWER:34; ((1 - (sqrt 5)) to_power 2) to_power n < (2 to_power 2) to_power n by A1, Lm17, Lm19, POWER:37; then ((1 - (sqrt 5)) to_power 2) to_power n < 2 to_power (2 * n) by POWER:33; then (1 - (sqrt 5)) to_power (2 * n) < 2 to_power (2 * n) by NEWTON:9; then ((1 - (sqrt 5)) to_power (2 * n)) / (2 to_power (2 * n)) < (2 to_power (2 * n)) / (2 to_power (2 * n)) by A3, XREAL_1:74; then ((1 - (sqrt 5)) to_power (2 * n)) / (2 to_power (2 * n)) < 1 by A3, XCMPLX_1:60; then tau_bar to_power (2 * n) < 1 by Th1, FIB_NUM:def_2; then tau_bar to_power (2 * n) < sqrt 5 by Lm16, XXREAL_0:2; then (tau_bar to_power (2 * n)) / (sqrt 5) < (sqrt 5) / (sqrt 5) by Lm18, XREAL_1:74; then (tau_bar to_power (2 * n)) / (sqrt 5) < 1 by Lm18, XCMPLX_1:60; then - ((tau_bar to_power (2 * n)) / (sqrt 5)) > - 1 by XREAL_1:24; then (- ((tau_bar to_power (2 * n)) / (sqrt 5))) + ((tau to_power (2 * n)) / (sqrt 5)) > (- 1) + ((tau to_power (2 * n)) / (sqrt 5)) by XREAL_1:8; then ((tau to_power (2 * n)) / (sqrt 5)) - ((tau_bar to_power (2 * n)) / (sqrt 5)) > (- 1) + ((tau to_power (2 * n)) / (sqrt 5)) ; then ((tau to_power (2 * n)) - (tau_bar to_power (2 * n))) / (sqrt 5) > (- 1) + ((tau to_power (2 * n)) / (sqrt 5)) by XCMPLX_1:120; hence ((tau to_power (2 * n)) / (sqrt 5)) - 1 < Fib (2 * n) by FIB_NUM:7; ::_thesis: verum end; tau_bar to_power (2 * n) = (tau_bar to_power 2) |^ n by NEWTON:9 .= (tau_bar ^2) to_power n by POWER:46 ; then tau_bar to_power (2 * n) > 0 by POWER:34; then (- ((tau_bar to_power (2 * n)) / (sqrt 5))) + ((tau to_power (2 * n)) / (sqrt 5)) < 0 + ((tau to_power (2 * n)) / (sqrt 5)) by Lm18, XREAL_1:8; then ((tau to_power (2 * n)) / (sqrt 5)) - ((tau_bar to_power (2 * n)) / (sqrt 5)) < (tau to_power (2 * n)) / (sqrt 5) ; then ((tau to_power (2 * n)) - (tau_bar to_power (2 * n))) / (sqrt 5) < (tau to_power (2 * n)) / (sqrt 5) by XCMPLX_1:120; then Fib (2 * n) <= (tau to_power (2 * n)) / (sqrt 5) by FIB_NUM:7; hence [\((tau to_power (2 * n)) / (sqrt 5))/] = Fib (2 * n) by A2, INT_1:def_6; ::_thesis: verum end; theorem :: FIB_NUM4:21 for n being Nat holds [/((tau to_power ((2 * n) + 1)) / (sqrt 5))\] = Fib ((2 * n) + 1) proof let n be Nat; ::_thesis: [/((tau to_power ((2 * n) + 1)) / (sqrt 5))\] = Fib ((2 * n) + 1) A1: Fib ((2 * n) + 1) = ((tau to_power ((2 * n) + 1)) - (tau_bar to_power ((2 * n) + 1))) / (sqrt 5) by FIB_NUM:7 .= ((tau to_power ((2 * n) + 1)) / (sqrt 5)) - ((tau_bar to_power ((2 * n) + 1)) / (sqrt 5)) by XCMPLX_1:120 ; A2: sqrt 5 > 0 by SQUARE_1:17, SQUARE_1:27; tau_bar to_power ((2 * n) + 1) < 0 proof set t = - tau_bar; A3: tau_bar to_power ((2 * n) + 1) = (- (- tau_bar)) to_power ((2 * n) + 1) .= - ((- tau_bar) to_power ((2 * n) + 1)) by Th4 ; (- tau_bar) to_power ((2 * n) + 1) > 0 by POWER:34; hence tau_bar to_power ((2 * n) + 1) < 0 by A3; ::_thesis: verum end; then A4: (tau to_power ((2 * n) + 1)) / (sqrt 5) <= Fib ((2 * n) + 1) by A1, A2, XREAL_1:46; ((tau_bar to_power ((2 * n) + 1)) / (sqrt 5)) + (1 / 2) > 0 by Th17; then (((tau_bar to_power ((2 * n) + 1)) / (sqrt 5)) + (1 / 2)) - (1 / 2) > 0 - (1 / 2) by XREAL_1:9; then (tau_bar to_power ((2 * n) + 1)) / (sqrt 5) > - 1 by XXREAL_0:2; then - ((tau_bar to_power ((2 * n) + 1)) / (sqrt 5)) < - (- 1) by XREAL_1:24; then (- ((tau_bar to_power ((2 * n) + 1)) / (sqrt 5))) + ((tau to_power ((2 * n) + 1)) / (sqrt 5)) < 1 + ((tau to_power ((2 * n) + 1)) / (sqrt 5)) by XREAL_1:8; then ((tau to_power ((2 * n) + 1)) / (sqrt 5)) - ((tau_bar to_power ((2 * n) + 1)) / (sqrt 5)) < 1 + ((tau to_power ((2 * n) + 1)) / (sqrt 5)) ; then ((tau to_power ((2 * n) + 1)) - (tau_bar to_power ((2 * n) + 1))) / (sqrt 5) < 1 + ((tau to_power ((2 * n) + 1)) / (sqrt 5)) by XCMPLX_1:120; then Fib ((2 * n) + 1) < ((tau to_power ((2 * n) + 1)) / (sqrt 5)) + 1 by FIB_NUM:7; hence [/((tau to_power ((2 * n) + 1)) / (sqrt 5))\] = Fib ((2 * n) + 1) by A4, INT_1:def_7; ::_thesis: verum end; theorem Th22: :: FIB_NUM4:22 for n being Nat st n >= 2 & n is even holds Fib (n + 1) = [\((tau * (Fib n)) + 1)/] proof let n be Nat; ::_thesis: ( n >= 2 & n is even implies Fib (n + 1) = [\((tau * (Fib n)) + 1)/] ) assume A1: ( n >= 2 & n is even ) ; ::_thesis: Fib (n + 1) = [\((tau * (Fib n)) + 1)/] set t = tau ; set tb = tau_bar ; A2: sqrt 5 > 0 by SQUARE_1:17, SQUARE_1:27; A3: tau * tau_bar = ((1 ^2) - ((sqrt 5) ^2)) / 4 by FIB_NUM:def_1, FIB_NUM:def_2 .= (1 - 5) / 4 by SQUARE_1:def_2 .= - 1 ; tau_bar to_power n = (- tau_bar) to_power n by A1, Th3; then A4: tau_bar to_power n > 0 by POWER:34; A5: (tau_bar to_power 2) + 1 = (tau_bar ^2) + 1 by POWER:46 .= ((((1 ^2) - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) / 4) + 1 by FIB_NUM:def_2 .= (((1 - (2 * (sqrt 5))) + 5) / 4) + 1 by SQUARE_1:def_2 .= (5 - (sqrt 5)) / 2 .= (((sqrt 5) ^2) - (sqrt 5)) / 2 by SQUARE_1:def_2 .= - ((sqrt 5) * tau_bar) by FIB_NUM:def_2 ; tau * (Fib n) = tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) by FIB_NUM:7 .= (tau * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5) by XCMPLX_1:74 .= ((tau * (tau to_power n)) - (tau * (tau_bar to_power n))) / (sqrt 5) .= (((tau to_power 1) * (tau to_power n)) - (tau * (tau_bar to_power n))) / (sqrt 5) by POWER:25 .= ((tau to_power (n + 1)) - (tau * (tau_bar to_power ((n - 1) + 1)))) / (sqrt 5) by POWER:27 .= ((tau to_power (n + 1)) - (tau * ((tau_bar to_power (n - 1)) * (tau_bar to_power 1)))) / (sqrt 5) by Th2 .= ((tau to_power (n + 1)) - (tau * ((tau_bar to_power (n - 1)) * tau_bar))) / (sqrt 5) by POWER:25 .= ((tau to_power (n + 1)) - ((tau * tau_bar) * (tau_bar to_power (n - 1)))) / (sqrt 5) .= ((((tau to_power (n + 1)) - ((- 1) * (tau_bar to_power (n - 1)))) + (tau_bar to_power (n - 1))) - (tau_bar to_power (n - 1))) / (sqrt 5) by A3 .= (((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) + ((tau_bar to_power (n - 1)) + (tau_bar to_power (n + 1)))) / (sqrt 5) .= (((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5)) + (((tau_bar to_power (n - 1)) + (tau_bar to_power ((n - 1) + 2))) / (sqrt 5)) by XCMPLX_1:62 .= (Fib (n + 1)) + (((tau_bar to_power (n - 1)) + (tau_bar to_power ((n - 1) + 2))) / (sqrt 5)) by FIB_NUM:7 .= (Fib (n + 1)) + ((((tau_bar to_power (n - 1)) * 1) + ((tau_bar to_power (n - 1)) * (tau_bar to_power 2))) / (sqrt 5)) by Th2 .= (Fib (n + 1)) + (((tau_bar to_power (n - 1)) * (1 + (tau_bar to_power 2))) / (sqrt 5)) .= (Fib (n + 1)) + (((tau_bar to_power (n - 1)) * (- ((sqrt 5) * tau_bar))) / (sqrt 5)) by A5 .= (Fib (n + 1)) + (((((- 1) * (tau_bar to_power (n - 1))) * tau_bar) * (sqrt 5)) / (sqrt 5)) .= (Fib (n + 1)) + (((- 1) * (tau_bar to_power (n - 1))) * tau_bar) by A2, XCMPLX_1:89 .= (Fib (n + 1)) - ((tau_bar to_power (n - 1)) * tau_bar) .= (Fib (n + 1)) - ((tau_bar to_power (n - 1)) * (tau_bar to_power 1)) by POWER:25 .= (Fib (n + 1)) - (tau_bar to_power ((n - 1) + 1)) by Th2 .= (Fib (n + 1)) - (tau_bar to_power n) ; then A6: Fib (n + 1) = ((tau * (Fib n)) + 1) - (1 - (tau_bar to_power n)) ; tau_bar to_power n < 1 by Th8, A1, XXREAL_0:2; then - (tau_bar to_power n) > - 1 by XREAL_1:24; then (- (tau_bar to_power n)) + 1 > (- 1) + 1 by XREAL_1:8; then A7: Fib (n + 1) < (tau * (Fib n)) + 1 by A6, XREAL_1:44; (tau * (Fib n)) + 1 < (Fib (n + 1)) + 1 proof A8: tau * (Fib n) = tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) by FIB_NUM:7 .= (tau * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5) by XCMPLX_1:74 .= ((tau * (tau to_power n)) - (tau * (tau_bar to_power n))) / (sqrt 5) .= (((tau to_power 1) * (tau to_power n)) - (tau * (tau_bar to_power n))) / (sqrt 5) by POWER:25 .= ((tau to_power (n + 1)) - (tau * (tau_bar to_power n))) / (sqrt 5) by POWER:27 .= ((tau to_power (n + 1)) / (sqrt 5)) - ((tau * (tau_bar to_power n)) / (sqrt 5)) by XCMPLX_1:120 ; A9: Fib (n + 1) = ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) by FIB_NUM:7 .= ((tau to_power (n + 1)) / (sqrt 5)) - ((tau_bar to_power (n + 1)) / (sqrt 5)) by XCMPLX_1:120 ; (tau_bar to_power n) * tau > (tau_bar to_power n) * tau_bar by A4, XREAL_1:68; then (tau_bar to_power n) * tau > (tau_bar to_power n) * (tau_bar to_power 1) by POWER:25; then (tau * (tau_bar to_power n)) / (sqrt 5) > ((tau_bar to_power n) * (tau_bar to_power 1)) / (sqrt 5) by A2, XREAL_1:74; then (tau * (tau_bar to_power n)) / (sqrt 5) > (tau_bar to_power (n + 1)) / (sqrt 5) by Th2; then - ((tau * (tau_bar to_power n)) / (sqrt 5)) < - ((tau_bar to_power (n + 1)) / (sqrt 5)) by XREAL_1:24; then (- ((tau * (tau_bar to_power n)) / (sqrt 5))) + ((tau to_power (n + 1)) / (sqrt 5)) < (- ((tau_bar to_power (n + 1)) / (sqrt 5))) + ((tau to_power (n + 1)) / (sqrt 5)) by XREAL_1:8; hence (tau * (Fib n)) + 1 < (Fib (n + 1)) + 1 by A8, A9, XREAL_1:8; ::_thesis: verum end; then ((tau * (Fib n)) + 1) - 1 < ((Fib (n + 1)) + 1) - 1 by XREAL_1:9; hence Fib (n + 1) = [\((tau * (Fib n)) + 1)/] by A7, INT_1:def_6; ::_thesis: verum end; theorem Th23: :: FIB_NUM4:23 for n being Nat st n >= 2 & n is odd holds Fib (n + 1) = [/((tau * (Fib n)) - 1)\] proof let n be Nat; ::_thesis: ( n >= 2 & n is odd implies Fib (n + 1) = [/((tau * (Fib n)) - 1)\] ) assume A1: ( n >= 2 & n is odd ) ; ::_thesis: Fib (n + 1) = [/((tau * (Fib n)) - 1)\] A2: sqrt 5 > 0 by SQUARE_1:17, SQUARE_1:27; (tau * (tau_bar to_power n)) + (sqrt 5) >= tau_bar to_power (n + 1) proof set tbn = tau_bar to_power n; A3: tau_bar to_power n < 0 by A1, Th7; tau + ((sqrt 5) / (tau_bar to_power n)) <= tau_bar proof n > 1 by A1, XXREAL_0:2; then tau_bar to_power n >= - (1 / 2) by Th14; then tau_bar to_power n > - 1 by XXREAL_0:2; then (tau_bar to_power n) + 1 >= (- 1) + 1 by XREAL_1:6; then ((tau_bar to_power n) + 1) / (tau_bar to_power n) <= 0 / (tau_bar to_power n) by A3; then ((tau_bar to_power n) / (tau_bar to_power n)) + (1 / (tau_bar to_power n)) <= 0 by XCMPLX_1:62; then 1 + (1 / (tau_bar to_power n)) <= 0 by A3, XCMPLX_1:60; then (1 + (1 / (tau_bar to_power n))) * (sqrt 5) <= 0 * (sqrt 5) by A2; then (1 * (sqrt 5)) + ((1 / (tau_bar to_power n)) * (sqrt 5)) <= 0 ; then (sqrt 5) + ((sqrt 5) / (tau_bar to_power n)) <= 0 by XCMPLX_1:74; then ((((sqrt 5) / 2) + ((sqrt 5) / (tau_bar to_power n))) + ((sqrt 5) / 2)) - ((sqrt 5) / 2) <= 0 - ((sqrt 5) / 2) by XREAL_1:9; then (((sqrt 5) / 2) + ((sqrt 5) / (tau_bar to_power n))) + (1 / 2) <= (- ((sqrt 5) / 2)) + (1 / 2) by XREAL_1:6; hence tau + ((sqrt 5) / (tau_bar to_power n)) <= tau_bar by FIB_NUM:def_1, FIB_NUM:def_2; ::_thesis: verum end; then (tau + ((sqrt 5) / (tau_bar to_power n))) * (tau_bar to_power n) >= tau_bar * (tau_bar to_power n) by A3, XREAL_1:65; then (tau + ((sqrt 5) / (tau_bar to_power n))) * (tau_bar to_power n) >= (tau_bar to_power 1) * (tau_bar to_power n) by POWER:25; then (tau * (tau_bar to_power n)) + (((sqrt 5) / (tau_bar to_power n)) * (tau_bar to_power n)) >= tau_bar to_power (n + 1) by Th2; hence (tau * (tau_bar to_power n)) + (sqrt 5) >= tau_bar to_power (n + 1) by A3, XCMPLX_1:87; ::_thesis: verum end; then - ((tau * (tau_bar to_power n)) + (sqrt 5)) <= - (tau_bar to_power (n + 1)) by XREAL_1:24; then ((- (tau * (tau_bar to_power n))) - (sqrt 5)) + (tau to_power (n + 1)) <= (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) by XREAL_1:6; then ((tau to_power (n + 1)) - (tau * (tau_bar to_power n))) - (sqrt 5) <= (tau to_power (n + 1)) - (tau_bar to_power (n + 1)) ; then (((tau to_power 1) * (tau to_power n)) - (tau * (tau_bar to_power n))) - (sqrt 5) <= (tau to_power (n + 1)) - (tau_bar to_power (n + 1)) by POWER:27; then ((tau * (tau to_power n)) - (tau * (tau_bar to_power n))) - (sqrt 5) <= (tau to_power (n + 1)) - (tau_bar to_power (n + 1)) by POWER:25; then ((tau * ((tau to_power n) - (tau_bar to_power n))) - (sqrt 5)) / (sqrt 5) <= ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) by A2, XREAL_1:72; then ((tau * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5)) - ((sqrt 5) / (sqrt 5)) <= ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) by XCMPLX_1:120; then (tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) - ((sqrt 5) / (sqrt 5)) <= ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) by XCMPLX_1:74; then (tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) - 1 <= ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) by A2, XCMPLX_1:60; then (tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) - 1 <= Fib (n + 1) by FIB_NUM:7; then A4: (tau * (Fib n)) - 1 <= Fib (n + 1) by FIB_NUM:7; ((tau * (Fib n)) - 1) + 1 > Fib (n + 1) proof set tn = tau to_power n; set tbn = tau_bar to_power n; A5: tau * (Fib n) = tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) by FIB_NUM:7 .= (tau * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5) by XCMPLX_1:74 ; A6: tau_bar to_power n < 0 by Th7, A1; tau > tau_bar to_power 1 by POWER:25; then tau * (tau_bar to_power n) < (tau_bar to_power 1) * (tau_bar to_power n) by A6, XREAL_1:69; then tau * (tau_bar to_power n) < tau_bar to_power (n + 1) by Th2; then - (tau * (tau_bar to_power n)) > - (tau_bar to_power (n + 1)) by XREAL_1:24; then (- (tau * (tau_bar to_power n))) + (tau to_power (n + 1)) > (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) by XREAL_1:6; then (tau to_power (n + 1)) - (tau * (tau_bar to_power n)) > (tau to_power (n + 1)) - (tau_bar to_power (n + 1)) ; then ((tau to_power 1) * (tau to_power n)) - (tau * (tau_bar to_power n)) > (tau to_power (n + 1)) - (tau_bar to_power (n + 1)) by Th2; then (tau * (tau to_power n)) - (tau * (tau_bar to_power n)) > (tau to_power (n + 1)) - (tau_bar to_power (n + 1)) by POWER:25; then (tau * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5) > ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) by A2, XREAL_1:74; hence ((tau * (Fib n)) - 1) + 1 > Fib (n + 1) by A5, FIB_NUM:7; ::_thesis: verum end; hence Fib (n + 1) = [/((tau * (Fib n)) - 1)\] by A4, INT_1:def_7; ::_thesis: verum end; theorem Th24: :: FIB_NUM4:24 for n being Nat st n >= 2 holds Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] proof let n be Nat; ::_thesis: ( n >= 2 implies Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] ) assume A1: n >= 2 ; ::_thesis: Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] A2: sqrt 5 > 0 by SQUARE_1:25; set tn = tau to_power n; set tb = tau_bar ; set s5 = sqrt 5; set tbn = tau_bar to_power n; percases ( n is even or n is odd ) ; supposeA3: n is even ; ::_thesis: Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] then A4: tau_bar to_power n > 0 by Th6; A5: (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 >= Fib (n + 1) proof tau_bar to_power n <= 1 / 2 by Th8, A1; then 2 * (tau_bar to_power n) <= 2 * (1 / 2) by XREAL_1:64; then (2 * (tau_bar to_power n)) / (tau_bar to_power n) <= 1 / (tau_bar to_power n) by A4, XREAL_1:72; then 2 <= 1 / (tau_bar to_power n) by A4, XCMPLX_1:89; then 2 * (sqrt 5) <= (1 / (tau_bar to_power n)) * (sqrt 5) by A2, XREAL_1:64; then (sqrt 5) + (sqrt 5) <= (1 * (sqrt 5)) / (tau_bar to_power n) by XCMPLX_1:74; then ((sqrt 5) + (sqrt 5)) - (sqrt 5) <= ((1 * (sqrt 5)) / (tau_bar to_power n)) - (sqrt 5) by XREAL_1:9; then - (sqrt 5) >= - (((sqrt 5) / (tau_bar to_power n)) - (sqrt 5)) by XREAL_1:24; then (- (sqrt 5)) + 1 >= ((- ((sqrt 5) / (tau_bar to_power n))) + (sqrt 5)) + 1 by XREAL_1:6; then tau_bar >= (((sqrt 5) + 1) - ((sqrt 5) / (tau_bar to_power n))) / 2 by FIB_NUM:def_2, XREAL_1:72; then tau_bar * (tau_bar to_power n) >= (tau - (((sqrt 5) / (tau_bar to_power n)) / 2)) * (tau_bar to_power n) by A4, FIB_NUM:def_1, XREAL_1:64; then tau_bar * (tau_bar to_power n) >= (tau - (((sqrt 5) / 2) / (tau_bar to_power n))) * (tau_bar to_power n) by XCMPLX_1:48; then tau_bar * (tau_bar to_power n) >= (tau * (tau_bar to_power n)) - ((((sqrt 5) / 2) / (tau_bar to_power n)) * (tau_bar to_power n)) ; then tau_bar * (tau_bar to_power n) >= (tau * (tau_bar to_power n)) - ((sqrt 5) / 2) by A4, XCMPLX_1:87; then (tau_bar to_power 1) * (tau_bar to_power n) >= (tau * (tau_bar to_power n)) - ((sqrt 5) / 2) by POWER:25; then tau_bar to_power (n + 1) >= (tau * (tau_bar to_power n)) - ((sqrt 5) / 2) by Th2; then - (tau_bar to_power (n + 1)) <= - ((tau * (tau_bar to_power n)) - ((sqrt 5) / 2)) by XREAL_1:24; then (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) <= ((- (tau * (tau_bar to_power n))) + ((sqrt 5) / 2)) + (tau to_power (n + 1)) by XREAL_1:6; then (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) <= ((tau to_power (n + 1)) - (tau * (tau_bar to_power n))) + ((sqrt 5) / 2) ; then (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) <= (((tau to_power n) * (tau to_power 1)) - (tau * (tau_bar to_power n))) + ((sqrt 5) / 2) by Th2; then (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) <= (((tau to_power n) * tau) - (tau * (tau_bar to_power n))) + ((sqrt 5) / 2) by POWER:25; then ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) <= ((tau * ((tau to_power n) - (tau_bar to_power n))) + ((sqrt 5) / 2)) / (sqrt 5) by A2, XREAL_1:72; then Fib (n + 1) <= ((tau * ((tau to_power n) - (tau_bar to_power n))) + ((sqrt 5) / 2)) / (sqrt 5) by FIB_NUM:7; then Fib (n + 1) <= ((tau * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5)) + (((sqrt 5) / 2) / (sqrt 5)) by XCMPLX_1:62; then Fib (n + 1) <= (tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) + (((sqrt 5) / 2) / (sqrt 5)) by XCMPLX_1:74; then Fib (n + 1) <= (tau * (Fib n)) + (((sqrt 5) / 2) / (sqrt 5)) by FIB_NUM:7; then Fib (n + 1) <= (tau * (Fib n)) + (((sqrt 5) / (sqrt 5)) / 2) by XCMPLX_1:48; then Fib (n + 1) <= (tau * (Fib n)) + (1 / 2) by A2, XCMPLX_1:60; hence (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 >= Fib (n + 1) by FIB_NUM:def_1; ::_thesis: verum end; ((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1) proof Fib (n + 1) = [\((tau * (Fib n)) + 1)/] by A1, A3, Th22; then A6: ((tau * (Fib n)) + 1) - 1 < Fib (n + 1) by INT_1:def_6; ((Fib n) + ((sqrt 5) * (Fib n))) + 1 <= ((Fib n) + ((sqrt 5) * (Fib n))) + 2 by XREAL_1:6; then (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 <= (((Fib n) + ((sqrt 5) * (Fib n))) + 2) / 2 by XREAL_1:72; then ((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 <= ((tau * (Fib n)) + 1) - 1 by FIB_NUM:def_1, XREAL_1:9; hence ((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1) by A6, XXREAL_0:2; ::_thesis: verum end; hence Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] by A5, INT_1:def_6; ::_thesis: verum end; supposeA7: n is odd ; ::_thesis: Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] A8: (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 >= Fib (n + 1) proof Fib (n + 1) = [/((tau * (Fib n)) - 1)\] by A1, A7, Th23; then A9: ((tau * (Fib n)) - 1) + 1 > Fib (n + 1) by INT_1:def_7; 1 + ((Fib n) + ((sqrt 5) * (Fib n))) > 0 + ((Fib n) + ((sqrt 5) * (Fib n))) by XREAL_1:6; then (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 > ((Fib n) + ((sqrt 5) * (Fib n))) / 2 by XREAL_1:74; hence (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 >= Fib (n + 1) by A9, FIB_NUM:def_1, XXREAL_0:2; ::_thesis: verum end; ((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1) proof n > 1 by A1, XXREAL_0:2; then (2 * (sqrt 5)) * (tau_bar to_power n) > (2 * (sqrt 5)) * (- (1 / 2)) by A2, Th14, XREAL_1:68; then - ((2 * (sqrt 5)) * (tau_bar to_power n)) < - ((2 * (sqrt 5)) * (- (1 / 2))) by XREAL_1:24; then ((((((1 * (tau to_power n)) + ((sqrt 5) * (tau to_power n))) - ((2 * tau) * (tau to_power n))) + ((2 * tau_bar) * (tau_bar to_power n))) - ((sqrt 5) * (tau_bar to_power n))) - (1 * (tau_bar to_power n))) + ((2 * tau) * (tau to_power n)) < (sqrt 5) + ((2 * tau) * (tau to_power n)) by FIB_NUM:def_1, FIB_NUM:def_2, XREAL_1:6; then (((((tau to_power n) + ((sqrt 5) * (tau to_power n))) + ((2 * tau_bar) * (tau_bar to_power n))) - ((sqrt 5) * (tau_bar to_power n))) - (tau_bar to_power n)) - ((2 * tau_bar) * (tau_bar to_power n)) < ((sqrt 5) + ((2 * tau) * (tau to_power n))) - ((2 * tau_bar) * (tau_bar to_power n)) by XREAL_1:9; then ((1 + (sqrt 5)) * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5) < (((sqrt 5) + ((2 * tau) * (tau to_power n))) - ((2 * tau_bar) * (tau_bar to_power n))) / (sqrt 5) by A2, XREAL_1:74; then (1 + (sqrt 5)) * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) < (((sqrt 5) + (2 * (tau * (tau to_power n)))) - ((2 * tau_bar) * (tau_bar to_power n))) / (sqrt 5) by XCMPLX_1:74; then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * (tau * (tau to_power n)))) - ((2 * tau_bar) * (tau_bar to_power n))) / (sqrt 5) by FIB_NUM:7; then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * ((tau to_power 1) * (tau to_power n)))) - ((2 * tau_bar) * (tau_bar to_power n))) / (sqrt 5) by POWER:25; then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * (tau to_power (n + 1)))) - (2 * (tau_bar * (tau_bar to_power n)))) / (sqrt 5) by Th2; then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * (tau to_power (n + 1)))) - (2 * ((tau_bar to_power 1) * (tau_bar to_power n)))) / (sqrt 5) by POWER:25; then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * (tau to_power (n + 1)))) - (2 * (tau_bar to_power (n + 1)))) / (sqrt 5) by Th2; then (1 + (sqrt 5)) * (Fib n) < ((sqrt 5) + (2 * ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))))) / (sqrt 5) ; then (1 + (sqrt 5)) * (Fib n) < ((sqrt 5) / (sqrt 5)) + ((2 * ((tau to_power (n + 1)) - (tau_bar to_power (n + 1)))) / (sqrt 5)) by XCMPLX_1:62; then (1 + (sqrt 5)) * (Fib n) < ((sqrt 5) / (sqrt 5)) + (2 * (((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5))) by XCMPLX_1:74; then (1 + (sqrt 5)) * (Fib n) < ((sqrt 5) / (sqrt 5)) + (2 * (Fib (n + 1))) by FIB_NUM:7; then (1 + (sqrt 5)) * (Fib n) < 1 + (2 * (Fib (n + 1))) by A2, XCMPLX_1:60; then ((1 + (sqrt 5)) * (Fib n)) / 2 < (1 + (2 * (Fib (n + 1)))) / 2 by XREAL_1:74; then (((1 + (sqrt 5)) * (Fib n)) / 2) - (1 / 2) < ((1 / 2) + (Fib (n + 1))) - (1 / 2) by XREAL_1:9; hence ((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1) ; ::_thesis: verum end; hence Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] by A8, INT_1:def_6; ::_thesis: verum end; end; end; theorem :: FIB_NUM4:25 for n being Nat st n >= 2 holds Fib (n + 1) = [/((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2)\] proof let n be Nat; ::_thesis: ( n >= 2 implies Fib (n + 1) = [/((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2)\] ) assume A1: n >= 2 ; ::_thesis: Fib (n + 1) = [/((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2)\] then Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] by Th24; then A2: ((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1) by INT_1:def_6; ((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2) + 1 > Fib (n + 1) proof Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] by Th24, A1; then A3: ((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2) + 1 >= Fib (n + 1) by INT_1:def_6; ((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2) + 1 <> Fib (n + 1) proof set tn = tau to_power n; set tbn = tau_bar to_power n; set t1 = tau to_power (n + 1); set t2 = tau_bar to_power (n + 1); set s5 = sqrt 5; A4: sqrt 5 > 0 by SQUARE_1:25; assume ((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2) + 1 = Fib (n + 1) ; ::_thesis: contradiction then ((Fib n) * (1 + (sqrt 5))) + 1 = 2 * (Fib (n + 1)) ; then ((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (1 + (sqrt 5))) + 1 = 2 * (Fib (n + 1)) by FIB_NUM:7; then (((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (1 + (sqrt 5))) + 1) * (sqrt 5) = (2 * (((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5))) * (sqrt 5) by FIB_NUM:7; then (((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (1 + (sqrt 5))) * (sqrt 5)) + (1 * (sqrt 5)) = 2 * ((((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5)) * (sqrt 5)) ; then (((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (1 + (sqrt 5))) * (sqrt 5)) + (sqrt 5) = 2 * ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) by A4, XCMPLX_1:87; then (((((tau to_power n) - (tau_bar to_power n)) * (1 + (sqrt 5))) / (sqrt 5)) * (sqrt 5)) + (sqrt 5) = (2 * (tau to_power (n + 1))) - (2 * (tau_bar to_power (n + 1))) by XCMPLX_1:74; then (((tau to_power n) - (tau_bar to_power n)) * (1 + (sqrt 5))) + (sqrt 5) = (2 * (tau to_power (n + 1))) - (2 * (tau_bar to_power (n + 1))) by A4, XCMPLX_1:87; then (((tau to_power n) * (1 + (sqrt 5))) - ((tau_bar to_power n) + ((tau_bar to_power n) * (sqrt 5)))) + (sqrt 5) = (2 * ((tau to_power n) * (tau to_power 1))) - (2 * (tau_bar to_power (n + 1))) by Th2; then (((tau to_power n) * (1 + (sqrt 5))) - ((tau_bar to_power n) * (1 + (sqrt 5)))) + (sqrt 5) = (2 * ((tau to_power n) * (tau to_power 1))) - (2 * ((tau_bar to_power n) * (tau_bar to_power 1))) by Th2; then (((tau to_power n) * (1 + (sqrt 5))) - ((tau_bar to_power n) * (1 + (sqrt 5)))) + (sqrt 5) = (2 * ((tau to_power n) * tau)) - (2 * ((tau_bar to_power n) * (tau_bar to_power 1))) by POWER:25; then (((tau to_power n) - (tau_bar to_power n)) * (1 + (sqrt 5))) + (sqrt 5) = (2 * ((tau to_power n) * tau)) - (2 * ((tau_bar to_power n) * tau_bar)) by POWER:25; then (((tau to_power n) * ((1 + (sqrt 5)) - (2 * tau))) + ((tau_bar to_power n) * ((2 * tau_bar) - (1 + (sqrt 5))))) + (sqrt 5) = 0 ; then ((- (2 * (tau_bar to_power n))) + 1) * (sqrt 5) = 0 by FIB_NUM:def_1, FIB_NUM:def_2; then (- (2 * (tau_bar to_power n))) + 1 = 0 by A4; hence contradiction by Th8, A1; ::_thesis: verum end; hence ((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2) + 1 > Fib (n + 1) by A3, XXREAL_0:1; ::_thesis: verum end; hence Fib (n + 1) = [/((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2)\] by A2, INT_1:def_7; ::_thesis: verum end; 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 let n be Nat; ::_thesis: Fib (n + 1) = ((Fib n) + (sqrt ((5 * ((Fib n) ^2)) + (4 * ((- 1) to_power n))))) / 2 A1: n - 0 is Element of NAT by NAT_1:21; A2: 2 * (Fib (n + 1)) = (Fib n) + (Lucas n) by FIB_NUM3:24; A3: ((Lucas n) ^2) - (5 * ((Fib n) ^2)) = ((Lucas n) to_power 2) - (5 * ((Fib n) ^2)) by POWER:46 .= ((Lucas n) to_power 2) - (5 * ((Fib n) to_power 2)) by POWER:46 .= - ((5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2)) .= - (4 * ((- 1) to_power (n + 1))) by A1, FIB_NUM3:30 .= (- 1) * (((- 1) to_power (n + 1)) * 4) .= ((- 1) to_power 1) * (((- 1) to_power (n + 1)) * 4) by POWER:25 .= (((- 1) to_power 1) * ((- 1) to_power (n + 1))) * 4 .= ((- 1) to_power ((n + 1) + 1)) * 4 by Th2 .= ((- 1) to_power (n + 2)) * 4 .= (((- 1) to_power n) * ((- 1) to_power 2)) * 4 by Th2 .= (((- 1) to_power n) * 1) * 4 by FIB_NUM2:3, POLYFORM:5 ; Fib (n + 1) = ((Fib n) + (Lucas n)) / 2 by A2; hence Fib (n + 1) = ((Fib n) + (sqrt ((5 * ((Fib n) ^2)) + (4 * ((- 1) to_power n))))) / 2 by A3, SQUARE_1:def_2; ::_thesis: verum 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)/] proof let n be Nat; ::_thesis: ( n >= 2 implies Fib (n + 1) = [\((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1))) / 2)/] ) assume A1: n >= 2 ; ::_thesis: Fib (n + 1) = [\((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1))) / 2)/] A2: n - 0 is Element of NAT by NAT_1:21; A3: n - 1 >= 2 - 1 by A1, XREAL_1:9; ((n + 1) -' 1) + 1 = ((n + 1) - 1) + 1 by NAT_D:37 .= ((n - 1) + 1) + 1 .= ((n -' 1) + 1) + 1 by A3, NAT_D:39 ; then A4: Fib (n + 1) = Fib (((n -' 1) + 1) + 1) by NAT_D:34 .= (Fib (n -' 1)) + (Fib ((n -' 1) + 1)) by PRE_FF:1 .= (Fib (n -' 1)) + (Fib ((n + 1) -' 1)) by A1, NAT_D:38, XXREAL_0:2 .= (Fib (n -' 1)) + (Fib n) by NAT_D:34 ; n + 2 >= 2 + 2 by A1, XREAL_1:6; then reconsider p = (n + 2) - 1 as Nat by NAT_1:21, XXREAL_0:2; A5: (Lucas n) - (Fib n) = (Lucas ((n + 1) -' 1)) - (Fib n) by NAT_D:34 .= (Lucas ((n -' 1) + 1)) - (Fib n) by A1, NAT_D:38, XXREAL_0:2 .= ((Fib (n -' 1)) + (Fib ((n -' 1) + 2))) - (Fib n) by FIB_NUM3:20 .= ((Fib (n -' 1)) + (Fib ((n + 2) -' 1))) - (Fib n) by A1, NAT_D:38, XXREAL_0:2 .= ((Fib (n -' 1)) + (Fib p)) - (Fib n) by NAT_D:37 .= 2 * (Fib (n -' 1)) by A4 ; A6: ((Lucas n) ^2) - (5 * ((Fib n) ^2)) = ((Lucas n) ^2) - (5 * ((Fib n) to_power 2)) by POWER:46 .= ((Lucas n) to_power 2) - (5 * ((Fib n) |^ 2)) by POWER:46 .= (- 1) * ((5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2)) .= (- 1) * (4 * ((- 1) to_power (n + 1))) by A2, FIB_NUM3:30 .= 4 * ((- 1) * ((- 1) to_power (n + 1))) .= 4 * (((- 1) to_power 1) * ((- 1) to_power (n + 1))) by POWER:25 .= 4 * ((- 1) to_power (1 + (n + 1))) by Th2 .= 4 * ((- 1) to_power (n + 2)) .= 4 * (((- 1) to_power n) * ((- 1) to_power 2)) by Th2 .= 4 * (((- 1) to_power n) * ((- 1) ^2)) by POWER:46 .= 4 * ((- 1) to_power n) ; ( n -' 1 >= 2 -' 1 & 2 - 1 >= 1 ) by A1, NAT_D:42; then n -' 1 >= 2 - 1 by NAT_D:39; then A7: Fib (n -' 1) >= 1 by FIB_NUM2:45, PRE_FF:1; 1 >= (- 1) to_power n proof percases ( n is even or n is odd ) ; suppose n is even ; ::_thesis: 1 >= (- 1) to_power n hence 1 >= (- 1) to_power n by FIB_NUM2:3; ::_thesis: verum end; suppose n is odd ; ::_thesis: 1 >= (- 1) to_power n hence 1 >= (- 1) to_power n by FIB_NUM2:2; ::_thesis: verum end; end; end; then (- 1) to_power n <= Fib (n -' 1) by A7, XXREAL_0:2; then ((Lucas n) ^2) - (5 * ((Fib n) ^2)) <= (2 * 2) * (Fib (n -' 1)) by A6, XREAL_1:64; then (((Lucas n) ^2) - (5 * ((Fib n) ^2))) - (2 * (Lucas n)) <= ((2 * (Lucas n)) - (2 * (Fib n))) - (2 * (Lucas n)) by A5, XREAL_1:9; then ((((Lucas n) ^2) - (5 * ((Fib n) ^2))) - (2 * (Lucas n))) + 1 <= (- (2 * (Fib n))) + 1 by XREAL_1:6; then A8: (((((Lucas n) ^2) - (5 * ((Fib n) ^2))) - (2 * (Lucas n))) + 1) + (5 * ((Fib n) ^2)) <= ((- (2 * (Fib n))) + 1) + (5 * ((Fib n) ^2)) by XREAL_1:6; A9: (n + 2) -' 1 = (n + 2) - 1 by NAT_D:37 .= n + 1 ; A10: Lucas n = Lucas ((n + 1) -' 1) by NAT_D:34 .= Lucas ((n -' 1) + 1) by A1, NAT_D:38, XXREAL_0:2 .= (Fib (n -' 1)) + (Fib ((n -' 1) + 2)) by FIB_NUM3:20 .= (Fib (n -' 1)) + (Fib ((n + 2) -' 1)) by A1, NAT_D:38, XXREAL_0:2 .= (2 * (Fib (n + 1))) - (Fib n) by A4, A9 ; A11: 2 * (Fib (n -' 1)) >= 2 * 0 ; n >= 1 by A1, XXREAL_0:2; then A12: Fib n >= 1 by FIB_NUM2:45, PRE_FF:1; then - (Fib n) <= - 1 by XREAL_1:24; then (- (Fib n)) + 1 <= (- 1) + 1 by XREAL_1:6; then (2 * (Fib (n -' 1))) + (Fib n) >= ((- (Fib n)) + 1) + (Fib n) by A11, XREAL_1:6; then A13: ((2 * (Fib (n -' 1))) + (Fib n)) - 1 >= 1 - 1 by XREAL_1:9; sqrt ((((2 * (Fib (n + 1))) - (Fib n)) - 1) ^2) <= sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1) by A10, A8, SQUARE_1:26; then ((2 * (Fib (n + 1))) - (Fib n)) - 1 <= sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1) by A4, A13, SQUARE_1:22; then (((2 * (Fib (n + 1))) - (Fib n)) - 1) + (Fib n) <= (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1)) + (Fib n) by XREAL_1:6; then ((((2 * (Fib (n + 1))) - (Fib n)) - 1) + (Fib n)) + 1 <= ((sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1)) + (Fib n)) + 1 by XREAL_1:6; then A14: (2 * (Fib (n + 1))) / 2 <= (((sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1)) + (Fib n)) + 1) / 2 by XREAL_1:72; A15: (5 * ((Fib n) ^2)) - (2 * (Fib n)) = ((5 * (Fib n)) - 2) * (Fib n) ; 5 * (Fib n) >= 5 * 1 by A12, XREAL_1:64; then (5 * (Fib n)) - 2 >= 5 - 2 by XREAL_1:9; then A16: (5 * (Fib n)) - 2 >= 0 by XXREAL_0:2; A17: (((Fib (n + 1)) + (Fib (n + 1))) - (Fib n)) + 1 = ((Fib (n + 1)) + (Fib (n -' 1))) + 1 by A4; ((Lucas n) ^2) - (5 * ((Fib n) ^2)) > - (2 * ((Lucas n) + (Fib n))) proof A18: Fib n > 0 by A1, FIB_NUM2:21, FIB_NUM2:45; Lucas n >= n by FIB_NUM3:17; then Lucas n >= 2 by A1, XXREAL_0:2; then (Lucas n) + (Fib n) > 0 + 2 by A18, XREAL_1:8; then ((Lucas n) + (Fib n)) * 2 > 2 * 2 by XREAL_1:68; then A19: - (((Lucas n) + (Fib n)) * 2) < - 4 by XREAL_1:24; - 4 <= 4 * ((- 1) to_power n) by Lm1; hence ((Lucas n) ^2) - (5 * ((Fib n) ^2)) > - (2 * ((Lucas n) + (Fib n))) by A6, A19, XXREAL_0:2; ::_thesis: verum end; then (((Lucas n) ^2) - (5 * ((Fib n) ^2))) + (2 * (Lucas n)) > (- (2 * ((Lucas n) + (Fib n)))) + (2 * (Lucas n)) by XREAL_1:6; then ((((Lucas n) ^2) - (5 * ((Fib n) ^2))) + (2 * (Lucas n))) + (5 * ((Fib n) ^2)) > (- (2 * (Fib n))) + (5 * ((Fib n) ^2)) by XREAL_1:6; then (((Lucas n) ^2) + ((2 * (Lucas n)) * 1)) + (1 ^2) > ((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + (1 ^2) by XREAL_1:6; then sqrt ((((2 * (Fib (n + 1))) - (Fib n)) + 1) ^2) > sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1) by A16, A15, A10, SQUARE_1:27; then ((2 * (Fib (n + 1))) - (Fib n)) + 1 > sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1) by A17, SQUARE_1:22; then (((2 * (Fib (n + 1))) - (Fib n)) + 1) - 1 > (sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1)) - 1 by XREAL_1:9; then ((2 * (Fib (n + 1))) - (Fib n)) + (Fib n) > ((sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1)) - 1) + (Fib n) by XREAL_1:6; then (2 * (Fib (n + 1))) / 2 > (((sqrt (((- (2 * (Fib n))) + (5 * ((Fib n) ^2))) + 1)) - 1) + (Fib n)) / 2 by XREAL_1:74; then ((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1))) / 2) - 1 < Fib (n + 1) ; hence Fib (n + 1) = [\((((Fib n) + 1) + (sqrt (((5 * ((Fib n) ^2)) - (2 * (Fib n))) + 1))) / 2)/] by A14, INT_1:def_6; ::_thesis: verum 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) ; theorem :: FIB_NUM4:28 for n being Nat st n >= 2 holds Fib n = [\((1 / tau) * ((Fib (n + 1)) + (1 / 2)))/] proof let n be Nat; ::_thesis: ( n >= 2 implies Fib n = [\((1 / tau) * ((Fib (n + 1)) + (1 / 2)))/] ) assume A1: n >= 2 ; ::_thesis: Fib n = [\((1 / tau) * ((Fib (n + 1)) + (1 / 2)))/] then A2: n > 1 by XXREAL_0:2; set tbn = tau_bar to_power n; sqrt 5 < sqrt (5 ^2) by SQUARE_1:27; then sqrt 5 < 5 by SQUARE_1:def_2; then A3: (sqrt 5) - 5 < 5 - 5 by XREAL_1:9; A4: (1 / tau) * ((Fib (n + 1)) + (1 / 2)) >= Fib n proof set tbm = tau_bar to_power (n + 1); set tn = tau to_power n; ((tau_bar to_power (n + 1)) / tau) - ((sqrt 5) / (2 * tau)) <= tau_bar to_power n proof percases ( n is even or n is odd ) ; supposeA5: n is even ; ::_thesis: ((tau_bar to_power (n + 1)) / tau) - ((sqrt 5) / (2 * tau)) <= tau_bar to_power n (sqrt 5) / (((sqrt 5) - 5) * tau) <= tau_bar to_power n by Lm21, A2, Th14; then ((sqrt 5) / (((sqrt 5) - 5) * tau)) * (((sqrt 5) - 5) * tau) >= (tau_bar to_power n) * (((sqrt 5) - 5) * tau) by A3, XREAL_1:65; then A6: sqrt 5 >= (tau_bar to_power n) * (((sqrt 5) - 5) * tau) by A3, XCMPLX_1:87; A7: tau_bar to_power n > 0 by Th6, A5; then (sqrt 5) / (tau_bar to_power n) >= ((tau * ((sqrt 5) - 5)) * (tau_bar to_power n)) / (tau_bar to_power n) by A6, XREAL_1:72; then (sqrt 5) / (tau_bar to_power n) >= tau * ((sqrt 5) - 5) by A7, XCMPLX_1:89; then ((sqrt 5) / (tau_bar to_power n)) / tau >= (((sqrt 5) - 5) * tau) / tau by XREAL_1:72; then ((sqrt 5) / (tau_bar to_power n)) / tau >= (sqrt 5) - 5 by XCMPLX_1:89; then (sqrt 5) / ((tau_bar to_power n) * tau) >= (sqrt 5) - 5 by XCMPLX_1:78; then ((sqrt 5) / ((tau_bar to_power n) * tau)) + ((- (sqrt 5)) + 5) >= ((sqrt 5) - 5) + ((- (sqrt 5)) + 5) by XREAL_1:6; then - ((((sqrt 5) / ((tau_bar to_power n) * tau)) - (sqrt 5)) + 5) <= 0 ; then (((- ((sqrt 5) / ((tau_bar to_power n) * tau))) + (sqrt 5)) - 5) + 2 <= 0 + 2 by XREAL_1:6; then ((- ((sqrt 5) / ((tau_bar to_power n) * tau))) + ((sqrt 5) - 3)) / 2 <= 2 / 2 by XREAL_1:72; then (- (((sqrt 5) / ((tau_bar to_power n) * tau)) / 2)) + (tau_bar / tau) <= 1 by Lm4; then (- ((sqrt 5) / (((tau_bar to_power n) * tau) * 2))) + (tau_bar / tau) <= 1 by XCMPLX_1:78; then ((tau_bar / tau) - ((sqrt 5) / ((2 * (tau_bar to_power n)) * tau))) * (tau_bar to_power n) <= 1 * (tau_bar to_power n) by A7, XREAL_1:64; then ((tau_bar / tau) * (tau_bar to_power n)) - (((sqrt 5) / ((2 * (tau_bar to_power n)) * tau)) * (tau_bar to_power n)) <= tau_bar to_power n ; then ((tau_bar * (tau_bar to_power n)) / tau) - (((sqrt 5) / ((2 * (tau_bar to_power n)) * tau)) * (tau_bar to_power n)) <= tau_bar to_power n by XCMPLX_1:74; then (((tau_bar to_power 1) * (tau_bar to_power n)) / tau) - (((sqrt 5) / ((2 * (tau_bar to_power n)) * tau)) * (tau_bar to_power n)) <= tau_bar to_power n by POWER:25; then ((tau_bar to_power (n + 1)) / tau) - (((sqrt 5) / ((2 * tau) * (tau_bar to_power n))) * (tau_bar to_power n)) <= tau_bar to_power n by Th2; then ((tau_bar to_power (n + 1)) / tau) - ((((sqrt 5) / (2 * tau)) / (tau_bar to_power n)) * (tau_bar to_power n)) <= tau_bar to_power n by XCMPLX_1:78; hence ((tau_bar to_power (n + 1)) / tau) - ((sqrt 5) / (2 * tau)) <= tau_bar to_power n by A7, XCMPLX_1:87; ::_thesis: verum end; suppose n is odd ; ::_thesis: ((tau_bar to_power (n + 1)) / tau) - ((sqrt 5) / (2 * tau)) <= tau_bar to_power n then A8: tau_bar to_power n < 0 by Th7; (sqrt 5) / (tau * ((sqrt 5) - 5)) <= tau_bar to_power n by Lm21, A2, Th14; then ((sqrt 5) / (tau * ((sqrt 5) - 5))) * ((sqrt 5) - 5) >= (tau_bar to_power n) * ((sqrt 5) - 5) by A3, XREAL_1:65; then (((sqrt 5) / tau) / ((sqrt 5) - 5)) * ((sqrt 5) - 5) >= (tau_bar to_power n) * ((sqrt 5) - 5) by XCMPLX_1:78; then (sqrt 5) / tau >= (tau_bar to_power n) * ((sqrt 5) - 5) by A3, XCMPLX_1:87; then ((sqrt 5) / tau) / (tau_bar to_power n) <= ((tau_bar to_power n) * ((sqrt 5) - 5)) / (tau_bar to_power n) by A8, XREAL_1:73; then (sqrt 5) / (tau * (tau_bar to_power n)) <= ((tau_bar to_power n) * ((sqrt 5) - 5)) / (tau_bar to_power n) by XCMPLX_1:78; then (sqrt 5) / (tau * (tau_bar to_power n)) <= (sqrt 5) - 5 by A8, XCMPLX_1:89; then - ((sqrt 5) / (tau * (tau_bar to_power n))) >= - ((sqrt 5) - 5) by XREAL_1:24; then (- ((sqrt 5) / (tau * (tau_bar to_power n)))) + ((sqrt 5) - 3) >= ((- (sqrt 5)) + 5) + ((sqrt 5) - 3) by XREAL_1:6; then ((- ((sqrt 5) / (tau * (tau_bar to_power n)))) + ((sqrt 5) - 3)) / 2 >= 2 / 2 by XREAL_1:72; then (tau_bar / tau) - (((sqrt 5) / (tau * (tau_bar to_power n))) / 2) >= 1 by Lm4; then (tau_bar / tau) - ((sqrt 5) / ((tau * (tau_bar to_power n)) * 2)) >= 1 by XCMPLX_1:78; then ((tau_bar / tau) - ((sqrt 5) / ((tau * (tau_bar to_power n)) * 2))) * (tau_bar to_power n) <= 1 * (tau_bar to_power n) by A8, XREAL_1:65; then ((tau_bar / tau) * (tau_bar to_power n)) - (((sqrt 5) / ((tau * 2) * (tau_bar to_power n))) * (tau_bar to_power n)) <= tau_bar to_power n ; then ((tau_bar / tau) * (tau_bar to_power n)) - ((((sqrt 5) / (tau * 2)) / (tau_bar to_power n)) * (tau_bar to_power n)) <= tau_bar to_power n by XCMPLX_1:78; then ((tau_bar / tau) * (tau_bar to_power n)) - ((sqrt 5) / (tau * 2)) <= tau_bar to_power n by A8, XCMPLX_1:87; then ((tau_bar * (tau_bar to_power n)) / tau) - ((sqrt 5) / (tau * 2)) <= tau_bar to_power n by XCMPLX_1:74; then (((tau_bar to_power 1) * (tau_bar to_power n)) / tau) - ((sqrt 5) / (tau * 2)) <= tau_bar to_power n by POWER:25; hence ((tau_bar to_power (n + 1)) / tau) - ((sqrt 5) / (2 * tau)) <= tau_bar to_power n by Th2; ::_thesis: verum end; end; end; then - (((tau_bar to_power (n + 1)) / tau) - ((sqrt 5) / (2 * tau))) >= - (tau_bar to_power n) by XREAL_1:24; then ((- ((tau_bar to_power (n + 1)) / tau)) + ((sqrt 5) / (2 * tau))) + (((tau to_power n) * tau) / tau) >= (- (tau_bar to_power n)) + (((tau to_power n) * tau) / tau) by XREAL_1:6; then ((((tau to_power n) * tau) / tau) - ((tau_bar to_power (n + 1)) / tau)) + ((sqrt 5) / (2 * tau)) >= (- (tau_bar to_power n)) + (((tau to_power n) * tau) / tau) ; then ((((tau to_power n) * tau) - (tau_bar to_power (n + 1))) / tau) + ((sqrt 5) / (2 * tau)) >= (- (tau_bar to_power n)) + (((tau to_power n) * tau) / tau) by XCMPLX_1:120; then ((((tau to_power n) * tau) - (tau_bar to_power (n + 1))) / tau) + ((sqrt 5) / (2 * tau)) >= (- (tau_bar to_power n)) + (tau to_power n) by XCMPLX_1:89; then ((((tau to_power n) * (tau to_power 1)) - (tau_bar to_power (n + 1))) / tau) + ((sqrt 5) / (2 * tau)) >= (tau to_power n) - (tau_bar to_power n) by POWER:25; then (((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / tau) + ((sqrt 5) / (2 * tau)) >= (tau to_power n) - (tau_bar to_power n) by Th2; then ((((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / tau) + ((sqrt 5) / (2 * tau))) / (sqrt 5) >= ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) by Lm20, XREAL_1:72; then ((((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / tau) + ((sqrt 5) / (2 * tau))) / (sqrt 5) >= Fib n by FIB_NUM:7; then ((((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / tau) / (sqrt 5)) + (((sqrt 5) / (2 * tau)) / (sqrt 5)) >= Fib n by XCMPLX_1:62; then ((((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5)) / tau) + (((sqrt 5) / (2 * tau)) / (sqrt 5)) >= Fib n by XCMPLX_1:48; then ((Fib (n + 1)) / tau) + (((sqrt 5) / (2 * tau)) / (sqrt 5)) >= Fib n by FIB_NUM:7; then ((Fib (n + 1)) / tau) + ((1 / (2 * tau)) * ((sqrt 5) / (sqrt 5))) >= Fib n by XCMPLX_1:104; then ((Fib (n + 1)) / tau) + ((1 / (2 * tau)) * 1) >= Fib n by Lm20, XCMPLX_1:60; then ((Fib (n + 1)) / tau) + ((1 / 2) / tau) >= Fib n by XCMPLX_1:78; then ((Fib (n + 1)) + (1 / 2)) / tau >= Fib n by XCMPLX_1:62; hence (1 / tau) * ((Fib (n + 1)) + (1 / 2)) >= Fib n by XCMPLX_1:99; ::_thesis: verum end; ((1 / tau) * ((Fib (n + 1)) + (1 / 2))) - 1 < Fib n proof 1 < sqrt 5 by SQUARE_1:18, SQUARE_1:27; then 1 / 2 < (sqrt 5) / 2 by XREAL_1:74; then tau_bar to_power n < (sqrt 5) / 2 by Th8, A1, XXREAL_0:2; then (tau_bar to_power n) * (sqrt 5) < (tau - (1 / 2)) * (sqrt 5) by Lm20, FIB_NUM:def_1, XREAL_1:68; then ((tau_bar to_power n) * tau) - ((tau_bar to_power n) * tau_bar) < (tau * (sqrt 5)) - ((1 * (sqrt 5)) / 2) by FIB_NUM:def_1, FIB_NUM:def_2; then ((tau_bar to_power n) * tau) - ((tau_bar to_power n) * (tau_bar to_power 1)) < (tau * (sqrt 5)) - ((sqrt 5) / 2) by POWER:25; then ((tau_bar to_power n) * tau) - (tau_bar to_power (n + 1)) < (tau * (sqrt 5)) - ((sqrt 5) / 2) by Th2; then (((tau_bar to_power n) * tau) - (tau_bar to_power (n + 1))) + ((sqrt 5) / 2) < ((tau * (sqrt 5)) - ((sqrt 5) / 2)) + ((sqrt 5) / 2) by XREAL_1:6; then ((((tau_bar to_power n) * tau) - (tau_bar to_power (n + 1))) + ((sqrt 5) / 2)) - ((tau_bar to_power n) * tau) < (tau * (sqrt 5)) - ((tau_bar to_power n) * tau) by XREAL_1:9; then ((- (tau_bar to_power (n + 1))) + ((sqrt 5) / 2)) - (tau * (sqrt 5)) < ((tau * (sqrt 5)) - ((tau_bar to_power n) * tau)) - (tau * (sqrt 5)) by XREAL_1:9; then (((- (tau_bar to_power (n + 1))) + ((sqrt 5) / 2)) - (tau * (sqrt 5))) / tau < (- ((tau_bar to_power n) * tau)) / tau by XREAL_1:74; then (((- (tau_bar to_power (n + 1))) / tau) + (((sqrt 5) / 2) / tau)) - ((tau * (sqrt 5)) / tau) < (- ((tau_bar to_power n) * tau)) / tau by XCMPLX_1:124; then ((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - ((tau * (sqrt 5)) / tau) < ((- (tau_bar to_power n)) * tau) / tau by XCMPLX_1:187; then ((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - ((tau * (sqrt 5)) / tau) < - (tau_bar to_power n) by XCMPLX_1:89; then ((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - (sqrt 5) < - (tau_bar to_power n) by XCMPLX_1:89; then (((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - (sqrt 5)) + ((tau to_power n) * 1) < (- (tau_bar to_power n)) + (tau to_power n) by XREAL_1:6; then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - (sqrt 5)) + ((tau to_power n) * 1)) / (sqrt 5) < ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) by Lm20, XREAL_1:74; then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - (sqrt 5)) + ((tau to_power n) * 1)) / (sqrt 5) < Fib n by FIB_NUM:7; then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - (sqrt 5)) + ((tau to_power n) * (tau / tau))) / (sqrt 5) < Fib n by XCMPLX_1:60; then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) + ((tau to_power n) * (tau / tau))) - (sqrt 5)) / (sqrt 5) < Fib n ; then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) + (((tau to_power n) * tau) / tau)) - (sqrt 5)) / (sqrt 5) < Fib n by XCMPLX_1:74; then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) + (((tau to_power n) * tau) / tau)) / (sqrt 5)) - ((sqrt 5) / (sqrt 5)) < Fib n by XCMPLX_1:120; then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) + (((tau to_power n) * tau) / tau)) / (sqrt 5)) - 1 < Fib n by Lm20, XCMPLX_1:60; then (((((- (tau_bar to_power (n + 1))) / tau) + (((sqrt 5) / 2) / tau)) + (((tau to_power n) * tau) / tau)) / (sqrt 5)) - 1 < Fib n by XCMPLX_1:187; then (((((- (tau_bar to_power (n + 1))) + ((sqrt 5) / 2)) + ((tau to_power n) * tau)) / tau) / (sqrt 5)) - 1 < Fib n by XCMPLX_1:63; then (((((- (tau_bar to_power (n + 1))) + ((sqrt 5) / 2)) + ((tau to_power n) * tau)) / (sqrt 5)) / tau) - 1 < Fib n by XCMPLX_1:48; then (((((- (tau_bar to_power (n + 1))) + ((tau to_power n) * tau)) + ((sqrt 5) / 2)) / (sqrt 5)) * (1 / tau)) - 1 < Fib n by XCMPLX_1:99; then (((((- (tau_bar to_power (n + 1))) + ((tau to_power n) * tau)) / (sqrt 5)) + (((sqrt 5) / 2) / (sqrt 5))) * (1 / tau)) - 1 < Fib n by XCMPLX_1:62; then (((((- (tau_bar to_power (n + 1))) + ((tau to_power n) * (tau to_power 1))) / (sqrt 5)) + (((sqrt 5) / 2) / (sqrt 5))) * (1 / tau)) - 1 < Fib n by POWER:25; then (((((- (tau_bar to_power (n + 1))) + (tau to_power (n + 1))) / (sqrt 5)) + (((sqrt 5) / 2) / (sqrt 5))) * (1 / tau)) - 1 < Fib n by Th2; then (((((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5)) + (((sqrt 5) / 2) / (sqrt 5))) * (1 / tau)) - 1 < Fib n ; then (((Fib (n + 1)) + (((sqrt 5) / 2) / (sqrt 5))) * (1 / tau)) - 1 < Fib n by FIB_NUM:7; then (((Fib (n + 1)) + (((sqrt 5) / (sqrt 5)) / 2)) * (1 / tau)) - 1 < Fib n by XCMPLX_1:48; hence ((1 / tau) * ((Fib (n + 1)) + (1 / 2))) - 1 < Fib n by Lm20, XCMPLX_1:60; ::_thesis: verum end; hence Fib n = [\((1 / tau) * ((Fib (n + 1)) + (1 / 2)))/] by A4, INT_1:def_6; ::_thesis: verum end; 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) proof let n, k be Nat; ::_thesis: ( ( ( n >= k & k > 1 ) or ( k = 1 & n > k ) ) implies [\(((tau to_power k) * (Fib n)) + (1 / 2))/] = Fib (n + k) ) set tb = tau_bar ; set tk = tau to_power k; set tbk = tau_bar to_power k; set ts = tau to_power (n + k); set tbs = tau_bar to_power (n + k); set tn = tau to_power n; set tbn = tau_bar to_power n; assume A1: ( ( n >= k & k > 1 ) or ( k = 1 & n > k ) ) ; ::_thesis: [\(((tau to_power k) * (Fib n)) + (1 / 2))/] = Fib (n + k) A2: (tau to_power k) * (Fib n) = (tau to_power k) * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) by FIB_NUM:7 .= ((tau to_power k) * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5) by XCMPLX_1:74 .= ((((tau to_power k) * (tau to_power n)) - (tau_bar to_power (n + k))) + ((tau_bar to_power (n + k)) - ((tau to_power k) * (tau_bar to_power n)))) / (sqrt 5) .= (((tau to_power (n + k)) - (tau_bar to_power (n + k))) + ((tau_bar to_power (n + k)) - ((tau to_power k) * (tau_bar to_power n)))) / (sqrt 5) by Th2 .= (((tau to_power (n + k)) - (tau_bar to_power (n + k))) / (sqrt 5)) + (((tau_bar to_power (n + k)) - ((tau to_power k) * (tau_bar to_power n))) / (sqrt 5)) by XCMPLX_1:62 .= (Fib (n + k)) + (((tau_bar to_power (n + k)) - ((tau to_power k) * (tau_bar to_power n))) / (sqrt 5)) by FIB_NUM:7 .= (Fib (n + k)) + ((((tau_bar to_power n) * (tau_bar to_power k)) - ((tau to_power k) * (tau_bar to_power n))) / (sqrt 5)) by Th2 .= (Fib (n + k)) + (((- (tau_bar to_power n)) * ((tau to_power k) - (tau_bar to_power k))) / (sqrt 5)) .= (Fib (n + k)) + ((- (tau_bar to_power n)) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5))) by XCMPLX_1:74 .= (Fib (n + k)) + ((- (tau_bar to_power n)) * (Fib k)) by FIB_NUM:7 .= (Fib (n + k)) - ((tau_bar to_power n) * (Fib k)) ; A3: ((tau to_power k) * (Fib n)) + (1 / 2) >= Fib (n + k) proof (tau_bar to_power n) * (Fib k) <= 1 / 2 proof percases ( n is even or n is odd ) ; supposeA4: n is even ; ::_thesis: (tau_bar to_power n) * (Fib k) <= 1 / 2 consider m being Nat such that A5: n = k + m by A1, NAT_1:10; A6: sqrt 5 > 0 by SQUARE_1:25; set tbm = tau_bar to_power m; (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 proof percases ( k is even or k is odd ) ; supposeA7: k is even ; ::_thesis: (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 tau_bar to_power (2 * k) > 0 by Th6; then A8: (- (tau_bar to_power (2 * k))) + 1 < 0 + 1 by XREAL_1:6; tau_bar to_power (2 * k) < 1 by Th8, A1, XXREAL_0:2; then - (tau_bar to_power (2 * k)) > - 1 by XREAL_1:24; then A9: (- (tau_bar to_power (2 * k))) + 1 > (- 1) + 1 by XREAL_1:6; m is even by A4, A5, A7; then A10: tau_bar to_power m > 0 by Th6; tau_bar to_power m <= (sqrt 5) / 2 proof A11: sqrt 5 > 2 by SQUARE_1:20, SQUARE_1:27; percases ( m = 0 or m > 0 ) ; supposeA12: m = 0 ; ::_thesis: tau_bar to_power m <= (sqrt 5) / 2 (sqrt 5) / 2 >= 2 / 2 by A11, XREAL_1:72; hence tau_bar to_power m <= (sqrt 5) / 2 by A12, POWER:24; ::_thesis: verum end; supposeA13: m > 0 ; ::_thesis: tau_bar to_power m <= (sqrt 5) / 2 sqrt 5 >= 1 by A11, XXREAL_0:2; then (sqrt 5) / 2 >= 1 / 2 by XREAL_1:72; hence tau_bar to_power m <= (sqrt 5) / 2 by A13, Th8, XXREAL_0:2; ::_thesis: verum end; end; end; then abs (tau_bar to_power m) <= (sqrt 5) / 2 by A10, ABSVALUE:def_1; then A14: (abs (tau_bar to_power m)) * (1 - (tau_bar to_power (2 * k))) <= ((sqrt 5) / 2) * 1 by A8, A9, XREAL_1:66; (tau_bar to_power m) * (1 - (tau_bar to_power (2 * k))) <= (abs (tau_bar to_power m)) * (1 - (tau_bar to_power (2 * k))) by A9, ABSVALUE:4, XREAL_1:64; then (tau_bar to_power m) * (1 - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by A14, XXREAL_0:2; hence (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by A7, FIB_NUM2:3; ::_thesis: verum end; supposeA15: k is odd ; ::_thesis: (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 then A16: m is odd by A4, A5; m <> 0 by A15, A4, A5; then A17: m >= 1 by NAT_1:14; percases ( m = 1 or m > 1 ) by A17, XXREAL_0:1; supposeA18: m = 1 ; ::_thesis: (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 tau_bar * ((- 1) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 proof A19: tau_bar to_power (2 * k) > 0 by Th6; tau_bar to_power (2 * k) < 1 / 2 by Th8, A1; then (tau_bar to_power (2 * k)) + 1 < (1 / 2) + 1 by XREAL_1:6; then (((sqrt 5) - 1) / (sqrt 5)) * (1 + (tau_bar to_power (2 * k))) < (6 / 10) * (3 / 2) by Lm23, Lm24, A19, XREAL_1:98; then ( (((sqrt 5) - 1) / (sqrt 5)) * (1 + (tau_bar to_power (2 * k))) < 1 & sqrt 5 > 0 ) by SQUARE_1:25, XXREAL_0:2; then ((((sqrt 5) - 1) / (sqrt 5)) * (1 + (tau_bar to_power (2 * k)))) * (sqrt 5) < 1 * (sqrt 5) by XREAL_1:68; then ((((sqrt 5) - 1) * (1 / (sqrt 5))) * (1 + (tau_bar to_power (2 * k)))) * (sqrt 5) < sqrt 5 by XCMPLX_1:99; then (((sqrt 5) - 1) * (1 + (tau_bar to_power (2 * k)))) * ((sqrt 5) * (1 / (sqrt 5))) < sqrt 5 ; then ( (((sqrt 5) - 1) * (1 + (tau_bar to_power (2 * k)))) * ((sqrt 5) / (sqrt 5)) < 1 * (sqrt 5) & sqrt 5 > 0 ) by SQUARE_1:25, XCMPLX_1:99; then (((sqrt 5) - 1) * (1 + (tau_bar to_power (2 * k)))) * 1 < sqrt 5 by XCMPLX_1:60; then ((1 - (sqrt 5)) * ((- 1) - (tau_bar to_power (2 * k)))) / 2 < (sqrt 5) / 2 by XREAL_1:74; hence tau_bar * ((- 1) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by FIB_NUM:def_2; ::_thesis: verum end; then (tau_bar to_power m) * ((- 1) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by A18, POWER:25; hence (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by A15, FIB_NUM2:2; ::_thesis: verum end; supposeA20: m > 1 ; ::_thesis: (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 A21: tau_bar to_power m < 0 by A16, Th7; A22: (tau_bar to_power m) * ((- 1) - (tau_bar to_power (2 * k))) = - ((tau_bar to_power m) * (1 + (tau_bar to_power (2 * k)))) ; A23: tau_bar to_power (2 * k) > 0 by Th6; tau_bar to_power (2 * k) <= 1 / 2 by A1, Th8; then A24: (tau_bar to_power (2 * k)) + 1 <= (1 / 2) + 1 by XREAL_1:6; tau_bar to_power m > - (1 / 2) by Th14, A20; then - (tau_bar to_power m) < - (- (1 / 2)) by XREAL_1:24; then (- (tau_bar to_power m)) * (1 + (tau_bar to_power (2 * k))) <= (1 / 2) * (3 / 2) by A21, A23, A24, XREAL_1:66; then - ((tau_bar to_power m) * (1 + (tau_bar to_power (2 * k)))) <= (sqrt 5) / 2 by Lm25, XXREAL_0:2; hence (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by A15, A22, FIB_NUM2:2; ::_thesis: verum end; end; end; end; end; then (tau_bar to_power m) * (((tau to_power k) * (tau_bar to_power k)) - (tau_bar to_power (k + k))) <= (sqrt 5) / 2 by Lm3, NEWTON:7; then (tau_bar to_power m) * (((tau to_power k) * (tau_bar to_power k)) - ((tau_bar to_power k) * (tau_bar to_power k))) <= (sqrt 5) / 2 by Th2; then (((tau_bar to_power m) * (tau_bar to_power k)) * ((tau to_power k) - (tau_bar to_power k))) / (sqrt 5) <= ((sqrt 5) / 2) / (sqrt 5) by A6, XREAL_1:72; then ((tau_bar to_power m) * (tau_bar to_power k)) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) <= ((sqrt 5) / 2) / (sqrt 5) by XCMPLX_1:74; then ((tau_bar to_power m) * (tau_bar to_power k)) * (Fib k) <= ((sqrt 5) / 2) / (sqrt 5) by FIB_NUM:7; then (tau_bar to_power n) * (Fib k) <= ((sqrt 5) / 2) / (sqrt 5) by A5, Th2; then (tau_bar to_power n) * (Fib k) <= (1 * (sqrt 5)) / (2 * (sqrt 5)) by XCMPLX_1:78; hence (tau_bar to_power n) * (Fib k) <= 1 / 2 by A6, XCMPLX_1:91; ::_thesis: verum end; suppose n is odd ; ::_thesis: (tau_bar to_power n) * (Fib k) <= 1 / 2 then tau_bar to_power n < 0 by Th7; hence (tau_bar to_power n) * (Fib k) <= 1 / 2 ; ::_thesis: verum end; end; end; then - ((tau_bar to_power n) * (Fib k)) >= - (1 / 2) by XREAL_1:24; then (- ((tau_bar to_power n) * (Fib k))) + (1 / 2) >= (- (1 / 2)) + (1 / 2) by XREAL_1:6; then ((- ((tau_bar to_power n) * (Fib k))) + (1 / 2)) + (Fib (n + k)) >= 0 + (Fib (n + k)) by XREAL_1:6; hence ((tau to_power k) * (Fib n)) + (1 / 2) >= Fib (n + k) by A2; ::_thesis: verum end; (((tau to_power k) * (Fib n)) + (1 / 2)) - 1 < Fib (n + k) proof (tau_bar to_power n) * (Fib k) > - (1 / 2) proof percases ( n is even or n is odd ) ; suppose n is even ; ::_thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2) then tau_bar to_power n > 0 by Th6; hence (tau_bar to_power n) * (Fib k) > - (1 / 2) ; ::_thesis: verum end; supposeA25: n is odd ; ::_thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2) consider m being Nat such that A26: n = k + m by A1, NAT_1:10; set tbm = tau_bar to_power m; percases ( k is even or k is odd ) ; supposeA27: k is even ; ::_thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2) then A28: m is odd by A25, A26; then A29: tau_bar to_power m < 0 by Th7; A30: m >= 1 by A28, NAT_1:14; percases ( m = 1 or m > 1 ) by A30, XXREAL_0:1; supposeA31: m = 1 ; ::_thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2) ((3 - (sqrt 5)) / 2) to_power k < 1 to_power k by Lm29, Lm28, A1, POWER:37; then ((3 - (sqrt 5)) / 2) to_power k < 1 by POWER:26; then - (((3 - (sqrt 5)) / 2) to_power k) > - 1 by XREAL_1:24; then A32: (- (((3 - (sqrt 5)) / 2) to_power k)) + 1 > (- 1) + 1 by XREAL_1:6; ((3 - (sqrt 5)) / 2) to_power k > 0 by Lm28, POWER:34; then A33: (- (((3 - (sqrt 5)) / 2) to_power k)) + 1 < 0 + 1 by XREAL_1:6; A34: 1 - (tau_bar to_power (2 * k)) = ((- 1) to_power k) - (tau_bar to_power (2 * k)) by A27, FIB_NUM2:3 .= ((tau to_power k) * (tau_bar to_power k)) - (tau_bar to_power (k + k)) by Lm3, NEWTON:7 .= ((tau to_power k) * (tau_bar to_power k)) - ((tau_bar to_power k) * (tau_bar to_power k)) by Th2 .= (tau_bar to_power k) * ((tau to_power k) - (tau_bar to_power k)) ; (((sqrt 5) - 1) / (sqrt 5)) * (1 - (((3 - (sqrt 5)) / 2) to_power k)) < 1 * 1 by Lm26, Lm27, A32, A33, XREAL_1:98; then - ((((sqrt 5) - 1) / (sqrt 5)) * (1 - (((3 - (sqrt 5)) / 2) to_power k))) > - 1 by XREAL_1:24; then (- (((sqrt 5) - 1) / (sqrt 5))) * (1 - (((3 - (sqrt 5)) / 2) to_power k)) > - 1 ; then ((- ((sqrt 5) - 1)) / (sqrt 5)) * (1 - (((3 - (sqrt 5)) / 2) to_power k)) > - 1 by XCMPLX_1:187; then ((1 - (sqrt 5)) / (sqrt 5)) * (1 - (tau_bar to_power (2 * k))) > - 1 by Lm7, NEWTON:9; then (((1 - (sqrt 5)) / (sqrt 5)) * (1 - (tau_bar to_power (2 * k)))) / 2 > (- 1) / 2 by XREAL_1:74; then ((1 - (sqrt 5)) / (sqrt 5)) * ((1 - (tau_bar to_power (2 * k))) / 2) > (- 1) / 2 ; then ((1 - (sqrt 5)) * (1 / (sqrt 5))) * ((1 - (tau_bar to_power (2 * k))) * (1 / 2)) > (- 1) / 2 by XCMPLX_1:99; then (tau_bar * (1 / (sqrt 5))) * (1 - (tau_bar to_power (2 * k))) > - (1 / 2) by FIB_NUM:def_2; then (tau_bar * (1 / (sqrt 5))) * ((tau_bar to_power k) * ((tau to_power k) - (tau_bar to_power k))) > - (1 / 2) by A34; then (tau_bar * (tau_bar to_power k)) * (((tau to_power k) - (tau_bar to_power k)) * (1 / (sqrt 5))) > - (1 / 2) ; then (tau_bar * (tau_bar to_power k)) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) > - (1 / 2) by XCMPLX_1:99; then ((tau_bar to_power 1) * (tau_bar to_power k)) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) > - (1 / 2) by POWER:25; then (tau_bar to_power (1 + k)) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) > - (1 / 2) by Th2; hence (tau_bar to_power n) * (Fib k) > - (1 / 2) by A31, A26, FIB_NUM:7; ::_thesis: verum end; suppose m > 1 ; ::_thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2) then tau_bar to_power m > - (1 / 2) by Th14; then A35: - (tau_bar to_power m) < - (- (1 / 2)) by XREAL_1:24; sqrt 5 > 1 by SQUARE_1:18, SQUARE_1:27; then - (sqrt 5) < - 1 by XREAL_1:24; then A36: (- (sqrt 5)) / 2 < (- 1) / 2 by XREAL_1:74; ( tau_bar to_power (2 * k) > 0 & tau_bar to_power (2 * k) < 1 / 2 ) by Th6, Th8, A1; then ( - (tau_bar to_power (2 * k)) < 0 & - (tau_bar to_power (2 * k)) > - (1 / 2) ) by XREAL_1:24; then ( (- (tau_bar to_power (2 * k))) + 1 < 0 + 1 & (- (tau_bar to_power (2 * k))) + 1 > (- (1 / 2)) + 1 ) by XREAL_1:6; then (- (tau_bar to_power m)) * (1 - (tau_bar to_power (2 * k))) < (1 / 2) * 1 by A35, A29, XREAL_1:98; then - (- ((tau_bar to_power m) * (1 - (tau_bar to_power (2 * k))))) > - (1 / 2) by XREAL_1:24; then (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) > - (1 / 2) by A27, FIB_NUM2:3; then (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) > - ((sqrt 5) / 2) by A36, XXREAL_0:2; then (tau_bar to_power m) * (((tau to_power k) * (tau_bar to_power k)) - (tau_bar to_power (k + k))) > - ((sqrt 5) / 2) by Lm3, NEWTON:7; then (tau_bar to_power m) * (((tau to_power k) * (tau_bar to_power k)) - ((tau_bar to_power k) * (tau_bar to_power k))) > - ((sqrt 5) / 2) by Th2; then ((tau_bar to_power m) * (tau_bar to_power k)) * ((tau to_power k) - (tau_bar to_power k)) > - ((sqrt 5) / 2) ; then ( (tau_bar to_power n) * ((tau to_power k) - (tau_bar to_power k)) > - ((sqrt 5) / 2) & sqrt 5 > 0 ) by Th2, A26, SQUARE_1:25; then ((tau_bar to_power n) * ((tau to_power k) - (tau_bar to_power k))) / (sqrt 5) > (- ((sqrt 5) / 2)) / (sqrt 5) by XREAL_1:74; then (tau_bar to_power n) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) > (- ((sqrt 5) / 2)) / (sqrt 5) by XCMPLX_1:74; then (tau_bar to_power n) * (Fib k) > ((- (sqrt 5)) / 2) / (sqrt 5) by FIB_NUM:7; then ( (tau_bar to_power n) * (Fib k) > ((- 1) * (sqrt 5)) / (2 * (sqrt 5)) & sqrt 5 > 0 ) by SQUARE_1:25, XCMPLX_1:78; then (tau_bar to_power n) * (Fib k) > (- 1) / 2 by XCMPLX_1:91; hence (tau_bar to_power n) * (Fib k) > - (1 / 2) ; ::_thesis: verum end; end; end; supposeA37: k is odd ; ::_thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2) then A38: m is even by A25, A26; percases ( m = 0 or m > 0 ) ; supposeA39: m = 0 ; ::_thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2) percases ( k = 1 or k > 1 ) by A1; suppose k = 1 ; ::_thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2) hence (tau_bar to_power n) * (Fib k) > - (1 / 2) by A1, A39, A26; ::_thesis: verum end; suppose k > 1 ; ::_thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2) then k >= 1 + 1 by NAT_1:13; then ( k = 2 or k > 2 ) by XXREAL_0:1; then k + 1 > 2 + 1 by A37, POLYFORM:5, XREAL_1:6; then k >= 3 by NAT_1:13; then k * 2 >= 3 * 2 by XREAL_1:64; then tau_bar to_power (k * 2) <= tau_bar to_power (3 * 2) by Th11; then A40: (tau_bar to_power (2 * k)) + 1 <= (9 - (4 * (sqrt 5))) + 1 by Lm9, XREAL_1:6; sqrt ((20 / 9) ^2) < sqrt 5 by SQUARE_1:27; then 20 / 9 < sqrt 5 by SQUARE_1:def_2; then (20 / 9) * 9 < 9 * (sqrt 5) by XREAL_1:68; then 20 - (8 * (sqrt 5)) < ((sqrt 5) + (8 * (sqrt 5))) - (8 * (sqrt 5)) by XREAL_1:9; then (20 - (8 * (sqrt 5))) / 2 < (sqrt 5) / 2 by XREAL_1:74; then (tau_bar to_power (2 * k)) + 1 < (sqrt 5) / 2 by A40, XXREAL_0:2; then - ((tau_bar to_power (2 * k)) + 1) > - ((sqrt 5) / 2) by XREAL_1:24; then (- (tau_bar to_power (2 * k))) + (- 1) > - ((sqrt 5) / 2) ; then (- (tau_bar to_power (2 * k))) + ((- 1) to_power k) > - ((sqrt 5) / 2) by A37, FIB_NUM2:2; then (- (tau_bar to_power (k + k))) + ((tau to_power k) * (tau_bar to_power k)) > - ((sqrt 5) / 2) by Lm3, NEWTON:7; then (- ((tau_bar to_power k) * (tau_bar to_power k))) + ((tau to_power k) * (tau_bar to_power k)) > - ((sqrt 5) / 2) by Th2; then ( (tau_bar to_power k) * ((- (tau_bar to_power k)) + (tau to_power k)) > - ((sqrt 5) / 2) & sqrt 5 > 0 ) by SQUARE_1:25; then ((tau_bar to_power k) * ((- (tau_bar to_power k)) + (tau to_power k))) / (sqrt 5) > (- ((sqrt 5) / 2)) / (sqrt 5) by XREAL_1:74; then (tau_bar to_power k) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) > (- ((sqrt 5) / 2)) / (sqrt 5) by XCMPLX_1:74; then (tau_bar to_power k) * (Fib k) > (- ((sqrt 5) / 2)) / (sqrt 5) by FIB_NUM:7; then (tau_bar to_power k) * (Fib k) > - (((sqrt 5) / 2) / (sqrt 5)) by XCMPLX_1:187; then ( (tau_bar to_power k) * (Fib k) > - (((sqrt 5) / (sqrt 5)) / 2) & sqrt 5 > 0 ) by SQUARE_1:25, XCMPLX_1:48; hence (tau_bar to_power n) * (Fib k) > - (1 / 2) by A39, A26, XCMPLX_1:60; ::_thesis: verum end; end; end; suppose m > 0 ; ::_thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2) then A41: ( tau_bar to_power m > 0 & tau_bar to_power m < 1 / 2 ) by A38, Th6, Th8; sqrt ((3 / 2) ^2) < sqrt 5 by SQUARE_1:27; then 3 / 2 < sqrt 5 by SQUARE_1:def_2; then (3 / 2) * 2 < (sqrt 5) * 2 by XREAL_1:68; then A42: 3 / (2 * 2) < (2 * (sqrt 5)) / (2 * 2) by XREAL_1:74; A43: ( tau_bar to_power (2 * k) < 1 / 2 & tau_bar to_power (2 * k) > 0 ) by Th8, A1, Th6; then (tau_bar to_power (2 * k)) + 1 < (1 / 2) + 1 by XREAL_1:6; then (tau_bar to_power m) * ((tau_bar to_power (2 * k)) + 1) < (1 / 2) * ((1 / 2) + 1) by A41, A43, XREAL_1:96; then (tau_bar to_power m) * ((tau_bar to_power (2 * k)) + 1) < (sqrt 5) / 2 by A42, XXREAL_0:2; then - ((tau_bar to_power m) * ((tau_bar to_power (2 * k)) + 1)) > - ((sqrt 5) / 2) by XREAL_1:24; then (tau_bar to_power m) * ((- (tau_bar to_power (2 * k))) + (- 1)) > - ((sqrt 5) / 2) ; then (tau_bar to_power m) * ((- (tau_bar to_power (2 * k))) + ((- 1) to_power k)) > - ((sqrt 5) / 2) by A37, FIB_NUM2:2; then (tau_bar to_power m) * ((- (tau_bar to_power (k + k))) + ((tau to_power k) * (tau_bar to_power k))) > - ((sqrt 5) / 2) by Lm3, NEWTON:7; then (tau_bar to_power m) * ((- ((tau_bar to_power k) * (tau_bar to_power k))) + ((tau to_power k) * (tau_bar to_power k))) > - ((sqrt 5) / 2) by Th2; then ((tau_bar to_power m) * (tau_bar to_power k)) * ((tau to_power k) - (tau_bar to_power k)) > - ((sqrt 5) / 2) ; then ( (tau_bar to_power n) * ((tau to_power k) - (tau_bar to_power k)) > - ((sqrt 5) / 2) & sqrt 5 > 0 ) by A26, Th2, SQUARE_1:25; then ((tau_bar to_power n) * ((tau to_power k) - (tau_bar to_power k))) / (sqrt 5) > (- ((sqrt 5) / 2)) / (sqrt 5) by XREAL_1:74; then (tau_bar to_power n) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) > (- ((sqrt 5) / 2)) / (sqrt 5) by XCMPLX_1:74; then (tau_bar to_power n) * (Fib k) > ((- (sqrt 5)) / 2) / (sqrt 5) by FIB_NUM:7; then ( (tau_bar to_power n) * (Fib k) > ((- 1) * (sqrt 5)) / (2 * (sqrt 5)) & sqrt 5 > 0 ) by SQUARE_1:25, XCMPLX_1:78; then (tau_bar to_power n) * (Fib k) > (- 1) / 2 by XCMPLX_1:91; hence (tau_bar to_power n) * (Fib k) > - (1 / 2) ; ::_thesis: verum end; end; end; end; end; end; end; then - ((tau_bar to_power n) * (Fib k)) < - (- (1 / 2)) by XREAL_1:24; then (- ((tau_bar to_power n) * (Fib k))) + (1 / 2) < (1 / 2) + (1 / 2) by XREAL_1:6; then ((- ((tau_bar to_power n) * (Fib k))) + (1 / 2)) - 1 < 1 - 1 by XREAL_1:9; then (((- ((tau_bar to_power n) * (Fib k))) + (1 / 2)) - 1) + (Fib (n + k)) < 0 + (Fib (n + k)) by XREAL_1:6; hence (((tau to_power k) * (Fib n)) + (1 / 2)) - 1 < Fib (n + k) by A2; ::_thesis: verum end; hence [\(((tau to_power k) * (Fib n)) + (1 / 2))/] = Fib (n + k) by A3, INT_1:def_6; ::_thesis: verum end; begin theorem :: FIB_NUM4:30 for n being Nat st n >= 2 holds Lucas n = [\((tau to_power n) + (1 / 2))/] proof let n be Nat; ::_thesis: ( n >= 2 implies Lucas n = [\((tau to_power n) + (1 / 2))/] ) assume A1: n >= 2 ; ::_thesis: Lucas n = [\((tau to_power n) + (1 / 2))/] then 1 / 2 >= tau_bar to_power n by Th8; then (tau to_power n) + (1 / 2) >= (tau to_power n) + (tau_bar to_power n) by XREAL_1:6; then A2: (tau to_power n) + (1 / 2) >= Lucas n by FIB_NUM3:21; n > 1 by A1, XXREAL_0:2; then (1 / 2) - 1 < tau_bar to_power n by Th14; then (tau to_power n) + ((1 / 2) - 1) < (tau to_power n) + (tau_bar to_power n) by XREAL_1:6; then ((tau to_power n) + (1 / 2)) - 1 < Lucas n by FIB_NUM3:21; hence Lucas n = [\((tau to_power n) + (1 / 2))/] by A2, INT_1:def_6; ::_thesis: verum end; theorem :: FIB_NUM4:31 for n being Nat st n >= 2 holds Lucas n = [/((tau to_power n) - (1 / 2))\] proof let n be Nat; ::_thesis: ( n >= 2 implies Lucas n = [/((tau to_power n) - (1 / 2))\] ) assume A1: n >= 2 ; ::_thesis: Lucas n = [/((tau to_power n) - (1 / 2))\] then n > 1 by XXREAL_0:2; then - (1 / 2) <= tau_bar to_power n by Th14; then (- (1 / 2)) + (tau to_power n) <= (tau_bar to_power n) + (tau to_power n) by XREAL_1:6; then A2: (tau to_power n) - (1 / 2) <= Lucas n by FIB_NUM3:21; tau_bar to_power n < 1 / 2 by Th8, A1; then (tau_bar to_power n) + (tau to_power n) < (1 / 2) + (tau to_power n) by XREAL_1:6; then ((tau to_power n) - (1 / 2)) + 1 > Lucas n by FIB_NUM3:21; hence Lucas n = [/((tau to_power n) - (1 / 2))\] by A2, INT_1:def_7; ::_thesis: verum end; theorem :: FIB_NUM4:32 for n being Nat st n >= 2 holds Lucas (2 * n) = [/(tau to_power (2 * n))\] proof let n be Nat; ::_thesis: ( n >= 2 implies Lucas (2 * n) = [/(tau to_power (2 * n))\] ) assume A1: n >= 2 ; ::_thesis: Lucas (2 * n) = [/(tau to_power (2 * n))\] A2: tau_bar to_power (2 * n) = (tau_bar to_power n) to_power 2 by NEWTON:9 .= (tau_bar to_power n) ^2 by POWER:46 ; n - 0 is Element of NAT by NAT_1:21; then tau_bar to_power n <> 0 by FIB_NUM3:1; then tau_bar to_power (2 * n) > 0 by A2, SQUARE_1:12; then 0 + (tau to_power (2 * n)) <= (tau to_power (2 * n)) + (tau_bar to_power (2 * n)) by XREAL_1:6; then A3: tau to_power (2 * n) <= Lucas (2 * n) by FIB_NUM3:21; tau_bar to_power (2 * n) < 1 by Th8, A1, XXREAL_0:2; then (tau_bar to_power (2 * n)) + (tau to_power (2 * n)) < 1 + (tau to_power (2 * n)) by XREAL_1:6; then (tau to_power (2 * n)) + 1 > Lucas (2 * n) by FIB_NUM3:21; hence Lucas (2 * n) = [/(tau to_power (2 * n))\] by A3, INT_1:def_7; ::_thesis: verum end; theorem :: FIB_NUM4:33 for n being Nat st n >= 2 holds Lucas ((2 * n) + 1) = [\(tau to_power ((2 * n) + 1))/] proof let n be Nat; ::_thesis: ( n >= 2 implies Lucas ((2 * n) + 1) = [\(tau to_power ((2 * n) + 1))/] ) assume n >= 2 ; ::_thesis: Lucas ((2 * n) + 1) = [\(tau to_power ((2 * n) + 1))/] then 2 * n >= 2 * 2 by XREAL_1:64; then (2 * n) + 1 >= 4 + 1 by XREAL_1:6; then A1: (2 * n) + 1 > 1 by XXREAL_0:2; tau_bar to_power ((2 * n) + 1) <= 0 by Th7; then (tau to_power ((2 * n) + 1)) + 0 >= (tau to_power ((2 * n) + 1)) + (tau_bar to_power ((2 * n) + 1)) by XREAL_1:6; then A2: tau to_power ((2 * n) + 1) >= Lucas ((2 * n) + 1) by FIB_NUM3:21; - (1 / 2) <= tau_bar to_power ((2 * n) + 1) by Th14, A1; then tau_bar to_power ((2 * n) + 1) > - 1 by XXREAL_0:2; then (- 1) + (tau to_power ((2 * n) + 1)) < (tau to_power ((2 * n) + 1)) + (tau_bar to_power ((2 * n) + 1)) by XREAL_1:6; then (tau to_power ((2 * n) + 1)) - 1 < Lucas ((2 * n) + 1) by FIB_NUM3:21; hence Lucas ((2 * n) + 1) = [\(tau to_power ((2 * n) + 1))/] by A2, INT_1:def_6; ::_thesis: verum end; theorem :: FIB_NUM4:34 for n being Nat st n >= 2 & n is odd holds Lucas (n + 1) = [\((tau * (Lucas n)) + 1)/] proof let n be Nat; ::_thesis: ( n >= 2 & n is odd implies Lucas (n + 1) = [\((tau * (Lucas n)) + 1)/] ) set tn = tau_bar to_power n; assume A1: ( n >= 2 & n is odd ) ; ::_thesis: Lucas (n + 1) = [\((tau * (Lucas n)) + 1)/] A2: (tau * (Lucas n)) + 1 >= Lucas (n + 1) proof percases ( n = 2 or n > 2 ) by A1, XXREAL_0:1; supposeA3: n = 2 ; ::_thesis: (tau * (Lucas n)) + 1 >= Lucas (n + 1) sqrt 5 >= 1 by SQUARE_1:18, SQUARE_1:26; then (sqrt 5) * 3 >= 1 * 3 by XREAL_1:64; then 5 + ((sqrt 5) * 3) >= 3 + 5 by XREAL_1:6; then (5 + ((sqrt 5) * 3)) / 2 >= 8 / 2 by XREAL_1:72; hence (tau * (Lucas n)) + 1 >= Lucas (n + 1) by A3, FIB_NUM:def_1, FIB_NUM3:14, FIB_NUM3:15; ::_thesis: verum end; supposeA4: n > 2 ; ::_thesis: (tau * (Lucas n)) + 1 >= Lucas (n + 1) A5: sqrt 5 > 0 by SQUARE_1:25; ( tau_bar to_power n >= - (1 / (sqrt 5)) & sqrt 5 > 0 ) by Th15, A4, SQUARE_1:25; then (tau_bar to_power n) * (sqrt 5) >= (- (1 / (sqrt 5))) * (sqrt 5) by XREAL_1:64; then (tau_bar to_power n) * (sqrt 5) >= (sqrt 5) * ((- 1) / (sqrt 5)) by XCMPLX_1:187; then (tau_bar to_power n) * (sqrt 5) >= ((sqrt 5) * (- 1)) / (sqrt 5) by XCMPLX_1:74; then (tau_bar to_power n) * (sqrt 5) >= ((sqrt 5) / (sqrt 5)) * (- 1) by XCMPLX_1:74; then (tau_bar to_power n) * (sqrt 5) >= 1 * (- 1) by A5, XCMPLX_1:60; then - ((tau_bar to_power n) * (sqrt 5)) <= - (- 1) by XREAL_1:24; then ((tau_bar to_power n) * tau_bar) - ((tau_bar to_power n) * tau) <= 1 by FIB_NUM:def_1, FIB_NUM:def_2; then ((tau_bar to_power n) * (tau_bar to_power 1)) - ((tau_bar to_power n) * tau) <= 1 by POWER:25; then (tau_bar to_power (n + 1)) - ((tau_bar to_power n) * tau) <= 1 by Th2; then ((tau_bar to_power (n + 1)) - ((tau_bar to_power n) * tau)) + ((tau_bar to_power n) * tau) <= 1 + ((tau_bar to_power n) * tau) by XREAL_1:6; then (((tau_bar to_power n) * tau) + 1) + (tau to_power (n + 1)) >= (tau_bar to_power (n + 1)) + (tau to_power (n + 1)) by XREAL_1:6; then (((tau_bar to_power n) * tau) + 1) + ((tau to_power n) * (tau to_power 1)) >= (tau_bar to_power (n + 1)) + (tau to_power (n + 1)) by Th2; then (((tau_bar to_power n) * tau) + 1) + ((tau to_power n) * tau) >= (tau_bar to_power (n + 1)) + (tau to_power (n + 1)) by POWER:25; then (((tau_bar to_power n) + (tau to_power n)) * tau) + 1 >= (tau_bar to_power (n + 1)) + (tau to_power (n + 1)) ; then ((Lucas n) * tau) + 1 >= (tau_bar to_power (n + 1)) + (tau to_power (n + 1)) by FIB_NUM3:21; hence (tau * (Lucas n)) + 1 >= Lucas (n + 1) by FIB_NUM3:21; ::_thesis: verum end; end; end; ((tau * (Lucas n)) + 1) - 1 < Lucas (n + 1) proof A6: Lucas (n + 1) = (tau to_power (n + 1)) + (tau_bar to_power (n + 1)) by FIB_NUM3:21; A7: tau * (Lucas n) = tau * ((tau to_power n) + (tau_bar to_power n)) by FIB_NUM3:21 .= (tau * (tau to_power n)) + (tau * (tau_bar to_power n)) .= ((tau to_power 1) * (tau to_power n)) + (tau * (tau_bar to_power n)) by POWER:25 .= (tau to_power (n + 1)) + (tau * (tau_bar to_power n)) by Th2 ; tau_bar to_power n < 0 by Th7, A1; then tau * (tau_bar to_power n) < tau_bar * (tau_bar to_power n) by XREAL_1:69; then tau * (tau_bar to_power n) < (tau_bar to_power 1) * (tau_bar to_power n) by POWER:25; then tau * (tau_bar to_power n) < tau_bar to_power (n + 1) by Th2; hence ((tau * (Lucas n)) + 1) - 1 < Lucas (n + 1) by A6, A7, XREAL_1:6; ::_thesis: verum end; hence Lucas (n + 1) = [\((tau * (Lucas n)) + 1)/] by A2, INT_1:def_6; ::_thesis: verum end; theorem :: FIB_NUM4:35 for n being Nat st n >= 2 & n is even holds Lucas (n + 1) = [/((tau * (Lucas n)) - 1)\] proof let n be Nat; ::_thesis: ( n >= 2 & n is even implies Lucas (n + 1) = [/((tau * (Lucas n)) - 1)\] ) set tn = tau_bar to_power n; assume A1: ( n >= 2 & n is even ) ; ::_thesis: Lucas (n + 1) = [/((tau * (Lucas n)) - 1)\] A2: Lucas (n + 1) = (tau to_power (n + 1)) + (tau_bar to_power (n + 1)) by FIB_NUM3:21; A3: tau * (Lucas n) = tau * ((tau to_power n) + (tau_bar to_power n)) by FIB_NUM3:21 .= (tau * (tau to_power n)) + (tau * (tau_bar to_power n)) .= ((tau to_power 1) * (tau to_power n)) + (tau * (tau_bar to_power n)) by POWER:25 .= (tau to_power (n + 1)) + (tau * (tau_bar to_power n)) by Th2 ; A4: (tau * (Lucas n)) - 1 <= Lucas (n + 1) proof (tau * (tau_bar to_power n)) - 1 <= tau_bar to_power (n + 1) proof A5: tau_bar to_power n > 0 by Th6, A1; tau_bar to_power n <= 1 / (sqrt 5) by Th16, A1; then 1 / (tau_bar to_power n) >= 1 / (1 / (sqrt 5)) by Th6, A1, XREAL_1:118; then 1 / (tau_bar to_power n) >= sqrt 5 by XCMPLX_1:52; then (1 / (tau_bar to_power n)) * 2 >= (sqrt 5) * 2 by XREAL_1:64; then ((1 / (tau_bar to_power n)) * 2) + 1 >= (2 * (sqrt 5)) + 1 by XREAL_1:6; then (((1 / (tau_bar to_power n)) * 2) + 1) - (sqrt 5) >= ((2 * (sqrt 5)) + 1) - (sqrt 5) by XREAL_1:13; then (((1 / (tau_bar to_power n)) * 2) + (1 - (sqrt 5))) / 2 >= ((sqrt 5) + 1) / 2 by XREAL_1:72; then ((1 / (tau_bar to_power n)) + tau_bar) * (tau_bar to_power n) >= tau * (tau_bar to_power n) by A5, FIB_NUM:def_1, FIB_NUM:def_2, XREAL_1:64; then ((1 / (tau_bar to_power n)) * (tau_bar to_power n)) + (tau_bar * (tau_bar to_power n)) >= tau * (tau_bar to_power n) ; then ((1 / (tau_bar to_power n)) * (tau_bar to_power n)) + ((tau_bar to_power 1) * (tau_bar to_power n)) >= tau * (tau_bar to_power n) by POWER:25; then 1 + ((tau_bar to_power 1) * (tau_bar to_power n)) >= tau * (tau_bar to_power n) by A5, XCMPLX_1:87; then 1 + (tau_bar to_power (n + 1)) >= tau * (tau_bar to_power n) by Th2; then (1 + (tau_bar to_power (n + 1))) - 1 >= (tau * (tau_bar to_power n)) - 1 by XREAL_1:9; hence (tau * (tau_bar to_power n)) - 1 <= tau_bar to_power (n + 1) ; ::_thesis: verum end; then (tau to_power (n + 1)) + ((tau * (tau_bar to_power n)) - 1) <= (tau to_power (n + 1)) + (tau_bar to_power (n + 1)) by XREAL_1:6; hence (tau * (Lucas n)) - 1 <= Lucas (n + 1) by A3, FIB_NUM3:21; ::_thesis: verum end; ((tau * (Lucas n)) - 1) + 1 > Lucas (n + 1) proof tau_bar to_power n = (- tau_bar) to_power n by A1, Th3; then tau_bar to_power n > 0 by POWER:34; then tau * (tau_bar to_power n) > tau_bar * (tau_bar to_power n) by XREAL_1:68; then tau * (tau_bar to_power n) > (tau_bar to_power 1) * (tau_bar to_power n) by POWER:25; then tau * (tau_bar to_power n) > tau_bar to_power (n + 1) by Th2; hence ((tau * (Lucas n)) - 1) + 1 > Lucas (n + 1) by A2, A3, XREAL_1:6; ::_thesis: verum end; hence Lucas (n + 1) = [/((tau * (Lucas n)) - 1)\] by A4, INT_1:def_7; ::_thesis: verum 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 proof let n be Nat; ::_thesis: ( n <> 1 implies Lucas (n + 1) = ((Lucas n) + (sqrt (5 * (((Lucas n) ^2) - (4 * ((- 1) to_power n)))))) / 2 ) assume A1: n <> 1 ; ::_thesis: Lucas (n + 1) = ((Lucas n) + (sqrt (5 * (((Lucas n) ^2) - (4 * ((- 1) to_power n)))))) / 2 A2: ((Lucas n) ^2) - (((- 1) to_power n) * 4) >= 0 proof percases ( n = 0 or n > 1 ) by A1, NAT_1:25; suppose n = 0 ; ::_thesis: ((Lucas n) ^2) - (((- 1) to_power n) * 4) >= 0 then ((Lucas n) ^2) - (((- 1) to_power n) * 4) = (2 * 2) - (1 * 4) by FIB_NUM3:11, POWER:24; hence ((Lucas n) ^2) - (((- 1) to_power n) * 4) >= 0 ; ::_thesis: verum end; suppose n > 1 ; ::_thesis: ((Lucas n) ^2) - (((- 1) to_power n) * 4) >= 0 then n + 1 > 1 + 1 by XREAL_1:8; then ( n >= 2 & Lucas n >= n ) by FIB_NUM3:17, NAT_1:13; then Lucas n >= 2 by XXREAL_0:2; then (Lucas n) ^2 >= 2 ^2 by SQUARE_1:15; then ( (Lucas n) ^2 >= 2 * 2 & - (4 * ((- 1) to_power n)) >= - 4 ) by Lm2; then ((Lucas n) ^2) + (- (4 * ((- 1) to_power n))) >= (2 * 2) + (- 4) by XREAL_1:7; hence ((Lucas n) ^2) - (((- 1) to_power n) * 4) >= 0 ; ::_thesis: verum end; end; end; A3: n - 0 is Element of NAT by NAT_1:21; then 2 * (Lucas (n + 1)) = ((Lucas n) * 1) + ((5 * (Fib n)) * 1) by FIB_NUM3:11, FIB_NUM3:26, PRE_FF:1; then A4: Lucas (n + 1) = ((5 * (Fib n)) + (Lucas n)) / 2 ; ((Lucas n) ^2) - (5 * ((Fib n) ^2)) = ((Lucas n) to_power 2) - (5 * ((Fib n) ^2)) by POWER:46 .= ((Lucas n) to_power 2) - (5 * ((Fib n) to_power 2)) by POWER:46 .= - ((5 * ((Fib n) |^ 2)) - ((Lucas n) |^ 2)) .= - (4 * ((- 1) to_power (n + 1))) by A3, FIB_NUM3:30 .= (- 1) * (((- 1) to_power (n + 1)) * 4) .= ((- 1) to_power 1) * (((- 1) to_power (n + 1)) * 4) by POWER:25 .= (((- 1) to_power 1) * ((- 1) to_power (n + 1))) * 4 .= ((- 1) to_power ((n + 1) + 1)) * 4 by Th2 .= ((- 1) to_power (n + 2)) * 4 .= (((- 1) to_power n) * ((- 1) to_power 2)) * 4 by Th2 .= (((- 1) to_power n) * 1) * 4 by FIB_NUM2:3, POLYFORM:5 ; then Fib n = sqrt ((((Lucas n) ^2) - (((- 1) to_power n) * 4)) / 5) by SQUARE_1:def_2; then Lucas (n + 1) = ((5 * ((sqrt (((Lucas n) ^2) - (((- 1) to_power n) * 4))) / (sqrt 5))) + (Lucas n)) / 2 by A2, A4, SQUARE_1:30 .= ((((sqrt (((Lucas n) ^2) - (((- 1) to_power n) * 4))) * 5) / (sqrt 5)) + (Lucas n)) / 2 by XCMPLX_1:74 .= (((sqrt (((Lucas n) ^2) - (((- 1) to_power n) * 4))) * (5 / (sqrt 5))) + (Lucas n)) / 2 by XCMPLX_1:74 .= (((sqrt (((Lucas n) ^2) - (((- 1) to_power n) * 4))) * (sqrt 5)) + (Lucas n)) / 2 by SQUARE_1:34 .= ((sqrt ((((Lucas n) ^2) - (((- 1) to_power n) * 4)) * 5)) + (Lucas n)) / 2 by A2, SQUARE_1:29 ; hence Lucas (n + 1) = ((Lucas n) + (sqrt (5 * (((Lucas n) ^2) - (4 * ((- 1) to_power n)))))) / 2 ; ::_thesis: verum 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)/] proof let n be Nat; ::_thesis: ( 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 ; ::_thesis: 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 empty 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 by POWER:25 .= ((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 by POWER:25 .= (((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 percases ( n = 4 or n > 4 ) by A1, XXREAL_0:1; suppose n = 4 ; ::_thesis: (5 * ((Lucas n) ^2)) - (2 * (Lucas n)) >= (25 * ((Fib n) ^2)) - (10 * (Fib n)) hence (5 * ((Lucas n) ^2)) - (2 * (Lucas n)) >= (25 * ((Fib n) ^2)) - (10 * (Fib n)) by FIB_NUM2:23, FIB_NUM3:16; ::_thesis: verum end; suppose n > 4 ; ::_thesis: (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; ::_thesis: verum end; 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) ; ::_thesis: 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 proof 5 * (Lucas n) >= 5 * 4 by A12, XREAL_1:66; then (5 * (Lucas n)) - 2 >= 20 - 2 by XREAL_1:9; then (Lucas n) * ((5 * (Lucas n)) - 2) >= 4 * 18 by A12, XREAL_1:66; then ((Lucas n) * ((5 * (Lucas n)) - 2)) + 1 >= (4 * 18) + 1 by XREAL_1:6; hence ((5 * ((Lucas n) ^2)) + 1) - (2 * (Lucas n)) >= 0 ; ::_thesis: verum end; 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 proof ((((2 * (tau to_power (n + 1))) - (tau to_power n)) + (2 * (tau_bar to_power (n + 1)))) - (tau_bar to_power n)) + 1 = ((((2 * ((tau to_power n) * (tau to_power 1))) - (tau to_power n)) + (2 * (tau_bar to_power (n + 1)))) - (tau_bar to_power n)) + 1 by Th2 .= ((((2 * ((tau to_power n) * (tau to_power 1))) - (tau to_power n)) + (2 * ((tau_bar to_power n) * (tau_bar to_power 1)))) - (tau_bar to_power n)) + 1 by Th2 .= ((((2 * ((tau to_power n) * tau)) - (tau to_power n)) + (2 * ((tau_bar to_power n) * (tau_bar to_power 1)))) - (tau_bar to_power n)) + 1 by POWER:25 .= ((((tau to_power n) * (sqrt 5)) + (2 * ((tau_bar to_power n) * tau_bar))) - (tau_bar to_power n)) + 1 by FIB_NUM:def_1, POWER:25 .= (((sqrt 5) * ((tau to_power n) - (tau_bar to_power n))) * 1) + 1 by FIB_NUM:def_2 .= (((sqrt 5) * ((tau to_power n) - (tau_bar to_power n))) * ((sqrt 5) / (sqrt 5))) + 1 by A2, XCMPLX_1:60 .= (((sqrt 5) * ((tau to_power n) - (tau_bar to_power n))) * ((sqrt 5) * (1 / (sqrt 5)))) + 1 by XCMPLX_1:99 .= (((sqrt 5) * (((tau to_power n) - (tau_bar to_power n)) * (1 / (sqrt 5)))) * (sqrt 5)) + 1 .= (((sqrt 5) * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) * (sqrt 5)) + 1 by XCMPLX_1:99 .= (((sqrt 5) * (Fib n)) * (sqrt 5)) + 1 by FIB_NUM:7 .= (((sqrt 5) ^2) * (Fib n)) + 1 .= (5 * (Fib n)) + 1 by SQUARE_1:def_2 ; hence ((((2 * (tau to_power (n + 1))) - (tau to_power n)) + (2 * (tau_bar to_power (n + 1)))) - (tau_bar to_power n)) + 1 > 0 ; ::_thesis: verum end; ((((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 by POWER:25 .= (((((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 by POWER:25 .= (((((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) ; ::_thesis: 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; ::_thesis: verum end; theorem :: FIB_NUM4:38 for n being Nat st n > 2 holds Lucas n = [\((1 / tau) * ((Lucas (n + 1)) + (1 / 2)))/] proof let n be Nat; ::_thesis: ( n > 2 implies Lucas n = [\((1 / tau) * ((Lucas (n + 1)) + (1 / 2)))/] ) assume A1: n > 2 ; ::_thesis: Lucas n = [\((1 / tau) * ((Lucas (n + 1)) + (1 / 2)))/] then A2: n > 1 by XXREAL_0:2; A3: sqrt 5 > 0 by SQUARE_1:25; set tbn = tau_bar to_power n; A4: (1 / tau) * ((Lucas (n + 1)) + (1 / 2)) >= Lucas n proof tau_bar to_power n <= 1 / (2 * (sqrt 5)) proof percases ( n is even or n is odd ) ; supposeA5: n is even ; ::_thesis: tau_bar to_power n <= 1 / (2 * (sqrt 5)) n >= 2 + 1 by A1, NAT_1:13; then ( n = 3 or n > 3 ) by XXREAL_0:1; then ( n = 3 or n >= 3 + 1 ) by NAT_1:8; then A6: tau_bar to_power n <= tau_bar to_power 4 by Th11, A5, POLYFORM:6; A7: tau_bar to_power (3 + 1) = (tau_bar to_power 3) * (tau_bar to_power 1) by Th2 .= (2 - (sqrt 5)) * tau_bar by Lm8, POWER:25 .= (((2 - (2 * (sqrt 5))) - (sqrt 5)) + ((sqrt 5) ^2)) / 2 by FIB_NUM:def_2 .= ((2 - (3 * (sqrt 5))) + 5) / 2 by SQUARE_1:def_2 .= (7 - (3 * (sqrt 5))) / 2 ; sqrt 5 <= sqrt ((16 / 7) ^2) by SQUARE_1:26; then sqrt 5 <= 16 / 7 by SQUARE_1:def_2; then 7 * (sqrt 5) <= (16 / 7) * 7 by XREAL_1:64; then (7 * (sqrt 5)) - (3 * 5) <= 16 - (3 * 5) by XREAL_1:9; then (7 * (sqrt 5)) - (3 * ((sqrt 5) ^2)) <= 1 by SQUARE_1:def_2; then ((7 - (3 * (sqrt 5))) * (sqrt 5)) / (sqrt 5) <= 1 / (sqrt 5) by A3, XREAL_1:72; then 7 - (3 * (sqrt 5)) <= 1 / (sqrt 5) by A3, XCMPLX_1:89; then (7 - (3 * (sqrt 5))) / 2 <= (1 / (sqrt 5)) / 2 by XREAL_1:72; then tau_bar to_power 4 <= 1 / (2 * (sqrt 5)) by A7, XCMPLX_1:78; hence tau_bar to_power n <= 1 / (2 * (sqrt 5)) by A6, XXREAL_0:2; ::_thesis: verum end; suppose n is odd ; ::_thesis: tau_bar to_power n <= 1 / (2 * (sqrt 5)) then tau_bar to_power n < 0 by Th7; hence tau_bar to_power n <= 1 / (2 * (sqrt 5)) by A3; ::_thesis: verum end; end; end; then (tau_bar to_power n) * (sqrt 5) <= (1 / (2 * (sqrt 5))) * (sqrt 5) by A3, XREAL_1:64; then (tau_bar to_power n) * (sqrt 5) <= 1 / 2 by A3, XCMPLX_1:92; then - ((tau_bar to_power n) * (sqrt 5)) >= - (1 / 2) by XREAL_1:24; then ((tau_bar * (tau_bar to_power n)) - (tau * (tau_bar to_power n))) + ((1 / 2) + (tau * (tau_bar to_power n))) >= (- (1 / 2)) + ((1 / 2) + (tau * (tau_bar to_power n))) by FIB_NUM:def_1, FIB_NUM:def_2, XREAL_1:6; then ((tau_bar * (tau_bar to_power n)) + (1 / 2)) / tau >= ((tau_bar to_power n) * tau) / tau by XREAL_1:72; then ((tau_bar * (tau_bar to_power n)) + (1 / 2)) / tau >= tau_bar to_power n by XCMPLX_1:89; then (((tau_bar * (tau_bar to_power n)) + (1 / 2)) / tau) + ((tau to_power (n + 1)) / tau) >= (tau_bar to_power n) + ((tau to_power (n + 1)) / tau) by XREAL_1:6; then (((tau_bar * (tau_bar to_power n)) + (1 / 2)) + (tau to_power (n + 1))) / tau >= (tau_bar to_power n) + ((tau to_power (n + 1)) / tau) by XCMPLX_1:62; then ((((tau_bar to_power 1) * (tau_bar to_power n)) + (1 / 2)) + (tau to_power (n + 1))) / tau >= (tau_bar to_power n) + ((tau to_power (n + 1)) / tau) by POWER:25; then ((((tau_bar to_power 1) * (tau_bar to_power n)) + (tau to_power (n + 1))) + (1 / 2)) / tau >= (tau_bar to_power n) + (((tau to_power n) * (tau to_power 1)) / tau) by Th2; then (((tau_bar to_power (1 + n)) + (tau to_power (n + 1))) + (1 / 2)) / tau >= (tau_bar to_power n) + (((tau to_power n) * (tau to_power 1)) / tau) by Th2; then ((Lucas (n + 1)) + (1 / 2)) / tau >= (tau_bar to_power n) + (((tau to_power n) * (tau to_power 1)) / tau) by FIB_NUM3:21; then ((Lucas (n + 1)) + (1 / 2)) / tau >= (tau_bar to_power n) + (((tau to_power n) * tau) / tau) by POWER:25; then ((Lucas (n + 1)) + (1 / 2)) / tau >= (tau_bar to_power n) + (tau to_power n) by XCMPLX_1:89; then ((Lucas (n + 1)) + (1 / 2)) / tau >= Lucas n by FIB_NUM3:21; hence (1 / tau) * ((Lucas (n + 1)) + (1 / 2)) >= Lucas n by XCMPLX_1:99; ::_thesis: verum end; ((1 / tau) * ((Lucas (n + 1)) + (1 / 2))) - 1 < Lucas n proof tau_bar to_power n > - (1 / 2) by Th14, A2; then - (tau_bar to_power n) < - (- (1 / 2)) by XREAL_1:24; then (- (tau_bar to_power n)) * (sqrt 5) < (1 / 2) * (sqrt 5) by A3, XREAL_1:68; then (((tau_bar to_power n) * tau_bar) - ((tau_bar to_power n) * tau)) + (((tau_bar to_power n) * tau) + (1 / 2)) < (tau - (1 / 2)) + (((tau_bar to_power n) * tau) + (1 / 2)) by FIB_NUM:def_1, FIB_NUM:def_2, XREAL_1:6; then (((tau_bar to_power n) * tau_bar) + (1 / 2)) - tau < (((tau - (1 / 2)) + ((tau_bar to_power n) * tau)) + (1 / 2)) - tau by XREAL_1:9; then ((((tau_bar to_power n) * tau_bar) + (1 / 2)) - tau) / tau < ((tau_bar to_power n) * tau) / tau by XREAL_1:74; then ((((tau_bar to_power n) * tau_bar) / tau) + ((1 / 2) / tau)) - (tau / tau) < ((tau_bar to_power n) * tau) / tau by XCMPLX_1:124; then ((((tau_bar to_power n) * tau_bar) / tau) + ((1 / 2) / tau)) - (tau / tau) < tau_bar to_power n by XCMPLX_1:89; then ((((tau_bar to_power n) * tau_bar) / tau) + ((1 / 2) / tau)) - 1 < tau_bar to_power n by XCMPLX_1:60; then (((((tau_bar to_power n) * tau_bar) / tau) + ((1 / 2) / tau)) - 1) + (tau to_power n) < (tau_bar to_power n) + (tau to_power n) by XREAL_1:6; then (((((tau_bar to_power n) * tau_bar) / tau) + ((1 / 2) / tau)) + ((tau to_power n) * 1)) - 1 < Lucas n by FIB_NUM3:21; then (((((tau_bar to_power n) * tau_bar) / tau) + ((1 / 2) / tau)) + ((tau to_power n) * (tau / tau))) - 1 < Lucas n by XCMPLX_1:60; then (((((tau_bar to_power n) * tau_bar) / tau) + ((1 / 2) / tau)) + (((tau to_power n) * tau) / tau)) - 1 < Lucas n by XCMPLX_1:74; then (((((tau_bar to_power n) * tau_bar) + (1 / 2)) + ((tau to_power n) * tau)) / tau) - 1 < Lucas n by XCMPLX_1:63; then (((((tau_bar to_power n) * (tau_bar to_power 1)) + (1 / 2)) + ((tau to_power n) * tau)) / tau) - 1 < Lucas n by POWER:25; then (((((tau_bar to_power n) * (tau_bar to_power 1)) + (1 / 2)) + ((tau to_power n) * (tau to_power 1))) / tau) - 1 < Lucas n by POWER:25; then ((((tau_bar to_power (n + 1)) + (1 / 2)) + ((tau to_power n) * (tau to_power 1))) / tau) - 1 < Lucas n by Th2; then ((((tau_bar to_power (n + 1)) + (1 / 2)) + (tau to_power (n + 1))) / tau) - 1 < Lucas n by Th2; then ((((tau_bar to_power (n + 1)) + (tau to_power (n + 1))) + (1 / 2)) / tau) - 1 < Lucas n ; then (((Lucas (n + 1)) + (1 / 2)) / tau) - 1 < Lucas n by FIB_NUM3:21; hence ((1 / tau) * ((Lucas (n + 1)) + (1 / 2))) - 1 < Lucas n by XCMPLX_1:99; ::_thesis: verum end; hence Lucas n = [\((1 / tau) * ((Lucas (n + 1)) + (1 / 2)))/] by A4, INT_1:def_6; ::_thesis: verum 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)/] proof let n, k be Nat; ::_thesis: ( 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 ) ; ::_thesis: 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 empty 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 percases ( k is even or k is odd ) ; supposeA8: k is even ; ::_thesis: ((((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; ::_thesis: verum end; supposeA15: k is odd ; ::_thesis: ((((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 empty 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 proof defpred S1[ Nat] means (2 to_power (\$1 + 1)) - (((sqrt 5) - 1) to_power (\$1 + 1)) >= ((sqrt 5) - 1) to_power (\$1 + 1); A22: (2 to_power (1 + 1)) - (((sqrt 5) - 1) to_power (1 + 1)) = (2 ^2) - (((sqrt 5) - 1) to_power 2) by POWER:46 .= 4 - (((sqrt 5) - 1) ^2) by POWER:46 .= 4 - ((((sqrt 5) ^2) - ((2 * (sqrt 5)) * 1)) + (1 ^2)) .= 4 - ((5 - (2 * (sqrt 5))) + 1) by SQUARE_1:def_2 .= (2 * (sqrt 5)) - 2 ; A23: ((sqrt 5) - 1) to_power (1 + 1) = ((sqrt 5) - 1) ^2 by POWER:46 .= (((sqrt 5) ^2) - ((2 * (sqrt 5)) * 1)) + (1 ^2) .= (5 - (2 * (sqrt 5))) + 1 by SQUARE_1:def_2 .= 6 - (2 * (sqrt 5)) ; sqrt 5 >= sqrt (2 ^2) by SQUARE_1:27; then sqrt 5 >= 2 by SQUARE_1:def_2; then (sqrt 5) * 4 >= 2 * 4 by XREAL_1:64; then (((sqrt 5) * 2) + ((sqrt 5) * 2)) - 2 >= (6 + 2) - 2 by XREAL_1:9; then ((((sqrt 5) * 2) + ((sqrt 5) * 2)) - 2) - (2 * (sqrt 5)) >= 6 - (2 * (sqrt 5)) by XREAL_1:9; then A24: S1[1] by A22, A23; A25: for k being non empty Nat st S1[k] holds S1[k + 1] proof let k be non empty Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) A26: (sqrt 5) - 1 > 1 - 1 by A2, XREAL_1:9; assume S1[k] ; ::_thesis: S1[k + 1] then ((2 to_power (k + 1)) - (((sqrt 5) - 1) to_power (k + 1))) + (((sqrt 5) - 1) to_power (k + 1)) >= (((sqrt 5) - 1) to_power (k + 1)) + (((sqrt 5) - 1) to_power (k + 1)) by XREAL_1:6; then (2 to_power (k + 1)) * ((sqrt 5) - 1) >= (2 * (((sqrt 5) - 1) to_power (k + 1))) * ((sqrt 5) - 1) by A26, XREAL_1:64; then (2 to_power (k + 1)) * ((sqrt 5) - 1) >= 2 * ((((sqrt 5) - 1) to_power (k + 1)) * ((sqrt 5) - 1)) ; then (2 to_power (k + 1)) * ((sqrt 5) - 1) >= 2 * ((((sqrt 5) - 1) to_power (k + 1)) * (((sqrt 5) - 1) to_power 1)) by POWER:25; then A27: (2 to_power (k + 1)) * ((sqrt 5) - 1) >= 2 * (((sqrt 5) - 1) to_power ((k + 1) + 1)) by Th2, A26; sqrt (3 ^2) >= sqrt 5 by SQUARE_1:27; then 3 >= sqrt 5 by SQUARE_1:def_2; then 3 - 1 >= (sqrt 5) - 1 by XREAL_1:9; then 2 * (2 to_power (k + 1)) >= ((sqrt 5) - 1) * (2 to_power (k + 1)) by XREAL_1:64; then (2 to_power 1) * (2 to_power (k + 1)) >= ((sqrt 5) - 1) * (2 to_power (k + 1)) by POWER:25; then 2 to_power ((1 + k) + 1) >= ((sqrt 5) - 1) * (2 to_power (k + 1)) by Th2; then 2 to_power ((1 + k) + 1) >= 2 * (((sqrt 5) - 1) to_power ((k + 1) + 1)) by A27, XXREAL_0:2; then (2 to_power ((1 + k) + 1)) - (((sqrt 5) - 1) to_power ((k + 1) + 1)) >= (2 * (((sqrt 5) - 1) to_power ((k + 1) + 1))) - (((sqrt 5) - 1) to_power ((k + 1) + 1)) by XREAL_1:9; hence S1[k + 1] ; ::_thesis: verum end; for k being non empty Nat holds S1[k] from NAT_1:sch_10(A24, A25); then (2 to_power ((m - 1) + 1)) - (((sqrt 5) - 1) to_power ((m - 1) + 1)) >= ((sqrt 5) - 1) to_power ((m - 1) + 1) by A19; hence (2 to_power m) - (((sqrt 5) - 1) to_power m) >= ((sqrt 5) - 1) to_power m ; ::_thesis: verum end; 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; ::_thesis: 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; ::_thesis: 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; ::_thesis: verum end; (((tau to_power k) * (Lucas n)) + 1) - 1 < Lucas (n + k) proof defpred S1[ Nat] means (tau to_power \$1) * (Lucas n) < Lucas (n + \$1); tau_bar to_power n < 0 by Th7, A1; then ((tau_bar to_power n) * tau) - ((tau_bar to_power n) * tau_bar) < 0 ; then ((tau_bar to_power n) * tau) - ((tau_bar to_power n) * (tau_bar to_power 1)) < 0 by POWER:25; then ((tau_bar to_power n) * tau) - (tau_bar to_power (n + 1)) < 0 by Th2; then (((tau_bar to_power n) * tau) - (tau_bar to_power (n + 1))) + ((tau to_power (n + 1)) + (tau_bar to_power (n + 1))) < 0 + ((tau to_power (n + 1)) + (tau_bar to_power (n + 1))) by XREAL_1:6; then ((tau_bar to_power n) * tau) + (tau to_power (n + 1)) < Lucas (n + 1) by FIB_NUM3:21; then ((tau_bar to_power n) * tau) + ((tau to_power n) * (tau to_power 1)) < Lucas (n + 1) by Th2; then ((tau_bar to_power n) * tau) + ((tau to_power n) * tau) < Lucas (n + 1) by POWER:25; then ((tau_bar to_power n) + (tau to_power n)) * tau < Lucas (n + 1) ; then (Lucas n) * tau < Lucas (n + 1) by FIB_NUM3:21; then A33: S1[1] by POWER:25; A34: for m being non empty Nat st S1[m] holds S1[m + 1] proof let m be non empty Nat; ::_thesis: ( S1[m] implies S1[m + 1] ) assume S1[m] ; ::_thesis: S1[m + 1] A35: (1 - (sqrt 5)) to_power (m + 1) < (1 + (sqrt 5)) to_power (m + 1) proof reconsider s = m + 1 as Element of NAT by ORDINAL1:def_12; (1 - (sqrt 5)) to_power s <= abs ((1 - (sqrt 5)) to_power s) by ABSVALUE:4; then A36: (1 - (sqrt 5)) to_power s <= (abs (1 - (sqrt 5))) to_power s by SERIES_1:2; sqrt 5 > sqrt 1 by SQUARE_1:27; then - (sqrt 5) < - 1 by SQUARE_1:18, XREAL_1:24; then A37: (- (sqrt 5)) + 1 < (- 1) + 1 by XREAL_1:6; then A38: abs (1 - (sqrt 5)) = - (1 - (sqrt 5)) by ABSVALUE:def_1; - (1 - (sqrt 5)) = (- 1) + (sqrt 5) ; then - (1 - (sqrt 5)) < 1 + (sqrt 5) by XREAL_1:6; then (abs (1 - (sqrt 5))) to_power s < (1 + (sqrt 5)) to_power s by A38, A37, POWER:37; hence (1 - (sqrt 5)) to_power (m + 1) < (1 + (sqrt 5)) to_power (m + 1) by A36, XXREAL_0:2; ::_thesis: verum end; 2 to_power (m + 1) > 0 by POWER:34; then ((1 - (sqrt 5)) to_power (m + 1)) / (2 to_power (m + 1)) < ((1 + (sqrt 5)) to_power (m + 1)) / (2 to_power (m + 1)) by A35, XREAL_1:74; then ((1 - (sqrt 5)) / 2) to_power (m + 1) < ((1 + (sqrt 5)) to_power (m + 1)) / (2 to_power (m + 1)) by Th1; then ( tau_bar to_power (m + 1) < tau to_power (m + 1) & tau_bar to_power n < 0 ) by A1, Th7, Th1, FIB_NUM:def_1, FIB_NUM:def_2; then (tau_bar to_power (m + 1)) * (tau_bar to_power n) > (tau to_power (m + 1)) * (tau_bar to_power n) by XREAL_1:69; then ((tau_bar to_power (m + 1)) * (tau_bar to_power n)) + (tau to_power ((n + m) + 1)) > ((tau to_power (m + 1)) * (tau_bar to_power n)) + (tau to_power ((n + m) + 1)) by XREAL_1:6; then (tau_bar to_power ((m + 1) + n)) + (tau to_power ((n + m) + 1)) > ((tau to_power (m + 1)) * (tau_bar to_power n)) + (tau to_power ((n + m) + 1)) by Th2; then (tau_bar to_power ((m + 1) + n)) + (tau to_power ((n + m) + 1)) > ((tau to_power (m + 1)) * (tau_bar to_power n)) + ((tau to_power n) * (tau to_power (m + 1))) by Th2; then Lucas ((n + m) + 1) > (tau to_power (m + 1)) * ((tau_bar to_power n) + (tau to_power n)) by FIB_NUM3:21; hence S1[m + 1] by FIB_NUM3:21; ::_thesis: verum end; for m being non empty Nat holds S1[m] from NAT_1:sch_10(A33, A34); hence (((tau to_power k) * (Lucas n)) + 1) - 1 < Lucas (n + k) by A1; ::_thesis: verum end; hence Lucas (n + k) = [\(((tau to_power k) * (Lucas n)) + 1)/] by A3, INT_1:def_6; ::_thesis: verum end;