Description: 5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | 5lt6 | $${\u22a2}5<6$$ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 5re | $${\u22a2}5\in \mathbb{R}$$ | |
2 | 1 | ltp1i | $${\u22a2}5<5+1$$ |
3 | df-6 | $${\u22a2}6=5+1$$ | |
4 | 2 3 | breqtrri | $${\u22a2}5<6$$ |