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 \in ℕ_{0} \land B \in ℝ) \to A . B \in ℝ$

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 ℕ_{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	$⊢ (A \in ℕ_{0} \land B \in ℝ) \to A . B \in ℝ$

Metamath Proof Explorer