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

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

Proof of Theorem nnzd
StepHypRef Expression
1 nnzd.1 . . 3 (𝜑𝐴 ∈ ℕ)
21nnnn0d 11228 . 2 (𝜑𝐴 ∈ ℕ0)
32nn0zd 11356 1 (𝜑𝐴 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  cn 10897  cz 11254
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-n0 11170  df-z 11255
This theorem is referenced by:  expaddzlem  12765  expmulz  12768  expmulnbnd  12858  facndiv  12937  bcval5  12967  bcpasc  12970  hashf1  13098  isercolllem1  14243  isercolllem2  14244  o1fsum  14386  bcxmas  14406  climcndslem2  14421  climcnds  14422  mertenslem1  14455  fprodser  14518  bpolydiflem  14624  eftlub  14678  eirrlem  14771  rpnnen2lem7  14788  rpnnen2lem9  14790  rpnnen2lem11  14792  sqr2irrlem  14816  dvdsfac  14886  dvdsmod  14888  oddpwp1fsum  14953  bitsfzolem  14994  bitsmod  14996  bitsfi  14997  bitscmp  14998  bitsinv1  15002  sadadd3  15021  sadaddlem  15026  bitsuz  15034  bitsshft  15035  gcdnncl  15067  gcd1  15087  bezoutlem3  15096  bezoutlem4  15097  mulgcd  15103  gcdmultiplez  15108  rplpwr  15114  rppwr  15115  sqgcd  15116  dvdssq  15118  lcmneg  15154  lcmgcdlem  15157  rpdvds  15212  coprmprod  15213  coprmproddvdslem  15214  congr  15216  cncongr1  15219  cncongr2  15220  prmz  15227  prmind2  15236  divgcdodd  15260  isprm6  15264  prmexpb  15268  prmfac1  15269  rpexp  15270  numdensq  15300  hashdvds  15318  phiprmpw  15319  crth  15321  phimullem  15322  eulerthlem1  15324  eulerthlem2  15325  prmdivdiv  15330  hashgcdlem  15331  odzdvds  15338  pythagtriplem4  15362  pythagtriplem6  15364  pythagtriplem7  15365  pythagtriplem11  15368  pythagtriplem13  15370  pythagtriplem19  15376  pclem  15381  pcprendvds2  15384  pcpre1  15385  pcpremul  15386  pceulem  15388  pcqmul  15396  pcdvdsb  15411  pcidlem  15414  pcdvdstr  15418  pcgcd1  15419  pc2dvds  15421  pcprmpw2  15424  pcaddlem  15430  pcadd  15431  pcmpt2  15435  pcmptdvds  15436  pcfac  15441  pcbc  15442  qexpz  15443  oddprmdvds  15445  prmpwdvds  15446  pockthlem  15447  pockthg  15448  prmreclem2  15459  prmreclem3  15460  prmreclem4  15461  prmreclem5  15462  prmreclem6  15463  4sqlem5  15484  4sqlem8  15487  4sqlem9  15488  4sqlem10  15489  4sqlem12  15498  4sqlem14  15500  4sqlem16  15502  4sqlem17  15503  vdwlem1  15523  vdwlem2  15524  vdwlem3  15525  vdwlem6  15528  vdwlem9  15531  vdwlem10  15532  vdwnnlem3  15539  prmdvdsprmop  15585  prmolelcmf  15590  prmgaplem1  15591  prmgaplem7  15599  prmgaplem8  15600  gsumwsubmcl  17198  gsumccat  17201  gsumwmhm  17205  mulgneg  17383  mulgnndir  17392  mulgnndirOLD  17393  psgnunilem4  17740  odlem2  17781  mndodconglem  17783  odmod  17788  gexlem2  17820  gexcl3  17825  gexcl2  17827  sylow1lem1  17836  sylow1lem3  17838  sylow1lem5  17840  pgpfi  17843  fislw  17863  sylow3lem4  17868  gexexlem  18078  ablfacrplem  18287  ablfacrp  18288  ablfacrp2  18289  ablfac1lem  18290  ablfac1b  18292  ablfac1eu  18295  pgpfac1lem3a  18298  ablfaclem3  18309  znrrg  19733  cayhamlem1  20490  caublcls  22915  ovolicc2lem4  23095  iundisj2  23124  volsup  23131  uniioombllem3  23159  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  elqaalem2  23879  aalioulem1  23891  aalioulem4  23894  aalioulem5  23895  aalioulem6  23896  aaliou  23897  aaliou3lem1  23901  aaliou3lem2  23902  aaliou3lem3  23903  aaliou3lem8  23904  aaliou3lem5  23906  aaliou3lem6  23907  aaliou3lem7  23908  taylthlem2  23932  cxpeq  24298  amgmlem  24516  lgamgulmlem4  24558  lgamcvg2  24581  wilthlem2  24595  wilth  24597  wilthimp  24598  ftalem5  24603  basellem2  24608  basellem3  24609  basellem4  24610  basellem5  24611  muval1  24659  dvdssqf  24664  sgmnncl  24673  efchtdvds  24685  mumullem2  24706  mumul  24707  sqff1o  24708  fsumdvdsdiaglem  24709  dvdsppwf1o  24712  dvdsflf1o  24713  muinv  24719  dvdsmulf1o  24720  chtublem  24736  fsumvma2  24739  vmasum  24741  chpchtsum  24744  logfacubnd  24746  mersenne  24752  perfect1  24753  perfectlem1  24754  perfectlem2  24755  perfect  24756  dchrelbas4  24768  dchrfi  24780  bcmono  24802  bcp1ctr  24804  bclbnd  24805  bposlem1  24809  bposlem3  24811  bposlem5  24813  bposlem6  24814  bposlem9  24817  lgsmod  24848  lgsdir  24857  lgsdilem2  24858  lgsne0  24860  lgsqrlem2  24872  lgsqr  24876  lgsqrmodndvds  24878  gausslemma2dlem0c  24883  gausslemma2dlem0h  24888  gausslemma2dlem0i  24889  gausslemma2dlem2  24892  gausslemma2dlem6  24897  gausslemma2dlem7  24898  gausslemma2d  24899  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgseisenlem4  24903  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  lgsquad2lem1  24909  lgsquad2lem2  24910  lgsquad2  24911  m1lgs  24913  2lgslem2  24920  2sqlem3  24945  2sqlem4  24946  2sqlem8  24951  chebbnd1lem1  24958  rplogsumlem2  24974  rpvmasumlem  24976  dchrisumlem1  24978  dchrisumlem2  24979  dchrisumlem3  24980  dchrisum0fmul  24995  dchrisum0ff  24996  dchrisum0flblem1  24997  dchrisum0flblem2  24998  dchrisum0flb  24999  dchrisum0  25009  pntrsumbnd2  25056  pntrlog2bndlem1  25066  pntrlog2bndlem6  25072  pntpbnd2  25076  pntlemg  25087  pntlemj  25092  pntlemf  25094  ostth2lem2  25123  ostth2lem3  25124  ostth3  25127  minvecolem4  27120  iundisj2f  28785  ssnnssfz  28937  iundisj2fi  28943  f1ocnt  28946  numdenneg  28950  ltesubnnd  28955  isarchi3  29072  archiabllem1b  29077  psgnfzto1stlem  29181  smatrcl  29190  1smat1  29198  submateqlem1  29201  submateqlem2  29202  lmatfvlem  29209  qqhval2  29354  qqhf  29358  qqhghm  29360  qqhrhm  29361  qqhnm  29362  qqhre  29392  esumcvg  29475  meascnbl  29609  omssubadd  29689  oddpwdc  29743  ballotlemfp1  29880  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemimin  29894  ballotlemic  29895  ballotlem1c  29896  subfaclim  30424  cvmliftlem7  30527  sinccvglem  30820  bcprod  30877  bccolsum  30878  faclimlem2  30883  faclim2  30887  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem6  32585  poimirlem8  32587  poimirlem9  32588  poimirlem10  32589  poimirlem11  32590  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem31  32610  mblfinlem2  32617  seqpo  32713  incsequz  32714  incsequz2  32715  irrapxlem3  36406  irrapxlem5  36408  pellexlem5  36415  pellexlem6  36416  pellex  36417  pell1234qrmulcl  36437  jm2.23  36581  jm2.20nn  36582  jm2.26lem3  36586  jm2.27a  36590  jm2.27b  36591  jm2.27c  36592  jm3.1lem1  36602  jm3.1lem3  36604  inductionexd  37473  nznngen  37537  hashnzfz2  37542  fmuldfeq  38650  divcnvg  38694  stoweidlem1  38894  stoweidlem3  38896  stoweidlem11  38904  stoweidlem20  38913  stoweidlem26  38919  stoweidlem34  38927  stoweidlem51  38944  stirlinglem4  38970  stirlinglem5  38971  stirlinglem8  38974  dirkerper  38989  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  dirkercncflem2  38997  fourierdlem11  39011  fourierdlem14  39014  fourierdlem20  39020  fourierdlem25  39025  fourierdlem37  39037  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem54  39053  fourierdlem64  39063  fourierdlem73  39072  fourierdlem79  39078  fourierdlem92  39091  fourierdlem93  39092  fourierdlem111  39110  sqwvfourb  39122  etransclem3  39130  etransclem7  39134  etransclem10  39137  etransclem15  39142  etransclem24  39151  etransclem25  39152  etransclem26  39153  etransclem27  39154  etransclem28  39155  etransclem35  39162  etransclem37  39164  etransclem38  39165  etransclem41  39168  etransclem44  39171  etransclem45  39172  etransclem48  39175  ovnsubaddlem1  39460  vonioolem1  39571  iccpartgtprec  39958  iccpartipre  39959  fmtnoodd  39983  goldbachthlem2  39996  goldbachth  39997  odz2prm2pw  40013  fmtnoprmfac1lem  40014  fmtnoprmfac2lem1  40016  fmtnoprmfac2  40017  fmtnofac2lem  40018  2pwp1prm  40041  lighneallem1  40060  lighneallem4  40065  proththdlem  40068  proththd  40069  divgcdoddALTV  40131  perfectALTVlem1  40164  perfectALTVlem2  40165  perfectALTV  40166  gboge7  40185  pw2m1lepw2m1  42104  nnolog2flm1  42182  dignn0fr  42193  dignn0flhalflem1  42207
  Copyright terms: Public domain W3C validator