Proof of Theorem swrds2
Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → 𝑊 ∈ Word 𝐴) |
2 | | simp2 1062 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → 𝐼 ∈
ℕ0) |
3 | | elfzo0 12508 |
. . . . . . . 8
⊢ ((𝐼 + 1) ∈ (0..^(#‘𝑊)) ↔ ((𝐼 + 1) ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ (𝐼 + 1) <
(#‘𝑊))) |
4 | 3 | simp2bi 1077 |
. . . . . . 7
⊢ ((𝐼 + 1) ∈ (0..^(#‘𝑊)) → (#‘𝑊) ∈
ℕ) |
5 | 4 | 3ad2ant3 1084 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (#‘𝑊) ∈
ℕ) |
6 | 2 | nn0red 11352 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → 𝐼 ∈ ℝ) |
7 | | peano2nn0 11333 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℕ0
→ (𝐼 + 1) ∈
ℕ0) |
8 | 2, 7 | syl 17 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝐼 + 1) ∈
ℕ0) |
9 | 8 | nn0red 11352 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝐼 + 1) ∈ ℝ) |
10 | 5 | nnred 11035 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (#‘𝑊) ∈
ℝ) |
11 | 6 | lep1d 10955 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → 𝐼 ≤ (𝐼 + 1)) |
12 | | elfzolt2 12479 |
. . . . . . . 8
⊢ ((𝐼 + 1) ∈ (0..^(#‘𝑊)) → (𝐼 + 1) < (#‘𝑊)) |
13 | 12 | 3ad2ant3 1084 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝐼 + 1) < (#‘𝑊)) |
14 | 6, 9, 10, 11, 13 | lelttrd 10195 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → 𝐼 < (#‘𝑊)) |
15 | | elfzo0 12508 |
. . . . . 6
⊢ (𝐼 ∈ (0..^(#‘𝑊)) ↔ (𝐼 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝐼 < (#‘𝑊))) |
16 | 2, 5, 14, 15 | syl3anbrc 1246 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → 𝐼 ∈ (0..^(#‘𝑊))) |
17 | | swrds1 13451 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (𝑊 substr 〈𝐼, (𝐼 + 1)〉) = 〈“(𝑊‘𝐼)”〉) |
18 | 1, 16, 17 | syl2anc 693 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝑊 substr 〈𝐼, (𝐼 + 1)〉) = 〈“(𝑊‘𝐼)”〉) |
19 | | nn0cn 11302 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℂ) |
20 | 19 | 3ad2ant2 1083 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → 𝐼 ∈ ℂ) |
21 | | ax-1cn 9994 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
22 | | addass 10023 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℂ ∧ 1 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1))) |
23 | 21, 21, 22 | mp3an23 1416 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℂ → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1))) |
24 | | df-2 11079 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
25 | 24 | oveq2i 6661 |
. . . . . . . . 9
⊢ (𝐼 + 2) = (𝐼 + (1 + 1)) |
26 | 23, 25 | syl6reqr 2675 |
. . . . . . . 8
⊢ (𝐼 ∈ ℂ → (𝐼 + 2) = ((𝐼 + 1) + 1)) |
27 | 20, 26 | syl 17 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝐼 + 2) = ((𝐼 + 1) + 1)) |
28 | 27 | opeq2d 4409 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → 〈(𝐼 + 1), (𝐼 + 2)〉 = 〈(𝐼 + 1), ((𝐼 + 1) + 1)〉) |
29 | 28 | oveq2d 6666 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝑊 substr 〈(𝐼 + 1), (𝐼 + 2)〉) = (𝑊 substr 〈(𝐼 + 1), ((𝐼 + 1) + 1)〉)) |
30 | | swrds1 13451 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝑊 substr 〈(𝐼 + 1), ((𝐼 + 1) + 1)〉) = 〈“(𝑊‘(𝐼 + 1))”〉) |
31 | 30 | 3adant2 1080 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝑊 substr 〈(𝐼 + 1), ((𝐼 + 1) + 1)〉) = 〈“(𝑊‘(𝐼 + 1))”〉) |
32 | 29, 31 | eqtrd 2656 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝑊 substr 〈(𝐼 + 1), (𝐼 + 2)〉) = 〈“(𝑊‘(𝐼 + 1))”〉) |
33 | 18, 32 | oveq12d 6668 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → ((𝑊 substr 〈𝐼, (𝐼 + 1)〉) ++ (𝑊 substr 〈(𝐼 + 1), (𝐼 + 2)〉)) = (〈“(𝑊‘𝐼)”〉 ++ 〈“(𝑊‘(𝐼 + 1))”〉)) |
34 | | df-s2 13593 |
. . 3
⊢
〈“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”〉 = (〈“(𝑊‘𝐼)”〉 ++ 〈“(𝑊‘(𝐼 + 1))”〉) |
35 | 33, 34 | syl6reqr 2675 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → 〈“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”〉 = ((𝑊 substr 〈𝐼, (𝐼 + 1)〉) ++ (𝑊 substr 〈(𝐼 + 1), (𝐼 + 2)〉))) |
36 | | elfz2nn0 12431 |
. . . 4
⊢ (𝐼 ∈ (0...(𝐼 + 1)) ↔ (𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ ℕ0
∧ 𝐼 ≤ (𝐼 + 1))) |
37 | 2, 8, 11, 36 | syl3anbrc 1246 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → 𝐼 ∈ (0...(𝐼 + 1))) |
38 | | peano2nn0 11333 |
. . . . . 6
⊢ ((𝐼 + 1) ∈ ℕ0
→ ((𝐼 + 1) + 1) ∈
ℕ0) |
39 | 8, 38 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → ((𝐼 + 1) + 1) ∈
ℕ0) |
40 | 27, 39 | eqeltrd 2701 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝐼 + 2) ∈
ℕ0) |
41 | 9 | lep1d 10955 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝐼 + 1) ≤ ((𝐼 + 1) + 1)) |
42 | 41, 27 | breqtrrd 4681 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝐼 + 1) ≤ (𝐼 + 2)) |
43 | | elfz2nn0 12431 |
. . . 4
⊢ ((𝐼 + 1) ∈ (0...(𝐼 + 2)) ↔ ((𝐼 + 1) ∈ ℕ0
∧ (𝐼 + 2) ∈
ℕ0 ∧ (𝐼 + 1) ≤ (𝐼 + 2))) |
44 | 8, 40, 42, 43 | syl3anbrc 1246 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝐼 + 1) ∈ (0...(𝐼 + 2))) |
45 | | fzofzp1 12565 |
. . . . 5
⊢ ((𝐼 + 1) ∈ (0..^(#‘𝑊)) → ((𝐼 + 1) + 1) ∈ (0...(#‘𝑊))) |
46 | 45 | 3ad2ant3 1084 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → ((𝐼 + 1) + 1) ∈ (0...(#‘𝑊))) |
47 | 27, 46 | eqeltrd 2701 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝐼 + 2) ∈ (0...(#‘𝑊))) |
48 | | ccatswrd 13456 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝐼 ∈ (0...(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (0...(𝐼 + 2)) ∧ (𝐼 + 2) ∈ (0...(#‘𝑊)))) → ((𝑊 substr 〈𝐼, (𝐼 + 1)〉) ++ (𝑊 substr 〈(𝐼 + 1), (𝐼 + 2)〉)) = (𝑊 substr 〈𝐼, (𝐼 + 2)〉)) |
49 | 1, 37, 44, 47, 48 | syl13anc 1328 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → ((𝑊 substr 〈𝐼, (𝐼 + 1)〉) ++ (𝑊 substr 〈(𝐼 + 1), (𝐼 + 2)〉)) = (𝑊 substr 〈𝐼, (𝐼 + 2)〉)) |
50 | 35, 49 | eqtr2d 2657 |
1
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ (0..^(#‘𝑊))) → (𝑊 substr 〈𝐼, (𝐼 + 2)〉) = 〈“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”〉) |