Theorem nn0zd 9563

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℕ₀cn0 9365  ℤcz 9442

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292  ax-un 4523  ax-setind 4628  ax-cnex 8086  ax-resscn 8087  ax-1cn 8088  ax-1re 8089  ax-icn 8090  ax-addcl 8091  ax-addrcl 8092  ax-mulcl 8093  ax-addcom 8095  ax-addass 8097  ax-distr 8099  ax-i2m1 8100  ax-0lt1 8101  ax-0id 8103  ax-rnegex 8104  ax-cnre 8106  ax-pre-ltirr 8107  ax-pre-ltwlin 8108  ax-pre-lttrn 8109  ax-pre-ltadd 8111

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-int 3923  df-br 4083  df-opab 4145  df-id 4383  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-iota 5277  df-fun 5319  df-fv 5325  df-riota 5953  df-ov 6003  df-oprab 6004  df-mpo 6005  df-pnf 8179  df-mnf 8180  df-xr 8181  df-ltxr 8182  df-le 8183  df-sub 8315  df-neg 8316  df-inn 9107  df-n0 9366  df-z 9443

This theorem is referenced by:  nnzd  9564  xnn0dcle  9994  xnn0letri  9995  fseq1p1m1  10286  difelfznle  10327  flltdivnn0lt  10519  zmodfz  10563  addmodid  10589  modaddmodup  10604  modaddmodlo  10605  modsumfzodifsn  10613  addmodlteq  10615  expnegzap  10790  expaddzaplem  10799  expaddzap  10800  expmulzap  10802  nn0ltexp2  10926  nn0opthd  10939  facdiv  10955  facwordi  10957  faclbnd  10958  facavg  10963  bcval  10966  bcval5  10980  bcpasc  10983  hashfiv01gt1  10999  isfinite4im  11009  fihashneq0  11011  fseq1hash  11018  fnfz0hash  11049  ffzo0hash  11051  zfz1isolemiso  11056  wrdfin  11085  wrdffz  11087  wrdsymb0  11099  wrdlenge1n0  11100  lswwrd  11113  ccatfvalfi  11122  ccatcl  11123  ccatlen  11125  ccatval2  11128  ccatval3  11129  ccatvalfn  11131  ccatsymb  11132  ccatval21sw  11135  ccatass  11138  ccatrn  11139  lswccatn0lsw  11141  ccats1val2  11166  ccat1st1st  11167  fzowrddc  11174  swrdnd  11186  swrdspsleq  11194  swrdccat2  11198  pfxval  11201  pfxwrdsymbg  11217  pfxtrcfv0  11221  pfxtrcfvl  11224  ccatpfx  11228  pfxccat1  11229  lenrevpfxcctswrd  11239  wrdind  11249  wrd2ind  11250  swrdccatin1  11252  swrdccatin2  11256  pfxccatin12  11260  swrdccat  11262  pfxccatpfx2  11264  pfxccat3a  11265  swrdccat3blem  11266  swrdccat3b  11267  resqrexlemga  11529  zabscl  11592  fsum0diaglem  11946  modfsummodlemstep  11963  binomlem  11989  binom1p  11991  binom1dif  11993  arisum2  12005  geosergap  12012  geoserap  12013  pwm1geoserap1  12014  geolim2  12018  cvgratnnlemrate  12036  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  efcvgfsum  12173  efaddlem  12180  dvdsdc  12304  divalglemnn  12424  divalgmod  12433  bitsfzolem  12460  bitsfzo  12461  bitsmod  12462  bitsfi  12463  bitsinv1lem  12467  bitsinv1  12468  zeqzmulgcd  12486  gcd0id  12495  gcdneg  12498  gcdaddm  12500  modgcd  12507  gcdmultipled  12509  bezoutlemnewy  12512  bezoutlemstep  12513  bezoutlemmain  12514  bezoutlemzz  12518  bezoutlemmo  12522  bezoutlemle  12524  bezoutlemsup  12525  dfgcd3  12526  dvdsgcdb  12529  gcdass  12531  mulgcd  12532  gcdzeq  12538  dvdsmulgcd  12541  bezoutr  12548  bezoutr1  12549  nn0seqcvgd  12558  algfx  12569  eucalgval2  12570  eucalginv  12573  eucalglt  12574  eucalg  12576  gcddvdslcm  12590  lcmneg  12591  lcmgcdlem  12594  lcmdvds  12596  lcmgcdeq  12600  lcmdvdsb  12601  lcmass  12602  mulgcddvds  12611  rpmulgcd2  12612  qredeu  12614  divgcdcoprm0  12618  divgcdcoprmex  12619  cncongr1  12620  cncongr2  12621  sqnprm  12653  rpexp  12670  sqpweven  12692  2sqpwodd  12693  divnumden  12713  phivalfi  12729  phicl2  12731  phiprmpw  12739  crth  12741  phimullem  12742  eulerthlemfi  12745  eulerthlema  12747  hashgcdeq  12757  phisum  12758  odzdvds  12763  powm2modprm  12770  coprimeprodsq  12775  pcprendvds  12808  pcpremul  12811  pceu  12813  pcdiv  12820  pcqcl  12824  pcdvdsb  12838  pc2dvds  12848  pcprmpw2  12851  dvdsprmpweqle  12855  pcadd  12858  fldivp1  12866  pcfaclem  12867  pcfac  12868  pcbc  12869  pockthlem  12874  1arith  12885  mul4sqlem  12911  4sqlemafi  12913  4sqlemffi  12914  4sqleminfi  12915  4sqexercise1  12916  4sqlemsdc  12918  4sqlem11  12919  4sqlem12  12920  4sqlem14  12922  ennnfoneleminc  12977  ennnfonelemrnh  12982  ennnfonelemim  12990  znunit  14617  psrbaglesuppg  14630  psrbagfi  14631  psr1clfi  14646  elply2  15403  plyf  15405  elplyd  15409  ply1termlem  15410  ply1term  15411  plyaddlem1  15415  plymullem1  15416  plyaddlem  15417  plycoeid3  15425  plycolemc  15426  plycjlemc  15428  plycn  15430  plyrecj  15431  dvply1  15433  dvply2g  15434  wilthlem1  15648  sgmppw  15660  lgsval  15677  lgsfvalg  15678  lgsfcl2  15679  lgsval2lem  15683  lgsmod  15699  lgsdir2  15706  lgsne0  15711  lgsprme0  15715  gausslemma2dlem0h  15729  gausslemma2dlem0i  15730  gausslemma2dlem2  15735  gausslemma2dlem6  15740  gausslemma2d  15742  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgseisenlem4  15746  lgsquadlem1  15750  lgsquadlem2  15751  m1lgs  15758  2lgslem1a  15761  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2lgslem3d1  15773  2lgs  15777  2lgsoddprmlem2  15779  2lgsoddprm  15786  2sqlem8  15796  wksfval  16028  iswlkg  16032  nninffeq  16345