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

Theorem mnflt 11371
Description: Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
mnflt  |-  ( A  e.  RR  -> -oo  <  A )

Proof of Theorem mnflt
StepHypRef Expression
1 eqid 2423 . . . 4  |- -oo  = -oo
2 olc 385 . . . 4  |-  ( ( -oo  = -oo  /\  A  e.  RR )  ->  ( ( -oo  e.  RR  /\  A  = +oo )  \/  ( -oo  = -oo  /\  A  e.  RR ) ) )
31, 2mpan 674 . . 3  |-  ( A  e.  RR  ->  (
( -oo  e.  RR  /\  A  = +oo )  \/  ( -oo  = -oo  /\  A  e.  RR ) ) )
43olcd 394 . 2  |-  ( A  e.  RR  ->  (
( ( ( -oo  e.  RR  /\  A  e.  RR )  /\ -oo  <RR  A )  \/  ( -oo  = -oo  /\  A  = +oo ) )  \/  ( ( -oo  e.  RR  /\  A  = +oo )  \/  ( -oo  = -oo  /\  A  e.  RR ) ) ) )
5 mnfxr 11360 . . 3  |- -oo  e.  RR*
6 rexr 9632 . . 3  |-  ( A  e.  RR  ->  A  e.  RR* )
7 ltxr 11361 . . 3  |-  ( ( -oo  e.  RR*  /\  A  e.  RR* )  ->  ( -oo  <  A  <->  ( (
( ( -oo  e.  RR  /\  A  e.  RR )  /\ -oo  <RR  A )  \/  ( -oo  = -oo  /\  A  = +oo ) )  \/  (
( -oo  e.  RR  /\  A  = +oo )  \/  ( -oo  = -oo  /\  A  e.  RR ) ) ) ) )
85, 6, 7sylancr 667 . 2  |-  ( A  e.  RR  ->  ( -oo  <  A  <->  ( (
( ( -oo  e.  RR  /\  A  e.  RR )  /\ -oo  <RR  A )  \/  ( -oo  = -oo  /\  A  = +oo ) )  \/  (
( -oo  e.  RR  /\  A  = +oo )  \/  ( -oo  = -oo  /\  A  e.  RR ) ) ) ) )
94, 8mpbird 235 1  |-  ( A  e.  RR  -> -oo  <  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    = wceq 1437    e. wcel 1872   class class class wbr 4361   RRcr 9484    <RR cltrr 9489   +oocpnf 9618   -oocmnf 9619   RR*cxr 9620    < clt 9621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-xp 4797  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626
This theorem is referenced by:  mnfltd  11372  mnflt0  11373  mnfltxr  11375  xrlttri  11384  xrlttr  11385  xrrebnd  11409  xrre3  11412  qbtwnxr  11439  xltnegi  11455  xrsupsslem  11538  xrub  11543  supxrre  11559  infmxrreOLD  11572  elico2  11644  elicc2  11645  ioomax  11655  elioomnf  11675  difreicc  11710  caucvgrlemOLD  13675  icopnfcld  21725  iocmnfcld  21726  tgioo  21751  xrtgioo  21761  reconnlem1  21781  reconnlem2  21782  bndth  21923  ovoliunlem1  22392  ovoliun  22395  ioombl1lem2  22449  mbfmax  22542  ismbf3d  22547  itg2seq  22637  dvferm1lem  22873  dvferm2lem  22875  degltlem1  22958  ply1divex  23024  dvdsq1p  23048  ellogdm  23521  logdmnrp  23523  atans2  23794  esumcvgsum  28856  dya2iocbrsiga  29044  dya2icobrsiga  29045  orvclteel  29252  iooelexlt  31672  itg2addnclem  31900  asindmre  31934  dvasin  31935  dvacos  31936  areacirclem5  31943  rfcnpre4  37271  infrpge  37471  icccncfext  37648  fourierdlem113  37966  fouriersw  37978  iccpartigtl  38550
  Copyright terms: Public domain W3C validator