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

Theorem nn0zd 11038
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 10958 . 2  |-  NN0  C_  ZZ
2 nn0zd.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3468 1  |-  ( ph  ->  A  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   NN0cn0 10869   ZZcz 10937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615
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 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  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 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-er 7371  df-en 7578  df-dom 7579  df-sdom 7580  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-nn 10610  df-n0 10870  df-z 10938
This theorem is referenced by:  nnzd  11039  elfz0addOLD  11890  difelfznle  11903  zmodfz  12115  expnegz  12303  expaddzlem  12312  expaddz  12313  expmulz  12315  faclbnd  12472  bcpasc  12503  hashf1  12615  fz1isolem  12619  hashge2el2dif  12630  hashtpg  12632  wrdsymb0  12688  wrdlenge1n0  12689  ccatcl  12707  ccatval3  12711  ccatsymb  12714  ccatass  12719  ccatrn  12720  lswccatn0lsw  12721  ccats1val2  12745  swrdnd  12773  swrdtrcfv0  12783  swrdtrcfvl  12791  swrdccat1  12798  swrdccat2  12799  swrdccatin2  12828  swrdccatin12  12832  splfv2a  12848  splval2  12849  revcl  12851  revccat  12856  revrev  12857  cshwmodn  12882  cshwsublen  12883  cshwn  12884  cshwidxmod  12890  2cshwid  12898  3cshw  12902  cshweqdif2  12903  revco  12916  ccatco  12917  ccat2s1fvwALT  13009  zabscl  13355  absrdbnd  13383  iseraltlem3  13728  fsum0diaglem  13815  modfsummods  13831  binomlem  13865  binom1p  13867  incexc2  13874  climcndslem1  13885  geoser  13903  geolim2  13905  mertenslem1  13918  mertenslem2  13919  mertens  13920  binomfallfaclem2  14071  binomrisefac  14073  fallfacval4  14074  bpolydiflem  14085  ruclem10  14269  divalglem9  14357  divalgmod  14362  bitsfzolem  14382  bitsfzo  14383  bitsmod  14384  bitsfi  14385  bitsinv1lem  14389  sadcaddlem  14405  sadadd3  14409  sadaddlem  14414  sadadd  14415  sadasslem  14418  sadass  14419  sadeq  14420  bitsres  14421  bitsuz  14422  bitsshft  14423  smuval2  14430  smupvallem  14431  smupval  14436  smueqlem  14438  smumullem  14440  smumul  14441  gcdcllem1  14447  gcd0id  14461  gcdneg  14464  modgcd  14474  bezoutlem4  14480  dvdsgcdb  14483  gcdass  14484  mulgcd  14485  gcdeq  14491  dvdsmulgcd  14493  nn0seqcvgd  14500  algfx  14510  eucalginv  14514  eucalg  14517  gcddvdslcm  14538  lcmneg  14539  lcmgcdlem  14542  lcmdvds  14544  lcmgcdeq  14548  lcmdvdsb  14549  lcmass  14550  lcmftp  14580  lcmfunsnlem1  14581  lcmfunsnlem2lem1  14582  lcmfunsnlem2lem2  14583  lcmfunsnlem2  14584  lcmfdvdsb  14587  lcmfun  14589  lcmfass  14590  sqnprm  14617  mulgcddvds  14632  rpmulgcd2  14633  qredeu  14635  divnumden  14668  powm2modprm  14717  coprimeprodsq  14722  iserodd  14748  pclem  14751  pcpre1  14755  pcpremul  14756  pcqcl  14769  pcdvdsb  14781  pcidlem  14784  pc2dvds  14791  pcprmpw2  14794  pcadd  14797  pcfac  14807  pcbc  14808  pockthlem  14812  prmreclem2  14824  prmreclem3  14825  mul4sqlem  14860  4sqlem11  14862  4sqlem12  14863  4sqlem14OLD  14865  4sqlem14  14871  vdwapun  14887  prmgaplcmlem1  14972  lagsubg  16830  psgnuni  17091  psgnran  17107  odmodnn0  17131  mndodconglem  17132  mndodcong  17133  odmulg2  17144  odmulg  17145  odmulgeq  17146  odbezout  17147  odinv  17150  odf1  17151  gexod  17173  gexdvds3  17177  sylow1lem1  17185  sylow1lem3  17187  pgpfi  17192  pgpssslw  17201  sylow2alem2  17205  sylow2blem3  17209  fislw  17212  sylow3lem4  17217  sylow3lem6  17219  efginvrel2  17312  efgredlemf  17326  efgredlemd  17329  efgredlemc  17330  efgredlem  17332  efgcpbllemb  17340  odadd1  17421  odadd2  17422  gexexlem  17425  gexex  17426  torsubg  17427  lt6abl  17464  gsummulg  17510  ablfacrplem  17633  ablfacrp  17634  ablfacrp2  17635  ablfac1b  17638  ablfac1c  17639  ablfac1eulem  17640  ablfac1eu  17641  pgpfac1lem2  17643  pgpfaclem1  17649  ablfaclem3  17655  srgbinomlem3  17710  srgbinomlem4  17711  psrbaglefi  18531  chrid  19029  znunit  19065  psgnghm  19079  chfacfscmulfsupp  19814  chfacfpmmulfsupp  19818  cpmadugsumlemF  19831  dyadss  22429  dyaddisjlem  22430  ply1divex  22962  ply1termlem  23025  plyeq0lem  23032  plyaddlem1  23035  plymullem1  23036  coeeulem  23046  coeidlem  23059  coeeq2  23064  coemulhi  23076  dvply1  23105  dvply2g  23106  plydivex  23118  elqaalem2  23141  aareccl  23147  aannenlem1  23149  aalioulem1  23153  taylplem1  23183  taylplem2  23184  taylpfval  23185  dvtaylp  23190  taylthlem2  23194  dvradcnv  23241  abelthlem7  23258  cxpeq  23562  birthdaylem2  23743  ftalem1  23862  basellem3  23872  isppw2  23905  isnsqf  23925  mule1  23938  ppinncl  23964  musum  23983  chtublem  24002  pclogsum  24006  vmasum  24007  dchrabs  24051  bcmax  24069  bposlem1  24075  bposlem6  24080  lgsval2lem  24097  lgsmod  24112  lgsdirprm  24120  lgsne0  24124  lgseisenlem1  24140  lgseisenlem2  24141  lgseisenlem3  24142  lgseisenlem4  24143  lgsquadlem1  24145  m1lgs  24153  2sqlem8  24163  chebbnd1lem1  24170  dchrisumlem1  24190  dchrisum0flblem1  24209  selberg2lem  24251  ostth2lem2  24335  ostth2lem3  24336  wwlknredwwlkn0  25300  wwlkextproplem2  25315  clwwlkndivn  25410  nbhashuvtx1  25488  eupath2lem3  25552  eupath2  25553  numclwwlkovf2ex  25659  numclwwlk5  25685  numclwwlk6  25686  ex-ind-dvds  25744  gxnn0mul  25850  nndiffz1  28202  2sqcoprm  28246  2sqmod  28247  archirng  28343  archirngz  28344  archiabllem1a  28346  madjusmdetlem4  28495  qqhval2lem  28624  oddpwdc  29013  eulerpartlems  29019  eulerpartlemb  29027  sseqfv1  29048  sseqfn  29049  sseqmw  29050  sseqf  29051  sseqfv2  29053  sseqp1  29054  eluzmn  29211  ccatmulgnn0dir  29216  ofccat  29217  signsplypnf  29227  signsply0  29228  signslema  29239  signstfvn  29246  signstfvp  29248  signstfvc  29251  subfacval3  29700  bcprod  30161  bccolsum  30162  fwddifnp1  30717  poimirlem3  31647  poimirlem4  31648  poimirlem6  31650  poimirlem13  31657  poimirlem14  31658  poimirlem17  31661  poimirlem21  31665  poimirlem22  31666  poimirlem23  31667  poimirlem24  31668  poimirlem26  31670  poimirlem27  31671  poimirlem31  31675  geomcau  31792  eldioph2lem1  35311  pellexlem5  35387  congrep  35529  bezoutr  35541  bezoutr1  35542  jm2.18  35549  jm2.19lem1  35550  jm2.19lem2  35551  jm2.19  35554  jm2.22  35556  jm2.23  35557  jm2.20nn  35558  jm2.25  35560  jm2.26a  35561  jm2.26lem3  35562  jm2.26  35563  jm2.27a  35566  jm2.27b  35567  jm2.27c  35568  jm3.1  35581  expdiophlem1  35582  hbtlem5  35693  radcnvrat  36300  nzin  36304  bccbc  36331  binomcxplemnn0  36335  binomcxplemnotnn0  36342  fprodexp  37246  mccllem  37249  ioodvbdlimc1lem2  37376  ioodvbdlimc2lem  37378  dvnxpaek  37386  dvnmul  37387  dvnprodlem1  37390  dvnprodlem2  37391  wallispilem1  37496  wallispilem5  37500  stirlinglem3  37507  stirlinglem5  37509  stirlinglem7  37511  stirlinglem8  37512  fourierdlem102  37640  fourierdlem114  37652  sqwvfoura  37660  elaa2lem  37665  etransclem10  37676  etransclem20  37686  etransclem21  37687  etransclem22  37688  etransclem23  37689  etransclem24  37690  etransclem27  37693  etransclem28  37694  etransclem35  37701  etransclem38  37704  etransclem44  37710  etransclem45  37711  etransclem46  37712  gcdzeq  38183  pfxtrcfv0  38333  pfxtrcfvl  38336  pfxccat1  38341  pfxccatin12  38356  pfxccatpfx2  38359  pfxccat3a  38360  fsummmodsnunz  38418  ssnn0ssfz  38890  altgsumbcALT  38894  flnn0ohalf  39102  dig2nn1st  39177  0dig2nn0o  39185  aacllem  39301
  Copyright terms: Public domain W3C validator