Theorem nnz 9461

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

Syntax hints:   -> wi 4   e. wcel 2200   NNcn 9106   ZZcz 9442

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292  ax-un 4523  ax-setind 4628  ax-cnex 8086  ax-resscn 8087  ax-1cn 8088  ax-1re 8089  ax-icn 8090  ax-addcl 8091  ax-addrcl 8092  ax-mulcl 8093  ax-addcom 8095  ax-addass 8097  ax-distr 8099  ax-i2m1 8100  ax-0lt1 8101  ax-0id 8103  ax-rnegex 8104  ax-cnre 8106  ax-pre-ltirr 8107  ax-pre-ltwlin 8108  ax-pre-lttrn 8109  ax-pre-ltadd 8111

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-int 3923  df-br 4083  df-opab 4145  df-id 4383  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-iota 5277  df-fun 5319  df-fv 5325  df-riota 5953  df-ov 6003  df-oprab 6004  df-mpo 6005  df-pnf 8179  df-mnf 8180  df-xr 8181  df-ltxr 8182  df-le 8183  df-sub 8315  df-neg 8316  df-inn 9107  df-z 9443

This theorem is referenced by:  elnnz1  9465  znegcl  9473  nnnle0  9491  nnleltp1  9502  nnltp1le  9503  elz2  9514  nnlem1lt  9527  nnltlem1  9528  nnm1ge0  9529  prime  9542  nneo  9546  zeo  9548  btwnz  9562  indstr  9784  eluz2b2  9794  elnn1uz2  9798  qaddcl  9826  qreccl  9833  elpqb  9841  elfz1end  10247  fznatpl1  10268  fznn  10281  elfz1b  10282  elfzo0  10378  fzo1fzo0n0  10379  elfzo0z  10380  elfzo1  10386  ubmelm1fzo  10427  intfracq  10537  zmodcl  10561  zmodfz  10563  zmodfzo  10564  zmodid2  10569  zmodidfzo  10570  modfzo0difsn  10612  mulexpzap  10796  nnesq  10876  expnlbnd  10881  expnlbnd2  10882  nn0ltexp2  10926  facdiv  10955  faclbnd  10958  bc0k  10973  bcval5  10980  seq3coll  11059  ccatval21sw  11135  caucvgrelemcau  11486  resqrexlemlo  11519  resqrexlemcalc3  11522  resqrexlemgt0  11526  absexpzap  11586  climuni  11799  fsum3  11893  arisum  12004  trireciplem  12006  expcnvap0  12008  geo2sum  12020  geo2lim  12022  0.999...  12027  geoihalfsum  12028  cvgratz  12038  zproddc  12085  fprodseq  12089  prod1dc  12092  dvdsval3  12297  nndivdvds  12302  modmulconst  12329  dvdsle  12350  dvdsssfz1  12358  fzm1ndvds  12362  dvdsfac  12366  oexpneg  12383  nnoddm1d2  12416  divalg2  12432  divalgmod  12433  modremain  12435  ndvdsadd  12437  nndvdslegcd  12481  divgcdz  12487  divgcdnn  12491  divgcdnnr  12492  modgcd  12507  gcddiv  12535  gcdmultiple  12536  gcdmultiplez  12537  gcdzeq  12538  gcdeq  12539  rpmulgcd  12542  rplpwr  12543  rppwr  12544  sqgcd  12545  dvdssqlem  12546  dvdssq  12547  eucalginv  12573  lcmgcdlem  12594  lcmgcdnn  12599  lcmass  12602  coprmgcdb  12605  qredeq  12613  qredeu  12614  cncongr1  12620  cncongr2  12621  1idssfct  12632  isprm2lem  12633  isprm3  12635  isprm4  12636  prmind2  12637  prmdc  12647  divgcdodd  12660  isprm6  12664  sqrt2irr  12679  pw2dvds  12683  sqrt2irraplemnn  12696  divnumden  12713  divdenle  12714  nn0gcdsq  12717  phivalfi  12729  phicl2  12731  phiprmpw  12739  hashgcdlem  12755  dvdsfi  12756  hashgcdeq  12757  phisum  12758  nnoddn2prm  12778  pythagtriplem2  12784  pythagtriplem3  12785  pythagtriplem4  12786  pythagtriplem6  12788  pythagtriplem7  12789  pythagtriplem8  12790  pythagtriplem9  12791  pythagtriplem11  12792  pythagtriplem13  12794  pythagtriplem15  12796  pythagtriplem19  12800  pythagtrip  12801  pceu  12813  pccl  12817  pcdiv  12820  pcqcl  12824  pcdvds  12833  pcndvds  12835  pcndvds2  12837  pcelnn  12839  pcz  12850  pcmpt  12861  fldivp1  12866  pcfac  12868  infpnlem1  12877  infpnlem2  12878  prmunb  12880  1arith  12885  oddennn  12958  evenennn  12959  unennn  12963  mulgnn  13658  mulgnngsum  13659  mulgaddcom  13678  mulginvcom  13679  mulgmodid  13693  ghmmulg  13788  mulgass2  14016  znfi  14613  znhash  14614  znidomb  14616  znrrg  14618  rpcxproot  15582  logbgcd1irr  15635  sgmnncl  15656  lgsval  15677  lgsval4a  15695  lgssq2  15714  gausslemma2dlem0c  15724  gausslemma2dlem0e  15726  gausslemma2dlem1a  15731  gausslemma2dlem3  15736  gausslemma2dlem5  15739  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad3  15757  2lgslem1a1  15759  2lgslem3  15774  2lgsoddprm  15786  trilpolemcl  16364