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

Theorem nn0zd 10733
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 10655 . 2  |-  NN0  C_  ZZ
2 nn0zd.1 . 2  |-  ( ph  ->  A  e.  NN0 )
31, 2sseldi 3342 1  |-  ( ph  ->  A  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   NN0cn0 10567   ZZcz 10634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-om 6466  df-recs 6818  df-rdg 6852  df-er 7089  df-en 7299  df-dom 7300  df-sdom 7301  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-nn 10311  df-n0 10568  df-z 10635
This theorem is referenced by:  nnzd  10734  elfzelfzadd  11493  zmodfz  11713  expnegz  11882  expaddzlem  11891  expaddz  11892  expmulz  11894  faclbnd  12050  bcpasc  12081  hashge2el2dif  12168  hashtpg  12170  hashf1  12194  fz1isolem  12198  ccatcl  12258  ccatval1  12260  ccatval3  12262  ccatsymb  12265  ccatass  12270  lswccatn0lsw  12271  ccats1val2  12291  swrdtrcfv0  12322  swrdtrcfvl  12328  swrdccat1  12335  swrdccat2  12336  swrdccatin2  12362  swrdccatin12  12366  splfv2a  12382  splval2  12383  revcl  12385  revccat  12390  revrev  12391  cshwmodn  12416  cshwsublen  12417  cshwn  12418  cshwidxmod  12424  2cshwid  12432  3cshw  12436  cshweqdif2  12437  revco  12446  ccatco  12447  nnabscl  12797  absrdbnd  12813  iseraltlem3  13145  fsum0diaglem  13227  binomlem  13275  binom1p  13277  incexc2  13284  climcndslem1  13295  geoser  13312  geolim2  13314  mertenslem1  13327  mertenslem2  13328  mertens  13329  ruclem10  13504  divalglem9  13588  divalgmod  13593  bitsfzolem  13613  bitsfzo  13614  bitsmod  13615  bitsfi  13616  bitsinv1lem  13620  sadcaddlem  13636  sadadd3  13640  sadaddlem  13645  sadadd  13646  sadasslem  13649  sadass  13650  sadeq  13651  bitsres  13652  bitsuz  13653  bitsshft  13654  smuval2  13661  smupvallem  13662  smupval  13667  smueqlem  13669  smumullem  13671  smumul  13672  gcdcllem1  13678  gcd0id  13690  gcdneg  13693  gcdabs2  13702  modgcd  13703  bezoutlem4  13708  dvdsgcdb  13711  gcdass  13712  mulgcd  13713  absmulgcd  13714  gcdeq  13719  dvdsmulgcd  13721  nn0seqcvgd  13728  algfx  13738  eucalginv  13742  eucalg  13745  sqnprm  13767  mulgcddvds  13773  rpmulgcd2  13774  qredeu  13776  divnumden  13809  coprimeprodsq  13859  iserodd  13885  pclem  13888  pcpre1  13892  pcpremul  13893  pcqcl  13906  pcdvdsb  13918  pcidlem  13921  pc2dvds  13928  pcprmpw2  13931  pcadd  13934  pcfac  13944  pcbc  13945  pockthlem  13949  prmreclem2  13961  prmreclem3  13962  mul4sqlem  13997  4sqlem11  13999  4sqlem12  14000  4sqlem14  14002  vdwapun  14018  lagsubg  15723  psgnuni  15985  psgnran  16001  odmodnn0  16023  mndodconglem  16024  mndodcong  16025  odmulg2  16036  odmulg  16037  odmulgeq  16038  odbezout  16039  odinv  16042  odf1  16043  gexod  16065  gexdvds3  16069  sylow1lem1  16077  sylow1lem3  16079  pgpfi  16084  pgpssslw  16093  sylow2alem2  16097  sylow2blem3  16101  fislw  16104  sylow3lem4  16109  sylow3lem6  16111  efginvrel2  16204  efgredlemf  16218  efgredlemd  16221  efgredlemc  16222  efgredlem  16224  efgcpbllemb  16232  odadd1  16310  odadd2  16311  gexexlem  16314  gexex  16315  torsubg  16316  lt6abl  16351  gsummulg  16414  ablfacrplem  16540  ablfacrp  16541  ablfacrp2  16542  ablfac1b  16545  ablfac1c  16546  ablfac1eulem  16547  ablfac1eu  16548  pgpfac1lem2  16550  pgpfaclem1  16556  ablfaclem3  16562  psrbaglefi  17375  psrbaglefiOLD  17376  chrid  17800  znunit  17838  psgnghm  17852  dyadss  20916  dyaddisjlem  20917  ply1divex  21493  ply1termlem  21556  plyeq0lem  21563  plyaddlem1  21566  plymullem1  21567  coeeulem  21577  coeidlem  21590  coeeq2  21595  coemulhi  21606  dvply1  21635  dvply2g  21636  plydivex  21648  elqaalem2  21671  aareccl  21677  aannenlem1  21679  aalioulem1  21683  taylplem1  21713  taylplem2  21714  taylpfval  21715  dvtaylp  21720  taylthlem2  21724  dvradcnv  21771  abelthlem7  21788  cxpeq  22080  birthdaylem2  22231  ftalem1  22295  basellem3  22305  isppw2  22338  isnsqf  22358  mule1  22371  ppinncl  22397  musum  22416  chtublem  22435  pclogsum  22439  vmasum  22440  dchrabs  22484  bcmax  22502  bposlem1  22508  bposlem6  22513  lgsval2lem  22530  lgsmod  22545  lgsdirprm  22553  lgsne0  22557  lgseisenlem1  22573  lgseisenlem2  22574  lgseisenlem3  22575  lgseisenlem4  22576  lgsquadlem1  22578  m1lgs  22586  2sqlem8  22596  chebbnd1lem1  22603  dchrisumlem1  22623  dchrisum0flblem1  22642  selberg2lem  22684  ostth2lem2  22768  ostth2lem3  22769  eupath2lem3  23423  eupath2  23424  gxnn0mul  23587  nndiffz1  25898  archirng  26029  archiabllem1a  26032  qqhval2lem  26264  oddpwdc  26585  eulerpartlems  26591  eulerpartlemb  26599  sseqfv1  26620  sseqfn  26621  sseqmw  26622  sseqf  26623  sseqfv2  26625  sseqp1  26626  eluzmn  26783  ccatmulgnn0dir  26788  ofccat  26789  signsplypnf  26799  signsply0  26800  signslema  26811  signstfvn  26818  signstfvp  26820  signstfvc  26823  subfacval3  26925  binomfallfaclem2  27390  binomrisefac  27392  fallfacval4  27393  bpolydiflem  28044  geomcau  28499  eldioph2lem1  28943  pellexlem5  29019  congrep  29161  bezoutr  29173  bezoutr1  29174  zabscl  29176  jm2.18  29182  jm2.19lem1  29183  jm2.19lem2  29184  jm2.19  29187  jm2.22  29189  jm2.23  29190  jm2.20nn  29191  jm2.25  29193  jm2.26a  29194  jm2.26lem3  29195  jm2.26  29196  jm2.27a  29199  jm2.27b  29200  jm2.27c  29201  jm3.1  29214  expdiophlem1  29215  hbtlem5  29329  wallispilem1  29706  wallispilem5  29710  stirlinglem3  29717  stirlinglem5  29719  stirlinglem7  29721  stirlinglem8  29722  stirlinglem10  29724  fsummmodsnunre  30089  modfsummods  30090  powm2modprm  30094  ccat2s1fvw  30117  wwlknredwwlkn0  30205  difelfznle  30334  clwwlkndivn  30357  wwlkextproplem2  30407  numclwwlkovf2ex  30525  numclwwlk5  30551  numclwwlk6  30552
  Copyright terms: Public domain W3C validator