Theorem nnz 9542

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

Syntax hints:   -> wi 4   e. wcel 2202   NNcn 9185   ZZcz 9523

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-un 4536  ax-setind 4641  ax-cnex 8166  ax-resscn 8167  ax-1cn 8168  ax-1re 8169  ax-icn 8170  ax-addcl 8171  ax-addrcl 8172  ax-mulcl 8173  ax-addcom 8175  ax-addass 8177  ax-distr 8179  ax-i2m1 8180  ax-0lt1 8181  ax-0id 8183  ax-rnegex 8184  ax-cnre 8186  ax-pre-ltirr 8187  ax-pre-ltwlin 8188  ax-pre-lttrn 8189  ax-pre-ltadd 8191

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-nel 2499  df-ral 2516  df-rex 2517  df-reu 2518  df-rab 2520  df-v 2805  df-sbc 3033  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-int 3934  df-br 4094  df-opab 4156  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-iota 5293  df-fun 5335  df-fv 5341  df-riota 5981  df-ov 6031  df-oprab 6032  df-mpo 6033  df-pnf 8258  df-mnf 8259  df-xr 8260  df-ltxr 8261  df-le 8262  df-sub 8394  df-neg 8395  df-inn 9186  df-z 9524

This theorem is referenced by:  elnnz1  9546  znegcl  9554  nnnle0  9572  nnleltp1  9583  nnltp1le  9584  elz2  9595  nnlem1lt  9608  nnltlem1  9609  nnm1ge0  9610  prime  9623  nneo  9627  zeo  9629  btwnz  9643  indstr  9871  eluz2b2  9881  elnn1uz2  9885  qaddcl  9913  qreccl  9920  elpqb  9928  elfz1end  10335  fznatpl1  10356  fznn  10369  elfz1b  10370  elfzo0  10466  fzo1fzo0n0  10468  elfzo0z  10469  elfzo1  10476  ubmelm1fzo  10517  intfracq  10628  zmodcl  10652  zmodfz  10654  zmodfzo  10655  zmodid2  10660  zmodidfzo  10661  modfzo0difsn  10703  mulexpzap  10887  nnesq  10967  expnlbnd  10972  expnlbnd2  10973  nn0ltexp2  11017  facdiv  11046  faclbnd  11049  bc0k  11064  bcval5  11071  seq3coll  11152  ccatval21sw  11231  caucvgrelemcau  11603  resqrexlemlo  11636  resqrexlemcalc3  11639  resqrexlemgt0  11643  absexpzap  11703  climuni  11916  fsum3  12011  arisum  12122  trireciplem  12124  expcnvap0  12126  geo2sum  12138  geo2lim  12140  0.999...  12145  geoihalfsum  12146  cvgratz  12156  zproddc  12203  fprodseq  12207  prod1dc  12210  dvdsval3  12415  nndivdvds  12420  modmulconst  12447  dvdsle  12468  dvdsssfz1  12476  fzm1ndvds  12480  dvdsfac  12484  oexpneg  12501  nnoddm1d2  12534  divalg2  12550  divalgmod  12551  modremain  12553  ndvdsadd  12555  nndvdslegcd  12599  divgcdz  12605  divgcdnn  12609  divgcdnnr  12610  modgcd  12625  gcddiv  12653  gcdmultiple  12654  gcdmultiplez  12655  gcdzeq  12656  gcdeq  12657  rpmulgcd  12660  rplpwr  12661  rppwr  12662  sqgcd  12663  dvdssqlem  12664  dvdssq  12665  eucalginv  12691  lcmgcdlem  12712  lcmgcdnn  12717  lcmass  12720  coprmgcdb  12723  qredeq  12731  qredeu  12732  cncongr1  12738  cncongr2  12739  1idssfct  12750  isprm2lem  12751  isprm3  12753  isprm4  12754  prmind2  12755  prmdc  12765  divgcdodd  12778  isprm6  12782  sqrt2irr  12797  pw2dvds  12801  sqrt2irraplemnn  12814  divnumden  12831  divdenle  12832  nn0gcdsq  12835  phivalfi  12847  phicl2  12849  phiprmpw  12857  hashgcdlem  12873  dvdsfi  12874  hashgcdeq  12875  phisum  12876  nnoddn2prm  12896  pythagtriplem2  12902  pythagtriplem3  12903  pythagtriplem4  12904  pythagtriplem6  12906  pythagtriplem7  12907  pythagtriplem8  12908  pythagtriplem9  12909  pythagtriplem11  12910  pythagtriplem13  12912  pythagtriplem15  12914  pythagtriplem19  12918  pythagtrip  12919  pceu  12931  pccl  12935  pcdiv  12938  pcqcl  12942  pcdvds  12951  pcndvds  12953  pcndvds2  12955  pcelnn  12957  pcz  12968  pcmpt  12979  fldivp1  12984  pcfac  12986  infpnlem1  12995  infpnlem2  12996  prmunb  12998  1arith  13003  oddennn  13076  evenennn  13077  unennn  13081  mulgnn  13776  mulgnngsum  13777  mulgaddcom  13796  mulginvcom  13797  mulgmodid  13811  ghmmulg  13906  mulgass2  14135  znfi  14734  znhash  14735  znidomb  14737  znrrg  14739  rpcxproot  15708  logbgcd1irr  15761  sgmnncl  15785  lgsval  15806  lgsval4a  15824  lgssq2  15843  gausslemma2dlem0c  15853  gausslemma2dlem0e  15855  gausslemma2dlem1a  15860  gausslemma2dlem3  15865  gausslemma2dlem5  15868  lgsquadlem1  15879  lgsquadlem2  15880  lgsquad3  15886  2lgslem1a1  15888  2lgslem3  15903  2lgsoddprm  15915  trilpolemcl  16752