Proof of Theorem fiblem
Step | Hyp | Ref
| Expression |
1 | | s2len 13484 |
. . . . . . 7
⊢
(#‘〈“01”〉) = 2 |
2 | 1 | eqcomi 2619 |
. . . . . 6
⊢ 2 =
(#‘〈“01”〉) |
3 | 2 | fveq2i 6106 |
. . . . 5
⊢
(ℤ≥‘2) =
(ℤ≥‘(#‘〈“01”〉)) |
4 | 3 | imaeq2i 5383 |
. . . 4
⊢ (◡# “ (ℤ≥‘2))
= (◡# “
(ℤ≥‘(#‘〈“01”〉))) |
5 | 4 | ineq2i 3773 |
. . 3
⊢ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘2))) = (Word ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) |
6 | | eqid 2610 |
. . 3
⊢ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))) = ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))) |
7 | 5, 6 | mpteq12i 4670 |
. 2
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))) = (𝑤 ∈ (Word ℕ0 ∩
(◡# “
(ℤ≥‘(#‘〈“01”〉)))) ↦
((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))) |
8 | | elin 3758 |
. . . . . 6
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) ↔
(𝑤 ∈ Word
ℕ0 ∧ 𝑤
∈ (◡# “
(ℤ≥‘(#‘〈“01”〉))))) |
9 | 8 | simplbi 475 |
. . . . 5
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
𝑤 ∈ Word
ℕ0) |
10 | | wrdf 13165 |
. . . . 5
⊢ (𝑤 ∈ Word ℕ0
→ 𝑤:(0..^(#‘𝑤))⟶ℕ0) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
𝑤:(0..^(#‘𝑤))⟶ℕ0) |
12 | 8 | simprbi 479 |
. . . . . . . . 9
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
𝑤 ∈ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) |
13 | | hashf 12987 |
. . . . . . . . . 10
⊢
#:V⟶(ℕ0 ∪ {+∞}) |
14 | | ffn 5958 |
. . . . . . . . . 10
⊢
(#:V⟶(ℕ0 ∪ {+∞}) → # Fn
V) |
15 | | elpreima 6245 |
. . . . . . . . . 10
⊢ (# Fn V
→ (𝑤 ∈ (◡# “
(ℤ≥‘(#‘〈“01”〉))) ↔
(𝑤 ∈ V ∧
(#‘𝑤) ∈
(ℤ≥‘(#‘〈“01”〉))))) |
16 | 13, 14, 15 | mp2b 10 |
. . . . . . . . 9
⊢ (𝑤 ∈ (◡# “
(ℤ≥‘(#‘〈“01”〉))) ↔
(𝑤 ∈ V ∧
(#‘𝑤) ∈
(ℤ≥‘(#‘〈“01”〉)))) |
17 | 12, 16 | sylib 207 |
. . . . . . . 8
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
(𝑤 ∈ V ∧
(#‘𝑤) ∈
(ℤ≥‘(#‘〈“01”〉)))) |
18 | 17 | simprd 478 |
. . . . . . 7
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
(#‘𝑤) ∈
(ℤ≥‘(#‘〈“01”〉))) |
19 | 18, 3 | syl6eleqr 2699 |
. . . . . 6
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
(#‘𝑤) ∈
(ℤ≥‘2)) |
20 | | uznn0sub 11595 |
. . . . . 6
⊢
((#‘𝑤) ∈
(ℤ≥‘2) → ((#‘𝑤) − 2) ∈
ℕ0) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
((#‘𝑤) − 2)
∈ ℕ0) |
22 | | 1zzd 11285 |
. . . . . . 7
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
1 ∈ ℤ) |
23 | | 1p1e2 11011 |
. . . . . . . . 9
⊢ (1 + 1) =
2 |
24 | 23 | fveq2i 6106 |
. . . . . . . 8
⊢
(ℤ≥‘(1 + 1)) =
(ℤ≥‘2) |
25 | 19, 24 | syl6eleqr 2699 |
. . . . . . 7
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
(#‘𝑤) ∈
(ℤ≥‘(1 + 1))) |
26 | | peano2uzr 11619 |
. . . . . . 7
⊢ ((1
∈ ℤ ∧ (#‘𝑤) ∈ (ℤ≥‘(1 +
1))) → (#‘𝑤)
∈ (ℤ≥‘1)) |
27 | 22, 25, 26 | syl2anc 691 |
. . . . . 6
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
(#‘𝑤) ∈
(ℤ≥‘1)) |
28 | | nnuz 11599 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
29 | 27, 28 | syl6eleqr 2699 |
. . . . 5
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
(#‘𝑤) ∈
ℕ) |
30 | 29 | nnred 10912 |
. . . . . 6
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
(#‘𝑤) ∈
ℝ) |
31 | | 2rp 11713 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
32 | 31 | a1i 11 |
. . . . . 6
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
2 ∈ ℝ+) |
33 | 30, 32 | ltsubrpd 11780 |
. . . . 5
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
((#‘𝑤) − 2)
< (#‘𝑤)) |
34 | | elfzo0 12376 |
. . . . 5
⊢
(((#‘𝑤)
− 2) ∈ (0..^(#‘𝑤)) ↔ (((#‘𝑤) − 2) ∈ ℕ0 ∧
(#‘𝑤) ∈ ℕ
∧ ((#‘𝑤) −
2) < (#‘𝑤))) |
35 | 21, 29, 33, 34 | syl3anbrc 1239 |
. . . 4
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
((#‘𝑤) − 2)
∈ (0..^(#‘𝑤))) |
36 | 11, 35 | ffvelrnd 6268 |
. . 3
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
(𝑤‘((#‘𝑤) − 2)) ∈
ℕ0) |
37 | | fzo0end 12426 |
. . . . 5
⊢
((#‘𝑤) ∈
ℕ → ((#‘𝑤)
− 1) ∈ (0..^(#‘𝑤))) |
38 | 29, 37 | syl 17 |
. . . 4
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
((#‘𝑤) − 1)
∈ (0..^(#‘𝑤))) |
39 | 11, 38 | ffvelrnd 6268 |
. . 3
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
(𝑤‘((#‘𝑤) − 1)) ∈
ℕ0) |
40 | 36, 39 | nn0addcld 11232 |
. 2
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘(#‘〈“01”〉)))) →
((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1))) ∈
ℕ0) |
41 | 7, 40 | fmpti 6291 |
1
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡# “
(ℤ≥‘2))) ↦ ((𝑤‘((#‘𝑤) − 2)) + (𝑤‘((#‘𝑤) − 1)))):(Word ℕ0
∩ (◡# “
(ℤ≥‘(#‘〈“01”〉))))⟶ℕ0 |