Metamath Proof Explorer

Theorem swrds2

Description: Extract two adjacent symbols from a word. (Contributed by Stefan O'Rear, 23-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion swrds2 ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → W substr I I + 2 = ⟨“ W ⁡ I W ⁡ I + 1 ”⟩

Proof

Step Hyp Ref Expression
1 df-s2 ⊢ ⟨“ W ⁡ I W ⁡ I + 1 ”⟩ = ⟨“ W ⁡ I ”⟩ ++ ⟨“ W ⁡ I + 1 ”⟩
2 simp1 ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → W ∈ Word A
3 simp2 ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I ∈ ℕ 0
4 elfzo0 ⊢ I + 1 ∈ 0 ..^ W ↔ I + 1 ∈ ℕ 0 ∧ W ∈ ℕ ∧ I + 1 < W
5 4 simp2bi ⊢ I + 1 ∈ 0 ..^ W → W ∈ ℕ
6 5 3ad2ant3 ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → W ∈ ℕ
7 3 nn0red ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I ∈ ℝ
8 peano2nn0 ⊢ I ∈ ℕ 0 → I + 1 ∈ ℕ 0
9 3 8 syl ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I + 1 ∈ ℕ 0
10 9 nn0red ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I + 1 ∈ ℝ
11 6 nnred ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → W ∈ ℝ
12 7 lep1d ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I ≤ I + 1
13 elfzolt2 ⊢ I + 1 ∈ 0 ..^ W → I + 1 < W
14 13 3ad2ant3 ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I + 1 < W
15 7 10 11 12 14 lelttrd ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I < W
16 elfzo0 ⊢ I ∈ 0 ..^ W ↔ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I < W
17 3 6 15 16 syl3anbrc ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I ∈ 0 ..^ W
18 swrds1 ⊢ W ∈ Word A ∧ I ∈ 0 ..^ W → W substr I I + 1 = ⟨“ W ⁡ I ”⟩
19 2 17 18 syl2anc ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → W substr I I + 1 = ⟨“ W ⁡ I ”⟩
20 nn0cn ⊢ I ∈ ℕ 0 → I ∈ ℂ
21 20 3ad2ant2 ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I ∈ ℂ
22 df-2 ⊢ 2 = 1 + 1
23 22 oveq2i ⊢ I + 2 = I + 1 + 1
24 ax-1cn ⊢ 1 ∈ ℂ
25 addass ⊢ I ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ → I + 1 + 1 = I + 1 + 1
26 24 24 25 mp3an23 ⊢ I ∈ ℂ → I + 1 + 1 = I + 1 + 1
27 23 26 eqtr4id ⊢ I ∈ ℂ → I + 2 = I + 1 + 1
28 21 27 syl ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I + 2 = I + 1 + 1
29 28 opeq2d ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I + 1 I + 2 = I + 1 I + 1 + 1
30 29 oveq2d ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → W substr I + 1 I + 2 = W substr I + 1 I + 1 + 1
31 swrds1 ⊢ W ∈ Word A ∧ I + 1 ∈ 0 ..^ W → W substr I + 1 I + 1 + 1 = ⟨“ W ⁡ I + 1 ”⟩
32 31 3adant2 ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → W substr I + 1 I + 1 + 1 = ⟨“ W ⁡ I + 1 ”⟩
33 30 32 eqtrd ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → W substr I + 1 I + 2 = ⟨“ W ⁡ I + 1 ”⟩
34 19 33 oveq12d ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → W substr I I + 1 ++ W substr I + 1 I + 2 = ⟨“ W ⁡ I ”⟩ ++ ⟨“ W ⁡ I + 1 ”⟩
35 1 34 eqtr4id ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → ⟨“ W ⁡ I W ⁡ I + 1 ”⟩ = W substr I I + 1 ++ W substr I + 1 I + 2
36 elfz2nn0 ⊢ I ∈ 0 … I + 1 ↔ I ∈ ℕ 0 ∧ I + 1 ∈ ℕ 0 ∧ I ≤ I + 1
37 3 9 12 36 syl3anbrc ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I ∈ 0 … I + 1
38 peano2nn0 ⊢ I + 1 ∈ ℕ 0 → I + 1 + 1 ∈ ℕ 0
39 9 38 syl ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I + 1 + 1 ∈ ℕ 0
40 28 39 eqeltrd ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I + 2 ∈ ℕ 0
41 10 lep1d ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I + 1 ≤ I + 1 + 1
42 41 28 breqtrrd ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I + 1 ≤ I + 2
43 elfz2nn0 ⊢ I + 1 ∈ 0 … I + 2 ↔ I + 1 ∈ ℕ 0 ∧ I + 2 ∈ ℕ 0 ∧ I + 1 ≤ I + 2
44 9 40 42 43 syl3anbrc ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I + 1 ∈ 0 … I + 2
45 fzofzp1 ⊢ I + 1 ∈ 0 ..^ W → I + 1 + 1 ∈ 0 … W
46 45 3ad2ant3 ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I + 1 + 1 ∈ 0 … W
47 28 46 eqeltrd ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → I + 2 ∈ 0 … W
48 ccatswrd ⊢ W ∈ Word A ∧ I ∈ 0 … I + 1 ∧ I + 1 ∈ 0 … I + 2 ∧ I + 2 ∈ 0 … W → W substr I I + 1 ++ W substr I + 1 I + 2 = W substr I I + 2
49 2 37 44 47 48 syl13anc ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → W substr I I + 1 ++ W substr I + 1 I + 2 = W substr I I + 2
50 35 49 eqtr2d ⊢ W ∈ Word A ∧ I ∈ ℕ 0 ∧ I + 1 ∈ 0 ..^ W → W substr I I + 2 = ⟨“ W ⁡ I W ⁡ I + 1 ”⟩