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∈WordV∧N∈2…W→WsubstrN−2N=⟨“W⁡N−2W⁡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−2N=N−2N-2+2
7 6 oveq2d ⊢N∈2…W→WsubstrN−2N=WsubstrN−2N-2+2
8 7 adantl ⊢W∈WordV∧N∈2…W→WsubstrN−2N=WsubstrN−2N-2+2
9 simpl ⊢W∈WordV∧N∈2…W→W∈WordV
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∈WordV∧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∈WordV∧N∈2…W→N-2+1∈0..^W
27 swrds2 ⊢W∈WordV∧N−2∈ℕ0∧N-2+1∈0..^W→WsubstrN−2N-2+2=⟨“W⁡N−2W⁡N-2+1”⟩
28 9 13 26 27 syl3anc ⊢W∈WordV∧N∈2…W→WsubstrN−2N-2+2=⟨“W⁡N−2W⁡N-2+1”⟩
29 eqidd ⊢W∈WordV∧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∈WordV∧N∈2…W→W⁡N-2+1=W⁡N−1
32 29 31 s2eqd ⊢W∈WordV∧N∈2…W→⟨“W⁡N−2W⁡N-2+1”⟩=⟨“W⁡N−2W⁡N−1”⟩
33 8 28 32 3eqtrd ⊢W∈WordV∧N∈2…W→WsubstrN−2N=⟨“W⁡N−2W⁡N−1”⟩