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

Theorem nnz 10045
Description: A natural number is an integer. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nnz  |-  ( N  e.  NN  ->  N  e.  ZZ )

Proof of Theorem nnz
StepHypRef Expression
1 nnssz 10043 . 2  |-  NN  C_  ZZ
21sseli 3176 1  |-  ( N  e.  NN  ->  N  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   NNcn 9746   ZZcz 10024
This theorem is referenced by:  elnnz1  10049  znegcl  10055  nnleltp1  10071  nnltp1le  10072  nnlem1lt  10080  nnltlem1  10081  prime  10092  nneo  10095  zeo  10097  uzindOLD  10106  btwnz  10114  eluz2b2  10290  qaddcl  10332  qreccl  10336  elfz1end  10820  fznn  10852  elfzo0  10904  quoremz  10959  intfracq  10963  fznnfl  10966  zmodcl  10989  zmodfz  10991  zmodfzo  10992  expnnval  11107  mulexpz  11142  nnesq  11225  expnlbnd  11231  expnlbnd2  11232  digit2  11234  faclbnd  11303  bcval5  11330  fz1isolem  11399  seqcoll  11401  absexpz  11790  climuni  12026  isercoll  12141  climcnds  12310  arisum  12318  trireciplem  12320  expcnv  12322  geo2sum  12329  geo2lim  12331  0.999...  12337  geoihalfsum  12338  rpnnen2lem6  12498  rpnnen2lem9  12501  rpnnen2lem10  12502  dvdsval3  12535  nndivdvds  12537  dvdsle  12574  dvdseq  12576  fzm1ndvds  12580  dvdsfac  12583  oexpneg  12590  divalg2  12604  divalgmod  12605  ndvdsadd  12607  modgcd  12715  gcddiv  12728  gcdmultiple  12729  gcdmultiplez  12730  gcdeq  12731  rpmulgcd  12734  rplpwr  12735  rppwr  12736  sqgcd  12737  dvdssqlem  12738  dvdssq  12739  eucalginv  12754  1idssfct  12764  isprm3  12767  prmind2  12769  qredeq  12785  qredeu  12786  isprm6  12788  divgcdodd  12798  divnumden  12819  divdenle  12820  nn0gcdsq  12823  phicl2  12836  phiprmpw  12844  eulerthlem2  12850  pythagtriplem3  12871  pythagtriplem4  12872  pythagtriplem6  12874  pythagtriplem7  12875  pythagtriplem8  12876  pythagtriplem9  12877  pythagtriplem11  12878  pythagtriplem13  12880  pythagtriplem15  12882  pythagtriplem19  12886  pythagtrip  12887  iserodd  12888  pclem  12891  pccl  12902  pcdiv  12905  pcqcl  12909  pcdvds  12916  pcndvds  12918  pcndvds2  12920  pcelnn  12922  pcz  12933  pcmpt  12940  fldivp1  12945  pcfac  12947  infpnlem1  12957  prmunb  12961  prmreclem1  12963  1arith  12974  0hashbc  13054  ram0  13069  mulgnn  14573  ghmmulg  14695  dfod2  14877  gexdvds  14895  gexnnod  14899  gexex  15145  mulgass2  15387  qsssubdrg  16431  prmirredlem  16446  znidomb  16515  znrrg  16519  lmmo  17108  1stckgenlem  17248  imasdsf1olem  17937  clmmulg  18591  cmetcaulem  18714  ovolunlem1a  18855  ovolicc2lem4  18879  mbfi1fseqlem6  19075  dvexp3  19325  dgreq0  19646  elqaalem2  19700  aaliou3lem1  19722  aaliou3lem2  19723  aaliou3lem3  19724  aaliou3lem9  19730  pserdvlem2  19804  logtayl2  20009  root1eq1  20095  root1cj  20096  atantayl2  20234  birthdaylem2  20247  birthdaylem3  20248  emcllem5  20293  basellem2  20319  basellem3  20320  basellem5  20322  sgmss  20344  issqf  20374  sgmnncl  20385  prmorcht  20416  mumullem1  20417  mumullem2  20418  sqff1o  20420  dvdsdivcl  20421  dvdsflsumcom  20428  muinv  20433  vmalelog  20444  chtublem  20450  vmasum  20455  logfac2  20456  logfaclbnd  20461  bclbnd  20519  bposlem5  20527  lgsval4a  20557  lgssq  20574  lgssq2  20575  lgsdchr  20587  lgsquadlem1  20593  lgsquadlem2  20594  lgsquad3  20600  rplogsumlem1  20633  rplogsumlem2  20634  dchrisumlem2  20639  dchrmusumlema  20642  dchrmusum2  20643  dchrvmasumiflem1  20650  dchrvmaeq0  20653  dchrisum0flblem2  20658  dchrisum0re  20662  dchrisum0lema  20663  dchrisum0lem1b  20664  dchrisum0lem2a  20666  logdivbnd  20705  pntrsumbnd2  20716  ostth2lem1  20767  ostth2lem3  20784  ostth3  20787  gxpval  20926  gxcom  20936  gxinv  20937  gxid  20940  gxmodid  20946  gxdi  20963  bcm1n  23032  elfzo1  23279  esumcvg  23454  erdszelem7  23728  climuzcnv  24004  elfzm12  24008  zmodid2  24010  fznatpl1  24093  axlowdimlem13  24582  cntrset  25602  nn0prpwlem  26238  fzmul  26443  incsequz  26458  geomcau  26475  heibor1lem  26533  bfplem2  26547  fzsplit1nn0  26833  irrapxlem1  26907  pellexlem5  26918  rmynn  27043  jm2.24nn  27046  jm2.17c  27049  congrep  27060  congabseq  27061  acongrep  27067  acongeq  27070  jm2.18  27081  jm2.23  27089  jm2.20nn  27090  jm2.26lem3  27094  jm2.26  27095  jm2.15nn0  27096  jm2.16nn0  27097  jm2.27dlem2  27103  rmydioph  27107  jm3.1  27113  expdiophlem1  27114  expdioph  27116  idomodle  27512  hashgcdlem  27516  hashgcdeq  27517  phisum  27518  proot1ex  27520  fmuldfeq  27713  stoweidlem1  27750  stoweidlem3  27752  stoweidlem7  27756  stoweidlem11  27760  stoweidlem20  27769  stoweidlem26  27775  stoweidlem34  27783  stoweidlem51  27800  wallispilem4  27817  stirlinglem2  27824  stirlinglem3  27825  stirlinglem4  27826  stirlinglem12  27834  stirlinglem13  27835  stirlinglem14  27836  stirlinglem15  27837  stirlingr  27839
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-riota 6304  df-recs 6388  df-rdg 6423  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-nn 9747  df-z 10025
  Copyright terms: Public domain W3C validator