Theorem nn0z 9676

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℕ₀cn0 9575  ℤcz 9656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-cnex 8277  ax-resscn 8278  ax-1cn 8279  ax-1re 8280  ax-icn 8281  ax-addcl 8282  ax-addrcl 8283  ax-mulcl 8284  ax-addcom 8286  ax-addass 8288  ax-distr 8290  ax-i2m1 8291  ax-0lt1 8292  ax-0id 8294  ax-rnegex 8295  ax-cnre 8297  ax-pre-ltirr 8298  ax-pre-ltwlin 8299  ax-pre-lttrn 8300  ax-pre-ltadd 8302

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4132  df-opab 4194  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-iota 5340  df-fun 5382  df-fv 5388  df-riota 6041  df-ov 6091  df-oprab 6092  df-mpo 6093  df-pnf 8369  df-mnf 8370  df-xr 8371  df-ltxr 8372  df-le 8373  df-sub 8507  df-neg 8508  df-inn 9315  df-n0 9576  df-z 9657

This theorem is used by:  nn0negz  9690  nn0ltp1le  9719  nn0leltp1  9720  nn0ltlem1  9721  nn0sub  9723  nn0n0n1ge2b  9737  nn0lt10b  9738  nn0lt2  9739  nn0le2is012  9740  nn0lem1lt  9741  fnn0ind  9774  nn0pzuz  10004  nn01to3  10034  nn0ge2m1nnALT  10035  fz1n  10466  ige2m1fz  10535  elfz2nn0  10537  fznn0  10538  elfz0add  10545  fzctr  10558  difelfzle  10559  fzoun  10608  fzo1fzo0n0  10613  fzofzim  10618  elincfzoext  10629  elfzodifsumelfzo  10637  zpnn0elfzo  10643  fzossfzop1  10648  ubmelm1fzo  10662  adddivflid  10749  fldivnn0  10752  divfl0  10753  flqmulnn0  10756  fldivnn0le  10760  zmodidfzoimp  10813  modqmuladdnn0  10827  modifeq2int  10845  modfzo0difsn  10854  uzennn  10895  expdivap  11049  nn0sqdc  11169  faclbnd3  11204  bccmpl  11215  bcnp1n  11220  bcn2  11225  bcp1m1  11226  iswrd  11329  wrdval  11330  wrdexg  11338  ffz0iswrdnn0  11354  wrdnval  11358  wrdred1  11370  wrdred1hash  11371  ccatalpha  11404  swrdfv2  11458  swrdsb0eq  11460  swrdsbslen  11461  swrdspsleq  11462  swrdlsw  11464  pfx0g  11471  fnpfx  11472  pfxclg  11473  pfxnd  11484  pfxwrdsymbg  11485  pfxccatin12lem4  11521  pfxccatin12lem3  11527  pfxccat3  11529  swrdccat  11530  pfxccat3a  11533  cats1fvd  11561  nn0maxcl  12015  modfsummodlemstep  12250  bcxmas  12282  geo2sum2  12308  mertenslemi1  12328  mertensabs  12330  esum  12455  efcvgfsum  12460  ege2le3  12464  eftlcl  12481  reeftlcl  12482  eftlub  12483  effsumlt  12485  eirraplem  12570  dvds1  12646  dvdsext  12648  addmodlteqALT  12652  3dvds  12657  oddnn02np1  12673  oddge22np1  12674  nn0ehalf  12696  nn0o1gt2  12698  nno  12699  nn0o  12700  nn0oddm1d2  12702  modremain  12722  bitsmod  12749  bitsinv1  12755  gcdn0gt0  12781  nn0gcdid0  12784  bezoutlemmain  12801  nn0seqcvgd  12845  algcvgblem  12853  algcvga  12855  eucalgf  12859  prmndvdsfaclt  12961  nn0sqrtelqelz  13012  nonsq  13013  sqrtrirr  13015  crth  13032  odzdvds  13054  coprimeprodsq  13066  coprimeprodsq2  13067  oddprm  13068  pcexp  13118  pcdvdsb  13129  pc11  13140  dvdsprmpweqle  13146  difsqpwdvds  13147  pcfac  13159  prmunb  13171  4sqexercise1  13207  4sqexercise2  13208  4sqlemsdc  13209  modxai  13225  mulgaddcom  14009  mulginvcom  14010  mulgz  14013  mulgdirlem  14016  mulgass  14022  mulgass2  14471  zncrng  15090  znzrh2  15091  zndvds  15094  znf1o  15096  znunit  15104  elply2  15973  elplyd  15979  dvply2g  16004  log2tlbndlog2  16232  birthdaylem1g  16237  birthdaylem3  16239  sgmnncl  16269  0sgmppw  16299  bcmono  16316  bcmax  16317  bcp1ctr  16318  lgsneg1  16361  lgsdirnn0  16383  lgsdinn0  16384  2lgslem1c  16426  2lgslem3a1  16433  2lgslem3b1  16434  2lgslem3c1  16435  2lgsoddprmlem2  16442  wlkv0  16827