Metamath Proof Explorer


Theorem p1lep2

Description: A real number increasd by 1 is less than or equal to the number increased by 2. (Contributed by Alexander van der Vekens, 17-Sep-2018)

Ref Expression
Assertion p1lep2 N N + 1 N + 2

Proof

Step Hyp Ref Expression
1 1red N 1
2 2re 2
3 2 a1i N 2
4 id N N
5 1le2 1 2
6 5 a1i N 1 2
7 1 3 4 6 leadd2dd N N + 1 N + 2