Theorem nnzd 12514

Description: A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
nnzd.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnzd	⊢ (𝜑 → 𝐴 ∈ ℤ)

Proof of Theorem nnzd

Step	Hyp	Ref	Expression
1		nnzd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2	1	nnnn0d 12462	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	2	nn0zd 12513	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2113  ℕcn 12145  ℤcz 12488

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-neg 11367  df-nn 12146  df-n0 12402  df-z 12489

This theorem is referenced by:  expaddzlem  14028  expmulz  14031  expmulnbnd  14158  facndiv  14211  bcval5  14241  bcpasc  14244  hashf1  14380  isercolllem1  15588  isercolllem2  15589  o1fsum  15736  bcxmas  15758  climcndslem2  15773  climcnds  15774  mertenslem1  15807  fprodser  15872  bpolydiflem  15977  eftlub  16034  eirrlem  16129  rpnnen2lem7  16145  rpnnen2lem9  16147  rpnnen2lem11  16149  sqrt2irrlem  16173  dvdsfac  16253  dvdsmod  16256  oddpwp1fsum  16319  bitsfzolem  16361  bitsmod  16363  bitsfi  16364  bitscmp  16365  bitsinv1  16369  sadadd3  16388  sadaddlem  16393  bitsuz  16401  bitsshft  16402  gcdnncl  16434  gcd1  16455  dvdsgcdidd  16464  bezoutlem3  16468  bezoutlem4  16469  mulgcd  16475  rplpwr  16485  rprpwr  16486  sqgcd  16489  expgcd  16490  nn0expgcd  16491  dvdssq  16494  lcmneg  16530  lcmgcdlem  16533  rpdvds  16587  coprmprod  16588  coprmproddvdslem  16589  congr  16591  cncongr1  16594  cncongr2  16595  prmz  16602  prmind2  16612  divgcdodd  16637  isprm6  16641  prmexpb  16646  prmfac1  16647  rpexp  16649  prmdvdsbc  16653  prmdvdsncoprmbd  16654  numdensq  16681  numdenexp  16687  hashdvds  16702  phiprmpw  16703  crth  16705  phimullem  16706  eulerthlem1  16708  eulerthlem2  16709  prmdivdiv  16714  hashgcdlem  16715  odzdvds  16723  pythagtriplem4  16747  pythagtriplem6  16749  pythagtriplem7  16750  pythagtriplem11  16753  pythagtriplem13  16755  pythagtriplem19  16761  pclem  16766  pcprendvds2  16769  pcpre1  16770  pcpremul  16771  pceulem  16773  pcqmul  16781  pcdvdsb  16797  pcidlem  16800  pcdvdstr  16804  pcgcd1  16805  pc2dvds  16807  pcprmpw2  16810  pcaddlem  16816  pcadd  16817  pcmpt2  16821  pcmptdvds  16822  pcfac  16827  pcbc  16828  qexpz  16829  oddprmdvds  16831  prmpwdvds  16832  pockthlem  16833  pockthg  16834  prmreclem2  16845  prmreclem3  16846  prmreclem4  16847  prmreclem5  16848  prmreclem6  16849  4sqlem5  16870  4sqlem8  16873  4sqlem9  16874  4sqlem10  16875  4sqlem12  16884  4sqlem14  16886  4sqlem16  16888  4sqlem17  16889  vdwlem1  16909  vdwlem2  16910  vdwlem3  16911  vdwlem6  16914  vdwlem9  16917  vdwlem10  16918  vdwnnlem3  16925  prmdvdsprmop  16971  prmolelcmf  16976  prmgaplem1  16977  prmgaplem7  16985  prmgaplem8  16986  gsumwsubmcl  18762  gsumsgrpccat  18765  gsumwmhm  18770  mulgneg  19022  mulgnndir  19033  psgnunilem4  19426  odlem2  19468  mndodconglem  19470  odmod  19475  gexlem2  19511  gexcl3  19516  gexcl2  19518  sylow1lem1  19527  sylow1lem3  19529  sylow1lem5  19531  pgpfi  19534  fislw  19554  sylow3lem4  19559  gexexlem  19781  ablfacrplem  19996  ablfacrp  19997  ablfacrp2  19998  ablfac1lem  19999  ablfac1b  20001  ablfac1eu  20004  pgpfac1lem3a  20007  ablfaclem3  20018  fincygsubgd  20042  fincygsubgodd  20043  znrrg  21520  psdpw  22113  cayhamlem1  22810  caublcls  25265  ovolicc2lem4  25477  iundisj2  25506  volsup  25513  uniioombllem3  25542  mbfi1fseqlem3  25674  mbfi1fseqlem4  25675  elqaalem2  26284  aalioulem1  26296  aalioulem4  26299  aalioulem5  26300  aalioulem6  26301  aaliou  26302  aaliou3lem1  26306  aaliou3lem2  26307  aaliou3lem3  26308  aaliou3lem8  26309  aaliou3lem5  26311  aaliou3lem6  26312  aaliou3lem7  26313  taylthlem2  26338  taylthlem2OLD  26339  cxpeq  26723  zrtelqelz  26724  amgmlem  26956  lgamgulmlem4  26998  lgamcvg2  27021  wilthlem2  27035  wilth  27037  wilthimp  27038  ftalem5  27043  basellem2  27048  basellem3  27049  basellem4  27050  basellem5  27051  muval1  27099  dvdssqf  27104  sgmnncl  27113  efchtdvds  27125  mumullem2  27146  mumul  27147  sqff1o  27148  fsumdvdsdiaglem  27149  dvdsppwf1o  27152  dvdsflf1o  27153  muinv  27159  mpodvdsmulf1o  27160  dvdsmulf1o  27162  chtublem  27178  fsumvma2  27181  vmasum  27183  chpchtsum  27186  logfacubnd  27188  mersenne  27194  perfect1  27195  perfectlem1  27196  perfectlem2  27197  perfect  27198  dchrelbas4  27210  dchrfi  27222  bcmono  27244  bcp1ctr  27246  bclbnd  27247  bposlem1  27251  bposlem3  27253  bposlem5  27255  bposlem6  27256  bposlem9  27259  lgsmod  27290  lgsdir  27299  lgsdilem2  27300  lgsne0  27302  lgsqrlem2  27314  lgsqr  27318  lgsqrmodndvds  27320  gausslemma2dlem0c  27325  gausslemma2dlem0h  27330  gausslemma2dlem0i  27331  gausslemma2dlem2  27334  gausslemma2dlem6  27339  gausslemma2dlem7  27340  gausslemma2d  27341  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgseisenlem4  27345  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  lgsquad2lem1  27351  lgsquad2lem2  27352  lgsquad2  27353  m1lgs  27355  2lgslem2  27362  2sqlem3  27387  2sqlem4  27388  2sqlem8  27393  chebbnd1lem1  27436  rplogsumlem2  27452  rpvmasumlem  27454  dchrisumlem1  27456  dchrisumlem2  27457  dchrisumlem3  27458  dchrisum0fmul  27473  dchrisum0ff  27474  dchrisum0flblem1  27475  dchrisum0flblem2  27476  dchrisum0flb  27477  dchrisum0  27487  pntrsumbnd2  27534  pntrlog2bndlem1  27544  pntrlog2bndlem6  27550  pntpbnd2  27554  pntlemg  27565  pntlemj  27570  pntlemf  27572  ostth2lem2  27601  ostth2lem3  27602  ostth3  27605  numclwlk2lem2f1o  30454  nrt2irr  30548  minvecolem4  30955  iundisj2f  32665  ssnnssfz  32867  iundisj2fi  32877  f1ocnt  32880  elq2  32892  numdenneg  32895  expgt0b  32897  ltesubnnd  32903  oexpled  32928  psgnfzto1stlem  33182  isarchi3  33269  archiabllem1b  33274  zringfrac  33635  fldextrspundgdvds  33838  cos9thpiminplylem2  33940  smatrcl  33953  1smat1  33961  submateqlem1  33964  lmatfvlem  33972  qqhval2  34139  qqhf  34143  qqhghm  34145  qqhrhm  34146  qqhnm  34147  qqhre  34177  esumcvg  34243  meascnbl  34376  omssubadd  34457  oddpwdc  34511  ballotlemfp1  34649  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemimin  34663  ballotlemic  34664  ballotlem1c  34665  hgt750lemc  34804  hgt750lemd  34805  hgt750lemb  34813  hgt750leme  34815  subfaclim  35382  cvmliftlem7  35485  sinccvglem  35866  bcprod  35932  bccolsum  35933  faclimlem2  35938  faclim2  35942  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem6  37827  poimirlem8  37829  poimirlem9  37830  poimirlem10  37831  poimirlem11  37832  poimirlem13  37834  poimirlem14  37835  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem18  37839  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem23  37844  poimirlem24  37845  poimirlem26  37847  poimirlem27  37848  poimirlem28  37849  poimirlem31  37852  mblfinlem2  37859  seqpo  37948  incsequz  37949  incsequz2  37950  zndvdchrrhm  42226  bccl2d  42245  nnproddivdvdsd  42254  lcmineqlem1  42283  lcmineqlem3  42285  lcmineqlem4  42286  lcmineqlem6  42288  lcmineqlem8  42290  lcmineqlem9  42291  lcmineqlem10  42292  lcmineqlem11  42293  lcmineqlem13  42295  lcmineqlem14  42296  lcmineqlem18  42300  lcmineqlem19  42301  lcmineqlem20  42302  lcmineqlem21  42303  lcmineqlem22  42304  lcmineqlem23  42305  lcmineqlem  42306  3lexlogpow5ineq2  42309  3lexlogpow2ineq1  42312  aks4d1p3  42332  aks4d1p5  42334  aks4d1p6  42335  aks4d1p8d1  42338  aks4d1p8d2  42339  aks4d1p8d3  42340  aks4d1p8  42341  aks4d1p9  42342  posbezout  42354  primrootscoprbij  42356  remexz  42358  primrootspoweq0  42360  aks6d1c1  42370  aks6d1c2p2  42373  hashscontpow1  42375  hashscontpow  42376  aks6d1c3  42377  aks6d1c4  42378  aks6d1c2lem4  42381  aks6d1c2  42384  aks6d1c5lem1  42390  sticksstones6  42405  sticksstones10  42409  sticksstones12a  42411  sticksstones12  42412  aks6d1c6lem3  42426  aks6d1c6lem4  42427  aks6d1c6isolem3  42430  aks6d1c6lem5  42431  aks6d1c7lem2  42435  aks6d1c7  42438  aks5lem1  42440  aks5lem2  42441  aks5lem3a  42443  grpods  42448  unitscyglem1  42449  unitscyglem2  42450  unitscyglem4  42452  unitscyglem5  42453  aks5  42458  sumcubes  42568  oexpreposd  42577  explt1d  42578  expeq1d  42579  expeqidd  42580  exp11d  42581  gcdle1d  42585  gcdle2d  42586  dvdsexpnn0  42589  fimgmcyc  42789  fltdvdsabdvdsc  42881  fltaccoprm  42883  fltbccoprm  42884  fltabcoprm  42885  fltne  42887  flt4lem2  42890  flt4lem3  42891  flt4lem4  42892  flt4lem5  42893  flt4lem5elem  42894  flt4lem5a  42895  flt4lem5b  42896  flt4lem5c  42897  flt4lem5d  42898  flt4lem5e  42899  flt4lem5f  42900  flt4lem6  42901  flt4lem7  42902  nna4b4nsq  42903  fltltc  42904  fltnlta  42906  irrapxlem3  43066  irrapxlem5  43068  pellexlem5  43075  pellexlem6  43076  pellex  43077  pell1234qrmulcl  43097  jm2.23  43238  jm2.20nn  43239  jm2.26lem3  43243  jm2.27a  43247  jm2.27b  43248  jm2.27c  43249  jm3.1lem1  43259  jm3.1lem3  43261  inductionexd  44396  nznngen  44557  hashnzfz2  44562  fmuldfeq  45829  divcnvg  45873  stoweidlem1  46245  stoweidlem3  46247  stoweidlem11  46255  stoweidlem20  46264  stoweidlem26  46270  stoweidlem34  46278  stoweidlem51  46295  stirlinglem4  46321  stirlinglem5  46322  stirlinglem8  46325  dirkerper  46340  dirkertrigeqlem2  46343  dirkertrigeqlem3  46344  dirkercncflem2  46348  fourierdlem11  46362  fourierdlem14  46365  fourierdlem20  46371  fourierdlem25  46376  fourierdlem37  46388  fourierdlem41  46392  fourierdlem48  46398  fourierdlem49  46399  fourierdlem54  46404  fourierdlem64  46414  fourierdlem73  46423  fourierdlem79  46429  fourierdlem92  46442  fourierdlem93  46443  fourierdlem111  46461  sqwvfourb  46473  etransclem3  46481  etransclem7  46485  etransclem10  46488  etransclem15  46493  etransclem24  46502  etransclem25  46503  etransclem26  46504  etransclem27  46505  etransclem28  46506  etransclem35  46513  etransclem37  46515  etransclem38  46516  etransclem41  46519  etransclem44  46522  etransclem45  46523  etransclem48  46526  ovnsubaddlem1  46814  vonioolem1  46924  iccpartgtprec  47666  iccpartipre  47667  fmtnoodd  47779  goldbachthlem2  47792  goldbachth  47793  odz2prm2pw  47809  fmtnoprmfac1lem  47810  fmtnoprmfac2lem1  47812  fmtnoprmfac2  47813  fmtnofac2lem  47814  2pwp1prm  47835  lighneallem1  47851  lighneallem4  47856  proththdlem  47859  proththd  47860  divgcdoddALTV  47928  perfectALTVlem1  47967  perfectALTVlem2  47968  perfectALTV  47969  gbowge7  48009  gpgedgvtx1  48308  gpg3kgrtriexlem2  48330  gpg3kgrtriexlem5  48333  pw2m1lepw2m1  48766  nnolog2flm1  48836  dignn0fr  48847  dignn0flhalflem1  48861