Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fibp1 Structured version   Visualization version   GIF version

Theorem fibp1 31767
Description: Value of the Fibonacci sequence at higher indices. (Contributed by Thierry Arnoux, 25-Apr-2019.)
Assertion
Ref Expression
fibp1 (𝑁 ∈ ℕ → (Fibci‘(𝑁 + 1)) = ((Fibci‘(𝑁 − 1)) + (Fibci‘𝑁)))

Proof of Theorem fibp1
Dummy variables 𝑤 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-fib 31763 . . . 4 Fibci = (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))))
21fveq1i 6650 . . 3 (Fibci‘(𝑁 + 1)) = ((⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))))‘(𝑁 + 1))
32a1i 11 . 2 (𝑁 ∈ ℕ → (Fibci‘(𝑁 + 1)) = ((⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))))‘(𝑁 + 1)))
4 nn0ex 11895 . . . 4 0 ∈ V
54a1i 11 . . 3 (𝑁 ∈ ℕ → ℕ0 ∈ V)
6 0nn0 11904 . . . . 5 0 ∈ ℕ0
76a1i 11 . . . 4 (𝑁 ∈ ℕ → 0 ∈ ℕ0)
8 1nn0 11905 . . . . 5 1 ∈ ℕ0
98a1i 11 . . . 4 (𝑁 ∈ ℕ → 1 ∈ ℕ0)
107, 9s2cld 14228 . . 3 (𝑁 ∈ ℕ → ⟨“01”⟩ ∈ Word ℕ0)
11 eqid 2801 . . 3 (Word ℕ0 ∩ (♯ “ (ℤ‘(♯‘⟨“01”⟩)))) = (Word ℕ0 ∩ (♯ “ (ℤ‘(♯‘⟨“01”⟩))))
12 fiblem 31764 . . . 4 (𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))):(Word ℕ0 ∩ (♯ “ (ℤ‘(♯‘⟨“01”⟩))))⟶ℕ0
1312a1i 11 . . 3 (𝑁 ∈ ℕ → (𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))):(Word ℕ0 ∩ (♯ “ (ℤ‘(♯‘⟨“01”⟩))))⟶ℕ0)
14 eluzp1p1 12262 . . . . 5 (𝑁 ∈ (ℤ‘1) → (𝑁 + 1) ∈ (ℤ‘(1 + 1)))
15 nnuz 12273 . . . . 5 ℕ = (ℤ‘1)
1614, 15eleq2s 2911 . . . 4 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ (ℤ‘(1 + 1)))
17 s2len 14246 . . . . . 6 (♯‘⟨“01”⟩) = 2
18 1p1e2 11754 . . . . . 6 (1 + 1) = 2
1917, 18eqtr4i 2827 . . . . 5 (♯‘⟨“01”⟩) = (1 + 1)
2019fveq2i 6652 . . . 4 (ℤ‘(♯‘⟨“01”⟩)) = (ℤ‘(1 + 1))
2116, 20eleqtrrdi 2904 . . 3 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ (ℤ‘(♯‘⟨“01”⟩)))
225, 10, 11, 13, 21sseqp1 31761 . 2 (𝑁 ∈ ℕ → ((⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))))‘(𝑁 + 1)) = ((𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))‘((⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))))
23 id 22 . . . . . . 7 (𝑤 = 𝑡𝑤 = 𝑡)
24 fveq2 6649 . . . . . . . 8 (𝑤 = 𝑡 → (♯‘𝑤) = (♯‘𝑡))
2524oveq1d 7154 . . . . . . 7 (𝑤 = 𝑡 → ((♯‘𝑤) − 2) = ((♯‘𝑡) − 2))
2623, 25fveq12d 6656 . . . . . 6 (𝑤 = 𝑡 → (𝑤‘((♯‘𝑤) − 2)) = (𝑡‘((♯‘𝑡) − 2)))
2724oveq1d 7154 . . . . . . 7 (𝑤 = 𝑡 → ((♯‘𝑤) − 1) = ((♯‘𝑡) − 1))
2823, 27fveq12d 6656 . . . . . 6 (𝑤 = 𝑡 → (𝑤‘((♯‘𝑤) − 1)) = (𝑡‘((♯‘𝑡) − 1)))
2926, 28oveq12d 7157 . . . . 5 (𝑤 = 𝑡 → ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))) = ((𝑡‘((♯‘𝑡) − 2)) + (𝑡‘((♯‘𝑡) − 1))))
3029cbvmptv 5136 . . . 4 (𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))) = (𝑡 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑡‘((♯‘𝑡) − 2)) + (𝑡‘((♯‘𝑡) − 1))))
3130a1i 11 . . 3 (𝑁 ∈ ℕ → (𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))) = (𝑡 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑡‘((♯‘𝑡) − 2)) + (𝑡‘((♯‘𝑡) − 1)))))
32 simpr 488 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑡 = ((⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) → 𝑡 = ((⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1))))
331a1i 11 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑡 = ((⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) → Fibci = (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))))
3433reseq1d 5821 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑡 = ((⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) → (Fibci ↾ (0..^(𝑁 + 1))) = ((⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1))))
3532, 34eqtr4d 2839 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑡 = ((⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) → 𝑡 = (Fibci ↾ (0..^(𝑁 + 1))))
36 simpr 488 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → 𝑡 = (Fibci ↾ (0..^(𝑁 + 1))))
3736fveq2d 6653 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (♯‘𝑡) = (♯‘(Fibci ↾ (0..^(𝑁 + 1)))))
385, 10, 11, 13sseqf 31758 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))):ℕ0⟶ℕ0)
391a1i 11 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → Fibci = (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))))
4039feq1d 6476 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (Fibci:ℕ0⟶ℕ0 ↔ (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))):ℕ0⟶ℕ0))
4138, 40mpbird 260 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → Fibci:ℕ0⟶ℕ0)
42 nnnn0 11896 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
4342, 9nn0addcld 11951 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ0)
445, 41, 43subiwrdlen 31752 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (♯‘(Fibci ↾ (0..^(𝑁 + 1)))) = (𝑁 + 1))
4544adantr 484 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (♯‘(Fibci ↾ (0..^(𝑁 + 1)))) = (𝑁 + 1))
4637, 45eqtrd 2836 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (♯‘𝑡) = (𝑁 + 1))
4746oveq1d 7154 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((♯‘𝑡) − 2) = ((𝑁 + 1) − 2))
48 nncn 11637 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
49 1cnd 10629 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 1 ∈ ℂ)
50 2cnd 11707 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 2 ∈ ℂ)
5148, 49, 50addsubassd 11010 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((𝑁 + 1) − 2) = (𝑁 + (1 − 2)))
5248, 50, 49subsub2d 11019 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑁 − (2 − 1)) = (𝑁 + (1 − 2)))
53 2m1e1 11755 . . . . . . . . . . . 12 (2 − 1) = 1
5453oveq2i 7150 . . . . . . . . . . 11 (𝑁 − (2 − 1)) = (𝑁 − 1)
5554a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑁 − (2 − 1)) = (𝑁 − 1))
5651, 52, 553eqtr2d 2842 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑁 + 1) − 2) = (𝑁 − 1))
5756adantr 484 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((𝑁 + 1) − 2) = (𝑁 − 1))
5847, 57eqtrd 2836 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((♯‘𝑡) − 2) = (𝑁 − 1))
5958fveq2d 6653 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (𝑡‘((♯‘𝑡) − 2)) = (𝑡‘(𝑁 − 1)))
6036fveq1d 6651 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (𝑡‘(𝑁 − 1)) = ((Fibci ↾ (0..^(𝑁 + 1)))‘(𝑁 − 1)))
61 nnm1nn0 11930 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
62 peano2nn 11641 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
63 nnre 11636 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
64 2re 11703 . . . . . . . . . . . . 13 2 ∈ ℝ
6564a1i 11 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 2 ∈ ℝ)
6663, 65readdcld 10663 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 + 2) ∈ ℝ)
67 1red 10635 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 1 ∈ ℝ)
68 2rp 12386 . . . . . . . . . . . . 13 2 ∈ ℝ+
6968a1i 11 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 2 ∈ ℝ+)
7063, 69ltaddrpd 12456 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 2))
7163, 66, 67, 70ltsub1dd 11245 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑁 − 1) < ((𝑁 + 2) − 1))
7248, 50, 49addsubassd 11010 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((𝑁 + 2) − 1) = (𝑁 + (2 − 1)))
7353oveq2i 7150 . . . . . . . . . . 11 (𝑁 + (2 − 1)) = (𝑁 + 1)
7472, 73eqtrdi 2852 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((𝑁 + 2) − 1) = (𝑁 + 1))
7571, 74breqtrd 5059 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 − 1) < (𝑁 + 1))
76 elfzo0 13077 . . . . . . . . 9 ((𝑁 − 1) ∈ (0..^(𝑁 + 1)) ↔ ((𝑁 − 1) ∈ ℕ0 ∧ (𝑁 + 1) ∈ ℕ ∧ (𝑁 − 1) < (𝑁 + 1)))
7761, 62, 75, 76syl3anbrc 1340 . . . . . . . 8 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^(𝑁 + 1)))
7877adantr 484 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (𝑁 − 1) ∈ (0..^(𝑁 + 1)))
79 fvres 6668 . . . . . . 7 ((𝑁 − 1) ∈ (0..^(𝑁 + 1)) → ((Fibci ↾ (0..^(𝑁 + 1)))‘(𝑁 − 1)) = (Fibci‘(𝑁 − 1)))
8078, 79syl 17 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((Fibci ↾ (0..^(𝑁 + 1)))‘(𝑁 − 1)) = (Fibci‘(𝑁 − 1)))
8159, 60, 803eqtrd 2840 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (𝑡‘((♯‘𝑡) − 2)) = (Fibci‘(𝑁 − 1)))
8246oveq1d 7154 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((♯‘𝑡) − 1) = ((𝑁 + 1) − 1))
83 simpl 486 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → 𝑁 ∈ ℕ)
8483nncnd 11645 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → 𝑁 ∈ ℂ)
85 1cnd 10629 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → 1 ∈ ℂ)
8684, 85pncand 10991 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((𝑁 + 1) − 1) = 𝑁)
8782, 86eqtrd 2836 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((♯‘𝑡) − 1) = 𝑁)
8887fveq2d 6653 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (𝑡‘((♯‘𝑡) − 1)) = (𝑡𝑁))
8936fveq1d 6651 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (𝑡𝑁) = ((Fibci ↾ (0..^(𝑁 + 1)))‘𝑁))
90 nn0fz0 13004 . . . . . . . . . 10 (𝑁 ∈ ℕ0𝑁 ∈ (0...𝑁))
9142, 90sylib 221 . . . . . . . . 9 (𝑁 ∈ ℕ → 𝑁 ∈ (0...𝑁))
92 nnz 11996 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
93 fzval3 13105 . . . . . . . . . 10 (𝑁 ∈ ℤ → (0...𝑁) = (0..^(𝑁 + 1)))
9492, 93syl 17 . . . . . . . . 9 (𝑁 ∈ ℕ → (0...𝑁) = (0..^(𝑁 + 1)))
9591, 94eleqtrd 2895 . . . . . . . 8 (𝑁 ∈ ℕ → 𝑁 ∈ (0..^(𝑁 + 1)))
9695adantr 484 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → 𝑁 ∈ (0..^(𝑁 + 1)))
97 fvres 6668 . . . . . . 7 (𝑁 ∈ (0..^(𝑁 + 1)) → ((Fibci ↾ (0..^(𝑁 + 1)))‘𝑁) = (Fibci‘𝑁))
9896, 97syl 17 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((Fibci ↾ (0..^(𝑁 + 1)))‘𝑁) = (Fibci‘𝑁))
9988, 89, 983eqtrd 2840 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (𝑡‘((♯‘𝑡) − 1)) = (Fibci‘𝑁))
10081, 99oveq12d 7157 . . . 4 ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((𝑡‘((♯‘𝑡) − 2)) + (𝑡‘((♯‘𝑡) − 1))) = ((Fibci‘(𝑁 − 1)) + (Fibci‘𝑁)))
10135, 100syldan 594 . . 3 ((𝑁 ∈ ℕ ∧ 𝑡 = ((⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) → ((𝑡‘((♯‘𝑡) − 2)) + (𝑡‘((♯‘𝑡) − 1))) = ((Fibci‘(𝑁 − 1)) + (Fibci‘𝑁)))
10239reseq1d 5821 . . . 4 (𝑁 ∈ ℕ → (Fibci ↾ (0..^(𝑁 + 1))) = ((⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1))))
1035, 41, 43subiwrd 31751 . . . . 5 (𝑁 ∈ ℕ → (Fibci ↾ (0..^(𝑁 + 1))) ∈ Word ℕ0)
104 ovex 7172 . . . . . . . . 9 (⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))) ∈ V
1051, 104eqeltri 2889 . . . . . . . 8 Fibci ∈ V
106105resex 5870 . . . . . . 7 (Fibci ↾ (0..^(𝑁 + 1))) ∈ V
107106a1i 11 . . . . . 6 (𝑁 ∈ ℕ → (Fibci ↾ (0..^(𝑁 + 1))) ∈ V)
10818fveq2i 6652 . . . . . . . 8 (ℤ‘(1 + 1)) = (ℤ‘2)
10916, 108eleqtrdi 2903 . . . . . . 7 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ (ℤ‘2))
11044, 109eqeltrd 2893 . . . . . 6 (𝑁 ∈ ℕ → (♯‘(Fibci ↾ (0..^(𝑁 + 1)))) ∈ (ℤ‘2))
111 hashf 13698 . . . . . . 7 ♯:V⟶(ℕ0 ∪ {+∞})
112 ffn 6491 . . . . . . 7 (♯:V⟶(ℕ0 ∪ {+∞}) → ♯ Fn V)
113 elpreima 6809 . . . . . . 7 (♯ Fn V → ((Fibci ↾ (0..^(𝑁 + 1))) ∈ (♯ “ (ℤ‘2)) ↔ ((Fibci ↾ (0..^(𝑁 + 1))) ∈ V ∧ (♯‘(Fibci ↾ (0..^(𝑁 + 1)))) ∈ (ℤ‘2))))
114111, 112, 113mp2b 10 . . . . . 6 ((Fibci ↾ (0..^(𝑁 + 1))) ∈ (♯ “ (ℤ‘2)) ↔ ((Fibci ↾ (0..^(𝑁 + 1))) ∈ V ∧ (♯‘(Fibci ↾ (0..^(𝑁 + 1)))) ∈ (ℤ‘2)))
115107, 110, 114sylanbrc 586 . . . . 5 (𝑁 ∈ ℕ → (Fibci ↾ (0..^(𝑁 + 1))) ∈ (♯ “ (ℤ‘2)))
116103, 115elind 4124 . . . 4 (𝑁 ∈ ℕ → (Fibci ↾ (0..^(𝑁 + 1))) ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))))
117102, 116eqeltrrd 2894 . . 3 (𝑁 ∈ ℕ → ((⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1))) ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))))
118 ovex 7172 . . . 4 ((Fibci‘(𝑁 − 1)) + (Fibci‘𝑁)) ∈ V
119118a1i 11 . . 3 (𝑁 ∈ ℕ → ((Fibci‘(𝑁 − 1)) + (Fibci‘𝑁)) ∈ V)
12031, 101, 117, 119fvmptd 6756 . 2 (𝑁 ∈ ℕ → ((𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))‘((⟨“01”⟩seqstr(𝑤 ∈ (Word ℕ0 ∩ (♯ “ (ℤ‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) = ((Fibci‘(𝑁 − 1)) + (Fibci‘𝑁)))
1213, 22, 1203eqtrd 2840 1 (𝑁 ∈ ℕ → (Fibci‘(𝑁 + 1)) = ((Fibci‘(𝑁 − 1)) + (Fibci‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2112  Vcvv 3444  cun 3882  cin 3883  {csn 4528   class class class wbr 5033  cmpt 5113  ccnv 5522  cres 5525  cima 5526   Fn wfn 6323  wf 6324  cfv 6328  (class class class)co 7139  cr 10529  0cc0 10530  1c1 10531   + caddc 10533  +∞cpnf 10665   < clt 10668  cmin 10863  cn 11629  2c2 11684  0cn0 11889  cz 11973  cuz 12235  +crp 12381  ...cfz 12889  ..^cfzo 13032  chash 13690  Word cword 13861  ⟨“cs2 14198  seqstrcsseq 31749  Fibcicfib 31762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-map 8395  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-nn 11630  df-2 11692  df-n0 11890  df-xnn0 11960  df-z 11974  df-uz 12236  df-rp 12382  df-fz 12890  df-fzo 13033  df-seq 13369  df-hash 13691  df-word 13862  df-lsw 13910  df-concat 13918  df-s1 13945  df-substr 13998  df-pfx 14028  df-s2 14205  df-sseq 31750  df-fib 31763
This theorem is referenced by:  fib2  31768  fib3  31769  fib4  31770  fib5  31771  fib6  31772
  Copyright terms: Public domain W3C validator