This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem p1le

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

Ref Expression
Assertion p1le ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 + 1 ) ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )

Proof

Step Hyp Ref Expression
1 lep1 ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ ( 𝐴 + 1 ) )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ≤ ( 𝐴 + 1 ) )
3 peano2re ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )
4 3 ancli ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℝ ) )
5 letr ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≤ ( 𝐴 + 1 ) ∧ ( 𝐴 + 1 ) ≤ 𝐵 ) → 𝐴 ≤ 𝐵 ) )
6 5 3expa ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℝ ) ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≤ ( 𝐴 + 1 ) ∧ ( 𝐴 + 1 ) ≤ 𝐵 ) → 𝐴 ≤ 𝐵 ) )
7 4 6 sylan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≤ ( 𝐴 + 1 ) ∧ ( 𝐴 + 1 ) ≤ 𝐵 ) → 𝐴 ≤ 𝐵 ) )
8 2 7 mpand ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 1 ) ≤ 𝐵 → 𝐴 ≤ 𝐵 ) )
9 8 3impia ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 + 1 ) ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )