Theorem nn0zd 12470

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

Syntax hints:   → wi 4   ∈ wcel 2104  ℕ₀cn0 12279  ℤcz 12365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620  ax-1cn 10975  ax-icn 10976  ax-addcl 10977  ax-addrcl 10978  ax-mulcl 10979  ax-mulrcl 10980  ax-i2m1 10985  ax-1ne0 10986  ax-rnegex 10988  ax-rrecex 10989  ax-cnre 10990

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-ov 7310  df-om 7745  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-neg 11254  df-nn 12020  df-n0 12280  df-z 12366

This theorem is referenced by:  nnzd  12471  eluzmn  12635  difelfznle  13416  zmodfz  13659  expnegz  13863  expaddzlem  13872  expaddz  13873  expmulz  13875  faclbnd  14050  bcpasc  14081  hashf1  14216  fz1isolem  14220  hashge2el2dif  14239  hashtpg  14244  wrdffz  14283  ffz0iswrd  14289  wrdsymb0  14297  wrdlenge1n0  14298  ccatcl  14322  ccatval3  14329  ccatsymb  14332  ccatval21sw  14335  ccatass  14338  ccatrn  14339  lswccatn0lsw  14341  ccats1val2  14379  swrdnd  14412  swrdccat2  14427  pfxtrcfv0  14452  pfxtrcfvl  14455  pfxccat1  14460  swrdccatin2  14487  pfxccatin12  14491  pfxccatpfx2  14495  pfxccat3a  14496  splfv2a  14514  splval2  14515  revcl  14519  revccat  14524  revrev  14525  cshwmodn  14553  cshwsublen  14554  cshwn  14555  cshwidxmod  14561  2cshwid  14572  3cshw  14576  cshweqdif2  14577  revco  14592  ccatco  14593  ccat2s1fvwALT  14714  ccat2s1fvwALTOLD  14715  ofccat  14725  zabscl  15070  absrdbnd  15098  iseraltlem3  15440  fsum0diaglem  15533  modfsummods  15550  binomlem  15586  binom1p  15588  incexc2  15595  climcndslem1  15606  geoser  15624  pwm1geoser  15626  geolim2  15628  mertenslem1  15641  mertenslem2  15642  mertens  15643  binomfallfaclem2  15795  binomrisefac  15797  fallfacval4  15798  bpolydiflem  15809  ruclem10  15993  sumodd  16142  divalglem9  16155  divalgmod  16160  bitsfzolem  16186  bitsfzo  16187  bitsmod  16188  bitsfi  16189  bitsinv1lem  16193  sadcaddlem  16209  sadadd3  16213  sadaddlem  16218  sadadd  16219  sadasslem  16222  sadass  16223  sadeq  16224  bitsres  16225  bitsuz  16226  bitsshft  16227  smuval2  16234  smupvallem  16235  smupval  16240  smueqlem  16242  smumullem  16244  smumul  16245  gcdcllem1  16251  zeqzmulgcd  16262  gcd0id  16271  gcdneg  16274  modgcd  16285  gcdmultipled  16287  bezoutlem4  16295  dvdsgcdb  16298  gcdass  16300  mulgcd  16301  gcdzeq  16307  dvdsmulgcd  16310  bezoutr  16318  bezoutr1  16319  nn0seqcvgd  16320  algfx  16330  eucalginv  16334  eucalg  16337  gcddvdslcm  16352  lcmneg  16353  lcmgcdlem  16356  lcmdvds  16358  lcmgcdeq  16362  lcmdvdsb  16363  lcmass  16364  lcmftp  16386  lcmfunsnlem1  16387  lcmfunsnlem2lem1  16388  lcmfunsnlem2lem2  16389  lcmfunsnlem2  16390  lcmfdvdsb  16393  lcmfun  16395  lcmfass  16396  mulgcddvds  16405  rpmulgcd2  16406  qredeu  16408  divgcdcoprm0  16415  sqnprm  16452  divnumden  16497  powm2modprm  16549  coprimeprodsq  16554  iserodd  16581  pclem  16584  pcpre1  16588  pcpremul  16589  pcqcl  16602  pcdvdsb  16615  pcidlem  16618  pc2dvds  16625  pcprmpw2  16628  dvdsprmpweqle  16632  pcadd  16635  pcfac  16645  pcbc  16646  pockthlem  16651  prmreclem2  16663  prmreclem3  16664  mul4sqlem  16699  4sqlem11  16701  4sqlem12  16702  4sqlem14  16704  vdwapun  16720  prmgaplcmlem1  16797  lagsubg  18863  psgnuni  19152  psgnran  19168  odmodnn0  19193  mndodconglem  19194  mndodcong  19195  odmulg2  19207  odmulg  19208  odmulgeq  19209  odbezout  19210  odinv  19213  odf1  19214  gexod  19236  gexdvds3  19240  sylow1lem1  19248  sylow1lem3  19250  pgpfi  19255  pgpssslw  19264  sylow2alem2  19268  sylow2blem3  19272  fislw  19275  sylow3lem4  19280  sylow3lem6  19282  efginvrel2  19378  efgredlemf  19392  efgredlemd  19395  efgredlemc  19396  efgredlem  19398  efgcpbllemb  19406  odadd1  19494  odadd2  19495  gexexlem  19498  gexex  19499  torsubg  19500  lt6abl  19541  gsummulg  19588  ablfacrplem  19713  ablfacrp  19714  ablfacrp2  19715  ablfac1b  19718  ablfac1c  19719  ablfac1eulem  19720  ablfac1eu  19721  pgpfac1lem2  19723  pgpfaclem1  19729  ablfaclem3  19735  srgbinomlem3  19823  srgbinomlem4  19824  chrid  20776  znunit  20816  psgnghm  20830  psrbaglefi  21180  psrbaglefiOLD  21181  chfacfscmulfsupp  22053  chfacfpmmulfsupp  22057  cpmadugsumlemF  22070  dyadss  24803  dyaddisjlem  24804  ply1divex  25346  ply1termlem  25409  plyeq0lem  25416  plyaddlem1  25419  plymullem1  25420  coeeulem  25430  coeidlem  25443  coeeq2  25448  coemulhi  25460  dvply1  25489  dvply2g  25490  plydivex  25502  elqaalem2  25525  aareccl  25531  aannenlem1  25533  aalioulem1  25537  taylplem1  25567  taylplem2  25568  taylpfval  25569  dvtaylp  25574  taylthlem2  25578  dvradcnv  25625  abelthlem7  25642  cxpeq  25955  birthdaylem2  26147  ftalem1  26267  basellem3  26277  isppw2  26309  isnsqf  26329  mule1  26342  ppinncl  26368  musum  26385  chtublem  26404  pclogsum  26408  vmasum  26409  dchrabs  26453  bcmax  26471  bposlem1  26477  bposlem6  26482  lgsval2lem  26500  lgsmod  26516  lgsne0  26528  gausslemma2dlem0h  26556  gausslemma2dlem0i  26557  gausslemma2dlem2  26560  gausslemma2dlem6  26565  gausslemma2d  26567  lgseisenlem1  26568  lgseisenlem2  26569  lgseisenlem3  26570  lgseisenlem4  26571  lgsquadlem1  26573  m1lgs  26581  2lgslem1a  26584  2lgslem3a  26589  2lgslem3b  26590  2lgslem3c  26591  2lgslem3d  26592  2lgslem3d1  26596  2lgsoddprmlem2  26602  2sqlem8  26619  2sqcoprm  26628  2sqmod  26629  chebbnd1lem1  26662  dchrisumlem1  26682  dchrisum0flblem1  26701  selberg2lem  26743  ostth2lem2  26827  ostth2lem3  26828  finsumvtxdg2sstep  27961  finsumvtxdgeven  27964  vtxdgoddnumeven  27965  redwlklem  28084  wlkdlem1  28095  pthdlem1  28179  crctcshwlkn0lem4  28223  wwlksnredwwlkn0  28306  wwlksnextproplem2  28320  clwwlkccatlem  28398  clwlkclwwlkfo  28418  clwwlkwwlksb  28463  clwwlkndivn  28489  eupth2lem3lem3  28639  eupth2lem3lem4  28640  eupth2lem3  28645  eupth2lems  28647  numclwwlk5  28797  numclwwlk6  28799  ex-ind-dvds  28870  nndiffz1  31152  prmdvdsbc  31175  ccatf1  31268  pfxlsw2ccat  31269  wrdt2ind  31270  cycpmfv1  31425  cycpmco2lem2  31439  cycpmco2lem3  31440  cycpmco2lem4  31441  cycpmco2lem5  31442  cycpmco2lem6  31443  cycpmco2  31445  cycpmrn  31455  cyc3genpm  31464  cycpmconjslem2  31467  cyc3conja  31469  archirng  31487  archirngz  31488  archiabllem1a  31490  freshmansdream  31529  elrspunidl  31651  asclmulg  31711  madjusmdetlem4  31825  qqhval2lem  31976  oddpwdc  32366  eulerpartlems  32372  eulerpartlemb  32380  sseqfv1  32401  sseqfn  32402  sseqmw  32403  sseqf  32404  sseqfv2  32406  sseqp1  32407  ccatmulgnn0dir  32566  signsplypnf  32574  signsply0  32575  signslema  32586  signstfvn  32593  signstfvp  32595  signstfvc  32598  fsum2dsub  32632  reprinfz1  32647  reprfi2  32648  hashrepr  32650  reprdifc  32652  breprexplema  32655  breprexplemc  32657  circlemeth  32665  circlevma  32667  circlemethhgt  32668  hgt750lema  32682  tgoldbachgtde  32685  lpadlem3  32703  revpfxsfxrev  33122  revwlk  33131  subfacval3  33196  bcprod  33749  bccolsum  33750  fwddifnp1  34512  knoppndvlem6  34742  knoppndvlem7  34743  knoppndvlem10  34746  knoppndvlem14  34750  knoppndvlem15  34751  knoppndvlem16  34752  knoppndvlem17  34753  knoppndvlem19  34755  knoppndvlem21  34757  dfgcd3  35539  poimirlem3  35824  poimirlem4  35825  poimirlem6  35827  poimirlem13  35834  poimirlem14  35835  poimirlem17  35838  poimirlem21  35842  poimirlem22  35843  poimirlem23  35844  poimirlem26  35847  poimirlem27  35848  poimirlem31  35852  geomcau  35961  bccl2d  40042  lcmineqlem12  40090  lcmineqlem17  40095  dvrelogpow2b  40118  aks4d1p1p2  40120  aks4d1p1p4  40121  aks4d1p1p6  40123  aks4d1p1p7  40124  aks4d1p1p5  40125  aks4d1p1  40126  aks4d1p3  40128  aks4d1p6  40131  aks4d1p8d2  40135  aks4d1p8d3  40136  aks4d1p8  40137  2np3bcnp1  40142  sticksstones5  40148  sticksstones6  40149  sticksstones7  40150  sticksstones10  40153  sticksstones11  40154  sticksstones12a  40155  sticksstones12  40156  sticksstones22  40166  prodsplit  40203  frlmvscadiccat  40274  gcdle1d  40367  gcdle2d  40368  fltdiv  40510  flt4lem4  40523  fltnltalem  40536  eldioph2lem1  40619  pellexlem5  40692  congrep  40833  jm2.18  40848  jm2.19lem1  40849  jm2.19lem2  40850  jm2.19  40853  jm2.22  40855  jm2.23  40856  jm2.20nn  40857  jm2.25  40859  jm2.26a  40860  jm2.26lem3  40861  jm2.26  40862  jm2.27a  40865  jm2.27b  40866  jm2.27c  40867  jm3.1  40880  expdiophlem1  40881  hbtlem5  40991  radcnvrat  41970  nzin  41974  bccbc  42001  binomcxplemnn0  42005  binomcxplemnotnn0  42012  fprodexp  43184  mccllem  43187  ioodvbdlimc1lem2  43522  ioodvbdlimc2lem  43524  dvnxpaek  43532  dvnmul  43533  dvnprodlem1  43536  dvnprodlem2  43537  wallispilem1  43655  wallispilem5  43659  stirlinglem3  43666  stirlinglem5  43668  stirlinglem7  43670  stirlinglem8  43671  fourierdlem102  43798  fourierdlem114  43810  sqwvfoura  43818  elaa2lem  43823  etransclem10  43834  etransclem20  43844  etransclem21  43845  etransclem22  43846  etransclem23  43847  etransclem24  43848  etransclem27  43851  etransclem28  43852  etransclem35  43859  etransclem38  43862  etransclem44  43868  etransclem45  43869  etransclem46  43870  sge0ad2en  44019  fsummmodsnunz  44885  fmtnoge3  45040  fmtnof1  45045  fmtnorec1  45047  sqrtpwpw2p  45048  fmtnodvds  45054  goldbachthlem2  45056  fmtnoprmfac2lem1  45076  lighneallem3  45117  lighneallem4b  45119  lighneallem4  45120  ssnn0ssfz  45743  altgsumbcALT  45747  flnn0ohalf  45938  dig2nn1st  46009  0dig2nn0o  46017  aacllem  46563