Metamath Proof Explorer

Theorem fibp1

Description: Value of the Fibonacci sequence at higher indices. (Contributed by Thierry Arnoux, 25-Apr-2019)

Ref Expression
Assertion fibp1 ⊢ N ∈ ℕ → Fibci ⁡ N + 1 = Fibci ⁡ N − 1 + Fibci ⁡ N

Proof

Step Hyp Ref Expression
1 df-fib ⊢ Fibci = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1
2 1 fveq1i ⊢ Fibci ⁡ N + 1 = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ⁡ N + 1
3 2 a1i ⊢ N ∈ ℕ → Fibci ⁡ N + 1 = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ⁡ N + 1
4 nn0ex ⊢ ℕ 0 ∈ V
5 4 a1i ⊢ N ∈ ℕ → ℕ 0 ∈ V
6 0nn0 ⊢ 0 ∈ ℕ 0
7 6 a1i ⊢ N ∈ ℕ → 0 ∈ ℕ 0
8 1nn0 ⊢ 1 ∈ ℕ 0
9 8 a1i ⊢ N ∈ ℕ → 1 ∈ ℕ 0
10 7 9 s2cld ⊢ N ∈ ℕ → ⟨“ 0 1 ”⟩ ∈ Word ℕ 0
11 eqid ⊢ Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ = Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩
12 fiblem ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 : Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ ⟶ ℕ 0
13 12 a1i ⊢ N ∈ ℕ → w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 : Word ℕ 0 ∩ . -1 ℤ ≥ ⟨“ 0 1 ”⟩ ⟶ ℕ 0
14 eluzp1p1 ⊢ N ∈ ℤ ≥ 1 → N + 1 ∈ ℤ ≥ 1 + 1
15 nnuz ⊢ ℕ = ℤ ≥ 1
16 14 15 eleq2s ⊢ N ∈ ℕ → N + 1 ∈ ℤ ≥ 1 + 1
17 s2len ⊢ ⟨“ 0 1 ”⟩ = 2
18 1p1e2 ⊢ 1 + 1 = 2
19 17 18 eqtr4i ⊢ ⟨“ 0 1 ”⟩ = 1 + 1
20 19 fveq2i ⊢ ℤ ≥ ⟨“ 0 1 ”⟩ = ℤ ≥ 1 + 1
21 16 20 eleqtrrdi ⊢ N ∈ ℕ → N + 1 ∈ ℤ ≥ ⟨“ 0 1 ”⟩
22 5 10 11 13 21 sseqp1 ⊢ N ∈ ℕ → ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ⁡ N + 1 = w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ⁡ ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ↾ 0 ..^ N + 1
23 id ⊢ w = t → w = t
24 fveq2 ⊢ w = t → w = t
25 24 oveq1d ⊢ w = t → w − 2 = t − 2
26 23 25 fveq12d ⊢ w = t → w ⁡ w − 2 = t ⁡ t − 2
27 24 oveq1d ⊢ w = t → w − 1 = t − 1
28 23 27 fveq12d ⊢ w = t → w ⁡ w − 1 = t ⁡ t − 1
29 26 28 oveq12d ⊢ w = t → w ⁡ w − 2 + w ⁡ w − 1 = t ⁡ t − 2 + t ⁡ t − 1
30 29 cbvmptv ⊢ w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 = t ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ t ⁡ t − 2 + t ⁡ t − 1
31 30 a1i ⊢ N ∈ ℕ → w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 = t ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ t ⁡ t − 2 + t ⁡ t − 1
32 simpr ⊢ N ∈ ℕ ∧ t = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ↾ 0 ..^ N + 1 → t = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ↾ 0 ..^ N + 1
33 1 a1i ⊢ N ∈ ℕ ∧ t = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ↾ 0 ..^ N + 1 → Fibci = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1
34 33 reseq1d ⊢ N ∈ ℕ ∧ t = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ↾ 0 ..^ N + 1 → Fibci ↾ 0 ..^ N + 1 = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ↾ 0 ..^ N + 1
35 32 34 eqtr4d ⊢ N ∈ ℕ ∧ t = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ↾ 0 ..^ N + 1 → t = Fibci ↾ 0 ..^ N + 1
36 simpr ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → t = Fibci ↾ 0 ..^ N + 1
37 36 fveq2d ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → t = Fibci ↾ 0 ..^ N + 1
38 5 10 11 13 sseqf ⊢ N ∈ ℕ → ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 : ℕ 0 ⟶ ℕ 0
39 1 a1i ⊢ N ∈ ℕ → Fibci = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1
40 39 feq1d ⊢ N ∈ ℕ → Fibci : ℕ 0 ⟶ ℕ 0 ↔ ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 : ℕ 0 ⟶ ℕ 0
41 38 40 mpbird ⊢ N ∈ ℕ → Fibci : ℕ 0 ⟶ ℕ 0
42 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
43 42 9 nn0addcld ⊢ N ∈ ℕ → N + 1 ∈ ℕ 0
44 5 41 43 subiwrdlen ⊢ N ∈ ℕ → Fibci ↾ 0 ..^ N + 1 = N + 1
45 44 adantr ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → Fibci ↾ 0 ..^ N + 1 = N + 1
46 37 45 eqtrd ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → t = N + 1
47 46 oveq1d ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → t − 2 = N + 1 - 2
48 nncn ⊢ N ∈ ℕ → N ∈ ℂ
49 1cnd ⊢ N ∈ ℕ → 1 ∈ ℂ
50 2cnd ⊢ N ∈ ℕ → 2 ∈ ℂ
51 48 49 50 addsubassd ⊢ N ∈ ℕ → N + 1 - 2 = N + 1 - 2
52 48 50 49 subsub2d ⊢ N ∈ ℕ → N − 2 − 1 = N + 1 - 2
53 2m1e1 ⊢ 2 − 1 = 1
54 53 oveq2i ⊢ N − 2 − 1 = N − 1
55 54 a1i ⊢ N ∈ ℕ → N − 2 − 1 = N − 1
56 51 52 55 3eqtr2d ⊢ N ∈ ℕ → N + 1 - 2 = N − 1
57 56 adantr ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → N + 1 - 2 = N − 1
58 47 57 eqtrd ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → t − 2 = N − 1
59 58 fveq2d ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → t ⁡ t − 2 = t ⁡ N − 1
60 36 fveq1d ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → t ⁡ N − 1 = Fibci ↾ 0 ..^ N + 1 ⁡ N − 1
61 nnm1nn0 ⊢ N ∈ ℕ → N − 1 ∈ ℕ 0
62 peano2nn ⊢ N ∈ ℕ → N + 1 ∈ ℕ
63 nnre ⊢ N ∈ ℕ → N ∈ ℝ
64 2re ⊢ 2 ∈ ℝ
65 64 a1i ⊢ N ∈ ℕ → 2 ∈ ℝ
66 63 65 readdcld ⊢ N ∈ ℕ → N + 2 ∈ ℝ
67 1red ⊢ N ∈ ℕ → 1 ∈ ℝ
68 2rp ⊢ 2 ∈ ℝ +
69 68 a1i ⊢ N ∈ ℕ → 2 ∈ ℝ +
70 63 69 ltaddrpd ⊢ N ∈ ℕ → N < N + 2
71 63 66 67 70 ltsub1dd ⊢ N ∈ ℕ → N − 1 < N + 2 - 1
72 48 50 49 addsubassd ⊢ N ∈ ℕ → N + 2 - 1 = N + 2 - 1
73 53 oveq2i ⊢ N + 2 - 1 = N + 1
74 72 73 eqtrdi ⊢ N ∈ ℕ → N + 2 - 1 = N + 1
75 71 74 breqtrd ⊢ N ∈ ℕ → N − 1 < N + 1
76 elfzo0 ⊢ N − 1 ∈ 0 ..^ N + 1 ↔ N − 1 ∈ ℕ 0 ∧ N + 1 ∈ ℕ ∧ N − 1 < N + 1
77 61 62 75 76 syl3anbrc ⊢ N ∈ ℕ → N − 1 ∈ 0 ..^ N + 1
78 77 adantr ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → N − 1 ∈ 0 ..^ N + 1
79 fvres ⊢ N − 1 ∈ 0 ..^ N + 1 → Fibci ↾ 0 ..^ N + 1 ⁡ N − 1 = Fibci ⁡ N − 1
80 78 79 syl ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → Fibci ↾ 0 ..^ N + 1 ⁡ N − 1 = Fibci ⁡ N − 1
81 59 60 80 3eqtrd ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → t ⁡ t − 2 = Fibci ⁡ N − 1
82 46 oveq1d ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → t − 1 = N + 1 - 1
83 simpl ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → N ∈ ℕ
84 83 nncnd ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → N ∈ ℂ
85 1cnd ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → 1 ∈ ℂ
86 84 85 pncand ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → N + 1 - 1 = N
87 82 86 eqtrd ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → t − 1 = N
88 87 fveq2d ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → t ⁡ t − 1 = t ⁡ N
89 36 fveq1d ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → t ⁡ N = Fibci ↾ 0 ..^ N + 1 ⁡ N
90 nn0fz0 ⊢ N ∈ ℕ 0 ↔ N ∈ 0 … N
91 42 90 sylib ⊢ N ∈ ℕ → N ∈ 0 … N
92 nnz ⊢ N ∈ ℕ → N ∈ ℤ
93 fzval3 ⊢ N ∈ ℤ → 0 … N = 0 ..^ N + 1
94 92 93 syl ⊢ N ∈ ℕ → 0 … N = 0 ..^ N + 1
95 91 94 eleqtrd ⊢ N ∈ ℕ → N ∈ 0 ..^ N + 1
96 95 adantr ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → N ∈ 0 ..^ N + 1
97 fvres ⊢ N ∈ 0 ..^ N + 1 → Fibci ↾ 0 ..^ N + 1 ⁡ N = Fibci ⁡ N
98 96 97 syl ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → Fibci ↾ 0 ..^ N + 1 ⁡ N = Fibci ⁡ N
99 88 89 98 3eqtrd ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → t ⁡ t − 1 = Fibci ⁡ N
100 81 99 oveq12d ⊢ N ∈ ℕ ∧ t = Fibci ↾ 0 ..^ N + 1 → t ⁡ t − 2 + t ⁡ t − 1 = Fibci ⁡ N − 1 + Fibci ⁡ N
101 35 100 syldan ⊢ N ∈ ℕ ∧ t = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ↾ 0 ..^ N + 1 → t ⁡ t − 2 + t ⁡ t − 1 = Fibci ⁡ N − 1 + Fibci ⁡ N
102 39 reseq1d ⊢ N ∈ ℕ → Fibci ↾ 0 ..^ N + 1 = ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ↾ 0 ..^ N + 1
103 5 41 43 subiwrd ⊢ N ∈ ℕ → Fibci ↾ 0 ..^ N + 1 ∈ Word ℕ 0
104 ovex ⊢ ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ∈ V
105 1 104 eqeltri ⊢ Fibci ∈ V
106 105 resex ⊢ Fibci ↾ 0 ..^ N + 1 ∈ V
107 106 a1i ⊢ N ∈ ℕ → Fibci ↾ 0 ..^ N + 1 ∈ V
108 18 fveq2i ⊢ ℤ ≥ 1 + 1 = ℤ ≥ 2
109 16 108 eleqtrdi ⊢ N ∈ ℕ → N + 1 ∈ ℤ ≥ 2
110 44 109 eqeltrd ⊢ N ∈ ℕ → Fibci ↾ 0 ..^ N + 1 ∈ ℤ ≥ 2
111 hashf ⊢ . : V ⟶ ℕ 0 ∪ +∞
112 ffn ⊢ . : V ⟶ ℕ 0 ∪ +∞ → . Fn V
113 elpreima ⊢ . Fn V → Fibci ↾ 0 ..^ N + 1 ∈ . -1 ℤ ≥ 2 ↔ Fibci ↾ 0 ..^ N + 1 ∈ V ∧ Fibci ↾ 0 ..^ N + 1 ∈ ℤ ≥ 2
114 111 112 113 mp2b ⊢ Fibci ↾ 0 ..^ N + 1 ∈ . -1 ℤ ≥ 2 ↔ Fibci ↾ 0 ..^ N + 1 ∈ V ∧ Fibci ↾ 0 ..^ N + 1 ∈ ℤ ≥ 2
115 107 110 114 sylanbrc ⊢ N ∈ ℕ → Fibci ↾ 0 ..^ N + 1 ∈ . -1 ℤ ≥ 2
116 103 115 elind ⊢ N ∈ ℕ → Fibci ↾ 0 ..^ N + 1 ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2
117 102 116 eqeltrrd ⊢ N ∈ ℕ → ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ↾ 0 ..^ N + 1 ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2
118 ovex ⊢ Fibci ⁡ N − 1 + Fibci ⁡ N ∈ V
119 118 a1i ⊢ N ∈ ℕ → Fibci ⁡ N − 1 + Fibci ⁡ N ∈ V
120 31 101 117 119 fvmptd ⊢ N ∈ ℕ → w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ⁡ ⟨“ 0 1 ”⟩ seq str w ∈ Word ℕ 0 ∩ . -1 ℤ ≥ 2 ⟼ w ⁡ w − 2 + w ⁡ w − 1 ↾ 0 ..^ N + 1 = Fibci ⁡ N − 1 + Fibci ⁡ N
121 3 22 120 3eqtrd ⊢ N ∈ ℕ → Fibci ⁡ N + 1 = Fibci ⁡ N − 1 + Fibci ⁡ N