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+