Step | Hyp | Ref
| Expression |
1 | | df-s2 14799 |
. . 3
⊢
⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩ = (⟨“(𝑊‘𝐼)”⟩ ++ ⟨“(𝑊‘(𝐼 + 1))”⟩) |
2 | | simp1 1137 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝑊 ∈ Word 𝐴) |
3 | | simp2 1138 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈
ℕ0) |
4 | | elfzo0 13673 |
. . . . . . . 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 12533 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈
ℝ) |
8 | | peano2nn0 12512 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℕ0
→ (𝐼 + 1) ∈
ℕ0) |
9 | 3, 8 | syl 17 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) ∈
ℕ0) |
10 | 9 | nn0red 12533 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) ∈
ℝ) |
11 | 6 | nnred 12227 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (♯‘𝑊)
∈ ℝ) |
12 | 7 | lep1d 12145 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ≤ (𝐼 + 1)) |
13 | | elfzolt2 13641 |
. . . . . . . 8
⊢ ((𝐼 + 1) ∈
(0..^(♯‘𝑊))
→ (𝐼 + 1) <
(♯‘𝑊)) |
14 | 13 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) <
(♯‘𝑊)) |
15 | 7, 10, 11, 12, 14 | lelttrd 11372 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 <
(♯‘𝑊)) |
16 | | elfzo0 13673 |
. . . . . 6
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
↔ (𝐼 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐼 < (♯‘𝑊))) |
17 | 3, 6, 15, 16 | syl3anbrc 1344 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈
(0..^(♯‘𝑊))) |
18 | | swrds1 14616 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊 substr ⟨𝐼, (𝐼 + 1)⟩) = ⟨“(𝑊‘𝐼)”⟩) |
19 | 2, 17, 18 | syl2anc 585 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝑊 substr
⟨𝐼, (𝐼 + 1)⟩) = ⟨“(𝑊‘𝐼)”⟩) |
20 | | nn0cn 12482 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℂ) |
21 | 20 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈
ℂ) |
22 | | df-2 12275 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
23 | 22 | oveq2i 7420 |
. . . . . . . . 9
⊢ (𝐼 + 2) = (𝐼 + (1 + 1)) |
24 | | ax-1cn 11168 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
25 | | addass 11197 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℂ ∧ 1 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1))) |
26 | 24, 24, 25 | mp3an23 1454 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℂ → ((𝐼 + 1) + 1) = (𝐼 + (1 + 1))) |
27 | 23, 26 | eqtr4id 2792 |
. . . . . . . 8
⊢ (𝐼 ∈ ℂ → (𝐼 + 2) = ((𝐼 + 1) + 1)) |
28 | 21, 27 | syl 17 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 2) = ((𝐼 + 1) + 1)) |
29 | 28 | opeq2d 4881 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ ⟨(𝐼 + 1),
(𝐼 + 2)⟩ =
⟨(𝐼 + 1), ((𝐼 + 1) +
1)⟩) |
30 | 29 | oveq2d 7425 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝑊 substr
⟨(𝐼 + 1), (𝐼 + 2)⟩) = (𝑊 substr ⟨(𝐼 + 1), ((𝐼 + 1) + 1)⟩)) |
31 | | swrds1 14616 |
. . . . . 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 2773 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝑊 substr
⟨(𝐼 + 1), (𝐼 + 2)⟩) =
⟨“(𝑊‘(𝐼 + 1))”⟩) |
34 | 19, 33 | oveq12d 7427 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ ((𝑊 substr
⟨𝐼, (𝐼 + 1)⟩) ++ (𝑊 substr ⟨(𝐼 + 1), (𝐼 + 2)⟩)) = (⟨“(𝑊‘𝐼)”⟩ ++ ⟨“(𝑊‘(𝐼 + 1))”⟩)) |
35 | 1, 34 | eqtr4id 2792 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩ = ((𝑊 substr ⟨𝐼, (𝐼 + 1)⟩) ++ (𝑊 substr ⟨(𝐼 + 1), (𝐼 + 2)⟩))) |
36 | | elfz2nn0 13592 |
. . . 4
⊢ (𝐼 ∈ (0...(𝐼 + 1)) ↔ (𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈ ℕ0
∧ 𝐼 ≤ (𝐼 + 1))) |
37 | 3, 9, 12, 36 | syl3anbrc 1344 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ 𝐼 ∈ (0...(𝐼 + 1))) |
38 | | peano2nn0 12512 |
. . . . . 6
⊢ ((𝐼 + 1) ∈ ℕ0
→ ((𝐼 + 1) + 1) ∈
ℕ0) |
39 | 9, 38 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ ((𝐼 + 1) + 1) ∈
ℕ0) |
40 | 28, 39 | eqeltrd 2834 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 2) ∈
ℕ0) |
41 | 10 | lep1d 12145 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) ≤ ((𝐼 + 1) + 1)) |
42 | 41, 28 | breqtrrd 5177 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 1) ≤ (𝐼 + 2)) |
43 | | elfz2nn0 13592 |
. . . 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 13729 |
. . . . 5
⊢ ((𝐼 + 1) ∈
(0..^(♯‘𝑊))
→ ((𝐼 + 1) + 1) ∈
(0...(♯‘𝑊))) |
46 | 45 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ ((𝐼 + 1) + 1) ∈
(0...(♯‘𝑊))) |
47 | 28, 46 | eqeltrd 2834 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝐼 + 2) ∈
(0...(♯‘𝑊))) |
48 | | ccatswrd 14618 |
. . 3
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝐼 ∈ (0...(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (0...(𝐼 + 2)) ∧ (𝐼 + 2) ∈ (0...(♯‘𝑊)))) → ((𝑊 substr ⟨𝐼, (𝐼 + 1)⟩) ++ (𝑊 substr ⟨(𝐼 + 1), (𝐼 + 2)⟩)) = (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) |
49 | 2, 37, 44, 47, 48 | syl13anc 1373 |
. 2
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ ((𝑊 substr
⟨𝐼, (𝐼 + 1)⟩) ++ (𝑊 substr ⟨(𝐼 + 1), (𝐼 + 2)⟩)) = (𝑊 substr ⟨𝐼, (𝐼 + 2)⟩)) |
50 | 35, 49 | eqtr2d 2774 |
1
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ (𝐼 + 1) ∈
(0..^(♯‘𝑊)))
→ (𝑊 substr
⟨𝐼, (𝐼 + 2)⟩) = ⟨“(𝑊‘𝐼)(𝑊‘(𝐼 + 1))”⟩) |