xrltletr

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

		Ref	Expression
	Assertion	xrltletr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A < B \land B \leq C) \to A < 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		xrlttr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A < B \land B < C) \to A < C)$
4	3	expcomd	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (B < C \to (A < B \to A < C))$
5		breq2	$⊢ B = C \to (A < B \leftrightarrow A < C)$
6	5	biimpd	$⊢ B = C \to (A < B \to A < C)$
7	6	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (B = C \to (A < B \to A < C))$
8	4 7	jaod	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((B < C \lor B = C) \to (A < B \to A < C))$
9	2 8	sylbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (B \leq C \to (A < B \to A < C))$
10	9	impcomd	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A < B \land B \leq C) \to A < C)$

Metamath Proof Explorer