MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrltnr Structured version   Visualization version   GIF version

Theorem xrltnr 12511
Description: The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
xrltnr (𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴)

Proof of Theorem xrltnr
StepHypRef Expression
1 elxr 12508 . 2 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2 ltnr 10733 . . 3 (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
3 pnfnre 10680 . . . . . . . . . 10 +∞ ∉ ℝ
43neli 3120 . . . . . . . . 9 ¬ +∞ ∈ ℝ
54intnan 490 . . . . . . . 8 ¬ (+∞ ∈ ℝ ∧ +∞ ∈ ℝ)
65intnanr 491 . . . . . . 7 ¬ ((+∞ ∈ ℝ ∧ +∞ ∈ ℝ) ∧ +∞ < +∞)
7 pnfnemnf 10694 . . . . . . . . 9 +∞ ≠ -∞
87neii 3016 . . . . . . . 8 ¬ +∞ = -∞
98intnanr 491 . . . . . . 7 ¬ (+∞ = -∞ ∧ +∞ = +∞)
106, 9pm3.2ni 878 . . . . . 6 ¬ (((+∞ ∈ ℝ ∧ +∞ ∈ ℝ) ∧ +∞ < +∞) ∨ (+∞ = -∞ ∧ +∞ = +∞))
114intnanr 491 . . . . . . 7 ¬ (+∞ ∈ ℝ ∧ +∞ = +∞)
124intnan 490 . . . . . . 7 ¬ (+∞ = -∞ ∧ +∞ ∈ ℝ)
1311, 12pm3.2ni 878 . . . . . 6 ¬ ((+∞ ∈ ℝ ∧ +∞ = +∞) ∨ (+∞ = -∞ ∧ +∞ ∈ ℝ))
1410, 13pm3.2ni 878 . . . . 5 ¬ ((((+∞ ∈ ℝ ∧ +∞ ∈ ℝ) ∧ +∞ < +∞) ∨ (+∞ = -∞ ∧ +∞ = +∞)) ∨ ((+∞ ∈ ℝ ∧ +∞ = +∞) ∨ (+∞ = -∞ ∧ +∞ ∈ ℝ)))
15 pnfxr 10693 . . . . . 6 +∞ ∈ ℝ*
16 ltxr 12507 . . . . . 6 ((+∞ ∈ ℝ* ∧ +∞ ∈ ℝ*) → (+∞ < +∞ ↔ ((((+∞ ∈ ℝ ∧ +∞ ∈ ℝ) ∧ +∞ < +∞) ∨ (+∞ = -∞ ∧ +∞ = +∞)) ∨ ((+∞ ∈ ℝ ∧ +∞ = +∞) ∨ (+∞ = -∞ ∧ +∞ ∈ ℝ)))))
1715, 15, 16mp2an 691 . . . . 5 (+∞ < +∞ ↔ ((((+∞ ∈ ℝ ∧ +∞ ∈ ℝ) ∧ +∞ < +∞) ∨ (+∞ = -∞ ∧ +∞ = +∞)) ∨ ((+∞ ∈ ℝ ∧ +∞ = +∞) ∨ (+∞ = -∞ ∧ +∞ ∈ ℝ))))
1814, 17mtbir 326 . . . 4 ¬ +∞ < +∞
19 breq12 5057 . . . . 5 ((𝐴 = +∞ ∧ 𝐴 = +∞) → (𝐴 < 𝐴 ↔ +∞ < +∞))
2019anidms 570 . . . 4 (𝐴 = +∞ → (𝐴 < 𝐴 ↔ +∞ < +∞))
2118, 20mtbiri 330 . . 3 (𝐴 = +∞ → ¬ 𝐴 < 𝐴)
22 mnfnre 10682 . . . . . . . . . 10 -∞ ∉ ℝ
2322neli 3120 . . . . . . . . 9 ¬ -∞ ∈ ℝ
2423intnan 490 . . . . . . . 8 ¬ (-∞ ∈ ℝ ∧ -∞ ∈ ℝ)
2524intnanr 491 . . . . . . 7 ¬ ((-∞ ∈ ℝ ∧ -∞ ∈ ℝ) ∧ -∞ < -∞)
267nesymi 3071 . . . . . . . 8 ¬ -∞ = +∞
2726intnan 490 . . . . . . 7 ¬ (-∞ = -∞ ∧ -∞ = +∞)
2825, 27pm3.2ni 878 . . . . . 6 ¬ (((-∞ ∈ ℝ ∧ -∞ ∈ ℝ) ∧ -∞ < -∞) ∨ (-∞ = -∞ ∧ -∞ = +∞))
2923intnanr 491 . . . . . . 7 ¬ (-∞ ∈ ℝ ∧ -∞ = +∞)
3023intnan 490 . . . . . . 7 ¬ (-∞ = -∞ ∧ -∞ ∈ ℝ)
3129, 30pm3.2ni 878 . . . . . 6 ¬ ((-∞ ∈ ℝ ∧ -∞ = +∞) ∨ (-∞ = -∞ ∧ -∞ ∈ ℝ))
3228, 31pm3.2ni 878 . . . . 5 ¬ ((((-∞ ∈ ℝ ∧ -∞ ∈ ℝ) ∧ -∞ < -∞) ∨ (-∞ = -∞ ∧ -∞ = +∞)) ∨ ((-∞ ∈ ℝ ∧ -∞ = +∞) ∨ (-∞ = -∞ ∧ -∞ ∈ ℝ)))
33 mnfxr 10696 . . . . . 6 -∞ ∈ ℝ*
34 ltxr 12507 . . . . . 6 ((-∞ ∈ ℝ* ∧ -∞ ∈ ℝ*) → (-∞ < -∞ ↔ ((((-∞ ∈ ℝ ∧ -∞ ∈ ℝ) ∧ -∞ < -∞) ∨ (-∞ = -∞ ∧ -∞ = +∞)) ∨ ((-∞ ∈ ℝ ∧ -∞ = +∞) ∨ (-∞ = -∞ ∧ -∞ ∈ ℝ)))))
3533, 33, 34mp2an 691 . . . . 5 (-∞ < -∞ ↔ ((((-∞ ∈ ℝ ∧ -∞ ∈ ℝ) ∧ -∞ < -∞) ∨ (-∞ = -∞ ∧ -∞ = +∞)) ∨ ((-∞ ∈ ℝ ∧ -∞ = +∞) ∨ (-∞ = -∞ ∧ -∞ ∈ ℝ))))
3632, 35mtbir 326 . . . 4 ¬ -∞ < -∞
37 breq12 5057 . . . . 5 ((𝐴 = -∞ ∧ 𝐴 = -∞) → (𝐴 < 𝐴 ↔ -∞ < -∞))
3837anidms 570 . . . 4 (𝐴 = -∞ → (𝐴 < 𝐴 ↔ -∞ < -∞))
3936, 38mtbiri 330 . . 3 (𝐴 = -∞ → ¬ 𝐴 < 𝐴)
402, 21, 393jaoi 1424 . 2 ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → ¬ 𝐴 < 𝐴)
411, 40sylbi 220 1 (𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3o 1083   = wceq 1538  wcel 2115   class class class wbr 5052  cr 10534   < cltrr 10539  +∞cpnf 10670  -∞cmnf 10671  *cxr 10672   < clt 10673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-cnex 10591  ax-resscn 10592  ax-pre-lttri 10609  ax-pre-lttrn 10610
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-po 5461  df-so 5462  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-er 8285  df-en 8506  df-dom 8507  df-sdom 8508  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678
This theorem is referenced by:  xrltnsym  12527  xrlttri  12529  nltpnft  12554  ngtmnft  12556  xrsupsslem  12697  xrinfmsslem  12698  xrub  12702  lbioo  12766  ubioo  12767  topnfbey  28260  lbioc  42080  icoub  42093  iccpartnel  43885
  Copyright terms: Public domain W3C validator