Metamath Proof Explorer


Theorem rpaddcl

Description: Closure law for addition of positive reals. Part of Axiom 7 of Apostol p. 20. (Contributed by NM, 27-Oct-2007)

Ref Expression
Assertion rpaddcl ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ+ ) → ( 𝐴 + 𝐵 ) ∈ ℝ+ )

Proof

Step Hyp Ref Expression
1 rpre ( 𝐴 ∈ ℝ+𝐴 ∈ ℝ )
2 rpre ( 𝐵 ∈ ℝ+𝐵 ∈ ℝ )
3 readdcl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
4 1 2 3 syl2an ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ+ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
5 elrp ( 𝐴 ∈ ℝ+ ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
6 elrp ( 𝐵 ∈ ℝ+ ↔ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
7 addgt0 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 < 𝐴 ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 + 𝐵 ) )
8 7 an4s ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 + 𝐵 ) )
9 5 6 8 syl2anb ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ+ ) → 0 < ( 𝐴 + 𝐵 ) )
10 elrp ( ( 𝐴 + 𝐵 ) ∈ ℝ+ ↔ ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 0 < ( 𝐴 + 𝐵 ) ) )
11 4 9 10 sylanbrc ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ+ ) → ( 𝐴 + 𝐵 ) ∈ ℝ+ )