Theorem nnrpd 11284

Description: A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
nnrpd.1

Assertion

Ref	Expression
nnrpd

Proof of Theorem nnrpd

Step	Hyp	Ref	Expression
1		nnrpd.1	. 2
2		nnrp 11258	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  e.wcel 1818  cn 10561  crp 11249

This theorem is referenced by:  modmulnn  12013  nnesq  12290  digit1  12300  bcpasc  12399  cshwn  12768  iseralt  13507  mertenslem1  13693  mertenslem2  13694  ege2le3  13825  eftlub  13844  effsumlt  13846  eirrlem  13937  sqr2irrlem  13981  dvdsmod  14043  bitsfzo  14085  bitsmod  14086  bitscmp  14088  bitsinv1lem  14091  sadaddlem  14116  sadasslem  14120  bitsres  14123  smumul  14143  bezoutlem3  14178  eucalglt  14214  prmind2  14228  crt  14308  eulerthlem2  14312  fermltl  14314  prmdiv  14315  prmdiveq  14316  odzdvds  14322  powm2modprm  14328  modprm0  14330  modprmn0modprm0  14332  prmreclem3  14436  prmreclem5  14438  prmreclem6  14439  4sqlem5  14460  4sqlem6  14461  4sqlem7  14462  4sqlem10  14465  4sqlem12  14474  vdwlem1  14499  mndodcong  16566  odmod  16570  oddvds  16571  dfod2  16586  gexexlem  16858  zringlpirlem3  18511  zlpirlem3  18516  met1stc  21024  met2ndci  21025  lebnumlem3  21463  lebnumii  21466  ovollb2lem  21899  ovoliunlem1  21913  ovoliunlem3  21915  uniioombllem6  21997  itg2cnlem2  22169  elqaalem2  22716  aalioulem2  22729  aalioulem4  22731  aalioulem5  22732  aaliou2b  22737  aaliou3lem9  22746  logfac  22985  cxpeq  23131  leibpi  23273  amgmlem  23319  emcllem1  23325  emcllem2  23326  emcllem3  23327  emcllem5  23329  harmoniclbnd  23338  harmonicubnd  23339  harmonicbnd4  23340  fsumharmonic  23341  wilthlem1  23342  wilthlem2  23343  basellem1  23354  basellem6  23359  basellem8  23361  chtf  23382  efchtcl  23385  chtge0  23386  vmacl  23392  efvmacl  23394  sgmnncl  23421  chtprm  23427  chtdif  23432  efchtdvds  23433  prmorcht  23452  sgmppw  23472  vmalelog  23480  chtleppi  23485  chtublem  23486  fsumvma2  23489  pclogsum  23490  vmasum  23491  chpchtsum  23494  chpub  23495  logfacubnd  23496  logfaclbnd  23497  logfacbnd3  23498  logfacrlim  23499  logexprlim  23500  logfacrlim2  23501  perfectlem2  23505  bclbnd  23555  bposlem1  23559  bposlem2  23560  bposlem4  23562  bposlem5  23563  bposlem6  23564  bposlem7  23565  bposlem9  23567  lgslem1  23571  lgslem4  23574  lgsvalmod  23590  lgsmod  23596  lgsdirprm  23604  lgsne0  23608  lgsqrlem2  23617  lgseisenlem1  23624  lgseisenlem2  23625  lgseisenlem3  23626  lgseisenlem4  23627  lgseisen  23628  lgsquadlem2  23630  lgsquadlem3  23631  m1lgs  23637  2sqlem8  23647  chebbnd1lem1  23654  chebbnd1lem2  23655  chebbnd1lem3  23656  chebbnd1  23657  chtppilimlem1  23658  chtppilimlem2  23659  chtppilim  23660  chebbnd2  23662  chto1lb  23663  vmadivsum  23667  vmadivsumb  23668  rplogsumlem1  23669  rplogsumlem2  23670  dchrisum0lem1a  23671  rpvmasumlem  23672  dchrisumlema  23673  dchrisumlem1  23674  dchrisumlem2  23675  dchrmusum2  23679  dchrvmasumlem1  23680  dchrvmasum2lem  23681  dchrvmasum2if  23682  dchrvmasumlem2  23683  dchrvmasumlem3  23684  dchrvmasumiflem1  23686  dchrvmasumiflem2  23687  dchrisum0flblem2  23694  dchrisum0fno1  23696  dchrisum0lema  23699  dchrisum0lem1b  23700  dchrisum0lem1  23701  dchrisum0lem2a  23702  dchrisum0lem2  23703  dchrisum0lem3  23704  dchrisum0  23705  dirith2  23713  mudivsum  23715  mulogsumlem  23716  mulogsum  23717  mulog2sumlem1  23719  mulog2sumlem2  23720  mulog2sumlem3  23721  vmalogdivsum2  23723  vmalogdivsum  23724  2vmadivsumlem  23725  logsqvma  23727  log2sumbnd  23729  selberglem1  23730  selberglem2  23731  selberglem3  23732  selberg  23733  selbergb  23734  selberg2lem  23735  selberg2  23736  selberg2b  23737  chpdifbndlem1  23738  logdivbnd  23741  selberg3lem1  23742  selberg3lem2  23743  selberg3  23744  selberg4lem1  23745  selberg4  23746  pntrsumo1  23750  pntrsumbnd2  23752  selbergr  23753  selberg3r  23754  selberg4r  23755  selberg34r  23756  pntsf  23758  pntsval2  23761  pntrlog2bndlem1  23762  pntrlog2bndlem2  23763  pntrlog2bndlem3  23764  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntrlog2bndlem6  23768  pntrlog2bnd  23769  pntpbnd1a  23770  pntpbnd1  23771  pntpbnd2  23772  pntibndlem2  23776  pntlemn  23785  pntlemj  23788  pntlemf  23790  pntlemk  23791  pntlemo  23792  pnt  23799  padicabvcxp  23817  ostth2lem2  23819  ostth2lem3  23820  ostth2lem4  23821  ostth2  23822  ostth3  23823  clwwisshclwwlem1  24805  numclwwlk5  25112  numclwwlk7  25114  ubthlem2  25787  minvecolem3  25792  lnconi  26952  ltesubnnd  27612  2sqmod  27636  rnlogblem  28015  eulerpartlemgc  28301  zetacvg  28557  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem4  28574  lgamgulmlem5  28575  lgamgulmlem6  28576  lgamgulm2  28578  lgambdd  28579  lgamucov  28580  lgamcvg2  28597  gamcvg  28598  gamcvg2lem  28601  regamcl  28603  relgamcl  28604  lgam1  28606  iprodgam  29125  faclimlem1  29168  faclimlem3  29170  faclim  29171  iprodfac  29172  heiborlem3  30309  heiborlem5  30311  heiborlem6  30312  heiborlem7  30313  heiborlem8  30314  heibor  30317  rrndstprj2  30327  rrncmslem  30328  rrnequiv  30331  irrapxlem5  30762  pell14qrgapw  30812  pellqrexplicit  30813  pellqrex  30815  pellfundge  30818  pellfundgt1  30819  jm3.1lem1  30959  jm3.1lem2  30960  hashnzfz2  31226  fsumnncl  31572  stoweidlem31  31813  stoweidlem59  31841  wallispilem3  31849  wallispi  31852  stirlinglem12  31867  stirlinglem15  31870  fourierdlem73  31962  etransclem23  32040

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-recs 7061  df-rdg 7095  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-nn 10562  df-rp 11250