Theorem 11multnc

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

	Ref	Expression
Hypothesis	11multnc.n	⊢ 𝑁 ∈ ℕ0
Assertion	11multnc	⊢ ( 𝑁 · ; 1 1 ) = ; 𝑁 𝑁

Proof

Step	Hyp	Ref	Expression
1		11multnc.n	⊢ 𝑁 ∈ ℕ0
2		1nn0	⊢ 1 ∈ ℕ0
3	1 2 2	decmulnc	⊢ ( 𝑁 · ; 1 1 ) = ; ( 𝑁 · 1 ) ( 𝑁 · 1 )
4	1	nn0cni	⊢ 𝑁 ∈ ℂ
5	4	mulridi	⊢ ( 𝑁 · 1 ) = 𝑁
6	5 5	deceq12i	⊢ ; ( 𝑁 · 1 ) ( 𝑁 · 1 ) = ; 𝑁 𝑁
7	3 6	eqtri	⊢ ( 𝑁 · ; 1 1 ) = ; 𝑁 𝑁