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

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 addridi ⊢ ( ( 𝑁 · 𝐴 ) + 0 ) = ( 𝑁 · 𝐴 )
10 5 dec0h ⊢ ( 𝑁 · 𝐵 ) = 0 ( 𝑁 · 𝐵 )
11 1 2 3 4 5 6 9 10 decmul2c ⊢ ( 𝑁 · 𝐴 𝐵 ) = ( 𝑁 · 𝐴 ) ( 𝑁 · 𝐵 )