Proof of Theorem swrdswrd0
Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → 𝑊 ∈ Word 𝑉) |
2 | | simpr 476 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → 𝑁 ∈ (0...(#‘𝑊))) |
3 | | elfznn0 12302 |
. . . . . . . 8
⊢ (𝑁 ∈ (0...(#‘𝑊)) → 𝑁 ∈
ℕ0) |
4 | | 0elfz 12305 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ (0...𝑁)) |
5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ (0...(#‘𝑊)) → 0 ∈ (0...𝑁)) |
6 | 5 | adantl 481 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → 0 ∈ (0...𝑁)) |
7 | 1, 2, 6 | 3jca 1235 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 0 ∈ (0...𝑁))) |
8 | 7 | adantr 480 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 0 ∈ (0...𝑁))) |
9 | | elfzelz 12213 |
. . . . . . . . . 10
⊢ (𝑁 ∈ (0...(#‘𝑊)) → 𝑁 ∈ ℤ) |
10 | | zcn 11259 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
11 | 10 | subid1d 10260 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (𝑁 − 0) = 𝑁) |
12 | 11 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 𝑁 = (𝑁 − 0)) |
13 | 9, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ (0...(#‘𝑊)) → 𝑁 = (𝑁 − 0)) |
14 | 13 | adantl 481 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → 𝑁 = (𝑁 − 0)) |
15 | 14 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → (0...𝑁) = (0...(𝑁 − 0))) |
16 | 15 | eleq2d 2673 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝐾 ∈ (0...𝑁) ↔ 𝐾 ∈ (0...(𝑁 − 0)))) |
17 | 14 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝐾...𝑁) = (𝐾...(𝑁 − 0))) |
18 | 17 | eleq2d 2673 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝐿 ∈ (𝐾...𝑁) ↔ 𝐿 ∈ (𝐾...(𝑁 − 0)))) |
19 | 16, 18 | anbi12d 743 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) ↔ (𝐾 ∈ (0...(𝑁 − 0)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 0))))) |
20 | 19 | biimpa 500 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (𝐾 ∈ (0...(𝑁 − 0)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 0)))) |
21 | | swrdswrd 13312 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 0 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁 − 0)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 0))) → ((𝑊 substr 〈0, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈(0 + 𝐾), (0 + 𝐿)〉))) |
22 | 8, 20, 21 | sylc 63 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → ((𝑊 substr 〈0, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈(0 + 𝐾), (0 + 𝐿)〉)) |
23 | | elfzelz 12213 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ) |
24 | 23 | zcnd 11359 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℂ) |
25 | 24 | adantr 480 |
. . . . . . 7
⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → 𝐾 ∈ ℂ) |
26 | 25 | adantl 481 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → 𝐾 ∈ ℂ) |
27 | 26 | addid2d 10116 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (0 + 𝐾) = 𝐾) |
28 | | elfzelz 12213 |
. . . . . . . . 9
⊢ (𝐿 ∈ (𝐾...𝑁) → 𝐿 ∈ ℤ) |
29 | 28 | zcnd 11359 |
. . . . . . . 8
⊢ (𝐿 ∈ (𝐾...𝑁) → 𝐿 ∈ ℂ) |
30 | 29 | adantl 481 |
. . . . . . 7
⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → 𝐿 ∈ ℂ) |
31 | 30 | adantl 481 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → 𝐿 ∈ ℂ) |
32 | 31 | addid2d 10116 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (0 + 𝐿) = 𝐿) |
33 | 27, 32 | opeq12d 4348 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → 〈(0 + 𝐾), (0 + 𝐿)〉 = 〈𝐾, 𝐿〉) |
34 | 33 | oveq2d 6565 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → (𝑊 substr 〈(0 + 𝐾), (0 + 𝐿)〉) = (𝑊 substr 〈𝐾, 𝐿〉)) |
35 | 22, 34 | eqtrd 2644 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁))) → ((𝑊 substr 〈0, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈𝐾, 𝐿〉)) |
36 | 35 | ex 449 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → ((𝐾 ∈ (0...𝑁) ∧ 𝐿 ∈ (𝐾...𝑁)) → ((𝑊 substr 〈0, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈𝐾, 𝐿〉))) |