MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0zd Structured version   Unicode version

Theorem nn0zd 10988
Description: A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
nn0zd.1  |-  ( ph  ->  A  e.  NN0 )
Assertion
Ref Expression
nn0zd  |-  ( ph  ->  A  e.  ZZ )

Proof of Theorem nn0zd
StepHypRef Expression
1 nn0ssz 10906 . 2  |-  NN0  C_  ZZ
2 nn0zd.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3497 1  |-  ( ph  ->  A  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1819   NN0cn0 10816   ZZcz 10885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6700  df-recs 7060  df-rdg 7094  df-er 7329  df-en 7536  df-dom 7537  df-sdom 7538  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-nn 10557  df-n0 10817  df-z 10886
This theorem is referenced by:  nnzd  10989  elfz0addOLD  11801  difelfznle  11814  zmodfz  12019  expnegz  12202  expaddzlem  12211  expaddz  12212  expmulz  12214  faclbnd  12370  bcpasc  12401  hashf1  12509  fz1isolem  12513  hashge2el2dif  12524  hashtpg  12526  wrdsymb0  12582  wrdlenge1n0  12583  ccatcl  12601  ccatval3  12605  ccatsymb  12608  ccatass  12613  ccatrn  12614  lswccatn0lsw  12615  ccats1val2  12639  swrdnd  12667  swrdtrcfv0  12677  swrdtrcfvl  12686  swrdccat1  12693  swrdccat2  12694  swrdccatin2  12723  swrdccatin12  12727  splfv2a  12743  splval2  12744  revcl  12746  revccat  12751  revrev  12752  cshwmodn  12777  cshwsublen  12778  cshwn  12779  cshwidxmod  12785  2cshwid  12793  3cshw  12797  cshweqdif2  12798  revco  12811  ccatco  12812  ccat2s1fvwALT  12904  zabscl  13157  absrdbnd  13185  iseraltlem3  13517  fsum0diaglem  13602  modfsummods  13618  binomlem  13652  binom1p  13654  incexc2  13661  climcndslem1  13672  geoser  13689  geolim2  13691  mertenslem1  13704  mertenslem2  13705  mertens  13706  ruclem10  13983  divalglem9  14070  divalgmod  14075  bitsfzolem  14095  bitsfzo  14096  bitsmod  14097  bitsfi  14098  bitsinv1lem  14102  sadcaddlem  14118  sadadd3  14122  sadaddlem  14127  sadadd  14128  sadasslem  14131  sadass  14132  sadeq  14133  bitsres  14134  bitsuz  14135  bitsshft  14136  smuval2  14143  smupvallem  14144  smupval  14149  smueqlem  14151  smumullem  14153  smumul  14154  gcdcllem1  14160  gcd0id  14172  gcdneg  14175  modgcd  14185  bezoutlem4  14190  dvdsgcdb  14193  gcdass  14194  mulgcd  14195  gcdeq  14201  dvdsmulgcd  14203  nn0seqcvgd  14210  algfx  14220  eucalginv  14224  eucalg  14227  sqnprm  14250  mulgcddvds  14256  rpmulgcd2  14257  qredeu  14259  divnumden  14292  powm2modprm  14339  coprimeprodsq  14344  iserodd  14370  pclem  14373  pcpre1  14377  pcpremul  14378  pcqcl  14391  pcdvdsb  14403  pcidlem  14406  pc2dvds  14413  pcprmpw2  14416  pcadd  14419  pcfac  14429  pcbc  14430  pockthlem  14434  prmreclem2  14446  prmreclem3  14447  mul4sqlem  14482  4sqlem11  14484  4sqlem12  14485  4sqlem14  14487  vdwapun  14503  lagsubg  16389  psgnuni  16650  psgnran  16666  odmodnn0  16690  mndodconglem  16691  mndodcong  16692  odmulg2  16703  odmulg  16704  odmulgeq  16705  odbezout  16706  odinv  16709  odf1  16710  gexod  16732  gexdvds3  16736  sylow1lem1  16744  sylow1lem3  16746  pgpfi  16751  pgpssslw  16760  sylow2alem2  16764  sylow2blem3  16768  fislw  16771  sylow3lem4  16776  sylow3lem6  16778  efginvrel2  16871  efgredlemf  16885  efgredlemd  16888  efgredlemc  16889  efgredlem  16891  efgcpbllemb  16899  odadd1  16980  odadd2  16981  gexexlem  16984  gexex  16985  torsubg  16986  lt6abl  17023  gsummulg  17091  ablfacrplem  17242  ablfacrp  17243  ablfacrp2  17244  ablfac1b  17247  ablfac1c  17248  ablfac1eulem  17249  ablfac1eu  17250  pgpfac1lem2  17252  pgpfaclem1  17258  ablfaclem3  17264  srgbinomlem3  17319  srgbinomlem4  17320  psrbaglefi  18149  psrbaglefiOLD  18150  chrid  18690  znunit  18728  psgnghm  18742  chfacfscmulfsupp  19486  chfacfpmmulfsupp  19490  cpmadugsumlemF  19503  dyadss  22128  dyaddisjlem  22129  ply1divex  22662  ply1termlem  22725  plyeq0lem  22732  plyaddlem1  22735  plymullem1  22736  coeeulem  22746  coeidlem  22759  coeeq2  22764  coemulhi  22776  dvply1  22805  dvply2g  22806  plydivex  22818  elqaalem2  22841  aareccl  22847  aannenlem1  22849  aalioulem1  22853  taylplem1  22883  taylplem2  22884  taylpfval  22885  dvtaylp  22890  taylthlem2  22894  dvradcnv  22941  abelthlem7  22958  cxpeq  23256  birthdaylem2  23407  ftalem1  23471  basellem3  23481  isppw2  23514  isnsqf  23534  mule1  23547  ppinncl  23573  musum  23592  chtublem  23611  pclogsum  23615  vmasum  23616  dchrabs  23660  bcmax  23678  bposlem1  23684  bposlem6  23689  lgsval2lem  23706  lgsmod  23721  lgsdirprm  23729  lgsne0  23733  lgseisenlem1  23749  lgseisenlem2  23750  lgseisenlem3  23751  lgseisenlem4  23752  lgsquadlem1  23754  m1lgs  23762  2sqlem8  23772  chebbnd1lem1  23779  dchrisumlem1  23799  dchrisum0flblem1  23818  selberg2lem  23860  ostth2lem2  23944  ostth2lem3  23945  wwlknredwwlkn0  24853  wwlkextproplem2  24868  clwwlkndivn  24963  nbhashuvtx1  25041  eupath2lem3  25105  eupath2  25106  numclwwlkovf2ex  25212  numclwwlk5  25238  numclwwlk6  25239  ex-ind-dvds  25296  gxnn0mul  25405  nndiffz1  27748  2sqcoprm  27787  2sqmod  27788  archirng  27884  archirngz  27885  archiabllem1a  27887  qqhval2lem  28115  oddpwdc  28468  eulerpartlems  28474  eulerpartlemb  28482  sseqfv1  28503  sseqfn  28504  sseqmw  28505  sseqf  28506  sseqfv2  28508  sseqp1  28509  eluzmn  28666  ccatmulgnn0dir  28671  ofccat  28672  signsplypnf  28682  signsply0  28683  signslema  28694  signstfvn  28701  signstfvp  28703  signstfvc  28706  subfacval3  28808  binomfallfaclem2  29337  binomrisefac  29339  fallfacval4  29340  bpolydiflem  29978  geomcau  30414  eldioph2lem1  30855  pellexlem5  30931  congrep  31073  bezoutr  31085  bezoutr1  31086  jm2.18  31092  jm2.19lem1  31093  jm2.19lem2  31094  jm2.19  31097  jm2.22  31099  jm2.23  31100  jm2.20nn  31101  jm2.25  31103  jm2.26a  31104  jm2.26lem3  31105  jm2.26  31106  jm2.27a  31109  jm2.27b  31110  jm2.27c  31111  jm3.1  31124  expdiophlem1  31125  hbtlem5  31239  radcnvrat  31357  gcddvdslcm  31370  lcmneg  31371  lcmgcdlem  31374  lcmdvds  31376  lcmgcdeq  31378  lcmdvdsb  31379  lcmass  31380  nzin  31385  bccbc  31412  binomcxplemnn0  31416  binomcxplemnotnn0  31423  fprodexp  31761  mccllem  31766  ioodvbdlimc1lem2  31890  ioodvbdlimc2lem  31892  dvnxpaek  31900  dvnmul  31901  dvnprodlem1  31904  dvnprodlem2  31905  wallispilem1  32008  wallispilem5  32012  stirlinglem3  32019  stirlinglem5  32021  stirlinglem7  32023  stirlinglem8  32024  fourierdlem102  32152  fourierdlem114  32164  sqwvfoura  32172  elaa2lem  32177  etransclem10  32188  etransclem20  32198  etransclem21  32199  etransclem22  32200  etransclem23  32201  etransclem24  32202  etransclem27  32205  etransclem28  32206  etransclem35  32213  etransclem38  32216  etransclem44  32222  etransclem45  32223  etransclem46  32224  pfxtrcfv0  32477  pfxtrcfvl  32481  pfxccat1  32486  pfxccatin12  32501  pfxccatpfx2  32504  pfxccat3a  32505  fsummmodsnunz  32568  ssnn0ssfz  33040  altgsumbcALT  33044  aacllem  33318
  Copyright terms: Public domain W3C validator