Proof of Theorem swrds1
Step | Hyp | Ref
| Expression |
1 | | swrdcl 13419 |
. . . 4
⊢ (𝑊 ∈ Word 𝐴 → (𝑊 substr 〈𝐼, (𝐼 + 1)〉) ∈ Word 𝐴) |
2 | 1 | adantr 481 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑊 substr 〈𝐼, (𝐼 + 1)〉) ∈ Word 𝐴) |
3 | | simpl 473 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → 𝑊 ∈ Word 𝐴) |
4 | | elfzouz 12474 |
. . . . . . 7
⊢ (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ∈
(ℤ≥‘0)) |
5 | 4 | adantl 482 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → 𝐼 ∈
(ℤ≥‘0)) |
6 | | elfzoelz 12470 |
. . . . . . . 8
⊢ (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ∈ ℤ) |
7 | 6 | adantl 482 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → 𝐼 ∈ ℤ) |
8 | | uzid 11702 |
. . . . . . 7
⊢ (𝐼 ∈ ℤ → 𝐼 ∈
(ℤ≥‘𝐼)) |
9 | | peano2uz 11741 |
. . . . . . 7
⊢ (𝐼 ∈
(ℤ≥‘𝐼) → (𝐼 + 1) ∈
(ℤ≥‘𝐼)) |
10 | 7, 8, 9 | 3syl 18 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝐼 + 1) ∈
(ℤ≥‘𝐼)) |
11 | | elfzuzb 12336 |
. . . . . 6
⊢ (𝐼 ∈ (0...(𝐼 + 1)) ↔ (𝐼 ∈ (ℤ≥‘0)
∧ (𝐼 + 1) ∈
(ℤ≥‘𝐼))) |
12 | 5, 10, 11 | sylanbrc 698 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → 𝐼 ∈ (0...(𝐼 + 1))) |
13 | | fzofzp1 12565 |
. . . . . 6
⊢ (𝐼 ∈ (0..^(#‘𝑊)) → (𝐼 + 1) ∈ (0...(#‘𝑊))) |
14 | 13 | adantl 482 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝐼 + 1) ∈ (0...(#‘𝑊))) |
15 | | swrdlen 13423 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0...(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (0...(#‘𝑊))) → (#‘(𝑊 substr 〈𝐼, (𝐼 + 1)〉)) = ((𝐼 + 1) − 𝐼)) |
16 | 3, 12, 14, 15 | syl3anc 1326 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (#‘(𝑊 substr 〈𝐼, (𝐼 + 1)〉)) = ((𝐼 + 1) − 𝐼)) |
17 | 7 | zcnd 11483 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → 𝐼 ∈ ℂ) |
18 | | ax-1cn 9994 |
. . . . 5
⊢ 1 ∈
ℂ |
19 | | pncan2 10288 |
. . . . 5
⊢ ((𝐼 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐼 + 1)
− 𝐼) =
1) |
20 | 17, 18, 19 | sylancl 694 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝐼 + 1) − 𝐼) = 1) |
21 | 16, 20 | eqtrd 2656 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (#‘(𝑊 substr 〈𝐼, (𝐼 + 1)〉)) = 1) |
22 | | eqs1 13392 |
. . 3
⊢ (((𝑊 substr 〈𝐼, (𝐼 + 1)〉) ∈ Word 𝐴 ∧ (#‘(𝑊 substr 〈𝐼, (𝐼 + 1)〉)) = 1) → (𝑊 substr 〈𝐼, (𝐼 + 1)〉) = 〈“((𝑊 substr 〈𝐼, (𝐼 +
1)〉)‘0)”〉) |
23 | 2, 21, 22 | syl2anc 693 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑊 substr 〈𝐼, (𝐼 + 1)〉) = 〈“((𝑊 substr 〈𝐼, (𝐼 +
1)〉)‘0)”〉) |
24 | | 0z 11388 |
. . . . . . 7
⊢ 0 ∈
ℤ |
25 | | snidg 4206 |
. . . . . . 7
⊢ (0 ∈
ℤ → 0 ∈ {0}) |
26 | 24, 25 | ax-mp 5 |
. . . . . 6
⊢ 0 ∈
{0} |
27 | 20 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (0..^((𝐼 + 1) − 𝐼)) = (0..^1)) |
28 | | fzo01 12550 |
. . . . . . 7
⊢ (0..^1) =
{0} |
29 | 27, 28 | syl6eq 2672 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (0..^((𝐼 + 1) − 𝐼)) = {0}) |
30 | 26, 29 | syl5eleqr 2708 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → 0 ∈ (0..^((𝐼 + 1) − 𝐼))) |
31 | | swrdfv 13424 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0...(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (0...(#‘𝑊))) ∧ 0 ∈ (0..^((𝐼 + 1) − 𝐼))) → ((𝑊 substr 〈𝐼, (𝐼 + 1)〉)‘0) = (𝑊‘(0 + 𝐼))) |
32 | 3, 12, 14, 30, 31 | syl31anc 1329 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 substr 〈𝐼, (𝐼 + 1)〉)‘0) = (𝑊‘(0 + 𝐼))) |
33 | | addid2 10219 |
. . . . . . 7
⊢ (𝐼 ∈ ℂ → (0 +
𝐼) = 𝐼) |
34 | 33 | eqcomd 2628 |
. . . . . 6
⊢ (𝐼 ∈ ℂ → 𝐼 = (0 + 𝐼)) |
35 | 17, 34 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → 𝐼 = (0 + 𝐼)) |
36 | 35 | fveq2d 6195 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑊‘𝐼) = (𝑊‘(0 + 𝐼))) |
37 | 32, 36 | eqtr4d 2659 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 substr 〈𝐼, (𝐼 + 1)〉)‘0) = (𝑊‘𝐼)) |
38 | 37 | s1eqd 13381 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → 〈“((𝑊 substr 〈𝐼, (𝐼 + 1)〉)‘0)”〉 =
〈“(𝑊‘𝐼)”〉) |
39 | 23, 38 | eqtrd 2656 |
1
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑊 substr 〈𝐼, (𝐼 + 1)〉) = 〈“(𝑊‘𝐼)”〉) |