Proof of Theorem swrds2
| Step | Hyp | Ref
| Expression |
| 1 | | df-s2 14887 |
. . 3
⊢
〈“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”〉 = (〈“(𝑊‘𝐼)”〉 ++ 〈“(𝑊‘(𝐼 + 1))”〉) |
| 2 | | simp1 1137 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝑊 ∈ Word 𝐴) |
| 3 | | simp2 1138 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈
ℕ0) |
| 4 | | elfzo0 13740 |
. . . . . . . 8
⊢ ((𝐼 + 1) ∈
(0..^(♯‘𝑊))
↔ ((𝐼 + 1) ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ (𝐼 + 1) < (♯‘𝑊))) |
| 5 | 4 | simp2bi 1147 |
. . . . . . 7
⊢ ((𝐼 + 1) ∈
(0..^(♯‘𝑊))
→ (♯‘𝑊)
∈ ℕ) |
| 6 | 5 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (♯‘𝑊)
∈ ℕ) |
| 7 | 3 | nn0red 12588 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈
ℝ) |
| 8 | | peano2nn0 12566 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℕ0
→ (𝐼 + 1) ∈
ℕ0) |
| 9 | 3, 8 | syl 17 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) ∈
ℕ0) |
| 10 | 9 | nn0red 12588 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) ∈
ℝ) |
| 11 | 6 | nnred 12281 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (♯‘𝑊)
∈ ℝ) |
| 12 | 7 | lep1d 12199 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ≤ (𝐼 + 1)) |
| 13 | | elfzolt2 13708 |
. . . . . . . 8
⊢ ((𝐼 + 1) ∈
(0..^(♯‘𝑊))
→ (𝐼 + 1) <
(♯‘𝑊)) |
| 14 | 13 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) <
(♯‘𝑊)) |
| 15 | 7, 10, 11, 12, 14 | lelttrd 11419 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 <
(♯‘𝑊)) |
| 16 | | elfzo0 13740 |
. . . . . 6
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
↔ (𝐼 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐼 < (♯‘𝑊))) |
| 17 | 3, 6, 15, 16 | syl3anbrc 1344 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈
(0..^(♯‘𝑊))) |
| 18 | | swrds1 14704 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊 substr 〈𝐼, (𝐼 + 1)〉) = 〈“(𝑊‘𝐼)”〉) |
| 19 | 2, 17, 18 | syl2anc 584 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝑊 substr
〈𝐼, (𝐼 + 1)〉) = 〈“(𝑊‘𝐼)”〉) |
| 20 | | nn0cn 12536 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℂ) |
| 21 | 20 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈
ℂ) |
| 22 | | df-2 12329 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
| 23 | 22 | oveq2i 7442 |
. . . . . . . . 9
⊢ (𝐼 + 2) = (𝐼 + (1 + 1)) |
| 24 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 25 | | addass 11242 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℂ ∧ 1 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1))) |
| 26 | 24, 24, 25 | mp3an23 1455 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℂ → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1))) |
| 27 | 23, 26 | eqtr4id 2796 |
. . . . . . . 8
⊢ (𝐼 ∈ ℂ → (𝐼 + 2) = ((𝐼 + 1) + 1)) |
| 28 | 21, 27 | syl 17 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 2) = ((𝐼 + 1) + 1)) |
| 29 | 28 | opeq2d 4880 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 〈(𝐼 + 1),
(𝐼 + 2)〉 =
〈(𝐼 + 1), ((𝐼 + 1) +
1)〉) |
| 30 | 29 | oveq2d 7447 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝑊 substr
〈(𝐼 + 1), (𝐼 + 2)〉) = (𝑊 substr 〈(𝐼 + 1), ((𝐼 + 1) + 1)〉)) |
| 31 | | swrds1 14704 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝐼 + 1) ∈ (0..^(♯‘𝑊))) → (𝑊 substr 〈(𝐼 + 1), ((𝐼 + 1) + 1)〉) = 〈“(𝑊‘(𝐼 + 1))”〉) |
| 32 | 31 | 3adant2 1132 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝑊 substr
〈(𝐼 + 1), ((𝐼 + 1) + 1)〉) =
〈“(𝑊‘(𝐼 + 1))”〉) |
| 33 | 30, 32 | eqtrd 2777 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝑊 substr
〈(𝐼 + 1), (𝐼 + 2)〉) =
〈“(𝑊‘(𝐼 + 1))”〉) |
| 34 | 19, 33 | oveq12d 7449 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ ((𝑊 substr
〈𝐼, (𝐼 + 1)〉) ++ (𝑊 substr 〈(𝐼 + 1), (𝐼 + 2)〉)) = (〈“(𝑊‘𝐼)”〉 ++ 〈“(𝑊‘(𝐼 + 1))”〉)) |
| 35 | 1, 34 | eqtr4id 2796 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 〈“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”〉 = ((𝑊 substr 〈𝐼, (𝐼 + 1)〉) ++ (𝑊 substr 〈(𝐼 + 1), (𝐼 + 2)〉))) |
| 36 | | elfz2nn0 13658 |
. . . 4
⊢ (𝐼 ∈ (0...(𝐼 + 1)) ↔ (𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ ℕ0
∧ 𝐼 ≤ (𝐼 + 1))) |
| 37 | 3, 9, 12, 36 | syl3anbrc 1344 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈ (0...(𝐼 + 1))) |
| 38 | | peano2nn0 12566 |
. . . . . 6
⊢ ((𝐼 + 1) ∈ ℕ0
→ ((𝐼 + 1) + 1) ∈
ℕ0) |
| 39 | 9, 38 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ ((𝐼 + 1) + 1) ∈
ℕ0) |
| 40 | 28, 39 | eqeltrd 2841 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 2) ∈
ℕ0) |
| 41 | 10 | lep1d 12199 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) ≤ ((𝐼 + 1) + 1)) |
| 42 | 41, 28 | breqtrrd 5171 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) ≤ (𝐼 + 2)) |
| 43 | | elfz2nn0 13658 |
. . . 4
⊢ ((𝐼 + 1) ∈ (0...(𝐼 + 2)) ↔ ((𝐼 + 1) ∈ ℕ0
∧ (𝐼 + 2) ∈
ℕ0 ∧ (𝐼 + 1) ≤ (𝐼 + 2))) |
| 44 | 9, 40, 42, 43 | syl3anbrc 1344 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) ∈
(0...(𝐼 +
2))) |
| 45 | | fzofzp1 13803 |
. . . . 5
⊢ ((𝐼 + 1) ∈
(0..^(♯‘𝑊))
→ ((𝐼 + 1) + 1) ∈
(0...(♯‘𝑊))) |
| 46 | 45 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ ((𝐼 + 1) + 1) ∈
(0...(♯‘𝑊))) |
| 47 | 28, 46 | eqeltrd 2841 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 2) ∈
(0...(♯‘𝑊))) |
| 48 | | ccatswrd 14706 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝐼 ∈ (0...(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (0...(𝐼 + 2)) ∧ (𝐼 + 2) ∈ (0...(♯‘𝑊)))) → ((𝑊 substr 〈𝐼, (𝐼 + 1)〉) ++ (𝑊 substr 〈(𝐼 + 1), (𝐼 + 2)〉)) = (𝑊 substr 〈𝐼, (𝐼 + 2)〉)) |
| 49 | 2, 37, 44, 47, 48 | syl13anc 1374 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ ((𝑊 substr
〈𝐼, (𝐼 + 1)〉) ++ (𝑊 substr 〈(𝐼 + 1), (𝐼 + 2)〉)) = (𝑊 substr 〈𝐼, (𝐼 + 2)〉)) |
| 50 | 35, 49 | eqtr2d 2778 |
1
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝑊 substr
〈𝐼, (𝐼 + 2)〉) = 〈“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”〉) |