Theorem nnzd 8792

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 8651	. 2 |- ( ph -> A e. NN0 )
3	2	nn0zd 8791	1 |- ( ph -> A e. ZZ )

Syntax hints:   -> wi 4   e. wcel 1436   NNcn 8349   ZZcz 8675

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3930  ax-pow 3982  ax-pr 4008  ax-un 4232  ax-setind 4324  ax-cnex 7372  ax-resscn 7373  ax-1cn 7374  ax-1re 7375  ax-icn 7376  ax-addcl 7377  ax-addrcl 7378  ax-mulcl 7379  ax-addcom 7381  ax-addass 7383  ax-distr 7385  ax-i2m1 7386  ax-0lt1 7387  ax-0id 7389  ax-rnegex 7390  ax-cnre 7392  ax-pre-ltirr 7393  ax-pre-ltwlin 7394  ax-pre-lttrn 7395  ax-pre-ltadd 7397

This theorem depends on definitions:  df-bi 115  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-nel 2347  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2617  df-sbc 2830  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-pw 3416  df-sn 3436  df-pr 3437  df-op 3439  df-uni 3636  df-int 3671  df-br 3820  df-opab 3874  df-id 4092  df-xp 4415  df-rel 4416  df-cnv 4417  df-co 4418  df-dm 4419  df-iota 4942  df-fun 4979  df-fv 4985  df-riota 5562  df-ov 5609  df-oprab 5610  df-mpt2 5611  df-pnf 7460  df-mnf 7461  df-xr 7462  df-ltxr 7463  df-le 7464  df-sub 7591  df-neg 7592  df-inn 8350  df-n0 8599  df-z 8676

This theorem is referenced by:  qapne  9048  qtri3or  9574  exbtwnzlemstep  9579  modifeq2int  9713  modsumfzodifsn  9723  addmodlteq  9725  expnegap0  9853  expaddzaplem  9888  expmulzap  9891  facndiv  10035  bcval  10045  ibcval5  10059  bcpasc  10062  caucvgre  10301  cvg1nlemcau  10304  cvg1nlemres  10305  resqrexlemdecn  10332  resqrexlemnmsq  10337  resqrexlemnm  10338  resqrexlemcvg  10339  resqrexlemoverl  10341  sumeq2  10630  isummolemnm  10650  isummolem3  10651  isummolem2a  10652  isummolem2  10653  isummo  10654  zisum  10655  fisum  10657  dvdsle  10711  fzm1ndvds  10723  dvdsfac  10727  dvdsmod  10729  divalglemeunn  10787  gcddvds  10821  gcdnncl  10825  gcd1  10844  bezoutlemnewy  10851  bezoutlemstep  10852  mulgcd  10871  gcdmultiplez  10876  rplpwr  10882  rppwr  10883  sqgcd  10884  dvdssq  10886  lcmneg  10922  lcmgcdlem  10925  ncoprmgcdne1b  10937  rpdvds  10947  congr  10948  cncongr1  10951  cncongr2  10952  prmz  10959  prmind2  10968  divgcdodd  10988  isprm6  10992  prmexpb  10996  prmfac1  10997  rpexp  10998  sqrt2irrlem  11006  pw2dvdslemn  11009  pw2dvdseulemle  11011  oddpwdclemxy  11013  oddpwdclemodd  11016  sqpweven  11019  2sqpwodd  11020  sqrt2irraplemnn  11023  numdensq  11046  phivalfi  11054  hashdvds  11063  phiprmpw  11064  crth  11066  phimullem  11067  hashgcdlem  11069  hashgcdeq  11070  oddennn  11071