Theorem nnzd 8777

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

Syntax hints:   → wi 4   ∈ wcel 1436  ℕcn 8334  ℤcz 8660

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 3925  ax-pow 3977  ax-pr 4003  ax-un 4227  ax-setind 4319  ax-cnex 7357  ax-resscn 7358  ax-1cn 7359  ax-1re 7360  ax-icn 7361  ax-addcl 7362  ax-addrcl 7363  ax-mulcl 7364  ax-addcom 7366  ax-addass 7368  ax-distr 7370  ax-i2m1 7371  ax-0lt1 7372  ax-0id 7374  ax-rnegex 7375  ax-cnre 7377  ax-pre-ltirr 7378  ax-pre-ltwlin 7379  ax-pre-lttrn 7380  ax-pre-ltadd 7382

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 2616  df-sbc 2829  df-dif 2988  df-un 2990  df-in 2992  df-ss 2999  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-int 3666  df-br 3815  df-opab 3869  df-id 4087  df-xp 4410  df-rel 4411  df-cnv 4412  df-co 4413  df-dm 4414  df-iota 4937  df-fun 4974  df-fv 4980  df-riota 5550  df-ov 5597  df-oprab 5598  df-mpt2 5599  df-pnf 7445  df-mnf 7446  df-xr 7447  df-ltxr 7448  df-le 7449  df-sub 7576  df-neg 7577  df-inn 8335  df-n0 8584  df-z 8661

This theorem is referenced by:  qapne  9033  qtri3or  9557  exbtwnzlemstep  9562  modifeq2int  9696  modsumfzodifsn  9706  addmodlteq  9708  expnegap0  9814  expaddzaplem  9849  expmulzap  9852  facndiv  9996  bcval  10006  ibcval5  10020  bcpasc  10023  caucvgre  10255  cvg1nlemcau  10258  cvg1nlemres  10259  resqrexlemdecn  10286  resqrexlemnmsq  10291  resqrexlemnm  10292  resqrexlemcvg  10293  resqrexlemoverl  10295  sumeq2d  10584  sumeq2  10585  dvdsle  10639  fzm1ndvds  10651  dvdsfac  10655  dvdsmod  10657  divalglemeunn  10715  gcddvds  10749  gcdnncl  10753  gcd1  10772  bezoutlemnewy  10779  bezoutlemstep  10780  mulgcd  10799  gcdmultiplez  10804  rplpwr  10810  rppwr  10811  sqgcd  10812  dvdssq  10814  lcmneg  10850  lcmgcdlem  10853  ncoprmgcdne1b  10865  rpdvds  10875  congr  10876  cncongr1  10879  cncongr2  10880  prmz  10887  prmind2  10896  divgcdodd  10916  isprm6  10920  prmexpb  10924  prmfac1  10925  rpexp  10926  sqrt2irrlem  10934  pw2dvdslemn  10937  pw2dvdseulemle  10939  oddpwdclemxy  10941  oddpwdclemodd  10944  sqpweven  10947  2sqpwodd  10948  sqrt2irraplemnn  10951  numdensq  10974  phivalfi  10982  hashdvds  10991  phiprmpw  10992  crth  10994  phimullem  10995  hashgcdlem  10997  hashgcdeq  10998  oddennn  10999