Metamath Proof Explorer

Theorem letrp1

Description: A transitive property of 'less than or equal' and plus 1. (Contributed by NM, 5-Aug-2005)

Ref Expression
Assertion letrp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ≤ B + 1

Proof

Step Hyp Ref Expression
1 ltp1 ⊢ B ∈ ℝ → B < B + 1
2 1 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ → B < B + 1
3 peano2re ⊢ B ∈ ℝ → B + 1 ∈ ℝ
4 3 ancli ⊢ B ∈ ℝ → B ∈ ℝ ∧ B + 1 ∈ ℝ
5 lelttr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B + 1 ∈ ℝ → A ≤ B ∧ B < B + 1 → A < B + 1
6 5 3expb ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B + 1 ∈ ℝ → A ≤ B ∧ B < B + 1 → A < B + 1
7 4 6 sylan2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ∧ B < B + 1 → A < B + 1
8 2 7 mpan2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B → A < B + 1
9 8 3impia ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A < B + 1
10 ltle ⊢ A ∈ ℝ ∧ B + 1 ∈ ℝ → A < B + 1 → A ≤ B + 1
11 3 10 sylan2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B + 1 → A ≤ B + 1
12 11 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A < B + 1 → A ≤ B + 1
13 9 12 mpd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ≤ B + 1