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

Theorem nnrp 10626
Description: A natural number is a positive real. (Contributed by NM, 28-Nov-2008.)
Assertion
Ref Expression
nnrp  |-  ( A  e.  NN  ->  A  e.  RR+ )

Proof of Theorem nnrp
StepHypRef Expression
1 nnre 10012 . 2  |-  ( A  e.  NN  ->  A  e.  RR )
2 nngt0 10034 . 2  |-  ( A  e.  NN  ->  0  <  A )
3 elrp 10619 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3sylanbrc 647 1  |-  ( A  e.  NN  ->  A  e.  RR+ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   class class class wbr 4215   RRcr 8994   0cc0 8995    < clt 9125   NNcn 10005   RR+crp 10617
This theorem is referenced by:  nnrpd  10652  zmodcl  11271  zmodfz  11273  nnesq  11508  digit2  11517  digit1  11518  bcrpcl  11604  bcval5  11614  divcnv  12638  supcvg  12640  harmonic  12643  expcnv  12648  rpnnen2lem11  12829  sqr2irr  12853  dvdsval3  12861  moddvds  12864  divalgmod  12931  modgcd  13041  isprm6  13114  isprm5  13117  pythagtriplem13  13206  fldivp1  13271  prmreclem5  13293  prmreclem6  13294  4sqlem12  13329  modxai  13409  modsubi  13413  odmodnn0  15183  gexdvds  15223  sylow1lem1  15237  gexexlem  15472  znf1o  16837  met1stc  18556  lmnn  19221  bcthlem5  19286  minveclem3  19335  vitalilem4  19508  vitali  19510  ismbf3d  19549  itg2seq  19637  plyeq0lem  20134  elqaalem3  20243  aalioulem6  20259  aaliou  20260  logtayllem  20555  atan1  20773  leibpi  20787  birthdaylem2  20796  dfef2  20814  divsqrsumlem  20823  emcllem1  20839  emcllem2  20840  emcllem3  20841  emcllem4  20842  emcllem6  20844  ppiub  20993  vmalelog  20994  logfacbnd3  21012  logexprlim  21014  bcmono  21066  bclbnd  21069  bposlem1  21073  bposlem7  21079  bposlem8  21080  bposlem9  21081  m1lgs  21151  rplogsumlem1  21183  dchrisumlema  21187  dchrisumlem2  21189  dchrisumlem3  21190  dchrvmasumlem2  21197  dchrvmasumiflem1  21200  dchrisum0lem1b  21214  dchrisum0lem2a  21216  rplogsum  21226  logdivsum  21232  mulog2sumlem2  21234  logsqvma  21241  logsqvma2  21242  log2sumbnd  21243  selberg2lem  21249  logdivbnd  21255  pntrsumo1  21264  pntrsumbnd  21265  pntibndlem1  21288  pntibndlem2  21290  pntibndlem3  21291  pntlemd  21293  pntlema  21295  pntlemb  21296  pntlemr  21301  pntlemj  21302  pntlemf  21304  pntlemo  21306  gxmodid  21872  lnconi  23541  zetacvg  24804  lgam1  24853  circum  25116  zmodid2  25119  faclimlem3  25369  faclim  25370  mblfinlem3  26257  itg2addnclem2  26271  itg2addnclem3  26272  itg2addnc  26273  pellexlem4  26909  pell1qrgaplem  26950  pellqrex  26956  congrep  27052  acongeq  27062  dvdsabsmod0  27071  proot1ex  27511  wallispilem4  27807  wallispi  27809  wallispi2lem1  27810  wallispi2lem2  27811  stirlinglem1  27813  stirlinglem2  27814  stirlinglem3  27815  stirlinglem4  27816  stirlinglem6  27818  stirlinglem7  27819  stirlinglem10  27822  stirlinglem11  27823  stirlinglem13  27825  stirlinglem14  27826  stirlinglem15  27827  stirlingr  27829  fldivnn0le  28169  modidmul0  28183  modifeq2int  28184  2cshwmod  28291  cshweqrep  28308  cshw1  28309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071  ax-pre-mulgt0 9072
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  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-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-riota 6552  df-recs 6636  df-rdg 6671  df-er 6908  df-en 7113  df-dom 7114  df-sdom 7115  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131  df-sub 9298  df-neg 9299  df-nn 10006  df-rp 10618
  Copyright terms: Public domain W3C validator