Metamath Proof Explorer


Theorem sn-ltp1

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

Ref Expression
Assertion sn-ltp1 A A < A + 1

Proof

Step Hyp Ref Expression
1 1re 1
2 sn-0lt1 0 < 1
3 sn-ltaddpos 1 A 0 < 1 A < A + 1
4 2 3 mpbii 1 A A < A + 1
5 1 4 mpan A A < A + 1