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

Theorem ltpnf 10510
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 2316 . . . 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 8922 . . 3  |-  ( A  e.  RR  ->  A  e.  RR* )
6 pnfxr 10502 . . 3  |-  +oo  e.  RR*
7 ltxr 10504 . . 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 1633    e. wcel 1701   class class class wbr 4060   RRcr 8781    <RR cltrr 8786    +oocpnf 8909    -oocmnf 8910   RR*cxr 8911    < clt 8912
This theorem is referenced by:  xrlttri  10520  xrlttr  10521  xrrebnd  10544  xrre  10545  qbtwnxr  10574  xltnegi  10590  xmulgt0  10650  xrinfmsslem  10673  xrub  10677  supxrunb1  10685  supxrunb2  10686  elioc2  10760  elicc2  10762  ioomax  10771  ioopos  10773  elioopnf  10784  elicopnf  10786  difreicc  10814  hashbnd  11390  limsupgre  12002  pcadd  12984  ramubcl  13112  pnfnei  17006  mnfnei  17007  icopnfcld  18329  iocmnfcld  18330  blcvx  18356  xrtgioo  18364  reconnlem1  18383  xrge0tsms  18391  iccpnfhmeo  18496  ioombl1lem4  18971  icombl1  18973  uniioombllem1  18989  mbfmax  19057  ismbf3d  19062  mbflimsup  19074  itg2seq  19150  lhop2  19415  dvfsumlem2  19427  logccv  20063  rlimcnp3  20315  xrlimcnp  20316  pntleme  20810  isblo3i  21434  htthlem  21552  0bdop  22628  xlt2addrd  23270  fsumrp0cl  23355  xrge0tsmsd  23360  xrge0iifcnv  23388  xrge0iifiso  23390  xrge0iifhom  23392  xrge0mulc1cn  23396  pnfneige0  23405  lmxrge0  23406  esumcst  23631  esumpfinvallem  23640  voliune  23759  volfiniune  23760  sxbrsigalem0  23795  orvcgteel  23899  dstfrvclim1  23909  umgrafi  24158  itg2addnclem2  25318  rfcnpre3  26852  hashnnn0genn0  27286  sgnpnf  27699
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-cnex 8838
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-xp 4732  df-pnf 8914  df-xr 8916  df-ltxr 8917
  Copyright terms: Public domain W3C validator