Theorem decdiv10

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

	Ref	Expression
Hypotheses	dpval2.a	⊢ 𝐴 ∈ ℕ0
	dpval2.b	⊢ 𝐵 ∈ ℝ
Assertion	decdiv10	⊢ ( ; 𝐴 𝐵 / ; 1 0 ) = ( 𝐴 . 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dpval2.a	⊢ 𝐴 ∈ ℕ0
2		dpval2.b	⊢ 𝐵 ∈ ℝ
3	1 2	dpmul10	⊢ ( ( 𝐴 . 𝐵 ) · ; 1 0 ) = ; 𝐴 𝐵
4	3	oveq1i	⊢ ( ( ( 𝐴 . 𝐵 ) · ; 1 0 ) / ; 1 0 ) = ( ; 𝐴 𝐵 / ; 1 0 )
5		dpcl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) ∈ ℝ )
6	1 2 5	mp2an	⊢ ( 𝐴 . 𝐵 ) ∈ ℝ
7	6	recni	⊢ ( 𝐴 . 𝐵 ) ∈ ℂ
8		10nn	⊢ ; 1 0 ∈ ℕ
9	8	nncni	⊢ ; 1 0 ∈ ℂ
10	8	nnne0i	⊢ ; 1 0 ≠ 0
11	7 9 10	divcan4i	⊢ ( ( ( 𝐴 . 𝐵 ) · ; 1 0 ) / ; 1 0 ) = ( 𝐴 . 𝐵 )
12	4 11	eqtr3i	⊢ ( ; 𝐴 𝐵 / ; 1 0 ) = ( 𝐴 . 𝐵 )