This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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