Theorem nn0zd 12725

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 12723	. 2 ⊢ ℕ0 ⊆ ℤ
2		nn0zd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3907	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℕ₀cn0 12613  ℤcz 12700

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391  ax-un 7755  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-i2m1 11275  ax-1ne0 11276  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7427  df-om 7882  df-2nd 8006  df-frecs 8306  df-wrecs 8337  df-recs 8386  df-rdg 8425  df-neg 11551  df-nn 12343  df-n0 12614  df-z 12701

This theorem is used by:  nnzd  12726  eluzmn  12979  difelfznle  13783  elfzodif0  13912  zmodfz  14040  expnegz  14246  expaddzlem  14255  expaddz  14256  expmulz  14258  faclbnd  14441  bcpasc  14472  hashf1  14609  fz1isolem  14613  hashge2el2dif  14632  hashtpg  14637  wrdffz  14687  ffz0iswrd  14693  wrdsymb0  14701  wrdlenge1n0  14702  ccatcl  14726  ccatval3  14731  ccatdmss  14734  ccatsymb  14735  ccatval21sw  14738  ccatass  14741  ccatrn  14742  ccatf1  14743  lswccatn0lsw  14745  ccats1val2  14783  swrdnd  14812  swrdccat2  14827  pfxtrcfv0  14851  pfxtrcfvl  14854  pfxccat1  14859  swrdccatin2  14886  pfxccatin12  14890  pfxccatpfx2  14894  pfxccat3a  14895  splfv2a  14913  splval2  14914  revcl  14918  revccat  14923  revrev  14924  revpfxsfxrev  14925  cshwmodn  14954  cshwsublen  14955  cshwn  14956  cshwidxmod  14962  2cshwid  14973  3cshw  14977  cshweqdif2  14978  revco  14993  ccatco  14994  ccat2s1fvwALT  15117  ofccat  15131  zabscl  15489  absrdbnd  15518  iseraltlem3  15860  fsum0diaglem  15951  modfsummods  15969  binomlem  16007  binom1p  16009  incexc2  16016  climcndslem1  16027  geoser  16045  pwm1geoser  16047  geolim2  16049  mertenslem1  16062  mertenslem2  16063  mertens  16064  binomfallfaclem2  16215  binomrisefac  16217  fallfacval4  16218  bpolydiflem  16229  ruclem10  16416  sumodd  16567  divalglem9  16580  divalgmod  16585  bitsfzolem  16613  bitsfzo  16614  bitsmod  16615  bitsfi  16616  bitsinv1lem  16620  sadcaddlem  16636  sadadd3  16640  sadaddlem  16645  sadadd  16646  sadasslem  16649  sadass  16650  sadeq  16651  bitsres  16652  bitsuz  16653  bitsshft  16654  smuval2  16661  smupvallem  16662  smupval  16667  smueqlem  16669  smumullem  16671  smumul  16672  gcdcllem1  16678  gcdle1d  16689  gcdle2d  16690  zeqzmulgcd  16691  gcd0id  16700  gcdneg  16703  modgcd  16714  gcdmultipled  16716  bezoutlem4  16724  dvdsgcdb  16727  gcdass  16729  mulgcd  16730  gcdzeq  16734  dvdsmulgcd  16739  bezoutr  16752  bezoutr1  16753  nn0seqcvgd  16754  algfx  16764  eucalginv  16768  eucalg  16771  gcddvdslcm  16786  lcmneg  16787  lcmgcdlem  16790  lcmdvds  16792  lcmgcdeq  16796  lcmdvdsb  16797  lcmass  16798  lcmftp  16820  lcmfunsnlem1  16821  lcmfunsnlem2lem1  16822  lcmfunsnlem2lem2  16823  lcmfunsnlem2  16824  lcmfdvdsb  16827  lcmfun  16829  lcmfass  16830  mulgcddvds  16839  rpmulgcd2  16840  qredeu  16842  divgcdcoprm0  16849  sqnprm  16887  prmdvdsbc  16911  divnumden  16933  powm2modprm  16990  coprimeprodsq  16995  iserodd  17022  pclem  17025  pcpre1  17029  pcpremul  17030  pcqcl  17043  pcdvdsb  17056  pcidlem  17059  pc2dvds  17066  pcprmpw2  17069  dvdsprmpweqle  17073  pcadd  17076  pcfac  17086  pcbc  17087  pockthlem  17092  prmreclem2  17104  prmreclem3  17105  mul4sqlem  17140  4sqlem11  17142  4sqlem12  17143  4sqlem14  17145  vdwapun  17161  prmgaplcmlem1  17238  chnind  18804  chnub  18805  chnpolfz  18816  lagsubg  19419  psgnuni  19722  psgnran  19738  odmodnn0  19763  mndodconglem  19764  mndodcong  19765  odm1inv  19776  odmulg2  19778  odmulg  19779  odmulgeq  19780  odbezout  19781  odinv  19784  odf1  19785  gexod  19809  gexdvds3  19813  sylow1lem1  19821  sylow1lem3  19823  pgpfi  19828  pgpssslw  19837  sylow2alem2  19841  sylow2blem3  19845  fislw  19848  sylow3lem4  19853  sylow3lem6  19855  efginvrel2  19950  efgredlemf  19964  efgredlemd  19967  efgredlemc  19968  efgredlem  19970  efgcpbllemb  19978  odadd1  20071  odadd2  20072  gexexlem  20075  gexex  20076  torsubg  20077  lt6abl  20118  gsummulg  20165  ablfacrplem  20290  ablfacrp  20291  ablfacrp2  20292  ablfac1b  20295  ablfac1c  20296  ablfac1eulem  20297  ablfac1eu  20298  pgpfac1lem2  20300  pgpfaclem1  20306  ablfaclem3  20312  srgbinomlem3  20463  srgbinomlem4  20464  chrid  21840  znunit  21878  freshmansdream  21889  psgnghm  21895  asclmulg  22219  psrbaglefi  22243  psdvsca  22494  psdmul  22496  chfacfscmulfsupp  23186  chfacfpmmulfsupp  23190  cpmadugsumlemF  23203  dyadss  25924  dyaddisjlem  25925  ply1divex  26464  ply1termlem  26530  plyeq0lem  26538  plyaddlem1  26541  plymullem1  26542  coeeulem  26552  coeidlem  26565  coeeq2  26570  coemulhi  26582  dvply1  26614  dvply2g  26615  plydivex  26627  elqaalem2  26652  aareccl  26662  aannenlem1  26664  aalioulem1  26668  taylplem1  26699  taylplem2  26700  taylpfval  26701  dvtaylp  26706  taylthlem2  26710  dvradcnv  26757  abelthlem7  26774  cxpeq  27094  birthdaylem2  27289  ftalem1  27409  basellem3  27419  isppw2  27451  isnsqf  27471  mule1  27484  ppinncl  27510  musum  27527  chtublem  27547  pclogsum  27551  vmasum  27552  dchrabs  27596  bcmax  27614  bposlem1  27620  bposlem6  27625  lgsval2lem  27643  lgsmod  27659  lgsne0  27671  gausslemma2dlem0h  27699  gausslemma2dlem0i  27700  gausslemma2dlem2  27703  gausslemma2dlem6  27708  gausslemma2d  27710  lgseisenlem1  27711  lgseisenlem2  27712  lgseisenlem3  27713  lgseisenlem4  27714  lgsquadlem1  27716  m1lgs  27724  2lgslem1a  27727  2lgslem3a  27732  2lgslem3b  27733  2lgslem3c  27734  2lgslem3d  27735  2lgslem3d1  27739  2lgsoddprmlem2  27745  2sqlem8  27762  2sqcoprm  27771  2sqmod  27772  chebbnd1lem1  27805  dchrisumlem1  27825  dchrisum0flblem1  27844  selberg2lem  27886  ostth2lem2  27970  ostth2lem3  27971  fltdiv  27977  flt4lem4  27988  finsumvtxdg2sstep  30139  finsumvtxdgeven  30142  vtxdgoddnumeven  30143  redwlklem  30259  wlkdlem1  30270  revwlk  30276  pthdlem1  30361  crctcshwlkn0lem4  30411  wwlksnredwwlkn0  30494  wwlksnextproplem2  30508  clwwlkccatlem  30589  clwlkclwwlkfo  30609  clwwlkwwlksb  30654  clwwlkndivn  30680  eupth2lem3lem3  30840  eupth2lem3lem4  30841  eupth2lem3  30846  eupth2lems  30848  numclwwlk5  30998  numclwwlk6  31000  ex-ind-dvds  31071  nndiffz1  33428  fzo0opth  33445  pfxlsw2ccat  33563  wrdt2ind  33566  gsummulsubdishift1  33679  gsumwrd2dccatlem  33688  cycpmfv1  33724  cycpmco2lem2  33738  cycpmco2lem3  33739  cycpmco2lem4  33740  cycpmco2lem5  33741  cycpmco2lem6  33742  cycpmco2  33744  cycpmrn  33754  cyc3genpm  33763  cycpmconjslem2  33766  cyc3conja  33768  archirng  33799  archirngz  33800  archiabllem1a  33802  gsumind  33956  elrspunidl  34028  ply1coedeg  34171  ply1degltel  34176  gsummoncoe1fz  34180  selvply1rhmlemb  34201  esplyfval2  34247  esplympl  34249  esplyfval3  34254  esplyindfv  34258  vietalem  34261  ply1degltdimlem  34304  fldextrspundgdvds  34363  algextdeglem8  34406  rtelextdg2  34409  constrext2chnlem  34432  cos9thpiminplylem2  34465  cos9thpiminplylem3  34466  cos9thpiminplylem6  34469  cos9thpiminply  34470  madjusmdetlem4  34512  zrhcntr  34661  qqhval2lem  34663  oddpwdc  35036  eulerpartlems  35042  eulerpartlemb  35050  sseqfv1  35071  sseqfn  35072  sseqmw  35073  sseqf  35074  sseqfv2  35076  sseqp1  35077  ccatmulgnn0dir  35224  signsplypnf  35229  signsply0  35230  signslema  35241  signstfvn  35248  signstfvp  35250  signstfvc  35253  fsum2dsub  35286  reprinfz1  35301  reprfi2  35302  hashrepr  35304  reprdifc  35306  breprexplema  35309  breprexplemc  35311  circlemeth  35319  circlevma  35321  circlemethhgt  35322  hgt750lema  35336  tgoldbachgtde  35339  lpadlem3  35360  subfacval3  36044  bcprod  36599  bccolsum  36600  fwddifnp1  37026  knoppndvlem6  37479  knoppndvlem7  37480  knoppndvlem10  37483  knoppndvlem14  37487  knoppndvlem15  37488  knoppndvlem16  37489  knoppndvlem17  37490  knoppndvlem19  37492  knoppndvlem21  37494  dfgcd3  38354  poimirlem3  38650  poimirlem4  38651  poimirlem6  38653  poimirlem13  38660  poimirlem14  38661  poimirlem17  38664  poimirlem21  38668  poimirlem22  38669  poimirlem23  38670  poimirlem26  38673  poimirlem27  38674  poimirlem31  38678  geomcau  38802  bccl2d  43150  lcmineqlem12  43199  lcmineqlem17  43204  dvrelogpow2b  43227  aks4d1p1p2  43229  aks4d1p1p4  43230  aks4d1p1p6  43232  aks4d1p1p7  43233  aks4d1p1p5  43234  aks4d1p1  43235  aks4d1p3  43237  aks4d1p6  43240  aks4d1p8d2  43244  aks4d1p8d3  43245  aks4d1p8  43246  primrootscoprmpow  43258  primrootlekpowne0  43264  aks6d1c1  43275  aks6d1c2p2  43278  aks6d1c2lem4  43286  aks6d1c2  43289  aks6d1c5lem3  43296  aks6d1c5lem2  43297  2np3bcnp1  43303  sticksstones5  43309  sticksstones6  43310  sticksstones7  43311  sticksstones10  43314  sticksstones11  43315  sticksstones12a  43316  sticksstones12  43317  sticksstones22  43327  aks6d1c6lem3  43331  bcled  43337  bcle2d  43338  aks6d1c7lem1  43339  aks6d1c7lem2  43340  grpods  43353  unitscyglem2  43355  unitscyglem4  43357  aks5lem8  43360  sumcubes  43479  frlmvscadiccat  43682  fltnltalem  43782  eldioph2lem1  43880  pellexlem5  43949  congrep  44089  jm2.18  44104  jm2.19lem1  44105  jm2.19lem2  44106  jm2.19  44109  jm2.22  44111  jm2.23  44112  jm2.20nn  44113  jm2.25  44115  jm2.26a  44116  jm2.26lem3  44117  jm2.26  44118  jm2.27a  44121  jm2.27b  44122  jm2.27c  44123  jm3.1  44136  expdiophlem1  44137  hbtlem5  44239  radcnvrat  45407  nzin  45411  bccbc  45438  binomcxplemnn0  45442  binomcxplemnotnn0  45449  fprodexp  46714  mccllem  46717  ioodvbdlimc1lem2  47050  ioodvbdlimc2lem  47052  dvnxpaek  47060  dvnmul  47061  dvnprodlem1  47064  dvnprodlem2  47065  wallispilem1  47183  wallispilem5  47187  stirlinglem3  47194  stirlinglem5  47196  stirlinglem7  47198  stirlinglem8  47199  fourierdlem102  47326  fourierdlem114  47338  sqwvfoura  47346  elaa2lem  47351  etransclem10  47362  etransclem20  47372  etransclem21  47373  etransclem22  47374  etransclem23  47375  etransclem24  47376  etransclem27  47379  etransclem28  47380  etransclem35  47387  etransclem38  47390  etransclem44  47396  etransclem45  47397  etransclem46  47398  sge0ad2en  47549  chnsubseqwl  47997  chnsubseq  47998  sqrtnpoly  48051  fsummmodsnunz  48561  fmtnoge3  48723  fmtnof1  48728  fmtnorec1  48730  sqrtpwpw2p  48731  fmtnodvds  48737  goldbachthlem2  48739  fmtnoprmfac2lem1  48759  lighneallem3  48800  lighneallem4b  48802  lighneallem4  48803  ssnn0ssfz  49569  altgsumbcALT  49573  flnn0ohalf  49754  dig2nn1st  49825  0dig2nn0o  49833  aacllem  51122