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

Metamath Proof Explorer

Theorem 0dp2dp

Description: Multiply by 10 a decimal expansion which starts with a zero. (Contributed by Thierry Arnoux, 16-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 0dp2dp.a 
 |-  A e. NN0
2 0dp2dp.b 
 |-  B e. RR+
3 0p1e1 
 |-  ( 0 + 1 ) = 1
4 0z 
 |-  0 e. ZZ
5 1z 
 |-  1 e. ZZ
6 1 2 3 4 5 dpexpp1 
 |-  ( ( A . B ) x. ( ; 1 0 ^ 0 ) ) = ( ( 0 . _ A B ) x. ( ; 1 0 ^ 1 ) )
7 10nn0 
 |-  ; 1 0 e. NN0
8 7 nn0cni 
 |-  ; 1 0 e. CC
9 exp0 
 |-  ( ; 1 0 e. CC -> ( ; 1 0 ^ 0 ) = 1 )
10 8 9 ax-mp 
 |-  ( ; 1 0 ^ 0 ) = 1
11 10 oveq2i 
 |-  ( ( A . B ) x. ( ; 1 0 ^ 0 ) ) = ( ( A . B ) x. 1 )
12 exp1 
 |-  ( ; 1 0 e. CC -> ( ; 1 0 ^ 1 ) = ; 1 0 )
13 8 12 ax-mp 
 |-  ( ; 1 0 ^ 1 ) = ; 1 0
14 13 oveq2i 
 |-  ( ( 0 . _ A B ) x. ( ; 1 0 ^ 1 ) ) = ( ( 0 . _ A B ) x. ; 1 0 )
15 6 11 14 3eqtr3ri 
 |-  ( ( 0 . _ A B ) x. ; 1 0 ) = ( ( A . B ) x. 1 )
16 1 2 rpdpcl 
 |-  ( A . B ) e. RR+
17 rpcn 
 |-  ( ( A . B ) e. RR+ -> ( A . B ) e. CC )
18 16 17 ax-mp 
 |-  ( A . B ) e. CC
19 mulrid 
 |-  ( ( A . B ) e. CC -> ( ( A . B ) x. 1 ) = ( A . B ) )
20 18 19 ax-mp 
 |-  ( ( A . B ) x. 1 ) = ( A . B )
21 15 20 eqtri 
 |-  ( ( 0 . _ A B ) x. ; 1 0 ) = ( A . B )