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

Theorem nnrpd 11373
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 11345 . 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 1898   NNcn 10642   RR+crp 11336
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-nn 10643  df-rp 11337
This theorem is referenced by:  zgt1rpn0n1  11374  modmulnn  12152  nnesq  12434  digit1  12444  bcpasc  12544  cshwn  12942  iseralt  13806  mertenslem1  13995  mertenslem2  13996  ege2le3  14199  eftlub  14218  effsumlt  14220  eirrlem  14311  sqr2irrlem  14355  dvdsmod  14417  bitsfzo  14464  bitsmod  14465  bitscmp  14467  bitsinv1lem  14470  sadaddlem  14495  sadasslem  14499  bitsres  14502  smumul  14522  bezoutlem3OLD  14560  bezoutlem3  14563  eucalglt  14599  prmind2  14690  crt  14781  eulerthlem2  14785  fermltl  14787  prmdiv  14788  prmdiveq  14789  odzdvds  14795  odzdvdsOLD  14801  vfermltlALT  14808  powm2modprm  14809  modprm0  14811  modprmn0modprm0  14813  prmreclem3  14917  prmreclem5  14919  prmreclem6  14920  4sqlem5  14941  4sqlem6  14942  4sqlem7  14943  4sqlem10  14946  4sqlem12  14955  vdwlem1  14986  mndodcong  17246  odmod  17250  oddvds  17251  dfod2  17270  gexexlem  17545  zringlpirlem3OLD  19110  zringlpirlem3  19112  met1stc  21591  met2ndci  21592  lebnumlem3  22046  lebnumlem3OLD  22049  lebnumii  22052  ovollb2lem  22496  ovoliunlem1  22510  ovoliunlem3  22512  uniioombllem6  22602  itg2cnlem2  22776  elqaalem2  23329  elqaalem2OLD  23332  aalioulem2  23345  aalioulem4  23347  aalioulem5  23348  aaliou2b  23353  aaliou3lem9  23362  logfac  23606  cxpeq  23753  leibpi  23924  amgmlem  23971  emcllem1  23977  emcllem2  23978  emcllem3  23979  emcllem5  23981  harmoniclbnd  23990  harmonicubnd  23991  harmonicbnd4  23992  fsumharmonic  23993  zetacvg  23996  lgamgulmlem2  24011  lgamgulmlem3  24012  lgamgulmlem4  24013  lgamgulmlem5  24014  lgamgulmlem6  24015  lgamgulm2  24017  lgambdd  24018  lgamucov  24019  lgamcvg2  24036  gamcvg  24037  gamcvg2lem  24040  regamcl  24042  relgamcl  24043  lgam1  24045  wilthlem1  24049  wilthlem2  24050  basellem1  24063  basellem6  24068  basellem8  24070  chtf  24091  efchtcl  24094  chtge0  24095  vmacl  24101  efvmacl  24103  sgmnncl  24130  chtprm  24136  chtdif  24141  efchtdvds  24142  prmorcht  24161  sgmppw  24181  vmalelog  24189  chtleppi  24194  chtublem  24195  fsumvma2  24198  pclogsum  24199  vmasum  24200  chpchtsum  24203  chpub  24204  logfacubnd  24205  logfaclbnd  24206  logfacbnd3  24207  logfacrlim  24208  logexprlim  24209  logfacrlim2  24210  perfectlem2  24214  bclbnd  24264  bposlem1  24268  bposlem2  24269  bposlem4  24271  bposlem5  24272  bposlem6  24273  bposlem7  24274  bposlem9  24276  lgslem1  24280  lgslem4  24283  lgsvalmod  24299  lgsmod  24305  lgsdirprm  24313  lgsne0  24317  lgsqrlem2  24326  lgseisenlem1  24333  lgseisenlem2  24334  lgseisenlem3  24335  lgseisenlem4  24336  lgseisen  24337  lgsquadlem2  24339  lgsquadlem3  24340  m1lgs  24346  2sqlem8  24356  chebbnd1lem1  24363  chebbnd1lem2  24364  chebbnd1lem3  24365  chebbnd1  24366  chtppilimlem1  24367  chtppilimlem2  24368  chtppilim  24369  chebbnd2  24371  chto1lb  24372  vmadivsum  24376  vmadivsumb  24377  rplogsumlem1  24378  rplogsumlem2  24379  dchrisum0lem1a  24380  rpvmasumlem  24381  dchrisumlema  24382  dchrisumlem1  24383  dchrisumlem2  24384  dchrmusum2  24388  dchrvmasumlem1  24389  dchrvmasum2lem  24390  dchrvmasum2if  24391  dchrvmasumlem2  24392  dchrvmasumlem3  24393  dchrvmasumiflem1  24395  dchrvmasumiflem2  24396  dchrisum0flblem2  24403  dchrisum0fno1  24405  dchrisum0lema  24408  dchrisum0lem1b  24409  dchrisum0lem1  24410  dchrisum0lem2a  24411  dchrisum0lem2  24412  dchrisum0lem3  24413  dchrisum0  24414  dirith2  24422  mudivsum  24424  mulogsumlem  24425  mulogsum  24426  mulog2sumlem1  24428  mulog2sumlem2  24429  mulog2sumlem3  24430  vmalogdivsum2  24432  vmalogdivsum  24433  2vmadivsumlem  24434  logsqvma  24436  log2sumbnd  24438  selberglem1  24439  selberglem2  24440  selberglem3  24441  selberg  24442  selbergb  24443  selberg2lem  24444  selberg2  24445  selberg2b  24446  chpdifbndlem1  24447  logdivbnd  24450  selberg3lem1  24451  selberg3lem2  24452  selberg3  24453  selberg4lem1  24454  selberg4  24455  pntrsumo1  24459  pntrsumbnd2  24461  selbergr  24462  selberg3r  24463  selberg4r  24464  selberg34r  24465  pntsf  24467  pntsval2  24470  pntrlog2bndlem1  24471  pntrlog2bndlem2  24472  pntrlog2bndlem3  24473  pntrlog2bndlem4  24474  pntrlog2bndlem5  24475  pntrlog2bndlem6  24477  pntrlog2bnd  24478  pntpbnd1a  24479  pntpbnd1  24480  pntpbnd2  24481  pntibndlem2  24485  pntlemn  24494  pntlemj  24497  pntlemf  24499  pntlemk  24500  pntlemo  24501  pnt  24508  padicabvcxp  24526  ostth2lem2  24528  ostth2lem3  24529  ostth2lem4  24530  ostth2  24531  ostth3  24532  clwwisshclwwlem1  25589  numclwwlk5  25896  numclwwlk7  25898  ubthlem2  26569  minvecolem3  26574  minvecolem3OLD  26584  lnconi  27742  ltesubnnd  28437  2sqmod  28461  madjusmdetlem2  28705  eulerpartlemgc  29245  iprodgam  30428  faclimlem1  30429  faclimlem3  30431  faclim  30432  iprodfac  30433  poimirlem29  32015  heiborlem3  32191  heiborlem5  32193  heiborlem6  32194  heiborlem7  32195  heiborlem8  32196  heibor  32199  rrndstprj2  32209  rrncmslem  32210  rrnequiv  32213  irrapxlem5  35716  pell14qrgapw  35768  pellqrexplicit  35769  pellqrex  35772  pellfundge  35776  pellfundgt1  35777  jm3.1lem1  35918  jm3.1lem2  35919  hashnzfz2  36715  fsumnncl  37735  stoweidlem31  37993  stoweidlem59  38021  wallispilem3  38030  wallispi  38033  stirlinglem12  38048  stirlinglem15  38051  fourierdlem73  38144  etransclem23  38223  nnfoctbdjlem  38398  ovnsubaddlem1  38499  ovolval5lem1  38581  ovolval5lem2  38582  perfectALTVlem2  38979  proththd  39049  pw2m1lepw2m1  40687  logbge0b  40743  logblt1b  40744  logbpw2m1  40747  nnpw2pmod  40763  nnolog2flm1  40770  blennngt2o2  40772  dignnld  40783  digexp  40787
  Copyright terms: Public domain W3C validator