Metamath Proof Explorer

Theorem decmul1

Description: The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021) (Revised by AV, 6-Sep-2021) Remove hypothesis D e. NN0 . (Revised by Steven Nguyen, 7-Dec-2022)

Ref Expression
Hypotheses decmul1.p ⊢ 𝑃 ∈ ℕ0
decmul1.a ⊢ 𝐴 ∈ ℕ0
decmul1.b ⊢ 𝐵 ∈ ℕ0
decmul1.n ⊢ 𝑁 = 𝐴 𝐵
decmul1.c ⊢ ( 𝐴 · 𝑃 ) = 𝐶
decmul1.d ⊢ ( 𝐵 · 𝑃 ) = 𝐷
Assertion decmul1 ( 𝑁 · 𝑃 ) = 𝐶 𝐷

Proof

Step Hyp Ref Expression
1 decmul1.p ⊢ 𝑃 ∈ ℕ0
2 decmul1.a ⊢ 𝐴 ∈ ℕ0
3 decmul1.b ⊢ 𝐵 ∈ ℕ0
4 decmul1.n ⊢ 𝑁 = 𝐴 𝐵
5 decmul1.c ⊢ ( 𝐴 · 𝑃 ) = 𝐶
6 decmul1.d ⊢ ( 𝐵 · 𝑃 ) = 𝐷
7 2 3 deccl ⊢ 𝐴 𝐵 ∈ ℕ0
8 4 7 eqeltri ⊢ 𝑁 ∈ ℕ0
9 8 1 num0u ⊢ ( 𝑁 · 𝑃 ) = ( ( 𝑁 · 𝑃 ) + 0 )
10 0nn0 ⊢ 0 ∈ ℕ0
11 3 1 nn0mulcli ⊢ ( 𝐵 · 𝑃 ) ∈ ℕ0
12 11 nn0cni ⊢ ( 𝐵 · 𝑃 ) ∈ ℂ
13 12 addridi ⊢ ( ( 𝐵 · 𝑃 ) + 0 ) = ( 𝐵 · 𝑃 )
14 13 6 eqtri ⊢ ( ( 𝐵 · 𝑃 ) + 0 ) = 𝐷
15 2 3 10 4 1 5 14 decrmanc ⊢ ( ( 𝑁 · 𝑃 ) + 0 ) = 𝐶 𝐷
16 9 15 eqtri ⊢ ( 𝑁 · 𝑃 ) = 𝐶 𝐷