Metamath Proof Explorer


Theorem sn-ltp1

Description: ltp1 without ax-mulcom . (Contributed by SN, 13-Feb-2024)

Ref Expression
Assertion sn-ltp1
|- ( A e. RR -> A < ( A + 1 ) )

Proof

Step Hyp Ref Expression
1 1re
 |-  1 e. RR
2 sn-0lt1
 |-  0 < 1
3 sn-ltaddpos
 |-  ( ( 1 e. RR /\ A e. RR ) -> ( 0 < 1 <-> A < ( A + 1 ) ) )
4 2 3 mpbii
 |-  ( ( 1 e. RR /\ A e. RR ) -> A < ( A + 1 ) )
5 1 4 mpan
 |-  ( A e. RR -> A < ( A + 1 ) )