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 ⊢ N ∈ ℕ 0
decmulnc.a ⊢ A ∈ ℕ 0
decmulnc.b ⊢ B ∈ ℕ 0
Assertion decmulnc Could not format assertion : No typesetting found for |- ( N x. ; A B ) = ; ( N x. A ) ( N x. B ) with typecode |-

Proof

Step Hyp Ref Expression
1 decmulnc.n ⊢ N ∈ ℕ 0
2 decmulnc.a ⊢ A ∈ ℕ 0
3 decmulnc.b ⊢ B ∈ ℕ 0
4 eqid Could not format ; A B = ; A B : No typesetting found for |- ; A B = ; A B with typecode |-
5 1 3 nn0mulcli ⊢ N ⁢ B ∈ ℕ 0
6 0nn0 ⊢ 0 ∈ ℕ 0
7 1 2 nn0mulcli ⊢ N ⁢ A ∈ ℕ 0
8 7 nn0cni ⊢ N ⁢ A ∈ ℂ
9 8 addridi ⊢ N ⁢ A + 0 = N ⁢ A
10 5 dec0h Could not format ( N x. B ) = ; 0 ( N x. B ) : No typesetting found for |- ( N x. B ) = ; 0 ( N x. B ) with typecode |-
11 1 2 3 4 5 6 9 10 decmul2c Could not format ( N x. ; A B ) = ; ( N x. A ) ( N x. B ) : No typesetting found for |- ( N x. ; A B ) = ; ( N x. A ) ( N x. B ) with typecode |-