Proof of Theorem swrds2
Step | Hyp | Ref
| Expression |
1 | | simp1 1128 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝑊 ∈ Word 𝐴) |
2 | | simp2 1129 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈
ℕ0) |
3 | | elfzo0 13066 |
. . . . . . . 8
⊢ ((𝐼 + 1) ∈
(0..^(♯‘𝑊))
↔ ((𝐼 + 1) ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ (𝐼 + 1) < (♯‘𝑊))) |
4 | 3 | simp2bi 1138 |
. . . . . . 7
⊢ ((𝐼 + 1) ∈
(0..^(♯‘𝑊))
→ (♯‘𝑊)
∈ ℕ) |
5 | 4 | 3ad2ant3 1127 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (♯‘𝑊)
∈ ℕ) |
6 | 2 | nn0red 11944 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈
ℝ) |
7 | | peano2nn0 11925 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℕ0
→ (𝐼 + 1) ∈
ℕ0) |
8 | 2, 7 | syl 17 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) ∈
ℕ0) |
9 | 8 | nn0red 11944 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) ∈
ℝ) |
10 | 5 | nnred 11641 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (♯‘𝑊)
∈ ℝ) |
11 | 6 | lep1d 11559 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ≤ (𝐼 + 1)) |
12 | | elfzolt2 13035 |
. . . . . . . 8
⊢ ((𝐼 + 1) ∈
(0..^(♯‘𝑊))
→ (𝐼 + 1) <
(♯‘𝑊)) |
13 | 12 | 3ad2ant3 1127 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) <
(♯‘𝑊)) |
14 | 6, 9, 10, 11, 13 | lelttrd 10786 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 <
(♯‘𝑊)) |
15 | | elfzo0 13066 |
. . . . . 6
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
↔ (𝐼 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐼 < (♯‘𝑊))) |
16 | 2, 5, 14, 15 | syl3anbrc 1335 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈
(0..^(♯‘𝑊))) |
17 | | swrds1 14016 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊 substr 〈𝐼, (𝐼 + 1)〉) = 〈“(𝑊‘𝐼)”〉) |
18 | 1, 16, 17 | syl2anc 584 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝑊 substr
〈𝐼, (𝐼 + 1)〉) = 〈“(𝑊‘𝐼)”〉) |
19 | | nn0cn 11895 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℂ) |
20 | 19 | 3ad2ant2 1126 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈
ℂ) |
21 | | ax-1cn 10583 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
22 | | addass 10612 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℂ ∧ 1 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1))) |
23 | 21, 21, 22 | mp3an23 1444 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℂ → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1))) |
24 | | df-2 11688 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
25 | 24 | oveq2i 7156 |
. . . . . . . . 9
⊢ (𝐼 + 2) = (𝐼 + (1 + 1)) |
26 | 23, 25 | syl6reqr 2872 |
. . . . . . . 8
⊢ (𝐼 ∈ ℂ → (𝐼 + 2) = ((𝐼 + 1) + 1)) |
27 | 20, 26 | syl 17 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 2) = ((𝐼 + 1) + 1)) |
28 | 27 | opeq2d 4802 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 〈(𝐼 + 1),
(𝐼 + 2)〉 =
〈(𝐼 + 1), ((𝐼 + 1) +
1)〉) |
29 | 28 | oveq2d 7161 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝑊 substr
〈(𝐼 + 1), (𝐼 + 2)〉) = (𝑊 substr 〈(𝐼 + 1), ((𝐼 + 1) + 1)〉)) |
30 | | swrds1 14016 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝐼 + 1) ∈ (0..^(♯‘𝑊))) → (𝑊 substr 〈(𝐼 + 1), ((𝐼 + 1) + 1)〉) = 〈“(𝑊‘(𝐼 + 1))”〉) |
31 | 30 | 3adant2 1123 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝑊 substr
〈(𝐼 + 1), ((𝐼 + 1) + 1)〉) =
〈“(𝑊‘(𝐼 + 1))”〉) |
32 | 29, 31 | eqtrd 2853 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝑊 substr
〈(𝐼 + 1), (𝐼 + 2)〉) =
〈“(𝑊‘(𝐼 + 1))”〉) |
33 | 18, 32 | oveq12d 7163 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ ((𝑊 substr
〈𝐼, (𝐼 + 1)〉) ++ (𝑊 substr 〈(𝐼 + 1), (𝐼 + 2)〉)) = (〈“(𝑊‘𝐼)”〉 ++ 〈“(𝑊‘(𝐼 + 1))”〉)) |
34 | | df-s2 14198 |
. . 3
⊢
〈“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”〉 = (〈“(𝑊‘𝐼)”〉 ++ 〈“(𝑊‘(𝐼 + 1))”〉) |
35 | 33, 34 | syl6reqr 2872 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 〈“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”〉 = ((𝑊 substr 〈𝐼, (𝐼 + 1)〉) ++ (𝑊 substr 〈(𝐼 + 1), (𝐼 + 2)〉))) |
36 | | elfz2nn0 12986 |
. . . 4
⊢ (𝐼 ∈ (0...(𝐼 + 1)) ↔ (𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ ℕ0
∧ 𝐼 ≤ (𝐼 + 1))) |
37 | 2, 8, 11, 36 | syl3anbrc 1335 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈ (0...(𝐼 + 1))) |
38 | | peano2nn0 11925 |
. . . . . 6
⊢ ((𝐼 + 1) ∈ ℕ0
→ ((𝐼 + 1) + 1) ∈
ℕ0) |
39 | 8, 38 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ ((𝐼 + 1) + 1) ∈
ℕ0) |
40 | 27, 39 | eqeltrd 2910 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 2) ∈
ℕ0) |
41 | 9 | lep1d 11559 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) ≤ ((𝐼 + 1) + 1)) |
42 | 41, 27 | breqtrrd 5085 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) ≤ (𝐼 + 2)) |
43 | | elfz2nn0 12986 |
. . . 4
⊢ ((𝐼 + 1) ∈ (0...(𝐼 + 2)) ↔ ((𝐼 + 1) ∈ ℕ0
∧ (𝐼 + 2) ∈
ℕ0 ∧ (𝐼 + 1) ≤ (𝐼 + 2))) |
44 | 8, 40, 42, 43 | syl3anbrc 1335 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) ∈
(0...(𝐼 +
2))) |
45 | | fzofzp1 13122 |
. . . . 5
⊢ ((𝐼 + 1) ∈
(0..^(♯‘𝑊))
→ ((𝐼 + 1) + 1) ∈
(0...(♯‘𝑊))) |
46 | 45 | 3ad2ant3 1127 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ ((𝐼 + 1) + 1) ∈
(0...(♯‘𝑊))) |
47 | 27, 46 | eqeltrd 2910 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 2) ∈
(0...(♯‘𝑊))) |
48 | | ccatswrd 14018 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝐼 ∈ (0...(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (0...(𝐼 + 2)) ∧ (𝐼 + 2) ∈ (0...(♯‘𝑊)))) → ((𝑊 substr 〈𝐼, (𝐼 + 1)〉) ++ (𝑊 substr 〈(𝐼 + 1), (𝐼 + 2)〉)) = (𝑊 substr 〈𝐼, (𝐼 + 2)〉)) |
49 | 1, 37, 44, 47, 48 | syl13anc 1364 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ ((𝑊 substr
〈𝐼, (𝐼 + 1)〉) ++ (𝑊 substr 〈(𝐼 + 1), (𝐼 + 2)〉)) = (𝑊 substr 〈𝐼, (𝐼 + 2)〉)) |
50 | 35, 49 | eqtr2d 2854 |
1
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝑊 substr
〈𝐼, (𝐼 + 2)〉) = 〈“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”〉) |