Theorem ge0p1rp

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

	Ref	Expression
Assertion	ge0p1rp	|- ( ( A e. RR /\ 0 <_ A ) -> ( A + 1 ) e. RR+ )

Proof

Step	Hyp	Ref	Expression
1		peano2re	|- ( A e. RR -> ( A + 1 ) e. RR )
2	1	adantr	|- ( ( A e. RR /\ 0 <_ A ) -> ( A + 1 ) e. RR )
3		0red	|- ( ( A e. RR /\ 0 <_ A ) -> 0 e. RR )
4		simpl	|- ( ( A e. RR /\ 0 <_ A ) -> A e. RR )
5		simpr	|- ( ( A e. RR /\ 0 <_ A ) -> 0 <_ A )
6		ltp1	|- ( A e. RR -> A < ( A + 1 ) )
7	6	adantr	|- ( ( A e. RR /\ 0 <_ A ) -> A < ( A + 1 ) )
8	3 4 2 5 7	lelttrd	|- ( ( A e. RR /\ 0 <_ A ) -> 0 < ( A + 1 ) )
9		elrp	|- ( ( A + 1 ) e. RR+ <-> ( ( A + 1 ) e. RR /\ 0 < ( A + 1 ) ) )
10	2 8 9	sylanbrc	|- ( ( A e. RR /\ 0 <_ A ) -> ( A + 1 ) e. RR+ )