Theorem nn0z 9499

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℕ₀cn0 9402  ℤcz 9479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-addcom 8132  ax-addass 8134  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-0id 8140  ax-rnegex 8141  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-ltadd 8148

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-inn 9144  df-n0 9403  df-z 9480

This theorem is referenced by:  nn0negz  9513  nn0ltp1le  9542  nn0leltp1  9543  nn0ltlem1  9544  nn0sub  9546  nn0n0n1ge2b  9559  nn0lt10b  9560  nn0lt2  9561  nn0le2is012  9562  nn0lem1lt  9563  fnn0ind  9596  nn0pzuz  9821  nn01to3  9851  nn0ge2m1nnALT  9852  fz1n  10279  ige2m1fz  10345  elfz2nn0  10347  fznn0  10348  elfz0add  10355  fzctr  10368  difelfzle  10369  fzoun  10418  fzo1fzo0n0  10423  fzofzim  10428  elincfzoext  10439  elfzodifsumelfzo  10447  zpnn0elfzo  10453  fzossfzop1  10458  ubmelm1fzo  10472  adddivflid  10553  fldivnn0  10556  divfl0  10557  flqmulnn0  10560  fldivnn0le  10564  zmodidfzoimp  10617  modqmuladdnn0  10631  modifeq2int  10649  modfzo0difsn  10658  uzennn  10699  expdivap  10853  faclbnd3  11006  bccmpl  11017  bcnp1n  11022  bcn2  11027  bcp1m1  11028  iswrd  11119  wrdval  11120  wrdexg  11128  ffz0iswrdnn0  11144  wrdnval  11148  wrdred1  11160  wrdred1hash  11161  ccatalpha  11194  swrdfv2  11248  swrdsb0eq  11250  swrdsbslen  11251  swrdspsleq  11252  swrdlsw  11254  pfx0g  11261  fnpfx  11262  pfxclg  11263  pfxnd  11274  pfxwrdsymbg  11275  pfxccatin12lem4  11311  pfxccatin12lem3  11317  pfxccat3  11319  swrdccat  11320  pfxccat3a  11323  cats1fvd  11351  nn0maxcl  11790  modfsummodlemstep  12023  bcxmas  12055  geo2sum2  12081  mertenslemi1  12101  mertensabs  12103  esum  12228  efcvgfsum  12233  ege2le3  12237  eftlcl  12254  reeftlcl  12255  eftlub  12256  effsumlt  12258  eirraplem  12343  dvds1  12419  dvdsext  12421  addmodlteqALT  12425  3dvds  12430  oddnn02np1  12446  oddge22np1  12447  nn0ehalf  12469  nn0o1gt2  12471  nno  12472  nn0o  12473  nn0oddm1d2  12475  modremain  12495  bitsmod  12522  bitsinv1  12528  gcdn0gt0  12554  nn0gcdid0  12557  bezoutlemmain  12574  nn0seqcvgd  12618  algcvgblem  12626  algcvga  12628  eucalgf  12632  prmndvdsfaclt  12733  nn0sqrtelqelz  12783  nonsq  12784  crth  12801  odzdvds  12823  coprimeprodsq  12835  coprimeprodsq2  12836  oddprm  12837  pcexp  12887  pcdvdsb  12898  pc11  12909  dvdsprmpweqle  12915  difsqpwdvds  12916  pcfac  12928  prmunb  12940  4sqexercise1  12976  4sqexercise2  12977  4sqlemsdc  12978  modxai  12994  mulgaddcom  13738  mulginvcom  13739  mulgz  13742  mulgdirlem  13745  mulgass  13751  mulgass2  14077  zncrng  14665  znzrh2  14666  zndvds  14669  znf1o  14671  znunit  14679  elply2  15465  elplyd  15471  dvply2g  15496  sgmnncl  15718  0sgmppw  15723  lgsneg1  15760  lgsdirnn0  15782  lgsdinn0  15783  2lgslem1c  15825  2lgslem3a1  15832  2lgslem3b1  15833  2lgslem3c1  15834  2lgsoddprmlem2  15841  wlkv0  16226