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

Theorem mnflt 11358
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 2457 . . . 4  |- -oo  = -oo
2 olc 384 . . . 4  |-  ( ( -oo  = -oo  /\  A  e.  RR )  ->  ( ( -oo  e.  RR  /\  A  = +oo )  \/  ( -oo  = -oo  /\  A  e.  RR ) ) )
31, 2mpan 670 . . 3  |-  ( A  e.  RR  ->  (
( -oo  e.  RR  /\  A  = +oo )  \/  ( -oo  = -oo  /\  A  e.  RR ) ) )
43olcd 393 . 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 11348 . . 3  |- -oo  e.  RR*
6 rexr 9656 . . 3  |-  ( A  e.  RR  ->  A  e.  RR* )
7 ltxr 11349 . . 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 663 . 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 232 1  |-  ( A  e.  RR  -> -oo  <  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1395    e. wcel 1819   class class class wbr 4456   RRcr 9508    <RR cltrr 9513   +oocpnf 9642   -oocmnf 9643   RR*cxr 9644    < clt 9645
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-cnex 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-xp 5014  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650
This theorem is referenced by:  mnflt0  11359  mnfltxr  11361  xrlttri  11370  xrlttr  11371  xrrebnd  11394  xrre3  11397  qbtwnxr  11424  xltnegi  11440  xrsupsslem  11523  xrub  11528  supxrre  11544  infmxrre  11552  elico2  11613  elicc2  11614  ioomax  11624  elioomnf  11644  difreicc  11677  caucvgrlem  13506  icopnfcld  21400  iocmnfcld  21401  tgioo  21426  xrtgioo  21436  reconnlem1  21456  reconnlem2  21457  bndth  21583  ovoliunlem1  22038  ovoliun  22041  ioombl1lem2  22094  mbfmax  22181  ismbf3d  22186  itg2seq  22274  dvferm1lem  22510  dvferm2lem  22512  degltlem1  22597  ply1divex  22662  dvdsq1p  22686  ellogdm  23145  logdmnrp  23147  atans2  23387  esumcvgsum  28250  dya2iocbrsiga  28407  dya2icobrsiga  28408  orvclteel  28586  itg2addnclem  30228  asindmre  30264  dvasin  30265  dvacos  30266  areacirclem5  30273  rfcnpre4  31570  mnfltd  31652  icccncfext  31851  fourierdlem113  32163  fouriersw  32175
  Copyright terms: Public domain W3C validator