Metamath Proof Explorer

Theorem swrd2lsw

Description: Extract the last two symbols from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018)

Ref Expression
Assertion swrd2lsw 
|- ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = <" ( W ` ( ( # ` W ) - 2 ) ) ( lastS ` W ) "> )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( W e. Word V /\ 1 < ( # ` W ) ) -> W e. Word V )
2 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
3 1z 
 |-  1 e. ZZ
4 nn0z 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. ZZ )
5 zltp1le 
 |-  ( ( 1 e. ZZ /\ ( # ` W ) e. ZZ ) -> ( 1 < ( # ` W ) <-> ( 1 + 1 ) <_ ( # ` W ) ) )
6 3 4 5 sylancr 
 |-  ( ( # ` W ) e. NN0 -> ( 1 < ( # ` W ) <-> ( 1 + 1 ) <_ ( # ` W ) ) )
7 1p1e2 
 |-  ( 1 + 1 ) = 2
8 7 a1i 
 |-  ( ( # ` W ) e. NN0 -> ( 1 + 1 ) = 2 )
9 8 breq1d 
 |-  ( ( # ` W ) e. NN0 -> ( ( 1 + 1 ) <_ ( # ` W ) <-> 2 <_ ( # ` W ) ) )
10 9 biimpd 
 |-  ( ( # ` W ) e. NN0 -> ( ( 1 + 1 ) <_ ( # ` W ) -> 2 <_ ( # ` W ) ) )
11 6 10 sylbid 
 |-  ( ( # ` W ) e. NN0 -> ( 1 < ( # ` W ) -> 2 <_ ( # ` W ) ) )
12 11 imp 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> 2 <_ ( # ` W ) )
13 2nn0 
 |-  2 e. NN0
14 13 jctl 
 |-  ( ( # ` W ) e. NN0 -> ( 2 e. NN0 /\ ( # ` W ) e. NN0 ) )
15 14 adantr 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> ( 2 e. NN0 /\ ( # ` W ) e. NN0 ) )
16 nn0sub 
 |-  ( ( 2 e. NN0 /\ ( # ` W ) e. NN0 ) -> ( 2 <_ ( # ` W ) <-> ( ( # ` W ) - 2 ) e. NN0 ) )
17 15 16 syl 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> ( 2 <_ ( # ` W ) <-> ( ( # ` W ) - 2 ) e. NN0 ) )
18 12 17 mpbid 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> ( ( # ` W ) - 2 ) e. NN0 )
19 2 18 sylan 
 |-  ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( ( # ` W ) - 2 ) e. NN0 )
20 0red 
 |-  ( ( # ` W ) e. ZZ -> 0 e. RR )
21 1red 
 |-  ( ( # ` W ) e. ZZ -> 1 e. RR )
22 zre 
 |-  ( ( # ` W ) e. ZZ -> ( # ` W ) e. RR )
23 20 21 22 3jca 
 |-  ( ( # ` W ) e. ZZ -> ( 0 e. RR /\ 1 e. RR /\ ( # ` W ) e. RR ) )
24 0lt1 
 |-  0 < 1
25 lttr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ ( # ` W ) e. RR ) -> ( ( 0 < 1 /\ 1 < ( # ` W ) ) -> 0 < ( # ` W ) ) )
26 25 expd 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ ( # ` W ) e. RR ) -> ( 0 < 1 -> ( 1 < ( # ` W ) -> 0 < ( # ` W ) ) ) )
27 23 24 26 mpisyl 
 |-  ( ( # ` W ) e. ZZ -> ( 1 < ( # ` W ) -> 0 < ( # ` W ) ) )
28 elnnz 
 |-  ( ( # ` W ) e. NN <-> ( ( # ` W ) e. ZZ /\ 0 < ( # ` W ) ) )
29 28 simplbi2 
 |-  ( ( # ` W ) e. ZZ -> ( 0 < ( # ` W ) -> ( # ` W ) e. NN ) )
30 27 29 syld 
 |-  ( ( # ` W ) e. ZZ -> ( 1 < ( # ` W ) -> ( # ` W ) e. NN ) )
31 4 30 syl 
 |-  ( ( # ` W ) e. NN0 -> ( 1 < ( # ` W ) -> ( # ` W ) e. NN ) )
32 31 imp 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> ( # ` W ) e. NN )
33 fzo0end 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
34 32 33 syl 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
35 nn0cn 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. CC )
36 2cn 
 |-  2 e. CC
37 36 a1i 
 |-  ( ( # ` W ) e. NN0 -> 2 e. CC )
38 1cnd 
 |-  ( ( # ` W ) e. NN0 -> 1 e. CC )
39 35 37 38 3jca 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) e. CC /\ 2 e. CC /\ 1 e. CC ) )
40 1e2m1 
 |-  1 = ( 2 - 1 )
41 40 a1i 
 |-  ( ( ( # ` W ) e. CC /\ 2 e. CC /\ 1 e. CC ) -> 1 = ( 2 - 1 ) )
42 41 oveq2d 
 |-  ( ( ( # ` W ) e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( # ` W ) - 1 ) = ( ( # ` W ) - ( 2 - 1 ) ) )
43 subsub 
 |-  ( ( ( # ` W ) e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( # ` W ) - ( 2 - 1 ) ) = ( ( ( # ` W ) - 2 ) + 1 ) )
44 42 43 eqtrd 
 |-  ( ( ( # ` W ) e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( # ` W ) - 1 ) = ( ( ( # ` W ) - 2 ) + 1 ) )
45 39 44 syl 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) - 1 ) = ( ( ( # ` W ) - 2 ) + 1 ) )
46 45 eqcomd 
 |-  ( ( # ` W ) e. NN0 -> ( ( ( # ` W ) - 2 ) + 1 ) = ( ( # ` W ) - 1 ) )
47 46 eleq1d 
 |-  ( ( # ` W ) e. NN0 -> ( ( ( ( # ` W ) - 2 ) + 1 ) e. ( 0 ..^ ( # ` W ) ) <-> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) )
48 47 adantr 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> ( ( ( ( # ` W ) - 2 ) + 1 ) e. ( 0 ..^ ( # ` W ) ) <-> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) )
49 34 48 mpbird 
 |-  ( ( ( # ` W ) e. NN0 /\ 1 < ( # ` W ) ) -> ( ( ( # ` W ) - 2 ) + 1 ) e. ( 0 ..^ ( # ` W ) ) )
50 2 49 sylan 
 |-  ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( ( ( # ` W ) - 2 ) + 1 ) e. ( 0 ..^ ( # ` W ) ) )
51 1 19 50 3jca 
 |-  ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( W e. Word V /\ ( ( # ` W ) - 2 ) e. NN0 /\ ( ( ( # ` W ) - 2 ) + 1 ) e. ( 0 ..^ ( # ` W ) ) ) )
52 swrds2 
 |-  ( ( W e. Word V /\ ( ( # ` W ) - 2 ) e. NN0 /\ ( ( ( # ` W ) - 2 ) + 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( W substr <. ( ( # ` W ) - 2 ) , ( ( ( # ` W ) - 2 ) + 2 ) >. ) = <" ( W ` ( ( # ` W ) - 2 ) ) ( W ` ( ( ( # ` W ) - 2 ) + 1 ) ) "> )
53 51 52 syl 
 |-  ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( W substr <. ( ( # ` W ) - 2 ) , ( ( ( # ` W ) - 2 ) + 2 ) >. ) = <" ( W ` ( ( # ` W ) - 2 ) ) ( W ` ( ( ( # ` W ) - 2 ) + 1 ) ) "> )
54 35 36 jctir 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) e. CC /\ 2 e. CC ) )
55 npcan 
 |-  ( ( ( # ` W ) e. CC /\ 2 e. CC ) -> ( ( ( # ` W ) - 2 ) + 2 ) = ( # ` W ) )
56 55 eqcomd 
 |-  ( ( ( # ` W ) e. CC /\ 2 e. CC ) -> ( # ` W ) = ( ( ( # ` W ) - 2 ) + 2 ) )
57 2 54 56 3syl 
 |-  ( W e. Word V -> ( # ` W ) = ( ( ( # ` W ) - 2 ) + 2 ) )
58 57 adantr 
 |-  ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( # ` W ) = ( ( ( # ` W ) - 2 ) + 2 ) )
59 58 opeq2d 
 |-  ( ( W e. Word V /\ 1 < ( # ` W ) ) -> <. ( ( # ` W ) - 2 ) , ( # ` W ) >. = <. ( ( # ` W ) - 2 ) , ( ( ( # ` W ) - 2 ) + 2 ) >. )
60 59 oveq2d 
 |-  ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = ( W substr <. ( ( # ` W ) - 2 ) , ( ( ( # ` W ) - 2 ) + 2 ) >. ) )
61 eqidd 
 |-  ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( W ` ( ( # ` W ) - 2 ) ) = ( W ` ( ( # ` W ) - 2 ) ) )
62 lsw 
 |-  ( W e. Word V -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
63 39 43 syl 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) - ( 2 - 1 ) ) = ( ( ( # ` W ) - 2 ) + 1 ) )
64 63 eqcomd 
 |-  ( ( # ` W ) e. NN0 -> ( ( ( # ` W ) - 2 ) + 1 ) = ( ( # ` W ) - ( 2 - 1 ) ) )
65 2m1e1 
 |-  ( 2 - 1 ) = 1
66 65 a1i 
 |-  ( ( # ` W ) e. NN0 -> ( 2 - 1 ) = 1 )
67 66 oveq2d 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) - ( 2 - 1 ) ) = ( ( # ` W ) - 1 ) )
68 64 67 eqtrd 
 |-  ( ( # ` W ) e. NN0 -> ( ( ( # ` W ) - 2 ) + 1 ) = ( ( # ` W ) - 1 ) )
69 2 68 syl 
 |-  ( W e. Word V -> ( ( ( # ` W ) - 2 ) + 1 ) = ( ( # ` W ) - 1 ) )
70 69 eqcomd 
 |-  ( W e. Word V -> ( ( # ` W ) - 1 ) = ( ( ( # ` W ) - 2 ) + 1 ) )
71 70 fveq2d 
 |-  ( W e. Word V -> ( W ` ( ( # ` W ) - 1 ) ) = ( W ` ( ( ( # ` W ) - 2 ) + 1 ) ) )
72 62 71 eqtrd 
 |-  ( W e. Word V -> ( lastS ` W ) = ( W ` ( ( ( # ` W ) - 2 ) + 1 ) ) )
73 72 adantr 
 |-  ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( lastS ` W ) = ( W ` ( ( ( # ` W ) - 2 ) + 1 ) ) )
74 61 73 s2eqd 
 |-  ( ( W e. Word V /\ 1 < ( # ` W ) ) -> <" ( W ` ( ( # ` W ) - 2 ) ) ( lastS ` W ) "> = <" ( W ` ( ( # ` W ) - 2 ) ) ( W ` ( ( ( # ` W ) - 2 ) + 1 ) ) "> )
75 53 60 74 3eqtr4d 
 |-  ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = <" ( W ` ( ( # ` W ) - 2 ) ) ( lastS ` W ) "> )