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

Theorem nn0zd 11046
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 10966 . 2  |-  NN0  C_  ZZ
2 nn0zd.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3462 1  |-  ( ph  ->  A  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872   NN0cn0 10877   ZZcz 10945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-resscn 9604  ax-1cn 9605  ax-icn 9606  ax-addcl 9607  ax-addrcl 9608  ax-mulcl 9609  ax-mulrcl 9610  ax-mulcom 9611  ax-addass 9612  ax-mulass 9613  ax-distr 9614  ax-i2m1 9615  ax-1ne0 9616  ax-1rid 9617  ax-rnegex 9618  ax-rrecex 9619  ax-cnre 9620  ax-pre-lttri 9621  ax-pre-lttrn 9622  ax-pre-ltadd 9623  ax-pre-mulgt0 9624
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6268  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-om 6708  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-er 7375  df-en 7582  df-dom 7583  df-sdom 7584  df-pnf 9685  df-mnf 9686  df-xr 9687  df-ltxr 9688  df-le 9689  df-sub 9870  df-neg 9871  df-nn 10618  df-n0 10878  df-z 10946
This theorem is referenced by:  nnzd  11047  elfz0addOLD  11900  difelfznle  11913  zmodfz  12125  expnegz  12313  expaddzlem  12322  expaddz  12323  expmulz  12325  faclbnd  12482  bcpasc  12513  hashf1  12625  fz1isolem  12629  hashge2el2dif  12642  hashtpg  12646  wrdsymb0  12706  wrdlenge1n0  12707  ccatcl  12725  ccatval3  12729  ccatsymb  12732  ccatass  12737  ccatrn  12738  lswccatn0lsw  12739  ccats1val2  12763  swrdnd  12791  swrdtrcfv0  12801  swrdtrcfvl  12809  swrdccat1  12816  swrdccat2  12817  swrdccatin2  12846  swrdccatin12  12850  splfv2a  12866  splval2  12867  revcl  12869  revccat  12874  revrev  12875  cshwmodn  12900  cshwsublen  12901  cshwn  12902  cshwidxmod  12908  2cshwid  12916  3cshw  12920  cshweqdif2  12921  revco  12934  ccatco  12935  ccat2s1fvwALT  13031  zabscl  13377  absrdbnd  13405  iseraltlem3  13750  fsum0diaglem  13837  modfsummods  13853  binomlem  13887  binom1p  13889  incexc2  13896  climcndslem1  13907  geoser  13925  geolim2  13927  mertenslem1  13940  mertenslem2  13941  mertens  13942  binomfallfaclem2  14093  binomrisefac  14095  fallfacval4  14096  bpolydiflem  14107  ruclem10  14291  divalglem9  14381  divalglem9OLD  14382  divalgmod  14387  bitsfzolem  14407  bitsfzolemOLD  14408  bitsfzo  14409  bitsmod  14410  bitsfi  14411  bitsinv1lem  14415  sadcaddlem  14431  sadadd3  14435  sadaddlem  14440  sadadd  14441  sadasslem  14444  sadass  14445  sadeq  14446  bitsres  14447  bitsuz  14448  bitsshft  14449  smuval2  14456  smupvallem  14457  smupval  14462  smueqlem  14464  smumullem  14466  smumul  14467  gcdcllem1  14473  gcd0id  14487  gcdneg  14490  modgcd  14500  bezoutlem4OLD  14506  bezoutlem4  14509  dvdsgcdb  14512  gcdass  14513  mulgcd  14514  gcdeq  14520  dvdsmulgcd  14522  nn0seqcvgd  14529  algfx  14539  eucalginv  14543  eucalg  14546  gcddvdslcm  14567  lcmneg  14568  lcmgcdlem  14571  lcmdvds  14573  lcmgcdeq  14577  lcmdvdsb  14578  lcmass  14579  lcmftp  14609  lcmfunsnlem1  14610  lcmfunsnlem2lem1  14611  lcmfunsnlem2lem2  14612  lcmfunsnlem2  14613  lcmfdvdsb  14616  lcmfun  14618  lcmfass  14619  sqnprm  14646  mulgcddvds  14661  rpmulgcd2  14662  qredeu  14664  divnumden  14697  powm2modprm  14754  coprimeprodsq  14759  iserodd  14785  pclem  14788  pcpre1  14792  pcpremul  14793  pcqcl  14806  pcdvdsb  14818  pcidlem  14821  pc2dvds  14828  pcprmpw2  14831  pcadd  14834  pcfac  14844  pcbc  14845  pockthlem  14849  prmreclem2  14861  prmreclem3  14862  mul4sqlem  14897  4sqlem11  14899  4sqlem12  14900  4sqlem14OLD  14902  4sqlem14  14908  vdwapun  14924  prmgaplcmlem1  15009  lagsubg  16879  psgnuni  17140  psgnran  17156  odmodnn0  17189  mndodconglem  17190  mndodcong  17191  odmulg2  17206  odmulg  17207  odmulgeq  17208  odbezout  17209  odinv  17212  odf1  17213  gexod  17238  gexdvds3  17242  sylow1lem1  17250  sylow1lem3  17252  pgpfi  17257  pgpssslw  17266  sylow2alem2  17270  sylow2blem3  17274  fislw  17277  sylow3lem4  17282  sylow3lem6  17284  efginvrel2  17377  efgredlemf  17391  efgredlemd  17394  efgredlemc  17395  efgredlem  17397  efgcpbllemb  17405  odadd1  17486  odadd2  17487  gexexlem  17490  gexex  17491  torsubg  17492  lt6abl  17529  gsummulg  17575  ablfacrplem  17698  ablfacrp  17699  ablfacrp2  17700  ablfac1b  17703  ablfac1c  17704  ablfac1eulem  17705  ablfac1eu  17706  pgpfac1lem2  17708  pgpfaclem1  17714  ablfaclem3  17720  srgbinomlem3  17775  srgbinomlem4  17776  psrbaglefi  18596  chrid  19097  znunit  19133  psgnghm  19147  chfacfscmulfsupp  19882  chfacfpmmulfsupp  19886  cpmadugsumlemF  19899  dyadss  22551  dyaddisjlem  22552  ply1divex  23086  ply1termlem  23156  plyeq0lem  23163  plyaddlem1  23166  plymullem1  23167  coeeulem  23177  coeidlem  23190  coeeq2  23195  coemulhi  23207  dvply1  23236  dvply2g  23237  plydivex  23249  elqaalem2  23272  elqaalem2OLD  23275  aareccl  23281  aannenlem1  23283  aalioulem1  23287  taylplem1  23317  taylplem2  23318  taylpfval  23319  dvtaylp  23324  taylthlem2  23328  dvradcnv  23375  abelthlem7  23392  cxpeq  23696  birthdaylem2  23877  ftalem1  23996  basellem3  24008  isppw2  24041  isnsqf  24061  mule1  24074  ppinncl  24100  musum  24119  chtublem  24138  pclogsum  24142  vmasum  24143  dchrabs  24187  bcmax  24205  bposlem1  24211  bposlem6  24216  lgsval2lem  24233  lgsmod  24248  lgsdirprm  24256  lgsne0  24260  lgseisenlem1  24276  lgseisenlem2  24277  lgseisenlem3  24278  lgseisenlem4  24279  lgsquadlem1  24281  m1lgs  24289  2sqlem8  24299  chebbnd1lem1  24306  dchrisumlem1  24326  dchrisum0flblem1  24345  selberg2lem  24387  ostth2lem2  24471  ostth2lem3  24472  wwlknredwwlkn0  25454  wwlkextproplem2  25469  clwwlkndivn  25564  nbhashuvtx1  25642  eupath2lem3  25706  eupath2  25707  numclwwlkovf2ex  25813  numclwwlk5  25839  numclwwlk6  25840  ex-ind-dvds  25898  gxnn0mul  26004  nndiffz1  28373  2sqcoprm  28416  2sqmod  28417  archirng  28513  archirngz  28514  archiabllem1a  28516  madjusmdetlem4  28665  qqhval2lem  28794  oddpwdc  29196  eulerpartlems  29202  eulerpartlemb  29210  sseqfv1  29231  sseqfn  29232  sseqmw  29233  sseqf  29234  sseqfv2  29236  sseqp1  29237  eluzmn  29432  ccatmulgnn0dir  29437  ofccat  29438  signsplypnf  29448  signsply0  29449  signslema  29460  signstfvn  29467  signstfvp  29469  signstfvc  29472  subfacval3  29921  bcprod  30382  bccolsum  30383  fwddifnp1  30938  poimirlem3  31908  poimirlem4  31909  poimirlem6  31911  poimirlem13  31918  poimirlem14  31919  poimirlem17  31922  poimirlem21  31926  poimirlem22  31927  poimirlem23  31928  poimirlem24  31929  poimirlem26  31931  poimirlem27  31932  poimirlem31  31936  geomcau  32053  eldioph2lem1  35572  pellexlem5  35648  congrep  35794  bezoutr  35806  bezoutr1  35807  jm2.18  35814  jm2.19lem1  35815  jm2.19lem2  35816  jm2.19  35819  jm2.22  35821  jm2.23  35822  jm2.20nn  35823  jm2.25  35825  jm2.26a  35826  jm2.26lem3  35827  jm2.26  35828  jm2.27a  35831  jm2.27b  35832  jm2.27c  35833  jm3.1  35846  expdiophlem1  35847  hbtlem5  35958  radcnvrat  36634  nzin  36638  bccbc  36665  binomcxplemnn0  36669  binomcxplemnotnn0  36676  fprodexp  37615  mccllem  37618  ioodvbdlimc1lem2  37745  ioodvbdlimc1lem2OLD  37747  ioodvbdlimc2lem  37749  ioodvbdlimc2lemOLD  37750  dvnxpaek  37758  dvnmul  37759  dvnprodlem1  37762  dvnprodlem2  37763  wallispilem1  37868  wallispilem5  37872  stirlinglem3  37879  stirlinglem5  37881  stirlinglem7  37883  stirlinglem8  37884  fourierdlem102  38013  fourierdlem114  38025  sqwvfoura  38033  elaa2lem  38038  elaa2lemOLD  38039  etransclem10  38050  etransclem20  38060  etransclem21  38061  etransclem22  38062  etransclem23  38063  etransclem24  38064  etransclem27  38067  etransclem28  38068  etransclem35  38075  etransclem38  38078  etransclem44  38084  etransclem45  38085  etransclem46  38086  sge0ad2en  38182  gcdzeq  38664  pfxtrcfv0  38814  pfxtrcfvl  38817  pfxccat1  38822  pfxccatin12  38837  pfxccatpfx2  38840  pfxccat3a  38841  fsummmodsnunz  38926  ssnn0ssfz  39781  altgsumbcALT  39785  flnn0ohalf  39992  dig2nn1st  40067  0dig2nn0o  40075  aacllem  40191
  Copyright terms: Public domain W3C validator