# 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 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to {A}\le {B}+1$

### Proof

Step Hyp Ref Expression
1 ltp1 ${⊢}{B}\in ℝ\to {B}<{B}+1$
2 1 adantl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {B}<{B}+1$
3 peano2re ${⊢}{B}\in ℝ\to {B}+1\in ℝ$
4 3 ancli ${⊢}{B}\in ℝ\to \left({B}\in ℝ\wedge {B}+1\in ℝ\right)$
5 lelttr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {B}+1\in ℝ\right)\to \left(\left({A}\le {B}\wedge {B}<{B}+1\right)\to {A}<{B}+1\right)$
6 5 3expb ${⊢}\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge {B}+1\in ℝ\right)\right)\to \left(\left({A}\le {B}\wedge {B}<{B}+1\right)\to {A}<{B}+1\right)$
7 4 6 sylan2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left({A}\le {B}\wedge {B}<{B}+1\right)\to {A}<{B}+1\right)$
8 2 7 mpan2d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}\le {B}\to {A}<{B}+1\right)$
9 8 3impia ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to {A}<{B}+1$
10 ltle ${⊢}\left({A}\in ℝ\wedge {B}+1\in ℝ\right)\to \left({A}<{B}+1\to {A}\le {B}+1\right)$
11 3 10 sylan2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}<{B}+1\to {A}\le {B}+1\right)$
12 11 3adant3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to \left({A}<{B}+1\to {A}\le {B}+1\right)$
13 9 12 mpd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to {A}\le {B}+1$