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

Theorem ltpnf 10723
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 2438 . . . 4  |-  +oo  =  +oo
2 orc 376 . . . 4  |-  ( ( A  e.  RR  /\  +oo  =  +oo )  -> 
( ( A  e.  RR  /\  +oo  =  +oo )  \/  ( A  =  -oo  /\  +oo  e.  RR ) ) )
31, 2mpan2 654 . . 3  |-  ( A  e.  RR  ->  (
( A  e.  RR  /\ 
+oo  =  +oo )  \/  ( A  =  -oo  /\ 
+oo  e.  RR )
) )
43olcd 384 . 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 9132 . . 3  |-  ( A  e.  RR  ->  A  e.  RR* )
6 pnfxr 10715 . . 3  |-  +oo  e.  RR*
7 ltxr 10717 . . 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 645 . 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 225 1  |-  ( A  e.  RR  ->  A  <  +oo )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    \/ wo 359    /\ wa 360    = wceq 1653    e. wcel 1726   class class class wbr 4214   RRcr 8991    <RR cltrr 8996    +oocpnf 9119    -oocmnf 9120   RR*cxr 9121    < clt 9122
This theorem is referenced by:  xrlttri  10734  xrlttr  10735  xrrebnd  10758  xrre  10759  qbtwnxr  10788  xltnegi  10804  xmulgt0  10864  xrinfmsslem  10888  xrub  10892  supxrunb1  10900  supxrunb2  10901  elioc2  10975  elicc2  10977  ioomax  10987  ioopos  10989  elioopnf  11000  elicopnf  11002  difreicc  11030  hashbnd  11626  hashnnn0genn0  11629  hashv01gt1  11631  limsupgre  12277  pcadd  13260  ramubcl  13388  pnfnei  17286  mnfnei  17287  xblss2ps  18433  icopnfcld  18804  iocmnfcld  18805  blcvx  18831  xrtgioo  18839  reconnlem1  18859  xrge0tsms  18867  iccpnfhmeo  18972  ioombl1lem4  19457  icombl1  19459  uniioombllem1  19475  mbfmax  19543  ismbf3d  19548  mbflimsup  19560  itg2seq  19636  lhop2  19901  dvfsumlem2  19913  logccv  20556  rlimcnp3  20808  xrlimcnp  20809  pntleme  21304  umgrafi  21359  isblo3i  22304  htthlem  22422  0bdop  23498  xlt2addrd  24126  fsumrp0cl  24219  xrge0tsmsd  24225  pnfinf  24255  xrge0iifcnv  24321  xrge0iifiso  24323  xrge0iifhom  24325  xrge0mulc1cn  24329  pnfneige0  24338  lmxrge0  24339  esumcst  24457  esumpfinvallem  24466  voliune  24587  volfiniune  24588  sxbrsigalem0  24623  orvcgteel  24727  dstfrvclim1  24737  mbfposadd  26256  itg2addnclem2  26259  ftc1anclem5  26286  rfcnpre3  27682  frgrawopreglem2  28496  sgnpnf  28585
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-cnex 9048
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-xp 4886  df-pnf 9124  df-xr 9126  df-ltxr 9127
  Copyright terms: Public domain W3C validator