Theorem nnrpd 12975

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 12945	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2119  ℕcn 12165  ℝ⁺crp 12933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-rp 12934

This theorem is referenced by:  zgt1rpn0n1  12976  modmulnn  13839  modaddid  13860  mulp1mod1  13864  modsumfzodifsn  13897  addmodlteq  13899  nnesq  14180  digit1  14190  bcpasc  14274  cshwn  14750  iseralt  15638  climcndslem2  15806  mertenslem1  15840  mertenslem2  15841  fprodmodd  15953  efcllem  16033  ege2le3  16046  eftlub  16067  effsumlt  16069  eirrlem  16162  sqrt2irrlem  16206  p1modz1  16219  dvdsmod  16289  bitsfzo  16395  bitsmod  16396  bitscmp  16398  bitsinv1lem  16401  sadaddlem  16426  sadasslem  16430  bitsres  16433  smumul  16453  bezoutlem3  16501  eucalglt  16545  prmind2  16645  prmdvdsbc  16687  crth  16739  eulerthlem2  16743  fermltl  16745  prmdiv  16746  prmdiveq  16747  odzdvds  16757  vfermltlALT  16764  powm2modprm  16765  modprm0  16767  modprmn0modprm0  16769  prmreclem3  16880  prmreclem5  16882  prmreclem6  16883  4sqlem5  16904  4sqlem6  16905  4sqlem7  16906  4sqlem10  16909  4sqlem12  16918  vdwlem1  16943  mndodcong  19508  odmod  19512  oddvds  19513  dfod2  19530  gexexlem  19818  zringlpirlem3  21439  fermltlchr  21504  met1stc  24504  met2ndci  24505  lebnumlem3  24948  lebnumii  24951  ovollb2lem  25473  ovoliunlem1  25487  ovoliunlem3  25489  uniioombllem6  25573  itg2cnlem2  25747  elqaalem2  26304  aalioulem2  26317  aalioulem4  26319  aalioulem5  26320  aaliou2b  26325  aaliou3lem9  26334  logfac  26583  cxpeq  26739  zrtelqelz  26740  rtprmirr  26742  logbgcd1irr  26776  leibpi  26924  birthdaylem2  26934  amgmlem  26971  emcllem1  26977  emcllem2  26978  emcllem3  26979  emcllem5  26981  harmoniclbnd  26990  harmonicubnd  26991  harmonicbnd4  26992  fsumharmonic  26993  zetacvg  26996  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem4  27013  lgamgulmlem5  27014  lgamgulmlem6  27015  lgamgulm2  27017  lgambdd  27018  lgamucov  27019  lgamcvg2  27036  gamcvg  27037  gamcvg2lem  27040  regamcl  27042  relgamcl  27043  lgam1  27045  wilthlem1  27049  wilthlem2  27050  basellem1  27062  basellem6  27067  basellem8  27069  chtf  27089  efchtcl  27092  chtge0  27093  vmacl  27099  efvmacl  27101  sgmnncl  27128  chtprm  27134  chtdif  27139  efchtdvds  27140  prmorcht  27159  sgmppw  27178  vmalelog  27186  chtleppi  27191  chtublem  27192  fsumvma2  27195  pclogsum  27196  vmasum  27197  chpchtsum  27200  chpub  27201  logfacubnd  27202  logfaclbnd  27203  logfacbnd3  27204  logfacrlim  27205  logexprlim  27206  logfacrlim2  27207  perfectlem2  27211  bclbnd  27261  bposlem1  27265  bposlem2  27266  bposlem4  27268  bposlem5  27269  bposlem6  27270  bposlem7  27271  bposlem9  27273  lgslem1  27278  lgsvalmod  27297  lgsmod  27304  lgsdirprm  27312  lgsne0  27316  lgsqrlem2  27328  gausslemma2dlem0i  27345  gausslemma2dlem5a  27351  gausslemma2d  27355  lgseisenlem1  27356  lgseisenlem2  27357  lgseisenlem3  27358  lgseisenlem4  27359  lgseisen  27360  lgsquadlem2  27362  lgsquadlem3  27363  m1lgs  27369  2sqlem8  27407  2sqmod  27417  chebbnd1lem1  27450  chebbnd1lem2  27451  chebbnd1lem3  27452  chebbnd1  27453  chtppilimlem1  27454  chtppilimlem2  27455  chtppilim  27456  chebbnd2  27458  chto1lb  27459  vmadivsum  27463  vmadivsumb  27464  rplogsumlem1  27465  rplogsumlem2  27466  dchrisum0lem1a  27467  rpvmasumlem  27468  dchrisumlema  27469  dchrisumlem1  27470  dchrisumlem2  27471  dchrmusum2  27475  dchrvmasumlem1  27476  dchrvmasum2lem  27477  dchrvmasum2if  27478  dchrvmasumlem2  27479  dchrvmasumlem3  27480  dchrvmasumiflem1  27482  dchrvmasumiflem2  27483  dchrisum0flblem2  27490  dchrisum0fno1  27492  dchrisum0lema  27495  dchrisum0lem1b  27496  dchrisum0lem1  27497  dchrisum0lem2a  27498  dchrisum0lem2  27499  dchrisum0lem3  27500  dchrisum0  27501  dirith2  27509  mudivsum  27511  mulogsumlem  27512  mulogsum  27513  mulog2sumlem1  27515  mulog2sumlem2  27516  mulog2sumlem3  27517  vmalogdivsum2  27519  vmalogdivsum  27520  2vmadivsumlem  27521  logsqvma  27523  log2sumbnd  27525  selberglem1  27526  selberglem2  27527  selberglem3  27528  selberg  27529  selbergb  27530  selberg2lem  27531  selberg2  27532  selberg2b  27533  chpdifbndlem1  27534  logdivbnd  27537  selberg3lem1  27538  selberg3lem2  27539  selberg3  27540  selberg4lem1  27541  selberg4  27542  pntrsumo1  27546  pntrsumbnd2  27548  selbergr  27549  selberg3r  27550  selberg4r  27551  selberg34r  27552  pntsf  27554  pntsval2  27557  pntrlog2bndlem1  27558  pntrlog2bndlem2  27559  pntrlog2bndlem3  27560  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntrlog2bndlem6  27564  pntrlog2bnd  27565  pntpbnd1a  27566  pntpbnd1  27567  pntpbnd2  27568  pntibndlem2  27572  pntlemn  27581  pntlemj  27584  pntlemf  27586  pntlemk  27587  pntlemo  27588  pnt  27595  padicabvcxp  27613  ostth2lem2  27615  ostth2lem3  27616  ostth2lem4  27617  ostth2  27618  ostth3  27619  clwwisshclwwslemlem  30101  numclwwlk5  30476  numclwwlk7  30479  nrt2irr  30561  ubthlem2  30960  minvecolem3  30965  lnconi  32122  ltesubnnd  32915  2exple2exp  32937  cshwrnid  33040  cycpmfv2  33195  znfermltl  33449  madjusmdetlem2  34012  eulerpartlemgc  34546  reprle  34798  hgt750lemc  34831  hgt750lemd  34832  hgt750lemb  34840  hgt750leme  34842  tgoldbachgtde  34844  iprodgam  35970  faclimlem1  35971  faclimlem3  35973  faclim  35974  iprodfac  35975  knoppndvlem17  36834  poimirlem29  38016  heiborlem3  38180  heiborlem5  38182  heiborlem6  38183  heiborlem7  38184  heiborlem8  38185  heibor  38188  rrndstprj2  38198  rrncmslem  38199  rrnequiv  38202  lcmineqlem20  42533  lcmineqlem23  42536  3lexlogpow5ineq2  42540  3lexlogpow2ineq2  42544  aks4d1p5  42565  aks4d1p6  42566  aks4d1p8d2  42570  aks4d1p8  42572  remexz  42589  hashscontpow1  42606  aks6d1c2lem4  42612  aks6d1c2  42615  bcled  42663  bcle2d  42664  aks6d1c7lem1  42665  dvdsexpnn  42810  fltne  43094  flt4lem7  43109  fltltc  43111  fltnltalem  43112  fltnlta  43113  irrapxlem5  43271  pell14qrgapw  43321  pellqrexplicit  43322  pellqrex  43324  pellfundge  43327  pellfundgt1  43328  jm3.1lem1  43462  jm3.1lem2  43463  hashnzfz2  44765  xralrple4  45817  recnnltrp  45821  rpgtrecnn  45824  fsumnncl  46017  limsup10exlem  46215  stoweidlem31  46474  stoweidlem59  46502  wallispilem3  46510  wallispi  46513  stirlinglem12  46528  stirlinglem15  46531  fourierdlem73  46622  etransclem23  46700  nnfoctbdjlem  46898  ovnsubaddlem1  47013  ovolval5lem1  47095  ovolval5lem2  47096  vonioolem1  47123  vonioolem2  47124  vonicclem2  47127  2timesltsqm1  47842  fmtnoprmfac1lem  48042  sfprmdvdsmersenne  48081  lighneallem2  48084  proththd  48092  perfectALTVlem2  48213  fppr2odd  48222  fpprwppr  48230  fpprel2  48232  gpgedgvtx1  48553  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx13starlem2  48563  gpg3nbgrvtx0  48567  pw2m1lepw2m1  49011  logbge0b  49054  logblt1b  49055  logbpw2m1  49058  nnpw2pmod  49074  nnolog2flm1  49081  blennngt2o2  49083  dignnld  49094  digexp  49098  amgmlemALT  50293