Metamath Proof Explorer


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 )