Theorem nn0zd 9440

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

Hypothesis

Ref	Expression
nn0zd.1	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Assertion

Ref	Expression
nn0zd	⊢ (𝜑 → 𝐴 ∈ ℤ)

Proof of Theorem nn0zd

Step	Hyp	Ref	Expression
1		nn0ssz 9338	. 2 ⊢ ℕ0 ⊆ ℤ
2		nn0zd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3178	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2164  ℕ₀cn0 9243  ℤcz 9320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465  ax-setind 4570  ax-cnex 7965  ax-resscn 7966  ax-1cn 7967  ax-1re 7968  ax-icn 7969  ax-addcl 7970  ax-addrcl 7971  ax-mulcl 7972  ax-addcom 7974  ax-addass 7976  ax-distr 7978  ax-i2m1 7979  ax-0lt1 7980  ax-0id 7982  ax-rnegex 7983  ax-cnre 7985  ax-pre-ltirr 7986  ax-pre-ltwlin 7987  ax-pre-lttrn 7988  ax-pre-ltadd 7990

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2987  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-int 3872  df-br 4031  df-opab 4092  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-iota 5216  df-fun 5257  df-fv 5263  df-riota 5874  df-ov 5922  df-oprab 5923  df-mpo 5924  df-pnf 8058  df-mnf 8059  df-xr 8060  df-ltxr 8061  df-le 8062  df-sub 8194  df-neg 8195  df-inn 8985  df-n0 9244  df-z 9321

This theorem is referenced by:  nnzd  9441  xnn0dcle  9871  xnn0letri  9872  fseq1p1m1  10163  difelfznle  10204  flltdivnn0lt  10376  zmodfz  10420  addmodid  10446  modaddmodup  10461  modaddmodlo  10462  modsumfzodifsn  10470  addmodlteq  10472  expnegzap  10647  expaddzaplem  10656  expaddzap  10657  expmulzap  10659  nn0ltexp2  10783  nn0opthd  10796  facdiv  10812  facwordi  10814  faclbnd  10815  facavg  10820  bcval  10823  bcval5  10837  bcpasc  10840  hashfiv01gt1  10856  isfinite4im  10866  fihashneq0  10868  fseq1hash  10875  fnfz0hash  10906  ffzo0hash  10908  zfz1isolemiso  10913  wrdfin  10936  wrdffz  10938  wrdsymb0  10949  wrdlenge1n0  10950  resqrexlemga  11170  zabscl  11233  fsum0diaglem  11586  modfsummodlemstep  11603  binomlem  11629  binom1p  11631  binom1dif  11633  arisum2  11645  geosergap  11652  geoserap  11653  pwm1geoserap1  11654  geolim2  11658  cvgratnnlemrate  11676  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  efcvgfsum  11813  efaddlem  11820  dvdsdc  11944  divalglemnn  12062  divalgmod  12071  zeqzmulgcd  12110  gcd0id  12119  gcdneg  12122  gcdaddm  12124  modgcd  12131  gcdmultipled  12133  bezoutlemnewy  12136  bezoutlemstep  12137  bezoutlemmain  12138  bezoutlemzz  12142  bezoutlemmo  12146  bezoutlemle  12148  bezoutlemsup  12149  dfgcd3  12150  dvdsgcdb  12153  gcdass  12155  mulgcd  12156  gcdzeq  12162  dvdsmulgcd  12165  bezoutr  12172  bezoutr1  12173  nn0seqcvgd  12182  algfx  12193  eucalgval2  12194  eucalginv  12197  eucalglt  12198  eucalg  12200  gcddvdslcm  12214  lcmneg  12215  lcmgcdlem  12218  lcmdvds  12220  lcmgcdeq  12224  lcmdvdsb  12225  lcmass  12226  mulgcddvds  12235  rpmulgcd2  12236  qredeu  12238  divgcdcoprm0  12242  divgcdcoprmex  12243  cncongr1  12244  cncongr2  12245  sqnprm  12277  rpexp  12294  sqpweven  12316  2sqpwodd  12317  divnumden  12337  phivalfi  12353  phicl2  12355  phiprmpw  12363  crth  12365  phimullem  12366  eulerthlemfi  12369  eulerthlema  12371  hashgcdeq  12380  phisum  12381  odzdvds  12386  powm2modprm  12393  coprimeprodsq  12398  pcprendvds  12431  pcpremul  12434  pceu  12436  pcdiv  12443  pcqcl  12447  pcdvdsb  12461  pc2dvds  12471  pcprmpw2  12474  dvdsprmpweqle  12478  pcadd  12481  fldivp1  12489  pcfaclem  12490  pcfac  12491  pcbc  12492  pockthlem  12497  1arith  12508  mul4sqlem  12534  4sqlemafi  12536  4sqlemffi  12537  4sqleminfi  12538  4sqexercise1  12539  4sqlemsdc  12541  4sqlem11  12542  4sqlem12  12543  4sqlem14  12545  ennnfoneleminc  12571  ennnfonelemrnh  12576  ennnfonelemim  12584  znunit  14158  psrbaglesuppg  14169  elply2  14914  plyf  14916  elplyd  14920  ply1termlem  14921  ply1term  14922  plyaddlem1  14926  plymullem1  14927  plyaddlem  14928  plycolemc  14936  plycjlemc  14938  plycn  14940  plyrecj  14941  dvply1  14943  wilthlem1  15153  lgsval  15161  lgsfvalg  15162  lgsfcl2  15163  lgsval2lem  15167  lgsmod  15183  lgsdir2  15190  lgsne0  15195  lgsprme0  15199  gausslemma2dlem0h  15213  gausslemma2dlem0i  15214  gausslemma2dlem2  15219  gausslemma2dlem6  15224  gausslemma2d  15226  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgsquadlem1  15234  lgsquadlem2  15235  m1lgs  15242  2lgslem1a  15245  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2lgslem3d1  15257  2lgs  15261  2lgsoddprmlem2  15263  2lgsoddprm  15270  2sqlem8  15280  nninffeq  15580