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