Theorem nnnn0d 12453

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 12395	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3928	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2113  ℕcn 12136  ℕ₀cn0 12392

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915  df-n0 12393

This theorem is referenced by:  nn0ge2m1nn0  12463  nnzd  12505  eluzge2nn0  12796  expgt1  14014  expaddzlem  14019  expaddz  14020  expmulz  14022  expmulnbnd  14149  exp11nnd  14175  facwordi  14203  faclbnd  14204  facavg  14215  bcm1k  14229  wrdeqs1cat  14634  cshwcsh2id  14742  relexpsucnnr  14939  isercolllem2  15580  bcxmas  15749  climcndslem1  15763  climcndslem2  15764  climcnds  15765  pwdif  15782  geo2sum  15787  mertenslem1  15798  prodmolem3  15847  prodmolem2a  15848  bpolydiflem  15968  eftabs  15989  efcllem  15991  eftlub  16025  eirrlem  16120  rpnnen2lem9  16138  rpnnen2lem11  16140  dvdsfac  16244  pwp1fsum  16309  oddpwp1fsum  16310  bitsfzo  16353  bitsfi  16355  sadcaddlem  16375  smumullem  16410  gcdcl  16424  dvdsgcdidd  16455  mulgcd  16466  rplpwr  16476  rprpwr  16477  rppwr  16478  nn0rppwr  16479  expgcd  16481  lcmcl  16519  lcmgcdnn  16529  lcmfcl  16546  nprmdvds1  16624  rpexp  16640  prmdvdsbc  16644  zsqrtelqelz  16676  phiprmpw  16694  eulerthlem2  16700  eulerth  16701  fermltl  16702  odzcllem  16711  odzdvds  16714  odzphi  16715  prm23lt5  16733  pythagtriplem6  16740  pythagtriplem7  16741  pcprmpw2  16801  dvdsprmpweqle  16805  pcprod  16814  pcfac  16818  pcbc  16819  expnprm  16821  pockthlem  16824  pockthg  16825  prmunb  16833  prmreclem2  16836  prmreclem3  16837  prmreclem4  16838  prmreclem5  16839  prmreclem6  16840  mul4sqlem  16872  4sqlem11  16874  4sqlem17  16880  vdwlem1  16900  vdwlem5  16904  vdwlem6  16905  vdwlem8  16907  vdwlem9  16908  vdwlem11  16910  vdwlem12  16911  vdwnnlem3  16916  ramz2  16943  ramub1lem1  16945  ramub1lem2  16946  ramub1  16947  prmgaplem3  16972  2expltfac  17011  psgnunilem3  19416  odfval  19452  mndodconglem  19461  gexcl3  19507  pgpfi1  19515  sylow1lem1  19518  gexexlem  19772  prmcyg  19814  gsumval3  19827  ablfacrplem  19987  ablfacrp  19988  ablfacrp2  19989  ablfac1eu  19995  prmgrpsimpgd  20036  srgbinomlem3  20154  srgbinomlem4  20155  fermltlchr  21475  freshmansdream  21520  chfacfscmulgsum  22795  chfacfpmmulgsum  22799  cpmadugsumlemF  22811  ovoliunlem1  25450  mbfi1fseqlem1  25663  mbfi1fseqlem3  25665  mbfi1fseqlem5  25667  itg2cnlem2  25710  dvply1  26238  aalioulem2  26288  aalioulem5  26291  aaliou3lem1  26297  aaliou3lem2  26298  aaliou3lem8  26300  aaliou3lem6  26303  taylthlem1  26328  taylthlem2  26329  taylthlem2OLD  26330  pserdvlem2  26385  cxpeq  26714  zrtelqelz  26715  dmgmdivn0  26985  lgamgulmlem5  26990  lgamcvg2  27012  wilthlem1  27025  ftalem1  27030  ftalem2  27031  ftalem4  27033  ftalem5  27034  basellem2  27039  basellem3  27040  basellem4  27041  basellem5  27042  isppw2  27072  mpodvdsmulf1o  27151  dvdsmulf1o  27153  sgmmul  27159  fsumvma2  27172  chpchtsum  27177  logfacubnd  27179  mersenne  27185  perfect1  27186  perfectlem1  27187  perfectlem2  27188  perfect  27189  dchrelbas3  27196  dchrelbasd  27197  dchrzrh1  27202  dchrzrhmul  27204  dchrmulcl  27207  dchrn0  27208  dchrfi  27213  dchrghm  27214  dchrabs  27218  dchrinv  27219  dchrptlem1  27222  dchrptlem2  27223  dchrptlem3  27224  dchrpt  27225  dchrsum2  27226  sum2dchr  27232  pcbcctr  27234  bcmono  27235  bclbnd  27238  bposlem1  27242  bposlem3  27244  bposlem5  27246  bposlem6  27247  lgslem1  27255  lgsval2lem  27265  lgsvalmod  27274  lgsmod  27281  lgsdirprm  27289  lgsne0  27293  lgsqrlem1  27304  lgsqrlem2  27305  lgsqrlem3  27306  lgsqrlem4  27307  gausslemma2dlem0b  27315  gausslemma2dlem0c  27316  gausslemma2dlem1  27324  gausslemma2dlem7  27331  gausslemma2d  27332  lgseisenlem1  27333  lgseisenlem2  27334  lgseisenlem3  27335  lgseisenlem4  27336  lgseisen  27337  lgsquadlem2  27339  lgsquadlem3  27340  m1lgs  27346  2lgslem1a  27349  2sqlem3  27378  2sqblem  27389  chebbnd1lem1  27427  chebbnd1lem3  27429  rplogsumlem2  27443  rpvmasumlem  27445  dchrisumlem1  27447  dchrisumlem2  27448  dchrmusum2  27452  dchrvmasumlem3  27457  dchrisum0ff  27465  dchrisum0flblem1  27466  rpvmasum2  27470  dchrisum0re  27471  dchrisum0lem2a  27475  dirith  27487  mudivsum  27488  pntpbnd1a  27543  pntlemq  27559  pntlemr  27560  pntlemj  27561  ostth2lem1  27576  ostth2lem2  27592  ostth2lem3  27593  ostth2  27595  crctcshwlkn0lem6  29814  hashecclwwlkn1  30078  umgrhashecclwwlk  30079  clwwlknon  30091  eucrctshift  30244  numclwlk1lem2  30371  nrt2irr  30474  dipcl  30713  dipcn  30721  bcm1n  32803  expgt0b  32825  nexple  32853  2exple2exp  32854  oexpled  32856  wrdpmtrlast  33103  psgnfzto1st  33115  isarchi2  33195  submarchi  33196  znfermltl  33375  fldextrspundgdvdslem  33765  fldextrspundgdvds  33766  fldext2rspun  33767  constrext2chnlem  33835  cos9thpiminplylem2  33868  submateqlem1  33892  madjusmdetlem2  33913  madjusmdetlem4  33915  mdetlap  33917  oddpwdc  34439  eulerpartlemsv2  34443  eulerpartlemsf  34444  eulerpartlems  34445  eulerpartlemv  34449  eulerpartlemb  34453  plymulx0  34632  signsvtn0  34655  fsum2dsub  34692  reprinfz1  34707  reprpmtf1o  34711  circlemeth  34725  circlemethnat  34726  hgt750lemb  34741  hgt750lema  34742  hgt750leme  34743  tgoldbachgtde  34745  tgoldbachgtda  34746  lpadleft  34768  subfacp1lem1  35295  subfacp1lem6  35301  subfaclim  35304  erdszelem8  35314  erdszelem10  35316  cvmliftlem10  35410  faclim2  35864  poimirlem7  37740  poimirlem17  37750  poimirlem18  37751  poimirlem20  37753  poimirlem21  37754  poimirlem22  37755  poimirlem25  37758  poimirlem26  37759  poimirlem27  37760  poimirlem28  37761  poimirlem32  37765  nninfnub  37864  bfplem1  37935  zndvdchrrhm  42138  lcmineqlem1  42195  lcmineqlem2  42196  lcmineqlem8  42202  lcmineqlem10  42204  lcmineqlem11  42205  lcmineqlem15  42209  lcmineqlem16  42210  lcmineqlem18  42212  lcmineqlem19  42213  lcmineqlem20  42214  lcmineqlem21  42215  lcmineqlem22  42216  3lexlogpow2ineq2  42225  dvrelogpow2b  42234  aks4d1p1p2  42236  aks4d1p1p4  42237  aks4d1p1  42242  aks4d1p3  42244  aks4d1p7d1  42248  aks4d1p7  42249  aks4d1p8  42253  aks4d1p9  42254  isprimroot2  42260  primrootsunit1  42263  primrootscoprmpow  42265  posbezout  42266  primrootscoprbij  42268  primrootlekpowne0  42271  primrootspoweq0  42272  aks6d1c1p2  42275  aks6d1c1p3  42276  aks6d1c1p4  42277  aks6d1c1p5  42278  aks6d1c1p7  42279  aks6d1c1p6  42280  aks6d1c1p8  42281  aks6d1c2p2  42285  hashscontpowcl  42286  hashscontpow1  42287  hashscontpow  42288  aks6d1c4  42290  aks6d1c2lem3  42292  aks6d1c2lem4  42293  aks6d1c2  42296  sticksstones6  42317  sticksstones7  42318  sticksstones10  42321  sticksstones12a  42323  sticksstones12  42324  sticksstones20  42332  sticksstones22  42334  aks6d1c6lem2  42337  aks6d1c6lem3  42338  aks6d1c6lem4  42339  aks6d1c6isolem1  42340  aks6d1c6isolem2  42341  aks6d1c6lem5  42343  bcled  42344  bcle2d  42345  aks6d1c7lem1  42346  aks6d1c7  42350  aks5lem2  42353  aks5lem3a  42355  aks5lem5a  42357  grpods  42360  unitscyglem2  42362  unitscyglem4  42364  aks5lem7  42366  aks5  42370  sumcubes  42483  oexpreposd  42492  exp11d  42496  dvdsexpb  42505  fiabv  42706  fsuppind  42748  dffltz  42792  fltdvdsabdvdsc  42796  fltne  42802  flt4lem4  42807  flt4lem7  42817  fltltc  42819  fltnltalem  42820  fltnlta  42821  3rexfrabdioph  42954  4rexfrabdioph  42955  6rexfrabdioph  42956  7rexfrabdioph  42957  irrapxlem5  42983  pellexlem2  42987  pellexlem6  42991  pell14qrgt0  43016  pell1qrge1  43027  pellfundgt1  43040  ltrmxnn0  43106  jm2.26lem3  43158  jm2.27a  43162  jm2.27c  43164  rmxdiophlem  43172  jm3.1lem1  43174  jm3.1lem2  43175  jm3.1lem3  43176  jm3.1  43177  dgrsub2  43292  mpaaeu  43307  idomsubgmo  43350  relexpxpmin  43874  nzprmdif  44476  binomcxplemwb  44505  fperiodmul  45468  xralrple4  45533  fsumnncl  45734  dvsinexp  46071  dvxpaek  46100  itgsinexplem1  46114  stoweidlem1  46161  stoweidlem17  46177  stoweidlem25  46185  stoweidlem34  46194  stoweidlem38  46198  stoweidlem40  46200  stoweidlem42  46202  stoweidlem45  46205  stirlinglem4  46237  stirlinglem5  46238  stirlinglem10  46243  stirlinglem13  46246  dirkertrigeq  46261  fourierdlem21  46288  fourierdlem25  46292  fourierdlem48  46314  fourierdlem54  46320  fourierdlem64  46330  fourierdlem65  46331  fourierdlem73  46339  fourierdlem81  46347  fourierdlem83  46349  fourierdlem92  46358  fourierdlem103  46369  fourierdlem104  46370  fourierdlem112  46378  fourierdlem113  46379  etransclem1  46395  etransclem4  46398  etransclem8  46402  etransclem15  46409  etransclem17  46411  etransclem18  46412  etransclem19  46413  etransclem20  46414  etransclem21  46415  etransclem22  46416  etransclem23  46417  etransclem24  46418  etransclem25  46419  etransclem27  46421  etransclem32  46426  etransclem35  46429  etransclem41  46435  etransclem44  46438  etransclem46  46440  modmknepk  47524  iccpartigtl  47585  iccpartgt  47589  iccpartgel  47591  iccelpart  47595  odz2prm2pw  47725  fmtnoprmfac1  47727  fmtnoprmfac2  47729  2pwp1prm  47751  sfprmdvdsmersenne  47765  lighneallem4a  47770  proththdlem  47775  proththd  47776  perfectALTVlem1  47883  perfectALTVlem2  47884  perfectALTV  47885  fpprwpprb  47902  gpgedgvtx1  48224  logbpw2m1  48729  nnpw2blenfzo  48743  nnolog2flm1  48752  dignn0fr  48763  nn0sumshdiglemA  48781  nn0sumshdiglemB  48782