Metamath Proof Explorer

Theorem swrds2m

Description: Extract two adjacent symbols from a word in reverse direction. (Contributed by AV, 11-May-2022)

Ref Expression
Assertion swrds2m ⊢ W ∈ Word V ∧ N ∈ 2 … W → W substr N − 2 N = ⟨“ W ⁡ N − 2 W ⁡ N − 1 ”⟩

Proof

Step Hyp Ref Expression
1 elfzelz ⊢ N ∈ 2 … W → N ∈ ℤ
2 1 zcnd ⊢ N ∈ 2 … W → N ∈ ℂ
3 2cnd ⊢ N ∈ 2 … W → 2 ∈ ℂ
4 2 3 npcand ⊢ N ∈ 2 … W → N - 2 + 2 = N
5 4 eqcomd ⊢ N ∈ 2 … W → N = N - 2 + 2
6 5 opeq2d ⊢ N ∈ 2 … W → N − 2 N = N − 2 N - 2 + 2
7 6 oveq2d ⊢ N ∈ 2 … W → W substr N − 2 N = W substr N − 2 N - 2 + 2
8 7 adantl ⊢ W ∈ Word V ∧ N ∈ 2 … W → W substr N − 2 N = W substr N − 2 N - 2 + 2
9 simpl ⊢ W ∈ Word V ∧ N ∈ 2 … W → W ∈ Word V
10 elfzuz ⊢ N ∈ 2 … W → N ∈ ℤ ≥ 2
11 uznn0sub ⊢ N ∈ ℤ ≥ 2 → N − 2 ∈ ℕ 0
12 10 11 syl ⊢ N ∈ 2 … W → N − 2 ∈ ℕ 0
13 12 adantl ⊢ W ∈ Word V ∧ N ∈ 2 … W → N − 2 ∈ ℕ 0
14 1cnd ⊢ N ∈ 2 … W → 1 ∈ ℂ
15 2 3 14 subsubd ⊢ N ∈ 2 … W → N − 2 − 1 = N - 2 + 1
16 2m1e1 ⊢ 2 − 1 = 1
17 16 oveq2i ⊢ N − 2 − 1 = N − 1
18 15 17 eqtr3di ⊢ N ∈ 2 … W → N - 2 + 1 = N − 1
19 2eluzge1 ⊢ 2 ∈ ℤ ≥ 1
20 fzss1 ⊢ 2 ∈ ℤ ≥ 1 → 2 … W ⊆ 1 … W
21 19 20 ax-mp ⊢ 2 … W ⊆ 1 … W
22 21 sseli ⊢ N ∈ 2 … W → N ∈ 1 … W
23 fz1fzo0m1 ⊢ N ∈ 1 … W → N − 1 ∈ 0 ..^ W
24 22 23 syl ⊢ N ∈ 2 … W → N − 1 ∈ 0 ..^ W
25 18 24 eqeltrd ⊢ N ∈ 2 … W → N - 2 + 1 ∈ 0 ..^ W
26 25 adantl ⊢ W ∈ Word V ∧ N ∈ 2 … W → N - 2 + 1 ∈ 0 ..^ W
27 swrds2 ⊢ W ∈ Word V ∧ N − 2 ∈ ℕ 0 ∧ N - 2 + 1 ∈ 0 ..^ W → W substr N − 2 N - 2 + 2 = ⟨“ W ⁡ N − 2 W ⁡ N - 2 + 1 ”⟩
28 9 13 26 27 syl3anc ⊢ W ∈ Word V ∧ N ∈ 2 … W → W substr N − 2 N - 2 + 2 = ⟨“ W ⁡ N − 2 W ⁡ N - 2 + 1 ”⟩
29 eqidd ⊢ W ∈ Word V ∧ N ∈ 2 … W → W ⁡ N − 2 = W ⁡ N − 2
30 18 fveq2d ⊢ N ∈ 2 … W → W ⁡ N - 2 + 1 = W ⁡ N − 1
31 30 adantl ⊢ W ∈ Word V ∧ N ∈ 2 … W → W ⁡ N - 2 + 1 = W ⁡ N − 1
32 29 31 s2eqd ⊢ W ∈ Word V ∧ N ∈ 2 … W → ⟨“ W ⁡ N − 2 W ⁡ N - 2 + 1 ”⟩ = ⟨“ W ⁡ N − 2 W ⁡ N − 1 ”⟩
33 8 28 32 3eqtrd ⊢ W ∈ Word V ∧ N ∈ 2 … W → W substr N − 2 N = ⟨“ W ⁡ N − 2 W ⁡ N − 1 ”⟩