Detailed syntax breakdown of Definition df-fib
Step | Hyp | Ref
| Expression |
1 | | cfib 29785 |
. 2
class
Fibci |
2 | | cc0 9815 |
. . . 4
class
0 |
3 | | c1 9816 |
. . . 4
class
1 |
4 | 2, 3 | cs2 13437 |
. . 3
class
〈“01”〉 |
5 | | vw |
. . . 4
setvar 𝑤 |
6 | | cn0 11169 |
. . . . . 6
class
ℕ0 |
7 | 6 | cword 13146 |
. . . . 5
class Word
ℕ0 |
8 | | chash 12979 |
. . . . . . 7
class
# |
9 | 8 | ccnv 5037 |
. . . . . 6
class ◡# |
10 | | c2 10947 |
. . . . . . 7
class
2 |
11 | | cuz 11563 |
. . . . . . 7
class
ℤ≥ |
12 | 10, 11 | cfv 5804 |
. . . . . 6
class
(ℤ≥‘2) |
13 | 9, 12 | cima 5041 |
. . . . 5
class (◡# “
(ℤ≥‘2)) |
14 | 7, 13 | cin 3539 |
. . . 4
class (Word
ℕ0 ∩ (◡# “
(ℤ≥‘2))) |
15 | 5 | cv 1474 |
. . . . . . . 8
class 𝑤 |
16 | 15, 8 | cfv 5804 |
. . . . . . 7
class
(#‘𝑤) |
17 | | cmin 10145 |
. . . . . . 7
class
− |
18 | 16, 10, 17 | co 6549 |
. . . . . 6
class
((#‘𝑤) −
2) |
19 | 18, 15 | cfv 5804 |
. . . . 5
class (𝑤‘((#‘𝑤) − 2)) |
20 | 16, 3, 17 | co 6549 |
. . . . . 6
class
((#‘𝑤) −
1) |
21 | 20, 15 | cfv 5804 |
. . . . 5
class (𝑤‘((#‘𝑤) − 1)) |
22 | | caddc 9818 |
. . . . 5
class
+ |
23 | 19, 21, 22 | co 6549 |
. . . 4
class ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))) |
24 | 5, 14, 23 | cmpt 4643 |
. . 3
class (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))) |
25 | | csseq 29772 |
. . 3
class
seqstr |
26 | 4, 24, 25 | co 6549 |
. 2
class
(〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))) |
27 | 1, 26 | wceq 1475 |
1
wff Fibci =
(〈“01”〉seqstr(𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))))) |