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

Theorem nn0zd 11072
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 10992 . 2  |-  NN0  C_  ZZ
2 nn0zd.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3442 1  |-  ( ph  ->  A  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   NN0cn0 10903   ZZcz 10971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-nn 10643  df-n0 10904  df-z 10972
This theorem is referenced by:  nnzd  11073  elfz0addOLD  11927  difelfznle  11941  zmodfz  12156  expnegz  12344  expaddzlem  12353  expaddz  12354  expmulz  12356  faclbnd  12513  bcpasc  12544  hashf1  12659  fz1isolem  12663  hashge2el2dif  12676  hashtpg  12680  wrdffz  12730  wrdsymb0  12743  wrdlenge1n0  12744  ccatcl  12762  ccatval3  12766  ccatsymb  12769  ccatass  12774  ccatrn  12775  lswccatn0lsw  12776  ccats1val2  12803  swrdnd  12831  swrdtrcfv0  12841  swrdtrcfvl  12849  swrdccat1  12856  swrdccat2  12857  swrdccatin2  12886  swrdccatin12  12890  splfv2a  12906  splval2  12907  revcl  12909  revccat  12914  revrev  12915  cshwmodn  12940  cshwsublen  12941  cshwn  12942  cshwidxmod  12948  2cshwid  12956  3cshw  12960  cshweqdif2  12961  revco  12974  ccatco  12975  ccat2s1fvwALT  13085  zabscl  13431  absrdbnd  13459  iseraltlem3  13805  fsum0diaglem  13892  modfsummods  13908  binomlem  13942  binom1p  13944  incexc2  13951  climcndslem1  13962  geoser  13980  geolim2  13982  mertenslem1  13995  mertenslem2  13996  mertens  13997  binomfallfaclem2  14148  binomrisefac  14150  fallfacval4  14151  bpolydiflem  14162  ruclem10  14346  divalglem9  14436  divalglem9OLD  14437  divalgmod  14442  bitsfzolem  14462  bitsfzolemOLD  14463  bitsfzo  14464  bitsmod  14465  bitsfi  14466  bitsinv1lem  14470  sadcaddlem  14486  sadadd3  14490  sadaddlem  14495  sadadd  14496  sadasslem  14499  sadass  14500  sadeq  14501  bitsres  14502  bitsuz  14503  bitsshft  14504  smuval2  14511  smupvallem  14512  smupval  14517  smueqlem  14519  smumullem  14521  smumul  14522  gcdcllem1  14528  gcd0id  14542  gcdneg  14545  modgcd  14555  bezoutlem4OLD  14561  bezoutlem4  14564  dvdsgcdb  14567  gcdass  14568  mulgcd  14569  gcdeq  14575  dvdsmulgcd  14577  nn0seqcvgd  14584  algfx  14594  eucalginv  14598  eucalg  14601  gcddvdslcm  14622  lcmneg  14623  lcmgcdlem  14626  lcmdvds  14628  lcmgcdeq  14632  lcmdvdsb  14633  lcmass  14634  lcmftp  14664  lcmfunsnlem1  14665  lcmfunsnlem2lem1  14666  lcmfunsnlem2lem2  14667  lcmfunsnlem2  14668  lcmfdvdsb  14671  lcmfun  14673  lcmfass  14674  sqnprm  14701  mulgcddvds  14716  rpmulgcd2  14717  qredeu  14719  divnumden  14752  powm2modprm  14809  coprimeprodsq  14814  iserodd  14840  pclem  14843  pcpre1  14847  pcpremul  14848  pcqcl  14861  pcdvdsb  14873  pcidlem  14876  pc2dvds  14883  pcprmpw2  14886  pcadd  14889  pcfac  14899  pcbc  14900  pockthlem  14904  prmreclem2  14916  prmreclem3  14917  mul4sqlem  14952  4sqlem11  14954  4sqlem12  14955  4sqlem14OLD  14957  4sqlem14  14963  vdwapun  14979  prmgaplcmlem1  15064  lagsubg  16934  psgnuni  17195  psgnran  17211  odmodnn0  17244  mndodconglem  17245  mndodcong  17246  odmulg2  17261  odmulg  17262  odmulgeq  17263  odbezout  17264  odinv  17267  odf1  17268  gexod  17293  gexdvds3  17297  sylow1lem1  17305  sylow1lem3  17307  pgpfi  17312  pgpssslw  17321  sylow2alem2  17325  sylow2blem3  17329  fislw  17332  sylow3lem4  17337  sylow3lem6  17339  efginvrel2  17432  efgredlemf  17446  efgredlemd  17449  efgredlemc  17450  efgredlem  17452  efgcpbllemb  17460  odadd1  17541  odadd2  17542  gexexlem  17545  gexex  17546  torsubg  17547  lt6abl  17584  gsummulg  17630  ablfacrplem  17753  ablfacrp  17754  ablfacrp2  17755  ablfac1b  17758  ablfac1c  17759  ablfac1eulem  17760  ablfac1eu  17761  pgpfac1lem2  17763  pgpfaclem1  17769  ablfaclem3  17775  srgbinomlem3  17830  srgbinomlem4  17831  psrbaglefi  18651  chrid  19153  znunit  19189  psgnghm  19203  chfacfscmulfsupp  19938  chfacfpmmulfsupp  19942  cpmadugsumlemF  19955  dyadss  22608  dyaddisjlem  22609  ply1divex  23143  ply1termlem  23213  plyeq0lem  23220  plyaddlem1  23223  plymullem1  23224  coeeulem  23234  coeidlem  23247  coeeq2  23252  coemulhi  23264  dvply1  23293  dvply2g  23294  plydivex  23306  elqaalem2  23329  elqaalem2OLD  23332  aareccl  23338  aannenlem1  23340  aalioulem1  23344  taylplem1  23374  taylplem2  23375  taylpfval  23376  dvtaylp  23381  taylthlem2  23385  dvradcnv  23432  abelthlem7  23449  cxpeq  23753  birthdaylem2  23934  ftalem1  24053  basellem3  24065  isppw2  24098  isnsqf  24118  mule1  24131  ppinncl  24157  musum  24176  chtublem  24195  pclogsum  24199  vmasum  24200  dchrabs  24244  bcmax  24262  bposlem1  24268  bposlem6  24273  lgsval2lem  24290  lgsmod  24305  lgsdirprm  24313  lgsne0  24317  lgseisenlem1  24333  lgseisenlem2  24334  lgseisenlem3  24335  lgseisenlem4  24336  lgsquadlem1  24338  m1lgs  24346  2sqlem8  24356  chebbnd1lem1  24363  dchrisumlem1  24383  dchrisum0flblem1  24402  selberg2lem  24444  ostth2lem2  24528  ostth2lem3  24529  wwlknredwwlkn0  25511  wwlkextproplem2  25526  clwwlkndivn  25621  nbhashuvtx1  25699  eupath2lem3  25763  eupath2  25764  numclwwlkovf2ex  25870  numclwwlk5  25896  numclwwlk6  25897  ex-ind-dvds  25955  gxnn0mul  26061  nndiffz1  28418  2sqcoprm  28460  2sqmod  28461  archirng  28556  archirngz  28557  archiabllem1a  28559  madjusmdetlem4  28707  qqhval2lem  28836  oddpwdc  29237  eulerpartlems  29243  eulerpartlemb  29251  sseqfv1  29272  sseqfn  29273  sseqmw  29274  sseqf  29275  sseqfv2  29277  sseqp1  29278  eluzmn  29473  ccatmulgnn0dir  29478  ofccat  29479  signsplypnf  29489  signsply0  29490  signslema  29501  signstfvn  29508  signstfvp  29510  signstfvc  29513  subfacval3  29962  bcprod  30424  bccolsum  30425  fwddifnp1  30982  poimirlem3  31989  poimirlem4  31990  poimirlem6  31992  poimirlem13  31999  poimirlem14  32000  poimirlem17  32003  poimirlem21  32007  poimirlem22  32008  poimirlem23  32009  poimirlem24  32010  poimirlem26  32012  poimirlem27  32013  poimirlem31  32017  geomcau  32134  eldioph2lem1  35648  pellexlem5  35723  congrep  35869  bezoutr  35881  bezoutr1  35882  jm2.18  35889  jm2.19lem1  35890  jm2.19lem2  35891  jm2.19  35894  jm2.22  35896  jm2.23  35897  jm2.20nn  35898  jm2.25  35900  jm2.26a  35901  jm2.26lem3  35902  jm2.26  35903  jm2.27a  35906  jm2.27b  35907  jm2.27c  35908  jm3.1  35921  expdiophlem1  35922  hbtlem5  36033  radcnvrat  36708  nzin  36712  bccbc  36739  binomcxplemnn0  36743  binomcxplemnotnn0  36750  fprodexp  37760  mccllem  37763  ioodvbdlimc1lem2  37890  ioodvbdlimc1lem2OLD  37892  ioodvbdlimc2lem  37894  ioodvbdlimc2lemOLD  37895  dvnxpaek  37903  dvnmul  37904  dvnprodlem1  37907  dvnprodlem2  37908  wallispilem1  38028  wallispilem5  38032  stirlinglem3  38039  stirlinglem5  38041  stirlinglem7  38043  stirlinglem8  38044  fourierdlem102  38173  fourierdlem114  38185  sqwvfoura  38193  elaa2lem  38198  elaa2lemOLD  38199  etransclem10  38210  etransclem20  38220  etransclem21  38221  etransclem22  38222  etransclem23  38223  etransclem24  38224  etransclem27  38227  etransclem28  38228  etransclem35  38235  etransclem38  38238  etransclem44  38244  etransclem45  38245  etransclem46  38246  sge0ad2en  38376  gcdzeq  38928  pfxtrcfv0  39080  pfxtrcfvl  39083  pfxccat1  39088  pfxccatin12  39103  pfxccatpfx2  39106  pfxccat3a  39107  fsummmodsnunz  39236  seqvtx1wlk  39778  red1wlklem  39812  1wlkdlem1  39821  pthdlem1  39888  ssnn0ssfz  40499  altgsumbcALT  40503  flnn0ohalf  40710  dig2nn1st  40785  0dig2nn0o  40793  aacllem  40909
  Copyright terms: Public domain W3C validator