Theorem nn0zd 12513

Description: A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

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

Assertion

Ref	Expression
nn0zd	⊢ (𝜑 → 𝐴 ∈ ℤ)

Proof of Theorem nn0zd

Step	Hyp	Ref	Expression
1		nn0ssz 12511	. 2 ⊢ ℕ0 ⊆ ℤ
2		nn0zd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3931	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2113  ℕ₀cn0 12401  ℤcz 12488

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-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-neg 11367  df-nn 12146  df-n0 12402  df-z 12489

This theorem is referenced by:  nnzd  12514  eluzmn  12758  difelfznle  13558  elfzodif0  13686  zmodfz  13813  expnegz  14019  expaddzlem  14028  expaddz  14029  expmulz  14031  faclbnd  14213  bcpasc  14244  hashf1  14380  fz1isolem  14384  hashge2el2dif  14403  hashtpg  14408  wrdffz  14458  ffz0iswrd  14464  wrdsymb0  14472  wrdlenge1n0  14473  ccatcl  14497  ccatval3  14502  ccatdmss  14505  ccatsymb  14506  ccatval21sw  14509  ccatass  14512  ccatrn  14513  lswccatn0lsw  14515  ccats1val2  14551  swrdnd  14578  swrdccat2  14593  pfxtrcfv0  14617  pfxtrcfvl  14620  pfxccat1  14625  swrdccatin2  14652  pfxccatin12  14656  pfxccatpfx2  14660  pfxccat3a  14661  splfv2a  14679  splval2  14680  revcl  14684  revccat  14689  revrev  14690  cshwmodn  14718  cshwsublen  14719  cshwn  14720  cshwidxmod  14726  2cshwid  14737  3cshw  14741  cshweqdif2  14742  revco  14757  ccatco  14758  ccat2s1fvwALT  14878  ofccat  14892  zabscl  15236  absrdbnd  15265  iseraltlem3  15607  fsum0diaglem  15699  modfsummods  15716  binomlem  15752  binom1p  15754  incexc2  15761  climcndslem1  15772  geoser  15790  pwm1geoser  15792  geolim2  15794  mertenslem1  15807  mertenslem2  15808  mertens  15809  binomfallfaclem2  15963  binomrisefac  15965  fallfacval4  15966  bpolydiflem  15977  ruclem10  16164  sumodd  16315  divalglem9  16328  divalgmod  16333  bitsfzolem  16361  bitsfzo  16362  bitsmod  16363  bitsfi  16364  bitsinv1lem  16368  sadcaddlem  16384  sadadd3  16388  sadaddlem  16393  sadadd  16394  sadasslem  16397  sadass  16398  sadeq  16399  bitsres  16400  bitsuz  16401  bitsshft  16402  smuval2  16409  smupvallem  16410  smupval  16415  smueqlem  16417  smumullem  16419  smumul  16420  gcdcllem1  16426  zeqzmulgcd  16437  gcd0id  16446  gcdneg  16449  modgcd  16459  gcdmultipled  16461  bezoutlem4  16469  dvdsgcdb  16472  gcdass  16474  mulgcd  16475  gcdzeq  16479  dvdsmulgcd  16483  bezoutr  16495  bezoutr1  16496  nn0seqcvgd  16497  algfx  16507  eucalginv  16511  eucalg  16514  gcddvdslcm  16529  lcmneg  16530  lcmgcdlem  16533  lcmdvds  16535  lcmgcdeq  16539  lcmdvdsb  16540  lcmass  16541  lcmftp  16563  lcmfunsnlem1  16564  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  lcmfunsnlem2  16567  lcmfdvdsb  16570  lcmfun  16572  lcmfass  16573  mulgcddvds  16582  rpmulgcd2  16583  qredeu  16585  divgcdcoprm0  16592  sqnprm  16629  prmdvdsbc  16653  divnumden  16675  powm2modprm  16731  coprimeprodsq  16736  iserodd  16763  pclem  16766  pcpre1  16770  pcpremul  16771  pcqcl  16784  pcdvdsb  16797  pcidlem  16800  pc2dvds  16807  pcprmpw2  16810  dvdsprmpweqle  16814  pcadd  16817  pcfac  16827  pcbc  16828  pockthlem  16833  prmreclem2  16845  prmreclem3  16846  mul4sqlem  16881  4sqlem11  16883  4sqlem12  16884  4sqlem14  16886  vdwapun  16902  prmgaplcmlem1  16979  chnind  18544  chnub  18545  chnpolfz  18556  lagsubg  19124  psgnuni  19428  psgnran  19444  odmodnn0  19469  mndodconglem  19470  mndodcong  19471  odm1inv  19482  odmulg2  19484  odmulg  19485  odmulgeq  19486  odbezout  19487  odinv  19490  odf1  19491  gexod  19515  gexdvds3  19519  sylow1lem1  19527  sylow1lem3  19529  pgpfi  19534  pgpssslw  19543  sylow2alem2  19547  sylow2blem3  19551  fislw  19554  sylow3lem4  19559  sylow3lem6  19561  efginvrel2  19656  efgredlemf  19670  efgredlemd  19673  efgredlemc  19674  efgredlem  19676  efgcpbllemb  19684  odadd1  19777  odadd2  19778  gexexlem  19781  gexex  19782  torsubg  19783  lt6abl  19824  gsummulg  19871  ablfacrplem  19996  ablfacrp  19997  ablfacrp2  19998  ablfac1b  20001  ablfac1c  20002  ablfac1eulem  20003  ablfac1eu  20004  pgpfac1lem2  20006  pgpfaclem1  20012  ablfaclem3  20018  srgbinomlem3  20163  srgbinomlem4  20164  chrid  21480  znunit  21518  freshmansdream  21529  psgnghm  21535  asclmulg  21858  psrbaglefi  21882  psdvsca  22107  psdmul  22109  chfacfscmulfsupp  22803  chfacfpmmulfsupp  22807  cpmadugsumlemF  22820  dyadss  25551  dyaddisjlem  25552  ply1divex  26098  ply1termlem  26164  plyeq0lem  26171  plyaddlem1  26174  plymullem1  26175  coeeulem  26185  coeidlem  26198  coeeq2  26203  coemulhi  26215  dvply1  26247  dvply2g  26248  dvply2gOLD  26249  plydivex  26261  elqaalem2  26284  aareccl  26290  aannenlem1  26292  aalioulem1  26296  taylplem1  26326  taylplem2  26327  taylpfval  26328  dvtaylp  26334  taylthlem2  26338  taylthlem2OLD  26339  dvradcnv  26386  abelthlem7  26404  cxpeq  26723  birthdaylem2  26918  ftalem1  27039  basellem3  27049  isppw2  27081  isnsqf  27101  mule1  27114  ppinncl  27140  musum  27157  chtublem  27178  pclogsum  27182  vmasum  27183  dchrabs  27227  bcmax  27245  bposlem1  27251  bposlem6  27256  lgsval2lem  27274  lgsmod  27290  lgsne0  27302  gausslemma2dlem0h  27330  gausslemma2dlem0i  27331  gausslemma2dlem2  27334  gausslemma2dlem6  27339  gausslemma2d  27341  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgseisenlem4  27345  lgsquadlem1  27347  m1lgs  27355  2lgslem1a  27358  2lgslem3a  27363  2lgslem3b  27364  2lgslem3c  27365  2lgslem3d  27366  2lgslem3d1  27370  2lgsoddprmlem2  27376  2sqlem8  27393  2sqcoprm  27402  2sqmod  27403  chebbnd1lem1  27436  dchrisumlem1  27456  dchrisum0flblem1  27475  selberg2lem  27517  ostth2lem2  27601  ostth2lem3  27602  finsumvtxdg2sstep  29623  finsumvtxdgeven  29626  vtxdgoddnumeven  29627  redwlklem  29743  wlkdlem1  29754  pthdlem1  29839  crctcshwlkn0lem4  29886  wwlksnredwwlkn0  29969  wwlksnextproplem2  29983  clwwlkccatlem  30064  clwlkclwwlkfo  30084  clwwlkwwlksb  30129  clwwlkndivn  30155  eupth2lem3lem3  30305  eupth2lem3lem4  30306  eupth2lem3  30311  eupth2lems  30313  numclwwlk5  30463  numclwwlk6  30465  ex-ind-dvds  30536  nndiffz1  32866  fzo0opth  32883  ccatf1  33031  pfxlsw2ccat  33032  wrdt2ind  33035  gsummulsubdishift1  33151  gsumwrd2dccatlem  33159  cycpmfv1  33195  cycpmco2lem2  33209  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2  33215  cycpmrn  33225  cyc3genpm  33234  cycpmconjslem2  33237  cyc3conja  33239  archirng  33270  archirngz  33271  archiabllem1a  33273  gsumind  33426  elrspunidl  33509  ply1coedeg  33670  ply1degltel  33675  gsummoncoe1fz  33679  esplyfval2  33723  esplympl  33725  esplyfval3  33730  esplyindfv  33732  vietalem  33735  ply1degltdimlem  33779  fldextrspundgdvds  33838  algextdeglem8  33881  rtelextdg2  33884  constrext2chnlem  33907  cos9thpiminplylem2  33940  cos9thpiminplylem3  33941  cos9thpiminplylem6  33944  cos9thpiminply  33945  madjusmdetlem4  33987  zrhcntr  34136  qqhval2lem  34138  oddpwdc  34511  eulerpartlems  34517  eulerpartlemb  34525  sseqfv1  34546  sseqfn  34547  sseqmw  34548  sseqf  34549  sseqfv2  34551  sseqp1  34552  ccatmulgnn0dir  34699  signsplypnf  34707  signsply0  34708  signslema  34719  signstfvn  34726  signstfvp  34728  signstfvc  34731  fsum2dsub  34764  reprinfz1  34779  reprfi2  34780  hashrepr  34782  reprdifc  34784  breprexplema  34787  breprexplemc  34789  circlemeth  34797  circlevma  34799  circlemethhgt  34800  hgt750lema  34814  tgoldbachgtde  34817  lpadlem3  34835  revpfxsfxrev  35310  revwlk  35319  subfacval3  35383  bcprod  35932  bccolsum  35933  fwddifnp1  36359  knoppndvlem6  36717  knoppndvlem7  36718  knoppndvlem10  36721  knoppndvlem14  36725  knoppndvlem15  36726  knoppndvlem16  36727  knoppndvlem17  36728  knoppndvlem19  36730  knoppndvlem21  36732  dfgcd3  37529  poimirlem3  37824  poimirlem4  37825  poimirlem6  37827  poimirlem13  37834  poimirlem14  37835  poimirlem17  37838  poimirlem21  37842  poimirlem22  37843  poimirlem23  37844  poimirlem26  37847  poimirlem27  37848  poimirlem31  37852  geomcau  37960  bccl2d  42245  lcmineqlem12  42294  lcmineqlem17  42299  dvrelogpow2b  42322  aks4d1p1p2  42324  aks4d1p1p4  42325  aks4d1p1p6  42327  aks4d1p1p7  42328  aks4d1p1p5  42329  aks4d1p1  42330  aks4d1p3  42332  aks4d1p6  42335  aks4d1p8d2  42339  aks4d1p8d3  42340  aks4d1p8  42341  primrootscoprmpow  42353  primrootlekpowne0  42359  aks6d1c1  42370  aks6d1c2p2  42373  aks6d1c2lem4  42381  aks6d1c2  42384  aks6d1c5lem3  42391  aks6d1c5lem2  42392  2np3bcnp1  42398  sticksstones5  42404  sticksstones6  42405  sticksstones7  42406  sticksstones10  42409  sticksstones11  42410  sticksstones12a  42411  sticksstones12  42412  sticksstones22  42422  aks6d1c6lem3  42426  bcled  42432  bcle2d  42433  aks6d1c7lem1  42434  aks6d1c7lem2  42435  grpods  42448  unitscyglem2  42450  unitscyglem4  42452  aks5lem8  42455  sumcubes  42568  gcdle1d  42585  gcdle2d  42586  frlmvscadiccat  42761  fltdiv  42879  flt4lem4  42892  fltnltalem  42905  eldioph2lem1  43002  pellexlem5  43075  congrep  43215  jm2.18  43230  jm2.19lem1  43231  jm2.19lem2  43232  jm2.19  43235  jm2.22  43237  jm2.23  43238  jm2.20nn  43239  jm2.25  43241  jm2.26a  43242  jm2.26lem3  43243  jm2.26  43244  jm2.27a  43247  jm2.27b  43248  jm2.27c  43249  jm3.1  43262  expdiophlem1  43263  hbtlem5  43370  radcnvrat  44555  nzin  44559  bccbc  44586  binomcxplemnn0  44590  binomcxplemnotnn0  44597  fprodexp  45840  mccllem  45843  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnxpaek  46186  dvnmul  46187  dvnprodlem1  46190  dvnprodlem2  46191  wallispilem1  46309  wallispilem5  46313  stirlinglem3  46320  stirlinglem5  46322  stirlinglem7  46324  stirlinglem8  46325  fourierdlem102  46452  fourierdlem114  46464  sqwvfoura  46472  elaa2lem  46477  etransclem10  46488  etransclem20  46498  etransclem21  46499  etransclem22  46500  etransclem23  46501  etransclem24  46502  etransclem27  46505  etransclem28  46506  etransclem35  46513  etransclem38  46516  etransclem44  46522  etransclem45  46523  etransclem46  46524  sge0ad2en  46675  chnsubseqwl  47123  chnsubseq  47124  fsummmodsnunz  47621  fmtnoge3  47776  fmtnof1  47781  fmtnorec1  47783  sqrtpwpw2p  47784  fmtnodvds  47790  goldbachthlem2  47792  fmtnoprmfac2lem1  47812  lighneallem3  47853  lighneallem4b  47855  lighneallem4  47856  ssnn0ssfz  48595  altgsumbcALT  48599  flnn0ohalf  48780  dig2nn1st  48851  0dig2nn0o  48859  aacllem  50046