Theorem nn0zd 12665

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕ₀cn0 12553  ℤcz 12639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-neg 11523  df-nn 12294  df-n0 12554  df-z 12640

This theorem is referenced by:  nnzd  12666  eluzmn  12910  difelfznle  13699  zmodfz  13944  expnegz  14147  expaddzlem  14156  expaddz  14157  expmulz  14159  faclbnd  14339  bcpasc  14370  hashf1  14506  fz1isolem  14510  hashge2el2dif  14529  hashtpg  14534  wrdffz  14583  ffz0iswrd  14589  wrdsymb0  14597  wrdlenge1n0  14598  ccatcl  14622  ccatval3  14627  ccatsymb  14630  ccatval21sw  14633  ccatass  14636  ccatrn  14637  lswccatn0lsw  14639  ccats1val2  14675  swrdnd  14702  swrdccat2  14717  pfxtrcfv0  14742  pfxtrcfvl  14745  pfxccat1  14750  swrdccatin2  14777  pfxccatin12  14781  pfxccatpfx2  14785  pfxccat3a  14786  splfv2a  14804  splval2  14805  revcl  14809  revccat  14814  revrev  14815  cshwmodn  14843  cshwsublen  14844  cshwn  14845  cshwidxmod  14851  2cshwid  14862  3cshw  14866  cshweqdif2  14867  revco  14883  ccatco  14884  ccat2s1fvwALT  15004  ofccat  15018  zabscl  15362  absrdbnd  15390  iseraltlem3  15732  fsum0diaglem  15824  modfsummods  15841  binomlem  15877  binom1p  15879  incexc2  15886  climcndslem1  15897  geoser  15915  pwm1geoser  15917  geolim2  15919  mertenslem1  15932  mertenslem2  15933  mertens  15934  binomfallfaclem2  16088  binomrisefac  16090  fallfacval4  16091  bpolydiflem  16102  ruclem10  16287  sumodd  16436  divalglem9  16449  divalgmod  16454  bitsfzolem  16480  bitsfzo  16481  bitsmod  16482  bitsfi  16483  bitsinv1lem  16487  sadcaddlem  16503  sadadd3  16507  sadaddlem  16512  sadadd  16513  sadasslem  16516  sadass  16517  sadeq  16518  bitsres  16519  bitsuz  16520  bitsshft  16521  smuval2  16528  smupvallem  16529  smupval  16534  smueqlem  16536  smumullem  16538  smumul  16539  gcdcllem1  16545  zeqzmulgcd  16556  gcd0id  16565  gcdneg  16568  modgcd  16579  gcdmultipled  16581  bezoutlem4  16589  dvdsgcdb  16592  gcdass  16594  mulgcd  16595  gcdzeq  16599  dvdsmulgcd  16603  bezoutr  16615  bezoutr1  16616  nn0seqcvgd  16617  algfx  16627  eucalginv  16631  eucalg  16634  gcddvdslcm  16649  lcmneg  16650  lcmgcdlem  16653  lcmdvds  16655  lcmgcdeq  16659  lcmdvdsb  16660  lcmass  16661  lcmftp  16683  lcmfunsnlem1  16684  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  lcmfunsnlem2  16687  lcmfdvdsb  16690  lcmfun  16692  lcmfass  16693  mulgcddvds  16702  rpmulgcd2  16703  qredeu  16705  divgcdcoprm0  16712  sqnprm  16749  prmdvdsbc  16773  divnumden  16795  powm2modprm  16850  coprimeprodsq  16855  iserodd  16882  pclem  16885  pcpre1  16889  pcpremul  16890  pcqcl  16903  pcdvdsb  16916  pcidlem  16919  pc2dvds  16926  pcprmpw2  16929  dvdsprmpweqle  16933  pcadd  16936  pcfac  16946  pcbc  16947  pockthlem  16952  prmreclem2  16964  prmreclem3  16965  mul4sqlem  17000  4sqlem11  17002  4sqlem12  17003  4sqlem14  17005  vdwapun  17021  prmgaplcmlem1  17098  lagsubg  19235  psgnuni  19541  psgnran  19557  odmodnn0  19582  mndodconglem  19583  mndodcong  19584  odm1inv  19595  odmulg2  19597  odmulg  19598  odmulgeq  19599  odbezout  19600  odinv  19603  odf1  19604  gexod  19628  gexdvds3  19632  sylow1lem1  19640  sylow1lem3  19642  pgpfi  19647  pgpssslw  19656  sylow2alem2  19660  sylow2blem3  19664  fislw  19667  sylow3lem4  19672  sylow3lem6  19674  efginvrel2  19769  efgredlemf  19783  efgredlemd  19786  efgredlemc  19787  efgredlem  19789  efgcpbllemb  19797  odadd1  19890  odadd2  19891  gexexlem  19894  gexex  19895  torsubg  19896  lt6abl  19937  gsummulg  19984  ablfacrplem  20109  ablfacrp  20110  ablfacrp2  20111  ablfac1b  20114  ablfac1c  20115  ablfac1eulem  20116  ablfac1eu  20117  pgpfac1lem2  20119  pgpfaclem1  20125  ablfaclem3  20131  srgbinomlem3  20255  srgbinomlem4  20256  chrid  21563  znunit  21605  freshmansdream  21616  psgnghm  21621  asclmulg  21945  psrbaglefi  21969  psdvsca  22191  psdmul  22193  chfacfscmulfsupp  22886  chfacfpmmulfsupp  22890  cpmadugsumlemF  22903  dyadss  25648  dyaddisjlem  25649  ply1divex  26196  ply1termlem  26262  plyeq0lem  26269  plyaddlem1  26272  plymullem1  26273  coeeulem  26283  coeidlem  26296  coeeq2  26301  coemulhi  26313  dvply1  26343  dvply2g  26344  dvply2gOLD  26345  plydivex  26357  elqaalem2  26380  aareccl  26386  aannenlem1  26388  aalioulem1  26392  taylplem1  26422  taylplem2  26423  taylpfval  26424  dvtaylp  26430  taylthlem2  26434  taylthlem2OLD  26435  dvradcnv  26482  abelthlem7  26500  cxpeq  26818  birthdaylem2  27013  ftalem1  27134  basellem3  27144  isppw2  27176  isnsqf  27196  mule1  27209  ppinncl  27235  musum  27252  chtublem  27273  pclogsum  27277  vmasum  27278  dchrabs  27322  bcmax  27340  bposlem1  27346  bposlem6  27351  lgsval2lem  27369  lgsmod  27385  lgsne0  27397  gausslemma2dlem0h  27425  gausslemma2dlem0i  27426  gausslemma2dlem2  27429  gausslemma2dlem6  27434  gausslemma2d  27436  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgseisenlem4  27440  lgsquadlem1  27442  m1lgs  27450  2lgslem1a  27453  2lgslem3a  27458  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  2lgslem3d1  27465  2lgsoddprmlem2  27471  2sqlem8  27488  2sqcoprm  27497  2sqmod  27498  chebbnd1lem1  27531  dchrisumlem1  27551  dchrisum0flblem1  27570  selberg2lem  27612  ostth2lem2  27696  ostth2lem3  27697  finsumvtxdg2sstep  29585  finsumvtxdgeven  29588  vtxdgoddnumeven  29589  redwlklem  29707  wlkdlem1  29718  pthdlem1  29802  crctcshwlkn0lem4  29846  wwlksnredwwlkn0  29929  wwlksnextproplem2  29943  clwwlkccatlem  30021  clwlkclwwlkfo  30041  clwwlkwwlksb  30086  clwwlkndivn  30112  eupth2lem3lem3  30262  eupth2lem3lem4  30263  eupth2lem3  30268  eupth2lems  30270  numclwwlk5  30420  numclwwlk6  30422  ex-ind-dvds  30493  nndiffz1  32791  fzo0opth  32810  ccatf1  32915  ccatdmss  32916  pfxlsw2ccat  32917  wrdt2ind  32920  chnind  32983  chnub  32984  cycpmfv1  33106  cycpmco2lem2  33120  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2  33126  cycpmrn  33136  cyc3genpm  33145  cycpmconjslem2  33148  cyc3conja  33150  archirng  33168  archirngz  33169  archiabllem1a  33171  elrspunidl  33421  ply1degltel  33580  ply1degltdimlem  33635  algextdeglem8  33715  rtelextdg2  33718  madjusmdetlem4  33776  qqhval2lem  33927  oddpwdc  34319  eulerpartlems  34325  eulerpartlemb  34333  sseqfv1  34354  sseqfn  34355  sseqmw  34356  sseqf  34357  sseqfv2  34359  sseqp1  34360  ccatmulgnn0dir  34519  signsplypnf  34527  signsply0  34528  signslema  34539  signstfvn  34546  signstfvp  34548  signstfvc  34551  fsum2dsub  34584  reprinfz1  34599  reprfi2  34600  hashrepr  34602  reprdifc  34604  breprexplema  34607  breprexplemc  34609  circlemeth  34617  circlevma  34619  circlemethhgt  34620  hgt750lema  34634  tgoldbachgtde  34637  lpadlem3  34655  revpfxsfxrev  35083  revwlk  35092  subfacval3  35157  bcprod  35700  bccolsum  35701  fwddifnp1  36129  knoppndvlem6  36483  knoppndvlem7  36484  knoppndvlem10  36487  knoppndvlem14  36491  knoppndvlem15  36492  knoppndvlem16  36493  knoppndvlem17  36494  knoppndvlem19  36496  knoppndvlem21  36498  dfgcd3  37290  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem13  37593  poimirlem14  37594  poimirlem17  37597  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem26  37606  poimirlem27  37607  poimirlem31  37611  geomcau  37719  bccl2d  41948  lcmineqlem12  41997  lcmineqlem17  42002  dvrelogpow2b  42025  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  aks4d1p3  42035  aks4d1p6  42038  aks4d1p8d2  42042  aks4d1p8d3  42043  aks4d1p8  42044  primrootscoprmpow  42056  primrootlekpowne0  42062  aks6d1c1  42073  aks6d1c2p2  42076  aks6d1c2lem4  42084  aks6d1c2  42087  aks6d1c5lem3  42094  aks6d1c5lem2  42095  2np3bcnp1  42101  sticksstones5  42107  sticksstones6  42108  sticksstones7  42109  sticksstones10  42112  sticksstones11  42113  sticksstones12a  42114  sticksstones12  42115  sticksstones22  42125  aks6d1c6lem3  42129  bcled  42135  bcle2d  42136  aks6d1c7lem1  42137  aks6d1c7lem2  42138  grpods  42151  unitscyglem2  42153  unitscyglem4  42155  aks5lem8  42158  prodsplit  42197  sumcubes  42301  gcdle1d  42317  gcdle2d  42318  frlmvscadiccat  42461  fltdiv  42591  flt4lem4  42604  fltnltalem  42617  eldioph2lem1  42716  pellexlem5  42789  congrep  42930  jm2.18  42945  jm2.19lem1  42946  jm2.19lem2  42947  jm2.19  42950  jm2.22  42952  jm2.23  42953  jm2.20nn  42954  jm2.25  42956  jm2.26a  42957  jm2.26lem3  42958  jm2.26  42959  jm2.27a  42962  jm2.27b  42963  jm2.27c  42964  jm3.1  42977  expdiophlem1  42978  hbtlem5  43085  radcnvrat  44283  nzin  44287  bccbc  44314  binomcxplemnn0  44318  binomcxplemnotnn0  44325  fprodexp  45515  mccllem  45518  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnxpaek  45863  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  wallispilem1  45986  wallispilem5  45990  stirlinglem3  45997  stirlinglem5  45999  stirlinglem7  46001  stirlinglem8  46002  fourierdlem102  46129  fourierdlem114  46141  sqwvfoura  46149  elaa2lem  46154  etransclem10  46165  etransclem20  46175  etransclem21  46176  etransclem22  46177  etransclem23  46178  etransclem24  46179  etransclem27  46182  etransclem28  46183  etransclem35  46190  etransclem38  46193  etransclem44  46199  etransclem45  46200  etransclem46  46201  sge0ad2en  46352  fsummmodsnunz  47249  fmtnoge3  47404  fmtnof1  47409  fmtnorec1  47411  sqrtpwpw2p  47412  fmtnodvds  47418  goldbachthlem2  47420  fmtnoprmfac2lem1  47440  lighneallem3  47481  lighneallem4b  47483  lighneallem4  47484  ssnn0ssfz  48074  altgsumbcALT  48078  flnn0ohalf  48268  dig2nn1st  48339  0dig2nn0o  48347  aacllem  48895