Metamath Proof Explorer


Theorem decdiv10

Description: Divide a decimal number by 10. (Contributed by Thierry Arnoux, 25-Dec-2021)

Ref Expression
Hypotheses dpval2.a
|- A e. NN0
dpval2.b
|- B e. RR
Assertion decdiv10
|- ( ; A B / ; 1 0 ) = ( A . B )

Proof

Step Hyp Ref Expression
1 dpval2.a
 |-  A e. NN0
2 dpval2.b
 |-  B e. RR
3 1 2 dpmul10
 |-  ( ( A . B ) x. ; 1 0 ) = ; A B
4 3 oveq1i
 |-  ( ( ( A . B ) x. ; 1 0 ) / ; 1 0 ) = ( ; A B / ; 1 0 )
5 dpcl
 |-  ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) e. RR )
6 1 2 5 mp2an
 |-  ( A . B ) e. RR
7 6 recni
 |-  ( A . B ) e. CC
8 10nn
 |-  ; 1 0 e. NN
9 8 nncni
 |-  ; 1 0 e. CC
10 8 nnne0i
 |-  ; 1 0 =/= 0
11 7 9 10 divcan4i
 |-  ( ( ( A . B ) x. ; 1 0 ) / ; 1 0 ) = ( A . B )
12 4 11 eqtr3i
 |-  ( ; A B / ; 1 0 ) = ( A . B )