Theorem nn0z 8695

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

Syntax hints:   -> wi 4   e. wcel 1436   NN0cn0 8598   ZZcz 8675

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3930  ax-pow 3982  ax-pr 4008  ax-un 4232  ax-setind 4324  ax-cnex 7372  ax-resscn 7373  ax-1cn 7374  ax-1re 7375  ax-icn 7376  ax-addcl 7377  ax-addrcl 7378  ax-mulcl 7379  ax-addcom 7381  ax-addass 7383  ax-distr 7385  ax-i2m1 7386  ax-0lt1 7387  ax-0id 7389  ax-rnegex 7390  ax-cnre 7392  ax-pre-ltirr 7393  ax-pre-ltwlin 7394  ax-pre-lttrn 7395  ax-pre-ltadd 7397

This theorem depends on definitions:  df-bi 115  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-nel 2347  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2617  df-sbc 2830  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-pw 3416  df-sn 3436  df-pr 3437  df-op 3439  df-uni 3636  df-int 3671  df-br 3820  df-opab 3874  df-id 4092  df-xp 4415  df-rel 4416  df-cnv 4417  df-co 4418  df-dm 4419  df-iota 4942  df-fun 4979  df-fv 4985  df-riota 5562  df-ov 5609  df-oprab 5610  df-mpt2 5611  df-pnf 7460  df-mnf 7461  df-xr 7462  df-ltxr 7463  df-le 7464  df-sub 7591  df-neg 7592  df-inn 8350  df-n0 8599  df-z 8676

This theorem is referenced by:  nn0negz  8709  nn0ltp1le  8737  nn0leltp1  8738  nn0ltlem1  8739  nn0sub  8741  nn0n0n1ge2b  8751  nn0lt10b  8752  nn0lt2  8753  nn0lem1lt  8754  fnn0ind  8787  nn0pzuz  8999  nn01to3  9026  nn0ge2m1nnALT  9027  fz1n  9382  ige2m1fz  9446  elfz2nn0  9448  fznn0  9449  elfz0add  9454  fzctr  9464  difelfzle  9465  fzo1fzo0n0  9514  fzofzim  9519  elfzodifsumelfzo  9532  zpnn0elfzo  9538  fzossfzop1  9543  ubmelm1fzo  9557  adddivflid  9619  fldivnn0  9622  divfl0  9623  flqmulnn0  9626  fldivnn0le  9630  zmodidfzoimp  9681  modqmuladdnn0  9695  modifeq2int  9713  modfzo0difsn  9722  expdivap  9896  faclbnd3  10039  bccmpl  10050  bcnp1n  10055  bcn2  10060  bcp1m1  10061  dvds1  10720  dvdsext  10722  addmodlteqALT  10726  oddnn02np1  10746  oddge22np1  10747  nn0ehalf  10769  nn0o1gt2  10771  nno  10772  nn0o  10773  nn0oddm1d2  10775  modremain  10795  gcdn0gt0  10835  nn0gcdid0  10838  bezoutlemmain  10853  nn0seqcvgd  10889  algcvgblem  10897  ialgcvga  10899  eucalgf  10903  prmndvdsfaclt  11001  nn0sqrtelqelz  11050  nonsq  11051  crth  11066