Theorem nn0zd 9437

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 9335	. 2 ⊢ ℕ0 ⊆ ℤ
2		nn0zd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3177	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2164  ℕ₀cn0 9240  ℤcz 9317

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 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-1cn 7965  ax-1re 7966  ax-icn 7967  ax-addcl 7968  ax-addrcl 7969  ax-mulcl 7970  ax-addcom 7972  ax-addass 7974  ax-distr 7976  ax-i2m1 7977  ax-0lt1 7978  ax-0id 7980  ax-rnegex 7981  ax-cnre 7983  ax-pre-ltirr 7984  ax-pre-ltwlin 7985  ax-pre-lttrn 7986  ax-pre-ltadd 7988

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 2986  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-br 4030  df-opab 4091  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-iota 5215  df-fun 5256  df-fv 5262  df-riota 5873  df-ov 5921  df-oprab 5922  df-mpo 5923  df-pnf 8056  df-mnf 8057  df-xr 8058  df-ltxr 8059  df-le 8060  df-sub 8192  df-neg 8193  df-inn 8983  df-n0 9241  df-z 9318

This theorem is referenced by:  nnzd  9438  xnn0dcle  9868  xnn0letri  9869  fseq1p1m1  10160  difelfznle  10201  flltdivnn0lt  10373  zmodfz  10417  addmodid  10443  modaddmodup  10458  modaddmodlo  10459  modsumfzodifsn  10467  addmodlteq  10469  expnegzap  10644  expaddzaplem  10653  expaddzap  10654  expmulzap  10656  nn0ltexp2  10780  nn0opthd  10793  facdiv  10809  facwordi  10811  faclbnd  10812  facavg  10817  bcval  10820  bcval5  10834  bcpasc  10837  hashfiv01gt1  10853  isfinite4im  10863  fihashneq0  10865  fseq1hash  10872  fnfz0hash  10903  ffzo0hash  10905  zfz1isolemiso  10910  wrdfin  10933  wrdffz  10935  wrdsymb0  10946  wrdlenge1n0  10947  resqrexlemga  11167  zabscl  11230  fsum0diaglem  11583  modfsummodlemstep  11600  binomlem  11626  binom1p  11628  binom1dif  11630  arisum2  11642  geosergap  11649  geoserap  11650  pwm1geoserap1  11651  geolim2  11655  cvgratnnlemrate  11673  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  efcvgfsum  11810  efaddlem  11817  dvdsdc  11941  divalglemnn  12059  divalgmod  12068  zeqzmulgcd  12107  gcd0id  12116  gcdneg  12119  gcdaddm  12121  modgcd  12128  gcdmultipled  12130  bezoutlemnewy  12133  bezoutlemstep  12134  bezoutlemmain  12135  bezoutlemzz  12139  bezoutlemmo  12143  bezoutlemle  12145  bezoutlemsup  12146  dfgcd3  12147  dvdsgcdb  12150  gcdass  12152  mulgcd  12153  gcdzeq  12159  dvdsmulgcd  12162  bezoutr  12169  bezoutr1  12170  nn0seqcvgd  12179  algfx  12190  eucalgval2  12191  eucalginv  12194  eucalglt  12195  eucalg  12197  gcddvdslcm  12211  lcmneg  12212  lcmgcdlem  12215  lcmdvds  12217  lcmgcdeq  12221  lcmdvdsb  12222  lcmass  12223  mulgcddvds  12232  rpmulgcd2  12233  qredeu  12235  divgcdcoprm0  12239  divgcdcoprmex  12240  cncongr1  12241  cncongr2  12242  sqnprm  12274  rpexp  12291  sqpweven  12313  2sqpwodd  12314  divnumden  12334  phivalfi  12350  phicl2  12352  phiprmpw  12360  crth  12362  phimullem  12363  eulerthlemfi  12366  eulerthlema  12368  hashgcdeq  12377  phisum  12378  odzdvds  12383  powm2modprm  12390  coprimeprodsq  12395  pcprendvds  12428  pcpremul  12431  pceu  12433  pcdiv  12440  pcqcl  12444  pcdvdsb  12458  pc2dvds  12468  pcprmpw2  12471  dvdsprmpweqle  12475  pcadd  12478  fldivp1  12486  pcfaclem  12487  pcfac  12488  pcbc  12489  pockthlem  12494  1arith  12505  mul4sqlem  12531  4sqlemafi  12533  4sqlemffi  12534  4sqleminfi  12535  4sqexercise1  12536  4sqlemsdc  12538  4sqlem11  12539  4sqlem12  12540  4sqlem14  12542  ennnfoneleminc  12568  ennnfonelemrnh  12573  ennnfonelemim  12581  znunit  14147  psrbaglesuppg  14158  elply2  14881  plyf  14883  elplyd  14887  ply1termlem  14888  ply1term  14889  plyaddlem1  14893  plymullem1  14894  plyaddlem  14895  wilthlem1  15112  lgsval  15120  lgsfvalg  15121  lgsfcl2  15122  lgsval2lem  15126  lgsmod  15142  lgsdir2  15149  lgsne0  15154  lgsprme0  15158  gausslemma2dlem0h  15172  gausslemma2dlem0i  15173  gausslemma2dlem2  15178  gausslemma2dlem6  15183  gausslemma2d  15185  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  lgsquadlem1  15191  m1lgs  15192  2lgsoddprmlem2  15194  2sqlem8  15210  nninffeq  15510