Theorem nnzd 12723

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 12671	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	2	nn0zd 12722	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℕcn 12339  ℤcz 12697

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7752  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-i2m1 11272  ax-1ne0 11273  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-neg 11548  df-nn 12340  df-n0 12611  df-z 12698

This theorem is used by:  expaddzlem  14252  expmulz  14255  expmulnbnd  14383  facndiv  14436  bcval5  14466  bcpasc  14469  hashf1  14606  isercolllem1  15838  isercolllem2  15839  o1fsum  15986  bcxmas  16010  climcndslem2  16025  climcnds  16026  mertenslem1  16059  fprodser  16122  bpolydiflem  16226  eftlub  16283  eirrlem  16378  rpnnen2lem7  16394  rpnnen2lem9  16396  rpnnen2lem11  16398  sqrt2irrlem  16422  dvdsfac  16502  dvdsmod  16505  oddpwp1fsum  16568  bitsfzolem  16610  bitsmod  16612  bitsfi  16613  bitscmp  16614  bitsinv1  16618  sadadd3  16637  sadaddlem  16642  bitsuz  16650  bitsshft  16651  gcdnncl  16683  gcdle1d  16686  gcdle2d  16687  gcd1  16707  dvdsgcdidd  16716  bezoutlem3  16720  bezoutlem4  16721  mulgcd  16727  rplpwr  16738  rprpwr  16739  sqgcd  16742  expgcd  16743  nn0expgcd  16744  dvdssq  16748  lcmneg  16784  lcmgcdlem  16787  rpdvds  16841  coprmprod  16842  coprmproddvdslem  16843  congr  16845  cncongr1  16848  cncongr2  16849  prmz  16856  prmind2  16866  divgcdodd  16892  isprm6  16896  prmexpb  16901  prmfac1  16902  rpexp  16904  prmdvdsbc  16908  prmdvdsncoprmbd  16909  numdensq  16936  numdenexp  16943  hashdvds  16958  phiprmpw  16959  crth  16961  phimullem  16962  eulerthlem1  16964  eulerthlem2  16965  prmdivdiv  16970  hashgcdlem  16971  odzdvds  16979  pythagtriplem4  17003  pythagtriplem6  17005  pythagtriplem7  17006  pythagtriplem11  17009  pythagtriplem13  17011  pythagtriplem19  17017  pclem  17022  pcprendvds2  17025  pcpre1  17026  pcpremul  17027  pceulem  17029  pcqmul  17037  pcdvdsb  17053  pcidlem  17056  pcdvdstr  17060  pcgcd1  17061  pc2dvds  17063  pcprmpw2  17066  pcaddlem  17072  pcadd  17073  pcmpt2  17077  pcmptdvds  17078  pcfac  17083  pcbc  17084  qexpz  17085  oddprmdvds  17087  prmpwdvds  17088  pockthlem  17089  pockthg  17090  prmreclem2  17101  prmreclem3  17102  prmreclem4  17103  prmreclem5  17104  prmreclem6  17105  4sqlem5  17126  4sqlem8  17129  4sqlem9  17130  4sqlem10  17131  4sqlem12  17140  4sqlem14  17142  4sqlem16  17144  4sqlem17  17145  vdwlem1  17165  vdwlem2  17166  vdwlem3  17167  vdwlem6  17170  vdwlem9  17173  vdwlem10  17174  vdwnnlem3  17181  prmdvdsprmop  17227  prmolelcmf  17232  prmgaplem1  17233  prmgaplem7  17241  prmgaplem8  17242  gsumwsubmcl  19039  gsumsgrpccat  19042  gsumwmhm  19047  mulgneg  19308  mulgnndir  19319  psgnunilem4  19717  odlem2  19759  mndodconglem  19761  odmod  19766  gexlem2  19802  gexcl3  19807  gexcl2  19809  sylow1lem1  19818  sylow1lem3  19820  sylow1lem5  19822  pgpfi  19825  fislw  19845  sylow3lem4  19850  gexexlem  20072  ablfacrplem  20287  ablfacrp  20288  ablfacrp2  20289  ablfac1lem  20290  ablfac1b  20292  ablfac1eu  20295  pgpfac1lem3a  20298  ablfaclem3  20309  fincygsubgd  20333  fincygsubgodd  20334  znrrg  21877  psdpw  22497  cayhamlem1  23190  caublcls  25636  ovolicc2lem4  25847  iundisj2  25876  volsup  25883  uniioombllem3  25912  mbfi1fseqlem3  26044  mbfi1fseqlem4  26045  elqaalem2  26649  aalioulem1  26665  aalioulem4  26668  aalioulem5  26669  aalioulem6  26670  aaliou  26671  aaliou3lem1  26675  aaliou3lem2  26676  aaliou3lem3  26677  aaliou3lem8  26678  aaliou3lem5  26680  aaliou3lem6  26681  aaliou3lem7  26682  taylthlem2  26707  cxpeq  27091  zrtelqelz  27092  amgmlem  27323  lgamgulmlem4  27365  lgamcvg2  27388  wilthlem2  27402  wilth  27404  wilthimp  27405  ftalem5  27410  basellem2  27415  basellem3  27416  basellem4  27417  basellem5  27418  muval1  27466  dvdssqf  27471  sgmnncl  27480  efchtdvds  27492  mumullem2  27513  mumul  27514  sqff1o  27515  fsumdvdsdiaglem  27516  dvdsppwf1o  27519  dvdsflf1o  27520  muinv  27526  mpodvdsmulf1o  27527  dvdsmulf1o  27529  chtublem  27544  fsumvma2  27547  vmasum  27549  chpchtsum  27552  logfacubnd  27554  mersenne  27560  perfect1  27561  perfectlem1  27562  perfectlem2  27563  perfect  27564  dchrelbas4  27576  dchrfi  27588  bcmono  27610  bcp1ctr  27612  bclbnd  27613  bposlem1  27617  bposlem3  27619  bposlem5  27621  bposlem6  27622  bposlem9  27625  lgsmod  27656  lgsdir  27665  lgsdilem2  27666  lgsne0  27668  lgsqrlem2  27680  lgsqr  27684  lgsqrmodndvds  27686  gausslemma2dlem0c  27691  gausslemma2dlem0h  27696  gausslemma2dlem0i  27697  gausslemma2dlem2  27700  gausslemma2dlem6  27705  gausslemma2dlem7  27706  gausslemma2d  27707  lgseisenlem1  27708  lgseisenlem2  27709  lgseisenlem3  27710  lgseisenlem4  27711  lgsquadlem1  27713  lgsquadlem2  27714  lgsquadlem3  27715  lgsquad2lem1  27717  lgsquad2lem2  27718  lgsquad2  27719  m1lgs  27721  2lgslem2  27728  2sqlem3  27753  2sqlem4  27754  2sqlem8  27759  chebbnd1lem1  27802  rplogsumlem2  27818  rpvmasumlem  27820  dchrisumlem1  27822  dchrisumlem2  27823  dchrisumlem3  27824  dchrisum0fmul  27839  dchrisum0ff  27840  dchrisum0flblem1  27841  dchrisum0flblem2  27842  dchrisum0flb  27843  dchrisum0  27853  pntrsumbnd2  27900  pntrlog2bndlem1  27910  pntrlog2bndlem6  27916  pntpbnd2  27920  pntlemg  27931  pntlemj  27936  pntlemf  27938  ostth2lem2  27967  ostth2lem3  27968  ostth3  27971  fltdvdsabdvdsc  27976  fltaccoprm  27978  fltbccoprm  27979  fltabcoprm  27980  fltne  27981  flt4lem3  27984  flt4lem4  27985  flt4lem5  27986  flt4lem5elem  27987  flt4lem5a  27988  flt4lem5b  27989  flt4lem5c  27990  flt4lem5d  27991  flt4lem5e  27992  flt4lem5f  27993  flt4lem6  27994  flt4lem7  27995  nna4b4nsq  27996  numclwlk2lem2f1o  30986  nrt2irr  31080  minvecolem4  31488  iundisj2f  33232  ssnnssfz  33426  iundisj2fi  33436  f1ocnt  33439  elq2  33450  numdenneg  33453  expgt0b  33455  ltesubnnd  33461  oexpled  33474  psgnfzto1stlem  33708  isarchi3  33795  archiabllem1b  33800  zringfrac  34133  fldextrspundgdvds  34360  cos9thpiminplylem2  34462  smatrcl  34475  1smat1  34483  submateqlem1  34486  lmatfvlem  34494  qqhval2  34661  qqhf  34665  qqhghm  34667  qqhrhm  34668  qqhnm  34669  qqhre  34699  esumcvg  34765  meascnbl  34899  omssubadd  34979  oddpwdc  35033  ballotlemfp1  35171  ballotlemfc0  35172  ballotlemfcc  35173  ballotlemimin  35185  ballotlemic  35186  ballotlem1c  35187  hgt750lemc  35323  hgt750lemd  35324  hgt750lemb  35332  hgt750leme  35334  subfaclim  36040  cvmliftlem7  36143  sinccvglem  36524  bcprod  36596  bccolsum  36597  faclimlem2  36602  faclim2  36606  poimirlem1  38633  poimirlem2  38634  poimirlem3  38635  poimirlem4  38636  poimirlem6  38638  poimirlem8  38640  poimirlem9  38641  poimirlem10  38642  poimirlem11  38643  poimirlem13  38645  poimirlem14  38646  poimirlem15  38647  poimirlem16  38648  poimirlem17  38649  poimirlem18  38650  poimirlem19  38651  poimirlem20  38652  poimirlem21  38653  poimirlem22  38654  poimirlem23  38655  poimirlem24  38656  poimirlem26  38658  poimirlem27  38659  poimirlem28  38660  poimirlem31  38663  mblfinlem2  38670  seqpo  38775  incsequz  38776  incsequz2  38777  zndvdchrrhm  43117  bccl2d  43135  nnproddivdvdsd  43144  lcmineqlem1  43173  lcmineqlem3  43175  lcmineqlem4  43176  lcmineqlem6  43178  lcmineqlem8  43180  lcmineqlem9  43181  lcmineqlem10  43182  lcmineqlem11  43183  lcmineqlem13  43185  lcmineqlem14  43186  lcmineqlem18  43190  lcmineqlem19  43191  lcmineqlem20  43192  lcmineqlem21  43193  lcmineqlem22  43194  lcmineqlem23  43195  lcmineqlem  43196  3lexlogpow5ineq2  43199  3lexlogpow2ineq1  43202  aks4d1p3  43222  aks4d1p5  43224  aks4d1p6  43225  aks4d1p8d1  43228  aks4d1p8d2  43229  aks4d1p8d3  43230  aks4d1p8  43231  aks4d1p9  43232  posbezout  43244  primrootscoprbij  43246  remexz  43248  primrootspoweq0  43250  aks6d1c1  43260  aks6d1c2p2  43263  hashscontpow1  43265  hashscontpow  43266  aks6d1c3  43267  aks6d1c4  43268  aks6d1c2lem4  43271  aks6d1c2  43274  aks6d1c5lem1  43280  sticksstones6  43295  sticksstones10  43299  sticksstones12a  43301  sticksstones12  43302  aks6d1c6lem3  43316  aks6d1c6lem4  43317  aks6d1c6isolem3  43320  aks6d1c6lem5  43321  aks6d1c7lem2  43325  aks6d1c7  43328  aks5lem1  43330  aks5lem2  43331  aks5lem3a  43333  grpods  43338  unitscyglem1  43339  unitscyglem2  43340  unitscyglem4  43342  unitscyglem5  43343  aks5  43348  sumcubes  43464  oexpreposd  43473  explt1d  43474  expeq1d  43475  expeqidd  43476  exp11d  43477  dvdsexpnn0  43480  fimgmcyc  43692  fltltc  43766  fltnlta  43768  irrapxlem3  43925  irrapxlem5  43927  pellexlem5  43934  pellexlem6  43935  pellex  43936  pell1234qrmulcl  43956  jm2.23  44097  jm2.20nn  44098  jm2.26lem3  44102  jm2.27a  44106  jm2.27b  44107  jm2.27c  44108  jm3.1lem1  44118  jm3.1lem3  44120  inductionexd  45249  nznngen  45394  hashnzfz2  45399  fmuldfeq  46689  divcnvg  46733  stoweidlem1  47105  stoweidlem3  47107  stoweidlem11  47115  stoweidlem20  47124  stoweidlem26  47130  stoweidlem34  47138  stoweidlem51  47155  stirlinglem4  47181  stirlinglem5  47182  stirlinglem8  47185  dirkerper  47200  dirkertrigeqlem2  47203  dirkertrigeqlem3  47204  dirkercncflem2  47208  fourierdlem11  47222  fourierdlem14  47225  fourierdlem20  47231  fourierdlem25  47236  fourierdlem37  47248  fourierdlem41  47252  fourierdlem48  47258  fourierdlem49  47259  fourierdlem54  47264  fourierdlem64  47274  fourierdlem73  47283  fourierdlem79  47289  fourierdlem92  47302  fourierdlem93  47303  fourierdlem111  47321  sqwvfourb  47333  etransclem3  47341  etransclem7  47345  etransclem10  47348  etransclem15  47353  etransclem24  47362  etransclem25  47363  etransclem26  47364  etransclem27  47365  etransclem28  47366  etransclem35  47373  etransclem37  47375  etransclem38  47376  etransclem41  47379  etransclem44  47382  etransclem45  47383  etransclem48  47386  ovnsubaddlem1  47674  vonioolem1  47784  facnn0dvdsfac  48549  muldvdsfacgt  48550  muldvdsfacm1  48551  iccpartgtprec  48596  iccpartipre  48597  fmtnoodd  48712  goldbachthlem2  48725  goldbachth  48726  odz2prm2pw  48742  fmtnoprmfac1lem  48743  fmtnoprmfac2lem1  48745  fmtnoprmfac2  48746  fmtnofac2lem  48747  2pwp1prm  48768  lighneallem1  48784  lighneallem4  48789  proththdlem  48792  proththd  48793  nprmdvdsfacm1lem4  48802  ppivalnnprm  48804  ppivalnnnprmge6  48805  divgcdoddALTV  48874  perfectALTVlem1  48913  perfectALTVlem2  48914  perfectALTV  48915  gbowge7  48955  gpgedgvtx1  49254  gpg3kgrtriexlem2  49276  gpg3kgrtriexlem5  49279  pw2m1lepw2m1  49726  nnolog2flm1  49796  dignn0fr  49807  dignn0flhalflem1  49821