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

Metamath Proof Explorer

Theorem s5len

Description: The length of a length 5 string. (Contributed by Mario Carneiro, 26-Feb-2016)

		Ref	Expression
	Assertion	s5len	$⊢ \|⟨“ A B C D E ”⟩\| = 5$

Step	Hyp	Ref	Expression
1		df-s5	$⊢ ⟨“ A B C D E ”⟩ = ⟨“ A B C D ”⟩ ++ ⟨“ E ”⟩$
2		s4cli	$⊢ ⟨“ A B C D ”⟩ \in Word V$
3		s4len	$⊢ \|⟨“ A B C D ”⟩\| = 4$
4		4p1e5	$⊢ 4 + 1 = 5$
5	1 2 3 4	cats1len	$⊢ \|⟨“ A B C D E ”⟩\| = 5$