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