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

Theorem nn0zd 11312
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 11231 . 2 0 ⊆ ℤ
2 nn0zd.1 . 2 (𝜑𝐴 ∈ ℕ0)
31, 2sseldi 3565 1 (𝜑𝐴 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  0cn0 11139  cz 11210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10868  df-n0 11140  df-z 11211
This theorem is referenced by:  nnzd  11313  eluzmn  11526  difelfznle  12277  zmodfz  12509  expnegz  12711  expaddzlem  12720  expaddz  12721  expmulz  12723  faclbnd  12894  bcpasc  12925  hashf1  13050  fz1isolem  13054  hashge2el2dif  13067  hashtpg  13071  wrdffz  13127  wrdsymb0  13140  wrdlenge1n0  13141  ccatcl  13158  ccatval3  13162  ccatsymb  13165  ccatass  13170  ccatrn  13171  lswccatn0lsw  13172  ccats1val2  13202  swrdnd  13230  swrdtrcfv0  13240  swrdtrcfvl  13248  swrdccat1  13255  swrdccat2  13256  swrdccatin2  13284  swrdccatin12  13288  splfv2a  13304  splval2  13305  revcl  13307  revccat  13312  revrev  13313  cshwmodn  13338  cshwsublen  13339  cshwn  13340  cshwidxmod  13346  2cshwid  13357  3cshw  13361  cshweqdif2  13362  revco  13377  ccatco  13378  ccat2s1fvwALT  13492  ofccat  13502  zabscl  13847  absrdbnd  13875  iseraltlem3  14208  fsum0diaglem  14296  modfsummods  14312  binomlem  14346  binom1p  14348  incexc2  14355  climcndslem1  14366  geoser  14384  pwm1geoser  14385  geolim2  14387  mertenslem1  14401  mertenslem2  14402  mertens  14403  binomfallfaclem2  14556  binomrisefac  14558  fallfacval4  14559  bpolydiflem  14570  ruclem10  14753  sumodd  14895  divalglem9  14908  divalgmod  14913  divalgmodOLD  14914  bitsfzolem  14940  bitsfzo  14941  bitsmod  14942  bitsfi  14943  bitsinv1lem  14947  sadcaddlem  14963  sadadd3  14967  sadaddlem  14972  sadadd  14973  sadasslem  14976  sadass  14977  sadeq  14978  bitsres  14979  bitsuz  14980  bitsshft  14981  smuval2  14988  smupvallem  14989  smupval  14994  smueqlem  14996  smumullem  14998  smumul  14999  gcdcllem1  15005  zeqzmulgcd  15016  gcd0id  15024  gcdneg  15027  modgcd  15037  bezoutlem4  15043  dvdsgcdb  15046  gcdass  15048  mulgcd  15049  gcdzeq  15055  dvdsmulgcd  15058  bezoutr  15065  bezoutr1  15066  nn0seqcvgd  15067  algfx  15077  eucalginv  15081  eucalg  15084  gcddvdslcm  15099  lcmneg  15100  lcmgcdlem  15103  lcmdvds  15105  lcmgcdeq  15109  lcmdvdsb  15110  lcmass  15111  lcmftp  15133  lcmfunsnlem1  15134  lcmfunsnlem2lem1  15135  lcmfunsnlem2lem2  15136  lcmfunsnlem2  15137  lcmfdvdsb  15140  lcmfun  15142  lcmfass  15143  mulgcddvds  15153  rpmulgcd2  15154  qredeu  15156  divgcdcoprm0  15163  sqnprm  15198  divnumden  15240  powm2modprm  15292  coprimeprodsq  15297  iserodd  15324  pclem  15327  pcpre1  15331  pcpremul  15332  pcqcl  15345  pcdvdsb  15357  pcidlem  15360  pc2dvds  15367  pcprmpw2  15370  dvdsprmpweqle  15374  pcadd  15377  pcfac  15387  pcbc  15388  pockthlem  15393  prmreclem2  15405  prmreclem3  15406  mul4sqlem  15441  4sqlem11  15443  4sqlem12  15444  4sqlem14  15446  vdwapun  15462  prmgaplcmlem1  15539  lagsubg  17425  psgnuni  17688  psgnran  17704  odmodnn0  17728  mndodconglem  17729  mndodcong  17730  odmulg2  17741  odmulg  17742  odmulgeq  17743  odbezout  17744  odinv  17747  odf1  17748  gexod  17770  gexdvds3  17774  sylow1lem1  17782  sylow1lem3  17784  pgpfi  17789  pgpssslw  17798  sylow2alem2  17802  sylow2blem3  17806  fislw  17809  sylow3lem4  17814  sylow3lem6  17816  efginvrel2  17909  efgredlemf  17923  efgredlemd  17926  efgredlemc  17927  efgredlem  17929  efgcpbllemb  17937  odadd1  18020  odadd2  18021  gexexlem  18024  gexex  18025  torsubg  18026  lt6abl  18065  gsummulg  18111  ablfacrplem  18233  ablfacrp  18234  ablfacrp2  18235  ablfac1b  18238  ablfac1c  18239  ablfac1eulem  18240  ablfac1eu  18241  pgpfac1lem2  18243  pgpfaclem1  18249  ablfaclem3  18255  srgbinomlem3  18311  srgbinomlem4  18312  psrbaglefi  19139  chrid  19639  znunit  19676  psgnghm  19690  chfacfscmulfsupp  20425  chfacfpmmulfsupp  20429  cpmadugsumlemF  20442  dyadss  23085  dyaddisjlem  23086  ply1divex  23617  ply1termlem  23680  plyeq0lem  23687  plyaddlem1  23690  plymullem1  23691  coeeulem  23701  coeidlem  23714  coeeq2  23719  coemulhi  23731  dvply1  23760  dvply2g  23761  plydivex  23773  elqaalem2  23796  aareccl  23802  aannenlem1  23804  aalioulem1  23808  taylplem1  23838  taylplem2  23839  taylpfval  23840  dvtaylp  23845  taylthlem2  23849  dvradcnv  23896  abelthlem7  23913  cxpeq  24215  birthdaylem2  24396  ftalem1  24516  basellem3  24526  isppw2  24558  isnsqf  24578  mule1  24591  ppinncl  24617  musum  24634  chtublem  24653  pclogsum  24657  vmasum  24658  dchrabs  24702  bcmax  24720  bposlem1  24726  bposlem6  24731  lgsval2lem  24749  lgsmod  24765  lgsdirprm  24773  lgsne0  24777  gausslemma2dlem0h  24805  gausslemma2dlem0i  24806  gausslemma2dlem2  24809  gausslemma2dlem6  24814  gausslemma2d  24816  lgseisenlem1  24817  lgseisenlem2  24818  lgseisenlem3  24819  lgseisenlem4  24820  lgsquadlem1  24822  m1lgs  24830  2lgslem1a  24833  2lgslem3a  24838  2lgslem3b  24839  2lgslem3c  24840  2lgslem3d  24841  2lgslem3d1  24845  2lgsoddprmlem2  24851  2sqlem8  24868  chebbnd1lem1  24875  dchrisumlem1  24895  dchrisum0flblem1  24914  selberg2lem  24956  ostth2lem2  25040  ostth2lem3  25041  wwlknredwwlkn0  26021  wwlkextproplem2  26036  clwwlkndivn  26130  nbhashuvtx1  26208  eupath2lem3  26272  eupath2  26273  numclwwlkovf2ex  26379  numclwwlk5  26405  numclwwlk6  26406  ex-ind-dvds  26476  nndiffz1  28742  2sqcoprm  28784  2sqmod  28785  archirng  28879  archirngz  28880  archiabllem1a  28882  madjusmdetlem4  29030  qqhval2lem  29159  oddpwdc  29549  eulerpartlems  29555  eulerpartlemb  29563  sseqfv1  29584  sseqfn  29585  sseqmw  29586  sseqf  29587  sseqfv2  29589  sseqp1  29590  ccatmulgnn0dir  29751  signsplypnf  29759  signsply0  29760  signslema  29771  signstfvn  29778  signstfvp  29780  signstfvc  29783  subfacval3  30231  bcprod  30683  bccolsum  30684  fwddifnp1  31248  knoppndvlem6  31484  knoppndvlem7  31485  knoppndvlem10  31488  knoppndvlem14  31492  knoppndvlem15  31493  knoppndvlem16  31494  knoppndvlem17  31495  knoppndvlem19  31497  knoppndvlem21  31499  poimirlem3  32378  poimirlem4  32379  poimirlem6  32381  poimirlem13  32388  poimirlem14  32389  poimirlem17  32392  poimirlem21  32396  poimirlem22  32397  poimirlem23  32398  poimirlem24  32399  poimirlem26  32401  poimirlem27  32402  poimirlem31  32406  geomcau  32521  eldioph2lem1  36137  pellexlem5  36211  congrep  36354  jm2.18  36369  jm2.19lem1  36370  jm2.19lem2  36371  jm2.19  36374  jm2.22  36376  jm2.23  36377  jm2.20nn  36378  jm2.25  36380  jm2.26a  36381  jm2.26lem3  36382  jm2.26  36383  jm2.27a  36386  jm2.27b  36387  jm2.27c  36388  jm3.1  36401  expdiophlem1  36402  hbtlem5  36513  radcnvrat  37331  nzin  37335  bccbc  37362  binomcxplemnn0  37366  binomcxplemnotnn0  37373  fprodexp  38458  mccllem  38461  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  dvnxpaek  38629  dvnmul  38630  dvnprodlem1  38633  dvnprodlem2  38634  wallispilem1  38755  wallispilem5  38759  stirlinglem3  38766  stirlinglem5  38768  stirlinglem7  38770  stirlinglem8  38771  fourierdlem102  38898  fourierdlem114  38910  sqwvfoura  38918  elaa2lem  38923  etransclem10  38934  etransclem20  38944  etransclem21  38945  etransclem22  38946  etransclem23  38947  etransclem24  38948  etransclem27  38951  etransclem28  38952  etransclem35  38959  etransclem38  38962  etransclem44  38968  etransclem45  38969  etransclem46  38970  sge0ad2en  39121  fmtnoge3  39778  fmtnof1  39783  fmtnorec1  39785  sqrtpwpw2p  39786  fmtnodvds  39792  goldbachthlem2  39794  fmtnoprmfac2lem1  39814  pwm1geoserALT  39838  lighneallem3  39860  lighneallem4b  39862  lighneallem4  39863  pfxtrcfv0  40063  pfxtrcfvl  40066  pfxccat1  40071  pfxccatin12  40086  pfxccatpfx2  40089  pfxccat3a  40090  fsummmodsnunz  40217  red1wlklem  40875  1wlkdlem1  40886  pthdlem1  40967  crctcsh1wlkn0lem4  41011  wwlksnredwwlkn0  41097  wwlksnextproplem1  41110  wwlksnextproplem2  41111  clwwlksndivn  41259  eupth2lem3lem3  41393  eupth2lem3lem4  41394  eupth2lem3  41399  eupth2lems  41401  av-numclwwlkovf2ex  41512  av-numclwwlk5  41537  av-numclwwlk6  41539  ssnn0ssfz  41915  altgsumbcALT  41919  flnn0ohalf  42117  dig2nn1st  42192  0dig2nn0o  42200  aacllem  42312
  Copyright terms: Public domain W3C validator