Theorem nn0z 12633

Description: A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nn0z	⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)

Proof of Theorem nn0z

Step	Hyp	Ref	Expression
1		nn0ssz 12632	. 2 ⊢ ℕ0 ⊆ ℤ
2	1	sseli 3936	1 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℕ₀cn0 12522  ℤcz 12609

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-i2m1 11186  ax-1ne0 11187  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-neg 11462  df-nn 12252  df-n0 12523  df-z 12610

This theorem is used by:  nn0negz  12650  nn0ltp1le  12672  nn0leltp1  12673  nn0ltlem1  12674  nn0lt2  12677  nn0le2is012  12678  nn0lem1lt  12679  fnn0ind  12713  nn0pzuz  12947  nn0ge2m1nnALT  12984  fz1n  13588  ige2m1fz  13664  elfz2nn0  13665  fznn0  13666  elfz0add  13673  fzctr  13687  difelfzle  13688  fzoun  13744  fzofzim  13757  fzo1fzo0n0  13763  elincfzoext  13771  elfzodifsumelfzo  13779  fz0add1fz1  13783  zpnn0elfzo  13786  fzossfzop1  13791  ubmelm1fzo  13811  elfznelfzo  13821  flmulnn0  13880  quoremnn0  13909  zmodidfzoimp  13954  modmuladdnn0  13971  modfzo0difsn  13999  expdiv  14169  expnngt1  14297  faclbnd3  14348  bccmpl  14365  bcnp1n  14370  bcval5  14374  bcn2  14375  bcp1m1  14376  hashge2el2difr  14538  fi1uzind  14564  wrdred1  14617  wrdred1hash  14618  ccatalpha  14652  swrdnd0  14719  swrdfv2  14723  swrdsb0eq  14725  swrdsbslen  14726  swrdspsleq  14727  swrdlsw  14729  pfxnd  14749  pfxccatin12lem4  14787  pfxccatin12lem3  14793  pfxccat3  14795  swrdccat  14796  pfxccat3a  14799  revlen  14823  repswswrd  14847  repswccat  14849  cshwidxmodr  14867  cshf1  14873  2cshw  14876  cshweqrep  14884  cshwcshid  14890  cshwcsh2id  14891  cats1fv  14922  swrd2lsw  15015  2swrd2eqwrdeq  15016  isercoll  15745  iseraltlem2  15760  bcxmas  15915  geo2sum2  15954  geomulcvg  15956  risefacval2  16090  fallfacval2  16091  zrisefaccl  16100  zfallfaccl  16101  fallrisefac  16105  bpolylem  16127  fsumkthpow  16135  esum  16159  ege2le3  16169  eftlcl  16188  reeftlcl  16189  eftlub  16190  effsumlt  16192  eirrlem  16285  dvds1  16402  dvdsext  16404  addmodlteqALT  16408  oddnn02np1  16431  oddge22np1  16432  nn0ehalf  16461  nn0o1gt2  16464  nno  16465  nn0o  16466  nn0oddm1d2  16468  divalglem4  16479  divalglem5  16480  modremain  16491  bitsinv1  16525  nn0gcdid0  16604  nn0seqcvgd  16653  algcvga  16662  eucalgf  16666  nonsq  16843  numdenexp  16844  odzdvds  16880  coprimeprodsq  16893  coprimeprodsq2  16894  oddprm  16895  iserodd  16920  pcexp  16944  pcidlem  16957  pc11  16965  dvdsprmpweqle  16971  difsqpwdvds  16972  pcfac  16984  prmunb  16999  hashbc2  17091  cshwshashlem2  17181  chnccat  18707  smndex1ibas  18990  smndex1iidm  18991  smndex2dnrinv  19008  smndex2dlinvh  19010  mulgaddcom  19195  mulginvcom  19196  mulgz  19199  mulgdirlem  19202  mulgass  19208  mndodcongi  19644  oddvdsnn0  19645  odeq  19651  odmulg  19657  efgsdmi  19833  cyggex2  19998  fincygsubgodd  20215  mulgass2  20425  chrrhm  21718  zncrng  21731  znzrh2  21732  zndvds  21736  znchr  21749  znunit  21750  chfacfisf  23048  chfacfisfcpmat  23049  chfacfscmulfsupp  23053  chfacfpmmulfsupp  23057  clmmulg  25297  itgcnlem  25986  degltlem1  26266  plyco0  26386  dgreq0  26459  plydivex  26495  aannenlem1  26528  abelthlem1  26631  abelthlem3  26633  abelthlem8  26639  abelthlem9  26640  advlogexp  26857  cxpexp  26870  leibpi  27144  log2cnv  27146  log2tlbnd  27147  basellem2  27283  sgmnncl  27348  chpp1  27356  bcmono  27478  bcmax  27479  bcp1ctr  27480  lgsneg1  27523  lgsdirnn0  27545  lgsdinn0  27546  2lgslem1c  27594  2lgslem3a1  27601  2lgslem3b1  27602  2lgslem3c1  27603  2lgsoddprmlem2  27610  2sq2  27634  2sqreultlem  27648  dchrisumlem1  27690  qabvle  27826  ostth2lem2  27835  tgldimor  28808  upgrewlkle2  29993  wlkv0  30036  redwlk  30057  pthdadjvtx  30114  pthdlem1  30152  wwlknvtx  30231  wlkiswwlks2lem3  30257  wwlksm1edg  30267  wwlksnred  30278  wwlksnext  30279  clwlkclwwlklem2a1  30380  clwlkclwwlklem2a2  30381  clwlkclwwlklem2fv1  30383  clwlkclwwlklem2fv2  30384  clwlkclwwlklem2a4  30385  clwlkclwwlklem2a  30386  clwlkclwwlklem2  30388  clwlkclwwlk  30390  clwwisshclwwslem  30402  eucrctshift  30631  eucrct2eupth1  30632  eucrct2eupth  30633  numclwwlk5lem  30775  numclwwlk5  30776  numclwwlk7  30779  frgrreggt1  30781  nndiffz1  33168  nn0diffz0  33176  xrge0mulgnn0  33366  hashf2  34505  signsvtn0  34989  nn0ltp1ne  35627  0nn0m1nnn0  35628  pthhashvtx  35641  fz0n  36244  bcneg1  36249  bccolsum  36252  faclimlem3  36258  faclim  36259  iprodfac  36260  poimirlem28  38340  mblfinlem1  38349  mblfinlem2  38350  lcmineqlem2  42838  sticksstones22  42976  gcdnn0id  43131  negexpidd  43454  nacsfix  43484  fzsplit1nn0  43526  eldioph2lem1  43532  fz1eqin  43541  diophin  43544  eq0rabdioph  43548  rexrabdioph  43562  rexzrexnn0  43572  irrapxlem4  43593  pell14qrss1234  43624  pell1qrss14  43636  monotoddzz  43711  rmxypos  43715  ltrmynn0  43716  ltrmxnn0  43717  lermxnn0  43718  rmxnn  43719  rmynn0  43725  jm2.17a  43728  jm2.17b  43729  rmygeid  43732  jm2.18  43756  jm2.19lem3  43759  jm2.19lem4  43760  jm2.22  43763  rmxdiophlem  43783  hbt  43898  proot1ex  43964  fzisoeu  46060  stirlinglem5  46833  elfzlble  48098  subsubelfzo0  48105  2ffzoeq  48106  addmodne  48128  fargshiftfo  48232  fmtnof1  48328  fmtnorec1  48330  goldbachthlem1  48338  odz2prm2pw  48356  flsqrt  48386  lighneallem4  48403  nn0eo  49349  nn0ofldiv2  49353  flnn0div2ge  49354  fllog2  49389  blenpw2  49399  blennngt2o2  49413  nn0digval  49421  dignn0fr  49422  digexp  49428  0dig2nn0e  49433  0dig2nn0o  49434  dig2bits  49435  dignn0flhalflem2  49437  dignn0ehalf  49438  dignn0flhalf  49439  nn0sumshdiglemB  49441