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

Metamath Proof Explorer

Theorem dpmul100

Description: Multiply by 100 a decimal expansion. (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 dpmul100 
|- ( ( A . _ B C ) x. ; ; 1 0 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 dpval2 
 |-  ( A . _ B C ) = ( A + ( _ B C / ; 1 0 ) )
8 1 nn0cni 
 |-  A e. CC
9 6 recni 
 |-  _ B C e. CC
10 10nn0 
 |-  ; 1 0 e. NN0
11 10 nn0cni 
 |-  ; 1 0 e. CC
12 10nn 
 |-  ; 1 0 e. NN
13 12 nnne0i 
 |-  ; 1 0 =/= 0
14 9 11 13 divcli 
 |-  ( _ B C / ; 1 0 ) e. CC
15 8 14 addcli 
 |-  ( A + ( _ B C / ; 1 0 ) ) e. CC
16 7 15 eqeltri 
 |-  ( A . _ B C ) e. CC
17 16 11 11 mulassi 
 |-  ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ( ( A . _ B C ) x. ( ; 1 0 x. ; 1 0 ) )
18 1 2 3 dfdec100 
 |-  ; ; A B C = ( ( ; ; 1 0 0 x. A ) + ; B C )
19 11 8 11 mul32i 
 |-  ( ( ; 1 0 x. A ) x. ; 1 0 ) = ( ( ; 1 0 x. ; 1 0 ) x. A )
20 10 dec0u 
 |-  ( ; 1 0 x. ; 1 0 ) = ; ; 1 0 0
21 20 oveq1i 
 |-  ( ( ; 1 0 x. ; 1 0 ) x. A ) = ( ; ; 1 0 0 x. A )
22 19 21 eqtri 
 |-  ( ( ; 1 0 x. A ) x. ; 1 0 ) = ( ; ; 1 0 0 x. A )
23 2 3 dpval3 
 |-  ( B . C ) = _ B C
24 23 oveq1i 
 |-  ( ( B . C ) x. ; 1 0 ) = ( _ B C x. ; 1 0 )
25 2 3 dpmul10 
 |-  ( ( B . C ) x. ; 1 0 ) = ; B C
26 24 25 eqtr3i 
 |-  ( _ B C x. ; 1 0 ) = ; B C
27 22 26 oveq12i 
 |-  ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) ) = ( ( ; ; 1 0 0 x. A ) + ; B C )
28 1 6 dpmul10 
 |-  ( ( A . _ B C ) x. ; 1 0 ) = ; A _ B C
29 dfdec10 
 |-  ; A _ B C = ( ( ; 1 0 x. A ) + _ B C )
30 28 29 eqtri 
 |-  ( ( A . _ B C ) x. ; 1 0 ) = ( ( ; 1 0 x. A ) + _ B C )
31 30 oveq1i 
 |-  ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ( ( ( ; 1 0 x. A ) + _ B C ) x. ; 1 0 )
32 11 8 mulcli 
 |-  ( ; 1 0 x. A ) e. CC
33 32 9 11 adddiri 
 |-  ( ( ( ; 1 0 x. A ) + _ B C ) x. ; 1 0 ) = ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) )
34 31 33 eqtr2i 
 |-  ( ( ( ; 1 0 x. A ) x. ; 1 0 ) + ( _ B C x. ; 1 0 ) ) = ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 )
35 18 27 34 3eqtr2ri 
 |-  ( ( ( A . _ B C ) x. ; 1 0 ) x. ; 1 0 ) = ; ; A B C
36 20 oveq2i 
 |-  ( ( A . _ B C ) x. ( ; 1 0 x. ; 1 0 ) ) = ( ( A . _ B C ) x. ; ; 1 0 0 )
37 17 35 36 3eqtr3ri 
 |-  ( ( A . _ B C ) x. ; ; 1 0 0 ) = ; ; A B C