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	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 + 𝐵 ) ∈ ℝ+ )