xrlelttr

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

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

Step	Hyp	Ref	Expression
1		xrleloe	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \leq B \leftrightarrow (A < B \lor A = B))$
2	1	3adant3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A \leq B \leftrightarrow (A < B \lor A = B))$
3		xrlttr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A < B \land B < C) \to A < C)$
4	3	expd	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A < B \to (B < C \to A < C))$
5		breq1	$⊢ A = B \to (A < C \leftrightarrow B < C)$
6	5	biimprd	$⊢ A = B \to (B < C \to A < C)$
7	6	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A = B \to (B < C \to A < C))$
8	4 7	jaod	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A < B \lor A = B) \to (B < C \to A < C))$
9	2 8	sylbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A \leq B \to (B < C \to A < C))$
10	9	impd	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A \leq B \land B < C) \to A < C)$

Metamath Proof Explorer