Metamath Proof Explorer

Theorem pfxtrcfv0

Description: The first symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018) (Revised by AV, 3-May-2020)

Ref Expression
Assertion pfxtrcfv0 ⊢ W ∈ Word V ∧ 2 ≤ W → W prefix W − 1 ⁡ 0 = W ⁡ 0

Proof

Step Hyp Ref Expression
1 simpl ⊢ W ∈ Word V ∧ 2 ≤ W → W ∈ Word V
2 wrdlenge2n0 ⊢ W ∈ Word V ∧ 2 ≤ W → W ≠ ∅
3 2z ⊢ 2 ∈ ℤ
4 3 a1i ⊢ W ∈ Word V ∧ 2 ≤ W → 2 ∈ ℤ
5 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
6 5 nn0zd ⊢ W ∈ Word V → W ∈ ℤ
7 6 adantr ⊢ W ∈ Word V ∧ 2 ≤ W → W ∈ ℤ
8 simpr ⊢ W ∈ Word V ∧ 2 ≤ W → 2 ≤ W
9 eluz2 ⊢ W ∈ ℤ ≥ 2 ↔ 2 ∈ ℤ ∧ W ∈ ℤ ∧ 2 ≤ W
10 4 7 8 9 syl3anbrc ⊢ W ∈ Word V ∧ 2 ≤ W → W ∈ ℤ ≥ 2
11 uz2m1nn ⊢ W ∈ ℤ ≥ 2 → W − 1 ∈ ℕ
12 10 11 syl ⊢ W ∈ Word V ∧ 2 ≤ W → W − 1 ∈ ℕ
13 lbfzo0 ⊢ 0 ∈ 0 ..^ W − 1 ↔ W − 1 ∈ ℕ
14 12 13 sylibr ⊢ W ∈ Word V ∧ 2 ≤ W → 0 ∈ 0 ..^ W − 1
15 pfxtrcfv ⊢ W ∈ Word V ∧ W ≠ ∅ ∧ 0 ∈ 0 ..^ W − 1 → W prefix W − 1 ⁡ 0 = W ⁡ 0
16 1 2 14 15 syl3anc ⊢ W ∈ Word V ∧ 2 ≤ W → W prefix W − 1 ⁡ 0 = W ⁡ 0