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

Proof

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