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 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 2 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) = ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ )

Proof

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