Theorem nn0z 9643

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

Syntax hints:   -> wi 4   e. wcel 2209   NN0cn0 9542   ZZcz 9623

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4244  ax-pow 4306  ax-pr 4341  ax-un 4573  ax-setind 4679  ax-cnex 8260  ax-resscn 8261  ax-1cn 8262  ax-1re 8263  ax-icn 8264  ax-addcl 8265  ax-addrcl 8266  ax-mulcl 8267  ax-addcom 8269  ax-addass 8271  ax-distr 8273  ax-i2m1 8274  ax-0lt1 8275  ax-0id 8277  ax-rnegex 8278  ax-cnre 8280  ax-pre-ltirr 8281  ax-pre-ltwlin 8282  ax-pre-lttrn 8283  ax-pre-ltadd 8285

This theorem depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-int 3966  df-br 4126  df-opab 4188  df-id 4433  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-iota 5332  df-fun 5374  df-fv 5380  df-riota 6028  df-ov 6078  df-oprab 6079  df-mpo 6080  df-pnf 8352  df-mnf 8353  df-xr 8354  df-ltxr 8355  df-le 8356  df-sub 8489  df-neg 8490  df-inn 9284  df-n0 9543  df-z 9624

This theorem is referenced by:  nn0negz  9657  nn0ltp1le  9686  nn0leltp1  9687  nn0ltlem1  9688  nn0sub  9690  nn0n0n1ge2b  9704  nn0lt10b  9705  nn0lt2  9706  nn0le2is012  9707  nn0lem1lt  9708  fnn0ind  9741  nn0pzuz  9966  nn01to3  9996  nn0ge2m1nnALT  9997  fz1n  10427  ige2m1fz  10495  elfz2nn0  10497  fznn0  10498  elfz0add  10505  fzctr  10518  difelfzle  10519  fzoun  10568  fzo1fzo0n0  10573  fzofzim  10578  elincfzoext  10589  elfzodifsumelfzo  10597  zpnn0elfzo  10603  fzossfzop1  10608  ubmelm1fzo  10622  adddivflid  10705  fldivnn0  10708  divfl0  10709  flqmulnn0  10712  fldivnn0le  10716  zmodidfzoimp  10769  modqmuladdnn0  10783  modifeq2int  10801  modfzo0difsn  10810  uzennn  10851  expdivap  11005  faclbnd3  11159  bccmpl  11170  bcnp1n  11175  bcn2  11180  bcp1m1  11181  iswrd  11284  wrdval  11285  wrdexg  11293  ffz0iswrdnn0  11309  wrdnval  11313  wrdred1  11325  wrdred1hash  11326  ccatalpha  11359  swrdfv2  11413  swrdsb0eq  11415  swrdsbslen  11416  swrdspsleq  11417  swrdlsw  11419  pfx0g  11426  fnpfx  11427  pfxclg  11428  pfxnd  11439  pfxwrdsymbg  11440  pfxccatin12lem4  11476  pfxccatin12lem3  11482  pfxccat3  11484  swrdccat  11485  pfxccat3a  11488  cats1fvd  11516  nn0maxcl  11969  modfsummodlemstep  12202  bcxmas  12234  geo2sum2  12260  mertenslemi1  12280  mertensabs  12282  esum  12407  efcvgfsum  12412  ege2le3  12416  eftlcl  12433  reeftlcl  12434  eftlub  12435  effsumlt  12437  eirraplem  12522  dvds1  12598  dvdsext  12600  addmodlteqALT  12604  3dvds  12609  oddnn02np1  12625  oddge22np1  12626  nn0ehalf  12648  nn0o1gt2  12650  nno  12651  nn0o  12652  nn0oddm1d2  12654  modremain  12674  bitsmod  12701  bitsinv1  12707  gcdn0gt0  12733  nn0gcdid0  12736  bezoutlemmain  12753  nn0seqcvgd  12797  algcvgblem  12805  algcvga  12807  eucalgf  12811  prmndvdsfaclt  12912  nn0sqrtelqelz  12962  nonsq  12963  crth  12980  odzdvds  13002  coprimeprodsq  13014  coprimeprodsq2  13015  oddprm  13016  pcexp  13066  pcdvdsb  13077  pc11  13088  dvdsprmpweqle  13094  difsqpwdvds  13095  pcfac  13107  prmunb  13119  4sqexercise1  13155  4sqexercise2  13156  4sqlemsdc  13157  modxai  13173  mulgaddcom  13926  mulginvcom  13927  mulgz  13930  mulgdirlem  13933  mulgass  13939  mulgass2  14336  zncrng  14952  znzrh2  14953  zndvds  14956  znf1o  14958  znunit  14966  elply2  15759  elplyd  15765  dvply2g  15790  sgmnncl  16016  0sgmppw  16021  lgsneg1  16058  lgsdirnn0  16080  lgsdinn0  16081  2lgslem1c  16123  2lgslem3a1  16130  2lgslem3b1  16131  2lgslem3c1  16132  2lgsoddprmlem2  16139  wlkv0  16524