This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 + 𝐹 )