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 0
dpval2.b B
Assertion decdiv10 Could not format assertion : No typesetting found for |- ( ; A B / ; 1 0 ) = ( A . B ) with typecode |-

Proof

Step Hyp Ref Expression
1 dpval2.a A 0
2 dpval2.b B
3 1 2 dpmul10 Could not format ( ( A . B ) x. ; 1 0 ) = ; A B : No typesetting found for |- ( ( A . B ) x. ; 1 0 ) = ; A B with typecode |-
4 3 oveq1i Could not format ( ( ( A . B ) x. ; 1 0 ) / ; 1 0 ) = ( ; A B / ; 1 0 ) : No typesetting found for |- ( ( ( A . B ) x. ; 1 0 ) / ; 1 0 ) = ( ; A B / ; 1 0 ) with typecode |-
5 dpcl A 0 B A . B
6 1 2 5 mp2an A . B
7 6 recni A . B
8 10nn 10
9 8 nncni 10
10 8 nnne0i 10 0
11 7 9 10 divcan4i A . B 10 10 = A . B
12 4 11 eqtr3i Could not format ( ; A B / ; 1 0 ) = ( A . B ) : No typesetting found for |- ( ; A B / ; 1 0 ) = ( A . B ) with typecode |-