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	⊢ 𝐴 ∈ ℕ
Assertion	rpdp2cl2	⊢ _ 𝐴 0 ∈ ℝ+

Proof

Step	Hyp	Ref	Expression
1		rpdp2cl2.a	⊢ 𝐴 ∈ ℕ
2	1	nnnn0i	⊢ 𝐴 ∈ ℕ0
3	2	dp20u	⊢ _ 𝐴 0 = 𝐴
4		nnrp	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ+ )
5	1 4	ax-mp	⊢ 𝐴 ∈ ℝ+
6	3 5	eqeltri	⊢ _ 𝐴 0 ∈ ℝ+