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

Theorem ltpnf 10463
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 2283 . . . 4  |-  +oo  =  +oo
2 orc 374 . . . 4  |-  ( ( A  e.  RR  /\  +oo  =  +oo )  -> 
( ( A  e.  RR  /\  +oo  =  +oo )  \/  ( A  =  -oo  /\  +oo  e.  RR ) ) )
31, 2mpan2 652 . . 3  |-  ( A  e.  RR  ->  (
( A  e.  RR  /\ 
+oo  =  +oo )  \/  ( A  =  -oo  /\ 
+oo  e.  RR )
) )
43olcd 382 . 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 8877 . . 3  |-  ( A  e.  RR  ->  A  e.  RR* )
6 pnfxr 10455 . . 3  |-  +oo  e.  RR*
7 ltxr 10457 . . 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 643 . 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 223 1  |-  ( A  e.  RR  ->  A  <  +oo )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    = wceq 1623    e. wcel 1684   class class class wbr 4023   RRcr 8736    <RR cltrr 8741    +oocpnf 8864    -oocmnf 8865   RR*cxr 8866    < clt 8867
This theorem is referenced by:  xrlttri  10473  xrlttr  10474  xrrebnd  10497  xrre  10498  qbtwnxr  10527  xltnegi  10543  xmulgt0  10603  xrinfmsslem  10626  xrub  10630  supxrunb1  10638  supxrunb2  10639  elioc2  10713  elicc2  10715  ioomax  10724  ioopos  10726  elioopnf  10737  elicopnf  10739  difreicc  10767  hashbnd  11343  limsupgre  11955  pcadd  12937  ramubcl  13065  pnfnei  16950  mnfnei  16951  icopnfcld  18277  iocmnfcld  18278  blcvx  18304  xrtgioo  18312  reconnlem1  18331  xrge0tsms  18339  iccpnfhmeo  18443  ioombl1lem4  18918  icombl1  18920  uniioombllem1  18936  mbfmax  19004  ismbf3d  19009  mbflimsup  19021  itg2seq  19097  lhop2  19362  dvfsumlem2  19374  logccv  20010  rlimcnp3  20262  xrlimcnp  20263  pntleme  20757  isblo3i  21379  htthlem  21497  0bdop  22573  xlt2addrd  23253  xrge0iifcnv  23315  xrge0iifiso  23317  xrge0iifhom  23319  xrge0mulc1cn  23323  fsumrp0cl  23334  pnfneige0  23374  lmxrge0  23375  xrge0tsmsd  23382  esumcst  23436  esumpfinvallem  23442  orvcgteel  23668  dstfrvclim1  23678  umgrafi  23874  truni1  25505  rfcnpre3  27704  sgnpnf  28250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-xp 4695  df-pnf 8869  df-xr 8871  df-ltxr 8872
  Copyright terms: Public domain W3C validator