Theorem nnz 9390

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

Syntax hints:   -> wi 4   e. wcel 2175   NNcn 9035   ZZcz 9371

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4479  ax-setind 4584  ax-cnex 8015  ax-resscn 8016  ax-1cn 8017  ax-1re 8018  ax-icn 8019  ax-addcl 8020  ax-addrcl 8021  ax-mulcl 8022  ax-addcom 8024  ax-addass 8026  ax-distr 8028  ax-i2m1 8029  ax-0lt1 8030  ax-0id 8032  ax-rnegex 8033  ax-cnre 8035  ax-pre-ltirr 8036  ax-pre-ltwlin 8037  ax-pre-lttrn 8038  ax-pre-ltadd 8040

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-nel 2471  df-ral 2488  df-rex 2489  df-reu 2490  df-rab 2492  df-v 2773  df-sbc 2998  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-br 4044  df-opab 4105  df-id 4339  df-xp 4680  df-rel 4681  df-cnv 4682  df-co 4683  df-dm 4684  df-iota 5231  df-fun 5272  df-fv 5278  df-riota 5898  df-ov 5946  df-oprab 5947  df-mpo 5948  df-pnf 8108  df-mnf 8109  df-xr 8110  df-ltxr 8111  df-le 8112  df-sub 8244  df-neg 8245  df-inn 9036  df-z 9372

This theorem is referenced by:  elnnz1  9394  znegcl  9402  nnnle0  9420  nnleltp1  9431  nnltp1le  9432  elz2  9443  nnlem1lt  9456  nnltlem1  9457  nnm1ge0  9458  prime  9471  nneo  9475  zeo  9477  btwnz  9491  indstr  9713  eluz2b2  9723  elnn1uz2  9727  qaddcl  9755  qreccl  9762  elpqb  9770  elfz1end  10176  fznatpl1  10197  fznn  10210  elfz1b  10211  elfzo0  10304  fzo1fzo0n0  10305  elfzo0z  10306  elfzo1  10312  ubmelm1fzo  10353  intfracq  10463  zmodcl  10487  zmodfz  10489  zmodfzo  10490  zmodid2  10495  zmodidfzo  10496  modfzo0difsn  10538  mulexpzap  10722  nnesq  10802  expnlbnd  10807  expnlbnd2  10808  nn0ltexp2  10852  facdiv  10881  faclbnd  10884  bc0k  10899  bcval5  10906  seq3coll  10985  ccatval21sw  11059  caucvgrelemcau  11262  resqrexlemlo  11295  resqrexlemcalc3  11298  resqrexlemgt0  11302  absexpzap  11362  climuni  11575  fsum3  11669  arisum  11780  trireciplem  11782  expcnvap0  11784  geo2sum  11796  geo2lim  11798  0.999...  11803  geoihalfsum  11804  cvgratz  11814  zproddc  11861  fprodseq  11865  prod1dc  11868  dvdsval3  12073  nndivdvds  12078  modmulconst  12105  dvdsle  12126  dvdsssfz1  12134  fzm1ndvds  12138  dvdsfac  12142  oexpneg  12159  nnoddm1d2  12192  divalg2  12208  divalgmod  12209  modremain  12211  ndvdsadd  12213  nndvdslegcd  12257  divgcdz  12263  divgcdnn  12267  divgcdnnr  12268  modgcd  12283  gcddiv  12311  gcdmultiple  12312  gcdmultiplez  12313  gcdzeq  12314  gcdeq  12315  rpmulgcd  12318  rplpwr  12319  rppwr  12320  sqgcd  12321  dvdssqlem  12322  dvdssq  12323  eucalginv  12349  lcmgcdlem  12370  lcmgcdnn  12375  lcmass  12378  coprmgcdb  12381  qredeq  12389  qredeu  12390  cncongr1  12396  cncongr2  12397  1idssfct  12408  isprm2lem  12409  isprm3  12411  isprm4  12412  prmind2  12413  prmdc  12423  divgcdodd  12436  isprm6  12440  sqrt2irr  12455  pw2dvds  12459  sqrt2irraplemnn  12472  divnumden  12489  divdenle  12490  nn0gcdsq  12493  phivalfi  12505  phicl2  12507  phiprmpw  12515  hashgcdlem  12531  dvdsfi  12532  hashgcdeq  12533  phisum  12534  nnoddn2prm  12554  pythagtriplem2  12560  pythagtriplem3  12561  pythagtriplem4  12562  pythagtriplem6  12564  pythagtriplem7  12565  pythagtriplem8  12566  pythagtriplem9  12567  pythagtriplem11  12568  pythagtriplem13  12570  pythagtriplem15  12572  pythagtriplem19  12576  pythagtrip  12577  pceu  12589  pccl  12593  pcdiv  12596  pcqcl  12600  pcdvds  12609  pcndvds  12611  pcndvds2  12613  pcelnn  12615  pcz  12626  pcmpt  12637  fldivp1  12642  pcfac  12644  infpnlem1  12653  infpnlem2  12654  prmunb  12656  1arith  12661  oddennn  12734  evenennn  12735  unennn  12739  mulgnn  13433  mulgnngsum  13434  mulgaddcom  13453  mulginvcom  13454  mulgmodid  13468  ghmmulg  13563  mulgass2  13791  znfi  14388  znhash  14389  znidomb  14391  znrrg  14393  rpcxproot  15357  logbgcd1irr  15410  sgmnncl  15431  lgsval  15452  lgsval4a  15470  lgssq2  15489  gausslemma2dlem0c  15499  gausslemma2dlem0e  15501  gausslemma2dlem1a  15506  gausslemma2dlem3  15511  gausslemma2dlem5  15514  lgsquadlem1  15525  lgsquadlem2  15526  lgsquad3  15532  2lgslem1a1  15534  2lgslem3  15549  2lgsoddprm  15561  trilpolemcl  15938