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

Theorem mnflt 10712
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 2435 . . . 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 10704 . . 3  |-  -oo  e.  RR*
6 rexr 9120 . . 3  |-  ( A  e.  RR  ->  A  e.  RR* )
7 ltxr 10705 . . 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 1652    e. wcel 1725   class class class wbr 4204   RRcr 8979    <RR cltrr 8984    +oocpnf 9107    -oocmnf 9108   RR*cxr 9109    < clt 9110
This theorem is referenced by:  mnfltxr  10714  xrlttri  10722  xrlttr  10723  xrrebnd  10746  xrre3  10749  ge0gtmnf  10750  qbtwnxr  10776  xltnegi  10792  xsubge0  10830  xrsupsslem  10875  xrub  10880  supxrre  10896  infmxrre  10904  elico2  10964  elicc2  10965  ioomax  10975  elioomnf  10989  difreicc  11018  caucvgrlem  12456  leordtval2  17266  mnfnei  17275  icopnfcld  18792  iocmnfcld  18793  tgioo  18817  xrtgioo  18827  reconnlem1  18847  reconnlem2  18848  bndth  18973  ovoliunlem1  19388  ovoliun  19391  ovolicopnf  19410  voliunlem3  19436  volsup  19440  ioombl1lem2  19443  volivth  19489  mbfmax  19531  ismbf3d  19536  itg2seq  19624  itg2monolem2  19633  dvferm1lem  19858  dvferm2lem  19860  degltlem1  19985  deg1lt0  20004  ply1divex  20049  dvdsq1p  20073  plypf1  20121  ellogdm  20520  logdmnrp  20522  atans2  20761  xrge00  24198  xrge0neqmnf  24202  xrge0adddir  24205  fsumrp0cl  24207  xrge0iifcnv  24309  lmlimxrge0  24324  rge0scvg  24325  lmdvg  24328  esumfsupre  24451  esumpfinvallem  24454  esumpfinval  24455  esumpfinvalf  24456  esumpcvgval  24458  esumcvg  24466  dya2iocbrsiga  24615  dya2icobrsiga  24616  orvclteel  24720  itg2addnclem  26219  dvreasin  26243  areacirclem6  26250  hbtlem5  27264  rfcnpre4  27636  sgnmnf  28426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-cnex 9036
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-xp 4876  df-pnf 9112  df-mnf 9113  df-xr 9114  df-ltxr 9115
  Copyright terms: Public domain W3C validator