Theorem nnnn0d 12489

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℕcn 12165  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900  df-n0 12429

This theorem is referenced by:  nn0ge2m1nn0  12499  nnzd  12541  eluzge2nn0  12833  expgt1  14053  expaddzlem  14058  expaddz  14059  expmulz  14061  expmulnbnd  14188  exp11nnd  14214  facwordi  14242  faclbnd  14243  facavg  14254  bcm1k  14268  wrdeqs1cat  14673  cshwcsh2id  14781  relexpsucnnr  14978  isercolllem2  15619  bcxmas  15791  climcndslem1  15805  climcndslem2  15806  climcnds  15807  pwdif  15824  geo2sum  15829  mertenslem1  15840  prodmolem3  15889  prodmolem2a  15890  bpolydiflem  16010  eftabs  16031  efcllem  16033  eftlub  16067  eirrlem  16162  rpnnen2lem9  16180  rpnnen2lem11  16182  dvdsfac  16286  pwp1fsum  16351  oddpwp1fsum  16352  bitsfzo  16395  bitsfi  16397  sadcaddlem  16417  smumullem  16452  gcdcl  16466  dvdsgcdidd  16497  mulgcd  16508  rplpwr  16518  rprpwr  16519  rppwr  16520  nn0rppwr  16521  expgcd  16523  lcmcl  16561  lcmgcdnn  16571  lcmfcl  16588  nprmdvds1  16667  rpexp  16683  prmdvdsbc  16687  zsqrtelqelz  16719  phiprmpw  16737  eulerthlem2  16743  eulerth  16744  fermltl  16745  odzcllem  16754  odzdvds  16757  odzphi  16758  prm23lt5  16776  pythagtriplem6  16783  pythagtriplem7  16784  pcprmpw2  16844  dvdsprmpweqle  16848  pcprod  16857  pcfac  16861  pcbc  16862  expnprm  16864  pockthlem  16867  pockthg  16868  prmunb  16876  prmreclem2  16879  prmreclem3  16880  prmreclem4  16881  prmreclem5  16882  prmreclem6  16883  mul4sqlem  16915  4sqlem11  16917  4sqlem17  16923  vdwlem1  16943  vdwlem5  16947  vdwlem6  16948  vdwlem8  16950  vdwlem9  16951  vdwlem11  16953  vdwlem12  16954  vdwnnlem3  16959  ramz2  16986  ramub1lem1  16988  ramub1lem2  16989  ramub1  16990  prmgaplem3  17015  2expltfac  17054  psgnunilem3  19462  odfval  19498  mndodconglem  19507  gexcl3  19553  pgpfi1  19561  sylow1lem1  19564  gexexlem  19818  prmcyg  19860  gsumval3  19873  ablfacrplem  20033  ablfacrp  20034  ablfacrp2  20035  ablfac1eu  20041  prmgrpsimpgd  20082  srgbinomlem3  20200  srgbinomlem4  20201  fermltlchr  21504  freshmansdream  21549  chfacfscmulgsum  22843  chfacfpmmulgsum  22847  cpmadugsumlemF  22859  ovoliunlem1  25487  mbfi1fseqlem1  25700  mbfi1fseqlem3  25702  mbfi1fseqlem5  25704  itg2cnlem2  25747  dvply1  26268  aalioulem2  26317  aalioulem5  26320  aaliou3lem1  26326  aaliou3lem2  26327  aaliou3lem8  26329  aaliou3lem6  26332  taylthlem1  26356  taylthlem2  26357  pserdvlem2  26411  cxpeq  26739  zrtelqelz  26740  dmgmdivn0  27009  lgamgulmlem5  27014  lgamcvg2  27036  wilthlem1  27049  ftalem1  27054  ftalem2  27055  ftalem4  27057  ftalem5  27058  basellem2  27063  basellem3  27064  basellem4  27065  basellem5  27066  isppw2  27096  mpodvdsmulf1o  27175  dvdsmulf1o  27177  sgmmul  27182  fsumvma2  27195  chpchtsum  27200  logfacubnd  27202  mersenne  27208  perfect1  27209  perfectlem1  27210  perfectlem2  27211  perfect  27212  dchrelbas3  27219  dchrelbasd  27220  dchrzrh1  27225  dchrzrhmul  27227  dchrmulcl  27230  dchrn0  27231  dchrfi  27236  dchrghm  27237  dchrabs  27241  dchrinv  27242  dchrptlem1  27245  dchrptlem2  27246  dchrptlem3  27247  dchrpt  27248  dchrsum2  27249  sum2dchr  27255  pcbcctr  27257  bcmono  27258  bclbnd  27261  bposlem1  27265  bposlem3  27267  bposlem5  27269  bposlem6  27270  lgslem1  27278  lgsval2lem  27288  lgsvalmod  27297  lgsmod  27304  lgsdirprm  27312  lgsne0  27316  lgsqrlem1  27327  lgsqrlem2  27328  lgsqrlem3  27329  lgsqrlem4  27330  gausslemma2dlem0b  27338  gausslemma2dlem0c  27339  gausslemma2dlem1  27347  gausslemma2dlem7  27354  gausslemma2d  27355  lgseisenlem1  27356  lgseisenlem2  27357  lgseisenlem3  27358  lgseisenlem4  27359  lgseisen  27360  lgsquadlem2  27362  lgsquadlem3  27363  m1lgs  27369  2lgslem1a  27372  2sqlem3  27401  2sqblem  27412  chebbnd1lem1  27450  chebbnd1lem3  27452  rplogsumlem2  27466  rpvmasumlem  27468  dchrisumlem1  27470  dchrisumlem2  27471  dchrmusum2  27475  dchrvmasumlem3  27480  dchrisum0ff  27488  dchrisum0flblem1  27489  rpvmasum2  27493  dchrisum0re  27494  dchrisum0lem2a  27498  dirith  27510  mudivsum  27511  pntpbnd1a  27566  pntlemq  27582  pntlemr  27583  pntlemj  27584  ostth2lem1  27599  ostth2lem2  27615  ostth2lem3  27616  ostth2  27618  crctcshwlkn0lem6  29901  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  clwwlknon  30178  eucrctshift  30331  numclwlk1lem2  30458  nrt2irr  30561  dipcl  30801  dipcn  30809  bcm1n  32887  expgt0b  32909  nexple  32936  2exple2exp  32937  oexpled  32939  wrdpmtrlast  33174  psgnfzto1st  33186  isarchi2  33266  submarchi  33267  znfermltl  33449  fldextrspundgdvdslem  33864  fldextrspundgdvds  33865  fldext2rspun  33866  constrext2chnlem  33934  cos9thpiminplylem2  33967  submateqlem1  33991  madjusmdetlem2  34012  madjusmdetlem4  34014  mdetlap  34016  oddpwdc  34538  eulerpartlemsv2  34542  eulerpartlemsf  34543  eulerpartlems  34544  eulerpartlemv  34548  eulerpartlemb  34552  plymulx0  34731  signsvtn0  34754  fsum2dsub  34791  reprinfz1  34806  reprpmtf1o  34810  circlemeth  34824  circlemethnat  34825  hgt750lemb  34840  hgt750lema  34841  hgt750leme  34842  tgoldbachgtde  34844  tgoldbachgtda  34845  lpadleft  34867  subfacp1lem1  35407  subfacp1lem6  35413  subfaclim  35416  erdszelem8  35426  erdszelem10  35428  cvmliftlem10  35522  faclim2  35976  poimirlem7  37994  poimirlem17  38004  poimirlem18  38005  poimirlem20  38007  poimirlem21  38008  poimirlem22  38009  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  poimirlem28  38015  poimirlem32  38019  nninfnub  38118  bfplem1  38189  zndvdchrrhm  42458  lcmineqlem1  42514  lcmineqlem2  42515  lcmineqlem8  42521  lcmineqlem10  42523  lcmineqlem11  42524  lcmineqlem15  42528  lcmineqlem16  42529  lcmineqlem18  42531  lcmineqlem19  42532  lcmineqlem20  42533  lcmineqlem21  42534  lcmineqlem22  42535  3lexlogpow2ineq2  42544  dvrelogpow2b  42553  aks4d1p1p2  42555  aks4d1p1p4  42556  aks4d1p1  42561  aks4d1p3  42563  aks4d1p7d1  42567  aks4d1p7  42568  aks4d1p8  42572  aks4d1p9  42573  isprimroot2  42579  primrootsunit1  42582  primrootscoprmpow  42584  posbezout  42585  primrootscoprbij  42587  primrootlekpowne0  42590  primrootspoweq0  42591  aks6d1c1p2  42594  aks6d1c1p3  42595  aks6d1c1p4  42596  aks6d1c1p5  42597  aks6d1c1p7  42598  aks6d1c1p6  42599  aks6d1c1p8  42600  aks6d1c2p2  42604  hashscontpowcl  42605  hashscontpow1  42606  hashscontpow  42607  aks6d1c4  42609  aks6d1c2lem3  42611  aks6d1c2lem4  42612  aks6d1c2  42615  sticksstones6  42636  sticksstones7  42637  sticksstones10  42640  sticksstones12a  42642  sticksstones12  42643  sticksstones20  42651  sticksstones22  42653  aks6d1c6lem2  42656  aks6d1c6lem3  42657  aks6d1c6lem4  42658  aks6d1c6isolem1  42659  aks6d1c6isolem2  42660  aks6d1c6lem5  42662  bcled  42663  bcle2d  42664  aks6d1c7lem1  42665  aks6d1c7  42669  aks5lem2  42672  aks5lem3a  42674  aks5lem5a  42676  grpods  42679  unitscyglem2  42681  unitscyglem4  42683  aks5lem7  42685  aks5  42689  sumcubes  42790  oexpreposd  42799  exp11d  42803  dvdsexpb  42812  fiabv  43022  fsuppind  43040  dffltz  43084  fltdvdsabdvdsc  43088  fltne  43094  flt4lem4  43099  flt4lem7  43109  fltltc  43111  fltnltalem  43112  fltnlta  43113  3rexfrabdioph  43242  4rexfrabdioph  43243  6rexfrabdioph  43244  7rexfrabdioph  43245  irrapxlem5  43271  pellexlem2  43275  pellexlem6  43279  pell14qrgt0  43304  pell1qrge1  43315  pellfundgt1  43328  ltrmxnn0  43394  jm2.26lem3  43446  jm2.27a  43450  jm2.27c  43452  rmxdiophlem  43460  jm3.1lem1  43462  jm3.1lem2  43463  jm3.1lem3  43464  jm3.1  43465  dgrsub2  43580  mpaaeu  43595  idomsubgmo  43638  relexpxpmin  44161  nzprmdif  44763  binomcxplemwb  44792  fperiodmul  45752  xralrple4  45817  fsumnncl  46017  dvsinexp  46354  dvxpaek  46383  itgsinexplem1  46397  stoweidlem1  46444  stoweidlem17  46460  stoweidlem25  46468  stoweidlem34  46477  stoweidlem38  46481  stoweidlem40  46483  stoweidlem42  46485  stoweidlem45  46488  stirlinglem4  46520  stirlinglem5  46521  stirlinglem10  46526  stirlinglem13  46529  dirkertrigeq  46544  fourierdlem21  46571  fourierdlem25  46575  fourierdlem48  46597  fourierdlem54  46603  fourierdlem64  46613  fourierdlem65  46614  fourierdlem73  46622  fourierdlem81  46630  fourierdlem83  46632  fourierdlem92  46641  fourierdlem103  46652  fourierdlem104  46653  fourierdlem112  46661  fourierdlem113  46662  etransclem1  46678  etransclem4  46681  etransclem8  46685  etransclem15  46692  etransclem17  46694  etransclem18  46695  etransclem19  46696  etransclem20  46697  etransclem21  46698  etransclem22  46699  etransclem23  46700  etransclem24  46701  etransclem25  46702  etransclem27  46704  etransclem32  46709  etransclem35  46712  etransclem41  46718  etransclem44  46721  etransclem46  46723  modmknepk  47831  iccpartigtl  47898  iccpartgt  47902  iccpartgel  47904  iccelpart  47908  odz2prm2pw  48041  fmtnoprmfac1  48043  fmtnoprmfac2  48045  2pwp1prm  48067  sfprmdvdsmersenne  48081  lighneallem4a  48086  proththdlem  48091  proththd  48092  perfectALTVlem1  48212  perfectALTVlem2  48213  perfectALTV  48214  fpprwpprb  48231  gpgedgvtx1  48553  logbpw2m1  49058  nnpw2blenfzo  49072  nnolog2flm1  49081  dignn0fr  49092  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111