Metamath Proof Explorer

Theorem repswfsts

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

Ref Expression
Assertion repswfsts ⊢ S ∈ V ∧ N ∈ ℕ → S repeatS N ⁡ 0 = S

Proof

Step Hyp Ref Expression
1 simpl ⊢ S ∈ V ∧ N ∈ ℕ → S ∈ V
2 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
3 2 adantl ⊢ S ∈ V ∧ N ∈ ℕ → N ∈ ℕ 0
4 lbfzo0 ⊢ 0 ∈ 0 ..^ N ↔ N ∈ ℕ
5 4 biimpri ⊢ N ∈ ℕ → 0 ∈ 0 ..^ N
6 5 adantl ⊢ S ∈ V ∧ N ∈ ℕ → 0 ∈ 0 ..^ N
7 repswsymb ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ 0 ∈ 0 ..^ N → S repeatS N ⁡ 0 = S
8 1 3 6 7 syl3anc ⊢ S ∈ V ∧ N ∈ ℕ → S repeatS N ⁡ 0 = S