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

Theorem nnrpd 12417
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
StepHypRef Expression
1 nnrpd.1 . 2 (𝜑𝐴 ∈ ℕ)
2 nnrp 12388 . 2 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)
31, 2syl 17 1 (𝜑𝐴 ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  cn 11625  +crp 12377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-rp 12378
This theorem is referenced by:  zgt1rpn0n1  12418  modmulnn  13252  mulp1mod1  13275  modsumfzodifsn  13307  addmodlteq  13309  nnesq  13584  digit1  13594  bcpasc  13677  cshwn  14150  iseralt  15033  climcndslem2  15197  mertenslem1  15232  mertenslem2  15233  fprodmodd  15343  efcllem  15423  ege2le3  15435  eftlub  15454  effsumlt  15456  eirrlem  15549  sqrt2irrlem  15593  p1modz1  15606  dvdsmod  15670  bitsfzo  15774  bitsmod  15775  bitscmp  15777  bitsinv1lem  15780  sadaddlem  15805  sadasslem  15809  bitsres  15812  smumul  15832  bezoutlem3  15879  eucalglt  15919  prmind2  16019  crth  16105  eulerthlem2  16109  fermltl  16111  prmdiv  16112  prmdiveq  16113  odzdvds  16122  vfermltlALT  16129  powm2modprm  16130  modprm0  16132  modprmn0modprm0  16134  prmreclem3  16244  prmreclem5  16246  prmreclem6  16247  4sqlem5  16268  4sqlem6  16269  4sqlem7  16270  4sqlem10  16273  4sqlem12  16282  vdwlem1  16307  mndodcong  18662  odmod  18666  oddvds  18667  dfod2  18683  gexexlem  18965  zringlpirlem3  20179  met1stc  23128  met2ndci  23129  lebnumlem3  23568  lebnumii  23571  ovollb2lem  24092  ovoliunlem1  24106  ovoliunlem3  24108  uniioombllem6  24192  itg2cnlem2  24366  elqaalem2  24916  aalioulem2  24929  aalioulem4  24931  aalioulem5  24932  aaliou2b  24937  aaliou3lem9  24946  logfac  25192  cxpeq  25346  logbgcd1irr  25380  leibpi  25528  birthdaylem2  25538  amgmlem  25575  emcllem1  25581  emcllem2  25582  emcllem3  25583  emcllem5  25585  harmoniclbnd  25594  harmonicubnd  25595  harmonicbnd4  25596  fsumharmonic  25597  zetacvg  25600  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamgulmlem4  25617  lgamgulmlem5  25618  lgamgulmlem6  25619  lgamgulm2  25621  lgambdd  25622  lgamucov  25623  lgamcvg2  25640  gamcvg  25641  gamcvg2lem  25644  regamcl  25646  relgamcl  25647  lgam1  25649  wilthlem1  25653  wilthlem2  25654  basellem1  25666  basellem6  25671  basellem8  25673  chtf  25693  efchtcl  25696  chtge0  25697  vmacl  25703  efvmacl  25705  sgmnncl  25732  chtprm  25738  chtdif  25743  efchtdvds  25744  prmorcht  25763  sgmppw  25781  vmalelog  25789  chtleppi  25794  chtublem  25795  fsumvma2  25798  pclogsum  25799  vmasum  25800  chpchtsum  25803  chpub  25804  logfacubnd  25805  logfaclbnd  25806  logfacbnd3  25807  logfacrlim  25808  logexprlim  25809  logfacrlim2  25810  perfectlem2  25814  bclbnd  25864  bposlem1  25868  bposlem2  25869  bposlem4  25871  bposlem5  25872  bposlem6  25873  bposlem7  25874  bposlem9  25876  lgslem1  25881  lgsvalmod  25900  lgsmod  25907  lgsdirprm  25915  lgsne0  25919  lgsqrlem2  25931  gausslemma2dlem0i  25948  gausslemma2dlem5a  25954  gausslemma2d  25958  lgseisenlem1  25959  lgseisenlem2  25960  lgseisenlem3  25961  lgseisenlem4  25962  lgseisen  25963  lgsquadlem2  25965  lgsquadlem3  25966  m1lgs  25972  2sqlem8  26010  2sqmod  26020  chebbnd1lem1  26053  chebbnd1lem2  26054  chebbnd1lem3  26055  chebbnd1  26056  chtppilimlem1  26057  chtppilimlem2  26058  chtppilim  26059  chebbnd2  26061  chto1lb  26062  vmadivsum  26066  vmadivsumb  26067  rplogsumlem1  26068  rplogsumlem2  26069  dchrisum0lem1a  26070  rpvmasumlem  26071  dchrisumlema  26072  dchrisumlem1  26073  dchrisumlem2  26074  dchrmusum2  26078  dchrvmasumlem1  26079  dchrvmasum2lem  26080  dchrvmasum2if  26081  dchrvmasumlem2  26082  dchrvmasumlem3  26083  dchrvmasumiflem1  26085  dchrvmasumiflem2  26086  dchrisum0flblem2  26093  dchrisum0fno1  26095  dchrisum0lema  26098  dchrisum0lem1b  26099  dchrisum0lem1  26100  dchrisum0lem2a  26101  dchrisum0lem2  26102  dchrisum0lem3  26103  dchrisum0  26104  dirith2  26112  mudivsum  26114  mulogsumlem  26115  mulogsum  26116  mulog2sumlem1  26118  mulog2sumlem2  26119  mulog2sumlem3  26120  vmalogdivsum2  26122  vmalogdivsum  26123  2vmadivsumlem  26124  logsqvma  26126  log2sumbnd  26128  selberglem1  26129  selberglem2  26130  selberglem3  26131  selberg  26132  selbergb  26133  selberg2lem  26134  selberg2  26135  selberg2b  26136  chpdifbndlem1  26137  logdivbnd  26140  selberg3lem1  26141  selberg3lem2  26142  selberg3  26143  selberg4lem1  26144  selberg4  26145  pntrsumo1  26149  pntrsumbnd2  26151  selbergr  26152  selberg3r  26153  selberg4r  26154  selberg34r  26155  pntsf  26157  pntsval2  26160  pntrlog2bndlem1  26161  pntrlog2bndlem2  26162  pntrlog2bndlem3  26163  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntrlog2bndlem6  26167  pntrlog2bnd  26168  pntpbnd1a  26169  pntpbnd1  26170  pntpbnd2  26171  pntibndlem2  26175  pntlemn  26184  pntlemj  26187  pntlemf  26189  pntlemk  26190  pntlemo  26191  pnt  26198  padicabvcxp  26216  ostth2lem2  26218  ostth2lem3  26219  ostth2lem4  26220  ostth2  26221  ostth3  26222  clwwisshclwwslemlem  27798  numclwwlk5  28173  numclwwlk7  28176  ubthlem2  28654  minvecolem3  28659  lnconi  29816  prmdvdsbc  30558  ltesubnnd  30564  cshwrnid  30661  cycpmfv2  30806  madjusmdetlem2  31181  eulerpartlemgc  31730  reprle  31995  hgt750lemc  32028  hgt750lemd  32029  hgt750lemb  32037  hgt750leme  32039  tgoldbachgtde  32041  iprodgam  33087  faclimlem1  33088  faclimlem3  33090  faclim  33091  iprodfac  33092  knoppndvlem17  33980  poimirlem29  35086  heiborlem3  35251  heiborlem5  35253  heiborlem6  35254  heiborlem7  35255  heiborlem8  35256  heibor  35259  rrndstprj2  35269  rrncmslem  35270  rrnequiv  35273  lcmineqlem20  39336  lcmineqlem23  39339  metakunt18  39365  metakunt30  39377  zrtelqelz  39498  rtprmirr  39500  fltne  39614  fltltc  39615  fltnltalem  39616  fltnlta  39617  irrapxlem5  39765  pell14qrgapw  39815  pellqrexplicit  39816  pellqrex  39818  pellfundge  39821  pellfundgt1  39822  jm3.1lem1  39956  jm3.1lem2  39957  hashnzfz2  41023  xralrple4  42003  recnnltrp  42007  rpgtrecnn  42011  fsumnncl  42211  limsup10exlem  42412  stoweidlem31  42671  stoweidlem59  42699  wallispilem3  42707  wallispi  42710  stirlinglem12  42725  stirlinglem15  42728  fourierdlem73  42819  etransclem23  42897  nnfoctbdjlem  43092  ovnsubaddlem1  43207  ovolval5lem1  43289  ovolval5lem2  43290  vonioolem1  43317  vonioolem2  43318  vonicclem2  43321  fmtnoprmfac1lem  44079  sfprmdvdsmersenne  44119  lighneallem2  44122  proththd  44130  perfectALTVlem2  44238  fppr2odd  44247  fpprwppr  44255  fpprel2  44257  pw2m1lepw2m1  44927  logbge0b  44975  logblt1b  44976  logbpw2m1  44979  nnpw2pmod  44995  nnolog2flm1  45002  blennngt2o2  45004  dignnld  45015  digexp  45019  amgmlemALT  45329
  Copyright terms: Public domain W3C validator