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

Theorem mnfle 10655
Description: Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
Assertion
Ref Expression
mnfle  |-  ( A  e.  RR*  ->  -oo  <_  A )

Proof of Theorem mnfle
StepHypRef Expression
1 nltmnf 10652 . 2  |-  ( A  e.  RR*  ->  -.  A  <  -oo )
2 mnfxr 10640 . . 3  |-  -oo  e.  RR*
3 xrlenlt 9070 . . 3  |-  ( ( 
-oo  e.  RR*  /\  A  e.  RR* )  ->  (  -oo  <_  A  <->  -.  A  <  -oo ) )
42, 3mpan 652 . 2  |-  ( A  e.  RR*  ->  (  -oo  <_  A  <->  -.  A  <  -oo ) )
51, 4mpbird 224 1  |-  ( A  e.  RR*  ->  -oo  <_  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    e. wcel 1717   class class class wbr 4147    -oocmnf 9045   RR*cxr 9046    < clt 9047    <_ cle 9048
This theorem is referenced by:  ngtmnft  10681  xrre2  10684  xleadd1a  10758  xlt2add  10765  xsubge0  10766  xlesubadd  10768  xlemul1a  10793  supxrmnf  10822  elioc2  10899  iccmax  10912  xrsdsreclblem  16661  leordtvallem2  17191  lecldbas  17199  tgioo  18692  xrtgioo  18702  ioombl  19320  ismbfd  19393  degltlem1  19856  ply1rem  19947  xrdifh  23973  tpr2rico  24108  itg2gt0cn  25954  hbtlem2  26991
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 2362  ax-sep 4265  ax-nul 4273  ax-pow 4312  ax-pr 4338  ax-un 4635  ax-cnex 8973  ax-resscn 8974
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 2236  df-mo 2237  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-ne 2546  df-nel 2547  df-ral 2648  df-rex 2649  df-rab 2652  df-v 2895  df-sbc 3099  df-csb 3189  df-dif 3260  df-un 3262  df-in 3264  df-ss 3271  df-nul 3566  df-if 3677  df-pw 3738  df-sn 3757  df-pr 3758  df-op 3760  df-uni 3952  df-br 4148  df-opab 4202  df-mpt 4203  df-id 4433  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5352  df-fun 5390  df-fn 5391  df-f 5392  df-f1 5393  df-fo 5394  df-f1o 5395  df-fv 5396  df-er 6835  df-en 7040  df-dom 7041  df-sdom 7042  df-pnf 9049  df-mnf 9050  df-xr 9051  df-ltxr 9052  df-le 9053
  Copyright terms: Public domain W3C validator