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	|- ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		dpval	|- ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B )
2		nn0re	|- ( A e. NN0 -> A e. RR )
3		dp2cl	|- ( ( A e. RR /\ B e. RR ) -> _ A B e. RR )
4	2 3	sylan	|- ( ( A e. NN0 /\ B e. RR ) -> _ A B e. RR )
5	1 4	eqeltrd	|- ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) e. RR )