Theorem nn0z 9272

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

Syntax hints:   -> wi 4   e. wcel 2148   NN0cn0 9175   ZZcz 9252

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-addcom 7910  ax-addass 7912  ax-distr 7914  ax-i2m1 7915  ax-0lt1 7916  ax-0id 7918  ax-rnegex 7919  ax-cnre 7921  ax-pre-ltirr 7922  ax-pre-ltwlin 7923  ax-pre-lttrn 7924  ax-pre-ltadd 7926

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-br 4004  df-opab 4065  df-id 4293  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-iota 5178  df-fun 5218  df-fv 5224  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-pnf 7993  df-mnf 7994  df-xr 7995  df-ltxr 7996  df-le 7997  df-sub 8129  df-neg 8130  df-inn 8919  df-n0 9176  df-z 9253

This theorem is referenced by:  nn0negz  9286  nn0ltp1le  9314  nn0leltp1  9315  nn0ltlem1  9316  nn0sub  9318  nn0n0n1ge2b  9331  nn0lt10b  9332  nn0lt2  9333  nn0le2is012  9334  nn0lem1lt  9335  fnn0ind  9368  nn0pzuz  9586  nn01to3  9616  nn0ge2m1nnALT  9617  fz1n  10043  ige2m1fz  10109  elfz2nn0  10111  fznn0  10112  elfz0add  10119  fzctr  10132  difelfzle  10133  fzo1fzo0n0  10182  fzofzim  10187  elfzodifsumelfzo  10200  zpnn0elfzo  10206  fzossfzop1  10211  ubmelm1fzo  10225  adddivflid  10291  fldivnn0  10294  divfl0  10295  flqmulnn0  10298  fldivnn0le  10302  zmodidfzoimp  10353  modqmuladdnn0  10367  modifeq2int  10385  modfzo0difsn  10394  uzennn  10435  expdivap  10570  faclbnd3  10722  bccmpl  10733  bcnp1n  10738  bcn2  10743  bcp1m1  10744  modfsummodlemstep  11464  bcxmas  11496  geo2sum2  11522  mertenslemi1  11542  mertensabs  11544  esum  11669  efcvgfsum  11674  ege2le3  11678  eftlcl  11695  reeftlcl  11696  eftlub  11697  effsumlt  11699  eirraplem  11783  dvds1  11858  dvdsext  11860  addmodlteqALT  11864  oddnn02np1  11884  oddge22np1  11885  nn0ehalf  11907  nn0o1gt2  11909  nno  11910  nn0o  11911  nn0oddm1d2  11913  modremain  11933  gcdn0gt0  11978  nn0gcdid0  11981  bezoutlemmain  11998  nn0seqcvgd  12040  algcvgblem  12048  algcvga  12050  eucalgf  12054  prmndvdsfaclt  12155  nn0sqrtelqelz  12205  nonsq  12206  crth  12223  odzdvds  12244  coprimeprodsq  12256  coprimeprodsq2  12257  oddprm  12258  pcexp  12308  pcdvdsb  12318  pc11  12329  dvdsprmpweqle  12335  difsqpwdvds  12336  pcfac  12347  prmunb  12359  mulgaddcom  13005  mulginvcom  13006  mulgz  13009  mulgdirlem  13012  mulgass  13018  mulgass2  13233  lgsneg1  14396  lgsdirnn0  14418  lgsdinn0  14419  2lgsoddprmlem2  14424