Theorem nnzd 12541

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 12165  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  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 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516

This theorem is referenced by:  expaddzlem  14058  expmulz  14061  expmulnbnd  14188  facndiv  14241  bcval5  14271  bcpasc  14274  hashf1  14410  isercolllem1  15618  isercolllem2  15619  o1fsum  15767  bcxmas  15791  climcndslem2  15806  climcnds  15807  mertenslem1  15840  fprodser  15905  bpolydiflem  16010  eftlub  16067  eirrlem  16162  rpnnen2lem7  16178  rpnnen2lem9  16180  rpnnen2lem11  16182  sqrt2irrlem  16206  dvdsfac  16286  dvdsmod  16289  oddpwp1fsum  16352  bitsfzolem  16394  bitsmod  16396  bitsfi  16397  bitscmp  16398  bitsinv1  16402  sadadd3  16421  sadaddlem  16426  bitsuz  16434  bitsshft  16435  gcdnncl  16467  gcd1  16488  dvdsgcdidd  16497  bezoutlem3  16501  bezoutlem4  16502  mulgcd  16508  rplpwr  16518  rprpwr  16519  sqgcd  16522  expgcd  16523  nn0expgcd  16524  dvdssq  16527  lcmneg  16563  lcmgcdlem  16566  rpdvds  16620  coprmprod  16621  coprmproddvdslem  16622  congr  16624  cncongr1  16627  cncongr2  16628  prmz  16635  prmind2  16645  divgcdodd  16671  isprm6  16675  prmexpb  16680  prmfac1  16681  rpexp  16683  prmdvdsbc  16687  prmdvdsncoprmbd  16688  numdensq  16715  numdenexp  16721  hashdvds  16736  phiprmpw  16737  crth  16739  phimullem  16740  eulerthlem1  16742  eulerthlem2  16743  prmdivdiv  16748  hashgcdlem  16749  odzdvds  16757  pythagtriplem4  16781  pythagtriplem6  16783  pythagtriplem7  16784  pythagtriplem11  16787  pythagtriplem13  16789  pythagtriplem19  16795  pclem  16800  pcprendvds2  16803  pcpre1  16804  pcpremul  16805  pceulem  16807  pcqmul  16815  pcdvdsb  16831  pcidlem  16834  pcdvdstr  16838  pcgcd1  16839  pc2dvds  16841  pcprmpw2  16844  pcaddlem  16850  pcadd  16851  pcmpt2  16855  pcmptdvds  16856  pcfac  16861  pcbc  16862  qexpz  16863  oddprmdvds  16865  prmpwdvds  16866  pockthlem  16867  pockthg  16868  prmreclem2  16879  prmreclem3  16880  prmreclem4  16881  prmreclem5  16882  prmreclem6  16883  4sqlem5  16904  4sqlem8  16907  4sqlem9  16908  4sqlem10  16909  4sqlem12  16918  4sqlem14  16920  4sqlem16  16922  4sqlem17  16923  vdwlem1  16943  vdwlem2  16944  vdwlem3  16945  vdwlem6  16948  vdwlem9  16951  vdwlem10  16952  vdwnnlem3  16959  prmdvdsprmop  17005  prmolelcmf  17010  prmgaplem1  17011  prmgaplem7  17019  prmgaplem8  17020  gsumwsubmcl  18796  gsumsgrpccat  18799  gsumwmhm  18804  mulgneg  19059  mulgnndir  19070  psgnunilem4  19463  odlem2  19505  mndodconglem  19507  odmod  19512  gexlem2  19548  gexcl3  19553  gexcl2  19555  sylow1lem1  19564  sylow1lem3  19566  sylow1lem5  19568  pgpfi  19571  fislw  19591  sylow3lem4  19596  gexexlem  19818  ablfacrplem  20033  ablfacrp  20034  ablfacrp2  20035  ablfac1lem  20036  ablfac1b  20038  ablfac1eu  20041  pgpfac1lem3a  20044  ablfaclem3  20055  fincygsubgd  20079  fincygsubgodd  20080  znrrg  21555  psdpw  22146  cayhamlem1  22841  caublcls  25286  ovolicc2lem4  25497  iundisj2  25526  volsup  25533  uniioombllem3  25562  mbfi1fseqlem3  25694  mbfi1fseqlem4  25695  elqaalem2  26297  aalioulem1  26309  aalioulem4  26312  aalioulem5  26313  aalioulem6  26314  aaliou  26315  aaliou3lem1  26319  aaliou3lem2  26320  aaliou3lem3  26321  aaliou3lem8  26322  aaliou3lem5  26324  aaliou3lem6  26325  aaliou3lem7  26326  taylthlem2  26351  taylthlem2OLD  26352  cxpeq  26734  zrtelqelz  26735  amgmlem  26967  lgamgulmlem4  27009  lgamcvg2  27032  wilthlem2  27046  wilth  27048  wilthimp  27049  ftalem5  27054  basellem2  27059  basellem3  27060  basellem4  27061  basellem5  27062  muval1  27110  dvdssqf  27115  sgmnncl  27124  efchtdvds  27136  mumullem2  27157  mumul  27158  sqff1o  27159  fsumdvdsdiaglem  27160  dvdsppwf1o  27163  dvdsflf1o  27164  muinv  27170  mpodvdsmulf1o  27171  dvdsmulf1o  27173  chtublem  27188  fsumvma2  27191  vmasum  27193  chpchtsum  27196  logfacubnd  27198  mersenne  27204  perfect1  27205  perfectlem1  27206  perfectlem2  27207  perfect  27208  dchrelbas4  27220  dchrfi  27232  bcmono  27254  bcp1ctr  27256  bclbnd  27257  bposlem1  27261  bposlem3  27263  bposlem5  27265  bposlem6  27266  bposlem9  27269  lgsmod  27300  lgsdir  27309  lgsdilem2  27310  lgsne0  27312  lgsqrlem2  27324  lgsqr  27328  lgsqrmodndvds  27330  gausslemma2dlem0c  27335  gausslemma2dlem0h  27340  gausslemma2dlem0i  27341  gausslemma2dlem2  27344  gausslemma2dlem6  27349  gausslemma2dlem7  27350  gausslemma2d  27351  lgseisenlem1  27352  lgseisenlem2  27353  lgseisenlem3  27354  lgseisenlem4  27355  lgsquadlem1  27357  lgsquadlem2  27358  lgsquadlem3  27359  lgsquad2lem1  27361  lgsquad2lem2  27362  lgsquad2  27363  m1lgs  27365  2lgslem2  27372  2sqlem3  27397  2sqlem4  27398  2sqlem8  27403  chebbnd1lem1  27446  rplogsumlem2  27462  rpvmasumlem  27464  dchrisumlem1  27466  dchrisumlem2  27467  dchrisumlem3  27468  dchrisum0fmul  27483  dchrisum0ff  27484  dchrisum0flblem1  27485  dchrisum0flblem2  27486  dchrisum0flb  27487  dchrisum0  27497  pntrsumbnd2  27544  pntrlog2bndlem1  27554  pntrlog2bndlem6  27560  pntpbnd2  27564  pntlemg  27575  pntlemj  27580  pntlemf  27582  ostth2lem2  27611  ostth2lem3  27612  ostth3  27615  numclwlk2lem2f1o  30464  nrt2irr  30558  minvecolem4  30966  iundisj2f  32675  ssnnssfz  32875  iundisj2fi  32885  f1ocnt  32888  elq2  32900  numdenneg  32903  expgt0b  32905  ltesubnnd  32911  oexpled  32935  psgnfzto1stlem  33176  isarchi3  33263  archiabllem1b  33268  zringfrac  33629  fldextrspundgdvds  33841  cos9thpiminplylem2  33943  smatrcl  33956  1smat1  33964  submateqlem1  33967  lmatfvlem  33975  qqhval2  34142  qqhf  34146  qqhghm  34148  qqhrhm  34149  qqhnm  34150  qqhre  34180  esumcvg  34246  meascnbl  34379  omssubadd  34460  oddpwdc  34514  ballotlemfp1  34652  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemimin  34666  ballotlemic  34667  ballotlem1c  34668  hgt750lemc  34807  hgt750lemd  34808  hgt750lemb  34816  hgt750leme  34818  subfaclim  35386  cvmliftlem7  35489  sinccvglem  35870  bcprod  35936  bccolsum  35937  faclimlem2  35942  faclim2  35946  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem4  37959  poimirlem6  37961  poimirlem8  37963  poimirlem9  37964  poimirlem10  37965  poimirlem11  37966  poimirlem13  37968  poimirlem14  37969  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem18  37973  poimirlem19  37974  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem23  37978  poimirlem24  37979  poimirlem26  37981  poimirlem27  37982  poimirlem28  37983  poimirlem31  37986  mblfinlem2  37993  seqpo  38082  incsequz  38083  incsequz2  38084  zndvdchrrhm  42426  bccl2d  42444  nnproddivdvdsd  42453  lcmineqlem1  42482  lcmineqlem3  42484  lcmineqlem4  42485  lcmineqlem6  42487  lcmineqlem8  42489  lcmineqlem9  42490  lcmineqlem10  42491  lcmineqlem11  42492  lcmineqlem13  42494  lcmineqlem14  42495  lcmineqlem18  42499  lcmineqlem19  42500  lcmineqlem20  42501  lcmineqlem21  42502  lcmineqlem22  42503  lcmineqlem23  42504  lcmineqlem  42505  3lexlogpow5ineq2  42508  3lexlogpow2ineq1  42511  aks4d1p3  42531  aks4d1p5  42533  aks4d1p6  42534  aks4d1p8d1  42537  aks4d1p8d2  42538  aks4d1p8d3  42539  aks4d1p8  42540  aks4d1p9  42541  posbezout  42553  primrootscoprbij  42555  remexz  42557  primrootspoweq0  42559  aks6d1c1  42569  aks6d1c2p2  42572  hashscontpow1  42574  hashscontpow  42575  aks6d1c3  42576  aks6d1c4  42577  aks6d1c2lem4  42580  aks6d1c2  42583  aks6d1c5lem1  42589  sticksstones6  42604  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  aks6d1c6lem3  42625  aks6d1c6lem4  42626  aks6d1c6isolem3  42629  aks6d1c6lem5  42630  aks6d1c7lem2  42634  aks6d1c7  42637  aks5lem1  42639  aks5lem2  42640  aks5lem3a  42642  grpods  42647  unitscyglem1  42648  unitscyglem2  42649  unitscyglem4  42651  unitscyglem5  42652  aks5  42657  sumcubes  42759  oexpreposd  42768  explt1d  42769  expeq1d  42770  expeqidd  42771  exp11d  42772  gcdle1d  42776  gcdle2d  42777  dvdsexpnn0  42780  fimgmcyc  42993  fltdvdsabdvdsc  43085  fltaccoprm  43087  fltbccoprm  43088  fltabcoprm  43089  fltne  43091  flt4lem2  43094  flt4lem3  43095  flt4lem4  43096  flt4lem5  43097  flt4lem5elem  43098  flt4lem5a  43099  flt4lem5b  43100  flt4lem5c  43101  flt4lem5d  43102  flt4lem5e  43103  flt4lem5f  43104  flt4lem6  43105  flt4lem7  43106  nna4b4nsq  43107  fltltc  43108  fltnlta  43110  irrapxlem3  43270  irrapxlem5  43272  pellexlem5  43279  pellexlem6  43280  pellex  43281  pell1234qrmulcl  43301  jm2.23  43442  jm2.20nn  43443  jm2.26lem3  43447  jm2.27a  43451  jm2.27b  43452  jm2.27c  43453  jm3.1lem1  43463  jm3.1lem3  43465  inductionexd  44600  nznngen  44761  hashnzfz2  44766  fmuldfeq  46031  divcnvg  46075  stoweidlem1  46447  stoweidlem3  46449  stoweidlem11  46457  stoweidlem20  46466  stoweidlem26  46472  stoweidlem34  46480  stoweidlem51  46497  stirlinglem4  46523  stirlinglem5  46524  stirlinglem8  46527  dirkerper  46542  dirkertrigeqlem2  46545  dirkertrigeqlem3  46546  dirkercncflem2  46550  fourierdlem11  46564  fourierdlem14  46567  fourierdlem20  46573  fourierdlem25  46578  fourierdlem37  46590  fourierdlem41  46594  fourierdlem48  46600  fourierdlem49  46601  fourierdlem54  46606  fourierdlem64  46616  fourierdlem73  46625  fourierdlem79  46631  fourierdlem92  46644  fourierdlem93  46645  fourierdlem111  46663  sqwvfourb  46675  etransclem3  46683  etransclem7  46687  etransclem10  46690  etransclem15  46695  etransclem24  46704  etransclem25  46705  etransclem26  46706  etransclem27  46707  etransclem28  46708  etransclem35  46715  etransclem37  46717  etransclem38  46718  etransclem41  46721  etransclem44  46724  etransclem45  46725  etransclem48  46728  ovnsubaddlem1  47016  vonioolem1  47126  facnn0dvdsfac  47845  muldvdsfacgt  47846  muldvdsfacm1  47847  iccpartgtprec  47892  iccpartipre  47893  fmtnoodd  48008  goldbachthlem2  48021  goldbachth  48022  odz2prm2pw  48038  fmtnoprmfac1lem  48039  fmtnoprmfac2lem1  48041  fmtnoprmfac2  48042  fmtnofac2lem  48043  2pwp1prm  48064  lighneallem1  48080  lighneallem4  48085  proththdlem  48088  proththd  48089  nprmdvdsfacm1lem4  48098  ppivalnnprm  48100  ppivalnnnprmge6  48101  divgcdoddALTV  48170  perfectALTVlem1  48209  perfectALTVlem2  48210  perfectALTV  48211  gbowge7  48251  gpgedgvtx1  48550  gpg3kgrtriexlem2  48572  gpg3kgrtriexlem5  48575  pw2m1lepw2m1  49008  nnolog2flm1  49078  dignn0fr  49089  dignn0flhalflem1  49103