Proof of Theorem fiblem
| Step | Hyp | Ref
| Expression |
| 1 | | s2len 14928 |
. . . . . . 7
⊢
(♯‘〈“01”〉) = 2 |
| 2 | 1 | eqcomi 2746 |
. . . . . 6
⊢ 2 =
(♯‘〈“01”〉) |
| 3 | 2 | fveq2i 6909 |
. . . . 5
⊢
(ℤ≥‘2) =
(ℤ≥‘(♯‘〈“01”〉)) |
| 4 | 3 | imaeq2i 6076 |
. . . 4
⊢ (◡♯ “
(ℤ≥‘2)) = (◡♯ “
(ℤ≥‘(♯‘〈“01”〉))) |
| 5 | 4 | ineq2i 4217 |
. . 3
⊢ (Word
ℕ0 ∩ (◡♯
“ (ℤ≥‘2))) = (Word ℕ0 ∩
(◡♯ “
(ℤ≥‘(♯‘〈“01”〉)))) |
| 6 | | eqid 2737 |
. . 3
⊢ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))) = ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))) |
| 7 | 5, 6 | mpteq12i 5248 |
. 2
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“ (ℤ≥‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))) = (𝑤 ∈ (Word ℕ0 ∩
(◡♯ “
(ℤ≥‘(♯‘〈“01”〉))))
↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))) |
| 8 | | elin 3967 |
. . . . . 6
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
↔ (𝑤 ∈ Word
ℕ0 ∧ 𝑤
∈ (◡♯ “
(ℤ≥‘(♯‘〈“01”〉))))) |
| 9 | 8 | simplbi 497 |
. . . . 5
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ 𝑤 ∈ Word
ℕ0) |
| 10 | | wrdf 14557 |
. . . . 5
⊢ (𝑤 ∈ Word ℕ0
→ 𝑤:(0..^(♯‘𝑤))⟶ℕ0) |
| 11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ 𝑤:(0..^(♯‘𝑤))⟶ℕ0) |
| 12 | 8 | simprbi 496 |
. . . . . . . . 9
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ 𝑤 ∈ (◡♯ “
(ℤ≥‘(♯‘〈“01”〉)))) |
| 13 | | hashf 14377 |
. . . . . . . . . 10
⊢
♯:V⟶(ℕ0 ∪ {+∞}) |
| 14 | | ffn 6736 |
. . . . . . . . . 10
⊢
(♯:V⟶(ℕ0 ∪ {+∞}) → ♯
Fn V) |
| 15 | | elpreima 7078 |
. . . . . . . . . 10
⊢ (♯
Fn V → (𝑤 ∈
(◡♯ “
(ℤ≥‘(♯‘〈“01”〉)))
↔ (𝑤 ∈ V ∧
(♯‘𝑤) ∈
(ℤ≥‘(♯‘〈“01”〉))))) |
| 16 | 13, 14, 15 | mp2b 10 |
. . . . . . . . 9
⊢ (𝑤 ∈ (◡♯ “
(ℤ≥‘(♯‘〈“01”〉)))
↔ (𝑤 ∈ V ∧
(♯‘𝑤) ∈
(ℤ≥‘(♯‘〈“01”〉)))) |
| 17 | 12, 16 | sylib 218 |
. . . . . . . 8
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ (𝑤 ∈ V ∧
(♯‘𝑤) ∈
(ℤ≥‘(♯‘〈“01”〉)))) |
| 18 | 17 | simprd 495 |
. . . . . . 7
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ (♯‘𝑤)
∈
(ℤ≥‘(♯‘〈“01”〉))) |
| 19 | 18, 3 | eleqtrrdi 2852 |
. . . . . 6
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ (♯‘𝑤)
∈ (ℤ≥‘2)) |
| 20 | | uznn0sub 12917 |
. . . . . 6
⊢
((♯‘𝑤)
∈ (ℤ≥‘2) → ((♯‘𝑤) − 2) ∈
ℕ0) |
| 21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ ((♯‘𝑤)
− 2) ∈ ℕ0) |
| 22 | | 1zzd 12648 |
. . . . . . 7
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ 1 ∈ ℤ) |
| 23 | | 1p1e2 12391 |
. . . . . . . . 9
⊢ (1 + 1) =
2 |
| 24 | 23 | fveq2i 6909 |
. . . . . . . 8
⊢
(ℤ≥‘(1 + 1)) =
(ℤ≥‘2) |
| 25 | 19, 24 | eleqtrrdi 2852 |
. . . . . . 7
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ (♯‘𝑤)
∈ (ℤ≥‘(1 + 1))) |
| 26 | | peano2uzr 12945 |
. . . . . . 7
⊢ ((1
∈ ℤ ∧ (♯‘𝑤) ∈ (ℤ≥‘(1 +
1))) → (♯‘𝑤) ∈
(ℤ≥‘1)) |
| 27 | 22, 25, 26 | syl2anc 584 |
. . . . . 6
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ (♯‘𝑤)
∈ (ℤ≥‘1)) |
| 28 | | nnuz 12921 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
| 29 | 27, 28 | eleqtrrdi 2852 |
. . . . 5
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ (♯‘𝑤)
∈ ℕ) |
| 30 | 29 | nnred 12281 |
. . . . . 6
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ (♯‘𝑤)
∈ ℝ) |
| 31 | | 2rp 13039 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
| 32 | 31 | a1i 11 |
. . . . . 6
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ 2 ∈ ℝ+) |
| 33 | 30, 32 | ltsubrpd 13109 |
. . . . 5
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ ((♯‘𝑤)
− 2) < (♯‘𝑤)) |
| 34 | | elfzo0 13740 |
. . . . 5
⊢
(((♯‘𝑤)
− 2) ∈ (0..^(♯‘𝑤)) ↔ (((♯‘𝑤) − 2) ∈ ℕ0 ∧
(♯‘𝑤) ∈
ℕ ∧ ((♯‘𝑤) − 2) < (♯‘𝑤))) |
| 35 | 21, 29, 33, 34 | syl3anbrc 1344 |
. . . 4
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ ((♯‘𝑤)
− 2) ∈ (0..^(♯‘𝑤))) |
| 36 | 11, 35 | ffvelcdmd 7105 |
. . 3
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ (𝑤‘((♯‘𝑤) − 2)) ∈
ℕ0) |
| 37 | | fzo0end 13797 |
. . . . 5
⊢
((♯‘𝑤)
∈ ℕ → ((♯‘𝑤) − 1) ∈ (0..^(♯‘𝑤))) |
| 38 | 29, 37 | syl 17 |
. . . 4
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ ((♯‘𝑤)
− 1) ∈ (0..^(♯‘𝑤))) |
| 39 | 11, 38 | ffvelcdmd 7105 |
. . 3
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ (𝑤‘((♯‘𝑤) − 1)) ∈
ℕ0) |
| 40 | 36, 39 | nn0addcld 12591 |
. 2
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“
(ℤ≥‘(♯‘〈“01”〉))))
→ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1))) ∈
ℕ0) |
| 41 | 7, 40 | fmpti 7132 |
1
⊢ (𝑤 ∈ (Word
ℕ0 ∩ (◡♯
“ (ℤ≥‘2))) ↦ ((𝑤‘((♯‘𝑤) − 2)) + (𝑤‘((♯‘𝑤) − 1)))):(Word ℕ0
∩ (◡♯ “
(ℤ≥‘(♯‘〈“01”〉))))⟶ℕ0 |