repswfsts

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

		Ref	Expression
	Assertion	repswfsts	$⊢ (S \in V \land N \in ℕ) \to (S repeatS N) (0) = S$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (S \in V \land N \in ℕ) \to S \in V$
2		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
3	2	adantl	$⊢ (S \in V \land N \in ℕ) \to N \in ℕ_{0}$
4		lbfzo0	$⊢ 0 \in (0 ..^N) \leftrightarrow N \in ℕ$
5	4	biimpri	$⊢ N \in ℕ \to 0 \in (0 ..^N)$
6	5	adantl	$⊢ (S \in V \land N \in ℕ) \to 0 \in (0 ..^N)$
7		repswsymb	$⊢ (S \in V \land N \in ℕ_{0} \land 0 \in (0 ..^N)) \to (S repeatS N) (0) = S$
8	1 3 6 7	syl3anc	$⊢ (S \in V \land N \in ℕ) \to (S repeatS N) (0) = S$

Metamath Proof Explorer