Theorem nn0z 9543

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

Syntax hints:   -> wi 4   e. wcel 2202   NN0cn0 9444   ZZcz 9523

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-un 4536  ax-setind 4641  ax-cnex 8166  ax-resscn 8167  ax-1cn 8168  ax-1re 8169  ax-icn 8170  ax-addcl 8171  ax-addrcl 8172  ax-mulcl 8173  ax-addcom 8175  ax-addass 8177  ax-distr 8179  ax-i2m1 8180  ax-0lt1 8181  ax-0id 8183  ax-rnegex 8184  ax-cnre 8186  ax-pre-ltirr 8187  ax-pre-ltwlin 8188  ax-pre-lttrn 8189  ax-pre-ltadd 8191

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-nel 2499  df-ral 2516  df-rex 2517  df-reu 2518  df-rab 2520  df-v 2805  df-sbc 3033  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-int 3934  df-br 4094  df-opab 4156  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-iota 5293  df-fun 5335  df-fv 5341  df-riota 5981  df-ov 6031  df-oprab 6032  df-mpo 6033  df-pnf 8258  df-mnf 8259  df-xr 8260  df-ltxr 8261  df-le 8262  df-sub 8394  df-neg 8395  df-inn 9186  df-n0 9445  df-z 9524

This theorem is referenced by:  nn0negz  9557  nn0ltp1le  9586  nn0leltp1  9587  nn0ltlem1  9588  nn0sub  9590  nn0n0n1ge2b  9603  nn0lt10b  9604  nn0lt2  9605  nn0le2is012  9606  nn0lem1lt  9607  fnn0ind  9640  nn0pzuz  9865  nn01to3  9895  nn0ge2m1nnALT  9896  fz1n  10324  ige2m1fz  10390  elfz2nn0  10392  fznn0  10393  elfz0add  10400  fzctr  10413  difelfzle  10414  fzoun  10463  fzo1fzo0n0  10468  fzofzim  10473  elincfzoext  10484  elfzodifsumelfzo  10492  zpnn0elfzo  10498  fzossfzop1  10503  ubmelm1fzo  10517  adddivflid  10598  fldivnn0  10601  divfl0  10602  flqmulnn0  10605  fldivnn0le  10609  zmodidfzoimp  10662  modqmuladdnn0  10676  modifeq2int  10694  modfzo0difsn  10703  uzennn  10744  expdivap  10898  faclbnd3  11051  bccmpl  11062  bcnp1n  11067  bcn2  11072  bcp1m1  11073  iswrd  11164  wrdval  11165  wrdexg  11173  ffz0iswrdnn0  11189  wrdnval  11193  wrdred1  11205  wrdred1hash  11206  ccatalpha  11239  swrdfv2  11293  swrdsb0eq  11295  swrdsbslen  11296  swrdspsleq  11297  swrdlsw  11299  pfx0g  11306  fnpfx  11307  pfxclg  11308  pfxnd  11319  pfxwrdsymbg  11320  pfxccatin12lem4  11356  pfxccatin12lem3  11362  pfxccat3  11364  swrdccat  11365  pfxccat3a  11368  cats1fvd  11396  nn0maxcl  11848  modfsummodlemstep  12081  bcxmas  12113  geo2sum2  12139  mertenslemi1  12159  mertensabs  12161  esum  12286  efcvgfsum  12291  ege2le3  12295  eftlcl  12312  reeftlcl  12313  eftlub  12314  effsumlt  12316  eirraplem  12401  dvds1  12477  dvdsext  12479  addmodlteqALT  12483  3dvds  12488  oddnn02np1  12504  oddge22np1  12505  nn0ehalf  12527  nn0o1gt2  12529  nno  12530  nn0o  12531  nn0oddm1d2  12533  modremain  12553  bitsmod  12580  bitsinv1  12586  gcdn0gt0  12612  nn0gcdid0  12615  bezoutlemmain  12632  nn0seqcvgd  12676  algcvgblem  12684  algcvga  12686  eucalgf  12690  prmndvdsfaclt  12791  nn0sqrtelqelz  12841  nonsq  12842  crth  12859  odzdvds  12881  coprimeprodsq  12893  coprimeprodsq2  12894  oddprm  12895  pcexp  12945  pcdvdsb  12956  pc11  12967  dvdsprmpweqle  12973  difsqpwdvds  12974  pcfac  12986  prmunb  12998  4sqexercise1  13034  4sqexercise2  13035  4sqlemsdc  13036  modxai  13052  mulgaddcom  13796  mulginvcom  13797  mulgz  13800  mulgdirlem  13803  mulgass  13809  mulgass2  14135  zncrng  14724  znzrh2  14725  zndvds  14728  znf1o  14730  znunit  14738  elply2  15529  elplyd  15535  dvply2g  15560  sgmnncl  15785  0sgmppw  15790  lgsneg1  15827  lgsdirnn0  15849  lgsdinn0  15850  2lgslem1c  15892  2lgslem3a1  15899  2lgslem3b1  15900  2lgslem3c1  15901  2lgsoddprmlem2  15908  wlkv0  16293