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

Theorem nnrpd 11346
Description: A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
nnrpd.1  |-  ( ph  ->  A  e.  NN )
Assertion
Ref Expression
nnrpd  |-  ( ph  ->  A  e.  RR+ )

Proof of Theorem nnrpd
StepHypRef Expression
1 nnrpd.1 . 2  |-  ( ph  ->  A  e.  NN )
2 nnrp 11318 . 2  |-  ( A  e.  NN  ->  A  e.  RR+ )
31, 2syl 17 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872   NNcn 10616   RR+crp 11309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-er 7374  df-en 7581  df-dom 7582  df-sdom 7583  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-nn 10617  df-rp 11310
This theorem is referenced by:  zgt1rpn0n1  11347  modmulnn  12120  nnesq  12402  digit1  12412  bcpasc  12512  cshwn  12901  iseralt  13750  mertenslem1  13939  mertenslem2  13940  ege2le3  14143  eftlub  14162  effsumlt  14164  eirrlem  14255  sqr2irrlem  14299  dvdsmod  14361  bitsfzo  14408  bitsmod  14409  bitscmp  14411  bitsinv1lem  14414  sadaddlem  14439  sadasslem  14443  bitsres  14446  smumul  14466  bezoutlem3OLD  14504  bezoutlem3  14507  eucalglt  14543  prmind2  14634  crt  14725  eulerthlem2  14729  fermltl  14731  prmdiv  14732  prmdiveq  14733  odzdvds  14739  odzdvdsOLD  14745  vfermltlALT  14752  powm2modprm  14753  modprm0  14755  modprmn0modprm0  14757  prmreclem3  14861  prmreclem5  14863  prmreclem6  14864  4sqlem5  14885  4sqlem6  14886  4sqlem7  14887  4sqlem10  14890  4sqlem12  14899  vdwlem1  14930  mndodcong  17190  odmod  17194  oddvds  17195  dfod2  17214  gexexlem  17489  zringlpirlem3OLD  19053  zringlpirlem3  19055  met1stc  21534  met2ndci  21535  lebnumlem3  21989  lebnumlem3OLD  21992  lebnumii  21995  ovollb2lem  22439  ovoliunlem1  22453  ovoliunlem3  22455  uniioombllem6  22544  itg2cnlem2  22718  elqaalem2  23271  elqaalem2OLD  23274  aalioulem2  23287  aalioulem4  23289  aalioulem5  23290  aaliou2b  23295  aaliou3lem9  23304  logfac  23548  cxpeq  23695  leibpi  23866  amgmlem  23913  emcllem1  23919  emcllem2  23920  emcllem3  23921  emcllem5  23923  harmoniclbnd  23932  harmonicubnd  23933  harmonicbnd4  23934  fsumharmonic  23935  zetacvg  23938  lgamgulmlem2  23953  lgamgulmlem3  23954  lgamgulmlem4  23955  lgamgulmlem5  23956  lgamgulmlem6  23957  lgamgulm2  23959  lgambdd  23960  lgamucov  23961  lgamcvg2  23978  gamcvg  23979  gamcvg2lem  23982  regamcl  23984  relgamcl  23985  lgam1  23987  wilthlem1  23991  wilthlem2  23992  basellem1  24005  basellem6  24010  basellem8  24012  chtf  24033  efchtcl  24036  chtge0  24037  vmacl  24043  efvmacl  24045  sgmnncl  24072  chtprm  24078  chtdif  24083  efchtdvds  24084  prmorcht  24103  sgmppw  24123  vmalelog  24131  chtleppi  24136  chtublem  24137  fsumvma2  24140  pclogsum  24141  vmasum  24142  chpchtsum  24145  chpub  24146  logfacubnd  24147  logfaclbnd  24148  logfacbnd3  24149  logfacrlim  24150  logexprlim  24151  logfacrlim2  24152  perfectlem2  24156  bclbnd  24206  bposlem1  24210  bposlem2  24211  bposlem4  24213  bposlem5  24214  bposlem6  24215  bposlem7  24216  bposlem9  24218  lgslem1  24222  lgslem4  24225  lgsvalmod  24241  lgsmod  24247  lgsdirprm  24255  lgsne0  24259  lgsqrlem2  24268  lgseisenlem1  24275  lgseisenlem2  24276  lgseisenlem3  24277  lgseisenlem4  24278  lgseisen  24279  lgsquadlem2  24281  lgsquadlem3  24282  m1lgs  24288  2sqlem8  24298  chebbnd1lem1  24305  chebbnd1lem2  24306  chebbnd1lem3  24307  chebbnd1  24308  chtppilimlem1  24309  chtppilimlem2  24310  chtppilim  24311  chebbnd2  24313  chto1lb  24314  vmadivsum  24318  vmadivsumb  24319  rplogsumlem1  24320  rplogsumlem2  24321  dchrisum0lem1a  24322  rpvmasumlem  24323  dchrisumlema  24324  dchrisumlem1  24325  dchrisumlem2  24326  dchrmusum2  24330  dchrvmasumlem1  24331  dchrvmasum2lem  24332  dchrvmasum2if  24333  dchrvmasumlem2  24334  dchrvmasumlem3  24335  dchrvmasumiflem1  24337  dchrvmasumiflem2  24338  dchrisum0flblem2  24345  dchrisum0fno1  24347  dchrisum0lema  24350  dchrisum0lem1b  24351  dchrisum0lem1  24352  dchrisum0lem2a  24353  dchrisum0lem2  24354  dchrisum0lem3  24355  dchrisum0  24356  dirith2  24364  mudivsum  24366  mulogsumlem  24367  mulogsum  24368  mulog2sumlem1  24370  mulog2sumlem2  24371  mulog2sumlem3  24372  vmalogdivsum2  24374  vmalogdivsum  24375  2vmadivsumlem  24376  logsqvma  24378  log2sumbnd  24380  selberglem1  24381  selberglem2  24382  selberglem3  24383  selberg  24384  selbergb  24385  selberg2lem  24386  selberg2  24387  selberg2b  24388  chpdifbndlem1  24389  logdivbnd  24392  selberg3lem1  24393  selberg3lem2  24394  selberg3  24395  selberg4lem1  24396  selberg4  24397  pntrsumo1  24401  pntrsumbnd2  24403  selbergr  24404  selberg3r  24405  selberg4r  24406  selberg34r  24407  pntsf  24409  pntsval2  24412  pntrlog2bndlem1  24413  pntrlog2bndlem2  24414  pntrlog2bndlem3  24415  pntrlog2bndlem4  24416  pntrlog2bndlem5  24417  pntrlog2bndlem6  24419  pntrlog2bnd  24420  pntpbnd1a  24421  pntpbnd1  24422  pntpbnd2  24423  pntibndlem2  24427  pntlemn  24436  pntlemj  24439  pntlemf  24441  pntlemk  24442  pntlemo  24443  pnt  24450  padicabvcxp  24468  ostth2lem2  24470  ostth2lem3  24471  ostth2lem4  24472  ostth2  24473  ostth3  24474  clwwisshclwwlem1  25531  numclwwlk5  25838  numclwwlk7  25840  ubthlem2  26511  minvecolem3  26516  minvecolem3OLD  26526  lnconi  27684  ltesubnnd  28392  2sqmod  28416  madjusmdetlem2  28662  eulerpartlemgc  29203  iprodgam  30385  faclimlem1  30386  faclimlem3  30388  faclim  30389  iprodfac  30390  poimirlem29  31933  heiborlem3  32109  heiborlem5  32111  heiborlem6  32112  heiborlem7  32113  heiborlem8  32114  heibor  32117  rrndstprj2  32127  rrncmslem  32128  rrnequiv  32131  irrapxlem5  35640  pell14qrgapw  35692  pellqrexplicit  35693  pellqrex  35696  pellfundge  35700  pellfundgt1  35701  jm3.1lem1  35842  jm3.1lem2  35843  hashnzfz2  36640  fsumnncl  37591  stoweidlem31  37832  stoweidlem59  37860  wallispilem3  37869  wallispi  37872  stirlinglem12  37887  stirlinglem15  37890  fourierdlem73  37983  etransclem23  38062  nnfoctbdjlem  38201  ovnsubaddlem1  38296  perfectALTVlem2  38714  proththd  38784  pw2m1lepw2m1  39939  logbge0b  39995  logblt1b  39996  logbpw2m1  39999  nnpw2pmod  40015  nnolog2flm1  40022  blennngt2o2  40024  dignnld  40035  digexp  40039
  Copyright terms: Public domain W3C validator