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 )