Theorem nnz 9665

Description: A positive integer is an integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nnz	⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Proof of Theorem nnz

Step	Hyp	Ref	Expression
1		nnssz 9663	. 2 ⊢ ℕ ⊆ ℤ
2	1	sseli 3244	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℕcn 9305  ℤcz 9646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-cnex 8270  ax-resscn 8271  ax-1cn 8272  ax-1re 8273  ax-icn 8274  ax-addcl 8275  ax-addrcl 8276  ax-mulcl 8277  ax-addcom 8279  ax-addass 8281  ax-distr 8283  ax-i2m1 8284  ax-0lt1 8285  ax-0id 8287  ax-rnegex 8288  ax-cnre 8290  ax-pre-ltirr 8291  ax-pre-ltwlin 8292  ax-pre-lttrn 8293  ax-pre-ltadd 8295

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4131  df-opab 4193  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-iota 5337  df-fun 5379  df-fv 5385  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-pnf 8362  df-mnf 8363  df-xr 8364  df-ltxr 8365  df-le 8366  df-sub 8499  df-neg 8500  df-inn 9306  df-z 9647

This theorem is used by:  elnnz1  9669  znegcl  9677  nnnle0  9695  nnleltp1  9706  nnltp1le  9707  elz2  9718  nnlem1lt  9732  nnltlem1  9733  nnm1ge0  9734  prime  9747  nneo  9751  zeo  9753  btwnz  9767  indstr  9995  eluz2b2  10005  elnn1uz2  10009  qaddcl  10037  qreccl  10044  elpqb  10052  elfz1end  10463  fznatpl1  10485  fznn  10498  elfz1b  10499  elfzo0  10595  fzo1fzo0n0  10597  elfzo0z  10598  elfzo1  10605  ubmelm1fzo  10646  intfracq  10759  zmodcl  10783  zmodfz  10785  zmodfzo  10786  zmodid2  10791  zmodidfzo  10792  modfzo0difsn  10834  mulexpzap  11018  nnesq  11099  expnlbnd  11104  expnlbnd2  11105  nn0ltexp2  11149  facdiv  11178  faclbnd  11181  bc0k  11196  bcval5  11203  bcm1n  11209  seq3coll  11296  ccatval21sw  11375  caucvgrelemcau  11748  resqrexlemlo  11781  resqrexlemcalc3  11784  resqrexlemgt0  11788  absexpzap  11848  climuni  12061  fsum3  12156  arisum  12267  trireciplem  12269  expcnvap0  12271  geo2sum  12283  geo2lim  12285  0.999...  12290  geoihalfsum  12291  cvgratz  12301  zproddc  12348  fprodseq  12352  prod1dc  12355  dvdsval3  12560  nndivdvds  12565  modmulconst  12592  dvdsle  12613  dvdsssfz1  12621  fzm1ndvds  12625  dvdsfac  12629  oexpneg  12646  nnoddm1d2  12679  divalg2  12695  divalgmod  12696  modremain  12698  ndvdsadd  12700  nndvdslegcd  12744  divgcdz  12750  divgcdnn  12754  divgcdnnr  12755  modgcd  12770  gcddiv  12798  gcdmultiple  12799  gcdmultiplez  12800  gcdzeq  12801  gcdeq  12802  rpmulgcd  12805  rplpwr  12806  rppwr  12807  sqgcd  12808  dvdssqlem  12809  dvdssq  12810  eucalginv  12836  lcmgcdlem  12857  lcmgcdnn  12862  lcmass  12865  coprmgcdb  12868  qredeq  12876  qredeu  12877  cncongr1  12883  cncongr2  12884  1idssfct  12895  isprm2lem  12896  isprm3  12898  isprm4  12899  prmind2  12900  prmdc  12910  divgcdodd  12923  isprm6  12927  sqrt2irr  12942  pw2dvds  12946  sqrt2irraplemnn  12959  divnumden  12976  divdenle  12977  nn0gcdsq  12980  phivalfi  12992  phicl2  12994  phiprmpw  13002  hashgcdlem  13018  dvdsfi  13019  hashgcdeq  13020  phisum  13021  nnoddn2prm  13041  pythagtriplem2  13047  pythagtriplem3  13048  pythagtriplem4  13049  pythagtriplem6  13051  pythagtriplem7  13052  pythagtriplem8  13053  pythagtriplem9  13054  pythagtriplem11  13055  pythagtriplem13  13057  pythagtriplem15  13059  pythagtriplem19  13063  pythagtrip  13064  pceu  13076  pccl  13080  pcdiv  13083  pcqcl  13087  pcdvds  13096  pcndvds  13098  pcndvds2  13100  pcelnn  13102  pcz  13113  pcmpt  13124  fldivp1  13129  pcfac  13131  infpnlem1  13140  infpnlem2  13141  prmunb  13143  1arith  13148  ballotfilemiex  13246  oddennn  13285  evenennn  13286  unennn  13290  mulgnn  13931  mulgnngzsum  13932  mulgaddcom  13951  mulginvcom  13952  mulgmodid  13966  ghmmulg  14061  mulgass2  14365  znfi  14992  znhash  14993  znidomb  14995  znrrg  14997  rpcxproot  16022  logbgcd1irr  16075  birthdaylem1g  16093  birthdaylem2  16094  birthdaylem3  16095  sgmnncl  16108  pcbcctr  16123  bclbnd  16127  lgsval  16135  lgsval4a  16153  lgssq2  16172  gausslemma2dlem0c  16182  gausslemma2dlem0e  16184  gausslemma2dlem1a  16189  gausslemma2dlem3  16194  gausslemma2dlem5  16197  lgsquadlem1  16208  lgsquadlem2  16209  lgsquad3  16215  2lgslem1a1  16217  2lgslem3  16232  2lgsoddprm  16244  trilpolemcl  17098