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 ⊢ ( 𝑁 · 𝑃 ) = 𝐶 𝐷