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

Theorem nnrpd 12245
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 12216 . 2 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)
31, 2syl 17 1 (𝜑𝐴 ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2051  cn 11438  +crp 12203
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-resscn 10391  ax-1cn 10392  ax-icn 10393  ax-addcl 10394  ax-addrcl 10395  ax-mulcl 10396  ax-mulrcl 10397  ax-mulcom 10398  ax-addass 10399  ax-mulass 10400  ax-distr 10401  ax-i2m1 10402  ax-1ne0 10403  ax-1rid 10404  ax-rnegex 10405  ax-rrecex 10406  ax-cnre 10407  ax-pre-lttri 10408  ax-pre-lttrn 10409  ax-pre-ltadd 10410  ax-pre-mulgt0 10411
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-reu 3090  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-iun 4791  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-om 7396  df-wrecs 7749  df-recs 7811  df-rdg 7849  df-er 8088  df-en 8306  df-dom 8307  df-sdom 8308  df-pnf 10475  df-mnf 10476  df-xr 10477  df-ltxr 10478  df-le 10479  df-sub 10671  df-neg 10672  df-nn 11439  df-rp 12204
This theorem is referenced by:  zgt1rpn0n1  12246  modmulnn  13071  mulp1mod1  13094  modsumfzodifsn  13126  addmodlteq  13128  nnesq  13402  digit1  13412  bcpasc  13495  cshwn  14020  iseralt  14901  climcndslem2  15064  mertenslem1  15099  mertenslem2  15100  fprodmodd  15210  efcllem  15290  ege2le3  15302  eftlub  15321  effsumlt  15323  eirrlem  15416  sqrt2irrlem  15460  p1modz1  15473  dvdsmod  15537  bitsfzo  15643  bitsmod  15644  bitscmp  15646  bitsinv1lem  15649  sadaddlem  15674  sadasslem  15678  bitsres  15681  smumul  15701  bezoutlem3  15744  eucalglt  15784  prmind2  15884  crth  15970  eulerthlem2  15974  fermltl  15976  prmdiv  15977  prmdiveq  15978  odzdvds  15987  vfermltlALT  15994  powm2modprm  15995  modprm0  15997  modprmn0modprm0  15999  prmreclem3  16109  prmreclem5  16111  prmreclem6  16112  4sqlem5  16133  4sqlem6  16134  4sqlem7  16135  4sqlem10  16138  4sqlem12  16147  vdwlem1  16172  mndodcong  18445  odmod  18449  oddvds  18450  dfod2  18465  gexexlem  18741  zringlpirlem3  20351  met1stc  22850  met2ndci  22851  lebnumlem3  23286  lebnumii  23289  ovollb2lem  23808  ovoliunlem1  23822  ovoliunlem3  23824  uniioombllem6  23908  itg2cnlem2  24082  elqaalem2  24628  aalioulem2  24641  aalioulem4  24643  aalioulem5  24644  aaliou2b  24649  aaliou3lem9  24658  logfac  24901  cxpeq  25055  logbgcd1irr  25089  leibpi  25238  birthdaylem2  25248  amgmlem  25285  emcllem1  25291  emcllem2  25292  emcllem3  25293  emcllem5  25295  harmoniclbnd  25304  harmonicubnd  25305  harmonicbnd4  25306  fsumharmonic  25307  zetacvg  25310  lgamgulmlem2  25325  lgamgulmlem3  25326  lgamgulmlem4  25327  lgamgulmlem5  25328  lgamgulmlem6  25329  lgamgulm2  25331  lgambdd  25332  lgamucov  25333  lgamcvg2  25350  gamcvg  25351  gamcvg2lem  25354  regamcl  25356  relgamcl  25357  lgam1  25359  wilthlem1  25363  wilthlem2  25364  basellem1  25376  basellem6  25381  basellem8  25383  chtf  25403  efchtcl  25406  chtge0  25407  vmacl  25413  efvmacl  25415  sgmnncl  25442  chtprm  25448  chtdif  25453  efchtdvds  25454  prmorcht  25473  sgmppw  25491  vmalelog  25499  chtleppi  25504  chtublem  25505  fsumvma2  25508  pclogsum  25509  vmasum  25510  chpchtsum  25513  chpub  25514  logfacubnd  25515  logfaclbnd  25516  logfacbnd3  25517  logfacrlim  25518  logexprlim  25519  logfacrlim2  25520  perfectlem2  25524  bclbnd  25574  bposlem1  25578  bposlem2  25579  bposlem4  25581  bposlem5  25582  bposlem6  25583  bposlem7  25584  bposlem9  25586  lgslem1  25591  lgsvalmod  25610  lgsmod  25617  lgsdirprm  25625  lgsne0  25629  lgsqrlem2  25641  gausslemma2dlem0i  25658  gausslemma2dlem5a  25664  gausslemma2d  25668  lgseisenlem1  25669  lgseisenlem2  25670  lgseisenlem3  25671  lgseisenlem4  25672  lgseisen  25673  lgsquadlem2  25675  lgsquadlem3  25676  m1lgs  25682  2sqlem8  25720  2sqmod  25730  chebbnd1lem1  25763  chebbnd1lem2  25764  chebbnd1lem3  25765  chebbnd1  25766  chtppilimlem1  25767  chtppilimlem2  25768  chtppilim  25769  chebbnd2  25771  chto1lb  25772  vmadivsum  25776  vmadivsumb  25777  rplogsumlem1  25778  rplogsumlem2  25779  dchrisum0lem1a  25780  rpvmasumlem  25781  dchrisumlema  25782  dchrisumlem1  25783  dchrisumlem2  25784  dchrmusum2  25788  dchrvmasumlem1  25789  dchrvmasum2lem  25790  dchrvmasum2if  25791  dchrvmasumlem2  25792  dchrvmasumlem3  25793  dchrvmasumiflem1  25795  dchrvmasumiflem2  25796  dchrisum0flblem2  25803  dchrisum0fno1  25805  dchrisum0lema  25808  dchrisum0lem1b  25809  dchrisum0lem1  25810  dchrisum0lem2a  25811  dchrisum0lem2  25812  dchrisum0lem3  25813  dchrisum0  25814  dirith2  25822  mudivsum  25824  mulogsumlem  25825  mulogsum  25826  mulog2sumlem1  25828  mulog2sumlem2  25829  mulog2sumlem3  25830  vmalogdivsum2  25832  vmalogdivsum  25833  2vmadivsumlem  25834  logsqvma  25836  log2sumbnd  25838  selberglem1  25839  selberglem2  25840  selberglem3  25841  selberg  25842  selbergb  25843  selberg2lem  25844  selberg2  25845  selberg2b  25846  chpdifbndlem1  25847  logdivbnd  25850  selberg3lem1  25851  selberg3lem2  25852  selberg3  25853  selberg4lem1  25854  selberg4  25855  pntrsumo1  25859  pntrsumbnd2  25861  selbergr  25862  selberg3r  25863  selberg4r  25864  selberg34r  25865  pntsf  25867  pntsval2  25870  pntrlog2bndlem1  25871  pntrlog2bndlem2  25872  pntrlog2bndlem3  25873  pntrlog2bndlem4  25874  pntrlog2bndlem5  25875  pntrlog2bndlem6  25877  pntrlog2bnd  25878  pntpbnd1a  25879  pntpbnd1  25880  pntpbnd2  25881  pntibndlem2  25885  pntlemn  25894  pntlemj  25897  pntlemf  25899  pntlemk  25900  pntlemo  25901  pnt  25908  padicabvcxp  25926  ostth2lem2  25928  ostth2lem3  25929  ostth2lem4  25930  ostth2  25931  ostth3  25932  clwwisshclwwslemlem  27544  numclwwlk5  27961  numclwwlk7  27964  ubthlem2  28442  minvecolem3  28447  lnconi  29607  prmdvdsbc  30303  ltesubnnd  30309  cshwrnid  30395  cycpmfv2  30477  madjusmdetlem2  30768  eulerpartlemgc  31298  reprle  31566  hgt750lemc  31599  hgt750lemd  31600  hgt750lemb  31608  hgt750leme  31610  tgoldbachgtde  31612  iprodgam  32527  faclimlem1  32528  faclimlem3  32530  faclim  32531  iprodfac  32532  knoppndvlem17  33420  poimirlem29  34395  heiborlem3  34566  heiborlem5  34568  heiborlem6  34569  heiborlem7  34570  heiborlem8  34571  heibor  34574  rrndstprj2  34584  rrncmslem  34585  rrnequiv  34588  zrtelqelz  38658  rtprmirr  38660  fltne  38713  fltltc  38714  fltnltalem  38715  fltnlta  38716  irrapxlem5  38853  pell14qrgapw  38903  pellqrexplicit  38904  pellqrex  38906  pellfundge  38909  pellfundgt1  38910  jm3.1lem1  39044  jm3.1lem2  39045  hashnzfz2  40103  xralrple4  41100  recnnltrp  41104  rpgtrecnn  41108  fsumnncl  41313  limsup10exlem  41514  stoweidlem31  41777  stoweidlem59  41805  wallispilem3  41813  wallispi  41816  stirlinglem12  41831  stirlinglem15  41834  fourierdlem73  41925  etransclem23  42003  nnfoctbdjlem  42198  ovnsubaddlem1  42313  ovolval5lem1  42395  ovolval5lem2  42396  vonioolem1  42423  vonioolem2  42424  vonicclem2  42427  fmtnoprmfac1lem  43124  sfprmdvdsmersenne  43166  lighneallem2  43169  proththd  43177  perfectALTVlem2  43285  fppr2odd  43294  fpprwppr  43302  fpprel2  43304  pw2m1lepw2m1  43973  logbge0b  44021  logblt1b  44022  logbpw2m1  44025  nnpw2pmod  44041  nnolog2flm1  44048  blennngt2o2  44050  dignnld  44061  digexp  44065  amgmlemALT  44301
  Copyright terms: Public domain W3C validator