Theorem xrltnr

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

	Ref	Expression
Assertion	xrltnr	⊢ ( 𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elxr	⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
2		ltnr	⊢ ( 𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴 )
3		pnfnre	⊢ +∞ ∉ ℝ
4	3	neli	⊢ ¬ +∞ ∈ ℝ
5	4	intnan	⊢ ¬ ( +∞ ∈ ℝ ∧ +∞ ∈ ℝ )
6	5	intnanr	⊢ ¬ ( ( +∞ ∈ ℝ ∧ +∞ ∈ ℝ ) ∧ +∞ <ℝ +∞ )
7		pnfnemnf	⊢ +∞ ≠ -∞
8	7	neii	⊢ ¬ +∞ = -∞
9	8	intnanr	⊢ ¬ ( +∞ = -∞ ∧ +∞ = +∞ )
10	6 9	pm3.2ni	⊢ ¬ ( ( ( +∞ ∈ ℝ ∧ +∞ ∈ ℝ ) ∧ +∞ <ℝ +∞ ) ∨ ( +∞ = -∞ ∧ +∞ = +∞ ) )
11	4	intnanr	⊢ ¬ ( +∞ ∈ ℝ ∧ +∞ = +∞ )
12	4	intnan	⊢ ¬ ( +∞ = -∞ ∧ +∞ ∈ ℝ )
13	11 12	pm3.2ni	⊢ ¬ ( ( +∞ ∈ ℝ ∧ +∞ = +∞ ) ∨ ( +∞ = -∞ ∧ +∞ ∈ ℝ ) )
14	10 13	pm3.2ni	⊢ ¬ ( ( ( ( +∞ ∈ ℝ ∧ +∞ ∈ ℝ ) ∧ +∞ <ℝ +∞ ) ∨ ( +∞ = -∞ ∧ +∞ = +∞ ) ) ∨ ( ( +∞ ∈ ℝ ∧ +∞ = +∞ ) ∨ ( +∞ = -∞ ∧ +∞ ∈ ℝ ) ) )
15		pnfxr	⊢ +∞ ∈ ℝ*
16		ltxr	⊢ ( ( +∞ ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( +∞ < +∞ ↔ ( ( ( ( +∞ ∈ ℝ ∧ +∞ ∈ ℝ ) ∧ +∞ <ℝ +∞ ) ∨ ( +∞ = -∞ ∧ +∞ = +∞ ) ) ∨ ( ( +∞ ∈ ℝ ∧ +∞ = +∞ ) ∨ ( +∞ = -∞ ∧ +∞ ∈ ℝ ) ) ) ) )
17	15 15 16	mp2an	⊢ ( +∞ < +∞ ↔ ( ( ( ( +∞ ∈ ℝ ∧ +∞ ∈ ℝ ) ∧ +∞ <ℝ +∞ ) ∨ ( +∞ = -∞ ∧ +∞ = +∞ ) ) ∨ ( ( +∞ ∈ ℝ ∧ +∞ = +∞ ) ∨ ( +∞ = -∞ ∧ +∞ ∈ ℝ ) ) ) )
18	14 17	mtbir	⊢ ¬ +∞ < +∞
19		breq12	⊢ ( ( 𝐴 = +∞ ∧ 𝐴 = +∞ ) → ( 𝐴 < 𝐴 ↔ +∞ < +∞ ) )
20	19	anidms	⊢ ( 𝐴 = +∞ → ( 𝐴 < 𝐴 ↔ +∞ < +∞ ) )
21	18 20	mtbiri	⊢ ( 𝐴 = +∞ → ¬ 𝐴 < 𝐴 )
22		mnfnre	⊢ -∞ ∉ ℝ
23	22	neli	⊢ ¬ -∞ ∈ ℝ
24	23	intnan	⊢ ¬ ( -∞ ∈ ℝ ∧ -∞ ∈ ℝ )
25	24	intnanr	⊢ ¬ ( ( -∞ ∈ ℝ ∧ -∞ ∈ ℝ ) ∧ -∞ <ℝ -∞ )
26	7	nesymi	⊢ ¬ -∞ = +∞
27	26	intnan	⊢ ¬ ( -∞ = -∞ ∧ -∞ = +∞ )
28	25 27	pm3.2ni	⊢ ¬ ( ( ( -∞ ∈ ℝ ∧ -∞ ∈ ℝ ) ∧ -∞ <ℝ -∞ ) ∨ ( -∞ = -∞ ∧ -∞ = +∞ ) )
29	23	intnanr	⊢ ¬ ( -∞ ∈ ℝ ∧ -∞ = +∞ )
30	23	intnan	⊢ ¬ ( -∞ = -∞ ∧ -∞ ∈ ℝ )
31	29 30	pm3.2ni	⊢ ¬ ( ( -∞ ∈ ℝ ∧ -∞ = +∞ ) ∨ ( -∞ = -∞ ∧ -∞ ∈ ℝ ) )
32	28 31	pm3.2ni	⊢ ¬ ( ( ( ( -∞ ∈ ℝ ∧ -∞ ∈ ℝ ) ∧ -∞ <ℝ -∞ ) ∨ ( -∞ = -∞ ∧ -∞ = +∞ ) ) ∨ ( ( -∞ ∈ ℝ ∧ -∞ = +∞ ) ∨ ( -∞ = -∞ ∧ -∞ ∈ ℝ ) ) )
33		mnfxr	⊢ -∞ ∈ ℝ*
34		ltxr	⊢ ( ( -∞ ∈ ℝ* ∧ -∞ ∈ ℝ* ) → ( -∞ < -∞ ↔ ( ( ( ( -∞ ∈ ℝ ∧ -∞ ∈ ℝ ) ∧ -∞ <ℝ -∞ ) ∨ ( -∞ = -∞ ∧ -∞ = +∞ ) ) ∨ ( ( -∞ ∈ ℝ ∧ -∞ = +∞ ) ∨ ( -∞ = -∞ ∧ -∞ ∈ ℝ ) ) ) ) )
35	33 33 34	mp2an	⊢ ( -∞ < -∞ ↔ ( ( ( ( -∞ ∈ ℝ ∧ -∞ ∈ ℝ ) ∧ -∞ <ℝ -∞ ) ∨ ( -∞ = -∞ ∧ -∞ = +∞ ) ) ∨ ( ( -∞ ∈ ℝ ∧ -∞ = +∞ ) ∨ ( -∞ = -∞ ∧ -∞ ∈ ℝ ) ) ) )
36	32 35	mtbir	⊢ ¬ -∞ < -∞
37		breq12	⊢ ( ( 𝐴 = -∞ ∧ 𝐴 = -∞ ) → ( 𝐴 < 𝐴 ↔ -∞ < -∞ ) )
38	37	anidms	⊢ ( 𝐴 = -∞ → ( 𝐴 < 𝐴 ↔ -∞ < -∞ ) )
39	36 38	mtbiri	⊢ ( 𝐴 = -∞ → ¬ 𝐴 < 𝐴 )
40	2 21 39	3jaoi	⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) → ¬ 𝐴 < 𝐴 )
41	1 40	sylbi	⊢ ( 𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴 )