xrltnsym

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

		Ref	Expression
	Assertion	xrltnsym	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \to \neg B < A)$

Proof

Step	Hyp	Ref	Expression
1		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
2		elxr	$⊢ B \in ℝ^{*} \leftrightarrow (B \in ℝ \lor B = +∞ \lor B = −∞)$
3		ltnsym	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \to \neg B < A)$
4		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
5		pnfnlt	$⊢ A \in ℝ^{*} \to \neg +∞ < A$
6	4 5	syl	$⊢ A \in ℝ \to \neg +∞ < A$
7	6	adantr	$⊢ (A \in ℝ \land B = +∞) \to \neg +∞ < A$
8		breq1	$⊢ B = +∞ \to (B < A \leftrightarrow +∞ < A)$
9	8	adantl	$⊢ (A \in ℝ \land B = +∞) \to (B < A \leftrightarrow +∞ < A)$
10	7 9	mtbird	$⊢ (A \in ℝ \land B = +∞) \to \neg B < A$
11	10	a1d	$⊢ (A \in ℝ \land B = +∞) \to (A < B \to \neg B < A)$
12		nltmnf	$⊢ A \in ℝ^{*} \to \neg A < −∞$
13	4 12	syl	$⊢ A \in ℝ \to \neg A < −∞$
14	13	adantr	$⊢ (A \in ℝ \land B = −∞) \to \neg A < −∞$
15		breq2	$⊢ B = −∞ \to (A < B \leftrightarrow A < −∞)$
16	15	adantl	$⊢ (A \in ℝ \land B = −∞) \to (A < B \leftrightarrow A < −∞)$
17	14 16	mtbird	$⊢ (A \in ℝ \land B = −∞) \to \neg A < B$
18	17	pm2.21d	$⊢ (A \in ℝ \land B = −∞) \to (A < B \to \neg B < A)$
19	3 11 18	3jaodan	$⊢ (A \in ℝ \land (B \in ℝ \lor B = +∞ \lor B = −∞)) \to (A < B \to \neg B < A)$
20		pnfnlt	$⊢ B \in ℝ^{*} \to \neg +∞ < B$
21	20	adantl	$⊢ (A = +∞ \land B \in ℝ^{*}) \to \neg +∞ < B$
22		breq1	$⊢ A = +∞ \to (A < B \leftrightarrow +∞ < B)$
23	22	adantr	$⊢ (A = +∞ \land B \in ℝ^{*}) \to (A < B \leftrightarrow +∞ < B)$
24	21 23	mtbird	$⊢ (A = +∞ \land B \in ℝ^{*}) \to \neg A < B$
25	24	pm2.21d	$⊢ (A = +∞ \land B \in ℝ^{*}) \to (A < B \to \neg B < A)$
26	2 25	sylan2br	$⊢ (A = +∞ \land (B \in ℝ \lor B = +∞ \lor B = −∞)) \to (A < B \to \neg B < A)$
27		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
28		nltmnf	$⊢ B \in ℝ^{*} \to \neg B < −∞$
29	27 28	syl	$⊢ B \in ℝ \to \neg B < −∞$
30	29	adantl	$⊢ (A = −∞ \land B \in ℝ) \to \neg B < −∞$
31		breq2	$⊢ A = −∞ \to (B < A \leftrightarrow B < −∞)$
32	31	adantr	$⊢ (A = −∞ \land B \in ℝ) \to (B < A \leftrightarrow B < −∞)$
33	30 32	mtbird	$⊢ (A = −∞ \land B \in ℝ) \to \neg B < A$
34	33	a1d	$⊢ (A = −∞ \land B \in ℝ) \to (A < B \to \neg B < A)$
35		mnfxr	$⊢ −∞ \in ℝ^{*}$
36		pnfnlt	$⊢ −∞ \in ℝ^{*} \to \neg +∞ < −∞$
37	35 36	ax-mp	$⊢ \neg +∞ < −∞$
38		breq12	$⊢ (B = +∞ \land A = −∞) \to (B < A \leftrightarrow +∞ < −∞)$
39	37 38	mtbiri	$⊢ (B = +∞ \land A = −∞) \to \neg B < A$
40	39	ancoms	$⊢ (A = −∞ \land B = +∞) \to \neg B < A$
41	40	a1d	$⊢ (A = −∞ \land B = +∞) \to (A < B \to \neg B < A)$
42		xrltnr	$⊢ −∞ \in ℝ^{*} \to \neg −∞ < −∞$
43	35 42	ax-mp	$⊢ \neg −∞ < −∞$
44		breq12	$⊢ (A = −∞ \land B = −∞) \to (A < B \leftrightarrow −∞ < −∞)$
45	43 44	mtbiri	$⊢ (A = −∞ \land B = −∞) \to \neg A < B$
46	45	pm2.21d	$⊢ (A = −∞ \land B = −∞) \to (A < B \to \neg B < A)$
47	34 41 46	3jaodan	$⊢ (A = −∞ \land (B \in ℝ \lor B = +∞ \lor B = −∞)) \to (A < B \to \neg B < A)$
48	19 26 47	3jaoian	$⊢ ((A \in ℝ \lor A = +∞ \lor A = −∞) \land (B \in ℝ \lor B = +∞ \lor B = −∞)) \to (A < B \to \neg B < A)$
49	1 2 48	syl2anb	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \to \neg B < A)$

Metamath Proof Explorer

Theorem xrltnsym

Proof