ge0p1rp

Description: A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 5-Oct-2015)

		Ref	Expression
	Assertion	ge0p1rp	$⊢ (A \in ℝ \land 0 \leq A) \to A + 1 \in ℝ^{+}$

Step	Hyp	Ref	Expression
1		peano2re	$⊢ A \in ℝ \to A + 1 \in ℝ$
2	1	adantr	$⊢ (A \in ℝ \land 0 \leq A) \to A + 1 \in ℝ$
3		0red	$⊢ (A \in ℝ \land 0 \leq A) \to 0 \in ℝ$
4		simpl	$⊢ (A \in ℝ \land 0 \leq A) \to A \in ℝ$
5		simpr	$⊢ (A \in ℝ \land 0 \leq A) \to 0 \leq A$
6		ltp1	$⊢ A \in ℝ \to A < A + 1$
7	6	adantr	$⊢ (A \in ℝ \land 0 \leq A) \to A < A + 1$
8	3 4 2 5 7	lelttrd	$⊢ (A \in ℝ \land 0 \leq A) \to 0 < A + 1$
9		elrp	$⊢ A + 1 \in ℝ^{+} \leftrightarrow (A + 1 \in ℝ \land 0 < A + 1)$
10	2 8 9	sylanbrc	$⊢ (A \in ℝ \land 0 \leq A) \to A + 1 \in ℝ^{+}$

Metamath Proof Explorer