Theorem nn0z 9499

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

Syntax hints:   -> wi 4   e. wcel 2202   NN0cn0 9402   ZZcz 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  11803  modfsummodlemstep  12036  bcxmas  12068  geo2sum2  12094  mertenslemi1  12114  mertensabs  12116  esum  12241  efcvgfsum  12246  ege2le3  12250  eftlcl  12267  reeftlcl  12268  eftlub  12269  effsumlt  12271  eirraplem  12356  dvds1  12432  dvdsext  12434  addmodlteqALT  12438  3dvds  12443  oddnn02np1  12459  oddge22np1  12460  nn0ehalf  12482  nn0o1gt2  12484  nno  12485  nn0o  12486  nn0oddm1d2  12488  modremain  12508  bitsmod  12535  bitsinv1  12541  gcdn0gt0  12567  nn0gcdid0  12570  bezoutlemmain  12587  nn0seqcvgd  12631  algcvgblem  12639  algcvga  12641  eucalgf  12645  prmndvdsfaclt  12746  nn0sqrtelqelz  12796  nonsq  12797  crth  12814  odzdvds  12836  coprimeprodsq  12848  coprimeprodsq2  12849  oddprm  12850  pcexp  12900  pcdvdsb  12911  pc11  12922  dvdsprmpweqle  12928  difsqpwdvds  12929  pcfac  12941  prmunb  12953  4sqexercise1  12989  4sqexercise2  12990  4sqlemsdc  12991  modxai  13007  mulgaddcom  13751  mulginvcom  13752  mulgz  13755  mulgdirlem  13758  mulgass  13764  mulgass2  14090  zncrng  14678  znzrh2  14679  zndvds  14682  znf1o  14684  znunit  14692  elply2  15478  elplyd  15484  dvply2g  15509  sgmnncl  15731  0sgmppw  15736  lgsneg1  15773  lgsdirnn0  15795  lgsdinn0  15796  2lgslem1c  15838  2lgslem3a1  15845  2lgslem3b1  15846  2lgslem3c1  15847  2lgsoddprmlem2  15854  wlkv0  16239