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	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 + 1 ) ≤ ( 𝑁 + 2 ) )

Proof

Step	Hyp	Ref	Expression
1		1red	⊢ ( 𝑁 ∈ ℝ → 1 ∈ ℝ )
2		2re	⊢ 2 ∈ ℝ
3	2	a1i	⊢ ( 𝑁 ∈ ℝ → 2 ∈ ℝ )
4		id	⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℝ )
5		1le2	⊢ 1 ≤ 2
6	5	a1i	⊢ ( 𝑁 ∈ ℝ → 1 ≤ 2 )
7	1 3 4 6	leadd2dd	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 + 1 ) ≤ ( 𝑁 + 2 ) )