Theorem nn0zd 12413

Description: A positive 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 12330	. 2 ⊢ ℕ0 ⊆ ℤ
2		nn0zd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3920	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2106  ℕ₀cn0 12222  ℤcz 12308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7580  ax-1cn 10918  ax-icn 10919  ax-addcl 10920  ax-addrcl 10921  ax-mulcl 10922  ax-mulrcl 10923  ax-i2m1 10928  ax-1ne0 10929  ax-rnegex 10931  ax-rrecex 10932  ax-cnre 10933

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3433  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-iun 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5486  df-eprel 5492  df-po 5500  df-so 5501  df-fr 5541  df-we 5543  df-xp 5592  df-rel 5593  df-cnv 5594  df-co 5595  df-dm 5596  df-rn 5597  df-res 5598  df-ima 5599  df-pred 6197  df-ord 6264  df-on 6265  df-lim 6266  df-suc 6267  df-iota 6386  df-fun 6430  df-fn 6431  df-f 6432  df-f1 6433  df-fo 6434  df-f1o 6435  df-fv 6436  df-ov 7272  df-om 7705  df-2nd 7823  df-frecs 8086  df-wrecs 8117  df-recs 8191  df-rdg 8230  df-neg 11197  df-nn 11963  df-n0 12223  df-z 12309

This theorem is referenced by:  nnzd  12414  eluzmn  12578  difelfznle  13359  zmodfz  13602  expnegz  13806  expaddzlem  13815  expaddz  13816  expmulz  13818  faclbnd  13993  bcpasc  14024  hashf1  14160  fz1isolem  14164  hashge2el2dif  14183  hashtpg  14188  wrdffz  14227  ffz0iswrd  14233  wrdsymb0  14241  wrdlenge1n0  14242  ccatcl  14266  ccatval3  14273  ccatsymb  14276  ccatval21sw  14279  ccatass  14282  ccatrn  14283  lswccatn0lsw  14285  ccats1val2  14323  swrdnd  14356  swrdccat2  14371  pfxtrcfv0  14396  pfxtrcfvl  14399  pfxccat1  14404  swrdccatin2  14431  pfxccatin12  14435  pfxccatpfx2  14439  pfxccat3a  14440  splfv2a  14458  splval2  14459  revcl  14463  revccat  14468  revrev  14469  cshwmodn  14497  cshwsublen  14498  cshwn  14499  cshwidxmod  14505  2cshwid  14516  3cshw  14520  cshweqdif2  14521  revco  14536  ccatco  14537  ccat2s1fvwALT  14658  ccat2s1fvwALTOLD  14659  ofccat  14669  zabscl  15014  absrdbnd  15042  iseraltlem3  15384  fsum0diaglem  15477  modfsummods  15494  binomlem  15530  binom1p  15532  incexc2  15539  climcndslem1  15550  geoser  15568  pwm1geoser  15570  geolim2  15572  mertenslem1  15585  mertenslem2  15586  mertens  15587  binomfallfaclem2  15739  binomrisefac  15741  fallfacval4  15742  bpolydiflem  15753  ruclem10  15937  sumodd  16086  divalglem9  16099  divalgmod  16104  bitsfzolem  16130  bitsfzo  16131  bitsmod  16132  bitsfi  16133  bitsinv1lem  16137  sadcaddlem  16153  sadadd3  16157  sadaddlem  16162  sadadd  16163  sadasslem  16166  sadass  16167  sadeq  16168  bitsres  16169  bitsuz  16170  bitsshft  16171  smuval2  16178  smupvallem  16179  smupval  16184  smueqlem  16186  smumullem  16188  smumul  16189  gcdcllem1  16195  zeqzmulgcd  16206  gcd0id  16215  gcdneg  16218  modgcd  16229  gcdmultipled  16231  bezoutlem4  16239  dvdsgcdb  16242  gcdass  16244  mulgcd  16245  gcdzeq  16251  dvdsmulgcd  16254  bezoutr  16262  bezoutr1  16263  nn0seqcvgd  16264  algfx  16274  eucalginv  16278  eucalg  16281  gcddvdslcm  16296  lcmneg  16297  lcmgcdlem  16300  lcmdvds  16302  lcmgcdeq  16306  lcmdvdsb  16307  lcmass  16308  lcmftp  16330  lcmfunsnlem1  16331  lcmfunsnlem2lem1  16332  lcmfunsnlem2lem2  16333  lcmfunsnlem2  16334  lcmfdvdsb  16337  lcmfun  16339  lcmfass  16340  mulgcddvds  16349  rpmulgcd2  16350  qredeu  16352  divgcdcoprm0  16359  sqnprm  16396  divnumden  16441  powm2modprm  16493  coprimeprodsq  16498  iserodd  16525  pclem  16528  pcpre1  16532  pcpremul  16533  pcqcl  16546  pcdvdsb  16559  pcidlem  16562  pc2dvds  16569  pcprmpw2  16572  dvdsprmpweqle  16576  pcadd  16579  pcfac  16589  pcbc  16590  pockthlem  16595  prmreclem2  16607  prmreclem3  16608  mul4sqlem  16643  4sqlem11  16645  4sqlem12  16646  4sqlem14  16648  vdwapun  16664  prmgaplcmlem1  16741  lagsubg  18807  psgnuni  19096  psgnran  19112  odmodnn0  19137  mndodconglem  19138  mndodcong  19139  odmulg2  19151  odmulg  19152  odmulgeq  19153  odbezout  19154  odinv  19157  odf1  19158  gexod  19180  gexdvds3  19184  sylow1lem1  19192  sylow1lem3  19194  pgpfi  19199  pgpssslw  19208  sylow2alem2  19212  sylow2blem3  19216  fislw  19219  sylow3lem4  19224  sylow3lem6  19226  efginvrel2  19322  efgredlemf  19336  efgredlemd  19339  efgredlemc  19340  efgredlem  19342  efgcpbllemb  19350  odadd1  19438  odadd2  19439  gexexlem  19442  gexex  19443  torsubg  19444  lt6abl  19485  gsummulg  19532  ablfacrplem  19657  ablfacrp  19658  ablfacrp2  19659  ablfac1b  19662  ablfac1c  19663  ablfac1eulem  19664  ablfac1eu  19665  pgpfac1lem2  19667  pgpfaclem1  19673  ablfaclem3  19679  srgbinomlem3  19767  srgbinomlem4  19768  chrid  20720  znunit  20760  psgnghm  20774  psrbaglefi  21124  psrbaglefiOLD  21125  chfacfscmulfsupp  21997  chfacfpmmulfsupp  22001  cpmadugsumlemF  22014  dyadss  24747  dyaddisjlem  24748  ply1divex  25290  ply1termlem  25353  plyeq0lem  25360  plyaddlem1  25363  plymullem1  25364  coeeulem  25374  coeidlem  25387  coeeq2  25392  coemulhi  25404  dvply1  25433  dvply2g  25434  plydivex  25446  elqaalem2  25469  aareccl  25475  aannenlem1  25477  aalioulem1  25481  taylplem1  25511  taylplem2  25512  taylpfval  25513  dvtaylp  25518  taylthlem2  25522  dvradcnv  25569  abelthlem7  25586  cxpeq  25899  birthdaylem2  26091  ftalem1  26211  basellem3  26221  isppw2  26253  isnsqf  26273  mule1  26286  ppinncl  26312  musum  26329  chtublem  26348  pclogsum  26352  vmasum  26353  dchrabs  26397  bcmax  26415  bposlem1  26421  bposlem6  26426  lgsval2lem  26444  lgsmod  26460  lgsne0  26472  gausslemma2dlem0h  26500  gausslemma2dlem0i  26501  gausslemma2dlem2  26504  gausslemma2dlem6  26509  gausslemma2d  26511  lgseisenlem1  26512  lgseisenlem2  26513  lgseisenlem3  26514  lgseisenlem4  26515  lgsquadlem1  26517  m1lgs  26525  2lgslem1a  26528  2lgslem3a  26533  2lgslem3b  26534  2lgslem3c  26535  2lgslem3d  26536  2lgslem3d1  26540  2lgsoddprmlem2  26546  2sqlem8  26563  2sqcoprm  26572  2sqmod  26573  chebbnd1lem1  26606  dchrisumlem1  26626  dchrisum0flblem1  26645  selberg2lem  26687  ostth2lem2  26771  ostth2lem3  26772  finsumvtxdg2sstep  27905  finsumvtxdgeven  27908  vtxdgoddnumeven  27909  redwlklem  28027  wlkdlem1  28038  pthdlem1  28121  crctcshwlkn0lem4  28165  wwlksnredwwlkn0  28248  wwlksnextproplem2  28262  clwwlkccatlem  28340  clwlkclwwlkfo  28360  clwwlkwwlksb  28405  clwwlkndivn  28431  eupth2lem3lem3  28581  eupth2lem3lem4  28582  eupth2lem3  28587  eupth2lems  28589  numclwwlk5  28739  numclwwlk6  28741  ex-ind-dvds  28812  nndiffz1  31094  prmdvdsbc  31117  ccatf1  31210  pfxlsw2ccat  31211  wrdt2ind  31212  cycpmfv1  31367  cycpmco2lem2  31381  cycpmco2lem3  31382  cycpmco2lem4  31383  cycpmco2lem5  31384  cycpmco2lem6  31385  cycpmco2  31387  cycpmrn  31397  cyc3genpm  31406  cycpmconjslem2  31409  cyc3conja  31411  archirng  31429  archirngz  31430  archiabllem1a  31432  freshmansdream  31471  elrspunidl  31593  asclmulg  31653  madjusmdetlem4  31767  qqhval2lem  31918  oddpwdc  32308  eulerpartlems  32314  eulerpartlemb  32322  sseqfv1  32343  sseqfn  32344  sseqmw  32345  sseqf  32346  sseqfv2  32348  sseqp1  32349  ccatmulgnn0dir  32508  signsplypnf  32516  signsply0  32517  signslema  32528  signstfvn  32535  signstfvp  32537  signstfvc  32540  fsum2dsub  32574  reprinfz1  32589  reprfi2  32590  hashrepr  32592  reprdifc  32594  breprexplema  32597  breprexplemc  32599  circlemeth  32607  circlevma  32609  circlemethhgt  32610  hgt750lema  32624  tgoldbachgtde  32627  lpadlem3  32645  revpfxsfxrev  33064  revwlk  33073  subfacval3  33138  bcprod  33691  bccolsum  33692  fwddifnp1  34454  knoppndvlem6  34684  knoppndvlem7  34685  knoppndvlem10  34688  knoppndvlem14  34692  knoppndvlem15  34693  knoppndvlem16  34694  knoppndvlem17  34695  knoppndvlem19  34697  knoppndvlem21  34699  dfgcd3  35482  poimirlem3  35767  poimirlem4  35768  poimirlem6  35770  poimirlem13  35777  poimirlem14  35778  poimirlem17  35781  poimirlem21  35785  poimirlem22  35786  poimirlem23  35787  poimirlem26  35790  poimirlem27  35791  poimirlem31  35795  geomcau  35904  bccl2d  39987  lcmineqlem12  40035  lcmineqlem17  40040  dvrelogpow2b  40063  aks4d1p1p2  40065  aks4d1p1p4  40066  aks4d1p1p6  40068  aks4d1p1p7  40069  aks4d1p1p5  40070  aks4d1p1  40071  aks4d1p3  40073  aks4d1p6  40076  aks4d1p8d2  40080  aks4d1p8d3  40081  aks4d1p8  40082  2np3bcnp1  40087  sticksstones5  40093  sticksstones6  40094  sticksstones7  40095  sticksstones10  40098  sticksstones11  40099  sticksstones12a  40100  sticksstones12  40101  sticksstones22  40111  prodsplit  40148  frlmvscadiccat  40224  gcdle1d  40317  gcdle2d  40318  fltdiv  40460  flt4lem4  40473  fltnltalem  40486  eldioph2lem1  40569  pellexlem5  40642  congrep  40782  jm2.18  40797  jm2.19lem1  40798  jm2.19lem2  40799  jm2.19  40802  jm2.22  40804  jm2.23  40805  jm2.20nn  40806  jm2.25  40808  jm2.26a  40809  jm2.26lem3  40810  jm2.26  40811  jm2.27a  40814  jm2.27b  40815  jm2.27c  40816  jm3.1  40829  expdiophlem1  40830  hbtlem5  40940  radcnvrat  41892  nzin  41896  bccbc  41923  binomcxplemnn0  41927  binomcxplemnotnn0  41934  fprodexp  43095  mccllem  43098  ioodvbdlimc1lem2  43433  ioodvbdlimc2lem  43435  dvnxpaek  43443  dvnmul  43444  dvnprodlem1  43447  dvnprodlem2  43448  wallispilem1  43566  wallispilem5  43570  stirlinglem3  43577  stirlinglem5  43579  stirlinglem7  43581  stirlinglem8  43582  fourierdlem102  43709  fourierdlem114  43721  sqwvfoura  43729  elaa2lem  43734  etransclem10  43745  etransclem20  43755  etransclem21  43756  etransclem22  43757  etransclem23  43758  etransclem24  43759  etransclem27  43762  etransclem28  43763  etransclem35  43770  etransclem38  43773  etransclem44  43779  etransclem45  43780  etransclem46  43781  sge0ad2en  43929  fsummmodsnunz  44784  fmtnoge3  44939  fmtnof1  44944  fmtnorec1  44946  sqrtpwpw2p  44947  fmtnodvds  44953  goldbachthlem2  44955  fmtnoprmfac2lem1  44975  lighneallem3  45016  lighneallem4b  45018  lighneallem4  45019  ssnn0ssfz  45642  altgsumbcALT  45646  flnn0ohalf  45837  dig2nn1st  45908  0dig2nn0o  45916  aacllem  46462