This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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