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 e. Word V /\ N e. ( 2 ... ( # ` W ) ) ) -> ( W substr <. ( N - 2 ) , N >. ) = <" ( W ` ( N - 2 ) ) ( W ` ( N - 1 ) ) "> )

Proof

Step Hyp Ref Expression
1 elfzelz 
 |-  ( N e. ( 2 ... ( # ` W ) ) -> N e. ZZ )
2 1 zcnd 
 |-  ( N e. ( 2 ... ( # ` W ) ) -> N e. CC )
3 2cnd 
 |-  ( N e. ( 2 ... ( # ` W ) ) -> 2 e. CC )
4 2 3 npcand 
 |-  ( N e. ( 2 ... ( # ` W ) ) -> ( ( N - 2 ) + 2 ) = N )
5 4 eqcomd 
 |-  ( N e. ( 2 ... ( # ` W ) ) -> N = ( ( N - 2 ) + 2 ) )
6 5 opeq2d 
 |-  ( N e. ( 2 ... ( # ` W ) ) -> <. ( N - 2 ) , N >. = <. ( N - 2 ) , ( ( N - 2 ) + 2 ) >. )
7 6 oveq2d 
 |-  ( N e. ( 2 ... ( # ` W ) ) -> ( W substr <. ( N - 2 ) , N >. ) = ( W substr <. ( N - 2 ) , ( ( N - 2 ) + 2 ) >. ) )
8 7 adantl 
 |-  ( ( W e. Word V /\ N e. ( 2 ... ( # ` W ) ) ) -> ( W substr <. ( N - 2 ) , N >. ) = ( W substr <. ( N - 2 ) , ( ( N - 2 ) + 2 ) >. ) )
9 simpl 
 |-  ( ( W e. Word V /\ N e. ( 2 ... ( # ` W ) ) ) -> W e. Word V )
10 elfzuz 
 |-  ( N e. ( 2 ... ( # ` W ) ) -> N e. ( ZZ>= ` 2 ) )
11 uznn0sub 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 2 ) e. NN0 )
12 10 11 syl 
 |-  ( N e. ( 2 ... ( # ` W ) ) -> ( N - 2 ) e. NN0 )
13 12 adantl 
 |-  ( ( W e. Word V /\ N e. ( 2 ... ( # ` W ) ) ) -> ( N - 2 ) e. NN0 )
14 1cnd 
 |-  ( N e. ( 2 ... ( # ` W ) ) -> 1 e. CC )
15 2 3 14 subsubd 
 |-  ( N e. ( 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 e. ( 2 ... ( # ` W ) ) -> ( ( N - 2 ) + 1 ) = ( N - 1 ) )
19 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
20 fzss1 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> ( 2 ... ( # ` W ) ) C_ ( 1 ... ( # ` W ) ) )
21 19 20 ax-mp 
 |-  ( 2 ... ( # ` W ) ) C_ ( 1 ... ( # ` W ) )
22 21 sseli 
 |-  ( N e. ( 2 ... ( # ` W ) ) -> N e. ( 1 ... ( # ` W ) ) )
23 fz1fzo0m1 
 |-  ( N e. ( 1 ... ( # ` W ) ) -> ( N - 1 ) e. ( 0 ..^ ( # ` W ) ) )
24 22 23 syl 
 |-  ( N e. ( 2 ... ( # ` W ) ) -> ( N - 1 ) e. ( 0 ..^ ( # ` W ) ) )
25 18 24 eqeltrd 
 |-  ( N e. ( 2 ... ( # ` W ) ) -> ( ( N - 2 ) + 1 ) e. ( 0 ..^ ( # ` W ) ) )
26 25 adantl 
 |-  ( ( W e. Word V /\ N e. ( 2 ... ( # ` W ) ) ) -> ( ( N - 2 ) + 1 ) e. ( 0 ..^ ( # ` W ) ) )
27 swrds2 
 |-  ( ( W e. Word V /\ ( N - 2 ) e. NN0 /\ ( ( N - 2 ) + 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( W substr <. ( N - 2 ) , ( ( N - 2 ) + 2 ) >. ) = <" ( W ` ( N - 2 ) ) ( W ` ( ( N - 2 ) + 1 ) ) "> )
28 9 13 26 27 syl3anc 
 |-  ( ( W e. Word V /\ N e. ( 2 ... ( # ` W ) ) ) -> ( W substr <. ( N - 2 ) , ( ( N - 2 ) + 2 ) >. ) = <" ( W ` ( N - 2 ) ) ( W ` ( ( N - 2 ) + 1 ) ) "> )
29 eqidd 
 |-  ( ( W e. Word V /\ N e. ( 2 ... ( # ` W ) ) ) -> ( W ` ( N - 2 ) ) = ( W ` ( N - 2 ) ) )
30 18 fveq2d 
 |-  ( N e. ( 2 ... ( # ` W ) ) -> ( W ` ( ( N - 2 ) + 1 ) ) = ( W ` ( N - 1 ) ) )
31 30 adantl 
 |-  ( ( W e. Word V /\ N e. ( 2 ... ( # ` W ) ) ) -> ( W ` ( ( N - 2 ) + 1 ) ) = ( W ` ( N - 1 ) ) )
32 29 31 s2eqd 
 |-  ( ( W e. Word V /\ N e. ( 2 ... ( # ` W ) ) ) -> <" ( W ` ( N - 2 ) ) ( W ` ( ( N - 2 ) + 1 ) ) "> = <" ( W ` ( N - 2 ) ) ( W ` ( N - 1 ) ) "> )
33 8 28 32 3eqtrd 
 |-  ( ( W e. Word V /\ N e. ( 2 ... ( # ` W ) ) ) -> ( W substr <. ( N - 2 ) , N >. ) = <" ( W ` ( N - 2 ) ) ( W ` ( N - 1 ) ) "> )