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

Theorem nn0zd 10960
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 10881 . 2  |-  NN0  C_  ZZ
2 nn0zd.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3502 1  |-  ( ph  ->  A  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   NN0cn0 10791   ZZcz 10860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-recs 7039  df-rdg 7073  df-er 7308  df-en 7514  df-dom 7515  df-sdom 7516  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-nn 10533  df-n0 10792  df-z 10861
This theorem is referenced by:  nnzd  10961  elfz0add  11770  difelfznle  11782  zmodfz  11980  expnegz  12162  expaddzlem  12171  expaddz  12172  expmulz  12174  faclbnd  12330  bcpasc  12361  hashf1  12466  fz1isolem  12470  hashge2el2dif  12481  hashtpg  12483  ccatcl  12552  ccatval1  12554  ccatval3  12556  ccatsymb  12559  ccatass  12564  lswccatn0lsw  12565  ccats1val2  12588  ccat2s1fvw  12599  swrdtrcfv0  12626  swrdtrcfvl  12632  swrdccat1  12639  swrdccat2  12640  swrdccatin2  12669  swrdccatin12  12673  splfv2a  12689  splval2  12690  revcl  12692  revccat  12697  revrev  12698  cshwmodn  12723  cshwsublen  12724  cshwn  12725  cshwidxmod  12731  2cshwid  12739  3cshw  12743  cshweqdif2  12744  revco  12757  ccatco  12758  ccat2s1fvwALT  12850  nnabscl  13114  absrdbnd  13130  iseraltlem3  13462  fsum0diaglem  13547  modfsummods  13563  binomlem  13597  binom1p  13599  incexc2  13606  climcndslem1  13617  geoser  13634  geolim2  13636  mertenslem1  13649  mertenslem2  13650  mertens  13651  ruclem10  13826  divalglem9  13911  divalgmod  13916  bitsfzolem  13936  bitsfzo  13937  bitsmod  13938  bitsfi  13939  bitsinv1lem  13943  sadcaddlem  13959  sadadd3  13963  sadaddlem  13968  sadadd  13969  sadasslem  13972  sadass  13973  sadeq  13974  bitsres  13975  bitsuz  13976  bitsshft  13977  smuval2  13984  smupvallem  13985  smupval  13990  smueqlem  13992  smumullem  13994  smumul  13995  gcdcllem1  14001  gcd0id  14013  gcdneg  14016  gcdabs2  14025  modgcd  14026  bezoutlem4  14031  dvdsgcdb  14034  gcdass  14035  mulgcd  14036  absmulgcd  14037  gcdeq  14042  dvdsmulgcd  14044  nn0seqcvgd  14051  algfx  14061  eucalginv  14065  eucalg  14068  sqnprm  14091  mulgcddvds  14097  rpmulgcd2  14098  qredeu  14100  divnumden  14133  powm2modprm  14180  coprimeprodsq  14185  iserodd  14211  pclem  14214  pcpre1  14218  pcpremul  14219  pcqcl  14232  pcdvdsb  14244  pcidlem  14247  pc2dvds  14254  pcprmpw2  14257  pcadd  14260  pcfac  14270  pcbc  14271  pockthlem  14275  prmreclem2  14287  prmreclem3  14288  mul4sqlem  14323  4sqlem11  14325  4sqlem12  14326  4sqlem14  14328  vdwapun  14344  lagsubg  16055  psgnuni  16317  psgnran  16333  odmodnn0  16357  mndodconglem  16358  mndodcong  16359  odmulg2  16370  odmulg  16371  odmulgeq  16372  odbezout  16373  odinv  16376  odf1  16377  gexod  16399  gexdvds3  16403  sylow1lem1  16411  sylow1lem3  16413  pgpfi  16418  pgpssslw  16427  sylow2alem2  16431  sylow2blem3  16435  fislw  16438  sylow3lem4  16443  sylow3lem6  16445  efginvrel2  16538  efgredlemf  16552  efgredlemd  16555  efgredlemc  16556  efgredlem  16558  efgcpbllemb  16566  odadd1  16644  odadd2  16645  gexexlem  16648  gexex  16649  torsubg  16650  lt6abl  16685  gsummulg  16753  ablfacrplem  16903  ablfacrp  16904  ablfacrp2  16905  ablfac1b  16908  ablfac1c  16909  ablfac1eulem  16910  ablfac1eu  16911  pgpfac1lem2  16913  pgpfaclem1  16919  ablfaclem3  16925  srgbinomlem3  16978  srgbinomlem4  16979  psrbaglefi  17791  psrbaglefiOLD  17792  chrid  18328  znunit  18366  psgnghm  18380  chfacfscmulfsupp  19124  chfacfpmmulfsupp  19128  cpmadugsumlemF  19141  dyadss  21735  dyaddisjlem  21736  ply1divex  22269  ply1termlem  22332  plyeq0lem  22339  plyaddlem1  22342  plymullem1  22343  coeeulem  22353  coeidlem  22366  coeeq2  22371  coemulhi  22382  dvply1  22411  dvply2g  22412  plydivex  22424  elqaalem2  22447  aareccl  22453  aannenlem1  22455  aalioulem1  22459  taylplem1  22489  taylplem2  22490  taylpfval  22491  dvtaylp  22496  taylthlem2  22500  dvradcnv  22547  abelthlem7  22564  cxpeq  22856  birthdaylem2  23007  ftalem1  23071  basellem3  23081  isppw2  23114  isnsqf  23134  mule1  23147  ppinncl  23173  musum  23192  chtublem  23211  pclogsum  23215  vmasum  23216  dchrabs  23260  bcmax  23278  bposlem1  23284  bposlem6  23289  lgsval2lem  23306  lgsmod  23321  lgsdirprm  23329  lgsne0  23333  lgseisenlem1  23349  lgseisenlem2  23350  lgseisenlem3  23351  lgseisenlem4  23352  lgsquadlem1  23354  m1lgs  23362  2sqlem8  23372  chebbnd1lem1  23379  dchrisumlem1  23399  dchrisum0flblem1  23418  selberg2lem  23460  ostth2lem2  23544  ostth2lem3  23545  wwlknredwwlkn0  24400  wwlkextproplem2  24415  clwwlkndivn  24510  eupath2lem3  24652  eupath2  24653  numclwwlkovf2ex  24760  numclwwlk5  24786  numclwwlk6  24787  gxnn0mul  24952  nndiffz1  27261  archirng  27391  archiabllem1a  27394  qqhval2lem  27595  oddpwdc  27930  eulerpartlems  27936  eulerpartlemb  27944  sseqfv1  27965  sseqfn  27966  sseqmw  27967  sseqf  27968  sseqfv2  27970  sseqp1  27971  eluzmn  28128  ccatmulgnn0dir  28133  ofccat  28134  signsplypnf  28144  signsply0  28145  signslema  28156  signstfvn  28163  signstfvp  28165  signstfvc  28168  subfacval3  28270  binomfallfaclem2  28736  binomrisefac  28738  fallfacval4  28739  bpolydiflem  29390  geomcau  29853  eldioph2lem1  30295  pellexlem5  30371  congrep  30513  bezoutr  30525  bezoutr1  30526  zabscl  30528  jm2.18  30534  jm2.19lem1  30535  jm2.19lem2  30536  jm2.19  30539  jm2.22  30541  jm2.23  30542  jm2.20nn  30543  jm2.25  30545  jm2.26a  30546  jm2.26lem3  30547  jm2.26  30548  jm2.27a  30551  jm2.27b  30552  jm2.27c  30553  jm3.1  30566  expdiophlem1  30567  hbtlem5  30681  gcddvdslcm  30808  lcmneg  30809  lcmgcdlem  30812  lcmdvds  30814  lcmgcdeq  30816  lcmdvdsb  30817  lcmass  30818  nzin  30823  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  iblsplit  31284  wallispilem1  31365  wallispilem5  31369  stirlinglem3  31376  stirlinglem5  31378  stirlinglem7  31380  stirlinglem8  31381  stirlinglem10  31383  fourierdlem48  31455  fourierdlem64  31471  fourierdlem102  31509  fourierdlem114  31521  sqwvfoura  31529  fsummmodsnunz  31817  ssnn0ssfz  32002  altgsumbcALT  32006
  Copyright terms: Public domain W3C validator