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	⊢ 𝐴 ∈ ℕ0
	rpdp2cl.b	⊢ 𝐵 ∈ ℝ+
Assertion	rpdp2cl	⊢ _ 𝐴 𝐵 ∈ ℝ+

Proof

Step	Hyp	Ref	Expression
1		rpdp2cl.a	⊢ 𝐴 ∈ ℕ0
2		rpdp2cl.b	⊢ 𝐵 ∈ ℝ+
3		df-dp2	⊢ _ 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / ; 1 0 ) )
4	1	nn0rei	⊢ 𝐴 ∈ ℝ
5		rpssre	⊢ ℝ+ ⊆ ℝ
6		10nn	⊢ ; 1 0 ∈ ℕ
7		nnrp	⊢ ( ; 1 0 ∈ ℕ → ; 1 0 ∈ ℝ+ )
8	6 7	ax-mp	⊢ ; 1 0 ∈ ℝ+
9		rpdivcl	⊢ ( ( 𝐵 ∈ ℝ+ ∧ ; 1 0 ∈ ℝ+ ) → ( 𝐵 / ; 1 0 ) ∈ ℝ+ )
10	2 8 9	mp2an	⊢ ( 𝐵 / ; 1 0 ) ∈ ℝ+
11	5 10	sselii	⊢ ( 𝐵 / ; 1 0 ) ∈ ℝ
12		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 / ; 1 0 ) ∈ ℝ ) → ( 𝐴 + ( 𝐵 / ; 1 0 ) ) ∈ ℝ )
13	4 11 12	mp2an	⊢ ( 𝐴 + ( 𝐵 / ; 1 0 ) ) ∈ ℝ
14	4 11	pm3.2i	⊢ ( 𝐴 ∈ ℝ ∧ ( 𝐵 / ; 1 0 ) ∈ ℝ )
15	1	nn0ge0i	⊢ 0 ≤ 𝐴
16		rpgt0	⊢ ( ( 𝐵 / ; 1 0 ) ∈ ℝ+ → 0 < ( 𝐵 / ; 1 0 ) )
17	10 16	ax-mp	⊢ 0 < ( 𝐵 / ; 1 0 )
18	15 17	pm3.2i	⊢ ( 0 ≤ 𝐴 ∧ 0 < ( 𝐵 / ; 1 0 ) )
19		addgegt0	⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 / ; 1 0 ) ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 < ( 𝐵 / ; 1 0 ) ) ) → 0 < ( 𝐴 + ( 𝐵 / ; 1 0 ) ) )
20	14 18 19	mp2an	⊢ 0 < ( 𝐴 + ( 𝐵 / ; 1 0 ) )
21		elrp	⊢ ( ( 𝐴 + ( 𝐵 / ; 1 0 ) ) ∈ ℝ+ ↔ ( ( 𝐴 + ( 𝐵 / ; 1 0 ) ) ∈ ℝ ∧ 0 < ( 𝐴 + ( 𝐵 / ; 1 0 ) ) ) )
22	13 20 21	mpbir2an	⊢ ( 𝐴 + ( 𝐵 / ; 1 0 ) ) ∈ ℝ+
23	3 22	eqeltri	⊢ _ 𝐴 𝐵 ∈ ℝ+