Metamath Proof Explorer


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 ( 𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴 )