Theorem decmulnc

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

	Ref	Expression
Hypotheses	decmulnc.n	⊢ 𝑁 ∈ ℕ0
	decmulnc.a	⊢ 𝐴 ∈ ℕ0
	decmulnc.b	⊢ 𝐵 ∈ ℕ0
Assertion	decmulnc	⊢ ( 𝑁 · ; 𝐴 𝐵 ) = ; ( 𝑁 · 𝐴 ) ( 𝑁 · 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		decmulnc.n	⊢ 𝑁 ∈ ℕ0
2		decmulnc.a	⊢ 𝐴 ∈ ℕ0
3		decmulnc.b	⊢ 𝐵 ∈ ℕ0
4		eqid	⊢ ; 𝐴 𝐵 = ; 𝐴 𝐵
5	1 3	nn0mulcli	⊢ ( 𝑁 · 𝐵 ) ∈ ℕ0
6		0nn0	⊢ 0 ∈ ℕ0
7	1 2	nn0mulcli	⊢ ( 𝑁 · 𝐴 ) ∈ ℕ0
8	7	nn0cni	⊢ ( 𝑁 · 𝐴 ) ∈ ℂ
9	8	addid1i	⊢ ( ( 𝑁 · 𝐴 ) + 0 ) = ( 𝑁 · 𝐴 )
10	5	dec0h	⊢ ( 𝑁 · 𝐵 ) = ; 0 ( 𝑁 · 𝐵 )
11	1 2 3 4 5 6 9 10	decmul2c	⊢ ( 𝑁 · ; 𝐴 𝐵 ) = ; ( 𝑁 · 𝐴 ) ( 𝑁 · 𝐵 )