Theorem rpdp2cl

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

	Ref	Expression
Hypotheses	rpdp2cl.a	$$⊢A\in {\mathbb{N}}_0$$
	rpdp2cl.b	$$⊢B\in {ℝ}^{+}$$
Assertion	rpdp2cl	Could not format assertion : No typesetting found for |- _ A B e. RR+ with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rpdp2cl.a	$$⊢A\in {\mathbb{N}}_0$$
2		rpdp2cl.b	$$⊢B\in {ℝ}^{+}$$
3		df-dp2	Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for |- _ A B = ( A + ( B / ; 1 0 ) ) with typecode |-
4	1	nn0rei	$$⊢A\in ℝ$$
5		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
6		10nn	$$⊢10\in \mathbb{N}$$
7		nnrp	$$⊢10\in \mathbb{N}\to 10\in {ℝ}^{+}$$
8	6 7	ax-mp	$$⊢10\in {ℝ}^{+}$$
9		rpdivcl	$$⊢\left(B\in {ℝ}^{+}\wedge 10\in {ℝ}^{+}\right)\to \frac{B}{10}\in {ℝ}^{+}$$
10	2 8 9	mp2an	$$⊢\frac{B}{10}\in {ℝ}^{+}$$
11	5 10	sselii	$$⊢\frac{B}{10}\in ℝ$$
12		readdcl	$$⊢\left(A\in ℝ\wedge \frac{B}{10}\in ℝ\right)\to A+\left(\frac{B}{10}\right)\in ℝ$$
13	4 11 12	mp2an	$$⊢A+\left(\frac{B}{10}\right)\in ℝ$$
14	4 11	pm3.2i	$$⊢\left(A\in ℝ\wedge \frac{B}{10}\in ℝ\right)$$
15	1	nn0ge0i	$$⊢0\le A$$
16		rpgt0	$$⊢\frac{B}{10}\in {ℝ}^{+}\to 0<\frac{B}{10}$$
17	10 16	ax-mp	$$⊢0<\frac{B}{10}$$
18	15 17	pm3.2i	$$⊢\left(0\le A\wedge 0<\frac{B}{10}\right)$$
19		addgegt0	$$⊢\left(\left(A\in ℝ\wedge \frac{B}{10}\in ℝ\right)\wedge \left(0\le A\wedge 0<\frac{B}{10}\right)\right)\to 0<A+\left(\frac{B}{10}\right)$$
20	14 18 19	mp2an	$$⊢0<A+\left(\frac{B}{10}\right)$$
21		elrp	$$⊢A+\left(\frac{B}{10}\right)\in {ℝ}^{+}\leftrightarrow \left(A+\left(\frac{B}{10}\right)\in ℝ\wedge 0<A+\left(\frac{B}{10}\right)\right)$$
22	13 20 21	mpbir2an	$$⊢A+\left(\frac{B}{10}\right)\in {ℝ}^{+}$$
23	3 22	eqeltri	Could not format _ A B e. RR+ : No typesetting found for |- _ A B e. RR+ with typecode |-