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

Theorem nnnn0d 10274
Description: A natural number is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnnn0d.1  |-  ( ph  ->  A  e.  NN )
Assertion
Ref Expression
nnnn0d  |-  ( ph  ->  A  e.  NN0 )

Proof of Theorem nnnn0d
StepHypRef Expression
1 nnssnn0 10224 . 2  |-  NN  C_  NN0
2 nnnn0d.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3346 1  |-  ( ph  ->  A  e.  NN0 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   NNcn 10000   NN0cn0 10221
This theorem is referenced by:  nnzd  10374  expgt1  11418  expaddzlem  11423  expaddz  11424  expmulz  11426  expmulnbnd  11511  facwordi  11580  faclbnd  11581  facavg  11592  bcm1k  11606  wrdeqs1cat  11789  isercolllem2  12459  bcxmas  12615  climcndslem1  12629  climcndslem2  12630  climcnds  12631  geo2sum  12650  mertenslem1  12661  eftabs  12678  efcllem  12680  eftlub  12710  eirrlem  12803  rpnnen2lem9  12822  rpnnen2lem11  12824  dvdsfac  12904  bitsfzo  12947  bitsfi  12949  sadcaddlem  12969  smumullem  13004  gcdcl  13017  mulgcd  13046  rplpwr  13056  rppwr  13057  nprmdvds1  13111  isprm5  13112  rpexp  13120  zsqrelqelz  13150  dfphi2  13163  phiprmpw  13165  eulerthlem2  13171  eulerth  13172  fermltl  13173  odzcllem  13178  odzdvds  13181  odzphi  13182  pythagtriplem6  13195  pythagtriplem7  13196  pcprmpw2  13255  pcprod  13264  pcfac  13268  pcbc  13269  expnprm  13271  pockthlem  13273  pockthg  13274  prmunb  13282  prmreclem2  13285  prmreclem3  13286  prmreclem4  13287  prmreclem5  13288  prmreclem6  13289  mul4sqlem  13321  4sqlem11  13323  4sqlem17  13329  vdwlem1  13349  vdwlem5  13353  vdwlem6  13354  vdwlem8  13356  vdwlem9  13357  vdwlem11  13359  vdwlem12  13360  vdwnnlem3  13365  ramz2  13392  ramub1lem1  13394  ramub1lem2  13395  ramub1  13396  2expltfac  13426  mndodconglem  15179  gexcl3  15221  pgpfi1  15229  sylow1lem1  15232  gexexlem  15467  prmcyg  15503  gsumval3  15514  ablfacrplem  15623  ablfacrp  15624  ablfacrp2  15625  ablfac1eu  15631  ovoliunlem1  19398  mbfi1fseqlem1  19607  mbfi1fseqlem3  19609  mbfi1fseqlem5  19611  itg2cnlem2  19654  dvply1  20201  aalioulem2  20250  aalioulem5  20253  aaliou3lem1  20259  aaliou3lem2  20260  aaliou3lem8  20262  aaliou3lem6  20265  taylthlem1  20289  taylthlem2  20290  pserdvlem2  20344  cxpeq  20641  wilthlem1  20851  ftalem1  20855  ftalem2  20856  ftalem4  20858  ftalem5  20859  basellem2  20864  basellem3  20865  basellem4  20866  basellem5  20867  isppw2  20898  dvdsmulf1o  20979  sgmmul  20985  chpchtsum  21003  logfacubnd  21005  mersenne  21011  perfect1  21012  perfectlem1  21013  perfectlem2  21014  perfect  21015  dchrelbas3  21022  dchrelbasd  21023  dchrzrh1  21028  dchrzrhmul  21030  dchrmulcl  21033  dchrn0  21034  dchrfi  21039  dchrghm  21040  dchrabs  21044  dchrinv  21045  dchrptlem1  21048  dchrptlem2  21049  dchrptlem3  21050  dchrpt  21051  dchrsum2  21052  sum2dchr  21058  pcbcctr  21060  bcmono  21061  bclbnd  21064  bposlem1  21068  bposlem3  21070  bposlem5  21072  bposlem6  21073  lgslem1  21080  lgslem4  21083  lgsval2lem  21090  lgsvalmod  21099  lgsmod  21105  lgsdirprm  21113  lgsne0  21117  lgsqrlem1  21125  lgsqrlem2  21126  lgsqrlem3  21127  lgsqrlem4  21128  lgseisenlem1  21133  lgseisenlem2  21134  lgseisenlem3  21135  lgseisenlem4  21136  lgseisen  21137  lgsquadlem2  21139  lgsquadlem3  21140  m1lgs  21146  2sqlem3  21150  2sqblem  21161  chebbnd1lem1  21163  chebbnd1lem3  21165  rplogsumlem2  21179  rpvmasumlem  21181  dchrisumlem1  21183  dchrisumlem2  21184  dchrmusum2  21188  dchrvmasumlem3  21193  dchrisum0ff  21201  dchrisum0flblem1  21202  rpvmasum2  21206  dchrisum0re  21207  dchrisum0lem2a  21211  dirith  21223  mudivsum  21224  pntpbnd1a  21279  pntlemq  21295  pntlemr  21296  pntlemj  21297  ostth2lem2  21328  ostth2lem3  21329  ostth2  21331  dipcl  22211  dipcn  22219  sspival  22237  bcm1n  24151  dmgmdivn0  24812  lgamgulmlem5  24817  lgamcvg2  24839  subfacp1lem1  24865  subfacp1lem6  24871  subfaclim  24874  erdszelem8  24884  erdszelem10  24886  cvmliftlem10  24981  prodmolem3  25259  prodmolem2a  25260  faclim2  25367  bpolydiflem  26100  nninfnub  26455  bfplem1  26531  3rexfrabdioph  26857  4rexfrabdioph  26858  6rexfrabdioph  26859  7rexfrabdioph  26860  irrapxlem5  26889  pellexlem2  26893  pellexlem6  26897  pell14qrgt0  26922  pell1qrge1  26933  pellfundgt1  26946  ltrmxnn0  27014  jm2.26lem3  27072  jm2.27a  27076  jm2.27c  27078  rmxdiophlem  27086  jm3.1lem1  27088  jm3.1lem2  27089  jm3.1lem3  27090  jm3.1  27091  dgrsub2  27316  mpaaeu  27332  psgnunilem3  27396  idomsubgmo  27491  dvsinexp  27716  itgsinexplem1  27724  stoweidlem1  27726  stoweidlem17  27742  stoweidlem25  27750  stoweidlem34  27759  stoweidlem38  27763  stoweidlem40  27765  stoweidlem42  27767  stoweidlem45  27770  stirlinglem4  27802  stirlinglem5  27803  stirlinglem10  27808  stirlinglem13  27811  cshwssizensame  28289
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-un 3325  df-in 3327  df-ss 3334  df-n0 10222
  Copyright terms: Public domain W3C validator