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 e. RR -> ( N + 1 ) <_ ( N + 2 ) )

Proof

Step	Hyp	Ref	Expression
1		1red	|- ( N e. RR -> 1 e. RR )
2		2re	|- 2 e. RR
3	2	a1i	|- ( N e. RR -> 2 e. RR )
4		id	|- ( N e. RR -> N e. RR )
5		1le2	|- 1 <_ 2
6	5	a1i	|- ( N e. RR -> 1 <_ 2 )
7	1 3 4 6	leadd2dd	|- ( N e. RR -> ( N + 1 ) <_ ( N + 2 ) )