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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ ( 𝐵 + 1 ) )

Proof

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