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 ) ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )