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\in \mathbb{N}$$
Assertion	rpdp2cl2	Could not format assertion : No typesetting found for |- _ A 0 e. RR+ with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rpdp2cl2.a	$$⊢A\in \mathbb{N}$$
2	1	nnnn0i	$$⊢A\in {\mathbb{N}}_0$$
3	2	dp20u	Could not format _ A 0 = A : No typesetting found for |- _ A 0 = A with typecode |-
4		nnrp	$$⊢A\in \mathbb{N}\to A\in {ℝ}^{+}$$
5	1 4	ax-mp	$$⊢A\in {ℝ}^{+}$$
6	3 5	eqeltri	Could not format _ A 0 e. RR+ : No typesetting found for |- _ A 0 e. RR+ with typecode |-