axlttrn

Description: Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. This restates ax-pre-lttrn with ordering on the extended reals. New proofs should use lttr instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)

		Ref	Expression
	Assertion	axlttrn	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A < B \land B < C) \to A < C)$

Proof

Step	Hyp	Ref	Expression
1		ax-pre-lttrn	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A <_{ℝ} B \land B <_{ℝ} C) \to A <_{ℝ} C)$
2		ltxrlt	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow A <_{ℝ} B)$
3	2	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A < B \leftrightarrow A <_{ℝ} B)$
4		ltxrlt	$⊢ (B \in ℝ \land C \in ℝ) \to (B < C \leftrightarrow B <_{ℝ} C)$
5	4	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (B < C \leftrightarrow B <_{ℝ} C)$
6	3 5	anbi12d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A < B \land B < C) \leftrightarrow (A <_{ℝ} B \land B <_{ℝ} C))$
7		ltxrlt	$⊢ (A \in ℝ \land C \in ℝ) \to (A < C \leftrightarrow A <_{ℝ} C)$
8	7	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A < C \leftrightarrow A <_{ℝ} C)$
9	1 6 8	3imtr4d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A < B \land B < C) \to A < C)$

Metamath Proof Explorer

Theorem axlttrn

Proof