Theorem dpval3

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

	Ref	Expression
Hypotheses	dpval2.a	⊢ 𝐴 ∈ ℕ0
	dpval2.b	⊢ 𝐵 ∈ ℝ
Assertion	dpval3	⊢ ( 𝐴 . 𝐵 ) = _ 𝐴 𝐵

Proof

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