Theorem decmul2c

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
	decmul2c.c	⊢ ( ( 𝑃 · 𝐴 ) + 𝐸 ) = 𝐶
	decmul2c.2	⊢ ( 𝑃 · 𝐵 ) = ; 𝐸 𝐷
Assertion	decmul2c	⊢ ( 𝑃 · 𝑁 ) = ; 𝐶 𝐷

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		decmul2c.c	⊢ ( ( 𝑃 · 𝐴 ) + 𝐸 ) = 𝐶
8		decmul2c.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	nummul2c	⊢ ( 𝑃 · 𝑁 ) = ( ( ; 1 0 · 𝐶 ) + 𝐷 )
15		dfdec10	⊢ ; 𝐶 𝐷 = ( ( ; 1 0 · 𝐶 ) + 𝐷 )
16	14 15	eqtr4i	⊢ ( 𝑃 · 𝑁 ) = ; 𝐶 𝐷