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