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

Theorem nnrpd 10391
Description: A natural number 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 10365 . 2  |-  ( A  e.  NN  ->  A  e.  RR+ )
31, 2syl 15 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1686   NNcn 9748   RR+crp 10356
This theorem is referenced by:  modmulnn  10990  nnesq  11227  digit1  11237  bcpasc  11335  iseralt  12159  mertenslem1  12342  mertenslem2  12343  ege2le3  12373  eftlub  12391  effsumlt  12393  eirrlem  12484  sqr2irrlem  12528  dvdsmod  12587  bitsfzo  12628  bitsmod  12629  bitscmp  12631  bitsinv1lem  12634  sadaddlem  12659  sadasslem  12663  bitsres  12666  smumul  12686  bezoutlem3  12721  eucalglt  12757  prmind2  12771  crt  12848  eulerthlem2  12852  fermltl  12854  prmdiv  12855  prmdiveq  12856  odzdvds  12862  prmreclem3  12967  prmreclem5  12969  prmreclem6  12970  4sqlem5  12991  4sqlem6  12992  4sqlem7  12993  4sqlem10  12996  4sqlem12  13005  vdwlem1  13030  mndodcong  14859  odmod  14863  oddvds  14864  dfod2  14879  gexexlem  15146  zlpirlem3  16445  met1stc  18069  met2ndci  18070  lebnumlem3  18463  lebnumii  18466  ovollb2lem  18849  ovoliunlem1  18863  ovoliunlem3  18865  uniioombllem6  18945  itg2cnlem2  19119  elqaalem2  19702  aalioulem2  19715  aalioulem4  19717  aalioulem5  19718  aaliou2b  19723  aaliou3lem9  19732  logfac  19956  cxpeq  20099  leibpi  20240  amgmlem  20286  emcllem1  20291  emcllem2  20292  emcllem3  20293  emcllem5  20295  harmoniclbnd  20304  harmonicubnd  20305  harmonicbnd4  20306  fsumharmonic  20307  wilthlem1  20308  wilthlem2  20309  basellem1  20320  basellem6  20325  basellem8  20327  chtf  20348  efchtcl  20351  chtge0  20352  vmacl  20358  efvmacl  20360  sgmnncl  20387  chtprm  20393  chtdif  20398  efchtdvds  20399  prmorcht  20418  sgmppw  20438  vmalelog  20446  chtleppi  20451  chtublem  20452  fsumvma2  20455  pclogsum  20456  vmasum  20457  chpchtsum  20460  chpub  20461  logfacubnd  20462  logfaclbnd  20463  logfacbnd3  20464  logfacrlim  20465  logexprlim  20466  logfacrlim2  20467  perfectlem2  20471  bclbnd  20521  bposlem1  20525  bposlem2  20526  bposlem4  20528  bposlem5  20529  bposlem6  20530  bposlem7  20531  bposlem9  20533  lgslem1  20537  lgslem4  20540  lgsvalmod  20556  lgsmod  20562  lgsdirprm  20570  lgsne0  20574  lgsqrlem2  20583  lgseisenlem1  20590  lgseisenlem2  20591  lgseisenlem3  20592  lgseisenlem4  20593  lgseisen  20594  lgsquadlem2  20596  lgsquadlem3  20597  m1lgs  20603  2sqlem8  20613  chebbnd1lem1  20620  chebbnd1lem2  20621  chebbnd1lem3  20622  chebbnd1  20623  chtppilimlem1  20624  chtppilimlem2  20625  chtppilim  20626  chebbnd2  20628  chto1lb  20629  vmadivsum  20633  vmadivsumb  20634  rplogsumlem1  20635  rplogsumlem2  20636  dchrisum0lem1a  20637  rpvmasumlem  20638  dchrisumlema  20639  dchrisumlem1  20640  dchrisumlem2  20641  dchrmusum2  20645  dchrvmasumlem1  20646  dchrvmasum2lem  20647  dchrvmasum2if  20648  dchrvmasumlem2  20649  dchrvmasumlem3  20650  dchrvmasumiflem1  20652  dchrvmasumiflem2  20653  dchrisum0flblem2  20660  dchrisum0fno1  20662  dchrisum0lema  20665  dchrisum0lem1b  20666  dchrisum0lem1  20667  dchrisum0lem2a  20668  dchrisum0lem2  20669  dchrisum0lem3  20670  dchrisum0  20671  dirith2  20679  mudivsum  20681  mulogsumlem  20682  mulogsum  20683  mulog2sumlem1  20685  mulog2sumlem2  20686  mulog2sumlem3  20687  vmalogdivsum2  20689  vmalogdivsum  20690  2vmadivsumlem  20691  logsqvma  20693  log2sumbnd  20695  selberglem1  20696  selberglem2  20697  selberglem3  20698  selberg  20699  selbergb  20700  selberg2lem  20701  selberg2  20702  selberg2b  20703  chpdifbndlem1  20704  logdivbnd  20707  selberg3lem1  20708  selberg3lem2  20709  selberg3  20710  selberg4lem1  20711  selberg4  20712  pntrsumo1  20716  pntrsumbnd2  20718  selbergr  20719  selberg3r  20720  selberg4r  20721  selberg34r  20722  pntsf  20724  pntsval2  20727  pntrlog2bndlem1  20728  pntrlog2bndlem2  20729  pntrlog2bndlem3  20730  pntrlog2bndlem4  20731  pntrlog2bndlem5  20732  pntrlog2bndlem6  20734  pntrlog2bnd  20735  pntpbnd1a  20736  pntpbnd1  20737  pntpbnd2  20738  pntibndlem2  20742  pntlemn  20751  pntlemj  20754  pntlemf  20756  pntlemk  20757  pntlemo  20758  pnt  20765  padicabvcxp  20783  ostth2lem2  20785  ostth2lem3  20786  ostth2lem4  20787  ostth2  20788  ostth3  20789  ubthlem2  21452  minvecolem3  21457  lnconi  22615  ltesubnnd  23035  rnlogblem  23403  zetacvg  23691  heiborlem3  26548  heiborlem5  26550  heiborlem6  26551  heiborlem7  26552  heiborlem8  26553  heibor  26556  rrndstprj2  26566  rrncmslem  26567  rrnequiv  26570  irrapxlem5  26922  pell14qrgapw  26972  pellqrexplicit  26973  pellqrex  26975  pellfundge  26978  pellfundgt1  26979  jm3.1lem1  27121  jm3.1lem2  27122  stoweidlem59  27819  wallispilem3  27827  wallispi  27830  stirlinglem12  27845  stirlinglem15  27848
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-resscn 8796  ax-1cn 8797  ax-icn 8798  ax-addcl 8799  ax-addrcl 8800  ax-mulcl 8801  ax-mulrcl 8802  ax-mulcom 8803  ax-addass 8804  ax-mulass 8805  ax-distr 8806  ax-i2m1 8807  ax-1ne0 8808  ax-1rid 8809  ax-rnegex 8810  ax-rrecex 8811  ax-cnre 8812  ax-pre-lttri 8813  ax-pre-lttrn 8814  ax-pre-ltadd 8815  ax-pre-mulgt0 8816
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-riota 6306  df-recs 6390  df-rdg 6425  df-er 6662  df-en 6866  df-dom 6867  df-sdom 6868  df-pnf 8871  df-mnf 8872  df-xr 8873  df-ltxr 8874  df-le 8875  df-sub 9041  df-neg 9042  df-nn 9749  df-rp 10357
  Copyright terms: Public domain W3C validator