Theorem nnzd 12550

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 12174  ℤcz 12524

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-neg 11380  df-nn 12175  df-n0 12438  df-z 12525

This theorem is referenced by:  expaddzlem  14067  expmulz  14070  expmulnbnd  14197  facndiv  14250  bcval5  14280  bcpasc  14283  hashf1  14419  isercolllem1  15627  isercolllem2  15628  o1fsum  15776  bcxmas  15800  climcndslem2  15815  climcnds  15816  mertenslem1  15849  fprodser  15914  bpolydiflem  16019  eftlub  16076  eirrlem  16171  rpnnen2lem7  16187  rpnnen2lem9  16189  rpnnen2lem11  16191  sqrt2irrlem  16215  dvdsfac  16295  dvdsmod  16298  oddpwp1fsum  16361  bitsfzolem  16403  bitsmod  16405  bitsfi  16406  bitscmp  16407  bitsinv1  16411  sadadd3  16430  sadaddlem  16435  bitsuz  16443  bitsshft  16444  gcdnncl  16476  gcd1  16497  dvdsgcdidd  16506  bezoutlem3  16510  bezoutlem4  16511  mulgcd  16517  rplpwr  16527  rprpwr  16528  sqgcd  16531  expgcd  16532  nn0expgcd  16533  dvdssq  16536  lcmneg  16572  lcmgcdlem  16575  rpdvds  16629  coprmprod  16630  coprmproddvdslem  16631  congr  16633  cncongr1  16636  cncongr2  16637  prmz  16644  prmind2  16654  divgcdodd  16680  isprm6  16684  prmexpb  16689  prmfac1  16690  rpexp  16692  prmdvdsbc  16696  prmdvdsncoprmbd  16697  numdensq  16724  numdenexp  16730  hashdvds  16745  phiprmpw  16746  crth  16748  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  prmdivdiv  16757  hashgcdlem  16758  odzdvds  16766  pythagtriplem4  16790  pythagtriplem6  16792  pythagtriplem7  16793  pythagtriplem11  16796  pythagtriplem13  16798  pythagtriplem19  16804  pclem  16809  pcprendvds2  16812  pcpre1  16813  pcpremul  16814  pceulem  16816  pcqmul  16824  pcdvdsb  16840  pcidlem  16843  pcdvdstr  16847  pcgcd1  16848  pc2dvds  16850  pcprmpw2  16853  pcaddlem  16859  pcadd  16860  pcmpt2  16864  pcmptdvds  16865  pcfac  16870  pcbc  16871  qexpz  16872  oddprmdvds  16874  prmpwdvds  16875  pockthlem  16876  pockthg  16877  prmreclem2  16888  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  4sqlem5  16913  4sqlem8  16916  4sqlem9  16917  4sqlem10  16918  4sqlem12  16927  4sqlem14  16929  4sqlem16  16931  4sqlem17  16932  vdwlem1  16952  vdwlem2  16953  vdwlem3  16954  vdwlem6  16957  vdwlem9  16960  vdwlem10  16961  vdwnnlem3  16968  prmdvdsprmop  17014  prmolelcmf  17019  prmgaplem1  17020  prmgaplem7  17028  prmgaplem8  17029  gsumwsubmcl  18805  gsumsgrpccat  18808  gsumwmhm  18813  mulgneg  19068  mulgnndir  19079  psgnunilem4  19472  odlem2  19514  mndodconglem  19516  odmod  19521  gexlem2  19557  gexcl3  19562  gexcl2  19564  sylow1lem1  19573  sylow1lem3  19575  sylow1lem5  19577  pgpfi  19580  fislw  19600  sylow3lem4  19605  gexexlem  19827  ablfacrplem  20042  ablfacrp  20043  ablfacrp2  20044  ablfac1lem  20045  ablfac1b  20047  ablfac1eu  20050  pgpfac1lem3a  20053  ablfaclem3  20064  fincygsubgd  20088  fincygsubgodd  20089  znrrg  21545  psdpw  22136  cayhamlem1  22831  caublcls  25276  ovolicc2lem4  25487  iundisj2  25516  volsup  25523  uniioombllem3  25552  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  elqaalem2  26286  aalioulem1  26298  aalioulem4  26301  aalioulem5  26302  aalioulem6  26303  aaliou  26304  aaliou3lem1  26308  aaliou3lem2  26309  aaliou3lem3  26310  aaliou3lem8  26311  aaliou3lem5  26313  aaliou3lem6  26314  aaliou3lem7  26315  taylthlem2  26339  cxpeq  26721  zrtelqelz  26722  amgmlem  26953  lgamgulmlem4  26995  lgamcvg2  27018  wilthlem2  27032  wilth  27034  wilthimp  27035  ftalem5  27040  basellem2  27045  basellem3  27046  basellem4  27047  basellem5  27048  muval1  27096  dvdssqf  27101  sgmnncl  27110  efchtdvds  27122  mumullem2  27143  mumul  27144  sqff1o  27145  fsumdvdsdiaglem  27146  dvdsppwf1o  27149  dvdsflf1o  27150  muinv  27156  mpodvdsmulf1o  27157  dvdsmulf1o  27159  chtublem  27174  fsumvma2  27177  vmasum  27179  chpchtsum  27182  logfacubnd  27184  mersenne  27190  perfect1  27191  perfectlem1  27192  perfectlem2  27193  perfect  27194  dchrelbas4  27206  dchrfi  27218  bcmono  27240  bcp1ctr  27242  bclbnd  27243  bposlem1  27247  bposlem3  27249  bposlem5  27251  bposlem6  27252  bposlem9  27255  lgsmod  27286  lgsdir  27295  lgsdilem2  27296  lgsne0  27298  lgsqrlem2  27310  lgsqr  27314  lgsqrmodndvds  27316  gausslemma2dlem0c  27321  gausslemma2dlem0h  27326  gausslemma2dlem0i  27327  gausslemma2dlem2  27330  gausslemma2dlem6  27335  gausslemma2dlem7  27336  gausslemma2d  27337  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisenlem4  27341  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  lgsquad2lem1  27347  lgsquad2lem2  27348  lgsquad2  27349  m1lgs  27351  2lgslem2  27358  2sqlem3  27383  2sqlem4  27384  2sqlem8  27389  chebbnd1lem1  27432  rplogsumlem2  27448  rpvmasumlem  27450  dchrisumlem1  27452  dchrisumlem2  27453  dchrisumlem3  27454  dchrisum0fmul  27469  dchrisum0ff  27470  dchrisum0flblem1  27471  dchrisum0flblem2  27472  dchrisum0flb  27473  dchrisum0  27483  pntrsumbnd2  27530  pntrlog2bndlem1  27540  pntrlog2bndlem6  27546  pntpbnd2  27550  pntlemg  27561  pntlemj  27566  pntlemf  27568  ostth2lem2  27597  ostth2lem3  27598  ostth3  27601  numclwlk2lem2f1o  30449  nrt2irr  30543  minvecolem4  30951  iundisj2f  32660  ssnnssfz  32860  iundisj2fi  32870  f1ocnt  32873  elq2  32885  numdenneg  32888  expgt0b  32890  ltesubnnd  32896  oexpled  32920  psgnfzto1stlem  33161  isarchi3  33248  archiabllem1b  33253  zringfrac  33614  fldextrspundgdvds  33825  cos9thpiminplylem2  33927  smatrcl  33940  1smat1  33948  submateqlem1  33951  lmatfvlem  33959  qqhval2  34126  qqhf  34130  qqhghm  34132  qqhrhm  34133  qqhnm  34134  qqhre  34164  esumcvg  34230  meascnbl  34363  omssubadd  34444  oddpwdc  34498  ballotlemfp1  34636  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemimin  34650  ballotlemic  34651  ballotlem1c  34652  hgt750lemc  34791  hgt750lemd  34792  hgt750lemb  34800  hgt750leme  34802  subfaclim  35370  cvmliftlem7  35473  sinccvglem  35854  bcprod  35920  bccolsum  35921  faclimlem2  35926  faclim2  35930  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem8  37949  poimirlem9  37950  poimirlem10  37951  poimirlem11  37952  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  poimirlem31  37972  mblfinlem2  37979  seqpo  38068  incsequz  38069  incsequz2  38070  zndvdchrrhm  42412  bccl2d  42430  nnproddivdvdsd  42439  lcmineqlem1  42468  lcmineqlem3  42470  lcmineqlem4  42471  lcmineqlem6  42473  lcmineqlem8  42475  lcmineqlem9  42476  lcmineqlem10  42477  lcmineqlem11  42478  lcmineqlem13  42480  lcmineqlem14  42481  lcmineqlem18  42485  lcmineqlem19  42486  lcmineqlem20  42487  lcmineqlem21  42488  lcmineqlem22  42489  lcmineqlem23  42490  lcmineqlem  42491  3lexlogpow5ineq2  42494  3lexlogpow2ineq1  42497  aks4d1p3  42517  aks4d1p5  42519  aks4d1p6  42520  aks4d1p8d1  42523  aks4d1p8d2  42524  aks4d1p8d3  42525  aks4d1p8  42526  aks4d1p9  42527  posbezout  42539  primrootscoprbij  42541  remexz  42543  primrootspoweq0  42545  aks6d1c1  42555  aks6d1c2p2  42558  hashscontpow1  42560  hashscontpow  42561  aks6d1c3  42562  aks6d1c4  42563  aks6d1c2lem4  42566  aks6d1c2  42569  aks6d1c5lem1  42575  sticksstones6  42590  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c6isolem3  42615  aks6d1c6lem5  42616  aks6d1c7lem2  42620  aks6d1c7  42623  aks5lem1  42625  aks5lem2  42626  aks5lem3a  42628  grpods  42633  unitscyglem1  42634  unitscyglem2  42635  unitscyglem4  42637  unitscyglem5  42638  aks5  42643  sumcubes  42745  oexpreposd  42754  explt1d  42755  expeq1d  42756  expeqidd  42757  exp11d  42758  gcdle1d  42762  gcdle2d  42763  dvdsexpnn0  42766  fimgmcyc  42979  fltdvdsabdvdsc  43071  fltaccoprm  43073  fltbccoprm  43074  fltabcoprm  43075  fltne  43077  flt4lem2  43080  flt4lem3  43081  flt4lem4  43082  flt4lem5  43083  flt4lem5elem  43084  flt4lem5a  43085  flt4lem5b  43086  flt4lem5c  43087  flt4lem5d  43088  flt4lem5e  43089  flt4lem5f  43090  flt4lem6  43091  flt4lem7  43092  nna4b4nsq  43093  fltltc  43094  fltnlta  43096  irrapxlem3  43252  irrapxlem5  43254  pellexlem5  43261  pellexlem6  43262  pellex  43263  pell1234qrmulcl  43283  jm2.23  43424  jm2.20nn  43425  jm2.26lem3  43429  jm2.27a  43433  jm2.27b  43434  jm2.27c  43435  jm3.1lem1  43445  jm3.1lem3  43447  inductionexd  44582  nznngen  44743  hashnzfz2  44748  fmuldfeq  46013  divcnvg  46057  stoweidlem1  46429  stoweidlem3  46431  stoweidlem11  46439  stoweidlem20  46448  stoweidlem26  46454  stoweidlem34  46462  stoweidlem51  46479  stirlinglem4  46505  stirlinglem5  46506  stirlinglem8  46509  dirkerper  46524  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkercncflem2  46532  fourierdlem11  46546  fourierdlem14  46549  fourierdlem20  46555  fourierdlem25  46560  fourierdlem37  46572  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem54  46588  fourierdlem64  46598  fourierdlem73  46607  fourierdlem79  46613  fourierdlem92  46626  fourierdlem93  46627  fourierdlem111  46645  sqwvfourb  46657  etransclem3  46665  etransclem7  46669  etransclem10  46672  etransclem15  46677  etransclem24  46686  etransclem25  46687  etransclem26  46688  etransclem27  46689  etransclem28  46690  etransclem35  46697  etransclem37  46699  etransclem38  46700  etransclem41  46703  etransclem44  46706  etransclem45  46707  etransclem48  46710  ovnsubaddlem1  46998  vonioolem1  47108  facnn0dvdsfac  47833  muldvdsfacgt  47834  muldvdsfacm1  47835  iccpartgtprec  47880  iccpartipre  47881  fmtnoodd  47996  goldbachthlem2  48009  goldbachth  48010  odz2prm2pw  48026  fmtnoprmfac1lem  48027  fmtnoprmfac2lem1  48029  fmtnoprmfac2  48030  fmtnofac2lem  48031  2pwp1prm  48052  lighneallem1  48068  lighneallem4  48073  proththdlem  48076  proththd  48077  nprmdvdsfacm1lem4  48086  ppivalnnprm  48088  ppivalnnnprmge6  48089  divgcdoddALTV  48158  perfectALTVlem1  48197  perfectALTVlem2  48198  perfectALTV  48199  gbowge7  48239  gpgedgvtx1  48538  gpg3kgrtriexlem2  48560  gpg3kgrtriexlem5  48563  pw2m1lepw2m1  48996  nnolog2flm1  49066  dignn0fr  49077  dignn0flhalflem1  49091