p1le

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

		Ref	Expression
	Assertion	p1le	$⊢ (A \in ℝ \land B \in ℝ \land A + 1 \leq B) \to A \leq B$

Step	Hyp	Ref	Expression
1		lep1	$⊢ A \in ℝ \to A \leq A + 1$
2	1	adantr	$⊢ (A \in ℝ \land B \in ℝ) \to A \leq A + 1$
3		peano2re	$⊢ A \in ℝ \to A + 1 \in ℝ$
4	3	ancli	$⊢ A \in ℝ \to (A \in ℝ \land A + 1 \in ℝ)$
5		letr	$⊢ (A \in ℝ \land A + 1 \in ℝ \land B \in ℝ) \to ((A \leq A + 1 \land A + 1 \leq B) \to A \leq B)$
6	5	3expa	$⊢ ((A \in ℝ \land A + 1 \in ℝ) \land B \in ℝ) \to ((A \leq A + 1 \land A + 1 \leq B) \to A \leq B)$
7	4 6	sylan	$⊢ (A \in ℝ \land B \in ℝ) \to ((A \leq A + 1 \land A + 1 \leq B) \to A \leq B)$
8	2 7	mpand	$⊢ (A \in ℝ \land B \in ℝ) \to (A + 1 \leq B \to A \leq B)$
9	8	3impia	$⊢ (A \in ℝ \land B \in ℝ \land A + 1 \leq B) \to A \leq B$

Metamath Proof Explorer