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 A0AA+1+

Proof

Step Hyp Ref Expression
1 peano2re AA+1
2 1 adantr A0AA+1
3 0red A0A0
4 simpl A0AA
5 simpr A0A0A
6 ltp1 AA<A+1
7 6 adantr A0AA<A+1
8 3 4 2 5 7 lelttrd A0A0<A+1
9 elrp A+1+A+10<A+1
10 2 8 9 sylanbrc A0AA+1+