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 ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ℕ0 ∧ ( 𝐼 + 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 2 ) ⟩ ) = ⟨“ ( 𝑊 ‘ 𝐼 ) ( 𝑊 ‘ ( 𝐼 + 1 ) ) ”⟩ )

Proof

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