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 mulid1
 |-  ( ( 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 )