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

Theorem nn0zd 10298
Description: A natural number 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 10227 . 2  |-  NN0  C_  ZZ
2 nn0zd.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3282 1  |-  ( ph  ->  A  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   NN0cn0 10146   ZZcz 10207
This theorem is referenced by:  nnzd  10299  zmodfz  11188  expnegz  11334  expaddzlem  11343  expaddz  11344  expmulz  11346  faclbnd  11501  bcpasc  11532  hashtpg  11611  hashf1  11626  fz1isolem  11630  ccatcl  11663  ccatval1  11665  ccatval3  11667  ccatass  11670  swrdccat1  11694  swrdccat2  11695  splfv2a  11705  splval2  11706  revcl  11713  revccat  11718  revrev  11719  revco  11723  ccatco  11724  nnabscl  12049  absrdbnd  12065  iseraltlem3  12397  fsum0diaglem  12480  binomlem  12528  binom1p  12530  incexc2  12538  climcndslem1  12549  geoser  12566  geolim2  12568  mertenslem1  12581  mertenslem2  12582  mertens  12583  ruclem10  12758  divalglem9  12841  divalgmod  12846  bitsfzolem  12866  bitsfzo  12867  bitsmod  12868  bitsfi  12869  bitsinv1lem  12873  sadcaddlem  12889  sadadd3  12893  sadaddlem  12898  sadadd  12899  sadasslem  12902  sadass  12903  sadeq  12904  bitsres  12905  bitsuz  12906  bitsshft  12907  smuval2  12914  smupvallem  12915  smupval  12920  smueqlem  12922  smumullem  12924  smumul  12925  gcdcllem1  12931  gcd0id  12943  gcdneg  12946  gcdabs2  12955  modgcd  12956  bezoutlem4  12961  dvdsgcdb  12964  gcdass  12965  mulgcd  12966  absmulgcd  12967  gcdeq  12972  dvdsmulgcd  12974  nn0seqcvgd  12981  algfx  12991  eucalginv  12995  eucalg  12998  sqnprm  13018  mulgcddvds  13024  rpmulgcd2  13025  qredeu  13027  divnumden  13060  coprimeprodsq  13103  iserodd  13129  pclem  13132  pcpre1  13136  pcpremul  13137  pcqcl  13150  pcdvdsb  13162  pcidlem  13165  pc2dvds  13172  pcprmpw2  13175  pcadd  13178  pcfac  13188  pcbc  13189  pockthlem  13193  prmreclem2  13205  prmreclem3  13206  mul4sqlem  13241  4sqlem11  13243  4sqlem12  13244  4sqlem14  13246  vdwapun  13262  lagsubg  14922  odmodnn0  15098  mndodconglem  15099  mndodcong  15100  odmulg2  15111  odmulg  15112  odmulgeq  15113  odbezout  15114  odinv  15117  odf1  15118  gexod  15140  gexdvds3  15144  sylow1lem1  15152  sylow1lem3  15154  pgpfi  15159  pgpssslw  15168  sylow2alem2  15172  sylow2blem3  15176  fislw  15179  sylow3lem4  15184  sylow3lem6  15186  efginvrel2  15279  efgredlemf  15293  efgredlemd  15296  efgredlemc  15297  efgredlem  15299  efgcpbllemb  15307  odadd1  15383  odadd2  15384  gexexlem  15387  gexex  15388  torsubg  15389  lt6abl  15424  gsummulg  15457  ablfacrplem  15543  ablfacrp  15544  ablfacrp2  15545  ablfac1b  15548  ablfac1c  15549  ablfac1eulem  15550  ablfac1eu  15551  pgpfac1lem2  15553  pgpfaclem1  15559  ablfaclem3  15565  psrbaglefi  16357  chrid  16724  znunit  16760  dyadss  19346  dyaddisjlem  19347  ply1divex  19919  ply1termlem  19982  plyeq0lem  19989  plyaddlem1  19992  plymullem1  19993  coeeulem  20003  coeidlem  20016  coeeq2  20021  coemulhi  20032  dvply1  20061  dvply2g  20062  plydivex  20074  elqaalem2  20097  aareccl  20103  aannenlem1  20105  aalioulem1  20109  taylplem1  20139  taylplem2  20140  taylpfval  20141  dvtaylp  20146  taylthlem2  20150  dvradcnv  20197  abelthlem7  20214  cxpeq  20501  birthdaylem2  20651  ftalem1  20715  basellem3  20725  isppw2  20758  isnsqf  20778  mule1  20791  ppinncl  20817  musum  20836  chtublem  20855  pclogsum  20859  vmasum  20860  dchrabs  20904  bcmax  20922  bposlem1  20928  bposlem6  20933  lgsval2lem  20950  lgsmod  20965  lgsdirprm  20973  lgsne0  20977  lgseisenlem1  20993  lgseisenlem2  20994  lgseisenlem3  20995  lgseisenlem4  20996  lgsquadlem1  20998  m1lgs  21006  2sqlem8  21016  chebbnd1lem1  21023  dchrisumlem1  21043  dchrisum0flblem1  21062  selberg2lem  21104  ostth2lem2  21188  ostth2lem3  21189  eupath2lem3  21542  eupath2  21543  gxnn0mul  21706  qqhval2lem  24157  subfacval3  24647  bpolydiflem  25807  geomcau  26149  eldioph2lem1  26502  pellexlem5  26580  congrep  26722  bezoutr  26734  bezoutr1  26735  zabscl  26737  jm2.18  26743  jm2.19lem1  26744  jm2.19lem2  26745  jm2.19  26748  jm2.22  26750  jm2.23  26751  jm2.20nn  26752  jm2.25  26754  jm2.26a  26755  jm2.26lem3  26756  jm2.26  26757  jm2.27a  26760  jm2.27b  26761  jm2.27c  26762  jm3.1  26775  expdiophlem1  26776  hbtlem5  26994  psgnuni  27084  psgnghm  27099  wallispilem1  27475  wallispilem5  27479  stirlinglem3  27486  stirlinglem5  27488  stirlinglem7  27490  stirlinglem8  27491  stirlinglem10  27493
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-sep 4264  ax-nul 4272  ax-pow 4311  ax-pr 4337  ax-un 4634  ax-resscn 8973  ax-1cn 8974  ax-icn 8975  ax-addcl 8976  ax-addrcl 8977  ax-mulcl 8978  ax-mulrcl 8979  ax-mulcom 8980  ax-addass 8981  ax-mulass 8982  ax-distr 8983  ax-i2m1 8984  ax-1ne0 8985  ax-1rid 8986  ax-rnegex 8987  ax-rrecex 8988  ax-cnre 8989  ax-pre-lttri 8990  ax-pre-lttrn 8991  ax-pre-ltadd 8992  ax-pre-mulgt0 8993
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2235  df-mo 2236  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-nel 2546  df-ral 2647  df-rex 2648  df-reu 2649  df-rab 2651  df-v 2894  df-sbc 3098  df-csb 3188  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-pss 3272  df-nul 3565  df-if 3676  df-pw 3737  df-sn 3756  df-pr 3757  df-tp 3758  df-op 3759  df-uni 3951  df-iun 4030  df-br 4147  df-opab 4201  df-mpt 4202  df-tr 4237  df-eprel 4428  df-id 4432  df-po 4437  df-so 4438  df-fr 4475  df-we 4477  df-ord 4518  df-on 4519  df-lim 4520  df-suc 4521  df-om 4779  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5351  df-fun 5389  df-fn 5390  df-f 5391  df-f1 5392  df-fo 5393  df-f1o 5394  df-fv 5395  df-ov 6016  df-oprab 6017  df-mpt2 6018  df-riota 6478  df-recs 6562  df-rdg 6597  df-er 6834  df-en 7039  df-dom 7040  df-sdom 7041  df-pnf 9048  df-mnf 9049  df-xr 9050  df-ltxr 9051  df-le 9052  df-sub 9218  df-neg 9219  df-nn 9926  df-n0 10147  df-z 10208
  Copyright terms: Public domain W3C validator