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 ( 𝑁 ∈ ℕ → ( Fibci ‘ ( 𝑁 + 1 ) ) = ( ( Fibci ‘ ( 𝑁 − 1 ) ) + ( Fibci ‘ 𝑁 ) ) )

Proof

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