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 ℕ_{0}$
	rpdp2cl.b	$⊢ B \in ℝ^{+}$
Assertion	rpdp2cl	Could not format assertion : No typesetting found for \|- _ A B e. RR+ with typecode \|-

Step	Hyp	Ref	Expression
1		rpdp2cl.a	$⊢ A \in ℕ_{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 ℕ$
7		nnrp	$⊢ 10 \in ℕ \to 10 \in ℝ^{+}$
8	6 7	ax-mp	$⊢ 10 \in ℝ^{+}$
9		rpdivcl	$⊢ (B \in ℝ^{+} \land 10 \in ℝ^{+}) \to \frac{B}{10} \in ℝ^{+}$
10	2 8 9	mp2an	$⊢ \frac{B}{10} \in ℝ^{+}$
11	5 10	sselii	$⊢ \frac{B}{10} \in ℝ$
12		readdcl	$⊢ (A \in ℝ \land \frac{B}{10} \in ℝ) \to A + (\frac{B}{10}) \in ℝ$
13	4 11 12	mp2an	$⊢ A + (\frac{B}{10}) \in ℝ$
14	4 11	pm3.2i	$⊢ (A \in ℝ \land \frac{B}{10} \in ℝ)$
15	1	nn0ge0i	$⊢ 0 \leq 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	$⊢ (0 \leq A \land 0 < \frac{B}{10})$
19		addgegt0	$⊢ ((A \in ℝ \land \frac{B}{10} \in ℝ) \land (0 \leq A \land 0 < \frac{B}{10})) \to 0 < A + (\frac{B}{10})$
20	14 18 19	mp2an	$⊢ 0 < A + (\frac{B}{10})$
21		elrp	$⊢ A + (\frac{B}{10}) \in ℝ^{+} \leftrightarrow (A + (\frac{B}{10}) \in ℝ \land 0 < A + (\frac{B}{10}))$
22	13 20 21	mpbir2an	$⊢ A + (\frac{B}{10}) \in ℝ^{+}$
23	3 22	eqeltri	Could not format _ A B e. RR+ : No typesetting found for \|- _ A B e. RR+ with typecode \|-

Metamath Proof Explorer