Metamath Proof Explorer

Theorem dpmul1000

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

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

Proof

Step Hyp Ref Expression
1 dpmul1000.a 
 |-  A e. NN0
2 dpmul1000.b 
 |-  B e. NN0
3 dpmul1000.c 
 |-  C e. NN0
4 dpmul1000.d 
 |-  D e. RR
5 2 nn0rei 
 |-  B e. RR
6 3 nn0rei 
 |-  C e. RR
7 dp2cl 
 |-  ( ( C e. RR /\ D e. RR ) -> _ C D e. RR )
8 6 4 7 mp2an 
 |-  _ C D e. RR
9 dp2cl 
 |-  ( ( B e. RR /\ _ C D e. RR ) -> _ B _ C D e. RR )
10 5 8 9 mp2an 
 |-  _ B _ C D e. RR
11 dpcl 
 |-  ( ( A e. NN0 /\ _ B _ C D e. RR ) -> ( A . _ B _ C D ) e. RR )
12 1 10 11 mp2an 
 |-  ( A . _ B _ C D ) e. RR
13 12 recni 
 |-  ( A . _ B _ C D ) e. CC
14 10nn0 
 |-  ; 1 0 e. NN0
15 0nn0 
 |-  0 e. NN0
16 14 15 deccl 
 |-  ; ; 1 0 0 e. NN0
17 16 nn0cni 
 |-  ; ; 1 0 0 e. CC
18 14 nn0cni 
 |-  ; 1 0 e. CC
19 13 17 18 mulassi 
 |-  ( ( ( A . _ B _ C D ) x. ; ; 1 0 0 ) x. ; 1 0 ) = ( ( A . _ B _ C D ) x. ( ; ; 1 0 0 x. ; 1 0 ) )
20 1 2 8 dpmul100 
 |-  ( ( A . _ B _ C D ) x. ; ; 1 0 0 ) = ; ; A B _ C D
21 20 oveq1i 
 |-  ( ( ( A . _ B _ C D ) x. ; ; 1 0 0 ) x. ; 1 0 ) = ( ; ; A B _ C D x. ; 1 0 )
22 16 dec0u 
 |-  ( ; 1 0 x. ; ; 1 0 0 ) = ; ; ; 1 0 0 0
23 18 17 22 mulcomli 
 |-  ( ; ; 1 0 0 x. ; 1 0 ) = ; ; ; 1 0 0 0
24 23 oveq2i 
 |-  ( ( A . _ B _ C D ) x. ( ; ; 1 0 0 x. ; 1 0 ) ) = ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 )
25 19 21 24 3eqtr3i 
 |-  ( ; ; A B _ C D x. ; 1 0 ) = ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 )
26 dfdec10 
 |-  ; ; A B _ C D = ( ( ; 1 0 x. ; A B ) + _ C D )
27 26 oveq1i 
 |-  ( ; ; A B _ C D x. ; 1 0 ) = ( ( ( ; 1 0 x. ; A B ) + _ C D ) x. ; 1 0 )
28 1 2 deccl 
 |-  ; A B e. NN0
29 28 nn0cni 
 |-  ; A B e. CC
30 18 29 mulcli 
 |-  ( ; 1 0 x. ; A B ) e. CC
31 8 recni 
 |-  _ C D e. CC
32 30 31 18 adddiri 
 |-  ( ( ( ; 1 0 x. ; A B ) + _ C D ) x. ; 1 0 ) = ( ( ( ; 1 0 x. ; A B ) x. ; 1 0 ) + ( _ C D x. ; 1 0 ) )
33 28 3 4 dfdec100 
 |-  ; ; ; A B C D = ( ( ; ; 1 0 0 x. ; A B ) + ; C D )
34 14 dec0u 
 |-  ( ; 1 0 x. ; 1 0 ) = ; ; 1 0 0
35 34 oveq1i 
 |-  ( ( ; 1 0 x. ; 1 0 ) x. ; A B ) = ( ; ; 1 0 0 x. ; A B )
36 18 18 29 mul32i 
 |-  ( ( ; 1 0 x. ; 1 0 ) x. ; A B ) = ( ( ; 1 0 x. ; A B ) x. ; 1 0 )
37 35 36 eqtr3i 
 |-  ( ; ; 1 0 0 x. ; A B ) = ( ( ; 1 0 x. ; A B ) x. ; 1 0 )
38 3 4 dpmul10 
 |-  ( ( C . D ) x. ; 1 0 ) = ; C D
39 dpval 
 |-  ( ( C e. NN0 /\ D e. RR ) -> ( C . D ) = _ C D )
40 3 4 39 mp2an 
 |-  ( C . D ) = _ C D
41 40 oveq1i 
 |-  ( ( C . D ) x. ; 1 0 ) = ( _ C D x. ; 1 0 )
42 38 41 eqtr3i 
 |-  ; C D = ( _ C D x. ; 1 0 )
43 37 42 oveq12i 
 |-  ( ( ; ; 1 0 0 x. ; A B ) + ; C D ) = ( ( ( ; 1 0 x. ; A B ) x. ; 1 0 ) + ( _ C D x. ; 1 0 ) )
44 33 43 eqtr2i 
 |-  ( ( ( ; 1 0 x. ; A B ) x. ; 1 0 ) + ( _ C D x. ; 1 0 ) ) = ; ; ; A B C D
45 27 32 44 3eqtri 
 |-  ( ; ; A B _ C D x. ; 1 0 ) = ; ; ; A B C D
46 25 45 eqtr3i 
 |-  ( ( A . _ B _ C D ) x. ; ; ; 1 0 0 0 ) = ; ; ; A B C D