Theorem decdiv10

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

	Ref	Expression
Hypotheses	dpval2.a	$$⊢A\in {\mathbb{N}}_0$$
	dpval2.b	$$⊢B\in ℝ$$
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\in {\mathbb{N}}_0$$
2		dpval2.b	$$⊢B\in ℝ$$
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	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in ℝ\right)\to A.B\in ℝ$$
6	1 2 5	mp2an	$$⊢A.B\in ℝ$$
7	6	recni	$$⊢A.B\in ℂ$$
8		10nn	$$⊢10\in \mathbb{N}$$
9	8	nncni	$$⊢10\in ℂ$$
10	8	nnne0i	$$⊢10\ne 0$$
11	7 9 10	divcan4i	$$⊢\frac{\left(A.B\right)\cdot 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 |-