Theorem nn0z 12607

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 12605	. 2 ⊢ ℕ0 ⊆ ℤ
2	1	sseli 3974	1 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2099  ℕ₀cn0 12496  ℤcz 12582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734  ax-1cn 11190  ax-icn 11191  ax-addcl 11192  ax-addrcl 11193  ax-mulcl 11194  ax-mulrcl 11195  ax-i2m1 11200  ax-1ne0 11201  ax-rnegex 11203  ax-rrecex 11204  ax-cnre 11205

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-om 7865  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-neg 11471  df-nn 12237  df-n0 12497  df-z 12583

This theorem is referenced by:  nn0negz  12624  nn0ltp1le  12644  nn0leltp1  12645  nn0ltlem1  12646  nn0lt2  12649  nn0le2is012  12650  nn0lem1lt  12651  fnn0ind  12685  nn0pzuz  12913  nn0ge2m1nnALT  12950  fz1n  13545  ige2m1fz  13617  elfz2nn0  13618  fznn0  13619  elfz0add  13626  fzctr  13639  difelfzle  13640  fzoun  13695  fzofzim  13705  fzo1fzo0n0  13709  elincfzoext  13716  elfzodifsumelfzo  13724  fz0add1fz1  13728  zpnn0elfzo  13731  fzossfzop1  13736  ubmelm1fzo  13754  elfznelfzo  13763  flmulnn0  13818  quoremnn0  13847  zmodidfzoimp  13892  modmuladdnn0  13906  modfzo0difsn  13934  expdiv  14104  expnngt1  14229  faclbnd3  14277  bccmpl  14294  bcnp1n  14299  bcval5  14303  bcn2  14304  bcp1m1  14305  hashge2el2difr  14468  fi1uzind  14484  wrdred1  14536  wrdred1hash  14537  ccatalpha  14569  swrdnd0  14633  swrdfv2  14637  swrdsb0eq  14639  swrdsbslen  14640  swrdspsleq  14641  swrdlsw  14643  pfxnd  14663  pfxccatin12lem4  14702  pfxccatin12lem3  14708  pfxccat3  14710  swrdccat  14711  pfxccat3a  14714  revlen  14738  repswswrd  14760  repswccat  14762  cshwidxmodr  14780  cshf1  14786  2cshw  14789  cshweqrep  14797  cshwcshid  14804  cshwcsh2id  14805  cats1fv  14836  swrd2lsw  14929  2swrd2eqwrdeq  14930  isercoll  15640  iseraltlem2  15655  bcxmas  15807  geo2sum2  15846  geomulcvg  15848  risefacval2  15980  fallfacval2  15981  zrisefaccl  15990  zfallfaccl  15991  fallrisefac  15995  bpolylem  16018  fsumkthpow  16026  esum  16050  ege2le3  16060  eftlcl  16077  reeftlcl  16078  eftlub  16079  effsumlt  16081  eirrlem  16174  dvds1  16289  dvdsext  16291  addmodlteqALT  16295  oddnn02np1  16318  oddge22np1  16319  nn0ehalf  16348  nn0o1gt2  16351  nno  16352  nn0o  16353  nn0oddm1d2  16355  divalglem4  16366  divalglem5  16367  modremain  16378  bitsinv1  16410  nn0gcdid0  16489  nn0seqcvgd  16534  algcvga  16543  eucalgf  16547  nonsq  16724  odzdvds  16757  coprimeprodsq  16770  coprimeprodsq2  16771  oddprm  16772  iserodd  16797  pcexp  16821  pcidlem  16834  pc11  16842  dvdsprmpweqle  16848  difsqpwdvds  16849  pcfac  16861  prmunb  16876  hashbc2  16968  cshwshashlem2  17059  smndex1ibas  18845  smndex1iidm  18846  smndex2dnrinv  18860  smndex2dlinvh  18862  mulgaddcom  19046  mulginvcom  19047  mulgz  19050  mulgdirlem  19053  mulgass  19059  mndodcongi  19491  oddvdsnn0  19492  odeq  19498  odmulg  19504  efgsdmi  19680  cyggex2  19845  fincygsubgodd  20062  mulgass2  20238  chrrhm  21454  zncrng  21471  znzrh2  21472  zndvds  21476  znchr  21489  znunit  21490  chfacfisf  22749  chfacfisfcpmat  22750  chfacfscmulfsupp  22754  chfacfpmmulfsupp  22758  clmmulg  25021  itgcnlem  25712  degltlem1  26001  plyco0  26119  dgreq0  26193  plydivex  26225  aannenlem1  26256  abelthlem1  26361  abelthlem3  26363  abelthlem8  26369  abelthlem9  26370  advlogexp  26582  cxpexp  26595  leibpi  26867  log2cnv  26869  log2tlbnd  26870  basellem2  27007  sgmnncl  27072  chpp1  27080  bcmono  27203  bcmax  27204  bcp1ctr  27205  lgsneg1  27248  lgsdirnn0  27270  lgsdinn0  27271  2lgslem1c  27319  2lgslem3a1  27326  2lgslem3b1  27327  2lgslem3c1  27328  2lgsoddprmlem2  27335  2sq2  27359  2sqreultlem  27373  dchrisumlem1  27415  qabvle  27551  ostth2lem2  27560  tgldimor  28299  upgrewlkle2  29413  wlkv0  29458  redwlk  29479  pthdadjvtx  29537  pthdlem1  29573  wwlknvtx  29649  wlkiswwlks2lem3  29675  wwlksm1edg  29685  wwlksnred  29696  wwlksnext  29697  clwlkclwwlklem2a1  29795  clwlkclwwlklem2a2  29796  clwlkclwwlklem2fv1  29798  clwlkclwwlklem2fv2  29799  clwlkclwwlklem2a4  29800  clwlkclwwlklem2a  29801  clwlkclwwlklem2  29803  clwlkclwwlk  29805  clwwisshclwwslem  29817  eucrctshift  30046  eucrct2eupth1  30047  eucrct2eupth  30048  numclwwlk5lem  30190  numclwwlk5  30191  numclwwlk7  30194  frgrreggt1  30196  nndiffz1  32548  xrge0mulgnn0  32739  hashf2  33697  signsvtn0  34196  nn0ltp1ne  34715  0nn0m1nnn0  34716  pthhashvtx  34731  fz0n  35319  bcneg1  35324  bccolsum  35327  faclimlem3  35333  faclim  35334  iprodfac  35335  poimirlem28  37115  mblfinlem1  37124  mblfinlem2  37125  lcmineqlem2  41495  sticksstones22  41634  gcdnn0id  41883  numdenexp  41891  negexpidd  42096  nacsfix  42126  fzsplit1nn0  42168  eldioph2lem1  42174  fz1eqin  42183  diophin  42186  eq0rabdioph  42190  rexrabdioph  42208  rexzrexnn0  42218  irrapxlem4  42239  pell14qrss1234  42270  pell1qrss14  42282  monotoddzz  42358  rmxypos  42362  ltrmynn0  42363  ltrmxnn0  42364  lermxnn0  42365  rmxnn  42366  rmynn0  42372  jm2.17a  42375  jm2.17b  42376  rmygeid  42379  jm2.18  42403  jm2.19lem3  42406  jm2.19lem4  42407  jm2.22  42410  rmxdiophlem  42430  hbt  42548  proot1ex  42618  fzisoeu  44676  stirlinglem5  45460  elfzlble  46694  subsubelfzo0  46700  2ffzoeq  46702  fargshiftfo  46776  fmtnof1  46869  fmtnorec1  46871  goldbachthlem1  46879  odz2prm2pw  46897  flsqrt  46927  lighneallem4  46944  nn0eo  47595  nn0ofldiv2  47599  flnn0div2ge  47600  fllog2  47635  blenpw2  47645  blennngt2o2  47659  nn0digval  47667  dignn0fr  47668  digexp  47674  0dig2nn0e  47679  0dig2nn0o  47680  dig2bits  47681  dignn0flhalflem2  47683  dignn0ehalf  47684  dignn0flhalf  47685  nn0sumshdiglemB  47687

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »