This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem repsw

Description: A function mapping a half-open range of nonnegative integers to a constant is a word consisting of one symbol repeated several times ("repeated symbol word"). (Contributed by AV, 4-Nov-2018)

		Ref	Expression
	Assertion	repsw	$⊢ (S \in V \land N \in ℕ_{0}) \to S repeatS N \in Word V$

Proof

Step	Hyp	Ref	Expression
1		repsf	$⊢ (S \in V \land N \in ℕ_{0}) \to (S repeatS N) : (0 ..^N) ⟶ V$
2		iswrdi	$⊢ (S repeatS N) : (0 ..^N) ⟶ V \to S repeatS N \in Word V$
3	1 2	syl	$⊢ (S \in V \land N \in ℕ_{0}) \to S repeatS N \in Word V$