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