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

Theorem ltpnf 11102
Description: Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
ltpnf  |-  ( A  e.  RR  ->  A  < +oo )

Proof of Theorem ltpnf
StepHypRef Expression
1 eqid 2443 . . . 4  |- +oo  = +oo
2 orc 385 . . . 4  |-  ( ( A  e.  RR  /\ +oo  = +oo )  -> 
( ( A  e.  RR  /\ +oo  = +oo )  \/  ( A  = -oo  /\ +oo  e.  RR ) ) )
31, 2mpan2 671 . . 3  |-  ( A  e.  RR  ->  (
( A  e.  RR  /\ +oo  = +oo )  \/  ( A  = -oo  /\ +oo  e.  RR ) ) )
43olcd 393 . 2  |-  ( A  e.  RR  ->  (
( ( ( A  e.  RR  /\ +oo  e.  RR )  /\  A  <RR +oo )  \/  ( A  = -oo  /\ +oo  = +oo ) )  \/  ( ( A  e.  RR  /\ +oo  = +oo )  \/  ( A  = -oo  /\ +oo  e.  RR ) ) ) )
5 rexr 9429 . . 3  |-  ( A  e.  RR  ->  A  e.  RR* )
6 pnfxr 11092 . . 3  |- +oo  e.  RR*
7 ltxr 11095 . . 3  |-  ( ( A  e.  RR*  /\ +oo  e.  RR* )  ->  ( A  < +oo  <->  ( ( ( ( A  e.  RR  /\ +oo  e.  RR )  /\  A  <RR +oo )  \/  ( A  = -oo  /\ +oo  = +oo ) )  \/  ( ( A  e.  RR  /\ +oo  = +oo )  \/  ( A  = -oo  /\ +oo  e.  RR ) ) ) ) )
85, 6, 7sylancl 662 . 2  |-  ( A  e.  RR  ->  ( A  < +oo  <->  ( ( ( ( A  e.  RR  /\ +oo  e.  RR )  /\  A  <RR +oo )  \/  ( A  = -oo  /\ +oo  = +oo ) )  \/  ( ( A  e.  RR  /\ +oo  = +oo )  \/  ( A  = -oo  /\ +oo  e.  RR ) ) ) ) )
94, 8mpbird 232 1  |-  ( A  e.  RR  ->  A  < +oo )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1369    e. wcel 1756   class class class wbr 4292   RRcr 9281    <RR cltrr 9286   +oocpnf 9415   -oocmnf 9416   RR*cxr 9417    < clt 9418
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372  ax-cnex 9338
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-xp 4846  df-pnf 9420  df-xr 9422  df-ltxr 9423
This theorem is referenced by:  0ltpnf  11103  xrlttri  11116  xrlttr  11117  xrrebnd  11140  xrre  11141  qbtwnxr  11170  xltnegi  11186  xrinfmsslem  11270  xrub  11274  supxrunb1  11282  supxrunb2  11283  elioc2  11358  elicc2  11360  ioomax  11370  ioopos  11372  elioopnf  11383  elicopnf  11385  difreicc  11417  hashbnd  12109  hashnnn0genn0  12114  hashv01gt1  12116  limsupgre  12959  pcadd  13951  ramubcl  14079  rge0srg  17882  mnfnei  18825  xblss2ps  19976  icopnfcld  20347  iocmnfcld  20348  blcvx  20375  xrtgioo  20383  reconnlem1  20403  xrge0tsms  20411  iccpnfhmeo  20517  ioombl1lem4  21042  icombl1  21044  uniioombllem1  21061  mbfmax  21127  ismbf3d  21132  mbflimsup  21144  itg2seq  21220  lhop2  21487  dvfsumlem2  21499  logccv  22108  xrlimcnp  22362  pntleme  22857  umgrafi  23256  isblo3i  24201  htthlem  24319  xlt2addrd  26051  fsumrp0cl  26158  pnfinf  26200  xrge0tsmsd  26253  xrge0slmod  26312  xrge0iifcnv  26363  xrge0iifiso  26365  xrge0iifhom  26367  lmxrge0  26382  esumcst  26514  voliune  26645  volfiniune  26646  sxbrsigalem0  26686  orvcgteel  26850  dstfrvclim1  26860  itg2addnclem2  28444  asindmre  28479  dvasin  28480  dvacos  28481  rfcnpre3  29755  frgrawopreglem2  30638
  Copyright terms: Public domain W3C validator