Metamath Proof Explorer


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 ( 𝑁 · 𝐴 𝐵 ) = ( 𝑁 · 𝐴 ) ( 𝑁 · 𝐵 )