Metamath Proof Explorer


Theorem decmul1c

Description: The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses decmul1.p 𝑃 ∈ ℕ0
decmul1.a 𝐴 ∈ ℕ0
decmul1.b 𝐵 ∈ ℕ0
decmul1.n 𝑁 = 𝐴 𝐵
decmul1.0 𝐷 ∈ ℕ0
decmul1c.e 𝐸 ∈ ℕ0
decmul1c.c ( ( 𝐴 · 𝑃 ) + 𝐸 ) = 𝐶
decmul1c.2 ( 𝐵 · 𝑃 ) = 𝐸 𝐷
Assertion decmul1c ( 𝑁 · 𝑃 ) = 𝐶 𝐷

Proof

Step Hyp Ref Expression
1 decmul1.p 𝑃 ∈ ℕ0
2 decmul1.a 𝐴 ∈ ℕ0
3 decmul1.b 𝐵 ∈ ℕ0
4 decmul1.n 𝑁 = 𝐴 𝐵
5 decmul1.0 𝐷 ∈ ℕ0
6 decmul1c.e 𝐸 ∈ ℕ0
7 decmul1c.c ( ( 𝐴 · 𝑃 ) + 𝐸 ) = 𝐶
8 decmul1c.2 ( 𝐵 · 𝑃 ) = 𝐸 𝐷
9 10nn0 1 0 ∈ ℕ0
10 dfdec10 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )
11 4 10 eqtri 𝑁 = ( ( 1 0 · 𝐴 ) + 𝐵 )
12 dfdec10 𝐸 𝐷 = ( ( 1 0 · 𝐸 ) + 𝐷 )
13 8 12 eqtri ( 𝐵 · 𝑃 ) = ( ( 1 0 · 𝐸 ) + 𝐷 )
14 9 1 2 3 11 5 6 7 13 nummul1c ( 𝑁 · 𝑃 ) = ( ( 1 0 · 𝐶 ) + 𝐷 )
15 dfdec10 𝐶 𝐷 = ( ( 1 0 · 𝐶 ) + 𝐷 )
16 14 15 eqtr4i ( 𝑁 · 𝑃 ) = 𝐶 𝐷