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

Theorem nnzd 10379
Description: A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
nnzd.1  |-  ( ph  ->  A  e.  NN )
Assertion
Ref Expression
nnzd  |-  ( ph  ->  A  e.  ZZ )

Proof of Theorem nnzd
StepHypRef Expression
1 nnzd.1 . . 3  |-  ( ph  ->  A  e.  NN )
21nnnn0d 10279 . 2  |-  ( ph  ->  A  e.  NN0 )
32nn0zd 10378 1  |-  ( ph  ->  A  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   NNcn 10005   ZZcz 10287
This theorem is referenced by:  expaddzlem  11428  expmulz  11431  expmulnbnd  11516  facndiv  11584  bcval5  11614  bcpasc  11617  hashf1  11711  isercolllem1  12463  isercolllem2  12464  o1fsum  12597  bcxmas  12620  climcndslem2  12635  climcnds  12636  mertenslem1  12666  eftlub  12715  eirrlem  12808  rpnnen2lem7  12825  rpnnen2lem9  12827  rpnnen2lem11  12829  sqr2irrlem  12852  dvdsfac  12909  dvdsmod  12911  bitsfzolem  12951  bitsmod  12953  bitsfi  12954  bitscmp  12955  bitsinv1  12959  sadadd3  12978  sadaddlem  12983  bitsuz  12991  bitsshft  12992  gcd1  13037  bezoutlem3  13045  bezoutlem4  13046  mulgcd  13051  gcdmultiplez  13056  rplpwr  13061  rppwr  13062  sqgcd  13063  dvdssq  13065  prmz  13088  prmind2  13095  isprm6  13114  prmexpb  13122  prmfac1  13123  divgcdodd  13124  rpexp  13125  rpdvds  13129  numdensq  13151  hashdvds  13169  phiprmpw  13170  crt  13172  phimullem  13173  eulerthlem1  13175  eulerthlem2  13176  prmdivdiv  13181  odzdvds  13186  pythagtriplem4  13198  pythagtriplem6  13200  pythagtriplem7  13201  pythagtriplem11  13204  pythagtriplem13  13206  pythagtriplem19  13212  pclem  13217  pcprendvds2  13220  pcpre1  13221  pcpremul  13222  pceulem  13224  pcqmul  13232  pcdvdsb  13247  pcidlem  13250  pcdvdstr  13254  pcgcd1  13255  pc2dvds  13257  pcprmpw2  13260  pcaddlem  13262  pcadd  13263  pcmpt2  13267  pcmptdvds  13268  pcfac  13273  pcbc  13274  qexpz  13275  prmpwdvds  13277  pockthlem  13278  pockthg  13279  prmreclem2  13290  prmreclem3  13291  prmreclem4  13292  prmreclem5  13293  prmreclem6  13294  4sqlem5  13315  4sqlem8  13318  4sqlem9  13319  4sqlem10  13320  4sqlem12  13329  4sqlem14  13331  4sqlem16  13333  4sqlem17  13334  vdwlem1  13354  vdwlem2  13355  vdwlem3  13356  vdwlem6  13359  vdwlem9  13362  vdwlem10  13363  vdwnnlem3  13370  gsumwsubmcl  14789  gsumccat  14792  gsumwmhm  14795  mulgneg  14913  mulgnndir  14917  odlem2  15182  mndodconglem  15184  odmod  15189  gexlem2  15221  gexcl3  15226  gexcl2  15228  sylow1lem1  15237  sylow1lem3  15239  sylow1lem5  15241  pgpfi  15244  fislw  15264  sylow3lem4  15269  gexexlem  15472  ablfacrplem  15628  ablfacrp  15629  ablfacrp2  15630  ablfac1lem  15631  ablfac1b  15633  ablfac1eu  15636  pgpfac1lem3a  15639  ablfaclem3  15650  caublcls  19266  ovolicc2lem4  19421  iundisj2  19448  volsup  19455  uniioombllem3  19482  mbfi1fseqlem3  19612  mbfi1fseqlem4  19613  elqaalem2  20242  aalioulem1  20254  aalioulem4  20257  aalioulem5  20258  aalioulem6  20259  aaliou  20260  aaliou3lem1  20264  aaliou3lem2  20265  aaliou3lem3  20266  aaliou3lem8  20267  aaliou3lem5  20269  aaliou3lem6  20270  aaliou3lem7  20271  taylthlem2  20295  cxpeq  20646  amgmlem  20833  wilthlem2  20857  wilth  20859  ftalem5  20864  basellem2  20869  basellem3  20870  basellem4  20871  basellem5  20872  muval1  20921  dvdssqf  20926  sgmnncl  20935  efchtdvds  20947  mumullem2  20968  mumul  20969  sqff1o  20970  fsumdvdsdiaglem  20973  dvdsppwf1o  20976  dvdsflf1o  20977  muinv  20983  dvdsmulf1o  20984  chtublem  21000  fsumvma2  21003  vmasum  21005  chpchtsum  21008  logfacubnd  21010  mersenne  21016  perfect1  21017  perfectlem1  21018  perfectlem2  21019  perfect  21020  dchrelbas4  21032  dchrfi  21044  bcmono  21066  bcp1ctr  21068  bclbnd  21069  bposlem1  21073  bposlem3  21075  bposlem5  21077  bposlem6  21078  bposlem9  21081  lgsmod  21110  lgsdir  21119  lgsdilem2  21120  lgsne0  21122  lgsqrlem2  21131  lgsqr  21135  lgseisenlem1  21138  lgseisenlem2  21139  lgseisenlem3  21140  lgseisenlem4  21141  lgsquadlem1  21143  lgsquadlem2  21144  lgsquadlem3  21145  lgsquad2lem1  21147  lgsquad2lem2  21148  lgsquad2  21149  m1lgs  21151  2sqlem3  21155  2sqlem4  21156  2sqlem8  21161  chebbnd1lem1  21168  rplogsumlem2  21184  rpvmasumlem  21186  dchrisumlem1  21188  dchrisumlem2  21189  dchrisumlem3  21190  dchrisum0fmul  21205  dchrisum0ff  21206  dchrisum0flblem1  21207  dchrisum0flblem2  21208  dchrisum0flb  21209  dchrisum0  21219  pntrsumbnd2  21266  pntrlog2bndlem1  21276  pntrlog2bndlem6  21282  pntpbnd2  21286  pntlemg  21297  pntlemj  21302  pntlemf  21304  ostth2lem2  21333  ostth2lem3  21334  ostth3  21337  minvecolem4  22387  iundisj2f  24035  ssnnssfz  24153  iundisj2fi  24158  numdenneg  24165  ltesubnnd  24167  isarchi2  24260  qqhval2  24371  qqhf  24375  qqhghm  24377  qqhrhm  24378  qqhnm  24379  qqhre  24391  esumcvg  24481  meascnbl  24578  ballotlemfp1  24754  ballotlemfc0  24755  ballotlemfcc  24756  ballotlemimin  24768  ballotlemic  24769  ballotlem1c  24770  lgamgulmlem4  24821  lgamcvg2  24844  subfaclim  24879  cvmliftlem7  24983  sinccvglem  25114  fprodser  25280  faclimlem2  25368  faclim2  25372  bpolydiflem  26105  mblfinlem2  26256  seqpo  26465  incsequz  26466  incsequz2  26467  irrapxlem3  26901  irrapxlem5  26903  pellexlem5  26910  pellexlem6  26911  pellex  26912  pell1234qrmulcl  26932  jm2.23  27081  jm2.20nn  27082  jm2.26lem3  27086  jm2.27a  27090  jm2.27b  27091  jm2.27c  27092  jm3.1lem1  27102  jm3.1lem3  27104  psgnunilem4  27411  hashgcdlem  27507  fmuldfeq  27703  stoweidlem1  27740  stoweidlem3  27742  stoweidlem11  27750  stoweidlem20  27759  stoweidlem26  27765  stoweidlem34  27773  stoweidlem51  27790  stirlinglem4  27816  stirlinglem5  27817  stirlinglem8  27820
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071  ax-pre-mulgt0 9072
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-riota 6552  df-recs 6636  df-rdg 6671  df-er 6908  df-en 7113  df-dom 7114  df-sdom 7115  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131  df-sub 9298  df-neg 9299  df-nn 10006  df-n0 10227  df-z 10288
  Copyright terms: Public domain W3C validator