xrletr

Description: Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006)

		Ref	Expression
	Assertion	xrletr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A \leq B \land B \leq C) \to A \leq C)$

Step	Hyp	Ref	Expression
1		xrleloe	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to (B \leq C \leftrightarrow (B < C \lor B = C))$
2	1	3adant1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (B \leq C \leftrightarrow (B < C \lor B = C))$
3	2	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to (B \leq C \leftrightarrow (B < C \lor B = C))$
4		xrlelttr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A \leq B \land B < C) \to A < C)$
5		xrltle	$⊢ (A \in ℝ^{} \land C \in ℝ^{}) \to (A < C \to A \leq C)$
6	5	3adant2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A < C \to A \leq C)$
7	4 6	syld	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A \leq B \land B < C) \to A \leq C)$
8	7	expdimp	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to (B < C \to A \leq C)$
9		breq2	$⊢ B = C \to (A \leq B \leftrightarrow A \leq C)$
10	9	biimpcd	$⊢ A \leq B \to (B = C \to A \leq C)$
11	10	adantl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to (B = C \to A \leq C)$
12	8 11	jaod	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to ((B < C \lor B = C) \to A \leq C)$
13	3 12	sylbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to (B \leq C \to A \leq C)$
14	13	expimpd	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A \leq B \land B \leq C) \to A \leq C)$

Metamath Proof Explorer