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

Theorem mnflt 10655
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 2388 . . . 4  |-  -oo  =  -oo
2 olc 374 . . . 4  |-  ( ( 
-oo  =  -oo  /\  A  e.  RR )  ->  ( (  -oo  e.  RR  /\  A  =  +oo )  \/  (  -oo  =  -oo  /\  A  e.  RR ) ) )
31, 2mpan 652 . . 3  |-  ( A  e.  RR  ->  (
(  -oo  e.  RR  /\  A  =  +oo )  \/  (  -oo  =  -oo  /\  A  e.  RR ) ) )
43olcd 383 . 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 10647 . . 3  |-  -oo  e.  RR*
6 rexr 9064 . . 3  |-  ( A  e.  RR  ->  A  e.  RR* )
7 ltxr 10648 . . 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 645 . 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 224 1  |-  ( A  e.  RR  ->  -oo  <  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    = wceq 1649    e. wcel 1717   class class class wbr 4154   RRcr 8923    <RR cltrr 8928    +oocpnf 9051    -oocmnf 9052   RR*cxr 9053    < clt 9054
This theorem is referenced by:  mnfltxr  10657  xrlttri  10665  xrlttr  10666  xrrebnd  10689  xrre3  10692  ge0gtmnf  10693  qbtwnxr  10719  xltnegi  10735  xsubge0  10773  xrsupsslem  10818  xrub  10823  supxrre  10839  infmxrre  10847  elico2  10907  elicc2  10908  ioomax  10918  elioomnf  10932  difreicc  10961  caucvgrlem  12394  leordtval2  17199  mnfnei  17208  icopnfcld  18674  iocmnfcld  18675  tgioo  18699  xrtgioo  18709  reconnlem1  18729  reconnlem2  18730  bndth  18855  ovoliunlem1  19266  ovoliun  19269  ovolicopnf  19288  voliunlem3  19314  volsup  19318  ioombl1lem2  19321  volivth  19367  mbfmax  19409  ismbf3d  19414  itg2seq  19502  itg2monolem2  19511  dvferm1lem  19736  dvferm2lem  19738  degltlem1  19863  deg1lt0  19882  ply1divex  19927  dvdsq1p  19951  plypf1  19999  ellogdm  20398  logdmnrp  20400  atans2  20639  xrge00  24038  xrge0neqmnf  24042  xrge0adddir  24045  fsumrp0cl  24047  xrge0iifcnv  24124  lmlimxrge0  24139  rge0scvg  24140  lmdvg  24143  esumfsupre  24258  esumpfinvallem  24261  esumpfinval  24262  esumpfinvalf  24263  esumpcvgval  24265  esumcvg  24273  dya2iocbrsiga  24420  dya2icobrsiga  24421  orvclteel  24510  itg2addnclem  25958  dvreasin  25981  areacirclem6  25988  hbtlem5  27002  rfcnpre4  27374  sgnmnf  27872
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pow 4319  ax-pr 4345  ax-un 4642  ax-cnex 8980
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-pw 3745  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-opab 4209  df-xp 4825  df-pnf 9056  df-mnf 9057  df-xr 9058  df-ltxr 9059
  Copyright terms: Public domain W3C validator