Metamath Proof Explorer

Theorem repswlsw

Description: The last symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018)

Ref Expression
Assertion repswlsw ⊢ S ∈ V ∧ N ∈ ℕ → lastS ⁡ S repeatS N = S

Proof

Step Hyp Ref Expression
1 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
2 repsw ⊢ S ∈ V ∧ N ∈ ℕ 0 → S repeatS N ∈ Word V
3 1 2 sylan2 ⊢ S ∈ V ∧ N ∈ ℕ → S repeatS N ∈ Word V
4 lsw ⊢ S repeatS N ∈ Word V → lastS ⁡ S repeatS N = S repeatS N ⁡ S repeatS N − 1
5 3 4 syl ⊢ S ∈ V ∧ N ∈ ℕ → lastS ⁡ S repeatS N = S repeatS N ⁡ S repeatS N − 1
6 simpl ⊢ S ∈ V ∧ N ∈ ℕ → S ∈ V
7 1 adantl ⊢ S ∈ V ∧ N ∈ ℕ → N ∈ ℕ 0
8 repswlen ⊢ S ∈ V ∧ N ∈ ℕ 0 → S repeatS N = N
9 1 8 sylan2 ⊢ S ∈ V ∧ N ∈ ℕ → S repeatS N = N
10 9 oveq1d ⊢ S ∈ V ∧ N ∈ ℕ → S repeatS N − 1 = N − 1
11 fzo0end ⊢ N ∈ ℕ → N − 1 ∈ 0 ..^ N
12 11 adantl ⊢ S ∈ V ∧ N ∈ ℕ → N − 1 ∈ 0 ..^ N
13 10 12 eqeltrd ⊢ S ∈ V ∧ N ∈ ℕ → S repeatS N − 1 ∈ 0 ..^ N
14 repswsymb ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ S repeatS N − 1 ∈ 0 ..^ N → S repeatS N ⁡ S repeatS N − 1 = S
15 6 7 13 14 syl3anc ⊢ S ∈ V ∧ N ∈ ℕ → S repeatS N ⁡ S repeatS N − 1 = S
16 5 15 eqtrd ⊢ S ∈ V ∧ N ∈ ℕ → lastS ⁡ S repeatS N = S