Theorem decmul10add

Description: A multiplication of a number and a numeral expressed as addition with first summand as multiple of 10. (Contributed by AV, 22-Jul-2021) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Hypotheses	decmul10add.1	⊢ 𝐴 ∈ ℕ0
	decmul10add.2	⊢ 𝐵 ∈ ℕ0
	decmul10add.3	⊢ 𝑀 ∈ ℕ0
	decmul10add.4	⊢ 𝐸 = ( 𝑀 · 𝐴 )
	decmul10add.5	⊢ 𝐹 = ( 𝑀 · 𝐵 )
Assertion	decmul10add	⊢ ( 𝑀 · ; 𝐴 𝐵 ) = ( ; 𝐸 0 + 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		decmul10add.1	⊢ 𝐴 ∈ ℕ0
2		decmul10add.2	⊢ 𝐵 ∈ ℕ0
3		decmul10add.3	⊢ 𝑀 ∈ ℕ0
4		decmul10add.4	⊢ 𝐸 = ( 𝑀 · 𝐴 )
5		decmul10add.5	⊢ 𝐹 = ( 𝑀 · 𝐵 )
6		dfdec10	⊢ ; 𝐴 𝐵 = ( ( ; 1 0 · 𝐴 ) + 𝐵 )
7	6	oveq2i	⊢ ( 𝑀 · ; 𝐴 𝐵 ) = ( 𝑀 · ( ( ; 1 0 · 𝐴 ) + 𝐵 ) )
8	3	nn0cni	⊢ 𝑀 ∈ ℂ
9		10nn0	⊢ ; 1 0 ∈ ℕ0
10	9 1	nn0mulcli	⊢ ( ; 1 0 · 𝐴 ) ∈ ℕ0
11	10	nn0cni	⊢ ( ; 1 0 · 𝐴 ) ∈ ℂ
12	2	nn0cni	⊢ 𝐵 ∈ ℂ
13	8 11 12	adddii	⊢ ( 𝑀 · ( ( ; 1 0 · 𝐴 ) + 𝐵 ) ) = ( ( 𝑀 · ( ; 1 0 · 𝐴 ) ) + ( 𝑀 · 𝐵 ) )
14	9	nn0cni	⊢ ; 1 0 ∈ ℂ
15	1	nn0cni	⊢ 𝐴 ∈ ℂ
16	8 14 15	mul12i	⊢ ( 𝑀 · ( ; 1 0 · 𝐴 ) ) = ( ; 1 0 · ( 𝑀 · 𝐴 ) )
17	3 1	nn0mulcli	⊢ ( 𝑀 · 𝐴 ) ∈ ℕ0
18	17	dec0u	⊢ ( ; 1 0 · ( 𝑀 · 𝐴 ) ) = ; ( 𝑀 · 𝐴 ) 0
19	4	eqcomi	⊢ ( 𝑀 · 𝐴 ) = 𝐸
20	19	deceq1i	⊢ ; ( 𝑀 · 𝐴 ) 0 = ; 𝐸 0
21	16 18 20	3eqtri	⊢ ( 𝑀 · ( ; 1 0 · 𝐴 ) ) = ; 𝐸 0
22	5	eqcomi	⊢ ( 𝑀 · 𝐵 ) = 𝐹
23	21 22	oveq12i	⊢ ( ( 𝑀 · ( ; 1 0 · 𝐴 ) ) + ( 𝑀 · 𝐵 ) ) = ( ; 𝐸 0 + 𝐹 )
24	7 13 23	3eqtri	⊢ ( 𝑀 · ; 𝐴 𝐵 ) = ( ; 𝐸 0 + 𝐹 )