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

Metamath Proof Explorer

Theorem rpaddcld

Description: Closure law for addition of positive reals. Part of Axiom 7 of Apostol p. 20. (Contributed by Mario Carneiro, 28-May-2016)

Step	Hyp	Ref	Expression
1		rpred.1	$⊢ φ \to A \in ℝ^{+}$
2		rpaddcld.1	$⊢ φ \to B \in ℝ^{+}$
3		rpaddcl	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to A + B \in ℝ^{+}$
4	1 2 3	syl2anc	$⊢ φ \to A + B \in ℝ^{+}$