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