Theorem nn0z 9492

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℕ₀cn0 9395  ℤcz 9472

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-cnex 8116  ax-resscn 8117  ax-1cn 8118  ax-1re 8119  ax-icn 8120  ax-addcl 8121  ax-addrcl 8122  ax-mulcl 8123  ax-addcom 8125  ax-addass 8127  ax-distr 8129  ax-i2m1 8130  ax-0lt1 8131  ax-0id 8133  ax-rnegex 8134  ax-cnre 8136  ax-pre-ltirr 8137  ax-pre-ltwlin 8138  ax-pre-lttrn 8139  ax-pre-ltadd 8141

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2802  df-sbc 3030  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-int 3927  df-br 4087  df-opab 4149  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-iota 5284  df-fun 5326  df-fv 5332  df-riota 5966  df-ov 6016  df-oprab 6017  df-mpo 6018  df-pnf 8209  df-mnf 8210  df-xr 8211  df-ltxr 8212  df-le 8213  df-sub 8345  df-neg 8346  df-inn 9137  df-n0 9396  df-z 9473

This theorem is referenced by:  nn0negz  9506  nn0ltp1le  9535  nn0leltp1  9536  nn0ltlem1  9537  nn0sub  9539  nn0n0n1ge2b  9552  nn0lt10b  9553  nn0lt2  9554  nn0le2is012  9555  nn0lem1lt  9556  fnn0ind  9589  nn0pzuz  9814  nn01to3  9844  nn0ge2m1nnALT  9845  fz1n  10272  ige2m1fz  10338  elfz2nn0  10340  fznn0  10341  elfz0add  10348  fzctr  10361  difelfzle  10362  fzoun  10411  fzo1fzo0n0  10415  fzofzim  10420  elincfzoext  10431  elfzodifsumelfzo  10439  zpnn0elfzo  10445  fzossfzop1  10450  ubmelm1fzo  10464  adddivflid  10545  fldivnn0  10548  divfl0  10549  flqmulnn0  10552  fldivnn0le  10556  zmodidfzoimp  10609  modqmuladdnn0  10623  modifeq2int  10641  modfzo0difsn  10650  uzennn  10691  expdivap  10845  faclbnd3  10998  bccmpl  11009  bcnp1n  11014  bcn2  11019  bcp1m1  11020  iswrd  11108  wrdval  11109  wrdexg  11117  ffz0iswrdnn0  11133  wrdnval  11137  wrdred1  11149  wrdred1hash  11150  ccatalpha  11183  swrdfv2  11237  swrdsb0eq  11239  swrdsbslen  11240  swrdspsleq  11241  swrdlsw  11243  pfx0g  11250  fnpfx  11251  pfxclg  11252  pfxnd  11263  pfxwrdsymbg  11264  pfxccatin12lem4  11300  pfxccatin12lem3  11306  pfxccat3  11308  swrdccat  11309  pfxccat3a  11312  cats1fvd  11340  nn0maxcl  11779  modfsummodlemstep  12011  bcxmas  12043  geo2sum2  12069  mertenslemi1  12089  mertensabs  12091  esum  12216  efcvgfsum  12221  ege2le3  12225  eftlcl  12242  reeftlcl  12243  eftlub  12244  effsumlt  12246  eirraplem  12331  dvds1  12407  dvdsext  12409  addmodlteqALT  12413  3dvds  12418  oddnn02np1  12434  oddge22np1  12435  nn0ehalf  12457  nn0o1gt2  12459  nno  12460  nn0o  12461  nn0oddm1d2  12463  modremain  12483  bitsmod  12510  bitsinv1  12516  gcdn0gt0  12542  nn0gcdid0  12545  bezoutlemmain  12562  nn0seqcvgd  12606  algcvgblem  12614  algcvga  12616  eucalgf  12620  prmndvdsfaclt  12721  nn0sqrtelqelz  12771  nonsq  12772  crth  12789  odzdvds  12811  coprimeprodsq  12823  coprimeprodsq2  12824  oddprm  12825  pcexp  12875  pcdvdsb  12886  pc11  12897  dvdsprmpweqle  12903  difsqpwdvds  12904  pcfac  12916  prmunb  12928  4sqexercise1  12964  4sqexercise2  12965  4sqlemsdc  12966  modxai  12982  mulgaddcom  13726  mulginvcom  13727  mulgz  13730  mulgdirlem  13733  mulgass  13739  mulgass2  14064  zncrng  14652  znzrh2  14653  zndvds  14656  znf1o  14658  znunit  14666  elply2  15452  elplyd  15458  dvply2g  15483  sgmnncl  15705  0sgmppw  15710  lgsneg1  15747  lgsdirnn0  15769  lgsdinn0  15770  2lgslem1c  15812  2lgslem3a1  15819  2lgslem3b1  15820  2lgslem3c1  15821  2lgsoddprmlem2  15828  wlkv0  16180