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

Theorem nn0zd 12073
Description: A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
nn0zd.1 (𝜑𝐴 ∈ ℕ0)
Assertion
Ref Expression
nn0zd (𝜑𝐴 ∈ ℤ)

Proof of Theorem nn0zd
StepHypRef Expression
1 nn0ssz 11991 . 2 0 ⊆ ℤ
2 nn0zd.1 . 2 (𝜑𝐴 ∈ ℕ0)
31, 2sseldi 3940 1 (𝜑𝐴 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  0cn0 11885  cz 11969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-ov 7143  df-om 7566  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-neg 10862  df-nn 11626  df-n0 11886  df-z 11970
This theorem is referenced by:  nnzd  12074  eluzmn  12238  difelfznle  13016  zmodfz  13256  expnegz  13459  expaddzlem  13468  expaddz  13469  expmulz  13471  faclbnd  13646  bcpasc  13677  hashf1  13811  fz1isolem  13815  hashge2el2dif  13834  hashtpg  13839  wrdffz  13878  ffz0iswrd  13884  wrdsymb0  13892  wrdlenge1n0  13893  ccatcl  13917  ccatval3  13924  ccatsymb  13927  ccatval21sw  13930  ccatass  13933  ccatrn  13934  lswccatn0lsw  13936  ccats1val2  13974  swrdnd  14007  swrdccat2  14022  pfxtrcfv0  14047  pfxtrcfvl  14050  pfxccat1  14055  swrdccatin2  14082  pfxccatin12  14086  pfxccatpfx2  14090  pfxccat3a  14091  splfv2a  14109  splval2  14110  revcl  14114  revccat  14119  revrev  14120  cshwmodn  14148  cshwsublen  14149  cshwn  14150  cshwidxmod  14156  2cshwid  14167  3cshw  14171  cshweqdif2  14172  revco  14187  ccatco  14188  ccat2s1fvwALT  14309  ccat2s1fvwALTOLD  14310  ofccat  14320  zabscl  14664  absrdbnd  14692  iseraltlem3  15031  fsum0diaglem  15122  modfsummods  15139  binomlem  15175  binom1p  15177  incexc2  15184  climcndslem1  15195  geoser  15213  pwm1geoser  15215  pwm1geoserOLD  15216  geolim2  15218  mertenslem1  15231  mertenslem2  15232  mertens  15233  binomfallfaclem2  15385  binomrisefac  15387  fallfacval4  15388  bpolydiflem  15399  ruclem10  15583  sumodd  15728  divalglem9  15741  divalgmod  15746  bitsfzolem  15772  bitsfzo  15773  bitsmod  15774  bitsfi  15775  bitsinv1lem  15779  sadcaddlem  15795  sadadd3  15799  sadaddlem  15804  sadadd  15805  sadasslem  15808  sadass  15809  sadeq  15810  bitsres  15811  bitsuz  15812  bitsshft  15813  smuval2  15820  smupvallem  15821  smupval  15826  smueqlem  15828  smumullem  15830  smumul  15831  gcdcllem1  15837  zeqzmulgcd  15848  gcd0id  15856  gcdneg  15859  modgcd  15869  gcdmultipled  15871  bezoutlem4  15879  dvdsgcdb  15882  gcdass  15884  mulgcd  15885  gcdzeq  15891  dvdsmulgcd  15894  bezoutr  15901  bezoutr1  15902  nn0seqcvgd  15903  algfx  15913  eucalginv  15917  eucalg  15920  gcddvdslcm  15935  lcmneg  15936  lcmgcdlem  15939  lcmdvds  15941  lcmgcdeq  15945  lcmdvdsb  15946  lcmass  15947  lcmftp  15969  lcmfunsnlem1  15970  lcmfunsnlem2lem1  15971  lcmfunsnlem2lem2  15972  lcmfunsnlem2  15973  lcmfdvdsb  15976  lcmfun  15978  lcmfass  15979  mulgcddvds  15988  rpmulgcd2  15989  qredeu  15991  divgcdcoprm0  15998  sqnprm  16035  divnumden  16077  powm2modprm  16129  coprimeprodsq  16134  iserodd  16161  pclem  16164  pcpre1  16168  pcpremul  16169  pcqcl  16182  pcdvdsb  16194  pcidlem  16197  pc2dvds  16204  pcprmpw2  16207  dvdsprmpweqle  16211  pcadd  16214  pcfac  16224  pcbc  16225  pockthlem  16230  prmreclem2  16242  prmreclem3  16243  mul4sqlem  16278  4sqlem11  16280  4sqlem12  16281  4sqlem14  16283  vdwapun  16299  prmgaplcmlem1  16376  lagsubg  18333  psgnuni  18618  psgnran  18634  odmodnn0  18659  mndodconglem  18660  mndodcong  18661  odmulg2  18673  odmulg  18674  odmulgeq  18675  odbezout  18676  odinv  18679  odf1  18680  gexod  18702  gexdvds3  18706  sylow1lem1  18714  sylow1lem3  18716  pgpfi  18721  pgpssslw  18730  sylow2alem2  18734  sylow2blem3  18738  fislw  18741  sylow3lem4  18746  sylow3lem6  18748  efginvrel2  18844  efgredlemf  18858  efgredlemd  18861  efgredlemc  18862  efgredlem  18864  efgcpbllemb  18872  odadd1  18959  odadd2  18960  gexexlem  18963  gexex  18964  torsubg  18965  lt6abl  19006  gsummulg  19053  ablfacrplem  19178  ablfacrp  19179  ablfacrp2  19180  ablfac1b  19183  ablfac1c  19184  ablfac1eulem  19185  ablfac1eu  19186  pgpfac1lem2  19188  pgpfaclem1  19194  ablfaclem3  19200  srgbinomlem3  19283  srgbinomlem4  19284  chrid  20217  znunit  20253  psgnghm  20267  psrbaglefi  20608  chfacfscmulfsupp  21462  chfacfpmmulfsupp  21466  cpmadugsumlemF  21479  dyadss  24196  dyaddisjlem  24197  ply1divex  24735  ply1termlem  24798  plyeq0lem  24805  plyaddlem1  24808  plymullem1  24809  coeeulem  24819  coeidlem  24832  coeeq2  24837  coemulhi  24849  dvply1  24878  dvply2g  24879  plydivex  24891  elqaalem2  24914  aareccl  24920  aannenlem1  24922  aalioulem1  24926  taylplem1  24956  taylplem2  24957  taylpfval  24958  dvtaylp  24963  taylthlem2  24967  dvradcnv  25014  abelthlem7  25031  cxpeq  25344  birthdaylem2  25536  ftalem1  25656  basellem3  25666  isppw2  25698  isnsqf  25718  mule1  25731  ppinncl  25757  musum  25774  chtublem  25793  pclogsum  25797  vmasum  25798  dchrabs  25842  bcmax  25860  bposlem1  25866  bposlem6  25871  lgsval2lem  25889  lgsmod  25905  lgsne0  25917  gausslemma2dlem0h  25945  gausslemma2dlem0i  25946  gausslemma2dlem2  25949  gausslemma2dlem6  25954  gausslemma2d  25956  lgseisenlem1  25957  lgseisenlem2  25958  lgseisenlem3  25959  lgseisenlem4  25960  lgsquadlem1  25962  m1lgs  25970  2lgslem1a  25973  2lgslem3a  25978  2lgslem3b  25979  2lgslem3c  25980  2lgslem3d  25981  2lgslem3d1  25985  2lgsoddprmlem2  25991  2sqlem8  26008  2sqcoprm  26017  2sqmod  26018  chebbnd1lem1  26051  dchrisumlem1  26071  dchrisum0flblem1  26090  selberg2lem  26132  ostth2lem2  26216  ostth2lem3  26217  finsumvtxdg2sstep  27337  finsumvtxdgeven  27340  vtxdgoddnumeven  27341  redwlklem  27459  wlkdlem1  27470  pthdlem1  27553  crctcshwlkn0lem4  27597  wwlksnredwwlkn0  27680  wwlksnextproplem2  27694  clwwlkccatlem  27772  clwlkclwwlkfo  27792  clwwlkwwlksb  27837  clwwlkndivn  27863  eupth2lem3lem3  28013  eupth2lem3lem4  28014  eupth2lem3  28019  eupth2lems  28021  numclwwlk5  28171  numclwwlk6  28173  ex-ind-dvds  28244  nndiffz1  30519  prmdvdsbc  30542  ccatf1  30635  pfxlsw2ccat  30636  wrdt2ind  30637  cycpmfv1  30786  cycpmco2lem2  30800  cycpmco2lem3  30801  cycpmco2lem4  30802  cycpmco2lem5  30803  cycpmco2lem6  30804  cycpmco2lem7  30805  cycpmco2  30806  cycpmrn  30816  cyc3genpm  30825  cycpmconjslem2  30828  cyc3conja  30830  archirng  30848  archirngz  30849  archiabllem1a  30851  freshmansdream  30890  madjusmdetlem4  31152  qqhval2lem  31296  oddpwdc  31686  eulerpartlems  31692  eulerpartlemb  31700  sseqfv1  31721  sseqfn  31722  sseqmw  31723  sseqf  31724  sseqfv2  31726  sseqp1  31727  ccatmulgnn0dir  31886  signsplypnf  31894  signsply0  31895  signslema  31906  signstfvn  31913  signstfvp  31915  signstfvc  31918  fsum2dsub  31952  reprinfz1  31967  reprfi2  31968  hashrepr  31970  reprdifc  31972  breprexplema  31975  breprexplemc  31977  circlemeth  31985  circlevma  31987  circlemethhgt  31988  hgt750lema  32002  tgoldbachgtde  32005  lpadlem3  32023  revpfxsfxrev  32436  revwlk  32445  subfacval3  32510  bcprod  33044  bccolsum  33045  fwddifnp1  33700  knoppndvlem6  33930  knoppndvlem7  33931  knoppndvlem10  33934  knoppndvlem14  33938  knoppndvlem15  33939  knoppndvlem16  33940  knoppndvlem17  33941  knoppndvlem19  33943  knoppndvlem21  33945  dfgcd3  34699  poimirlem3  35018  poimirlem4  35019  poimirlem6  35021  poimirlem13  35028  poimirlem14  35029  poimirlem17  35032  poimirlem21  35036  poimirlem22  35037  poimirlem23  35038  poimirlem24  35039  poimirlem26  35041  poimirlem27  35042  poimirlem31  35046  geomcau  35155  bccl2d  39240  lcmineqlem12  39289  lcmineqlem17  39294  3lexlogpow5ineq2  39303  2np3bcnp1  39307  prodsplit  39336  frlmvscadiccat  39386  fltnltalem  39548  eldioph2lem1  39631  pellexlem5  39704  congrep  39844  jm2.18  39859  jm2.19lem1  39860  jm2.19lem2  39861  jm2.19  39864  jm2.22  39866  jm2.23  39867  jm2.20nn  39868  jm2.25  39870  jm2.26a  39871  jm2.26lem3  39872  jm2.26  39873  jm2.27a  39876  jm2.27b  39877  jm2.27c  39878  jm3.1  39891  expdiophlem1  39892  hbtlem5  40002  radcnvrat  40952  nzin  40956  bccbc  40983  binomcxplemnn0  40987  binomcxplemnotnn0  40994  fprodexp  42175  mccllem  42178  ioodvbdlimc1lem2  42513  ioodvbdlimc2lem  42515  dvnxpaek  42523  dvnmul  42524  dvnprodlem1  42527  dvnprodlem2  42528  wallispilem1  42646  wallispilem5  42650  stirlinglem3  42657  stirlinglem5  42659  stirlinglem7  42661  stirlinglem8  42662  fourierdlem102  42789  fourierdlem114  42801  sqwvfoura  42809  elaa2lem  42814  etransclem10  42825  etransclem20  42835  etransclem21  42836  etransclem22  42837  etransclem23  42838  etransclem24  42839  etransclem27  42842  etransclem28  42843  etransclem35  42850  etransclem38  42853  etransclem44  42859  etransclem45  42860  etransclem46  42861  sge0ad2en  43009  fsummmodsnunz  43831  fmtnoge3  43986  fmtnof1  43991  fmtnorec1  43993  sqrtpwpw2p  43994  fmtnodvds  44000  goldbachthlem2  44002  fmtnoprmfac2lem1  44022  lighneallem3  44064  lighneallem4b  44066  lighneallem4  44067  ssnn0ssfz  44690  altgsumbcALT  44694  flnn0ohalf  44887  dig2nn1st  44958  0dig2nn0o  44966  aacllem  45268
  Copyright terms: Public domain W3C validator