This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ 𝐴 𝐵 ∈ ℝ+