xrlttri

Description: Ordering on the extended reals satisfies strict trichotomy. New proofs should generally use this instead of ax-pre-lttri or axlttri . (Contributed by NM, 14-Oct-2005)

		Ref	Expression
	Assertion	xrlttri	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \leftrightarrow \neg (A = B \lor B < A))$

Proof

Step	Hyp	Ref	Expression
1		xrltnr	$⊢ A \in ℝ^{*} \to \neg A < A$
2	1	adantr	$⊢ (A \in ℝ^{*} \land A = B) \to \neg A < A$
3		breq2	$⊢ A = B \to (A < A \leftrightarrow A < B)$
4	3	adantl	$⊢ (A \in ℝ^{*} \land A = B) \to (A < A \leftrightarrow A < B)$
5	2 4	mtbid	$⊢ (A \in ℝ^{*} \land A = B) \to \neg A < B$
6	5	ex	$⊢ A \in ℝ^{*} \to (A = B \to \neg A < B)$
7	6	adantr	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A = B \to \neg A < B)$
8		xrltnsym	$⊢ (B \in ℝ^{} \land A \in ℝ^{}) \to (B < A \to \neg A < B)$
9	8	ancoms	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (B < A \to \neg A < B)$
10	7 9	jaod	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A = B \lor B < A) \to \neg A < B)$
11		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
12		elxr	$⊢ B \in ℝ^{*} \leftrightarrow (B \in ℝ \lor B = +∞ \lor B = −∞)$
13		axlttri	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow \neg (A = B \lor B < A))$
14	13	biimprd	$⊢ (A \in ℝ \land B \in ℝ) \to (\neg (A = B \lor B < A) \to A < B)$
15	14	con1d	$⊢ (A \in ℝ \land B \in ℝ) \to (\neg A < B \to (A = B \lor B < A))$
16		ltpnf	$⊢ A \in ℝ \to A < +∞$
17	16	adantr	$⊢ (A \in ℝ \land B = +∞) \to A < +∞$
18		breq2	$⊢ B = +∞ \to (A < B \leftrightarrow A < +∞)$
19	18	adantl	$⊢ (A \in ℝ \land B = +∞) \to (A < B \leftrightarrow A < +∞)$
20	17 19	mpbird	$⊢ (A \in ℝ \land B = +∞) \to A < B$
21	20	pm2.24d	$⊢ (A \in ℝ \land B = +∞) \to (\neg A < B \to (A = B \lor B < A))$
22		mnflt	$⊢ A \in ℝ \to −∞ < A$
23	22	adantr	$⊢ (A \in ℝ \land B = −∞) \to −∞ < A$
24		breq1	$⊢ B = −∞ \to (B < A \leftrightarrow −∞ < A)$
25	24	adantl	$⊢ (A \in ℝ \land B = −∞) \to (B < A \leftrightarrow −∞ < A)$
26	23 25	mpbird	$⊢ (A \in ℝ \land B = −∞) \to B < A$
27	26	olcd	$⊢ (A \in ℝ \land B = −∞) \to (A = B \lor B < A)$
28	27	a1d	$⊢ (A \in ℝ \land B = −∞) \to (\neg A < B \to (A = B \lor B < A))$
29	15 21 28	3jaodan	$⊢ (A \in ℝ \land (B \in ℝ \lor B = +∞ \lor B = −∞)) \to (\neg A < B \to (A = B \lor B < A))$
30		ltpnf	$⊢ B \in ℝ \to B < +∞$
31	30	adantl	$⊢ (A = +∞ \land B \in ℝ) \to B < +∞$
32		breq2	$⊢ A = +∞ \to (B < A \leftrightarrow B < +∞)$
33	32	adantr	$⊢ (A = +∞ \land B \in ℝ) \to (B < A \leftrightarrow B < +∞)$
34	31 33	mpbird	$⊢ (A = +∞ \land B \in ℝ) \to B < A$
35	34	olcd	$⊢ (A = +∞ \land B \in ℝ) \to (A = B \lor B < A)$
36	35	a1d	$⊢ (A = +∞ \land B \in ℝ) \to (\neg A < B \to (A = B \lor B < A))$
37		eqtr3	$⊢ (A = +∞ \land B = +∞) \to A = B$
38	37	orcd	$⊢ (A = +∞ \land B = +∞) \to (A = B \lor B < A)$
39	38	a1d	$⊢ (A = +∞ \land B = +∞) \to (\neg A < B \to (A = B \lor B < A))$
40		mnfltpnf	$⊢ −∞ < +∞$
41		breq12	$⊢ (B = −∞ \land A = +∞) \to (B < A \leftrightarrow −∞ < +∞)$
42	40 41	mpbiri	$⊢ (B = −∞ \land A = +∞) \to B < A$
43	42	ancoms	$⊢ (A = +∞ \land B = −∞) \to B < A$
44	43	olcd	$⊢ (A = +∞ \land B = −∞) \to (A = B \lor B < A)$
45	44	a1d	$⊢ (A = +∞ \land B = −∞) \to (\neg A < B \to (A = B \lor B < A))$
46	36 39 45	3jaodan	$⊢ (A = +∞ \land (B \in ℝ \lor B = +∞ \lor B = −∞)) \to (\neg A < B \to (A = B \lor B < A))$
47		mnflt	$⊢ B \in ℝ \to −∞ < B$
48	47	adantl	$⊢ (A = −∞ \land B \in ℝ) \to −∞ < B$
49		breq1	$⊢ A = −∞ \to (A < B \leftrightarrow −∞ < B)$
50	49	adantr	$⊢ (A = −∞ \land B \in ℝ) \to (A < B \leftrightarrow −∞ < B)$
51	48 50	mpbird	$⊢ (A = −∞ \land B \in ℝ) \to A < B$
52	51	pm2.24d	$⊢ (A = −∞ \land B \in ℝ) \to (\neg A < B \to (A = B \lor B < A))$
53		breq12	$⊢ (A = −∞ \land B = +∞) \to (A < B \leftrightarrow −∞ < +∞)$
54	40 53	mpbiri	$⊢ (A = −∞ \land B = +∞) \to A < B$
55	54	pm2.24d	$⊢ (A = −∞ \land B = +∞) \to (\neg A < B \to (A = B \lor B < A))$
56		eqtr3	$⊢ (A = −∞ \land B = −∞) \to A = B$
57	56	orcd	$⊢ (A = −∞ \land B = −∞) \to (A = B \lor B < A)$
58	57	a1d	$⊢ (A = −∞ \land B = −∞) \to (\neg A < B \to (A = B \lor B < A))$
59	52 55 58	3jaodan	$⊢ (A = −∞ \land (B \in ℝ \lor B = +∞ \lor B = −∞)) \to (\neg A < B \to (A = B \lor B < A))$
60	29 46 59	3jaoian	$⊢ ((A \in ℝ \lor A = +∞ \lor A = −∞) \land (B \in ℝ \lor B = +∞ \lor B = −∞)) \to (\neg A < B \to (A = B \lor B < A))$
61	11 12 60	syl2anb	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\neg A < B \to (A = B \lor B < A))$
62	10 61	impbid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A = B \lor B < A) \leftrightarrow \neg A < B)$
63	62	con2bid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \leftrightarrow \neg (A = B \lor B < A))$

Metamath Proof Explorer

Theorem xrlttri

Proof