Proof of Theorem iwrdsplit
Step | Hyp | Ref
| Expression |
1 | | iwrdsplit.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ V) |
2 | | iwrdsplit.f |
. . . 4
⊢ (𝜑 → 𝐹:ℕ0⟶𝑆) |
3 | | iwrdsplit.n |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
4 | | 1nn0 11308 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
5 | 4 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℕ0) |
6 | 3, 5 | nn0addcld 11355 |
. . . 4
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
7 | 1, 2, 6 | subiwrd 30447 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (0..^(𝑁 + 1))) ∈ Word 𝑆) |
8 | | 1re 10039 |
. . . . . 6
⊢ 1 ∈
ℝ |
9 | | nn0addge2 11340 |
. . . . . 6
⊢ ((1
∈ ℝ ∧ 𝑁
∈ ℕ0) → 1 ≤ (𝑁 + 1)) |
10 | 8, 3, 9 | sylancr 695 |
. . . . 5
⊢ (𝜑 → 1 ≤ (𝑁 + 1)) |
11 | 1, 2, 6 | subiwrdlen 30448 |
. . . . 5
⊢ (𝜑 → (#‘(𝐹 ↾ (0..^(𝑁 + 1)))) = (𝑁 + 1)) |
12 | 10, 11 | breqtrrd 4681 |
. . . 4
⊢ (𝜑 → 1 ≤ (#‘(𝐹 ↾ (0..^(𝑁 + 1))))) |
13 | | wrdlenge1n0 13340 |
. . . . 5
⊢ ((𝐹 ↾ (0..^(𝑁 + 1))) ∈ Word 𝑆 → ((𝐹 ↾ (0..^(𝑁 + 1))) ≠ ∅ ↔ 1 ≤
(#‘(𝐹 ↾
(0..^(𝑁 +
1)))))) |
14 | 7, 13 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ (0..^(𝑁 + 1))) ≠ ∅ ↔ 1 ≤
(#‘(𝐹 ↾
(0..^(𝑁 +
1)))))) |
15 | 12, 14 | mpbird 247 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (0..^(𝑁 + 1))) ≠ ∅) |
16 | | swrdccatwrd 13468 |
. . 3
⊢ (((𝐹 ↾ (0..^(𝑁 + 1))) ∈ Word 𝑆 ∧ (𝐹 ↾ (0..^(𝑁 + 1))) ≠ ∅) → (((𝐹 ↾ (0..^(𝑁 + 1))) substr 〈0, ((#‘(𝐹 ↾ (0..^(𝑁 + 1)))) − 1)〉) ++ 〈“(
lastS ‘(𝐹 ↾
(0..^(𝑁 +
1))))”〉) = (𝐹
↾ (0..^(𝑁 +
1)))) |
17 | 7, 15, 16 | syl2anc 693 |
. 2
⊢ (𝜑 → (((𝐹 ↾ (0..^(𝑁 + 1))) substr 〈0, ((#‘(𝐹 ↾ (0..^(𝑁 + 1)))) − 1)〉) ++ 〈“(
lastS ‘(𝐹 ↾
(0..^(𝑁 +
1))))”〉) = (𝐹
↾ (0..^(𝑁 +
1)))) |
18 | 11 | oveq1d 6665 |
. . . . . . 7
⊢ (𝜑 → ((#‘(𝐹 ↾ (0..^(𝑁 + 1)))) − 1) = ((𝑁 + 1) − 1)) |
19 | 3 | nn0cnd 11353 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℂ) |
20 | | 1cnd 10056 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℂ) |
21 | 19, 20 | pncand 10393 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
22 | 18, 21 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → ((#‘(𝐹 ↾ (0..^(𝑁 + 1)))) − 1) = 𝑁) |
23 | 22 | opeq2d 4409 |
. . . . 5
⊢ (𝜑 → 〈0, ((#‘(𝐹 ↾ (0..^(𝑁 + 1)))) − 1)〉 = 〈0, 𝑁〉) |
24 | 23 | oveq2d 6666 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ (0..^(𝑁 + 1))) substr 〈0, ((#‘(𝐹 ↾ (0..^(𝑁 + 1)))) − 1)〉) = ((𝐹 ↾ (0..^(𝑁 + 1))) substr 〈0, 𝑁〉)) |
25 | | nn0fz0 12437 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈ (0...𝑁)) |
26 | 3, 25 | sylib 208 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) |
27 | | elfz0add 12438 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 1 ∈ ℕ0) → (𝑁 ∈ (0...𝑁) → 𝑁 ∈ (0...(𝑁 + 1)))) |
28 | 27 | imp 445 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 1 ∈ ℕ0) ∧ 𝑁 ∈ (0...𝑁)) → 𝑁 ∈ (0...(𝑁 + 1))) |
29 | 3, 5, 26, 28 | syl21anc 1325 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (0...(𝑁 + 1))) |
30 | 11 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → (0...(#‘(𝐹 ↾ (0..^(𝑁 + 1))))) = (0...(𝑁 + 1))) |
31 | 29, 30 | eleqtrrd 2704 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (0...(#‘(𝐹 ↾ (0..^(𝑁 + 1)))))) |
32 | | swrd0val 13421 |
. . . . 5
⊢ (((𝐹 ↾ (0..^(𝑁 + 1))) ∈ Word 𝑆 ∧ 𝑁 ∈ (0...(#‘(𝐹 ↾ (0..^(𝑁 + 1)))))) → ((𝐹 ↾ (0..^(𝑁 + 1))) substr 〈0, 𝑁〉) = ((𝐹 ↾ (0..^(𝑁 + 1))) ↾ (0..^𝑁))) |
33 | 7, 31, 32 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ (0..^(𝑁 + 1))) substr 〈0, 𝑁〉) = ((𝐹 ↾ (0..^(𝑁 + 1))) ↾ (0..^𝑁))) |
34 | | fzossfzop1 12545 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (0..^𝑁) ⊆
(0..^(𝑁 +
1))) |
35 | | resabs1 5427 |
. . . . 5
⊢
((0..^𝑁) ⊆
(0..^(𝑁 + 1)) →
((𝐹 ↾ (0..^(𝑁 + 1))) ↾ (0..^𝑁)) = (𝐹 ↾ (0..^𝑁))) |
36 | 3, 34, 35 | 3syl 18 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ (0..^(𝑁 + 1))) ↾ (0..^𝑁)) = (𝐹 ↾ (0..^𝑁))) |
37 | 24, 33, 36 | 3eqtrd 2660 |
. . 3
⊢ (𝜑 → ((𝐹 ↾ (0..^(𝑁 + 1))) substr 〈0, ((#‘(𝐹 ↾ (0..^(𝑁 + 1)))) − 1)〉) = (𝐹 ↾ (0..^𝑁))) |
38 | | lsw 13351 |
. . . . . 6
⊢ ((𝐹 ↾ (0..^(𝑁 + 1))) ∈ Word 𝑆 → ( lastS ‘(𝐹 ↾ (0..^(𝑁 + 1)))) = ((𝐹 ↾ (0..^(𝑁 + 1)))‘((#‘(𝐹 ↾ (0..^(𝑁 + 1)))) − 1))) |
39 | 7, 38 | syl 17 |
. . . . 5
⊢ (𝜑 → ( lastS ‘(𝐹 ↾ (0..^(𝑁 + 1)))) = ((𝐹 ↾ (0..^(𝑁 + 1)))‘((#‘(𝐹 ↾ (0..^(𝑁 + 1)))) − 1))) |
40 | 22 | fveq2d 6195 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ (0..^(𝑁 + 1)))‘((#‘(𝐹 ↾ (0..^(𝑁 + 1)))) − 1)) = ((𝐹 ↾ (0..^(𝑁 + 1)))‘𝑁)) |
41 | | fzonn0p1 12544 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0..^(𝑁 + 1))) |
42 | | fvres 6207 |
. . . . . 6
⊢ (𝑁 ∈ (0..^(𝑁 + 1)) → ((𝐹 ↾ (0..^(𝑁 + 1)))‘𝑁) = (𝐹‘𝑁)) |
43 | 3, 41, 42 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ (0..^(𝑁 + 1)))‘𝑁) = (𝐹‘𝑁)) |
44 | 39, 40, 43 | 3eqtrd 2660 |
. . . 4
⊢ (𝜑 → ( lastS ‘(𝐹 ↾ (0..^(𝑁 + 1)))) = (𝐹‘𝑁)) |
45 | 44 | s1eqd 13381 |
. . 3
⊢ (𝜑 → 〈“( lastS
‘(𝐹 ↾
(0..^(𝑁 +
1))))”〉 = 〈“(𝐹‘𝑁)”〉) |
46 | 37, 45 | oveq12d 6668 |
. 2
⊢ (𝜑 → (((𝐹 ↾ (0..^(𝑁 + 1))) substr 〈0, ((#‘(𝐹 ↾ (0..^(𝑁 + 1)))) − 1)〉) ++ 〈“(
lastS ‘(𝐹 ↾
(0..^(𝑁 +
1))))”〉) = ((𝐹
↾ (0..^𝑁)) ++
〈“(𝐹‘𝑁)”〉)) |
47 | 17, 46 | eqtr3d 2658 |
1
⊢ (𝜑 → (𝐹 ↾ (0..^(𝑁 + 1))) = ((𝐹 ↾ (0..^𝑁)) ++ 〈“(𝐹‘𝑁)”〉)) |