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

Theorem nn0zd 11672
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 11590 . 2 0 ⊆ ℤ
2 nn0zd.1 . 2 (𝜑𝐴 ∈ ℕ0)
31, 2sseldi 3742 1 (𝜑𝐴 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  0cn0 11484  cz 11569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-n0 11485  df-z 11570
This theorem is referenced by:  nnzd  11673  eluzmn  11886  difelfznle  12647  zmodfz  12886  expnegz  13088  expaddzlem  13097  expaddz  13098  expmulz  13100  faclbnd  13271  bcpasc  13302  hashf1  13433  fz1isolem  13437  hashge2el2dif  13454  hashtpg  13459  wrdffz  13512  wrdsymb0  13525  wrdlenge1n0  13526  ccatcl  13546  ccatval3  13551  ccatsymb  13554  ccatval21sw  13557  ccatass  13560  ccatrn  13561  lswccatn0lsw  13563  ccats1val2  13601  swrdnd  13632  swrdtrcfv0  13642  swrdtrcfvl  13650  swrdccat1  13657  swrdccat2  13658  swrdccatin2  13687  swrdccatin12  13691  splfv2a  13707  splval2  13708  revcl  13710  revccat  13715  revrev  13716  cshwmodn  13741  cshwsublen  13742  cshwn  13743  cshwidxmod  13749  2cshwid  13760  3cshw  13764  cshweqdif2  13765  revco  13780  ccatco  13781  ccat2s1fvwALT  13899  ofccat  13909  zabscl  14252  absrdbnd  14280  iseraltlem3  14613  fsum0diaglem  14707  modfsummods  14724  binomlem  14760  binom1p  14762  incexc2  14769  climcndslem1  14780  geoser  14798  pwm1geoser  14799  geolim2  14801  mertenslem1  14815  mertenslem2  14816  mertens  14817  binomfallfaclem2  14970  binomrisefac  14972  fallfacval4  14973  bpolydiflem  14984  ruclem10  15167  sumodd  15313  divalglem9  15326  divalgmod  15331  divalgmodOLD  15332  bitsfzolem  15358  bitsfzo  15359  bitsmod  15360  bitsfi  15361  bitsinv1lem  15365  sadcaddlem  15381  sadadd3  15385  sadaddlem  15390  sadadd  15391  sadasslem  15394  sadass  15395  sadeq  15396  bitsres  15397  bitsuz  15398  bitsshft  15399  smuval2  15406  smupvallem  15407  smupval  15412  smueqlem  15414  smumullem  15416  smumul  15417  gcdcllem1  15423  zeqzmulgcd  15434  gcd0id  15442  gcdneg  15445  modgcd  15455  bezoutlem4  15461  dvdsgcdb  15464  gcdass  15466  mulgcd  15467  gcdzeq  15473  dvdsmulgcd  15476  bezoutr  15483  bezoutr1  15484  nn0seqcvgd  15485  algfx  15495  eucalginv  15499  eucalg  15502  gcddvdslcm  15517  lcmneg  15518  lcmgcdlem  15521  lcmdvds  15523  lcmgcdeq  15527  lcmdvdsb  15528  lcmass  15529  lcmftp  15551  lcmfunsnlem1  15552  lcmfunsnlem2lem1  15553  lcmfunsnlem2lem2  15554  lcmfunsnlem2  15555  lcmfdvdsb  15558  lcmfun  15560  lcmfass  15561  mulgcddvds  15571  rpmulgcd2  15572  qredeu  15574  divgcdcoprm0  15581  sqnprm  15616  divnumden  15658  powm2modprm  15710  coprimeprodsq  15715  iserodd  15742  pclem  15745  pcpre1  15749  pcpremul  15750  pcqcl  15763  pcdvdsb  15775  pcidlem  15778  pc2dvds  15785  pcprmpw2  15788  dvdsprmpweqle  15792  pcadd  15795  pcfac  15805  pcbc  15806  pockthlem  15811  prmreclem2  15823  prmreclem3  15824  mul4sqlem  15859  4sqlem11  15861  4sqlem12  15862  4sqlem14  15864  vdwapun  15880  prmgaplcmlem1  15957  lagsubg  17857  psgnuni  18119  psgnran  18135  odmodnn0  18159  mndodconglem  18160  mndodcong  18161  odmulg2  18172  odmulg  18173  odmulgeq  18174  odbezout  18175  odinv  18178  odf1  18179  gexod  18201  gexdvds3  18205  sylow1lem1  18213  sylow1lem3  18215  pgpfi  18220  pgpssslw  18229  sylow2alem2  18233  sylow2blem3  18237  fislw  18240  sylow3lem4  18245  sylow3lem6  18247  efginvrel2  18340  efgredlemf  18354  efgredlemd  18357  efgredlemc  18358  efgredlem  18360  efgcpbllemb  18368  odadd1  18451  odadd2  18452  gexexlem  18455  gexex  18456  torsubg  18457  lt6abl  18496  gsummulg  18542  ablfacrplem  18664  ablfacrp  18665  ablfacrp2  18666  ablfac1b  18669  ablfac1c  18670  ablfac1eulem  18671  ablfac1eu  18672  pgpfac1lem2  18674  pgpfaclem1  18680  ablfaclem3  18686  srgbinomlem3  18742  srgbinomlem4  18743  psrbaglefi  19574  chrid  20077  znunit  20114  psgnghm  20128  chfacfscmulfsupp  20866  chfacfpmmulfsupp  20870  cpmadugsumlemF  20883  dyadss  23562  dyaddisjlem  23563  ply1divex  24095  ply1termlem  24158  plyeq0lem  24165  plyaddlem1  24168  plymullem1  24169  coeeulem  24179  coeidlem  24192  coeeq2  24197  coemulhi  24209  dvply1  24238  dvply2g  24239  plydivex  24251  elqaalem2  24274  aareccl  24280  aannenlem1  24282  aalioulem1  24286  taylplem1  24316  taylplem2  24317  taylpfval  24318  dvtaylp  24323  taylthlem2  24327  dvradcnv  24374  abelthlem7  24391  cxpeq  24697  birthdaylem2  24878  ftalem1  24998  basellem3  25008  isppw2  25040  isnsqf  25060  mule1  25073  ppinncl  25099  musum  25116  chtublem  25135  pclogsum  25139  vmasum  25140  dchrabs  25184  bcmax  25202  bposlem1  25208  bposlem6  25213  lgsval2lem  25231  lgsmod  25247  lgsne0  25259  gausslemma2dlem0h  25287  gausslemma2dlem0i  25288  gausslemma2dlem2  25291  gausslemma2dlem6  25296  gausslemma2d  25298  lgseisenlem1  25299  lgseisenlem2  25300  lgseisenlem3  25301  lgseisenlem4  25302  lgsquadlem1  25304  m1lgs  25312  2lgslem1a  25315  2lgslem3a  25320  2lgslem3b  25321  2lgslem3c  25322  2lgslem3d  25323  2lgslem3d1  25327  2lgsoddprmlem2  25333  2sqlem8  25350  chebbnd1lem1  25357  dchrisumlem1  25377  dchrisum0flblem1  25396  selberg2lem  25438  ostth2lem2  25522  ostth2lem3  25523  finsumvtxdg2sstep  26655  finsumvtxdgeven  26658  vtxdgoddnumeven  26659  redwlklem  26778  wlkdlem1  26789  pthdlem1  26872  crctcshwlkn0lem4  26916  wwlksnredwwlkn0  27014  wwlksnextproplem2  27028  clwwlkccatlem  27112  clwlkclwwlkfo  27132  clwwlkwwlksb  27184  clwwlkndivn  27211  eupth2lem3lem3  27382  eupth2lem3lem4  27383  eupth2lem3  27388  eupth2lems  27390  numclwwlk5  27556  numclwwlk6  27558  ex-ind-dvds  27629  nndiffz1  29857  2sqcoprm  29956  2sqmod  29957  archirng  30051  archirngz  30052  archiabllem1a  30054  madjusmdetlem4  30205  qqhval2lem  30334  oddpwdc  30725  eulerpartlems  30731  eulerpartlemb  30739  sseqfv1  30760  sseqfn  30761  sseqmw  30762  sseqf  30763  sseqfv2  30765  sseqp1  30766  ccatmulgnn0dir  30928  signsplypnf  30936  signsply0  30937  signslema  30948  signstfvn  30955  signstfvp  30957  signstfvc  30960  fsum2dsub  30994  reprinfz1  31009  reprfi2  31010  hashrepr  31012  reprdifc  31014  breprexplema  31017  breprexplemc  31019  circlemeth  31027  circlevma  31029  circlemethhgt  31030  hgt750lema  31044  tgoldbachgtde  31047  subfacval3  31478  bcprod  31931  bccolsum  31932  fwddifnp1  32578  knoppndvlem6  32814  knoppndvlem7  32815  knoppndvlem10  32818  knoppndvlem14  32822  knoppndvlem15  32823  knoppndvlem16  32824  knoppndvlem17  32825  knoppndvlem19  32827  knoppndvlem21  32829  dfgcd3  33481  poimirlem3  33725  poimirlem4  33726  poimirlem6  33728  poimirlem13  33735  poimirlem14  33736  poimirlem17  33739  poimirlem21  33743  poimirlem22  33744  poimirlem23  33745  poimirlem24  33746  poimirlem26  33748  poimirlem27  33749  poimirlem31  33753  geomcau  33868  eldioph2lem1  37825  pellexlem5  37899  congrep  38042  jm2.18  38057  jm2.19lem1  38058  jm2.19lem2  38059  jm2.19  38062  jm2.22  38064  jm2.23  38065  jm2.20nn  38066  jm2.25  38068  jm2.26a  38069  jm2.26lem3  38070  jm2.26  38071  jm2.27a  38074  jm2.27b  38075  jm2.27c  38076  jm3.1  38089  expdiophlem1  38090  hbtlem5  38200  radcnvrat  39015  nzin  39019  bccbc  39046  binomcxplemnn0  39050  binomcxplemnotnn0  39057  fprodexp  40329  mccllem  40332  ioodvbdlimc1lem2  40650  ioodvbdlimc2lem  40652  dvnxpaek  40660  dvnmul  40661  dvnprodlem1  40664  dvnprodlem2  40665  wallispilem1  40785  wallispilem5  40789  stirlinglem3  40796  stirlinglem5  40798  stirlinglem7  40800  stirlinglem8  40801  fourierdlem102  40928  fourierdlem114  40940  sqwvfoura  40948  elaa2lem  40953  etransclem10  40964  etransclem20  40974  etransclem21  40975  etransclem22  40976  etransclem23  40977  etransclem24  40978  etransclem27  40981  etransclem28  40982  etransclem35  40989  etransclem38  40992  etransclem44  40998  etransclem45  40999  etransclem46  41000  sge0ad2en  41151  fsummmodsnunz  41855  pfxtrcfv0  41912  pfxtrcfvl  41915  pfxccat1  41920  pfxccatin12  41935  pfxccatpfx2  41938  pfxccat3a  41939  fmtnoge3  41952  fmtnof1  41957  fmtnorec1  41959  sqrtpwpw2p  41960  fmtnodvds  41966  goldbachthlem2  41968  fmtnoprmfac2lem1  41988  pwm1geoserALT  42012  lighneallem3  42034  lighneallem4b  42036  lighneallem4  42037  ssnn0ssfz  42637  altgsumbcALT  42641  flnn0ohalf  42838  dig2nn1st  42909  0dig2nn0o  42917  aacllem  43060
  Copyright terms: Public domain W3C validator