11multnc

Description: The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021)

		Ref	Expression
	Hypothesis	11multnc.n	$⊢ N \in ℕ_{0}$
	Assertion	11multnc	$⊢ N \cdot 11 = NN$

Step	Hyp	Ref	Expression
1		11multnc.n	$⊢ N \in ℕ_{0}$
2		1nn0	$⊢ 1 \in ℕ_{0}$
3	1 2 2	decmulnc	Could not format ( N x. ; 1 1 ) = ; ( N x. 1 ) ( N x. 1 ) : No typesetting found for \|- ( N x. ; 1 1 ) = ; ( N x. 1 ) ( N x. 1 ) with typecode \|-
4	1	nn0cni	$⊢ N \in ℂ$
5	4	mulridi	$⊢ N \cdot 1 = N$
6	5 5	deceq12i	Could not format ; ( N x. 1 ) ( N x. 1 ) = ; N N : No typesetting found for \|- ; ( N x. 1 ) ( N x. 1 ) = ; N N with typecode \|-
7	3 6	eqtri	$⊢ N \cdot 11 = NN$

Metamath Proof Explorer