Metamath Proof Explorer


Theorem rpdp2cl2

Description: Closure for a decimal fraction with no decimal expansion in the positive real numbers. (Contributed by Thierry Arnoux, 25-Dec-2021)

Ref Expression
Hypothesis rpdp2cl2.a
|- A e. NN
Assertion rpdp2cl2
|- _ A 0 e. RR+

Proof

Step Hyp Ref Expression
1 rpdp2cl2.a
 |-  A e. NN
2 1 nnnn0i
 |-  A e. NN0
3 2 dp20u
 |-  _ A 0 = A
4 nnrp
 |-  ( A e. NN -> A e. RR+ )
5 1 4 ax-mp
 |-  A e. RR+
6 3 5 eqeltri
 |-  _ A 0 e. RR+