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∈WordV∧2≤W→lastS⁡WprefixW−1=W⁡W−2

Proof

Step Hyp Ref Expression
1 2z ⊢2∈ℤ
2 1 a1i ⊢W∈WordV∧2≤W→2∈ℤ
3 lencl ⊢W∈WordV→W∈ℕ0
4 3 nn0zd ⊢W∈WordV→W∈ℤ
5 4 adantr ⊢W∈WordV∧2≤W→W∈ℤ
6 simpr ⊢W∈WordV∧2≤W→2≤W
7 eluz2 ⊢W∈ℤ≥2↔2∈ℤ∧W∈ℤ∧2≤W
8 2 5 6 7 syl3anbrc ⊢W∈WordV∧2≤W→W∈ℤ≥2
9 ige2m1fz1 ⊢W∈ℤ≥2→W−1∈1…W
10 8 9 syl ⊢W∈WordV∧2≤W→W−1∈1…W
11 pfxfvlsw ⊢W∈WordV∧W−1∈1…W→lastS⁡WprefixW−1=W⁡W-1-1
12 10 11 syldan ⊢W∈WordV∧2≤W→lastS⁡WprefixW−1=W⁡W-1-1
13 3 nn0cnd ⊢W∈WordV→W∈ℂ
14 sub1m1 ⊢W∈ℂ→W-1-1=W−2
15 13 14 syl ⊢W∈WordV→W-1-1=W−2
16 15 adantr ⊢W∈WordV∧2≤W→W-1-1=W−2
17 16 fveq2d ⊢W∈WordV∧2≤W→W⁡W-1-1=W⁡W−2
18 12 17 eqtrd ⊢W∈WordV∧2≤W→lastS⁡WprefixW−1=W⁡W−2