Theorem nn0zd 9770

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℕ₀cn0 9567  ℤcz 9648

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 8500  df-neg 8501  df-inn 9307  df-n0 9568  df-z 9649

This theorem is used by:  nnzd  9771  eluzmn  9937  xnn0dcle  10214  xnn0letri  10215  fseq1p1m1  10511  difelfznle  10552  flltdivnn0lt  10752  zmodfz  10796  addmodid  10822  modaddmodup  10837  modaddmodlo  10838  modsumfzodifsn  10846  addmodlteq  10848  expnegzap  11023  expaddzaplem  11032  expaddzap  11033  expmulzap  11035  nn0ltexp2  11161  nn0opthd  11174  facdiv  11190  facwordi  11192  faclbnd  11193  facavg  11198  bcval  11201  bcval5  11215  bcpasc  11218  hashfiv01gt1  11235  isfinite4im  11245  fihashneq0  11247  fseq1hash  11255  fnfz0hash  11289  ffzo0hash  11291  sseqn  11293  hashfibclem  11296  hashf1  11301  zfz1isolemiso  11305  wrdfin  11337  wrdffz  11339  wrdsymb0  11351  wrdlenge1n0  11352  lswwrd  11365  ccatfvalfi  11374  ccatcl  11375  ccatlen  11377  ccatval2  11380  ccatval3  11381  ccatvalfn  11383  ccatsymb  11384  ccatval21sw  11387  ccatass  11390  ccatrn  11391  lswccatn0lsw  11393  ccatalpha  11395  ccats1val2  11422  ccat1st1st  11423  fzowrddc  11433  swrdnd  11445  swrdspsleq  11453  swrdccat2  11457  pfxval  11460  pfxwrdsymbg  11476  pfxtrcfv0  11480  pfxtrcfvl  11483  ccatpfx  11487  pfxccat1  11488  lenrevpfxcctswrd  11498  wrdind  11508  wrd2ind  11509  swrdccatin1  11511  swrdccatin2  11515  pfxccatin12  11519  swrdccat  11521  pfxccatpfx2  11523  pfxccat3a  11524  swrdccat3blem  11525  swrdccat3b  11526  resqrexlemga  11803  zabscl  11867  fsum0diaglem  12223  modfsummodlemstep  12240  binomlem  12266  binom1p  12268  binom1dif  12270  arisum2  12282  geosergap  12289  geoserap  12290  pwm1geoserap1  12291  geolim2  12295  cvgratnnlemrate  12313  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  efcvgfsum  12450  efaddlem  12457  dvdsdc  12581  divalglemnn  12701  divalgmod  12710  bitsfzolem  12737  bitsfzo  12738  bitsmod  12739  bitsfi  12740  bitsinv1lem  12744  bitsinv1  12745  zeqzmulgcd  12763  gcd0id  12772  gcdneg  12775  gcdaddm  12777  modgcd  12784  gcdmultipled  12786  bezoutlemnewy  12789  bezoutlemstep  12790  bezoutlemmain  12791  bezoutlemzz  12795  bezoutlemmo  12799  bezoutlemle  12801  bezoutlemsup  12802  dfgcd3  12803  dvdsgcdb  12806  gcdass  12808  mulgcd  12809  gcdzeq  12815  dvdsmulgcd  12818  bezoutr  12825  bezoutr1  12826  nn0seqcvgd  12835  algfx  12846  eucalgval2  12847  eucalginv  12850  eucalglt  12851  eucalg  12853  gcddvdslcm  12867  lcmneg  12868  lcmgcdlem  12871  lcmdvds  12873  lcmgcdeq  12877  lcmdvdsb  12878  lcmass  12879  mulgcddvds  12888  rpmulgcd2  12889  qredeu  12891  divgcdcoprm0  12895  divgcdcoprmex  12896  cncongr1  12897  cncongr2  12898  sqnprm  12931  rpexp  12948  sqpweven  12971  2sqpwodd  12972  divnumden  12992  phivalfi  13010  phicl2  13012  phiprmpw  13020  crth  13022  phimullem  13023  eulerthlemfi  13026  eulerthlema  13028  hashgcdeq  13038  phisum  13039  odzdvds  13044  powm2modprm  13051  coprimeprodsq  13056  pcprendvds  13089  pcpremul  13092  pceu  13094  pcdiv  13101  pcqcl  13105  pcdvdsb  13119  pc2dvds  13129  pcprmpw2  13132  dvdsprmpweqle  13136  pcadd  13139  fldivp1  13147  pcfaclem  13148  pcfac  13149  pcbc  13150  pockthlem  13155  1arith  13166  mul4sqlem  13192  4sqlemafi  13194  4sqlemffi  13195  4sqleminfi  13196  4sqexercise1  13197  4sqlemsdc  13199  4sqlem11  13200  4sqlem12  13201  4sqlem14  13203  ballotfilemofi  13268  ballotfilemfval  13278  ballotfilemfelz  13279  ballotfilemgval  13316  ennnfoneleminc  13351  ennnfonelemrnh  13356  ennnfonelemim  13364  gsumvalfi  14201  gzsumgsum1  14202  gsumf1ofi  14209  gsummhmfi  14213  gsumressfi  14216  znunit  15043  asclmulg  15093  psrbaglesuppg  15106  psrbagfi  15108  psrbaglecl  15109  psrbagcon  15111  psrbagconf1o  15113  psr1clfi  15128  elply2  15885  plyf  15887  elplyd  15891  ply1termlem  15892  ply1term  15893  plyaddlem1  15897  plymullem1  15898  plyaddlem  15899  plycoeid3  15907  plycolemc  15908  plycjlemc  15910  plycn  15912  plyrecj  15913  dvply1  15915  dvply2g  15916  zprmlogbaplem1  16134  zprmlogbaplem2  16135  birthdaylem2  16145  wilthlem1  16151  ppiqnncl  16181  sgmppw  16187  ppiqub  16194  bcmax  16203  bposlem1  16209  bposlem5  16213  lgsval  16221  lgsfvalg  16222  lgsfcl2  16223  lgsval2lem  16227  lgsmod  16243  lgsdir2  16250  lgsne0  16255  lgsprme0  16259  gausslemma2dlem0h  16273  gausslemma2dlem0i  16274  gausslemma2dlem2  16279  gausslemma2dlem6  16284  gausslemma2d  16286  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgsquadlem1  16294  lgsquadlem2  16295  m1lgs  16302  2lgslem1a  16305  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2lgslem3d1  16317  2lgs  16321  2lgsoddprmlem2  16323  2lgsoddprm  16330  2sqlem8  16340  vdegp1bid  16654  wksfval  16661  wlkex  16664  iswlkg  16668  clwwlkccatlem  16739  umgrclwwlkge2  16741  clwwlknonex2lem2  16777  eupthfi  16790  eupth2lem3lem3fi  16809  eupth2lem3lem4fi  16812  eupth2lem3fi  16815  eupth2lemsfi  16817  konigsberglem5  16831  nninffeq  17161