Theorem nn0z 9498

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

Assertion

Ref	Expression
nn0z	|- ( N e. NN0 -> N e. ZZ )

Proof of Theorem nn0z

Step	Hyp	Ref	Expression
1		nn0ssz 9496	. 2 |- NN0 C_ ZZ
2	1	sseli 3223	1 |- ( N e. NN0 -> N e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2202   NN0cn0 9401   ZZcz 9478

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 8122  ax-resscn 8123  ax-1cn 8124  ax-1re 8125  ax-icn 8126  ax-addcl 8127  ax-addrcl 8128  ax-mulcl 8129  ax-addcom 8131  ax-addass 8133  ax-distr 8135  ax-i2m1 8136  ax-0lt1 8137  ax-0id 8139  ax-rnegex 8140  ax-cnre 8142  ax-pre-ltirr 8143  ax-pre-ltwlin 8144  ax-pre-lttrn 8145  ax-pre-ltadd 8147

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 5970  df-ov 6020  df-oprab 6021  df-mpo 6022  df-pnf 8215  df-mnf 8216  df-xr 8217  df-ltxr 8218  df-le 8219  df-sub 8351  df-neg 8352  df-inn 9143  df-n0 9402  df-z 9479

This theorem is referenced by:  nn0negz  9512  nn0ltp1le  9541  nn0leltp1  9542  nn0ltlem1  9543  nn0sub  9545  nn0n0n1ge2b  9558  nn0lt10b  9559  nn0lt2  9560  nn0le2is012  9561  nn0lem1lt  9562  fnn0ind  9595  nn0pzuz  9820  nn01to3  9850  nn0ge2m1nnALT  9851  fz1n  10278  ige2m1fz  10344  elfz2nn0  10346  fznn0  10347  elfz0add  10354  fzctr  10367  difelfzle  10368  fzoun  10417  fzo1fzo0n0  10421  fzofzim  10426  elincfzoext  10437  elfzodifsumelfzo  10445  zpnn0elfzo  10451  fzossfzop1  10456  ubmelm1fzo  10470  adddivflid  10551  fldivnn0  10554  divfl0  10555  flqmulnn0  10558  fldivnn0le  10562  zmodidfzoimp  10615  modqmuladdnn0  10629  modifeq2int  10647  modfzo0difsn  10656  uzennn  10697  expdivap  10851  faclbnd3  11004  bccmpl  11015  bcnp1n  11020  bcn2  11025  bcp1m1  11026  iswrd  11114  wrdval  11115  wrdexg  11123  ffz0iswrdnn0  11139  wrdnval  11143  wrdred1  11155  wrdred1hash  11156  ccatalpha  11189  swrdfv2  11243  swrdsb0eq  11245  swrdsbslen  11246  swrdspsleq  11247  swrdlsw  11249  pfx0g  11256  fnpfx  11257  pfxclg  11258  pfxnd  11269  pfxwrdsymbg  11270  pfxccatin12lem4  11306  pfxccatin12lem3  11312  pfxccat3  11314  swrdccat  11315  pfxccat3a  11318  cats1fvd  11346  nn0maxcl  11785  modfsummodlemstep  12017  bcxmas  12049  geo2sum2  12075  mertenslemi1  12095  mertensabs  12097  esum  12222  efcvgfsum  12227  ege2le3  12231  eftlcl  12248  reeftlcl  12249  eftlub  12250  effsumlt  12252  eirraplem  12337  dvds1  12413  dvdsext  12415  addmodlteqALT  12419  3dvds  12424  oddnn02np1  12440  oddge22np1  12441  nn0ehalf  12463  nn0o1gt2  12465  nno  12466  nn0o  12467  nn0oddm1d2  12469  modremain  12489  bitsmod  12516  bitsinv1  12522  gcdn0gt0  12548  nn0gcdid0  12551  bezoutlemmain  12568  nn0seqcvgd  12612  algcvgblem  12620  algcvga  12622  eucalgf  12626  prmndvdsfaclt  12727  nn0sqrtelqelz  12777  nonsq  12778  crth  12795  odzdvds  12817  coprimeprodsq  12829  coprimeprodsq2  12830  oddprm  12831  pcexp  12881  pcdvdsb  12892  pc11  12903  dvdsprmpweqle  12909  difsqpwdvds  12910  pcfac  12922  prmunb  12934  4sqexercise1  12970  4sqexercise2  12971  4sqlemsdc  12972  modxai  12988  mulgaddcom  13732  mulginvcom  13733  mulgz  13736  mulgdirlem  13739  mulgass  13745  mulgass2  14070  zncrng  14658  znzrh2  14659  zndvds  14662  znf1o  14664  znunit  14672  elply2  15458  elplyd  15464  dvply2g  15489  sgmnncl  15711  0sgmppw  15716  lgsneg1  15753  lgsdirnn0  15775  lgsdinn0  15776  2lgslem1c  15818  2lgslem3a1  15825  2lgslem3b1  15826  2lgslem3c1  15827  2lgsoddprmlem2  15834  wlkv0  16219