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

Theorem mnflt 11995
Description: Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
mnflt (𝐴 ∈ ℝ → -∞ < 𝐴)

Proof of Theorem mnflt
StepHypRef Expression
1 eqid 2651 . . . 4 -∞ = -∞
2 olc 398 . . . 4 ((-∞ = -∞ ∧ 𝐴 ∈ ℝ) → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
31, 2mpan 706 . . 3 (𝐴 ∈ ℝ → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
43olcd 407 . 2 (𝐴 ∈ ℝ → ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ < 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))))
5 mnfxr 10134 . . 3 -∞ ∈ ℝ*
6 rexr 10123 . . 3 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
7 ltxr 11987 . . 3 ((-∞ ∈ ℝ*𝐴 ∈ ℝ*) → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ < 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
85, 6, 7sylancr 696 . 2 (𝐴 ∈ ℝ → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ < 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
94, 8mpbird 247 1 (𝐴 ∈ ℝ → -∞ < 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030   class class class wbr 4685  cr 9973   < cltrr 9978  +∞cpnf 10109  -∞cmnf 10110  *cxr 10111   < clt 10112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-xp 5149  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117
This theorem is referenced by:  mnfltd  11996  mnflt0  11997  mnfltxr  11999  xrlttri  12010  xrlttr  12011  xrrebnd  12037  xrre3  12040  qbtwnxr  12069  xltnegi  12085  xrsupsslem  12175  xrub  12180  supxrre  12195  elico2  12275  elicc2  12276  ioomax  12286  elioomnf  12306  difreicc  12342  icopnfcld  22618  iocmnfcld  22619  tgioo  22646  xrtgioo  22656  reconnlem1  22676  reconnlem2  22677  bndth  22804  ovoliunlem1  23316  ovoliun  23319  ioombl1lem2  23373  mbfmax  23461  ismbf3d  23466  itg2seq  23554  dvferm1lem  23792  dvferm2lem  23794  degltlem1  23877  ply1divex  23941  dvdsq1p  23965  ellogdm  24430  logdmnrp  24432  atans2  24703  esumcvgsum  30278  dya2iocbrsiga  30465  dya2icobrsiga  30466  orvclteel  30662  iooelexlt  33340  itg2addnclem  33591  asindmre  33625  dvasin  33626  dvacos  33627  rfcnpre4  39507  infrpge  39880  infxr  39896  infxrunb2  39897  infleinflem2  39900  icccncfext  40418  fourierdlem113  40754  fouriersw  40766  iccpartigtl  41684
  Copyright terms: Public domain W3C validator