Theorem nnz 9498

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

Syntax hints:   -> wi 4   e. wcel 2202   NNcn 9143   ZZcz 9479

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-addcom 8132  ax-addass 8134  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-0id 8140  ax-rnegex 8141  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-ltadd 8148

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-inn 9144  df-z 9480

This theorem is referenced by:  elnnz1  9502  znegcl  9510  nnnle0  9528  nnleltp1  9539  nnltp1le  9540  elz2  9551  nnlem1lt  9564  nnltlem1  9565  nnm1ge0  9566  prime  9579  nneo  9583  zeo  9585  btwnz  9599  indstr  9827  eluz2b2  9837  elnn1uz2  9841  qaddcl  9869  qreccl  9876  elpqb  9884  elfz1end  10290  fznatpl1  10311  fznn  10324  elfz1b  10325  elfzo0  10421  fzo1fzo0n0  10423  elfzo0z  10424  elfzo1  10431  ubmelm1fzo  10472  intfracq  10583  zmodcl  10607  zmodfz  10609  zmodfzo  10610  zmodid2  10615  zmodidfzo  10616  modfzo0difsn  10658  mulexpzap  10842  nnesq  10922  expnlbnd  10927  expnlbnd2  10928  nn0ltexp2  10972  facdiv  11001  faclbnd  11004  bc0k  11019  bcval5  11026  seq3coll  11107  ccatval21sw  11186  caucvgrelemcau  11558  resqrexlemlo  11591  resqrexlemcalc3  11594  resqrexlemgt0  11598  absexpzap  11658  climuni  11871  fsum3  11966  arisum  12077  trireciplem  12079  expcnvap0  12081  geo2sum  12093  geo2lim  12095  0.999...  12100  geoihalfsum  12101  cvgratz  12111  zproddc  12158  fprodseq  12162  prod1dc  12165  dvdsval3  12370  nndivdvds  12375  modmulconst  12402  dvdsle  12423  dvdsssfz1  12431  fzm1ndvds  12435  dvdsfac  12439  oexpneg  12456  nnoddm1d2  12489  divalg2  12505  divalgmod  12506  modremain  12508  ndvdsadd  12510  nndvdslegcd  12554  divgcdz  12560  divgcdnn  12564  divgcdnnr  12565  modgcd  12580  gcddiv  12608  gcdmultiple  12609  gcdmultiplez  12610  gcdzeq  12611  gcdeq  12612  rpmulgcd  12615  rplpwr  12616  rppwr  12617  sqgcd  12618  dvdssqlem  12619  dvdssq  12620  eucalginv  12646  lcmgcdlem  12667  lcmgcdnn  12672  lcmass  12675  coprmgcdb  12678  qredeq  12686  qredeu  12687  cncongr1  12693  cncongr2  12694  1idssfct  12705  isprm2lem  12706  isprm3  12708  isprm4  12709  prmind2  12710  prmdc  12720  divgcdodd  12733  isprm6  12737  sqrt2irr  12752  pw2dvds  12756  sqrt2irraplemnn  12769  divnumden  12786  divdenle  12787  nn0gcdsq  12790  phivalfi  12802  phicl2  12804  phiprmpw  12812  hashgcdlem  12828  dvdsfi  12829  hashgcdeq  12830  phisum  12831  nnoddn2prm  12851  pythagtriplem2  12857  pythagtriplem3  12858  pythagtriplem4  12859  pythagtriplem6  12861  pythagtriplem7  12862  pythagtriplem8  12863  pythagtriplem9  12864  pythagtriplem11  12865  pythagtriplem13  12867  pythagtriplem15  12869  pythagtriplem19  12873  pythagtrip  12874  pceu  12886  pccl  12890  pcdiv  12893  pcqcl  12897  pcdvds  12906  pcndvds  12908  pcndvds2  12910  pcelnn  12912  pcz  12923  pcmpt  12934  fldivp1  12939  pcfac  12941  infpnlem1  12950  infpnlem2  12951  prmunb  12953  1arith  12958  oddennn  13031  evenennn  13032  unennn  13036  mulgnn  13731  mulgnngsum  13732  mulgaddcom  13751  mulginvcom  13752  mulgmodid  13766  ghmmulg  13861  mulgass2  14090  znfi  14688  znhash  14689  znidomb  14691  znrrg  14693  rpcxproot  15657  logbgcd1irr  15710  sgmnncl  15731  lgsval  15752  lgsval4a  15770  lgssq2  15789  gausslemma2dlem0c  15799  gausslemma2dlem0e  15801  gausslemma2dlem1a  15806  gausslemma2dlem3  15811  gausslemma2dlem5  15814  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad3  15832  2lgslem1a1  15834  2lgslem3  15849  2lgsoddprm  15861  trilpolemcl  16692