Theorem nnz 8705

Description: A positive integer is an integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nnz	|- ( N e. NN -> N e. ZZ )

Proof of Theorem nnz

Step	Hyp	Ref	Expression
1		nnssz 8703	. 2 |- NN C_ ZZ
2	1	sseli 3010	1 |- ( N e. NN -> N e. ZZ )

Syntax hints:   -> wi 4   e. wcel 1436   NNcn 8360   ZZcz 8686

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 3934  ax-pow 3986  ax-pr 4012  ax-un 4236  ax-setind 4328  ax-cnex 7383  ax-resscn 7384  ax-1cn 7385  ax-1re 7386  ax-icn 7387  ax-addcl 7388  ax-addrcl 7389  ax-mulcl 7390  ax-addcom 7392  ax-addass 7394  ax-distr 7396  ax-i2m1 7397  ax-0lt1 7398  ax-0id 7400  ax-rnegex 7401  ax-cnre 7403  ax-pre-ltirr 7404  ax-pre-ltwlin 7405  ax-pre-lttrn 7406  ax-pre-ltadd 7408

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 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-int 3674  df-br 3823  df-opab 3877  df-id 4096  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-iota 4948  df-fun 4985  df-fv 4991  df-riota 5571  df-ov 5618  df-oprab 5619  df-mpt2 5620  df-pnf 7471  df-mnf 7472  df-xr 7473  df-ltxr 7474  df-le 7475  df-sub 7602  df-neg 7603  df-inn 8361  df-z 8687

This theorem is referenced by:  elnnz1  8709  znegcl  8717  nnleltp1  8745  nnltp1le  8746  elz2  8754  nnlem1lt  8766  nnltlem1  8767  nnm1ge0  8768  prime  8781  nneo  8785  zeo  8787  btwnz  8801  indstr  9016  eluz2b2  9025  elnn1uz2  9029  qaddcl  9055  qreccl  9062  elfz1end  9404  fznatpl1  9423  fznn  9436  elfz1b  9437  elfzo0  9524  fzo1fzo0n0  9525  elfzo0z  9526  elfzo1  9532  ubmelm1fzo  9568  intfracq  9658  zmodcl  9682  zmodfz  9684  zmodfzo  9685  zmodid2  9690  zmodidfzo  9691  modfzo0difsn  9733  expinnval  9860  mulexpzap  9897  nnesq  9973  expnlbnd  9978  expnlbnd2  9979  facdiv  10046  faclbnd  10049  bc0k  10064  ibcval5  10071  iseqcoll  10147  caucvgrelemcau  10312  resqrexlemlo  10345  resqrexlemcalc3  10348  resqrexlemgt0  10352  absexpzap  10412  climuni  10579  fisum  10670  dvdsval3  10706  nndivdvds  10708  modmulconst  10734  dvdsle  10751  dvdsssfz1  10759  fzm1ndvds  10763  dvdsfac  10767  oexpneg  10783  nnoddm1d2  10816  divalg2  10832  divalgmod  10833  modremain  10835  ndvdsadd  10837  nndvdslegcd  10863  divgcdz  10869  divgcdnn  10872  divgcdnnr  10873  modgcd  10888  gcddiv  10914  gcdmultiple  10915  gcdmultiplez  10916  gcdzeq  10917  gcdeq  10918  rpmulgcd  10921  rplpwr  10922  rppwr  10923  sqgcd  10924  dvdssqlem  10925  dvdssq  10926  eucalginv  10944  lcmgcdlem  10965  lcmgcdnn  10970  lcmass  10973  coprmgcdb  10976  qredeq  10984  qredeu  10985  cncongr1  10991  cncongr2  10992  1idssfct  11003  isprm2lem  11004  isprm3  11006  isprm4  11007  prmind2  11008  divgcdodd  11028  isprm6  11032  sqrt2irr  11047  pw2dvds  11050  sqrt2irraplemnn  11063  divnumden  11080  divdenle  11081  nn0gcdsq  11084  phivalfi  11094  phicl2  11096  phiprmpw  11104  hashgcdlem  11109  hashgcdeq  11110  oddennn  11111  evenennn  11112  unennn  11116