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

Metamath Proof Explorer

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+ )