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 
|- A e. NN0
decmul10add.2 
|- B e. NN0
decmul10add.3 
|- M e. NN0
decmul10add.4 
|- E = ( M x. A )
decmul10add.5 
|- F = ( M x. B )
Assertion decmul10add 
|- ( M x. ; A B ) = ( ; E 0 + F )

Proof

Step Hyp Ref Expression
1 decmul10add.1 
 |-  A e. NN0
2 decmul10add.2 
 |-  B e. NN0
3 decmul10add.3 
 |-  M e. NN0
4 decmul10add.4 
 |-  E = ( M x. A )
5 decmul10add.5 
 |-  F = ( M x. B )
6 dfdec10 
 |-  ; A B = ( ( ; 1 0 x. A ) + B )
7 6 oveq2i 
 |-  ( M x. ; A B ) = ( M x. ( ( ; 1 0 x. A ) + B ) )
8 3 nn0cni 
 |-  M e. CC
9 10nn0 
 |-  ; 1 0 e. NN0
10 9 1 nn0mulcli 
 |-  ( ; 1 0 x. A ) e. NN0
11 10 nn0cni 
 |-  ( ; 1 0 x. A ) e. CC
12 2 nn0cni 
 |-  B e. CC
13 8 11 12 adddii 
 |-  ( M x. ( ( ; 1 0 x. A ) + B ) ) = ( ( M x. ( ; 1 0 x. A ) ) + ( M x. B ) )
14 9 nn0cni 
 |-  ; 1 0 e. CC
15 1 nn0cni 
 |-  A e. CC
16 8 14 15 mul12i 
 |-  ( M x. ( ; 1 0 x. A ) ) = ( ; 1 0 x. ( M x. A ) )
17 3 1 nn0mulcli 
 |-  ( M x. A ) e. NN0
18 17 dec0u 
 |-  ( ; 1 0 x. ( M x. A ) ) = ; ( M x. A ) 0
19 4 eqcomi 
 |-  ( M x. A ) = E
20 19 deceq1i 
 |-  ; ( M x. A ) 0 = ; E 0
21 16 18 20 3eqtri 
 |-  ( M x. ( ; 1 0 x. A ) ) = ; E 0
22 5 eqcomi 
 |-  ( M x. B ) = F
23 21 22 oveq12i 
 |-  ( ( M x. ( ; 1 0 x. A ) ) + ( M x. B ) ) = ( ; E 0 + F )
24 7 13 23 3eqtri 
 |-  ( M x. ; A B ) = ( ; E 0 + F )