Theorem nnz 9289

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 9287	. 2 |- NN C_ ZZ
2	1	sseli 3165	1 |- ( N e. NN -> N e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2159   NNcn 8936   ZZcz 9270

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 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2161  ax-14 2162  ax-ext 2170  ax-sep 4135  ax-pow 4188  ax-pr 4223  ax-un 4447  ax-setind 4550  ax-cnex 7919  ax-resscn 7920  ax-1cn 7921  ax-1re 7922  ax-icn 7923  ax-addcl 7924  ax-addrcl 7925  ax-mulcl 7926  ax-addcom 7928  ax-addass 7930  ax-distr 7932  ax-i2m1 7933  ax-0lt1 7934  ax-0id 7936  ax-rnegex 7937  ax-cnre 7939  ax-pre-ltirr 7940  ax-pre-ltwlin 7941  ax-pre-lttrn 7942  ax-pre-ltadd 7944

This theorem depends on definitions:  df-bi 117  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2040  df-mo 2041  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-ne 2360  df-nel 2455  df-ral 2472  df-rex 2473  df-reu 2474  df-rab 2476  df-v 2753  df-sbc 2977  df-dif 3145  df-un 3147  df-in 3149  df-ss 3156  df-pw 3591  df-sn 3612  df-pr 3613  df-op 3615  df-uni 3824  df-int 3859  df-br 4018  df-opab 4079  df-id 4307  df-xp 4646  df-rel 4647  df-cnv 4648  df-co 4649  df-dm 4650  df-iota 5192  df-fun 5232  df-fv 5238  df-riota 5846  df-ov 5893  df-oprab 5894  df-mpo 5895  df-pnf 8011  df-mnf 8012  df-xr 8013  df-ltxr 8014  df-le 8015  df-sub 8147  df-neg 8148  df-inn 8937  df-z 9271

This theorem is referenced by:  elnnz1  9293  znegcl  9301  nnleltp1  9329  nnltp1le  9330  elz2  9341  nnlem1lt  9354  nnltlem1  9355  nnm1ge0  9356  prime  9369  nneo  9373  zeo  9375  btwnz  9389  indstr  9610  eluz2b2  9620  elnn1uz2  9624  qaddcl  9652  qreccl  9659  elpqb  9666  elfz1end  10072  fznatpl1  10093  fznn  10106  elfz1b  10107  elfzo0  10199  fzo1fzo0n0  10200  elfzo0z  10201  elfzo1  10207  ubmelm1fzo  10243  intfracq  10337  zmodcl  10361  zmodfz  10363  zmodfzo  10364  zmodid2  10369  zmodidfzo  10370  modfzo0difsn  10412  mulexpzap  10577  nnesq  10657  expnlbnd  10662  expnlbnd2  10663  nn0ltexp2  10706  facdiv  10735  faclbnd  10738  bc0k  10753  bcval5  10760  seq3coll  10839  caucvgrelemcau  11006  resqrexlemlo  11039  resqrexlemcalc3  11042  resqrexlemgt0  11046  absexpzap  11106  climuni  11318  fsum3  11412  arisum  11523  trireciplem  11525  expcnvap0  11527  geo2sum  11539  geo2lim  11541  0.999...  11546  geoihalfsum  11547  cvgratz  11557  zproddc  11604  fprodseq  11608  prod1dc  11611  dvdsval3  11815  nndivdvds  11820  modmulconst  11847  dvdsle  11867  dvdsssfz1  11875  fzm1ndvds  11879  dvdsfac  11883  oexpneg  11899  nnoddm1d2  11932  divalg2  11948  divalgmod  11949  modremain  11951  ndvdsadd  11953  nndvdslegcd  11983  divgcdz  11989  divgcdnn  11993  divgcdnnr  11994  modgcd  12009  gcddiv  12037  gcdmultiple  12038  gcdmultiplez  12039  gcdzeq  12040  gcdeq  12041  rpmulgcd  12044  rplpwr  12045  rppwr  12046  sqgcd  12047  dvdssqlem  12048  dvdssq  12049  eucalginv  12073  lcmgcdlem  12094  lcmgcdnn  12099  lcmass  12102  coprmgcdb  12105  qredeq  12113  qredeu  12114  cncongr1  12120  cncongr2  12121  1idssfct  12132  isprm2lem  12133  isprm3  12135  isprm4  12136  prmind2  12137  prmdc  12147  divgcdodd  12160  isprm6  12164  sqrt2irr  12179  pw2dvds  12183  sqrt2irraplemnn  12196  divnumden  12213  divdenle  12214  nn0gcdsq  12217  phivalfi  12229  phicl2  12231  phiprmpw  12239  hashgcdlem  12255  hashgcdeq  12256  phisum  12257  nnoddn2prm  12277  pythagtriplem2  12283  pythagtriplem3  12284  pythagtriplem4  12285  pythagtriplem6  12287  pythagtriplem7  12288  pythagtriplem8  12289  pythagtriplem9  12290  pythagtriplem11  12291  pythagtriplem13  12293  pythagtriplem15  12295  pythagtriplem19  12299  pythagtrip  12300  pceu  12312  pccl  12316  pcdiv  12319  pcqcl  12323  pcdvds  12331  pcndvds  12333  pcndvds2  12335  pcelnn  12337  pcz  12348  pcmpt  12358  fldivp1  12363  pcfac  12365  infpnlem1  12374  infpnlem2  12375  prmunb  12377  1arith  12382  oddennn  12410  evenennn  12411  unennn  12415  mulgnn  13033  mulgaddcom  13051  mulginvcom  13052  mulgmodid  13066  ghmmulg  13155  mulgass2  13370  rpcxproot  14717  logbgcd1irr  14768  lgsval  14788  lgsval4a  14806  lgssq2  14825  trilpolemcl  15169