Theorem nnzd 11481

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

Hypothesis

Ref	Expression
nnzd.1	|- ( ph -> A e. NN )

Assertion

Ref	Expression
nnzd	|- ( ph -> A e. ZZ )

Proof of Theorem nnzd

Step	Hyp	Ref	Expression
1		nnzd.1	. . 3 |- ( ph -> A e. NN )
2	1	nnnn0d 11351	. 2 |- ( ph -> A e. NN0 )
3	2	nn0zd 11480	1 |- ( ph -> A e. ZZ )

Syntax hints:   -> wi 4   e. wcel 1990   NNcn 11020   ZZcz 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378

This theorem is referenced by:  expaddzlem  12903  expmulz  12906  expmulnbnd  12996  facndiv  13075  bcval5  13105  bcpasc  13108  hashf1  13241  isercolllem1  14395  isercolllem2  14396  o1fsum  14545  bcxmas  14567  climcndslem2  14582  climcnds  14583  mertenslem1  14616  fprodser  14679  bpolydiflem  14785  eftlub  14839  eirrlem  14932  rpnnen2lem7  14949  rpnnen2lem9  14951  rpnnen2lem11  14953  sqrt2irrlem  14977  sqrt2irrlemOLD  14978  dvdsfac  15048  dvdsmod  15050  oddpwp1fsum  15115  bitsfzolem  15156  bitsmod  15158  bitsfi  15159  bitscmp  15160  bitsinv1  15164  sadadd3  15183  sadaddlem  15188  bitsuz  15196  bitsshft  15197  gcdnncl  15229  gcd1  15249  bezoutlem3  15258  bezoutlem4  15259  mulgcd  15265  gcdmultiplez  15270  rplpwr  15276  rppwr  15277  sqgcd  15278  dvdssq  15280  lcmneg  15316  lcmgcdlem  15319  rpdvds  15374  coprmprod  15375  coprmproddvdslem  15376  congr  15378  cncongr1  15381  cncongr2  15382  prmz  15389  prmind2  15398  divgcdodd  15422  isprm6  15426  prmexpb  15430  prmfac1  15431  rpexp  15432  numdensq  15462  hashdvds  15480  phiprmpw  15481  crth  15483  phimullem  15484  eulerthlem1  15486  eulerthlem2  15487  prmdivdiv  15492  hashgcdlem  15493  odzdvds  15500  pythagtriplem4  15524  pythagtriplem6  15526  pythagtriplem7  15527  pythagtriplem11  15530  pythagtriplem13  15532  pythagtriplem19  15538  pclem  15543  pcprendvds2  15546  pcpre1  15547  pcpremul  15548  pceulem  15550  pcqmul  15558  pcdvdsb  15573  pcidlem  15576  pcdvdstr  15580  pcgcd1  15581  pc2dvds  15583  pcprmpw2  15586  pcaddlem  15592  pcadd  15593  pcmpt2  15597  pcmptdvds  15598  pcfac  15603  pcbc  15604  qexpz  15605  oddprmdvds  15607  prmpwdvds  15608  pockthlem  15609  pockthg  15610  prmreclem2  15621  prmreclem3  15622  prmreclem4  15623  prmreclem5  15624  prmreclem6  15625  4sqlem5  15646  4sqlem8  15649  4sqlem9  15650  4sqlem10  15651  4sqlem12  15660  4sqlem14  15662  4sqlem16  15664  4sqlem17  15665  vdwlem1  15685  vdwlem2  15686  vdwlem3  15687  vdwlem6  15690  vdwlem9  15693  vdwlem10  15694  vdwnnlem3  15701  prmdvdsprmop  15747  prmolelcmf  15752  prmgaplem1  15753  prmgaplem7  15761  prmgaplem8  15762  gsumwsubmcl  17375  gsumccat  17378  gsumwmhm  17382  mulgneg  17560  mulgnndir  17569  mulgnndirOLD  17570  psgnunilem4  17917  odlem2  17958  mndodconglem  17960  odmod  17965  gexlem2  17997  gexcl3  18002  gexcl2  18004  sylow1lem1  18013  sylow1lem3  18015  sylow1lem5  18017  pgpfi  18020  fislw  18040  sylow3lem4  18045  gexexlem  18255  ablfacrplem  18464  ablfacrp  18465  ablfacrp2  18466  ablfac1lem  18467  ablfac1b  18469  ablfac1eu  18472  pgpfac1lem3a  18475  ablfaclem3  18486  znrrg  19914  cayhamlem1  20671  caublcls  23107  ovolicc2lem4  23288  iundisj2  23317  volsup  23324  uniioombllem3  23353  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  elqaalem2  24075  aalioulem1  24087  aalioulem4  24090  aalioulem5  24091  aalioulem6  24092  aaliou  24093  aaliou3lem1  24097  aaliou3lem2  24098  aaliou3lem3  24099  aaliou3lem8  24100  aaliou3lem5  24102  aaliou3lem6  24103  aaliou3lem7  24104  taylthlem2  24128  cxpeq  24498  amgmlem  24716  lgamgulmlem4  24758  lgamcvg2  24781  wilthlem2  24795  wilth  24797  wilthimp  24798  ftalem5  24803  basellem2  24808  basellem3  24809  basellem4  24810  basellem5  24811  muval1  24859  dvdssqf  24864  sgmnncl  24873  efchtdvds  24885  mumullem2  24906  mumul  24907  sqff1o  24908  fsumdvdsdiaglem  24909  dvdsppwf1o  24912  dvdsflf1o  24913  muinv  24919  dvdsmulf1o  24920  chtublem  24936  fsumvma2  24939  vmasum  24941  chpchtsum  24944  logfacubnd  24946  mersenne  24952  perfect1  24953  perfectlem1  24954  perfectlem2  24955  perfect  24956  dchrelbas4  24968  dchrfi  24980  bcmono  25002  bcp1ctr  25004  bclbnd  25005  bposlem1  25009  bposlem3  25011  bposlem5  25013  bposlem6  25014  bposlem9  25017  lgsmod  25048  lgsdir  25057  lgsdilem2  25058  lgsne0  25060  lgsqrlem2  25072  lgsqr  25076  lgsqrmodndvds  25078  gausslemma2dlem0c  25083  gausslemma2dlem0h  25088  gausslemma2dlem0i  25089  gausslemma2dlem2  25092  gausslemma2dlem6  25097  gausslemma2dlem7  25098  gausslemma2d  25099  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgseisenlem4  25103  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  lgsquad2lem1  25109  lgsquad2lem2  25110  lgsquad2  25111  m1lgs  25113  2lgslem2  25120  2sqlem3  25145  2sqlem4  25146  2sqlem8  25151  chebbnd1lem1  25158  rplogsumlem2  25174  rpvmasumlem  25176  dchrisumlem1  25178  dchrisumlem2  25179  dchrisumlem3  25180  dchrisum0fmul  25195  dchrisum0ff  25196  dchrisum0flblem1  25197  dchrisum0flblem2  25198  dchrisum0flb  25199  dchrisum0  25209  pntrsumbnd2  25256  pntrlog2bndlem1  25266  pntrlog2bndlem6  25272  pntpbnd2  25276  pntlemg  25287  pntlemj  25292  pntlemf  25294  ostth2lem2  25323  ostth2lem3  25324  ostth3  25327  minvecolem4  27736  iundisj2f  29403  ssnnssfz  29549  iundisj2fi  29556  f1ocnt  29559  numdenneg  29563  ltesubnnd  29568  isarchi3  29741  archiabllem1b  29746  psgnfzto1stlem  29850  smatrcl  29862  1smat1  29870  submateqlem1  29873  submateqlem2  29874  lmatfvlem  29881  qqhval2  30026  qqhf  30030  qqhghm  30032  qqhrhm  30033  qqhnm  30034  qqhre  30064  esumcvg  30148  meascnbl  30282  omssubadd  30362  oddpwdc  30416  ballotlemfp1  30553  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemimin  30567  ballotlemic  30568  ballotlem1c  30569  hgt750lemc  30725  hgt750lemd  30726  hgt750lemb  30734  hgt750leme  30736  subfaclim  31170  cvmliftlem7  31273  sinccvglem  31566  bcprod  31624  bccolsum  31625  faclimlem2  31630  faclim2  31634  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem8  33417  poimirlem9  33418  poimirlem10  33419  poimirlem11  33420  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem31  33440  mblfinlem2  33447  seqpo  33543  incsequz  33544  incsequz2  33545  irrapxlem3  37388  irrapxlem5  37390  pellexlem5  37397  pellexlem6  37398  pellex  37399  pell1234qrmulcl  37419  jm2.23  37563  jm2.20nn  37564  jm2.26lem3  37568  jm2.27a  37572  jm2.27b  37573  jm2.27c  37574  jm3.1lem1  37584  jm3.1lem3  37586  inductionexd  38453  nznngen  38515  hashnzfz2  38520  fmuldfeq  39815  divcnvg  39859  stoweidlem1  40218  stoweidlem3  40220  stoweidlem11  40228  stoweidlem20  40237  stoweidlem26  40243  stoweidlem34  40251  stoweidlem51  40268  stirlinglem4  40294  stirlinglem5  40295  stirlinglem8  40298  dirkerper  40313  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkercncflem2  40321  fourierdlem11  40335  fourierdlem14  40338  fourierdlem20  40344  fourierdlem25  40349  fourierdlem37  40361  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem54  40377  fourierdlem64  40387  fourierdlem73  40396  fourierdlem79  40402  fourierdlem92  40415  fourierdlem93  40416  fourierdlem111  40434  sqwvfourb  40446  etransclem3  40454  etransclem7  40458  etransclem10  40461  etransclem15  40466  etransclem24  40475  etransclem25  40476  etransclem26  40477  etransclem27  40478  etransclem28  40479  etransclem35  40486  etransclem37  40488  etransclem38  40489  etransclem41  40492  etransclem44  40495  etransclem45  40496  etransclem48  40499  ovnsubaddlem1  40784  vonioolem1  40894  iccpartgtprec  41356  iccpartipre  41357  fmtnoodd  41445  goldbachthlem2  41458  goldbachth  41459  odz2prm2pw  41475  fmtnoprmfac1lem  41476  fmtnoprmfac2lem1  41478  fmtnoprmfac2  41479  fmtnofac2lem  41480  2pwp1prm  41503  lighneallem1  41522  lighneallem4  41527  proththdlem  41530  proththd  41531  divgcdoddALTV  41593  perfectALTVlem1  41630  perfectALTVlem2  41631  perfectALTV  41632  gbowge7  41651  pw2m1lepw2m1  42310  nnolog2flm1  42384  dignn0fr  42395  dignn0flhalflem1  42409