Theorem nnnn0d 12560

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕcn 12238  ℕ₀cn0 12499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-n0 12500

This theorem is referenced by:  nn0ge2m1nn0  12570  nnzd  12613  eluzge2nn0  12901  expgt1  14116  expaddzlem  14121  expaddz  14122  expmulz  14124  expmulnbnd  14251  exp11nnd  14277  facwordi  14305  faclbnd  14306  facavg  14317  bcm1k  14331  wrdeqs1cat  14736  cshwcsh2id  14845  relexpsucnnr  15042  isercolllem2  15680  bcxmas  15849  climcndslem1  15863  climcndslem2  15864  climcnds  15865  pwdif  15882  geo2sum  15887  mertenslem1  15898  prodmolem3  15947  prodmolem2a  15948  bpolydiflem  16068  eftabs  16089  efcllem  16091  eftlub  16125  eirrlem  16220  rpnnen2lem9  16238  rpnnen2lem11  16240  dvdsfac  16343  pwp1fsum  16408  oddpwp1fsum  16409  bitsfzo  16452  bitsfi  16454  sadcaddlem  16474  smumullem  16509  gcdcl  16523  dvdsgcdidd  16554  mulgcd  16565  rplpwr  16575  rprpwr  16576  rppwr  16577  nn0rppwr  16578  expgcd  16580  lcmcl  16618  lcmgcdnn  16628  lcmfcl  16645  nprmdvds1  16723  rpexp  16739  prmdvdsbc  16743  zsqrtelqelz  16775  phiprmpw  16793  eulerthlem2  16799  eulerth  16800  fermltl  16801  odzcllem  16810  odzdvds  16813  odzphi  16814  prm23lt5  16832  pythagtriplem6  16839  pythagtriplem7  16840  pcprmpw2  16900  dvdsprmpweqle  16904  pcprod  16913  pcfac  16917  pcbc  16918  expnprm  16920  pockthlem  16923  pockthg  16924  prmunb  16932  prmreclem2  16935  prmreclem3  16936  prmreclem4  16937  prmreclem5  16938  prmreclem6  16939  mul4sqlem  16971  4sqlem11  16973  4sqlem17  16979  vdwlem1  16999  vdwlem5  17003  vdwlem6  17004  vdwlem8  17006  vdwlem9  17007  vdwlem11  17009  vdwlem12  17010  vdwnnlem3  17015  ramz2  17042  ramub1lem1  17044  ramub1lem2  17045  ramub1  17046  prmgaplem3  17071  2expltfac  17110  psgnunilem3  19475  odfval  19511  mndodconglem  19520  gexcl3  19566  pgpfi1  19574  sylow1lem1  19577  gexexlem  19831  prmcyg  19873  gsumval3  19886  ablfacrplem  20046  ablfacrp  20047  ablfacrp2  20048  ablfac1eu  20054  prmgrpsimpgd  20095  srgbinomlem3  20186  srgbinomlem4  20187  fermltlchr  21488  freshmansdream  21533  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  cpmadugsumlemF  22812  ovoliunlem1  25453  mbfi1fseqlem1  25666  mbfi1fseqlem3  25668  mbfi1fseqlem5  25670  itg2cnlem2  25713  dvply1  26241  aalioulem2  26291  aalioulem5  26294  aaliou3lem1  26300  aaliou3lem2  26301  aaliou3lem8  26303  aaliou3lem6  26306  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  pserdvlem2  26388  cxpeq  26717  zrtelqelz  26718  dmgmdivn0  26988  lgamgulmlem5  26993  lgamcvg2  27015  wilthlem1  27028  ftalem1  27033  ftalem2  27034  ftalem4  27036  ftalem5  27037  basellem2  27042  basellem3  27043  basellem4  27044  basellem5  27045  isppw2  27075  mpodvdsmulf1o  27154  dvdsmulf1o  27156  sgmmul  27162  fsumvma2  27175  chpchtsum  27180  logfacubnd  27182  mersenne  27188  perfect1  27189  perfectlem1  27190  perfectlem2  27191  perfect  27192  dchrelbas3  27199  dchrelbasd  27200  dchrzrh1  27205  dchrzrhmul  27207  dchrmulcl  27210  dchrn0  27211  dchrfi  27216  dchrghm  27217  dchrabs  27221  dchrinv  27222  dchrptlem1  27225  dchrptlem2  27226  dchrptlem3  27227  dchrpt  27228  dchrsum2  27229  sum2dchr  27235  pcbcctr  27237  bcmono  27238  bclbnd  27241  bposlem1  27245  bposlem3  27247  bposlem5  27249  bposlem6  27250  lgslem1  27258  lgsval2lem  27268  lgsvalmod  27277  lgsmod  27284  lgsdirprm  27292  lgsne0  27296  lgsqrlem1  27307  lgsqrlem2  27308  lgsqrlem3  27309  lgsqrlem4  27310  gausslemma2dlem0b  27318  gausslemma2dlem0c  27319  gausslemma2dlem1  27327  gausslemma2dlem7  27334  gausslemma2d  27335  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem3  27338  lgseisenlem4  27339  lgseisen  27340  lgsquadlem2  27342  lgsquadlem3  27343  m1lgs  27349  2lgslem1a  27352  2sqlem3  27381  2sqblem  27392  chebbnd1lem1  27430  chebbnd1lem3  27432  rplogsumlem2  27446  rpvmasumlem  27448  dchrisumlem1  27450  dchrisumlem2  27451  dchrmusum2  27455  dchrvmasumlem3  27460  dchrisum0ff  27468  dchrisum0flblem1  27469  rpvmasum2  27473  dchrisum0re  27474  dchrisum0lem2a  27478  dirith  27490  mudivsum  27491  pntpbnd1a  27546  pntlemq  27562  pntlemr  27563  pntlemj  27564  ostth2lem1  27579  ostth2lem2  27595  ostth2lem3  27596  ostth2  27598  crctcshwlkn0lem6  29743  hashecclwwlkn1  30004  umgrhashecclwwlk  30005  clwwlknon  30017  eucrctshift  30170  numclwlk1lem2  30297  nrt2irr  30400  dipcl  30639  dipcn  30647  bcm1n  32718  expgt0b  32741  nexple  32769  2exple2exp  32770  oexpled  32772  wrdpmtrlast  33050  psgnfzto1st  33062  isarchi2  33129  submarchi  33130  znfermltl  33327  fldextrspundgdvdslem  33667  fldextrspundgdvds  33668  fldext2rspun  33669  constrext2chnlem  33730  cos9thpiminplylem2  33763  submateqlem1  33784  madjusmdetlem2  33805  madjusmdetlem4  33807  mdetlap  33809  oddpwdc  34332  eulerpartlemsv2  34336  eulerpartlemsf  34337  eulerpartlems  34338  eulerpartlemv  34342  eulerpartlemb  34346  plymulx0  34525  signsvtn0  34548  fsum2dsub  34585  reprinfz1  34600  reprpmtf1o  34604  circlemeth  34618  circlemethnat  34619  hgt750lemb  34634  hgt750lema  34635  hgt750leme  34636  tgoldbachgtde  34638  tgoldbachgtda  34639  lpadleft  34661  subfacp1lem1  35147  subfacp1lem6  35153  subfaclim  35156  erdszelem8  35166  erdszelem10  35168  cvmliftlem10  35262  faclim2  35711  poimirlem7  37597  poimirlem17  37607  poimirlem18  37608  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem28  37618  poimirlem32  37622  nninfnub  37721  bfplem1  37792  zndvdchrrhm  41931  lcmineqlem1  41988  lcmineqlem2  41989  lcmineqlem8  41995  lcmineqlem10  41997  lcmineqlem11  41998  lcmineqlem15  42002  lcmineqlem16  42003  lcmineqlem18  42005  lcmineqlem19  42006  lcmineqlem20  42007  lcmineqlem21  42008  lcmineqlem22  42009  3lexlogpow2ineq2  42018  dvrelogpow2b  42027  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1  42035  aks4d1p3  42037  aks4d1p7d1  42041  aks4d1p7  42042  aks4d1p8  42046  aks4d1p9  42047  isprimroot2  42053  primrootsunit1  42056  primrootscoprmpow  42058  posbezout  42059  primrootscoprbij  42061  primrootlekpowne0  42064  primrootspoweq0  42065  aks6d1c1p2  42068  aks6d1c1p3  42069  aks6d1c1p4  42070  aks6d1c1p5  42071  aks6d1c1p7  42072  aks6d1c1p6  42073  aks6d1c1p8  42074  aks6d1c2p2  42078  hashscontpowcl  42079  hashscontpow1  42080  hashscontpow  42081  aks6d1c4  42083  aks6d1c2lem3  42085  aks6d1c2lem4  42086  aks6d1c2  42089  sticksstones6  42110  sticksstones7  42111  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  sticksstones20  42125  sticksstones22  42127  aks6d1c6lem2  42130  aks6d1c6lem3  42131  aks6d1c6lem4  42132  aks6d1c6isolem1  42133  aks6d1c6isolem2  42134  aks6d1c6lem5  42136  bcled  42137  bcle2d  42138  aks6d1c7lem1  42139  aks6d1c7  42143  aks5lem2  42146  aks5lem3a  42148  aks5lem5a  42150  grpods  42153  unitscyglem2  42155  unitscyglem4  42157  aks5lem7  42159  aks5  42163  metakunt2  42165  sumcubes  42309  oexpreposd  42318  exp11d  42322  dvdsexpb  42331  fiabv  42506  fsuppind  42560  dffltz  42604  fltdvdsabdvdsc  42608  fltne  42614  flt4lem4  42619  flt4lem7  42629  fltltc  42631  fltnltalem  42632  fltnlta  42633  3rexfrabdioph  42767  4rexfrabdioph  42768  6rexfrabdioph  42769  7rexfrabdioph  42770  irrapxlem5  42796  pellexlem2  42800  pellexlem6  42804  pell14qrgt0  42829  pell1qrge1  42840  pellfundgt1  42853  ltrmxnn0  42920  jm2.26lem3  42972  jm2.27a  42976  jm2.27c  42978  rmxdiophlem  42986  jm3.1lem1  42988  jm3.1lem2  42989  jm3.1lem3  42990  jm3.1  42991  dgrsub2  43106  mpaaeu  43121  idomsubgmo  43164  relexpxpmin  43688  nzprmdif  44291  binomcxplemwb  44320  fperiodmul  45281  xralrple4  45348  fsumnncl  45549  dvsinexp  45888  dvxpaek  45917  itgsinexplem1  45931  stoweidlem1  45978  stoweidlem17  45994  stoweidlem25  46002  stoweidlem34  46011  stoweidlem38  46015  stoweidlem40  46017  stoweidlem42  46019  stoweidlem45  46022  stirlinglem4  46054  stirlinglem5  46055  stirlinglem10  46060  stirlinglem13  46063  dirkertrigeq  46078  fourierdlem21  46105  fourierdlem25  46109  fourierdlem48  46131  fourierdlem54  46137  fourierdlem64  46147  fourierdlem65  46148  fourierdlem73  46156  fourierdlem81  46164  fourierdlem83  46166  fourierdlem92  46175  fourierdlem103  46186  fourierdlem104  46187  fourierdlem112  46195  fourierdlem113  46196  etransclem1  46212  etransclem4  46215  etransclem8  46219  etransclem15  46226  etransclem17  46228  etransclem18  46229  etransclem19  46230  etransclem20  46231  etransclem21  46232  etransclem22  46233  etransclem23  46234  etransclem24  46235  etransclem25  46236  etransclem27  46238  etransclem32  46243  etransclem35  46246  etransclem41  46252  etransclem44  46255  etransclem46  46257  iccpartigtl  47385  iccpartgt  47389  iccpartgel  47391  iccelpart  47395  odz2prm2pw  47525  fmtnoprmfac1  47527  fmtnoprmfac2  47529  2pwp1prm  47551  sfprmdvdsmersenne  47565  lighneallem4a  47570  proththdlem  47575  proththd  47576  perfectALTVlem1  47683  perfectALTVlem2  47684  perfectALTV  47685  fpprwpprb  47702  gpgedgvtx1  48014  gpg3nbgrvtxlem  48017  logbpw2m1  48495  nnpw2blenfzo  48509  nnolog2flm1  48518  dignn0fr  48529  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548