Theorem nnnn0d 11956

Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnnn0d.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnnn0d	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0d

Step	Hyp	Ref	Expression
1		nnssnn0 11901	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sseldi 3965	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 11638  ℕ₀cn0 11898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-n0 11899

This theorem is referenced by:  nn0ge2m1nn0  11966  nnzd  12087  eluzge2nn0  12288  expgt1  13468  expaddzlem  13473  expaddz  13474  expmulz  13476  expmulnbnd  13597  facwordi  13650  faclbnd  13651  facavg  13662  bcm1k  13676  wrdeqs1cat  14082  cshwcsh2id  14190  relexpsucnnr  14384  isercolllem2  15022  bcxmas  15190  climcndslem1  15204  climcndslem2  15205  climcnds  15206  pwdif  15223  geo2sum  15229  mertenslem1  15240  prodmolem3  15287  prodmolem2a  15288  bpolydiflem  15408  eftabs  15429  efcllem  15431  eftlub  15462  eirrlem  15557  rpnnen2lem9  15575  rpnnen2lem11  15577  dvdsfac  15676  pwp1fsum  15742  oddpwp1fsum  15743  bitsfzo  15784  bitsfi  15786  sadcaddlem  15806  smumullem  15841  gcdcl  15855  dvdsgcdidd  15885  mulgcd  15896  rplpwr  15907  rppwr  15908  lcmcl  15945  lcmgcdnn  15955  lcmfcl  15972  nprmdvds1  16050  rpexp  16064  zsqrtelqelz  16098  phiprmpw  16113  eulerthlem2  16119  eulerth  16120  fermltl  16121  odzcllem  16129  odzdvds  16132  odzphi  16133  prm23lt5  16151  pythagtriplem6  16158  pythagtriplem7  16159  pcprmpw2  16218  dvdsprmpweqle  16222  pcprod  16231  pcfac  16235  pcbc  16236  expnprm  16238  pockthlem  16241  pockthg  16242  prmunb  16250  prmreclem2  16253  prmreclem3  16254  prmreclem4  16255  prmreclem5  16256  prmreclem6  16257  mul4sqlem  16289  4sqlem11  16291  4sqlem17  16297  vdwlem1  16317  vdwlem5  16321  vdwlem6  16322  vdwlem8  16324  vdwlem9  16325  vdwlem11  16327  vdwlem12  16328  vdwnnlem3  16333  ramz2  16360  ramub1lem1  16362  ramub1lem2  16363  ramub1  16364  prmgaplem3  16389  2expltfac  16426  psgnunilem3  18624  odfval  18660  mndodconglem  18669  gexcl3  18712  pgpfi1  18720  sylow1lem1  18723  gexexlem  18972  prmcyg  19014  gsumval3  19027  ablfacrplem  19187  ablfacrp  19188  ablfacrp2  19189  ablfac1eu  19195  prmgrpsimpgd  19236  srgbinomlem3  19292  srgbinomlem4  19293  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  cpmadugsumlemF  21484  ovoliunlem1  24103  mbfi1fseqlem1  24316  mbfi1fseqlem3  24318  mbfi1fseqlem5  24320  itg2cnlem2  24363  dvply1  24873  aalioulem2  24922  aalioulem5  24925  aaliou3lem1  24931  aaliou3lem2  24932  aaliou3lem8  24934  aaliou3lem6  24937  taylthlem1  24961  taylthlem2  24962  pserdvlem2  25016  cxpeq  25338  dmgmdivn0  25605  lgamgulmlem5  25610  lgamcvg2  25632  wilthlem1  25645  ftalem1  25650  ftalem2  25651  ftalem4  25653  ftalem5  25654  basellem2  25659  basellem3  25660  basellem4  25661  basellem5  25662  isppw2  25692  dvdsmulf1o  25771  sgmmul  25777  fsumvma2  25790  chpchtsum  25795  logfacubnd  25797  mersenne  25803  perfect1  25804  perfectlem1  25805  perfectlem2  25806  perfect  25807  dchrelbas3  25814  dchrelbasd  25815  dchrzrh1  25820  dchrzrhmul  25822  dchrmulcl  25825  dchrn0  25826  dchrfi  25831  dchrghm  25832  dchrabs  25836  dchrinv  25837  dchrptlem1  25840  dchrptlem2  25841  dchrptlem3  25842  dchrpt  25843  dchrsum2  25844  sum2dchr  25850  pcbcctr  25852  bcmono  25853  bclbnd  25856  bposlem1  25860  bposlem3  25862  bposlem5  25864  bposlem6  25865  lgslem1  25873  lgsval2lem  25883  lgsvalmod  25892  lgsmod  25899  lgsdirprm  25907  lgsne0  25911  lgsqrlem1  25922  lgsqrlem2  25923  lgsqrlem3  25924  lgsqrlem4  25925  gausslemma2dlem0b  25933  gausslemma2dlem0c  25934  gausslemma2dlem1  25942  gausslemma2dlem7  25949  gausslemma2d  25950  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgseisenlem4  25954  lgseisen  25955  lgsquadlem2  25957  lgsquadlem3  25958  m1lgs  25964  2lgslem1a  25967  2sqlem3  25996  2sqblem  26007  chebbnd1lem1  26045  chebbnd1lem3  26047  rplogsumlem2  26061  rpvmasumlem  26063  dchrisumlem1  26065  dchrisumlem2  26066  dchrmusum2  26070  dchrvmasumlem3  26075  dchrisum0ff  26083  dchrisum0flblem1  26084  rpvmasum2  26088  dchrisum0re  26089  dchrisum0lem2a  26093  dirith  26105  mudivsum  26106  pntpbnd1a  26161  pntlemq  26177  pntlemr  26178  pntlemj  26179  ostth2lem1  26194  ostth2lem2  26210  ostth2lem3  26211  ostth2  26213  crctcshwlkn0lem6  27593  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  clwwlknon  27869  eucrctshift  28022  numclwlk1lem2  28149  dipcl  28489  dipcn  28497  bcm1n  30518  prmdvdsbc  30532  psgnfzto1st  30747  isarchi2  30814  submarchi  30815  freshmansdream  30859  submateqlem1  31072  madjusmdetlem2  31093  madjusmdetlem4  31095  mdetlap  31097  nexple  31268  oddpwdc  31612  eulerpartlemsv2  31616  eulerpartlemsf  31617  eulerpartlems  31618  eulerpartlemv  31622  eulerpartlemb  31626  plymulx0  31817  signsvtn0  31840  fsum2dsub  31878  reprinfz1  31893  reprpmtf1o  31897  circlemeth  31911  circlemethnat  31912  hgt750lemb  31927  hgt750lema  31928  hgt750leme  31929  tgoldbachgtde  31931  tgoldbachgtda  31932  lpadleft  31954  subfacp1lem1  32426  subfacp1lem6  32432  subfaclim  32435  erdszelem8  32445  erdszelem10  32447  cvmliftlem10  32541  faclim2  32980  poimirlem7  34914  poimirlem17  34924  poimirlem18  34925  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  poimirlem32  34939  nninfnub  35041  bfplem1  35115  oexpreposd  39228  nn0rppwr  39231  expgcd  39232  zrtelqelz  39241  dffltz  39320  fltne  39321  fltltc  39322  fltnltalem  39323  fltnlta  39324  3rexfrabdioph  39443  4rexfrabdioph  39444  6rexfrabdioph  39445  7rexfrabdioph  39446  irrapxlem5  39472  pellexlem2  39476  pellexlem6  39480  pell14qrgt0  39505  pell1qrge1  39516  pellfundgt1  39529  ltrmxnn0  39595  jm2.26lem3  39647  jm2.27a  39651  jm2.27c  39653  rmxdiophlem  39661  jm3.1lem1  39663  jm3.1lem2  39664  jm3.1lem3  39665  jm3.1  39666  dgrsub2  39784  mpaaeu  39799  idomsubgmo  39847  relexpxpmin  40111  nzprmdif  40700  binomcxplemwb  40729  fperiodmul  41620  xralrple4  41690  fsumnncl  41901  dvsinexp  42244  dvxpaek  42274  itgsinexplem1  42288  stoweidlem1  42335  stoweidlem17  42351  stoweidlem25  42359  stoweidlem34  42368  stoweidlem38  42372  stoweidlem40  42374  stoweidlem42  42376  stoweidlem45  42379  stirlinglem4  42411  stirlinglem5  42412  stirlinglem10  42417  stirlinglem13  42420  dirkertrigeq  42435  fourierdlem21  42462  fourierdlem25  42466  fourierdlem48  42488  fourierdlem54  42494  fourierdlem64  42504  fourierdlem65  42505  fourierdlem73  42513  fourierdlem81  42521  fourierdlem83  42523  fourierdlem92  42532  fourierdlem103  42543  fourierdlem104  42544  fourierdlem112  42552  fourierdlem113  42553  etransclem1  42569  etransclem4  42572  etransclem8  42576  etransclem15  42583  etransclem17  42585  etransclem18  42586  etransclem19  42587  etransclem20  42588  etransclem21  42589  etransclem22  42590  etransclem23  42591  etransclem24  42592  etransclem25  42593  etransclem27  42595  etransclem32  42600  etransclem35  42603  etransclem41  42609  etransclem44  42612  etransclem46  42614  iccpartigtl  43632  iccpartgt  43636  iccpartgel  43638  iccelpart  43642  odz2prm2pw  43774  fmtnoprmfac1  43776  fmtnoprmfac2  43778  2pwp1prm  43800  sfprmdvdsmersenne  43817  lighneallem4a  43822  proththdlem  43827  proththd  43828  perfectALTVlem1  43935  perfectALTVlem2  43936  perfectALTV  43937  fpprwpprb  43954  logbpw2m1  44676  nnpw2blenfzo  44690  nnolog2flm1  44699  dignn0fr  44710  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729