Theorem dpcl

Description: Prove that the closure of the decimal point is RR as we have defined it. See df-dp . (Contributed by David A. Wheeler, 15-May-2015)

	Ref	Expression
Assertion	dpcl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in ℝ\right)\to A.B\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		dpval	Could not format ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B ) : No typesetting found for |- ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B ) with typecode |-
2		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
3		dp2cl	Could not format ( ( A e. RR /\ B e. RR ) -> _ A B e. RR ) : No typesetting found for |- ( ( A e. RR /\ B e. RR ) -> _ A B e. RR ) with typecode |-
4	2 3	sylan	Could not format ( ( A e. NN0 /\ B e. RR ) -> _ A B e. RR ) : No typesetting found for |- ( ( A e. NN0 /\ B e. RR ) -> _ A B e. RR ) with typecode |-
5	1 4	eqeltrd	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in ℝ\right)\to A.B\in ℝ$$