Theorem nnzd 9767

Description: A nonnegative 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 9620	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	2	nn0zd 9766	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℕcn 9304  ℤcz 9644

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-cnex 8270  ax-resscn 8271  ax-1cn 8272  ax-1re 8273  ax-icn 8274  ax-addcl 8275  ax-addrcl 8276  ax-mulcl 8277  ax-addcom 8279  ax-addass 8281  ax-distr 8283  ax-i2m1 8284  ax-0lt1 8285  ax-0id 8287  ax-rnegex 8288  ax-cnre 8290  ax-pre-ltirr 8291  ax-pre-ltwlin 8292  ax-pre-lttrn 8293  ax-pre-ltadd 8295

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4131  df-opab 4193  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-iota 5337  df-fun 5379  df-fv 5385  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-pnf 8362  df-mnf 8363  df-xr 8364  df-ltxr 8365  df-le 8366  df-sub 8499  df-neg 8500  df-inn 9305  df-n0 9564  df-z 9645

This theorem is used by:  qapne  10039  ltesubnnd  10170  qtri3or  10675  exbtwnzlemstep  10682  modifeq2int  10823  modsumfzodifsn  10833  addmodlteq  10835  expnnval  10979  expnegap0  10984  expaddzaplem  11019  expmulzap  11022  facndiv  11177  bcval  11187  bcval5  11201  bcpasc  11204  hashf1  11287  caucvgre  11747  cvg1nlemcau  11750  cvg1nlemres  11751  resqrexlemdecn  11778  resqrexlemnmsq  11783  resqrexlemnm  11784  resqrexlemcvg  11785  resqrexlemoverl  11787  sumeq2  12125  nnf1o  12143  summodclem3  12147  summodclem2a  12148  summodclem2  12149  summodc  12150  zsumdc  12151  fsum3  12154  fisumss  12159  fsum3cvg3  12163  fsumcl2lem  12165  fsumadd  12173  sumsnf  12176  fsummulc2  12215  bcxmas  12256  geo2lim  12283  cvgratnnlembern  12290  cvgratnnlemseq  12293  cvgratnnlemabsle  12294  cvgratnnlemsumlt  12295  cvgratnnlemfm  12296  cvgratnnlemrate  12297  cvgratz  12299  mertenslemub  12301  mertenslemi1  12302  mertenslem2  12303  prodeq2  12324  prodmodclem3  12342  prodmodclem2a  12343  prodmodclem2  12344  fprodseq  12350  fprodssdc  12357  fprodmul  12358  prodsnf  12359  eftcl  12421  eftlub  12457  eirraplem  12544  dvdsle  12611  fzm1ndvds  12623  dvdsfac  12627  dvdsmod  12629  divalglemeunn  12688  bitsfzolem  12721  bitsmod  12723  bitsfi  12724  bitscmp  12725  bitsinv1  12729  gcddvds  12740  gcdnncl  12744  gcd1  12764  dvdsgcdidd  12771  bezoutlemnewy  12773  bezoutlemstep  12774  mulgcd  12793  gcdmultiplez  12798  rplpwr  12804  rppwr  12805  sqgcd  12806  dvdssq  12808  uzwodc  12814  lcmneg  12852  lcmgcdlem  12855  ncoprmgcdne1b  12867  rpdvds  12877  congr  12878  cncongr1  12881  cncongr2  12882  prmz  12889  prmind2  12898  divgcdodd  12921  isprm6  12925  prmexpb  12929  prmfac1  12930  rpexp  12931  sqrt2irrlem  12939  pw2dvdslemn  12943  pw2dvdseulemle  12945  oddpwdclemxy  12947  oddpwdclemodd  12950  sqpweven  12953  2sqpwodd  12954  sqrt2irraplemnn  12957  numdensq  12980  phivalfi  12990  hashdvds  12999  phiprmpw  13000  crth  13002  phimullem  13003  eulerthlem1  13005  eulerthlemfi  13006  eulerthlemrprm  13007  eulerthlema  13008  eulerthlemh  13009  eulerthlemth  13010  eulerth  13011  prmdivdiv  13015  hashgcdlem  13016  hashgcdeq  13018  phisum  13019  odzdvds  13024  powm2modprm  13031  pythagtriplem2  13045  pythagtriplem4  13047  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem11  13053  pythagtriplem13  13055  pythagtriplem16  13058  pythagtriplem19  13061  pythagtrip  13062  pclemub  13066  pcprendvds2  13070  pcpre1  13071  pcpremul  13072  pceulem  13073  pcqmul  13082  pcdvdsb  13099  pcidlem  13102  pcdvdstr  13106  pcgcd1  13107  pc2dvds  13109  pcprmpw2  13112  pcaddlem  13118  pcadd  13119  pcmpt  13122  pcmpt2  13123  pcmptdvds  13124  pcprod  13125  pcfac  13129  pcbc  13130  qexpz  13131  oddprmdvds  13133  prmpwdvds  13134  pockthlem  13135  pockthg  13136  infpnlem2  13139  1arithlem4  13145  1arith  13146  4sqlem5  13161  4sqlem6  13162  4sqlem8  13164  4sqlem9  13165  4sqlem10  13166  4sqlemafi  13174  4sqlemffi  13175  4sqleminfi  13176  4sqlem11  13180  4sqlem12  13181  4sqlem14  13183  4sqlem16  13185  4sqlem17  13186  ballotfilemfp1  13231  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemimin  13249  ballotfilemic  13250  ballotfilem1c  13251  oddennn  13283  exmidunben  13317  nninfdclemcl  13339  nninfdclemp1  13341  nninfdclemlt  13342  unbendc  13345  bassetsnn  13409  strleund  13457  gzsumwsubmcl  13801  gzsumwmhm  13803  mulgneg  13943  mulgnndir  13954  znrrg  14995  logbgcd1irraplemexp  16070  logbgcd1irraplemap  16071  sgmnncl  16102  dvdsppwf1o  16103  mpodvdsmulf1o  16104  mersenne  16111  perfect1  16112  perfectlem1  16113  perfectlem2  16114  perfect  16115  lgsfvalg  16124  lgsfcl2  16125  lgsmod  16145  lgsdir  16154  lgsdilem2  16155  lgsne0  16157  gausslemma2dlem0c  16170  gausslemma2dlem0d  16171  gausslemma2dlem0h  16175  gausslemma2dlem0i  16176  gausslemma2dlem1  16180  gausslemma2dlem2  16181  gausslemma2dlem3  16182  gausslemma2dlem4  16183  gausslemma2dlem5a  16184  gausslemma2dlem5  16185  gausslemma2dlem6  16186  gausslemma2dlem7  16187  gausslemma2d  16188  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgseisen  16193  lgsquadlemsfi  16194  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad2lem1  16200  lgsquad2lem2  16201  lgsquad2  16202  lgsquad3  16203  m1lgs  16204  2lgslem1  16210  2lgslem2  16211  2sqlem3  16236  2sqlem4  16237  2sqlem8  16242  2sqlem9  16243  cvgcmp2nlemabs  17081  trilpolemclim  17085  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  nconstwlpolemgt0  17114