xrlttr

Description: Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005)

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

Proof

Step	Hyp	Ref	Expression
1		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
2		elxr	$⊢ C \in ℝ^{*} \leftrightarrow (C \in ℝ \lor C = +∞ \lor C = −∞)$
3		elxr	$⊢ B \in ℝ^{*} \leftrightarrow (B \in ℝ \lor B = +∞ \lor B = −∞)$
4		lttr	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A < B \land B < C) \to A < C)$
5	4	3expa	$⊢ ((A \in ℝ \land B \in ℝ) \land C \in ℝ) \to ((A < B \land B < C) \to A < C)$
6	5	an32s	$⊢ ((A \in ℝ \land C \in ℝ) \land B \in ℝ) \to ((A < B \land B < C) \to A < C)$
7		rexr	$⊢ C \in ℝ \to C \in ℝ^{*}$
8		pnfnlt	$⊢ C \in ℝ^{*} \to \neg +∞ < C$
9	7 8	syl	$⊢ C \in ℝ \to \neg +∞ < C$
10	9	adantr	$⊢ (C \in ℝ \land B = +∞) \to \neg +∞ < C$
11		breq1	$⊢ B = +∞ \to (B < C \leftrightarrow +∞ < C)$
12	11	adantl	$⊢ (C \in ℝ \land B = +∞) \to (B < C \leftrightarrow +∞ < C)$
13	10 12	mtbird	$⊢ (C \in ℝ \land B = +∞) \to \neg B < C$
14	13	pm2.21d	$⊢ (C \in ℝ \land B = +∞) \to (B < C \to A < C)$
15	14	adantll	$⊢ ((A \in ℝ \land C \in ℝ) \land B = +∞) \to (B < C \to A < C)$
16	15	adantld	$⊢ ((A \in ℝ \land C \in ℝ) \land B = +∞) \to ((A < B \land B < C) \to A < C)$
17		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
18		nltmnf	$⊢ A \in ℝ^{*} \to \neg A < −∞$
19	17 18	syl	$⊢ A \in ℝ \to \neg A < −∞$
20	19	adantr	$⊢ (A \in ℝ \land B = −∞) \to \neg A < −∞$
21		breq2	$⊢ B = −∞ \to (A < B \leftrightarrow A < −∞)$
22	21	adantl	$⊢ (A \in ℝ \land B = −∞) \to (A < B \leftrightarrow A < −∞)$
23	20 22	mtbird	$⊢ (A \in ℝ \land B = −∞) \to \neg A < B$
24	23	pm2.21d	$⊢ (A \in ℝ \land B = −∞) \to (A < B \to A < C)$
25	24	adantlr	$⊢ ((A \in ℝ \land C \in ℝ) \land B = −∞) \to (A < B \to A < C)$
26	25	adantrd	$⊢ ((A \in ℝ \land C \in ℝ) \land B = −∞) \to ((A < B \land B < C) \to A < C)$
27	6 16 26	3jaodan	$⊢ ((A \in ℝ \land C \in ℝ) \land (B \in ℝ \lor B = +∞ \lor B = −∞)) \to ((A < B \land B < C) \to A < C)$
28	3 27	sylan2b	$⊢ ((A \in ℝ \land C \in ℝ) \land B \in ℝ^{*}) \to ((A < B \land B < C) \to A < C)$
29	28	an32s	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land C \in ℝ) \to ((A < B \land B < C) \to A < C)$
30		ltpnf	$⊢ A \in ℝ \to A < +∞$
31	30	adantr	$⊢ (A \in ℝ \land C = +∞) \to A < +∞$
32		breq2	$⊢ C = +∞ \to (A < C \leftrightarrow A < +∞)$
33	32	adantl	$⊢ (A \in ℝ \land C = +∞) \to (A < C \leftrightarrow A < +∞)$
34	31 33	mpbird	$⊢ (A \in ℝ \land C = +∞) \to A < C$
35	34	adantlr	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land C = +∞) \to A < C$
36	35	a1d	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land C = +∞) \to ((A < B \land B < C) \to A < C)$
37		nltmnf	$⊢ B \in ℝ^{*} \to \neg B < −∞$
38	37	adantr	$⊢ (B \in ℝ^{*} \land C = −∞) \to \neg B < −∞$
39		breq2	$⊢ C = −∞ \to (B < C \leftrightarrow B < −∞)$
40	39	adantl	$⊢ (B \in ℝ^{*} \land C = −∞) \to (B < C \leftrightarrow B < −∞)$
41	38 40	mtbird	$⊢ (B \in ℝ^{*} \land C = −∞) \to \neg B < C$
42	41	pm2.21d	$⊢ (B \in ℝ^{*} \land C = −∞) \to (B < C \to A < C)$
43	42	adantld	$⊢ (B \in ℝ^{*} \land C = −∞) \to ((A < B \land B < C) \to A < C)$
44	43	adantll	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land C = −∞) \to ((A < B \land B < C) \to A < C)$
45	29 36 44	3jaodan	$⊢ ((A \in ℝ \land B \in ℝ^{*}) \land (C \in ℝ \lor C = +∞ \lor C = −∞)) \to ((A < B \land B < C) \to A < C)$
46	45	anasss	$⊢ (A \in ℝ \land (B \in ℝ^{*} \land (C \in ℝ \lor C = +∞ \lor C = −∞))) \to ((A < B \land B < C) \to A < C)$
47		pnfnlt	$⊢ B \in ℝ^{*} \to \neg +∞ < B$
48	47	adantl	$⊢ (A = +∞ \land B \in ℝ^{*}) \to \neg +∞ < B$
49		breq1	$⊢ A = +∞ \to (A < B \leftrightarrow +∞ < B)$
50	49	adantr	$⊢ (A = +∞ \land B \in ℝ^{*}) \to (A < B \leftrightarrow +∞ < B)$
51	48 50	mtbird	$⊢ (A = +∞ \land B \in ℝ^{*}) \to \neg A < B$
52	51	pm2.21d	$⊢ (A = +∞ \land B \in ℝ^{*}) \to (A < B \to A < C)$
53	52	adantrd	$⊢ (A = +∞ \land B \in ℝ^{*}) \to ((A < B \land B < C) \to A < C)$
54	53	adantrr	$⊢ (A = +∞ \land (B \in ℝ^{*} \land (C \in ℝ \lor C = +∞ \lor C = −∞))) \to ((A < B \land B < C) \to A < C)$
55		mnflt	$⊢ C \in ℝ \to −∞ < C$
56	55	adantl	$⊢ (A = −∞ \land C \in ℝ) \to −∞ < C$
57		breq1	$⊢ A = −∞ \to (A < C \leftrightarrow −∞ < C)$
58	57	adantr	$⊢ (A = −∞ \land C \in ℝ) \to (A < C \leftrightarrow −∞ < C)$
59	56 58	mpbird	$⊢ (A = −∞ \land C \in ℝ) \to A < C$
60	59	a1d	$⊢ (A = −∞ \land C \in ℝ) \to ((A < B \land B < C) \to A < C)$
61	60	adantlr	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land C \in ℝ) \to ((A < B \land B < C) \to A < C)$
62		mnfltpnf	$⊢ −∞ < +∞$
63		breq12	$⊢ (A = −∞ \land C = +∞) \to (A < C \leftrightarrow −∞ < +∞)$
64	62 63	mpbiri	$⊢ (A = −∞ \land C = +∞) \to A < C$
65	64	a1d	$⊢ (A = −∞ \land C = +∞) \to ((A < B \land B < C) \to A < C)$
66	65	adantlr	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land C = +∞) \to ((A < B \land B < C) \to A < C)$
67	43	adantll	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land C = −∞) \to ((A < B \land B < C) \to A < C)$
68	61 66 67	3jaodan	$⊢ ((A = −∞ \land B \in ℝ^{*}) \land (C \in ℝ \lor C = +∞ \lor C = −∞)) \to ((A < B \land B < C) \to A < C)$
69	68	anasss	$⊢ (A = −∞ \land (B \in ℝ^{*} \land (C \in ℝ \lor C = +∞ \lor C = −∞))) \to ((A < B \land B < C) \to A < C)$
70	46 54 69	3jaoian	$⊢ ((A \in ℝ \lor A = +∞ \lor A = −∞) \land (B \in ℝ^{*} \land (C \in ℝ \lor C = +∞ \lor C = −∞))) \to ((A < B \land B < C) \to A < C)$
71	70	3impb	$⊢ ((A \in ℝ \lor A = +∞ \lor A = −∞) \land B \in ℝ^{*} \land (C \in ℝ \lor C = +∞ \lor C = −∞)) \to ((A < B \land B < C) \to A < C)$
72	2 71	syl3an3b	$⊢ ((A \in ℝ \lor A = +∞ \lor A = −∞) \land B \in ℝ^{} \land C \in ℝ^{}) \to ((A < B \land B < C) \to A < C)$
73	1 72	syl3an1b	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A < B \land B < C) \to A < C)$

Metamath Proof Explorer

Theorem xrlttr

Proof