Theorem ge0p1rp

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

	Ref	Expression
Assertion	ge0p1rp	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to A+1\in {ℝ}^{+}$$

Proof

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