Step | Hyp | Ref
| Expression |
1 | | df-fib 29786 |
. . . 4
⊢ Fibci =
(〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))) |
2 | 1 | fveq1i 6104 |
. . 3
⊢
(Fibci‘(𝑁 +
1)) = ((〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))))‘(𝑁 + 1)) |
3 | 2 | a1i 11 |
. 2
⊢ (𝑁 ∈ ℕ →
(Fibci‘(𝑁 + 1)) =
((〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))))‘(𝑁 + 1))) |
4 | | nn0ex 11175 |
. . . 4
⊢
ℕ0 ∈ V |
5 | 4 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ →
ℕ0 ∈ V) |
6 | | 0nn0 11184 |
. . . . 5
⊢ 0 ∈
ℕ0 |
7 | 6 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℕ → 0 ∈
ℕ0) |
8 | | 1nn0 11185 |
. . . . 5
⊢ 1 ∈
ℕ0 |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝑁 ∈ ℕ → 1 ∈
ℕ0) |
10 | 7, 9 | s2cld 13466 |
. . 3
⊢ (𝑁 ∈ ℕ →
〈“01”〉 ∈ Word ℕ0) |
11 | | eqid 2610 |
. . 3
⊢ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) = (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) |
12 | | fiblem 29787 |
. . . 4
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))):(Word ℕ0
∩ (◡# “
(ℤ≥‘(#‘〈“01”〉))))⟶ℕ0 |
13 | 12 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))):(Word ℕ0
∩ (◡# “
(ℤ≥‘(#‘〈“01”〉))))⟶ℕ0) |
14 | | eluzp1p1 11589 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘1) → (𝑁 + 1) ∈
(ℤ≥‘(1 + 1))) |
15 | | nnuz 11599 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
16 | 14, 15 | eleq2s 2706 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
(ℤ≥‘(1 + 1))) |
17 | | s2len 13484 |
. . . . . 6
⊢
(#‘〈“01”〉) = 2 |
18 | | 1p1e2 11011 |
. . . . . 6
⊢ (1 + 1) =
2 |
19 | 17, 18 | eqtr4i 2635 |
. . . . 5
⊢
(#‘〈“01”〉) = (1 + 1) |
20 | 19 | fveq2i 6106 |
. . . 4
⊢
(ℤ≥‘(#‘〈“01”〉)) =
(ℤ≥‘(1 + 1)) |
21 | 16, 20 | syl6eleqr 2699 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
(ℤ≥‘(#‘〈“01”〉))) |
22 | 5, 10, 11, 13, 21 | sseqp1 29784 |
. 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 6103 |
. . . . . . . 8
⊢ (𝑤 = 𝑡 → (#‘𝑤) = (#‘𝑡)) |
25 | 24 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → ((#‘𝑤) − 2) = ((#‘𝑡) − 2)) |
26 | 23, 25 | fveq12d 6109 |
. . . . . 6
⊢ (𝑤 = 𝑡 → (𝑤‘((#‘𝑤) − 2)) = (𝑡‘((#‘𝑡) − 2))) |
27 | 24 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑤 = 𝑡 → ((#‘𝑤) − 1) = ((#‘𝑡) − 1)) |
28 | 23, 27 | fveq12d 6109 |
. . . . . 6
⊢ (𝑤 = 𝑡 → (𝑤‘((#‘𝑤) − 1)) = (𝑡‘((#‘𝑡) − 1))) |
29 | 26, 28 | oveq12d 6567 |
. . . . 5
⊢ (𝑤 = 𝑡 → ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))) = ((𝑡‘((#‘𝑡) − 2)) + (𝑡‘((#‘𝑡) − 1)))) |
30 | 29 | cbvmptv 4678 |
. . . 4
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))) = (𝑡 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑡‘((#‘𝑡) − 2)) + (𝑡‘((#‘𝑡) − 1)))) |
31 | 30 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))) = (𝑡 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑡‘((#‘𝑡) − 2)) + (𝑡‘((#‘𝑡) − 1))))) |
32 | | simpr 476 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 =
((〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) → 𝑡 =
((〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) |
33 | 1 | a1i 11 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 =
((〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) → Fibci =
(〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))))) |
34 | 33 | reseq1d 5316 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 =
((〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) → (Fibci ↾
(0..^(𝑁 + 1))) =
((〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) |
35 | 32, 34 | eqtr4d 2647 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 =
((〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) → 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) |
36 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) |
37 | 36 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (#‘𝑡) = (#‘(Fibci ↾
(0..^(𝑁 +
1))))) |
38 | 5, 10, 11, 13 | sseqf 29781 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
(〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) −
1))))):ℕ0⟶ℕ0) |
39 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → Fibci =
(〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))))) |
40 | 39 | feq1d 5943 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
(Fibci:ℕ0⟶ℕ0 ↔
(〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) −
1))))):ℕ0⟶ℕ0)) |
41 | 38, 40 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
Fibci:ℕ0⟶ℕ0) |
42 | | nnnn0 11176 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
43 | 42, 9 | nn0addcld 11232 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ0) |
44 | 5, 41, 43 | subiwrdlen 29775 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(#‘(Fibci ↾ (0..^(𝑁 + 1)))) = (𝑁 + 1)) |
45 | 44 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (#‘(Fibci
↾ (0..^(𝑁 + 1)))) =
(𝑁 + 1)) |
46 | 37, 45 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (#‘𝑡) = (𝑁 + 1)) |
47 | 46 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((#‘𝑡) − 2) = ((𝑁 + 1) −
2)) |
48 | | nncn 10905 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
49 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
50 | | 2cnd 10970 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) |
51 | 48, 49, 50 | addsubassd 10291 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 2) = (𝑁 + (1 −
2))) |
52 | 48, 50, 49 | subsub2d 10300 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 − (2 − 1)) = (𝑁 + (1 −
2))) |
53 | | 2m1e1 11012 |
. . . . . . . . . . . 12
⊢ (2
− 1) = 1 |
54 | 53 | oveq2i 6560 |
. . . . . . . . . . 11
⊢ (𝑁 − (2 − 1)) = (𝑁 − 1) |
55 | 54 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 − (2 − 1)) = (𝑁 − 1)) |
56 | 51, 52, 55 | 3eqtr2d 2650 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 2) = (𝑁 − 1)) |
57 | 56 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((𝑁 + 1) − 2) = (𝑁 − 1)) |
58 | 47, 57 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((#‘𝑡) − 2) = (𝑁 − 1)) |
59 | 58 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (𝑡‘((#‘𝑡) − 2)) = (𝑡‘(𝑁 − 1))) |
60 | 36 | fveq1d 6105 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (𝑡‘(𝑁 − 1)) = ((Fibci ↾ (0..^(𝑁 + 1)))‘(𝑁 − 1))) |
61 | | nnm1nn0 11211 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
62 | | peano2nn 10909 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) |
63 | | nnre 10904 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
64 | | 2re 10967 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
65 | 64 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ) |
66 | 63, 65 | readdcld 9948 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 + 2) ∈
ℝ) |
67 | | 1red 9934 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) |
68 | | 2rp 11713 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ+ |
69 | 68 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 2 ∈
ℝ+) |
70 | 63, 69 | ltaddrpd 11781 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 2)) |
71 | 63, 66, 67, 70 | ltsub1dd 10518 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < ((𝑁 + 2) −
1)) |
72 | 48, 50, 49 | addsubassd 10291 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((𝑁 + 2) − 1) = (𝑁 + (2 −
1))) |
73 | 53 | oveq2i 6560 |
. . . . . . . . . . 11
⊢ (𝑁 + (2 − 1)) = (𝑁 + 1) |
74 | 72, 73 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((𝑁 + 2) − 1) = (𝑁 + 1)) |
75 | 71, 74 | breqtrd 4609 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < (𝑁 + 1)) |
76 | | elfzo0 12376 |
. . . . . . . . 9
⊢ ((𝑁 − 1) ∈ (0..^(𝑁 + 1)) ↔ ((𝑁 − 1) ∈
ℕ0 ∧ (𝑁 + 1) ∈ ℕ ∧ (𝑁 − 1) < (𝑁 + 1))) |
77 | 61, 62, 75, 76 | syl3anbrc 1239 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (0..^(𝑁 + 1))) |
78 | 77 | adantr 480 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (𝑁 − 1) ∈ (0..^(𝑁 + 1))) |
79 | | fvres 6117 |
. . . . . . 7
⊢ ((𝑁 − 1) ∈ (0..^(𝑁 + 1)) → ((Fibci ↾
(0..^(𝑁 + 1)))‘(𝑁 − 1)) =
(Fibci‘(𝑁 −
1))) |
80 | 78, 79 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((Fibci ↾
(0..^(𝑁 + 1)))‘(𝑁 − 1)) =
(Fibci‘(𝑁 −
1))) |
81 | 59, 60, 80 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (𝑡‘((#‘𝑡) − 2)) =
(Fibci‘(𝑁 −
1))) |
82 | 46 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((#‘𝑡) − 1) = ((𝑁 + 1) −
1)) |
83 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → 𝑁 ∈
ℕ) |
84 | 83 | nncnd 10913 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → 𝑁 ∈
ℂ) |
85 | | 1cnd 9935 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → 1 ∈
ℂ) |
86 | 84, 85 | pncand 10272 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((𝑁 + 1) − 1) = 𝑁) |
87 | 82, 86 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((#‘𝑡) − 1) = 𝑁) |
88 | 87 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (𝑡‘((#‘𝑡) − 1)) = (𝑡‘𝑁)) |
89 | 36 | fveq1d 6105 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (𝑡‘𝑁) = ((Fibci ↾ (0..^(𝑁 + 1)))‘𝑁)) |
90 | | nn0fz0 12306 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈ (0...𝑁)) |
91 | 42, 90 | sylib 207 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (0...𝑁)) |
92 | | nnz 11276 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
93 | | fzval3 12404 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ →
(0...𝑁) = (0..^(𝑁 + 1))) |
94 | 92, 93 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(0...𝑁) = (0..^(𝑁 + 1))) |
95 | 91, 94 | eleqtrd 2690 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (0..^(𝑁 + 1))) |
96 | 95 | adantr 480 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → 𝑁 ∈ (0..^(𝑁 + 1))) |
97 | | fvres 6117 |
. . . . . . 7
⊢ (𝑁 ∈ (0..^(𝑁 + 1)) → ((Fibci ↾ (0..^(𝑁 + 1)))‘𝑁) = (Fibci‘𝑁)) |
98 | 96, 97 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((Fibci ↾
(0..^(𝑁 + 1)))‘𝑁) = (Fibci‘𝑁)) |
99 | 88, 89, 98 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → (𝑡‘((#‘𝑡) − 1)) =
(Fibci‘𝑁)) |
100 | 81, 99 | oveq12d 6567 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 = (Fibci ↾ (0..^(𝑁 + 1)))) → ((𝑡‘((#‘𝑡) − 2)) + (𝑡‘((#‘𝑡) − 1))) =
((Fibci‘(𝑁 −
1)) + (Fibci‘𝑁))) |
101 | 35, 100 | syldan 486 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑡 =
((〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) → ((𝑡‘((#‘𝑡) − 2)) + (𝑡‘((#‘𝑡) − 1))) =
((Fibci‘(𝑁 −
1)) + (Fibci‘𝑁))) |
102 | 39 | reseq1d 5316 |
. . . 4
⊢ (𝑁 ∈ ℕ → (Fibci
↾ (0..^(𝑁 + 1))) =
((〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) |
103 | 5, 41, 43 | subiwrd 29774 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (Fibci
↾ (0..^(𝑁 + 1)))
∈ Word ℕ0) |
104 | | ovex 6577 |
. . . . . . . . 9
⊢
(〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))) ∈ V |
105 | 1, 104 | eqeltri 2684 |
. . . . . . . 8
⊢ Fibci
∈ V |
106 | 105 | resex 5363 |
. . . . . . 7
⊢ (Fibci
↾ (0..^(𝑁 + 1)))
∈ V |
107 | 106 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (Fibci
↾ (0..^(𝑁 + 1)))
∈ V) |
108 | 18 | fveq2i 6106 |
. . . . . . . 8
⊢
(ℤ≥‘(1 + 1)) =
(ℤ≥‘2) |
109 | 16, 108 | syl6eleq 2698 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
(ℤ≥‘2)) |
110 | 44, 109 | eqeltrd 2688 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(#‘(Fibci ↾ (0..^(𝑁 + 1)))) ∈
(ℤ≥‘2)) |
111 | | hashf 12987 |
. . . . . . 7
⊢
#:V⟶(ℕ0 ∪ {+∞}) |
112 | | ffn 5958 |
. . . . . . 7
⊢
(#:V⟶(ℕ0 ∪ {+∞}) → # Fn
V) |
113 | | elpreima 6245 |
. . . . . . 7
⊢ (# Fn V
→ ((Fibci ↾ (0..^(𝑁 + 1))) ∈ (◡# “ (ℤ≥‘2))
↔ ((Fibci ↾ (0..^(𝑁 + 1))) ∈ V ∧ (#‘(Fibci
↾ (0..^(𝑁 + 1))))
∈ (ℤ≥‘2)))) |
114 | 111, 112,
113 | mp2b 10 |
. . . . . 6
⊢ ((Fibci
↾ (0..^(𝑁 + 1)))
∈ (◡# “
(ℤ≥‘2)) ↔ ((Fibci ↾ (0..^(𝑁 + 1))) ∈ V ∧
(#‘(Fibci ↾ (0..^(𝑁 + 1)))) ∈
(ℤ≥‘2))) |
115 | 107, 110,
114 | sylanbrc 695 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (Fibci
↾ (0..^(𝑁 + 1)))
∈ (◡# “
(ℤ≥‘2))) |
116 | 103, 115 | elind 3760 |
. . . 4
⊢ (𝑁 ∈ ℕ → (Fibci
↾ (0..^(𝑁 + 1)))
∈ (Word ℕ0 ∩ (◡# “
(ℤ≥‘2)))) |
117 | 102, 116 | eqeltrrd 2689 |
. . 3
⊢ (𝑁 ∈ ℕ →
((〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1))) ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘2)))) |
118 | | ovex 6577 |
. . . 4
⊢
((Fibci‘(𝑁
− 1)) + (Fibci‘𝑁)) ∈ V |
119 | 118 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ →
((Fibci‘(𝑁 −
1)) + (Fibci‘𝑁))
∈ V) |
120 | 31, 101, 117, 119 | fvmptd 6197 |
. 2
⊢ (𝑁 ∈ ℕ → ((𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) −
1))))‘((〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))) ↾ (0..^(𝑁 + 1)))) = ((Fibci‘(𝑁 − 1)) +
(Fibci‘𝑁))) |
121 | 3, 22, 120 | 3eqtrd 2648 |
1
⊢ (𝑁 ∈ ℕ →
(Fibci‘(𝑁 + 1)) =
((Fibci‘(𝑁 −
1)) + (Fibci‘𝑁))) |