Metamath Proof Explorer

Theorem dpmul10

Description: Multiply by 10 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021)

Ref Expression
Hypotheses dpval2.a 
|- A e. NN0
dpval2.b 
|- B e. RR
Assertion dpmul10 
|- ( ( A . B ) x. ; 1 0 ) = ; A B

Proof

Step Hyp Ref Expression
1 dpval2.a 
 |-  A e. NN0
2 dpval2.b 
 |-  B e. RR
3 2 recni 
 |-  B e. CC
4 10nn 
 |-  ; 1 0 e. NN
5 4 nncni 
 |-  ; 1 0 e. CC
6 4 nnne0i 
 |-  ; 1 0 =/= 0
7 3 5 6 divcan2i 
 |-  ( ; 1 0 x. ( B / ; 1 0 ) ) = B
8 7 oveq2i 
 |-  ( ( ; 1 0 x. A ) + ( ; 1 0 x. ( B / ; 1 0 ) ) ) = ( ( ; 1 0 x. A ) + B )
9 1 2 dpval2 
 |-  ( A . B ) = ( A + ( B / ; 1 0 ) )
10 9 oveq2i 
 |-  ( ; 1 0 x. ( A . B ) ) = ( ; 1 0 x. ( A + ( B / ; 1 0 ) ) )
11 dpcl 
 |-  ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) e. RR )
12 1 2 11 mp2an 
 |-  ( A . B ) e. RR
13 12 recni 
 |-  ( A . B ) e. CC
14 5 13 mulcomi 
 |-  ( ; 1 0 x. ( A . B ) ) = ( ( A . B ) x. ; 1 0 )
15 1 nn0cni 
 |-  A e. CC
16 3 5 6 divcli 
 |-  ( B / ; 1 0 ) e. CC
17 5 15 16 adddii 
 |-  ( ; 1 0 x. ( A + ( B / ; 1 0 ) ) ) = ( ( ; 1 0 x. A ) + ( ; 1 0 x. ( B / ; 1 0 ) ) )
18 10 14 17 3eqtr3i 
 |-  ( ( A . B ) x. ; 1 0 ) = ( ( ; 1 0 x. A ) + ( ; 1 0 x. ( B / ; 1 0 ) ) )
19 dfdec10 
 |-  ; A B = ( ( ; 1 0 x. A ) + B )
20 8 18 19 3eqtr4i 
 |-  ( ( A . B ) x. ; 1 0 ) = ; A B