Theorem nn0zd 9346

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

Syntax hints:   → wi 4   ∈ wcel 2146  ℕ₀cn0 9149  ℤcz 9226

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 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530  ax-cnex 7877  ax-resscn 7878  ax-1cn 7879  ax-1re 7880  ax-icn 7881  ax-addcl 7882  ax-addrcl 7883  ax-mulcl 7884  ax-addcom 7886  ax-addass 7888  ax-distr 7890  ax-i2m1 7891  ax-0lt1 7892  ax-0id 7894  ax-rnegex 7895  ax-cnre 7897  ax-pre-ltirr 7898  ax-pre-ltwlin 7899  ax-pre-lttrn 7900  ax-pre-ltadd 7902

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-nel 2441  df-ral 2458  df-rex 2459  df-reu 2460  df-rab 2462  df-v 2737  df-sbc 2961  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-br 3999  df-opab 4060  df-id 4287  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-iota 5170  df-fun 5210  df-fv 5216  df-riota 5821  df-ov 5868  df-oprab 5869  df-mpo 5870  df-pnf 7968  df-mnf 7969  df-xr 7970  df-ltxr 7971  df-le 7972  df-sub 8104  df-neg 8105  df-inn 8893  df-n0 9150  df-z 9227

This theorem is referenced by:  nnzd  9347  xnn0dcle  9773  xnn0letri  9774  fseq1p1m1  10064  difelfznle  10105  flltdivnn0lt  10274  zmodfz  10316  addmodid  10342  modaddmodup  10357  modaddmodlo  10358  modsumfzodifsn  10366  addmodlteq  10368  expnegzap  10524  expaddzaplem  10533  expaddzap  10534  expmulzap  10536  nn0ltexp2  10658  nn0opthd  10670  facdiv  10686  facwordi  10688  faclbnd  10689  facavg  10694  bcval  10697  bcval5  10711  bcpasc  10714  hashfiv01gt1  10730  isfinite4im  10740  fihashneq0  10742  fseq1hash  10749  fnfz0hash  10780  ffzo0hash  10782  zfz1isolemiso  10787  resqrexlemga  11000  zabscl  11063  fsum0diaglem  11416  modfsummodlemstep  11433  binomlem  11459  binom1p  11461  binom1dif  11463  arisum2  11475  geosergap  11482  geoserap  11483  pwm1geoserap1  11484  geolim2  11488  cvgratnnlemrate  11506  mertenslemi1  11511  mertenslem2  11512  mertensabs  11513  efcvgfsum  11643  efaddlem  11650  dvdsdc  11773  divalglemnn  11890  divalgmod  11899  zeqzmulgcd  11938  gcd0id  11947  gcdneg  11950  gcdaddm  11952  modgcd  11959  gcdmultipled  11961  bezoutlemnewy  11964  bezoutlemstep  11965  bezoutlemmain  11966  bezoutlemzz  11970  bezoutlemmo  11974  bezoutlemle  11976  bezoutlemsup  11977  dfgcd3  11978  dvdsgcdb  11981  gcdass  11983  mulgcd  11984  gcdzeq  11990  dvdsmulgcd  11993  bezoutr  12000  bezoutr1  12001  nn0seqcvgd  12008  algfx  12019  eucalgval2  12020  eucalginv  12023  eucalglt  12024  eucalg  12026  gcddvdslcm  12040  lcmneg  12041  lcmgcdlem  12044  lcmdvds  12046  lcmgcdeq  12050  lcmdvdsb  12051  lcmass  12052  mulgcddvds  12061  rpmulgcd2  12062  qredeu  12064  divgcdcoprm0  12068  divgcdcoprmex  12069  cncongr1  12070  cncongr2  12071  sqnprm  12103  rpexp  12120  sqpweven  12142  2sqpwodd  12143  divnumden  12163  phivalfi  12179  phicl2  12181  phiprmpw  12189  crth  12191  phimullem  12192  eulerthlemfi  12195  eulerthlema  12197  hashgcdeq  12206  phisum  12207  odzdvds  12212  powm2modprm  12219  coprimeprodsq  12224  pcprendvds  12257  pcpremul  12260  pceu  12262  pcdiv  12269  pcqcl  12273  pcdvdsb  12286  pc2dvds  12296  pcprmpw2  12299  dvdsprmpweqle  12303  pcadd  12306  fldivp1  12313  pcfaclem  12314  pcfac  12315  pcbc  12316  pockthlem  12321  1arith  12332  mul4sqlem  12358  ennnfoneleminc  12379  ennnfonelemrnh  12384  ennnfonelemim  12392  lgsval  13985  lgsfvalg  13986  lgsfcl2  13987  lgsval2lem  13991  lgsmod  14007  lgsdir2  14014  lgsne0  14019  lgsprme0  14023  2sqlem8  14039  nninffeq  14339