Theorem dpval2

Description: Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		dpval2.a	⊢ 𝐴 ∈ ℕ0
2		dpval2.b	⊢ 𝐵 ∈ ℝ
3		dpval	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) = _ 𝐴 𝐵 )
4	1 2 3	mp2an	⊢ ( 𝐴 . 𝐵 ) = _ 𝐴 𝐵
5		df-dp2	⊢ _ 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / ; 1 0 ) )
6	4 5	eqtri	⊢ ( 𝐴 . 𝐵 ) = ( 𝐴 + ( 𝐵 / ; 1 0 ) )