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

Theorem nn0zd 11742
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 11660 . 2 0 ⊆ ℤ
2 nn0zd.1 . 2 (𝜑𝐴 ∈ ℕ0)
31, 2sseldi 3796 1 (𝜑𝐴 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  0cn0 11555  cz 11639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-er 7975  df-en 8189  df-dom 8190  df-sdom 8191  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-nn 11302  df-n0 11556  df-z 11640
This theorem is referenced by:  nnzd  11743  eluzmn  11907  difelfznle  12673  zmodfz  12912  expnegz  13113  expaddzlem  13122  expaddz  13123  expmulz  13125  faclbnd  13293  bcpasc  13324  hashf1  13454  fz1isolem  13458  hashge2el2dif  13475  hashtpg  13480  wrdffz  13533  wrdsymb0  13546  wrdlenge1n0  13547  ccatcl  13567  ccatval3  13572  ccatsymb  13575  ccatval21sw  13578  ccatass  13581  ccatrn  13582  lswccatn0lsw  13584  ccats1val2  13621  swrdnd  13652  swrdtrcfv0  13662  swrdtrcfvl  13670  swrdccat1  13677  swrdccat2  13678  swrdccatin2  13707  swrdccatin12  13711  splfv2a  13727  splval2  13728  revcl  13730  revccat  13735  revrev  13736  cshwmodn  13761  cshwsublen  13762  cshwn  13763  cshwidxmod  13769  2cshwid  13780  3cshw  13784  cshweqdif2  13785  revco  13800  ccatco  13801  ccat2s1fvwALT  13919  ofccat  13929  zabscl  14272  absrdbnd  14300  iseraltlem3  14633  fsum0diaglem  14726  modfsummods  14743  binomlem  14779  binom1p  14781  incexc2  14788  climcndslem1  14799  geoser  14817  pwm1geoser  14818  geolim2  14820  mertenslem1  14833  mertenslem2  14834  mertens  14835  binomfallfaclem2  14987  binomrisefac  14989  fallfacval4  14990  bpolydiflem  15001  ruclem10  15184  sumodd  15327  divalglem9  15340  divalgmod  15345  bitsfzolem  15371  bitsfzo  15372  bitsmod  15373  bitsfi  15374  bitsinv1lem  15378  sadcaddlem  15394  sadadd3  15398  sadaddlem  15403  sadadd  15404  sadasslem  15407  sadass  15408  sadeq  15409  bitsres  15410  bitsuz  15411  bitsshft  15412  smuval2  15419  smupvallem  15420  smupval  15425  smueqlem  15427  smumullem  15429  smumul  15430  gcdcllem1  15436  zeqzmulgcd  15447  gcd0id  15455  gcdneg  15458  modgcd  15468  bezoutlem4  15474  dvdsgcdb  15477  gcdass  15479  mulgcd  15480  gcdzeq  15486  dvdsmulgcd  15489  bezoutr  15496  bezoutr1  15497  nn0seqcvgd  15498  algfx  15508  eucalginv  15512  eucalg  15515  gcddvdslcm  15530  lcmneg  15531  lcmgcdlem  15534  lcmdvds  15536  lcmgcdeq  15540  lcmdvdsb  15541  lcmass  15542  lcmftp  15564  lcmfunsnlem1  15565  lcmfunsnlem2lem1  15566  lcmfunsnlem2lem2  15567  lcmfunsnlem2  15568  lcmfdvdsb  15571  lcmfun  15573  lcmfass  15574  mulgcddvds  15583  rpmulgcd2  15584  qredeu  15586  divgcdcoprm0  15593  sqnprm  15627  divnumden  15669  powm2modprm  15721  coprimeprodsq  15726  iserodd  15753  pclem  15756  pcpre1  15760  pcpremul  15761  pcqcl  15774  pcdvdsb  15786  pcidlem  15789  pc2dvds  15796  pcprmpw2  15799  dvdsprmpweqle  15803  pcadd  15806  pcfac  15816  pcbc  15817  pockthlem  15822  prmreclem2  15834  prmreclem3  15835  mul4sqlem  15870  4sqlem11  15872  4sqlem12  15873  4sqlem14  15875  vdwapun  15891  prmgaplcmlem1  15968  lagsubg  17854  psgnuni  18116  psgnran  18132  odmodnn0  18156  mndodconglem  18157  mndodcong  18158  odmulg2  18169  odmulg  18170  odmulgeq  18171  odbezout  18172  odinv  18175  odf1  18176  gexod  18198  gexdvds3  18202  sylow1lem1  18210  sylow1lem3  18212  pgpfi  18217  pgpssslw  18226  sylow2alem2  18230  sylow2blem3  18234  fislw  18237  sylow3lem4  18242  sylow3lem6  18244  efginvrel2  18337  efgredlemf  18351  efgredlemd  18354  efgredlemc  18355  efgredlem  18357  efgcpbllemb  18365  odadd1  18448  odadd2  18449  gexexlem  18452  gexex  18453  torsubg  18454  lt6abl  18493  gsummulg  18539  ablfacrplem  18662  ablfacrp  18663  ablfacrp2  18664  ablfac1b  18667  ablfac1c  18668  ablfac1eulem  18669  ablfac1eu  18670  pgpfac1lem2  18672  pgpfaclem1  18678  ablfaclem3  18684  srgbinomlem3  18740  srgbinomlem4  18741  psrbaglefi  19577  chrid  20079  znunit  20115  psgnghm  20129  chfacfscmulfsupp  20874  chfacfpmmulfsupp  20878  cpmadugsumlemF  20891  dyadss  23574  dyaddisjlem  23575  ply1divex  24109  ply1termlem  24172  plyeq0lem  24179  plyaddlem1  24182  plymullem1  24183  coeeulem  24193  coeidlem  24206  coeeq2  24211  coemulhi  24223  dvply1  24252  dvply2g  24253  plydivex  24265  elqaalem2  24288  aareccl  24294  aannenlem1  24296  aalioulem1  24300  taylplem1  24330  taylplem2  24331  taylpfval  24332  dvtaylp  24337  taylthlem2  24341  dvradcnv  24388  abelthlem7  24405  cxpeq  24711  birthdaylem2  24892  ftalem1  25012  basellem3  25022  isppw2  25054  isnsqf  25074  mule1  25087  ppinncl  25113  musum  25130  chtublem  25149  pclogsum  25153  vmasum  25154  dchrabs  25198  bcmax  25216  bposlem1  25222  bposlem6  25227  lgsval2lem  25245  lgsmod  25261  lgsne0  25273  gausslemma2dlem0h  25301  gausslemma2dlem0i  25302  gausslemma2dlem2  25305  gausslemma2dlem6  25310  gausslemma2d  25312  lgseisenlem1  25313  lgseisenlem2  25314  lgseisenlem3  25315  lgseisenlem4  25316  lgsquadlem1  25318  m1lgs  25326  2lgslem1a  25329  2lgslem3a  25334  2lgslem3b  25335  2lgslem3c  25336  2lgslem3d  25337  2lgslem3d1  25341  2lgsoddprmlem2  25347  2sqlem8  25364  chebbnd1lem1  25371  dchrisumlem1  25391  dchrisum0flblem1  25410  selberg2lem  25452  ostth2lem2  25536  ostth2lem3  25537  finsumvtxdg2sstep  26672  finsumvtxdgeven  26675  vtxdgoddnumeven  26676  redwlklem  26795  wlkdlem1  26806  pthdlem1  26889  crctcshwlkn0lem4  26933  wwlksnredwwlkn0  27032  wwlksnextproplem2  27047  clwwlkccatlem  27131  clwlkclwwlkfo  27151  clwwlkwwlksb  27203  clwwlkndivn  27230  eupth2lem3lem3  27402  eupth2lem3lem4  27403  eupth2lem3  27408  eupth2lems  27410  numclwwlk5  27575  numclwwlk6  27577  ex-ind-dvds  27648  nndiffz1  29874  2sqcoprm  29971  2sqmod  29972  archirng  30066  archirngz  30067  archiabllem1a  30069  madjusmdetlem4  30220  qqhval2lem  30349  oddpwdc  30740  eulerpartlems  30746  eulerpartlemb  30754  sseqfv1  30775  sseqfn  30776  sseqmw  30777  sseqf  30778  sseqfv2  30780  sseqp1  30781  ccatmulgnn0dir  30943  signsplypnf  30951  signsply0  30952  signslema  30963  signstfvn  30970  signstfvp  30972  signstfvc  30975  fsum2dsub  31009  reprinfz1  31024  reprfi2  31025  hashrepr  31027  reprdifc  31029  breprexplema  31032  breprexplemc  31034  circlemeth  31042  circlevma  31044  circlemethhgt  31045  hgt750lema  31059  tgoldbachgtde  31062  subfacval3  31492  bcprod  31944  bccolsum  31945  fwddifnp1  32591  knoppndvlem6  32823  knoppndvlem7  32824  knoppndvlem10  32827  knoppndvlem14  32831  knoppndvlem15  32832  knoppndvlem16  32833  knoppndvlem17  32834  knoppndvlem19  32836  knoppndvlem21  32838  dfgcd3  33485  poimirlem3  33723  poimirlem4  33724  poimirlem6  33726  poimirlem13  33733  poimirlem14  33734  poimirlem17  33737  poimirlem21  33741  poimirlem22  33742  poimirlem23  33743  poimirlem24  33744  poimirlem26  33746  poimirlem27  33747  poimirlem31  33751  geomcau  33864  eldioph2lem1  37822  pellexlem5  37896  congrep  38038  jm2.18  38053  jm2.19lem1  38054  jm2.19lem2  38055  jm2.19  38058  jm2.22  38060  jm2.23  38061  jm2.20nn  38062  jm2.25  38064  jm2.26a  38065  jm2.26lem3  38066  jm2.26  38067  jm2.27a  38070  jm2.27b  38071  jm2.27c  38072  jm3.1  38085  expdiophlem1  38086  hbtlem5  38196  radcnvrat  39010  nzin  39014  bccbc  39041  binomcxplemnn0  39045  binomcxplemnotnn0  39052  fprodexp  40303  mccllem  40306  ioodvbdlimc1lem2  40624  ioodvbdlimc2lem  40626  dvnxpaek  40634  dvnmul  40635  dvnprodlem1  40638  dvnprodlem2  40639  wallispilem1  40758  wallispilem5  40762  stirlinglem3  40769  stirlinglem5  40771  stirlinglem7  40773  stirlinglem8  40774  fourierdlem102  40901  fourierdlem114  40913  sqwvfoura  40921  elaa2lem  40926  etransclem10  40937  etransclem20  40947  etransclem21  40948  etransclem22  40949  etransclem23  40950  etransclem24  40951  etransclem27  40954  etransclem28  40955  etransclem35  40962  etransclem38  40965  etransclem44  40971  etransclem45  40972  etransclem46  40973  sge0ad2en  41124  fsummmodsnunz  41917  pfxtrcfv0  41974  pfxtrcfvl  41977  pfxccat1  41982  pfxccatin12  41997  pfxccatpfx2  42000  pfxccat3a  42001  fmtnoge3  42014  fmtnof1  42019  fmtnorec1  42021  sqrtpwpw2p  42022  fmtnodvds  42028  goldbachthlem2  42030  fmtnoprmfac2lem1  42050  pwm1geoserALT  42074  lighneallem3  42096  lighneallem4b  42098  lighneallem4  42099  ssnn0ssfz  42692  altgsumbcALT  42696  flnn0ohalf  42893  dig2nn1st  42964  0dig2nn0o  42972  aacllem  43115
  Copyright terms: Public domain W3C validator