:: Fibonacci Numbers :: by Robert M. Solovay :: :: Received April 19, 2002 :: Copyright (c) 2002-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, INT_2, ARYTM_3, RELAT_1, NAT_1, CARD_1, XXREAL_0, PRE_FF, FUNCT_3, SQUARE_1, ARYTM_1, COMPLEX1, POWER, NEWTON, SEQ_1, VALUED_0, VALUED_1, FUNCT_1, SEQ_2, ORDINAL2, XXREAL_2, FIB_NUM, REAL_1; notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, NAT_D, INT_2, VALUED_0, VALUED_1, SEQ_1, XXREAL_0, COMPLEX1, PRE_FF, COMSEQ_2, SEQ_2, QUIN_1, NEWTON, POWER; constructors REAL_1, SQUARE_1, NAT_1, NAT_D, QUIN_1, SEQ_2, SEQM_3, LIMFUNC1, NEWTON, POWER, PRE_FF, VALUED_1, PARTFUN1, SETFAM_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, NUMBERS; registrations RELSET_1, XREAL_0, SQUARE_1, MEMBERED, QUIN_1, NEWTON, INT_1, VALUED_0, VALUED_1, FUNCT_2, NUMBERS, SEQ_4, NAT_1, SEQ_2, ORDINAL1, FDIFF_1; requirements SUBSET, NUMERALS, REAL, ARITHM, BOOLE; equalities SQUARE_1, VALUED_1, XCMPLX_0; theorems NAT_1, PRE_FF, INT_2, SQUARE_1, WSIERP_1, EULER_1, PYTHTRIP, QUIN_1, ABSVALUE, POWER, NEWTON, SEQM_3, SEQ_1, SEQ_2, SEQ_4, PREPOWER, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, FUNCT_2, ORDINAL1, NAT_D, VALUED_1, VALUED_0, XREAL_0, TARSKI; schemes NAT_1, SEQ_1; begin :: Fibonacci commutes with gcd :: The proof we present is a slight adaptation of the one found in :: ``The Fibonacci Numbers'' by N. N. Vorobyov reserve k,m, n, p for Element of NAT; :: Preliminary lemmas theorem Th1: for m, n being Element of NAT holds m gcd n = m gcd (n + m) proof let m, n; set a = m gcd n; set b = m gcd (n + m); A1: a divides m by NAT_D:def 5; A2: b divides m by NAT_D:def 5; b divides n + m by NAT_D:def 5; then b divides n by A2,NAT_D:10; then A3: b divides a by A2,NAT_D:def 5; a divides n by NAT_D:def 5; then a divides n + m by A1,NAT_D:8; then a divides b by A1,NAT_D:def 5; hence thesis by A3,NAT_D:5; end; theorem Th2: for k, m, n being Element of NAT st k gcd m = 1 holds k gcd m * n = k gcd n proof defpred P[Nat] means for m, n holds \$1 gcd m = 1 implies \$1 gcd m * n = \$1 gcd n; A1: for k being Nat holds (for a being Nat st a < k holds P[a]) implies P[k] proof let k be Nat; assume A2: for a being Nat st a < k holds P[a]; per cases by NAT_1:25; suppose A3: k = 0; let m, n; assume k gcd m = 1; then 1 = m by A3,NEWTON:52; hence thesis; end; suppose A4: k = 1; let m, n; assume k gcd m = 1; k gcd m * n = 1 by A4,NEWTON:51; hence thesis by A4,NEWTON:51; end; suppose A5: k > 1; let m, n; set b = k gcd m * n; assume A6: k gcd m = 1; thus thesis proof per cases by NAT_1:25; suppose b = 0; then 0 divides k by NAT_D:def 5; then k = 0 by INT_2:3; hence thesis by A5; end; suppose A7: b = 1; set c = k gcd n; A8: c divides k by NAT_D:def 5; A9: n divides m * n by NAT_D:def 3; c divides n by NAT_D:def 5; then c divides m * n by A9,NAT_D:4; then c divides 1 by A7,A8,NAT_D:def 5; hence thesis by A7,WSIERP_1:15; end; suppose b > 1; then b >= 1 + 1 by NAT_1:13; then consider p such that A10: p is prime and A11: p divides b by INT_2:31; b divides k by NAT_D:def 5; then A12: p divides k by A11,NAT_D:4; then consider s being Nat such that A13: k = p * s by NAT_D:def 3; A14: not p divides m proof assume p divides m; then p divides 1 by A6,A12,NAT_D:def 5; then p = 1 by WSIERP_1:15; hence thesis by A10,INT_2:def 4; end; b divides m * n by NAT_D:def 5; then p divides m * n by A11,NAT_D:4; then p divides n by A10,A14,NEWTON:80; then consider r being Nat such that A15: n = p * r by NAT_D:def 3; reconsider s as Element of NAT by ORDINAL1:def 12; A16: s + 1 > s by XREAL_1:29; p > 1 by A10,INT_2:def 4; then p >= 1 + 1 by NAT_1:13; then A17: s * p >= s * (1 + 1) by NAT_1:4; s <> 0 by A5,A13; then s + s > s by XREAL_1:29; then s + s >= s + 1 by NAT_1:13; then k >= s + 1 by A13,A17,XXREAL_0:2; then A18: s < k by A16,XXREAL_0:2; A19: s gcd m = 1 proof set c = s gcd m; A20: c divides s by NAT_D:def 5; A21: c divides m by NAT_D:def 5; s divides k by A13,NAT_D:def 3; then c divides k by A20,NAT_D:4; then c divides 1 by A6,A21,NAT_D:def 5; hence thesis by WSIERP_1:15; end; reconsider r as Element of NAT by ORDINAL1:def 12; A22: k gcd n = p * (s gcd r) by A13,A15,PYTHTRIP:8; k gcd m * n = p * s gcd p * (m * r) by A13,A15 .= p * (s gcd m * r) by PYTHTRIP:8; hence thesis by A2,A18,A19,A22; end; end; end; end; for k being Nat holds P[k] from NAT_1:sch 4(A1); hence thesis; end; theorem Th3: for s being Real st s > 0 ex n being Element of NAT st n > 0 & 0 < 1/n & 1/n <= s proof let s be Real; consider n being Nat such that A1: n > 1/s by SEQ_4:3; A2: 1/(1/s) = 1/s" .= s; A3: n in NAT by ORDINAL1:def 12; assume s > 0; then A4: 1/s > 0; take n; thus thesis by A4,A1,A2,XREAL_1:85,A3; end; scheme FibInd {P[set] } : for k being Nat holds P[k] provided A1: P[0] and A2: P[1] and A3: for k being Nat st P[k] & P[k+1] holds P[k+2] proof let k be Nat; defpred Q[Nat] means P[\$1] & P[\$1 + 1]; A4: for k being Nat st Q[k] holds Q[k+1] proof let k be Nat; A5: k + 2 = (k + 1) + 1; assume Q[k]; hence thesis by A3,A5; end; A6: Q[0] by A1,A2; for k being Nat holds Q[k] from NAT_1:sch 2(A6,A4); hence thesis; end; scheme BinInd { P[Nat,Nat] } : for m, n being Element of NAT holds P[m, n] provided A1: for m, n being Element of NAT st P[m,n] holds P[n,m] and A2: for k being Element of NAT st (for m, n being Element of NAT st (m < k & n < k) holds P[m,n]) holds for m being Element of NAT st m <= k holds P[k,m ] proof defpred Q[Nat] means for m, n st (m <= \$1 & n <= \$1) holds P[m,n]; A3: for k being Nat st (for r being Nat st r < k holds Q[r]) holds Q[k] proof let k be Nat; assume A4: for r being Nat st r < k holds Q[r]; let m, n; assume that A5: m <= k and A6: n <= k; set s = max(m,n); A0: s is Nat by TARSKI:1; A7: s <= k by A5,A6,XXREAL_0:28; per cases by A7,XXREAL_0:1; suppose s < k; then m <= s & n <= s implies P[m,n] by A4,A0; hence thesis by XXREAL_0:25; end; suppose A8: s = k; A9: for m, n holds m < k & n < k implies P[m,n] proof let m, n; assume that A10: m < k and A11: n < k; set s = max(m,n); A0: s is Nat by TARSKI:1; A12: m <= s by XXREAL_0:25; A13: n <= s by XXREAL_0:25; s < k by A10,A11,XXREAL_0:16; hence thesis by A4,A0,A12,A13; end; thus thesis proof per cases by A8,XXREAL_0:16; suppose k = m; hence thesis by A2,A6,A9; end; suppose k = n; then P[n,m] by A2,A5,A9; hence thesis by A1; end; end; end; end; A14: for k being Nat holds Q[k] from NAT_1:sch 4(A3); let m, n; set k = max(m,n); k is Nat by TARSKI:1; then m <= k & n <= k implies P[m,n] by A14; hence thesis by XXREAL_0:30; end; 0 + 1 + 1 = 2; then Lm1: Fib(2) = 1 by PRE_FF:1; Lm2: 1 + 1 + 1 = 3; Lm3: for k being Nat holds Fib(k+1) >= k proof defpred P[Nat] means Fib(\$1 +1) >= \$1; 0 + 1 + 1 = 2; then A1: P[1] by PRE_FF:1; A2: for k being Nat st P[k] & P[k+1] holds P[k+2] proof let k be Nat; assume that A3: P[k] and A4: P[k+1]; per cases; suppose k = 0; hence thesis by Lm1,Lm2,PRE_FF:1; end; suppose k <> 0; then 1 <= k by NAT_1:14; then A5: 1 + (k+1) <= k + (k+1) by XREAL_1:6; A6: Fib((k + 2) + 1) = Fib((k+1) + 1) + Fib(k+1) by PRE_FF:1; A7: k + (k+1) <= Fib(k+1) + (k+1) by A3,XREAL_1:6; Fib(k+1) + (k+1) <= Fib((k+1)+1) + Fib(k+1) by A4,XREAL_1:6; then k + (k+1) <= Fib((k+2)+1) by A6,A7,XXREAL_0:2; hence thesis by A5,XXREAL_0:2; end; end; A8: P[0]; thus for k being Nat holds P[k] from FibInd(A8, A1, A2); end; Lm4: for m being Nat holds Fib(m+1) >= Fib(m) proof defpred P[Nat] means Fib(\$1 + 1) >= Fib(\$1); A1: for k being Nat st P[k] holds P[k+1] proof let k be Nat; Fib((k+1) + 1) = Fib(k+1) + Fib(k) by PRE_FF:1; then Fib((k+1) + 1) >= Fib(k+1) + 0 by XREAL_1:6; hence thesis; end; A2: P[0] by PRE_FF:1; thus for k being Nat holds P[k] from NAT_1:sch 2(A2,A1); end; Lm5: for m, n being Element of NAT st m >= n holds Fib(m) >= Fib(n) proof A1: for k, n being Element of NAT holds Fib(n+k) >= Fib(n) proof defpred P[Nat] means for n being Element of NAT holds Fib(n+\$1) >= Fib(n); A2: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume A3: P[k]; let n; n + (k+1) = (n+k) + 1; then A4: Fib(n + (k+1)) >= Fib(n+k) by Lm4; Fib(n+k) >= Fib(n) by A3; hence thesis by A4,XXREAL_0:2; end; let k, n be Element of NAT; A5: P[0]; for k being Nat holds P[k] from NAT_1:sch 2(A5, A2); hence thesis; end; let m, n be Element of NAT; assume m >= n; then consider k be Nat such that A6: m = n+k by NAT_1:10; reconsider k as Element of NAT by ORDINAL1:def 12; m = n+k by A6; hence thesis by A1; end; Lm6: for m being Element of NAT holds Fib(m+1) <> 0 proof let m; per cases; suppose m = 0; hence thesis by PRE_FF:1; end; suppose m <> 0; hence thesis by Lm3,NAT_1:3; end; end; theorem Th4: for m, n being Nat holds Fib(m + (n + 1)) = (Fib(n) * Fib (m)) + (Fib(n + 1) * Fib (m + 1)) proof defpred P[Nat] means for n being Nat holds Fib(\$1 + (n + 1)) = (Fib(n) * Fib (\$1)) + (Fib(n + 1) * Fib(\$1 + 1)); A1: P[0] by PRE_FF:1; A2: now let k be Nat; assume that A3: P[k] and A4: P[k+1]; thus P[k+2] proof let n be Nat; A5: Fib(((k+1) + 1) + (n+1)) = Fib(((k + (n + 1)) + 1) + 1) .= Fib(k + (n+1)) + Fib((k+1) + (n+1)) by PRE_FF:1; set a = Fib(n) * Fib(k), b = Fib(n+1) * Fib(k+1), c = Fib(n) * Fib(k+1), d = Fib(n+1) * Fib((k+1) + 1); A6: (a + b) + (c + d) = (a + c) + (b + d); A7: b + d = Fib(n+1) * (Fib(k+1) + Fib ((k+1) + 1)) .= Fib(n+1) * Fib(((k + 1) + 1) + 1) by PRE_FF:1; A8: a + c = Fib(n) * (Fib(k) + Fib(k+1)) .= Fib(n) * Fib((k+1) + 1) by PRE_FF:1; Fib(k + (n+1)) = Fib(n) * Fib(k) + Fib(n+1) * Fib(k+1) by A3; hence thesis by A4,A5,A6,A8,A7; end; end; A9: P[1] by Lm1,PRE_FF:1; thus for k being Nat holds P[k] from FibInd(A1, A9, A2); end; Lm7: for n being Nat holds Fib(n) gcd Fib(n + 1) = 1 proof defpred P[Nat] means Fib(\$1) gcd Fib(\$1 + 1) = 1; A1: now let k be Nat; assume A2: P[k]; Fib(k +1) gcd Fib((k + 1) + 1) = Fib(k +1) gcd (Fib(k + 1) + Fib(k)) by PRE_FF:1 .= 1 by A2,Th1; hence P[k+1]; end; A3: P[0] by NEWTON:52,PRE_FF:1; thus for m being Nat holds P[m] from NAT_1:sch 2(A3,A1); end; theorem for m, n being Element of NAT holds Fib(m) gcd Fib(n) = Fib(m gcd n) proof defpred P[Element of NAT,Element of NAT] means Fib(\$1) gcd Fib(\$2) = Fib(\$1 gcd \$2); A1: for k st (for m, n st (m < k & n < k) holds P[m,n]) holds for m st m <= k holds P[k,m] proof let k; assume A2: for m, n st m < k & n < k holds P[m,n]; let m; assume A3: m <= k; per cases by A3,XXREAL_0:1; suppose A4: m = k; hence Fib k gcd Fib m = Fib k by NAT_D:32 .= Fib(k gcd m) by A4,NAT_D:32; end; suppose A5: m < k; thus thesis proof per cases; suppose A6: m = 0; then Fib(k) gcd Fib(m) = Fib(k) by NEWTON:52,PRE_FF:1; hence thesis by A6,NEWTON:52; end; suppose A7: m > 0; thus thesis proof consider r be Nat such that A8: k = m + r by A3,NAT_1:10; reconsider r as Element of NAT by ORDINAL1:def 12; A9: r <= k by A8,NAT_1:11; r <> 0 by A5,A8; then consider rr being Nat such that A10: r = rr + 1 by NAT_1:6; reconsider rr as Element of NAT by ORDINAL1:def 12; Fib(k) = (Fib(rr+1) * Fib(m+1)) + (Fib (rr) * Fib(m)) by A8,A10,Th4 ; then A11: Fib (k) gcd Fib(m) = Fib(m) gcd (Fib(m+1) * Fib(r)) by A10,EULER_1:8; Fib(m) gcd Fib(m+1) = 1 by Lm7; then A12: Fib(k) gcd Fib(m) = Fib(m) gcd Fib(r) by A11,Th2; r <> k by A7,A8; then A13: r < k by A9,XXREAL_0:1; k gcd m = m gcd r by A8,Th1; hence thesis by A2,A5,A12,A13; end; end; end; end; end; A14: for m, n holds P[m,n] implies P[n,m]; thus for m, n holds P[m,n] from BinInd(A14,A1); end; begin :: The relationship between the Fibonacci numbers and the :: roots of the equation x^2 = x + 1 :: The formula for the roots of a quadratic equation reserve x, a, b, c for Real; theorem Th6: for x, a, b, c being Real st a <> 0 & delta(a,b,c) >= 0 holds a * x^2 + b * x + c = 0 iff (x = (- b - sqrt delta(a,b,c))/(2 * a) or x = (- b + sqrt delta(a,b,c))/(2 * a)) proof let x, a, b, c; set lh = a * x^2 + b * x + c; set r1 = (- b - sqrt delta(a,b,c))/(2 * a); set r2 = ( - b + sqrt delta(a,b,c))/(2 * a); assume that A1: a <> 0 and A2: delta(a,b,c) >= 0; lh = a * (x - r1) * (x - r2) by A1,A2,QUIN_1:16; hence thesis by A1,A2,QUIN_1:15; end; :: The roots of x^2 - x - 1 = 0 :: The value of tau is approximately 1.618 definition func tau -> Real equals (1 + sqrt 5)/2; correctness; end; :: The value of tau_bar is approximately -.618 definition func tau_bar -> Real equals (1 - sqrt 5)/2; correctness; end; Lm8: tau ^2 = tau + 1 & tau_bar ^2 = tau_bar + 1 proof A1: delta(1, -1, -1) = (-1) ^2 - (4 * 1 * (-1)) by QUIN_1:def 1 .= 5; then A2: (- (-1) - sqrt delta(1, -1, -1)) / (2 * 1) = tau_bar; A3: for x holds (x = tau or x = tau_bar) implies x^2 = x + 1 proof let x; assume x = tau or x = tau_bar; then 1 * x^2 + (-1) * x + (-1) = 0 by A1,A2,Th6; hence thesis; end; hence tau^2 = tau + 1; thus thesis by A3; end; Lm9: 2 < sqrt 5 by SQUARE_1:20,27; Lm10: sqrt 5 <> 0 by SQUARE_1:20,27; Lm11: sqrt 5 < 3 proof 3 ^2 = 9; then sqrt 9 = 3 by SQUARE_1:22; hence thesis by SQUARE_1:27; end; 1 < tau proof 2 < sqrt 5 by SQUARE_1:20,27; then 1 < sqrt 5 by XXREAL_0:2; then 1 + 1 < (1 + sqrt 5) by XREAL_1:8; then 2/2 < (1 + sqrt 5)/2 by XREAL_1:74; hence thesis; end; then Lm12: 0 < tau; Lm13: tau_bar < 0 proof 2 < sqrt 5 by SQUARE_1:20,27; then not (0 + sqrt 5) <= 1 by XXREAL_0:2; then 0 * 2 > (1 - sqrt 5)/1 by XREAL_1:19; then (1 - sqrt 5)/2 < 0 * 1 by XREAL_1:113; hence thesis; end; Lm14: |.tau_bar.| < 1 proof sqrt 5 - 1 < 3 - 1 by Lm11,XREAL_1:9; then A1: (sqrt 5 - 1)/2 < 2/2 by XREAL_1:74; |.tau_bar.| = -(1 - sqrt 5)/2 by Lm13,ABSVALUE:def 1 .= (sqrt 5 - 1)/2; hence thesis by A1; end; theorem Th7: for n being Nat holds Fib(n) = ((tau to_power n) - (tau_bar to_power n))/(sqrt 5) proof defpred P[Nat] means Fib(\$1) = ((tau to_power \$1) - (tau_bar to_power \$1))/( sqrt 5); A1: tau_bar to_power 1 = tau_bar by POWER:25; tau_bar to_power 0 = 1 by POWER:24; then ((tau to_power 0) - (tau_bar to_power 0))/(sqrt 5) = (1 - 1)/(sqrt 5) by POWER:24 .= 0; then A2: P[0] by PRE_FF:1; A3: for k being Nat st P[k] & P[k+1] holds P[k+2] proof let k be Nat; assume that A4: P[k] and A5: P[k+1]; set a = tau to_power k, a1 = tau_bar to_power k, b = tau to_power (k+1), b1 = tau_bar to_power (k+1), c = tau to_power (k+2), c1 = tau_bar to_power (k+2 ); A6: c1 = tau_bar |^ (k + 2) by POWER:41 .= (tau_bar |^ k) * (tau_bar |^ (1 + 1)) by NEWTON:8 .= (tau_bar |^ k) * (tau_bar * (tau_bar |^ 1)) by NEWTON:6 .= (tau_bar |^ k) * (tau_bar + 1) by Lm8 .= (tau_bar |^ k * tau_bar) + (tau_bar |^ k) * 1 .= (tau_bar |^ (k+1)) + (tau_bar |^ k) * 1 by NEWTON:6 .= b1 + (tau_bar |^ k) by POWER:41 .= a1 + b1 by POWER:41; A7: c = (tau to_power 2) * (tau to_power k) by Lm12,POWER:27 .= (tau to_power k) * (tau + 1) by Lm8,POWER:46 .= (tau to_power k) * tau + (tau to_power k) * 1 .= (tau to_power k) * (tau to_power 1) + a by POWER:25 .= a + b by Lm12,POWER:27; Fib(k+2) = Fib((k + 1) + 1) .= (a - a1)/(sqrt 5) + (b - b1)/(sqrt 5) by A4,A5,PRE_FF:1 .= (c - c1)/(sqrt 5) by A7,A6; hence thesis; end; tau - tau_bar = sqrt 5; then ((tau to_power 1) - (tau_bar to_power 1))/(sqrt 5) = (sqrt 5)/(sqrt 5) by A1,POWER:25 .= Fib(1) by Lm10,PRE_FF:1,XCMPLX_1:60; then A8: P[1]; thus for n being Nat holds P[n] from FibInd(A2, A8, A3); end; Lm15: for x being Real st |.x.| <= 1 holds |.x |^ n.| <= 1 proof let x; defpred P[Nat] means |.x |^ \$1.| <= 1; assume A1: |.x.| <= 1; A2: for k being Nat st P[k] holds P[k+1] proof let k be Nat; A3: |.x |^ (k+1).| = |.(x |^ k) * x.| by NEWTON:6 .= |.x |^ k.| * |.x.| by COMPLEX1:65; assume P[k]; hence thesis by A1,A3,COMPLEX1:46,XREAL_1:160; end; |.x |^ 0.| = |.1.| by NEWTON:4 .= 1 by ABSVALUE:def 1; then A4: P[0]; for k being Nat holds P[k] from NAT_1:sch 2(A4, A2); hence thesis; end; Lm16: for n holds |.(tau_bar to_power n)/(sqrt 5).| < 1 proof let n; set y = (tau_bar to_power n), z = sqrt 5; A1: |.y.| = |.tau_bar |^ n.| by POWER:41; A2: |.y/z.| = |.y * z".| .= |.y.| * |.z".| by COMPLEX1:65; A3: 1/z < 1/2 by Lm9,XREAL_1:88; z > 0 by Lm9; then A4: z" > 0; then |.z".| = z" by ABSVALUE:def 1; then A5: |.z".| < 1 by A3,XXREAL_0:2; |.z".| >= 0 by A4,ABSVALUE:def 1; hence thesis by A1,A2,A5,Lm14,Lm15,XREAL_1:162; end; theorem for n being Element of NAT holds |.Fib(n) - (tau to_power n)/(sqrt 5 ).| < 1 proof let n; set k = Fib(n), x = (tau to_power n), y = (tau_bar to_power n), z = sqrt 5; k = (x - y)/z by Th7 .= x/z - y/z; then |.-(k - x/z).| < 1 by Lm16; hence thesis by COMPLEX1:52; end; reserve F, f, g, h for Real_Sequence; theorem Th9: for f, g, h being Real_Sequence st g is non-zero holds (f /" g) (#) (g /" h) = (f /" h) proof let f, g, h be Real_Sequence; set f3 = (f /" g), g3 = (g /" h), h3 = (f /" h); assume A1: g is non-zero; for n holds (f3 (#) g3).n = h3.n proof let n; set a = f.n, b = (g.n)", c = g.n, d = (h.n)"; A2: g3.n = c * (h".n) by SEQ_1:8 .= c * d by VALUED_1:10; A3: h3.n = a * (h".n) by SEQ_1:8 .= a * d by VALUED_1:10; A4: g.n <> 0 by A1,SEQ_1:5; A5: b * c = (1/c) * c .= 1 by A4,XCMPLX_1:106; f3.n = a * (g".n) by SEQ_1:8 .= a * b by VALUED_1:10; then (f3 (#) g3).n = (a * b) * (c * d) by A2,SEQ_1:8 .= ((b * c) * a) * d .= h3.n by A3,A5; hence thesis; end; hence thesis by FUNCT_2:63; end; theorem Th10: for f, g being Real_Sequence for n being Element of NAT holds (f /" g) . n = (f .n) / (g.n) & (f /" g) . n = (f.n) * (g.n)" proof let f, g; let n; A1: (f /" g). n = (f.n) * (g".n) by SEQ_1:8 .= (f.n) * (g.n)" by VALUED_1:10; hence (f /" g). n = (f.n) / (g.n); thus thesis by A1; end; theorem for F being Real_Sequence st (for n being Element of NAT holds F.n = Fib(n+1)/Fib(n)) holds F is convergent & lim F = tau proof deffunc ff(Nat) = (tau to_power \$1)/(sqrt 5); let F; consider f such that A1: for n being Nat holds f.n = Fib(n) from SEQ_1:sch 1; set f2 = f ^\ 2; set f1 = (f ^\ 1); A2: f1 ^\ 1 = f ^\ (1 + 1) by NAT_1:48 .= f2; A3: for n holds f2.n <> 0 proof let n; f2.n = f.(n+2) by NAT_1:def 3 .= Fib((n+1) + 1) by A1; hence thesis by Lm3; end; reconsider jj=1 as Element of REAL by XREAL_0:def 1; A4: for n being Nat holds (f2 /" f2) . n = jj proof let n be Nat; A5: n in NAT by ORDINAL1:def 12; then (f2 /" f2).n = (f2.n) * (f2.n)" by Th10 .= (f2.n) * ( 1/ (f2.n)) .= 1 by A3,A5,XCMPLX_1:106; hence thesis; end; then A6: (f2 /" f2) is constant by VALUED_0:def 18; A7: (f /" f) ^\ 2 = (f2 /" f2) by SEQM_3:20; then A8: f /" f is convergent by A6,SEQ_4:21; (f2 /" f2) . 0 = 1 by A4; then lim (f2 /" f2) = 1 by A6,SEQ_4:25; then A9: lim (f /" f) = 1 by A6,A7,SEQ_4:22; ex g st for n being Nat holds g . n = ff(n) from SEQ_1:sch 1; then consider g such that A10: for n being Nat holds g.n = ff(n); set g1 = g ^\ 1; A11: for n being Nat holds g.n <> 0 proof let n be Nat; A12: (sqrt 5) " <> 0 by SQUARE_1:20,27,XCMPLX_1:202; A13: (tau |^ n) <> 0 by Lm12,PREPOWER:5; g.n = (tau to_power n) / (sqrt 5) by A10 .= (tau to_power n) * (sqrt 5)" .= (tau |^ n) * (sqrt 5)" by POWER:41; hence thesis by A13,A12,XCMPLX_1:6; end; then A14: g is non-zero by SEQ_1:5; A15: (f2 /" f1) = (f2 /" g1) (#) (g1 /" f1) by Th9,A14; set g2 = g1 ^\ 1; :::BB: g2 is non-zero; for n being Nat holds f1.n <> 0 proof let n be Nat ; A16: n in NAT by ORDINAL1:def 12; f1.n = f.(n+1) by NAT_1:def 3 .= Fib(n+1) by A1; hence thesis by Lm6,A16; end; then A17: f1 is non-zero by SEQ_1:5; for n being Nat holds (g2 /" f2).n <> 0 proof let n be Nat ; A18: n in NAT by ORDINAL1:def 12; A19: (g2.n) <> 0 by A14,SEQ_1:5; A20: (g2 /" f2).n = (g2.n) * (f2.n)" by Th10,A18; (f2.n)" <> 0 by A17,A2,SEQ_1:5,XCMPLX_1:202; hence thesis by A19,A20,XCMPLX_1:6; end; then A21: (g2 /" f2) is non-zero by SEQ_1:5; g2 = g ^\ (1 + 1) by NAT_1:48; then A22: (g2 /" f2) = (g /" f) ^\ 2 by SEQM_3:20; A23: for n holds f1.n = Fib(n+1) proof let n; f1.n = f.(n+1) by NAT_1:def 3 .= Fib(n+1) by A1; hence thesis; end; assume A24: for n being Element of NAT holds F.n = Fib(n+1)/Fib(n); for n holds F.n = (f1 /" f). n proof let n; (f1 /" f). n = (f1 . n) / (f . n) by Th10 .= Fib(n+1)/ (f.n) by A23 .= Fib(n+1)/Fib(n) by A1; hence thesis by A24; end; then F = f1 /" f by FUNCT_2:63; then A25: (f2 /" f1) = F ^\ 1 by A2,SEQM_3:20; A26: (g2 /" g1) = (g1 /" g) ^\ 1 by SEQM_3:20; A27: for n being Nat holds (g1 /" g) . n = tau proof let n be Nat; A28: n in NAT by ORDINAL1:def 12; A29: g.n = (tau to_power n) / (sqrt 5) by A10 .= (tau to_power n) * (sqrt 5)" .= (tau |^ n) * (sqrt 5)" by POWER:41; A30: g.n <> 0 by A11; g1.n = g.(n+1) by NAT_1:def 3 .= (tau to_power (n + 1)) / (sqrt 5) by A10 .= (tau to_power (n+1)) * (sqrt 5)" .= (tau |^ (n+1)) * (sqrt 5)" by POWER:41 .= (tau * (tau |^ n)) * (sqrt 5)" by NEWTON:6 .= tau * (g.n) by A29; then (g1 /" g).n = (tau * (g.n)) * ((g.n)") by A28,Th10 .= tau * ((g.n) * (g.n)") .= tau * 1 by A30,XCMPLX_0:def 7 .= tau; hence thesis; end; tau in REAL by XREAL_0:def 1; then A31: (g1 /" g) is constant by A27,VALUED_0:def 18; A32: for x st 0 < x ex n being Nat st for m being Nat st n <= m holds |.(f".m) - 0.| < x proof let x; assume 0 < x; then consider k such that A33: k > 0 and 0 < 1/k and A34: 1/k <= x by Th3; for m being Nat st (k+2) <= m holds |.(f" . m) - 0.| < x proof let m be Nat; A35: m in NAT by ORDINAL1:def 12; k + 2 = (k + 1) + 1; then A36: Fib(k+2) >= k+1 by Lm3; assume (k+2) <= m; then Fib(k+2) <= Fib(m) by Lm5,A35; then k + 1 <= Fib(m) by A36,XXREAL_0:2; then A37: k + 1 <= f.m by A1; then 0 < f.m; then A38: 0 <= (f.m)"; k + 0 < (k+1) by XREAL_1:6; then A39: 1/(k+1) < 1/k by A33,XREAL_1:88; A40: |.(f".m) - 0.| = |.(f.m)".| by VALUED_1:10 .= (f.m)" by A38,ABSVALUE:def 1 .= 1/(f.m); 1/(f.m) <= 1/(k+1) by A37,XREAL_1:85; then 1/(f.m) < 1/k by A39,XXREAL_0:2; hence thesis by A34,A40,XXREAL_0:2; end; hence thesis; end; then A41: f" is convergent by SEQ_2:def 6; then A42: lim f" = 0 by A32,SEQ_2:def 7; deffunc ff(Nat) = (tau_bar to_power \$1)/(sqrt 5); ex h st for n being Nat holds h . n = ff(n) from SEQ_1:sch 1; then consider h such that A43: for n being Nat holds h.n = ff(n); A44: for n holds f.n = g.n - h.n proof let n; f.n = Fib(n) by A1 .= ((tau to_power n) - (tau_bar to_power n))/(sqrt 5) by Th7 .= (tau to_power n)/(sqrt 5) - (tau_bar to_power n)/(sqrt 5) .= g.n - (tau_bar to_power n)/(sqrt 5) by A10 .= g.n - h.n by A43; hence thesis; end; for n being Nat holds g.n = f.n + h.n proof let n being Nat ; A45: n in NAT by ORDINAL1:def 12; f.n = g.n - h.n by A44,A45; hence thesis; end; then g = f + h by SEQ_1:7; then A46: (g /" f) = (f /" f) + (h /" f) by SEQ_1:49; for n being Nat holds |.h.n.| < 1 proof let n being Nat ; A47: n in NAT by ORDINAL1:def 12; h.n = (tau_bar to_power n)/(sqrt 5) by A43; hence thesis by Lm16,A47; end; then A48: h is bounded by SEQ_2:3; f" is convergent by A32,SEQ_2:def 6; then A49: h /" f is convergent by A48,A42,SEQ_2:25; then A50: (g /" f) is convergent by A8,A46; (g1 /" g) . 0 = tau by A27; then lim (g1 /" g) = tau by A31,SEQ_4:25; then A51: lim (g2 /" g1) = tau by A31,A26,SEQ_4:20; A52: (g1 /" f1) = (g /" f) ^\ 1 by SEQM_3:20; lim (h /" f) = 0 by A48,A41,A42,SEQ_2:26; then A53: lim (g /" f) = 1 + 0 by A49,A8,A9,A46,SEQ_2:6 .= 1; then A54: lim (g2 /" f2) = 1 by A50,A22,SEQ_4:20; then (g2 /" f2)" is convergent by A50,A22,A21,SEQ_2:21; then A55: (f2 /" g2) is convergent by SEQ_1:40; A56: f2 /" g1 = (f2 /" g2) (#) (g2 /" g1) by A14,Th9; then A57: f2 /" g1 is convergent by A31,A55,A26; then A58: (f2 /" f1) is convergent by A50,A52,A15; hence F is convergent by A25,SEQ_4:21; lim (g2 /" f2)" = 1" by A50,A22,A54,A21,SEQ_2:22 .= 1; then lim (f2 /" g2) = 1 by SEQ_1:40; then A59: lim (f2 /" g1) = 1 * tau by A31,A56,A55,A26,A51,SEQ_2:15 .= tau; lim (g1 /" f1) = 1 by A50,A53,A52,SEQ_4:20; then lim (f2 /" f1) = tau * 1 by A50,A59,A57,A52,A15,SEQ_2:15; hence thesis by A58,A25,SEQ_4:22; end;