Theorem nn0z 9477

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 9475	. 2 |- NN0 C_ ZZ
2	1	sseli 3220	1 |- ( N e. NN0 -> N e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2200   NN0cn0 9380   ZZcz 9457

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 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8101  ax-resscn 8102  ax-1cn 8103  ax-1re 8104  ax-icn 8105  ax-addcl 8106  ax-addrcl 8107  ax-mulcl 8108  ax-addcom 8110  ax-addass 8112  ax-distr 8114  ax-i2m1 8115  ax-0lt1 8116  ax-0id 8118  ax-rnegex 8119  ax-cnre 8121  ax-pre-ltirr 8122  ax-pre-ltwlin 8123  ax-pre-lttrn 8124  ax-pre-ltadd 8126

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 2801  df-sbc 3029  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-opab 4146  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-iota 5278  df-fun 5320  df-fv 5326  df-riota 5960  df-ov 6010  df-oprab 6011  df-mpo 6012  df-pnf 8194  df-mnf 8195  df-xr 8196  df-ltxr 8197  df-le 8198  df-sub 8330  df-neg 8331  df-inn 9122  df-n0 9381  df-z 9458

This theorem is referenced by:  nn0negz  9491  nn0ltp1le  9520  nn0leltp1  9521  nn0ltlem1  9522  nn0sub  9524  nn0n0n1ge2b  9537  nn0lt10b  9538  nn0lt2  9539  nn0le2is012  9540  nn0lem1lt  9541  fnn0ind  9574  nn0pzuz  9794  nn01to3  9824  nn0ge2m1nnALT  9825  fz1n  10252  ige2m1fz  10318  elfz2nn0  10320  fznn0  10321  elfz0add  10328  fzctr  10341  difelfzle  10342  fzoun  10391  fzo1fzo0n0  10395  fzofzim  10400  elincfzoext  10411  elfzodifsumelfzo  10419  zpnn0elfzo  10425  fzossfzop1  10430  ubmelm1fzo  10444  adddivflid  10524  fldivnn0  10527  divfl0  10528  flqmulnn0  10531  fldivnn0le  10535  zmodidfzoimp  10588  modqmuladdnn0  10602  modifeq2int  10620  modfzo0difsn  10629  uzennn  10670  expdivap  10824  faclbnd3  10977  bccmpl  10988  bcnp1n  10993  bcn2  10998  bcp1m1  10999  iswrd  11086  wrdval  11087  wrdexg  11095  ffz0iswrdnn0  11111  wrdnval  11115  wrdred1  11127  wrdred1hash  11128  ccatalpha  11161  swrdfv2  11210  swrdsb0eq  11212  swrdsbslen  11213  swrdspsleq  11214  swrdlsw  11216  pfx0g  11223  fnpfx  11224  pfxclg  11225  pfxnd  11236  pfxwrdsymbg  11237  pfxccatin12lem4  11273  pfxccatin12lem3  11279  pfxccat3  11281  swrdccat  11282  pfxccat3a  11285  cats1fvd  11313  nn0maxcl  11751  modfsummodlemstep  11983  bcxmas  12015  geo2sum2  12041  mertenslemi1  12061  mertensabs  12063  esum  12188  efcvgfsum  12193  ege2le3  12197  eftlcl  12214  reeftlcl  12215  eftlub  12216  effsumlt  12218  eirraplem  12303  dvds1  12379  dvdsext  12381  addmodlteqALT  12385  3dvds  12390  oddnn02np1  12406  oddge22np1  12407  nn0ehalf  12429  nn0o1gt2  12431  nno  12432  nn0o  12433  nn0oddm1d2  12435  modremain  12455  bitsmod  12482  bitsinv1  12488  gcdn0gt0  12514  nn0gcdid0  12517  bezoutlemmain  12534  nn0seqcvgd  12578  algcvgblem  12586  algcvga  12588  eucalgf  12592  prmndvdsfaclt  12693  nn0sqrtelqelz  12743  nonsq  12744  crth  12761  odzdvds  12783  coprimeprodsq  12795  coprimeprodsq2  12796  oddprm  12797  pcexp  12847  pcdvdsb  12858  pc11  12869  dvdsprmpweqle  12875  difsqpwdvds  12876  pcfac  12888  prmunb  12900  4sqexercise1  12936  4sqexercise2  12937  4sqlemsdc  12938  modxai  12954  mulgaddcom  13698  mulginvcom  13699  mulgz  13702  mulgdirlem  13705  mulgass  13711  mulgass2  14036  zncrng  14624  znzrh2  14625  zndvds  14628  znf1o  14630  znunit  14638  elply2  15424  elplyd  15430  dvply2g  15455  sgmnncl  15677  0sgmppw  15682  lgsneg1  15719  lgsdirnn0  15741  lgsdinn0  15742  2lgslem1c  15784  2lgslem3a1  15791  2lgslem3b1  15792  2lgslem3c1  15793  2lgsoddprmlem2  15800  wlkv0  16110