:: Some Properties of {F}ibonacci Numbers :: by Magdalena Jastrz\c{e}bska and Adam Grabowski :: :: Received May 10, 2004 :: Copyright (c) 2004-2021 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, NAT_1, XBOOLE_0, SUBSET_1, ARYTM_1, ARYTM_3, XXREAL_0, ABIAN, INT_1, POWER, RELAT_1, NEWTON, PREPOWER, SQUARE_1, FINSET_1, MEMBERED, SETFAM_1, FUNCT_1, FINSEQ_1, TARSKI, TURING_1, CARD_1, XXREAL_2, FUNCOP_1, VALUED_1, FUNCT_4, ZFMISC_1, PRE_FF, FIB_NUM, INT_2, ORDINAL4, CARD_3, PYTHTRIP, FIB_NUM2, REAL_1, XCMPLX_0; notations TARSKI, ORDINAL1, ENUMSET1, SUBSET_1, XBOOLE_0, SETFAM_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, VALUED_1, SQUARE_1, INT_1, NAT_1, INT_2, NAT_D, FINSET_1, MEMBERED, RELAT_1, FUNCT_1, FUNCT_2, PRE_FF, RVSUM_1, ZFMISC_1, NEWTON, PREPOWER, POWER, XXREAL_2, ABIAN, DOMAIN_1, FINSEQ_1, FUNCT_4, FIB_NUM, PYTHTRIP, PEPIN, TREES_4; constructors REAL_1, NAT_D, FINSOP_1, NEWTON, PREPOWER, POWER, PRE_FF, BINARITH, WSIERP_1, ABIAN, PEPIN, PYTHTRIP, FIB_NUM, XXREAL_2, RELSET_1, DOMAIN_1, NUMBERS; registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, INT_1, MEMBERED, FINSEQ_1, NEWTON, PREPOWER, ABIAN, NAT_2, VALUED_0, XXREAL_2, RELSET_1, XCMPLX_0; requirements SUBSET, NUMERALS, REAL, ARITHM, BOOLE; begin :: Preliminaries reserve n, k, r, m, i, j for Nat; theorem :: FIB_NUM2:1 for n being non zero Element of NAT holds n -' 1 + 2 = n + 1; theorem :: FIB_NUM2:2 for n being odd Integer holds (-1) to_power n = -1; theorem :: FIB_NUM2:3 for n being even Integer holds (-1) to_power n = 1; theorem :: FIB_NUM2:4 for m being non zero Real, n being Integer holds ((-1) * m) to_power n = ((-1) to_power n) * (m to_power n); theorem :: FIB_NUM2:5 for a being Real holds a to_power (k+m) = (a to_power k) * (a to_power m); theorem :: FIB_NUM2:6 for k being non zero Real, m being odd Integer holds k to_power m to_power n = k to_power (m * n); theorem :: FIB_NUM2:7 ((-1) to_power (-n)) ^2 = 1; theorem :: FIB_NUM2:8 for a being non zero Real holds (a to_power (-k)) * (a to_power (-m)) = a to_power (-k-m); theorem :: FIB_NUM2:9 (-1) to_power (-2 * n) = 1; theorem :: FIB_NUM2:10 for a being non zero Real holds (a to_power k) * (a to_power (-k)) = 1; registration let n be odd Integer; cluster -n -> odd; end; registration let n be even Integer; cluster -n -> even; end; theorem :: FIB_NUM2:11 (-1) to_power (-n) = (-1) to_power n; theorem :: FIB_NUM2:12 for k, m, m1, n1 being Element of NAT st k divides m & k divides n holds k divides m * m1 + n * n1; registration cluster finite non empty natural-membered with_non-empty_elements for set; end; registration let f be sequence of NAT; let A be finite natural-membered with_non-empty_elements set; cluster f | A -> FinSubsequence-like; end; theorem :: FIB_NUM2:13 for p being FinSubsequence holds rng Seq p c= rng p; definition let f be sequence of NAT; let A be finite with_non-empty_elements natural-membered set; func Prefix (f, A) -> FinSequence of NAT equals :: FIB_NUM2:def 1 Seq (f | A); end; theorem :: FIB_NUM2:14 for k being Element of NAT st k <> 0 holds k + m <= n implies m < n; registration cluster NAT -> bounded_below; end; theorem :: FIB_NUM2:15 for x, y being set st 0 < i & i < j holds {[i,x], [j,y]} is FinSubsequence; theorem :: FIB_NUM2:16 for x, y being set, q being FinSubsequence st i < j & q = {[i,x] , [j,y]} holds Seq q = <*x,y*>; registration let n be Nat; cluster Seg n -> with_non-empty_elements; end; registration let A be with_non-empty_elements set; cluster -> with_non-empty_elements for Subset of A; end; registration let A be with_non-empty_elements set; let B be set; cluster A /\ B -> with_non-empty_elements; cluster B /\ A -> with_non-empty_elements; end; theorem :: FIB_NUM2:17 for k being Element of NAT, a being set st k >= 1 holds {[k, a]} is FinSubsequence; theorem :: FIB_NUM2:18 for i being Element of NAT, y being set, f being FinSubsequence st f = { [1,y] } holds Shift(f,i) = { [1+i,y] }; theorem :: FIB_NUM2:19 for q being FinSubsequence, k, n being Element of NAT st dom q c= Seg k & n > k ex p being FinSequence st q c= p & dom p = Seg n; theorem :: FIB_NUM2:20 for q being FinSubsequence holds ex p being FinSequence st q c= p; begin :: Fibonacci Numbers scheme :: FIB_NUM2:sch 1 FibInd1 {P[set] } : for k being non zero Nat holds P[k] provided P[1] and P[2] and for k being non zero Nat st P[k] & P[k+1] holds P[k+2]; scheme :: FIB_NUM2:sch 2 FibInd2 {P[set] } : for k be non trivial Nat holds P[k] provided P[2] and P[3] and for k be non trivial Nat st P[k] & P[k+1] holds P[k+2]; theorem :: FIB_NUM2:21 Fib (2) = 1; theorem :: FIB_NUM2:22 Fib (3) = 2; theorem :: FIB_NUM2:23 Fib (4) = 3; theorem :: FIB_NUM2:24 for n being Nat holds Fib (n + 2) = Fib (n) + Fib (n + 1); theorem :: FIB_NUM2:25 for n being Nat holds Fib (n + 3) = Fib (n + 2) + Fib (n + 1); theorem :: FIB_NUM2:26 Fib (n + 4) = Fib (n + 2) + Fib (n + 3); theorem :: FIB_NUM2:27 Fib (n + 5) = Fib (n + 3) + Fib (n + 4); theorem :: FIB_NUM2:28 Fib (n + 2) = Fib (n + 3) - Fib (n + 1); theorem :: FIB_NUM2:29 for n being Nat holds Fib (n + 1) = Fib (n + 2) - Fib (n); theorem :: FIB_NUM2:30 Fib (n) = Fib (n+2) - Fib (n+1); begin :: Cassini's and Catalan's Identities theorem :: FIB_NUM2:31 Fib (n) * Fib (n+2) - (Fib (n+1)) ^2 = (-1) |^ (n+1); theorem :: FIB_NUM2:32 for n being non zero Element of NAT holds Fib (n-'1) * Fib (n+1) - ( Fib (n)) ^2 = (-1) |^n; theorem :: FIB_NUM2:33 tau > 0; theorem :: FIB_NUM2:34 tau_bar = (- tau) to_power (-1); theorem :: FIB_NUM2:35 (-tau) to_power ((-1) * n) = (-tau) to_power (-1) to_power n; theorem :: FIB_NUM2:36 - 1 / tau = tau_bar; theorem :: FIB_NUM2:37 (tau to_power r) ^2 - 2 * ((-1) to_power r) + (tau to_power (-r) ) ^2 = ((tau to_power r) - (tau_bar to_power r)) ^2; theorem :: FIB_NUM2:38 for n,r being non zero Element of NAT st r <= n holds (Fib (n)) ^2 - Fib (n+r) * Fib (n-'r) = ((-1) |^(n-'r)) * (Fib (r)) ^2; theorem :: FIB_NUM2:39 (Fib (n)) ^2 + (Fib (n+1)) ^2 = Fib (2*n + 1); theorem :: FIB_NUM2:40 for k being non zero Element of NAT holds Fib (n+k) = Fib (k) * Fib (n+1) + Fib (k-'1) * Fib (n); theorem :: FIB_NUM2:41 for n being non zero Element of NAT holds Fib (n) divides Fib ( n*k); theorem :: FIB_NUM2:42 for k being non zero Element of NAT holds k divides n implies Fib (k) divides Fib (n); theorem :: FIB_NUM2:43 Fib (n) <= Fib (n + 1); theorem :: FIB_NUM2:44 for n being Nat st n > 1 holds Fib (n) < Fib (n+1); theorem :: FIB_NUM2:45 for m, n st m >= n holds Fib(m) >= Fib(n); theorem :: FIB_NUM2:46 for k being Nat st k > 1 holds k < n implies Fib (k) < Fib (n); theorem :: FIB_NUM2:47 Fib (k) = 1 iff k = 1 or k = 2; theorem :: FIB_NUM2:48 for k,n being Element of NAT st n > 1 & k <> 0 & k <> 1 holds Fib (k) = Fib (n) iff k = n; theorem :: FIB_NUM2:49 for n being Element of NAT st n > 1 & n <> 4 holds n is non prime implies ex k being non zero Element of NAT st k <> 1 & k <> 2 & k <> n & k divides n; theorem :: FIB_NUM2:50 for n being Element of NAT st n > 1 & n <> 4 holds Fib (n) is prime implies n is prime; begin :: Sequence of Fibonacci Numbers definition func FIB -> sequence of NAT means :: FIB_NUM2:def 2 for k being Element of NAT holds it.k = Fib(k); end; definition func EvenNAT -> Subset of NAT equals :: FIB_NUM2:def 3 the set of all 2 * k where k is Nat ; func OddNAT -> Subset of NAT equals :: FIB_NUM2:def 4 the set of all 2 * k + 1 where k is Element of NAT ; end; theorem :: FIB_NUM2:51 for k being Nat holds 2 * k in EvenNAT & not 2 * k + 1 in EvenNAT; theorem :: FIB_NUM2:52 for k being Element of NAT holds 2 * k + 1 in OddNAT & not 2 * k in OddNAT; definition let n be Nat; func EvenFibs (n) -> FinSequence of NAT equals :: FIB_NUM2:def 5 Prefix (FIB, EvenNAT /\ Seg n); func OddFibs (n) -> FinSequence of NAT equals :: FIB_NUM2:def 6 Prefix (FIB, OddNAT /\ Seg n); end; theorem :: FIB_NUM2:53 EvenFibs (0) = {}; theorem :: FIB_NUM2:54 Seq (FIB| {2}) = <*1*>; theorem :: FIB_NUM2:55 EvenFibs (2) = <*1*>; theorem :: FIB_NUM2:56 EvenFibs (4) = <*1,3*>; theorem :: FIB_NUM2:57 for k being Nat holds (EvenNAT /\ Seg (2 * k + 2)) \/ {2 * k + 4} = EvenNAT /\ Seg (2 * k + 4); theorem :: FIB_NUM2:58 for k being Nat holds FIB | (EvenNAT /\ Seg (2 * k + 2)) \/ {[2*k+4,FIB.(2 * k + 4)]} = FIB | (EvenNAT /\ Seg (2 * k + 4)); theorem :: FIB_NUM2:59 for n being Element of NAT holds EvenFibs (2 * n + 2) = EvenFibs (2 * n) ^ <* Fib (2 * n + 2) *>; theorem :: FIB_NUM2:60 OddFibs (1) = <*1*>; theorem :: FIB_NUM2:61 OddFibs (3) = <*1,2*>; theorem :: FIB_NUM2:62 for k being Nat holds OddNAT /\ Seg (2 * k + 3) \/ {2 * k + 5} = OddNAT /\ Seg (2 * k + 5); theorem :: FIB_NUM2:63 for k being Nat holds (FIB | (OddNAT /\ Seg (2 * k + 3))) \/ {[2 *k+5,FIB.(2 * k + 5)]} = (FIB | (OddNAT /\ Seg (2 * k + 5))); theorem :: FIB_NUM2:64 for n being Nat holds OddFibs (2 * n + 3) = OddFibs (2 * n + 1) ^ <* Fib (2 * n + 3) *>; theorem :: FIB_NUM2:65 for n being Element of NAT holds Sum EvenFibs (2 * n + 2) = Fib (2 * n + 3) - 1; theorem :: FIB_NUM2:66 for n being Nat holds Sum OddFibs (2 * n + 1) = Fib (2 * n + 2); begin :: Carmichael's Theorem on Prime Divisors theorem :: FIB_NUM2:67 for n being Element of NAT holds Fib (n), Fib (n+1) are_coprime; theorem :: FIB_NUM2:68 for n being non zero Nat, m being Nat st m <> 1 holds m divides Fib (n) implies not m divides Fib (n-'1); ::$N Carmichael's Theorem on Prime Divisors theorem :: FIB_NUM2:69 for n being non zero Nat holds m is prime & n is prime & m divides Fib (n) implies for r being Nat st r < n & r <> 0 holds not m divides Fib (r) ; begin :: Fibonacci Numbers and Pythagorean Triples theorem :: FIB_NUM2:70 for n being non zero Element of NAT holds {Fib (n) * Fib (n+3), 2 * Fib (n+1) * Fib (n+2), (Fib (n+1)) ^2 + (Fib (n+2)) ^2} is Pythagorean_triple ;