Theorem nnzd 12612

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℕcn 12228  ℤcz 12586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-neg 11439  df-nn 12229  df-n0 12500  df-z 12587

This theorem is referenced by:  expaddzlem  14137  expmulz  14140  expmulnbnd  14267  facndiv  14320  bcval5  14350  bcpasc  14353  hashf1  14490  isercolllem1  15712  isercolllem2  15713  o1fsum  15861  bcxmas  15885  climcndslem2  15900  climcnds  15901  mertenslem1  15934  fprodser  15999  bpolydiflem  16103  eftlub  16160  eirrlem  16255  rpnnen2lem7  16271  rpnnen2lem9  16273  rpnnen2lem11  16275  sqrt2irrlem  16299  dvdsfac  16379  dvdsmod  16382  oddpwp1fsum  16445  bitsfzolem  16487  bitsmod  16489  bitsfi  16490  bitscmp  16491  bitsinv1  16495  sadadd3  16514  sadaddlem  16519  bitsuz  16527  bitsshft  16528  gcdnncl  16560  gcd1  16581  dvdsgcdidd  16590  bezoutlem3  16594  bezoutlem4  16595  mulgcd  16601  rplpwr  16611  rprpwr  16612  sqgcd  16615  expgcd  16616  nn0expgcd  16617  dvdssq  16620  lcmneg  16656  lcmgcdlem  16659  rpdvds  16713  coprmprod  16714  coprmproddvdslem  16715  congr  16717  cncongr1  16720  cncongr2  16721  prmz  16728  prmind2  16738  divgcdodd  16764  isprm6  16768  prmexpb  16773  prmfac1  16774  rpexp  16776  prmdvdsbc  16780  prmdvdsncoprmbd  16781  numdensq  16808  numdenexp  16814  hashdvds  16829  phiprmpw  16830  crth  16832  phimullem  16833  eulerthlem1  16835  eulerthlem2  16836  prmdivdiv  16841  hashgcdlem  16842  odzdvds  16850  pythagtriplem4  16874  pythagtriplem6  16876  pythagtriplem7  16877  pythagtriplem11  16880  pythagtriplem13  16882  pythagtriplem19  16888  pclem  16893  pcprendvds2  16896  pcpre1  16897  pcpremul  16898  pceulem  16900  pcqmul  16908  pcdvdsb  16924  pcidlem  16927  pcdvdstr  16931  pcgcd1  16932  pc2dvds  16934  pcprmpw2  16937  pcaddlem  16943  pcadd  16944  pcmpt2  16948  pcmptdvds  16949  pcfac  16954  pcbc  16955  qexpz  16956  oddprmdvds  16958  prmpwdvds  16959  pockthlem  16960  pockthg  16961  prmreclem2  16972  prmreclem3  16973  prmreclem4  16974  prmreclem5  16975  prmreclem6  16976  4sqlem5  16997  4sqlem8  17000  4sqlem9  17001  4sqlem10  17002  4sqlem12  17011  4sqlem14  17013  4sqlem16  17015  4sqlem17  17016  vdwlem1  17036  vdwlem2  17037  vdwlem3  17038  vdwlem6  17041  vdwlem9  17044  vdwlem10  17045  vdwnnlem3  17052  prmdvdsprmop  17098  prmolelcmf  17103  prmgaplem1  17104  prmgaplem7  17112  prmgaplem8  17113  gsumwsubmcl  18891  gsumsgrpccat  18894  gsumwmhm  18899  mulgneg  19153  mulgnndir  19164  psgnunilem4  19562  odlem2  19604  mndodconglem  19606  odmod  19611  gexlem2  19647  gexcl3  19652  gexcl2  19654  sylow1lem1  19663  sylow1lem3  19665  sylow1lem5  19667  pgpfi  19670  fislw  19690  sylow3lem4  19695  gexexlem  19917  ablfacrplem  20132  ablfacrp  20133  ablfacrp2  20134  ablfac1lem  20135  ablfac1b  20137  ablfac1eu  20140  pgpfac1lem3a  20143  ablfaclem3  20154  fincygsubgd  20178  fincygsubgodd  20179  znrrg  21715  psdpw  22333  cayhamlem1  23023  caublcls  25468  ovolicc2lem4  25679  iundisj2  25708  volsup  25715  uniioombllem3  25744  mbfi1fseqlem3  25876  mbfi1fseqlem4  25877  elqaalem2  26481  aalioulem1  26495  aalioulem4  26498  aalioulem5  26499  aalioulem6  26500  aaliou  26501  aaliou3lem1  26505  aaliou3lem2  26506  aaliou3lem3  26507  aaliou3lem8  26508  aaliou3lem5  26510  aaliou3lem6  26511  aaliou3lem7  26512  taylthlem2  26537  cxpeq  26922  zrtelqelz  26923  amgmlem  27154  lgamgulmlem4  27196  lgamcvg2  27219  wilthlem2  27233  wilth  27235  wilthimp  27236  ftalem5  27241  basellem2  27246  basellem3  27247  basellem4  27248  basellem5  27249  muval1  27297  dvdssqf  27302  sgmnncl  27311  efchtdvds  27323  mumullem2  27344  mumul  27345  sqff1o  27346  fsumdvdsdiaglem  27347  dvdsppwf1o  27350  dvdsflf1o  27351  muinv  27357  mpodvdsmulf1o  27358  dvdsmulf1o  27360  chtublem  27375  fsumvma2  27378  vmasum  27380  chpchtsum  27383  logfacubnd  27385  mersenne  27391  perfect1  27392  perfectlem1  27393  perfectlem2  27394  perfect  27395  dchrelbas4  27407  dchrfi  27419  bcmono  27441  bcp1ctr  27443  bclbnd  27444  bposlem1  27448  bposlem3  27450  bposlem5  27452  bposlem6  27453  bposlem9  27456  lgsmod  27487  lgsdir  27496  lgsdilem2  27497  lgsne0  27499  lgsqrlem2  27511  lgsqr  27515  lgsqrmodndvds  27517  gausslemma2dlem0c  27522  gausslemma2dlem0h  27527  gausslemma2dlem0i  27528  gausslemma2dlem2  27531  gausslemma2dlem6  27536  gausslemma2dlem7  27537  gausslemma2d  27538  lgseisenlem1  27539  lgseisenlem2  27540  lgseisenlem3  27541  lgseisenlem4  27542  lgsquadlem1  27544  lgsquadlem2  27545  lgsquadlem3  27546  lgsquad2lem1  27548  lgsquad2lem2  27549  lgsquad2  27550  m1lgs  27552  2lgslem2  27559  2sqlem3  27584  2sqlem4  27585  2sqlem8  27590  chebbnd1lem1  27633  rplogsumlem2  27649  rpvmasumlem  27651  dchrisumlem1  27653  dchrisumlem2  27654  dchrisumlem3  27655  dchrisum0fmul  27670  dchrisum0ff  27671  dchrisum0flblem1  27672  dchrisum0flblem2  27673  dchrisum0flb  27674  dchrisum0  27684  pntrsumbnd2  27731  pntrlog2bndlem1  27741  pntrlog2bndlem6  27747  pntpbnd2  27751  pntlemg  27762  pntlemj  27767  pntlemf  27769  ostth2lem2  27798  ostth2lem3  27799  ostth3  27802  numclwlk2lem2f1o  30730  nrt2irr  30824  minvecolem4  31232  iundisj2f  32935  ssnnssfz  33132  iundisj2fi  33142  f1ocnt  33145  elq2  33156  numdenneg  33159  expgt0b  33161  ltesubnnd  33167  oexpled  33180  psgnfzto1stlem  33420  isarchi3  33507  archiabllem1b  33512  zringfrac  33844  fldextrspundgdvds  34071  cos9thpiminplylem2  34173  smatrcl  34186  1smat1  34194  submateqlem1  34197  lmatfvlem  34205  qqhval2  34372  qqhf  34376  qqhghm  34378  qqhrhm  34379  qqhnm  34380  qqhre  34410  esumcvg  34476  meascnbl  34609  omssubadd  34690  oddpwdc  34744  ballotlemfp1  34882  ballotlemfc0  34883  ballotlemfcc  34884  ballotlemimin  34896  ballotlemic  34897  ballotlem1c  34898  hgt750lemc  35034  hgt750lemd  35035  hgt750lemb  35043  hgt750leme  35045  subfaclim  35680  cvmliftlem7  35783  sinccvglem  36164  bcprod  36230  bccolsum  36231  faclimlem2  36236  faclim2  36240  poimirlem1  38272  poimirlem2  38273  poimirlem3  38274  poimirlem4  38275  poimirlem6  38277  poimirlem8  38279  poimirlem9  38280  poimirlem10  38281  poimirlem11  38282  poimirlem13  38284  poimirlem14  38285  poimirlem15  38286  poimirlem16  38287  poimirlem17  38288  poimirlem18  38289  poimirlem19  38290  poimirlem20  38291  poimirlem21  38292  poimirlem22  38293  poimirlem23  38294  poimirlem24  38295  poimirlem26  38297  poimirlem27  38298  poimirlem28  38299  poimirlem31  38302  mblfinlem2  38309  seqpo  38398  incsequz  38399  incsequz2  38400  zndvdchrrhm  42740  bccl2d  42758  nnproddivdvdsd  42767  lcmineqlem1  42796  lcmineqlem3  42798  lcmineqlem4  42799  lcmineqlem6  42801  lcmineqlem8  42803  lcmineqlem9  42804  lcmineqlem10  42805  lcmineqlem11  42806  lcmineqlem13  42808  lcmineqlem14  42809  lcmineqlem18  42813  lcmineqlem19  42814  lcmineqlem20  42815  lcmineqlem21  42816  lcmineqlem22  42817  lcmineqlem23  42818  lcmineqlem  42819  3lexlogpow5ineq2  42822  3lexlogpow2ineq1  42825  aks4d1p3  42845  aks4d1p5  42847  aks4d1p6  42848  aks4d1p8d1  42851  aks4d1p8d2  42852  aks4d1p8d3  42853  aks4d1p8  42854  aks4d1p9  42855  posbezout  42867  primrootscoprbij  42869  remexz  42871  primrootspoweq0  42873  aks6d1c1  42883  aks6d1c2p2  42886  hashscontpow1  42888  hashscontpow  42889  aks6d1c3  42890  aks6d1c4  42891  aks6d1c2lem4  42894  aks6d1c2  42897  aks6d1c5lem1  42903  sticksstones6  42918  sticksstones10  42922  sticksstones12a  42924  sticksstones12  42925  aks6d1c6lem3  42939  aks6d1c6lem4  42940  aks6d1c6isolem3  42943  aks6d1c6lem5  42944  aks6d1c7lem2  42948  aks6d1c7  42951  aks5lem1  42953  aks5lem2  42954  aks5lem3a  42956  grpods  42961  unitscyglem1  42962  unitscyglem2  42963  unitscyglem4  42965  unitscyglem5  42966  aks5  42971  sumcubes  43074  oexpreposd  43083  explt1d  43084  expeq1d  43085  expeqidd  43086  exp11d  43087  gcdle1d  43091  gcdle2d  43092  dvdsexpnn0  43095  fimgmcyc  43302  fltdvdsabdvdsc  43370  fltaccoprm  43372  fltbccoprm  43373  fltabcoprm  43374  fltne  43376  flt4lem2  43379  flt4lem3  43380  flt4lem4  43381  flt4lem5  43382  flt4lem5elem  43383  flt4lem5a  43384  flt4lem5b  43385  flt4lem5c  43386  flt4lem5d  43387  flt4lem5e  43388  flt4lem5f  43389  flt4lem6  43390  flt4lem7  43391  nna4b4nsq  43392  fltltc  43393  fltnlta  43395  irrapxlem3  43551  irrapxlem5  43553  pellexlem5  43560  pellexlem6  43561  pellex  43562  pell1234qrmulcl  43582  jm2.23  43723  jm2.20nn  43724  jm2.26lem3  43728  jm2.27a  43732  jm2.27b  43733  jm2.27c  43734  jm3.1lem1  43744  jm3.1lem3  43746  inductionexd  44881  nznngen  45026  hashnzfz2  45031  fmuldfeq  46299  divcnvg  46343  stoweidlem1  46715  stoweidlem3  46717  stoweidlem11  46725  stoweidlem20  46734  stoweidlem26  46740  stoweidlem34  46748  stoweidlem51  46765  stirlinglem4  46791  stirlinglem5  46792  stirlinglem8  46795  dirkerper  46810  dirkertrigeqlem2  46813  dirkertrigeqlem3  46814  dirkercncflem2  46818  fourierdlem11  46832  fourierdlem14  46835  fourierdlem20  46841  fourierdlem25  46846  fourierdlem37  46858  fourierdlem41  46862  fourierdlem48  46868  fourierdlem49  46869  fourierdlem54  46874  fourierdlem64  46884  fourierdlem73  46893  fourierdlem79  46899  fourierdlem92  46912  fourierdlem93  46913  fourierdlem111  46931  sqwvfourb  46943  etransclem3  46951  etransclem7  46955  etransclem10  46958  etransclem15  46963  etransclem24  46972  etransclem25  46973  etransclem26  46974  etransclem27  46975  etransclem28  46976  etransclem35  46983  etransclem37  46985  etransclem38  46986  etransclem41  46989  etransclem44  46992  etransclem45  46993  etransclem48  46996  ovnsubaddlem1  47284  vonioolem1  47394  facnn0dvdsfac  48122  muldvdsfacgt  48123  muldvdsfacm1  48124  iccpartgtprec  48169  iccpartipre  48170  fmtnoodd  48285  goldbachthlem2  48298  goldbachth  48299  odz2prm2pw  48315  fmtnoprmfac1lem  48316  fmtnoprmfac2lem1  48318  fmtnoprmfac2  48319  fmtnofac2lem  48320  2pwp1prm  48341  lighneallem1  48357  lighneallem4  48362  proththdlem  48365  proththd  48366  nprmdvdsfacm1lem4  48375  ppivalnnprm  48377  ppivalnnnprmge6  48378  divgcdoddALTV  48447  perfectALTVlem1  48486  perfectALTVlem2  48487  perfectALTV  48488  gbowge7  48528  gpgedgvtx1  48827  gpg3kgrtriexlem2  48849  gpg3kgrtriexlem5  48852  pw2m1lepw2m1  49300  nnolog2flm1  49370  dignn0fr  49381  dignn0flhalflem1  49395