Metamath Proof Explorer


Theorem pfxtrcfvl

Description: The last symbol in a word truncated by one symbol. (Contributed by AV, 16-Jun-2018) (Revised by AV, 5-May-2020)

Ref Expression
Assertion pfxtrcfvl W Word V 2 W lastS W prefix W 1 = W W 2

Proof

Step Hyp Ref Expression
1 2z 2
2 1 a1i W Word V 2 W 2
3 lencl W Word V W 0
4 3 nn0zd W Word V W
5 4 adantr W Word V 2 W W
6 simpr W Word V 2 W 2 W
7 eluz2 W 2 2 W 2 W
8 2 5 6 7 syl3anbrc W Word V 2 W W 2
9 ige2m1fz1 W 2 W 1 1 W
10 8 9 syl W Word V 2 W W 1 1 W
11 pfxfvlsw W Word V W 1 1 W lastS W prefix W 1 = W W - 1 - 1
12 10 11 syldan W Word V 2 W lastS W prefix W 1 = W W - 1 - 1
13 3 nn0cnd W Word V W
14 sub1m1 W W - 1 - 1 = W 2
15 13 14 syl W Word V W - 1 - 1 = W 2
16 15 adantr W Word V 2 W W - 1 - 1 = W 2
17 16 fveq2d W Word V 2 W W W - 1 - 1 = W W 2
18 12 17 eqtrd W Word V 2 W lastS W prefix W 1 = W W 2