Theorem nn0zd 12086

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕ₀cn0 11898  ℤcz 11982

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-i2m1 10605  ax-1ne0 10606  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-neg 10873  df-nn 11639  df-n0 11899  df-z 11983

This theorem is referenced by:  nnzd  12087  eluzmn  12251  difelfznle  13022  zmodfz  13262  expnegz  13464  expaddzlem  13473  expaddz  13474  expmulz  13476  faclbnd  13651  bcpasc  13682  hashf1  13816  fz1isolem  13820  hashge2el2dif  13839  hashtpg  13844  wrdffz  13885  ffz0iswrd  13891  wrdsymb0  13901  wrdlenge1n0  13902  ccatcl  13926  ccatval3  13933  ccatsymb  13936  ccatval21sw  13939  ccatass  13942  ccatrn  13943  lswccatn0lsw  13945  ccats1val2  13983  swrdnd  14016  swrdccat2  14031  pfxtrcfv0  14056  pfxtrcfvl  14059  pfxccat1  14064  swrdccatin2  14091  pfxccatin12  14095  pfxccatpfx2  14099  pfxccat3a  14100  splfv2a  14118  splval2  14119  revcl  14123  revccat  14128  revrev  14129  cshwmodn  14157  cshwsublen  14158  cshwn  14159  cshwidxmod  14165  2cshwid  14176  3cshw  14180  cshweqdif2  14181  revco  14196  ccatco  14197  ccat2s1fvwALT  14318  ccat2s1fvwALTOLD  14319  ofccat  14329  zabscl  14673  absrdbnd  14701  iseraltlem3  15040  fsum0diaglem  15131  modfsummods  15148  binomlem  15184  binom1p  15186  incexc2  15193  climcndslem1  15204  geoser  15222  pwm1geoser  15224  pwm1geoserOLD  15225  geolim2  15227  mertenslem1  15240  mertenslem2  15241  mertens  15242  binomfallfaclem2  15394  binomrisefac  15396  fallfacval4  15397  bpolydiflem  15408  ruclem10  15592  sumodd  15739  divalglem9  15752  divalgmod  15757  bitsfzolem  15783  bitsfzo  15784  bitsmod  15785  bitsfi  15786  bitsinv1lem  15790  sadcaddlem  15806  sadadd3  15810  sadaddlem  15815  sadadd  15816  sadasslem  15819  sadass  15820  sadeq  15821  bitsres  15822  bitsuz  15823  bitsshft  15824  smuval2  15831  smupvallem  15832  smupval  15837  smueqlem  15839  smumullem  15841  smumul  15842  gcdcllem1  15848  zeqzmulgcd  15859  gcd0id  15867  gcdneg  15870  modgcd  15880  gcdmultipled  15882  bezoutlem4  15890  dvdsgcdb  15893  gcdass  15895  mulgcd  15896  gcdzeq  15902  dvdsmulgcd  15905  bezoutr  15912  bezoutr1  15913  nn0seqcvgd  15914  algfx  15924  eucalginv  15928  eucalg  15931  gcddvdslcm  15946  lcmneg  15947  lcmgcdlem  15950  lcmdvds  15952  lcmgcdeq  15956  lcmdvdsb  15957  lcmass  15958  lcmftp  15980  lcmfunsnlem1  15981  lcmfunsnlem2lem1  15982  lcmfunsnlem2lem2  15983  lcmfunsnlem2  15984  lcmfdvdsb  15987  lcmfun  15989  lcmfass  15990  mulgcddvds  15999  rpmulgcd2  16000  qredeu  16002  divgcdcoprm0  16009  sqnprm  16046  divnumden  16088  powm2modprm  16140  coprimeprodsq  16145  iserodd  16172  pclem  16175  pcpre1  16179  pcpremul  16180  pcqcl  16193  pcdvdsb  16205  pcidlem  16208  pc2dvds  16215  pcprmpw2  16218  dvdsprmpweqle  16222  pcadd  16225  pcfac  16235  pcbc  16236  pockthlem  16241  prmreclem2  16253  prmreclem3  16254  mul4sqlem  16289  4sqlem11  16291  4sqlem12  16292  4sqlem14  16294  vdwapun  16310  prmgaplcmlem1  16387  lagsubg  18342  psgnuni  18627  psgnran  18643  odmodnn0  18668  mndodconglem  18669  mndodcong  18670  odmulg2  18682  odmulg  18683  odmulgeq  18684  odbezout  18685  odinv  18688  odf1  18689  gexod  18711  gexdvds3  18715  sylow1lem1  18723  sylow1lem3  18725  pgpfi  18730  pgpssslw  18739  sylow2alem2  18743  sylow2blem3  18747  fislw  18750  sylow3lem4  18755  sylow3lem6  18757  efginvrel2  18853  efgredlemf  18867  efgredlemd  18870  efgredlemc  18871  efgredlem  18873  efgcpbllemb  18881  odadd1  18968  odadd2  18969  gexexlem  18972  gexex  18973  torsubg  18974  lt6abl  19015  gsummulg  19062  ablfacrplem  19187  ablfacrp  19188  ablfacrp2  19189  ablfac1b  19192  ablfac1c  19193  ablfac1eulem  19194  ablfac1eu  19195  pgpfac1lem2  19197  pgpfaclem1  19203  ablfaclem3  19209  srgbinomlem3  19292  srgbinomlem4  19293  psrbaglefi  20152  chrid  20674  znunit  20710  psgnghm  20724  chfacfscmulfsupp  21467  chfacfpmmulfsupp  21471  cpmadugsumlemF  21484  dyadss  24195  dyaddisjlem  24196  ply1divex  24730  ply1termlem  24793  plyeq0lem  24800  plyaddlem1  24803  plymullem1  24804  coeeulem  24814  coeidlem  24827  coeeq2  24832  coemulhi  24844  dvply1  24873  dvply2g  24874  plydivex  24886  elqaalem2  24909  aareccl  24915  aannenlem1  24917  aalioulem1  24921  taylplem1  24951  taylplem2  24952  taylpfval  24953  dvtaylp  24958  taylthlem2  24962  dvradcnv  25009  abelthlem7  25026  cxpeq  25338  birthdaylem2  25530  ftalem1  25650  basellem3  25660  isppw2  25692  isnsqf  25712  mule1  25725  ppinncl  25751  musum  25768  chtublem  25787  pclogsum  25791  vmasum  25792  dchrabs  25836  bcmax  25854  bposlem1  25860  bposlem6  25865  lgsval2lem  25883  lgsmod  25899  lgsne0  25911  gausslemma2dlem0h  25939  gausslemma2dlem0i  25940  gausslemma2dlem2  25943  gausslemma2dlem6  25948  gausslemma2d  25950  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgseisenlem4  25954  lgsquadlem1  25956  m1lgs  25964  2lgslem1a  25967  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2lgslem3d1  25979  2lgsoddprmlem2  25985  2sqlem8  26002  2sqcoprm  26011  2sqmod  26012  chebbnd1lem1  26045  dchrisumlem1  26065  dchrisum0flblem1  26084  selberg2lem  26126  ostth2lem2  26210  ostth2lem3  26211  finsumvtxdg2sstep  27331  finsumvtxdgeven  27334  vtxdgoddnumeven  27335  redwlklem  27453  wlkdlem1  27464  pthdlem1  27547  crctcshwlkn0lem4  27591  wwlksnredwwlkn0  27674  wwlksnextproplem2  27689  clwwlkccatlem  27767  clwlkclwwlkfo  27787  clwwlkwwlksb  27833  clwwlkndivn  27859  eupth2lem3lem3  28009  eupth2lem3lem4  28010  eupth2lem3  28015  eupth2lems  28017  numclwwlk5  28167  numclwwlk6  28169  ex-ind-dvds  28240  nndiffz1  30509  prmdvdsbc  30532  ccatf1  30625  pfxlsw2ccat  30626  wrdt2ind  30627  cycpmfv1  30755  cycpmco2lem2  30769  cycpmco2lem3  30770  cycpmco2lem4  30771  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2lem7  30774  cycpmco2  30775  cycpmrn  30785  cyc3genpm  30794  cycpmconjslem2  30797  cyc3conja  30799  archirng  30817  archirngz  30818  archiabllem1a  30820  freshmansdream  30859  madjusmdetlem4  31095  qqhval2lem  31222  oddpwdc  31612  eulerpartlems  31618  eulerpartlemb  31626  sseqfv1  31647  sseqfn  31648  sseqmw  31649  sseqf  31650  sseqfv2  31652  sseqp1  31653  ccatmulgnn0dir  31812  signsplypnf  31820  signsply0  31821  signslema  31832  signstfvn  31839  signstfvp  31841  signstfvc  31844  fsum2dsub  31878  reprinfz1  31893  reprfi2  31894  hashrepr  31896  reprdifc  31898  breprexplema  31901  breprexplemc  31903  circlemeth  31911  circlevma  31913  circlemethhgt  31914  hgt750lema  31928  tgoldbachgtde  31931  lpadlem3  31949  revpfxsfxrev  32362  revwlk  32371  subfacval3  32436  bcprod  32970  bccolsum  32971  fwddifnp1  33626  knoppndvlem6  33856  knoppndvlem7  33857  knoppndvlem10  33860  knoppndvlem14  33864  knoppndvlem15  33865  knoppndvlem16  33866  knoppndvlem17  33867  knoppndvlem19  33869  knoppndvlem21  33871  dfgcd3  34608  poimirlem3  34910  poimirlem4  34911  poimirlem6  34913  poimirlem13  34920  poimirlem14  34921  poimirlem17  34924  poimirlem21  34928  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  poimirlem26  34933  poimirlem27  34934  poimirlem31  34938  geomcau  35049  prodsplit  39145  frlmvscadiccat  39194  fltnltalem  39323  eldioph2lem1  39406  pellexlem5  39479  congrep  39619  jm2.18  39634  jm2.19lem1  39635  jm2.19lem2  39636  jm2.19  39639  jm2.22  39641  jm2.23  39642  jm2.20nn  39643  jm2.25  39645  jm2.26a  39646  jm2.26lem3  39647  jm2.26  39648  jm2.27a  39651  jm2.27b  39652  jm2.27c  39653  jm3.1  39666  expdiophlem1  39667  hbtlem5  39777  radcnvrat  40695  nzin  40699  bccbc  40726  binomcxplemnn0  40730  binomcxplemnotnn0  40737  fprodexp  41924  mccllem  41927  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnxpaek  42276  dvnmul  42277  dvnprodlem1  42280  dvnprodlem2  42281  wallispilem1  42399  wallispilem5  42403  stirlinglem3  42410  stirlinglem5  42412  stirlinglem7  42414  stirlinglem8  42415  fourierdlem102  42542  fourierdlem114  42554  sqwvfoura  42562  elaa2lem  42567  etransclem10  42578  etransclem20  42588  etransclem21  42589  etransclem22  42590  etransclem23  42591  etransclem24  42592  etransclem27  42595  etransclem28  42596  etransclem35  42603  etransclem38  42606  etransclem44  42612  etransclem45  42613  etransclem46  42614  sge0ad2en  42762  fsummmodsnunz  43584  fmtnoge3  43741  fmtnof1  43746  fmtnorec1  43748  sqrtpwpw2p  43749  fmtnodvds  43755  goldbachthlem2  43757  fmtnoprmfac2lem1  43777  lighneallem3  43821  lighneallem4b  43823  lighneallem4  43824  ssnn0ssfz  44446  altgsumbcALT  44450  flnn0ohalf  44643  dig2nn1st  44714  0dig2nn0o  44722  aacllem  44951