Theorem nn0zd 9766

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℕ₀cn0 9563  ℤ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:  nnzd  9767  eluzmn  9928  xnn0dcle  10204  xnn0letri  10205  fseq1p1m1  10501  difelfznle  10542  flltdivnn0lt  10739  zmodfz  10783  addmodid  10809  modaddmodup  10824  modaddmodlo  10825  modsumfzodifsn  10833  addmodlteq  10835  expnegzap  11010  expaddzaplem  11019  expaddzap  11020  expmulzap  11022  nn0ltexp2  11147  nn0opthd  11160  facdiv  11176  facwordi  11178  faclbnd  11179  facavg  11184  bcval  11187  bcval5  11201  bcpasc  11204  hashfiv01gt1  11221  isfinite4im  11231  fihashneq0  11233  fseq1hash  11241  fnfz0hash  11275  ffzo0hash  11277  sseqn  11279  hashfibclem  11282  hashf1  11287  zfz1isolemiso  11291  wrdfin  11323  wrdffz  11325  wrdsymb0  11337  wrdlenge1n0  11338  lswwrd  11351  ccatfvalfi  11360  ccatcl  11361  ccatlen  11363  ccatval2  11366  ccatval3  11367  ccatvalfn  11369  ccatsymb  11370  ccatval21sw  11373  ccatass  11376  ccatrn  11377  lswccatn0lsw  11379  ccatalpha  11381  ccats1val2  11408  ccat1st1st  11409  fzowrddc  11419  swrdnd  11431  swrdspsleq  11439  swrdccat2  11443  pfxval  11446  pfxwrdsymbg  11462  pfxtrcfv0  11466  pfxtrcfvl  11469  ccatpfx  11473  pfxccat1  11474  lenrevpfxcctswrd  11484  wrdind  11494  wrd2ind  11495  swrdccatin1  11497  swrdccatin2  11501  pfxccatin12  11505  swrdccat  11507  pfxccatpfx2  11509  pfxccat3a  11510  swrdccat3blem  11511  swrdccat3b  11512  resqrexlemga  11789  zabscl  11852  fsum0diaglem  12207  modfsummodlemstep  12224  binomlem  12250  binom1p  12252  binom1dif  12254  arisum2  12266  geosergap  12273  geoserap  12274  pwm1geoserap1  12275  geolim2  12279  cvgratnnlemrate  12297  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  efcvgfsum  12434  efaddlem  12441  dvdsdc  12565  divalglemnn  12685  divalgmod  12694  bitsfzolem  12721  bitsfzo  12722  bitsmod  12723  bitsfi  12724  bitsinv1lem  12728  bitsinv1  12729  zeqzmulgcd  12747  gcd0id  12756  gcdneg  12759  gcdaddm  12761  modgcd  12768  gcdmultipled  12770  bezoutlemnewy  12773  bezoutlemstep  12774  bezoutlemmain  12775  bezoutlemzz  12779  bezoutlemmo  12783  bezoutlemle  12785  bezoutlemsup  12786  dfgcd3  12787  dvdsgcdb  12790  gcdass  12792  mulgcd  12793  gcdzeq  12799  dvdsmulgcd  12802  bezoutr  12809  bezoutr1  12810  nn0seqcvgd  12819  algfx  12830  eucalgval2  12831  eucalginv  12834  eucalglt  12835  eucalg  12837  gcddvdslcm  12851  lcmneg  12852  lcmgcdlem  12855  lcmdvds  12857  lcmgcdeq  12861  lcmdvdsb  12862  lcmass  12863  mulgcddvds  12872  rpmulgcd2  12873  qredeu  12875  divgcdcoprm0  12879  divgcdcoprmex  12880  cncongr1  12881  cncongr2  12882  sqnprm  12914  rpexp  12931  sqpweven  12953  2sqpwodd  12954  divnumden  12974  phivalfi  12990  phicl2  12992  phiprmpw  13000  crth  13002  phimullem  13003  eulerthlemfi  13006  eulerthlema  13008  hashgcdeq  13018  phisum  13019  odzdvds  13024  powm2modprm  13031  coprimeprodsq  13036  pcprendvds  13069  pcpremul  13072  pceu  13074  pcdiv  13081  pcqcl  13085  pcdvdsb  13099  pc2dvds  13109  pcprmpw2  13112  dvdsprmpweqle  13116  pcadd  13119  fldivp1  13127  pcfaclem  13128  pcfac  13129  pcbc  13130  pockthlem  13135  1arith  13146  mul4sqlem  13172  4sqlemafi  13174  4sqlemffi  13175  4sqleminfi  13176  4sqexercise1  13177  4sqlemsdc  13179  4sqlem11  13180  4sqlem12  13181  4sqlem14  13183  ballotfilemofi  13219  ballotfilemfval  13229  ballotfilemfelz  13230  ballotfilemgval  13267  ennnfoneleminc  13302  ennnfonelemrnh  13307  ennnfonelemim  13315  gsumvalfi  14152  gzsumgsum1  14153  gsumf1ofi  14160  gsummhmfi  14164  gsumressfi  14167  znunit  14994  asclmulg  15044  psrbaglesuppg  15057  psrbagfi  15059  psrbaglecl  15060  psrbagcon  15062  psrbagconf1o  15064  psr1clfi  15079  elply2  15836  plyf  15838  elplyd  15842  ply1termlem  15843  ply1term  15844  plyaddlem1  15848  plymullem1  15849  plyaddlem  15850  plycoeid3  15858  plycolemc  15859  plycjlemc  15861  plycn  15863  plyrecj  15864  dvply1  15866  dvply2g  15867  birthdaylem2  16088  wilthlem1  16094  sgmppw  16106  lgsval  16123  lgsfvalg  16124  lgsfcl2  16125  lgsval2lem  16129  lgsmod  16145  lgsdir2  16152  lgsne0  16157  lgsprme0  16161  gausslemma2dlem0h  16175  gausslemma2dlem0i  16176  gausslemma2dlem2  16181  gausslemma2dlem6  16186  gausslemma2d  16188  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgsquadlem1  16196  lgsquadlem2  16197  m1lgs  16204  2lgslem1a  16207  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2lgslem3d1  16219  2lgs  16223  2lgsoddprmlem2  16225  2lgsoddprm  16232  2sqlem8  16242  vdegp1bid  16556  wksfval  16563  wlkex  16566  iswlkg  16570  clwwlkccatlem  16641  umgrclwwlkge2  16643  clwwlknonex2lem2  16679  eupthfi  16692  eupth2lem3lem3fi  16711  eupth2lem3lem4fi  16714  eupth2lem3fi  16717  eupth2lemsfi  16719  konigsberglem5  16733  nninffeq  17063