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

Metamath Proof Explorer

Theorem dp3mul10

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

Ref Expression
Hypotheses dp3mul10.a 
|- A e. NN0
dp3mul10.b 
|- B e. NN0
dp3mul10.c 
|- C e. RR
Assertion dp3mul10 
|- ( ( A . _ B C ) x. ; 1 0 ) = ( ; A B . C )

Proof

Step Hyp Ref Expression
1 dp3mul10.a 
 |-  A e. NN0
2 dp3mul10.b 
 |-  B e. NN0
3 dp3mul10.c 
 |-  C e. RR
4 2 nn0rei 
 |-  B e. RR
5 dp2cl 
 |-  ( ( B e. RR /\ C e. RR ) -> _ B C e. RR )
6 4 3 5 mp2an 
 |-  _ B C e. RR
7 1 6 dpmul10 
 |-  ( ( A . _ B C ) x. ; 1 0 ) = ; A _ B C
8 dfdec10 
 |-  ; A _ B C = ( ( ; 1 0 x. A ) + _ B C )
9 10nn 
 |-  ; 1 0 e. NN
10 9 nncni 
 |-  ; 1 0 e. CC
11 1 nn0cni 
 |-  A e. CC
12 10 11 mulcli 
 |-  ( ; 1 0 x. A ) e. CC
13 4 recni 
 |-  B e. CC
14 3 recni 
 |-  C e. CC
15 9 nnne0i 
 |-  ; 1 0 =/= 0
16 14 10 15 divcli 
 |-  ( C / ; 1 0 ) e. CC
17 12 13 16 addassi 
 |-  ( ( ( ; 1 0 x. A ) + B ) + ( C / ; 1 0 ) ) = ( ( ; 1 0 x. A ) + ( B + ( C / ; 1 0 ) ) )
18 dfdec10 
 |-  ; A B = ( ( ; 1 0 x. A ) + B )
19 18 oveq1i 
 |-  ( ; A B + ( C / ; 1 0 ) ) = ( ( ( ; 1 0 x. A ) + B ) + ( C / ; 1 0 ) )
20 df-dp2 
 |-  _ B C = ( B + ( C / ; 1 0 ) )
21 20 oveq2i 
 |-  ( ( ; 1 0 x. A ) + _ B C ) = ( ( ; 1 0 x. A ) + ( B + ( C / ; 1 0 ) ) )
22 17 19 21 3eqtr4ri 
 |-  ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B + ( C / ; 1 0 ) )
23 1 2 deccl 
 |-  ; A B e. NN0
24 23 3 dpval2 
 |-  ( ; A B . C ) = ( ; A B + ( C / ; 1 0 ) )
25 22 24 eqtr4i 
 |-  ( ( ; 1 0 x. A ) + _ B C ) = ( ; A B . C )
26 7 8 25 3eqtri 
 |-  ( ( A . _ B C ) x. ; 1 0 ) = ( ; A B . C )