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=⟨“01”⟩seqstrw∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1
2 1 fveq1i ⊢Fibci⁡N+1=⟨“01”⟩seqstrw∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1⁡N+1
3 2 a1i ⊢N∈ℕ→Fibci⁡N+1=⟨“01”⟩seqstrw∈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∈ℕ→⟨“01”⟩∈Wordℕ0
11 eqid ⊢Wordℕ0∩.-1ℤ≥⟨“01”⟩=Wordℕ0∩.-1ℤ≥⟨“01”⟩
12 fiblem ⊢w∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1:Wordℕ0∩.-1ℤ≥⟨“01”⟩⟶ℕ0
13 12 a1i ⊢N∈ℕ→w∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1:Wordℕ0∩.-1ℤ≥⟨“01”⟩⟶ℕ0
14 eluzp1p1 ⊢N∈ℤ≥1→N+1∈ℤ≥1+1
15 nnuz ⊢ℕ=ℤ≥1
16 14 15 eleq2s ⊢N∈ℕ→N+1∈ℤ≥1+1
17 s2len ⊢⟨“01”⟩=2
18 1p1e2 ⊢1+1=2
19 17 18 eqtr4i ⊢⟨“01”⟩=1+1
20 19 fveq2i ⊢ℤ≥⟨“01”⟩=ℤ≥1+1
21 16 20 eleqtrrdi ⊢N∈ℕ→N+1∈ℤ≥⟨“01”⟩
22 5 10 11 13 21 sseqp1 ⊢N∈ℕ→⟨“01”⟩seqstrw∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1⁡N+1=w∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1⁡⟨“01”⟩seqstrw∈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=⟨“01”⟩seqstrw∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1↾0..^N+1→t=⟨“01”⟩seqstrw∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1↾0..^N+1
33 1 a1i ⊢N∈ℕ∧t=⟨“01”⟩seqstrw∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1↾0..^N+1→Fibci=⟨“01”⟩seqstrw∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1
34 33 reseq1d ⊢N∈ℕ∧t=⟨“01”⟩seqstrw∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1↾0..^N+1→Fibci↾0..^N+1=⟨“01”⟩seqstrw∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1↾0..^N+1
35 32 34 eqtr4d ⊢N∈ℕ∧t=⟨“01”⟩seqstrw∈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∈ℕ→⟨“01”⟩seqstrw∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1:ℕ0⟶ℕ0
39 1 a1i ⊢N∈ℕ→Fibci=⟨“01”⟩seqstrw∈Wordℕ0∩.-1ℤ≥2⟼w⁡w−2+w⁡w−1
40 39 feq1d ⊢N∈ℕ→Fibci:ℕ0⟶ℕ0↔⟨“01”⟩seqstrw∈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=⟨“01”⟩seqstrw∈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=⟨“01”⟩seqstrw∈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 ⊢⟨“01”⟩seqstrw∈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∪+∞→.FnV
113 elpreima ⊢.FnV→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∈ℕ→⟨“01”⟩seqstrw∈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⁡⟨“01”⟩seqstrw∈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