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 ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) )

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 1 a1i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 2 ∈ ℤ )
3 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
4 3 nn0zd ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
5 4 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
6 simpr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 2 ≤ ( ♯ ‘ 𝑊 ) )
7 eluz2 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) )
8 2 5 6 7 syl3anbrc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 2 ) )
9 ige2m1fz1 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 2 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
10 8 9 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
11 pfxfvlsw ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) )
12 10 11 syldan ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) )
13 3 nn0cnd ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
14 sub1m1 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℂ → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 2 ) )
15 13 14 syl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 2 ) )
16 15 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 2 ) )
17 16 fveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) )
18 12 17 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) )