xrltnr

Description: The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005)

		Ref	Expression
	Assertion	xrltnr	$⊢ A \in ℝ^{*} \to \neg A < A$

Proof

Step	Hyp	Ref	Expression
1		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
2		ltnr	$⊢ A \in ℝ \to \neg A < A$
3		pnfnre	$⊢ +∞ \notin ℝ$
4	3	neli	$⊢ \neg +∞ \in ℝ$
5	4	intnan	$⊢ \neg (+∞ \in ℝ \land +∞ \in ℝ)$
6	5	intnanr	$⊢ \neg ((+∞ \in ℝ \land +∞ \in ℝ) \land +∞ <_{ℝ} +∞)$
7		pnfnemnf	$⊢ +∞ \neq −∞$
8	7	neii	$⊢ \neg +∞ = −∞$
9	8	intnanr	$⊢ \neg (+∞ = −∞ \land +∞ = +∞)$
10	6 9	pm3.2ni	$⊢ \neg (((+∞ \in ℝ \land +∞ \in ℝ) \land +∞ <_{ℝ} +∞) \lor (+∞ = −∞ \land +∞ = +∞))$
11	4	intnanr	$⊢ \neg (+∞ \in ℝ \land +∞ = +∞)$
12	4	intnan	$⊢ \neg (+∞ = −∞ \land +∞ \in ℝ)$
13	11 12	pm3.2ni	$⊢ \neg ((+∞ \in ℝ \land +∞ = +∞) \lor (+∞ = −∞ \land +∞ \in ℝ))$
14	10 13	pm3.2ni	$⊢ \neg ((((+∞ \in ℝ \land +∞ \in ℝ) \land +∞ <_{ℝ} +∞) \lor (+∞ = −∞ \land +∞ = +∞)) \lor ((+∞ \in ℝ \land +∞ = +∞) \lor (+∞ = −∞ \land +∞ \in ℝ)))$
15		pnfxr	$⊢ +∞ \in ℝ^{*}$
16		ltxr	$⊢ (+∞ \in ℝ^{} \land +∞ \in ℝ^{}) \to (+∞ < +∞ \leftrightarrow ((((+∞ \in ℝ \land +∞ \in ℝ) \land +∞ <_{ℝ} +∞) \lor (+∞ = −∞ \land +∞ = +∞)) \lor ((+∞ \in ℝ \land +∞ = +∞) \lor (+∞ = −∞ \land +∞ \in ℝ))))$
17	15 15 16	mp2an	$⊢ +∞ < +∞ \leftrightarrow ((((+∞ \in ℝ \land +∞ \in ℝ) \land +∞ <_{ℝ} +∞) \lor (+∞ = −∞ \land +∞ = +∞)) \lor ((+∞ \in ℝ \land +∞ = +∞) \lor (+∞ = −∞ \land +∞ \in ℝ)))$
18	14 17	mtbir	$⊢ \neg +∞ < +∞$
19		breq12	$⊢ (A = +∞ \land A = +∞) \to (A < A \leftrightarrow +∞ < +∞)$
20	19	anidms	$⊢ A = +∞ \to (A < A \leftrightarrow +∞ < +∞)$
21	18 20	mtbiri	$⊢ A = +∞ \to \neg A < A$
22		mnfnre	$⊢ −∞ \notin ℝ$
23	22	neli	$⊢ \neg −∞ \in ℝ$
24	23	intnan	$⊢ \neg (−∞ \in ℝ \land −∞ \in ℝ)$
25	24	intnanr	$⊢ \neg ((−∞ \in ℝ \land −∞ \in ℝ) \land −∞ <_{ℝ} −∞)$
26	7	nesymi	$⊢ \neg −∞ = +∞$
27	26	intnan	$⊢ \neg (−∞ = −∞ \land −∞ = +∞)$
28	25 27	pm3.2ni	$⊢ \neg (((−∞ \in ℝ \land −∞ \in ℝ) \land −∞ <_{ℝ} −∞) \lor (−∞ = −∞ \land −∞ = +∞))$
29	23	intnanr	$⊢ \neg (−∞ \in ℝ \land −∞ = +∞)$
30	23	intnan	$⊢ \neg (−∞ = −∞ \land −∞ \in ℝ)$
31	29 30	pm3.2ni	$⊢ \neg ((−∞ \in ℝ \land −∞ = +∞) \lor (−∞ = −∞ \land −∞ \in ℝ))$
32	28 31	pm3.2ni	$⊢ \neg ((((−∞ \in ℝ \land −∞ \in ℝ) \land −∞ <_{ℝ} −∞) \lor (−∞ = −∞ \land −∞ = +∞)) \lor ((−∞ \in ℝ \land −∞ = +∞) \lor (−∞ = −∞ \land −∞ \in ℝ)))$
33		mnfxr	$⊢ −∞ \in ℝ^{*}$
34		ltxr	$⊢ (−∞ \in ℝ^{} \land −∞ \in ℝ^{}) \to (−∞ < −∞ \leftrightarrow ((((−∞ \in ℝ \land −∞ \in ℝ) \land −∞ <_{ℝ} −∞) \lor (−∞ = −∞ \land −∞ = +∞)) \lor ((−∞ \in ℝ \land −∞ = +∞) \lor (−∞ = −∞ \land −∞ \in ℝ))))$
35	33 33 34	mp2an	$⊢ −∞ < −∞ \leftrightarrow ((((−∞ \in ℝ \land −∞ \in ℝ) \land −∞ <_{ℝ} −∞) \lor (−∞ = −∞ \land −∞ = +∞)) \lor ((−∞ \in ℝ \land −∞ = +∞) \lor (−∞ = −∞ \land −∞ \in ℝ)))$
36	32 35	mtbir	$⊢ \neg −∞ < −∞$
37		breq12	$⊢ (A = −∞ \land A = −∞) \to (A < A \leftrightarrow −∞ < −∞)$
38	37	anidms	$⊢ A = −∞ \to (A < A \leftrightarrow −∞ < −∞)$
39	36 38	mtbiri	$⊢ A = −∞ \to \neg A < A$
40	2 21 39	3jaoi	$⊢ (A \in ℝ \lor A = +∞ \lor A = −∞) \to \neg A < A$
41	1 40	sylbi	$⊢ A \in ℝ^{*} \to \neg A < A$

Metamath Proof Explorer

Theorem xrltnr

Proof