ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nnz GIF version

Theorem nnz 9093
Description: A positive integer is an integer. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nnz (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Proof of Theorem nnz
StepHypRef Expression
1 nnssz 9091 . 2 ℕ ⊆ ℤ
21sseli 3094 1 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1481  cn 8740  cz 9074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4050  ax-pow 4102  ax-pr 4135  ax-un 4359  ax-setind 4456  ax-cnex 7731  ax-resscn 7732  ax-1cn 7733  ax-1re 7734  ax-icn 7735  ax-addcl 7736  ax-addrcl 7737  ax-mulcl 7738  ax-addcom 7740  ax-addass 7742  ax-distr 7744  ax-i2m1 7745  ax-0lt1 7746  ax-0id 7748  ax-rnegex 7749  ax-cnre 7751  ax-pre-ltirr 7752  ax-pre-ltwlin 7753  ax-pre-lttrn 7754  ax-pre-ltadd 7756
This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2689  df-sbc 2911  df-dif 3074  df-un 3076  df-in 3078  df-ss 3085  df-pw 3513  df-sn 3534  df-pr 3535  df-op 3537  df-uni 3741  df-int 3776  df-br 3934  df-opab 3994  df-id 4219  df-xp 4549  df-rel 4550  df-cnv 4551  df-co 4552  df-dm 4553  df-iota 5092  df-fun 5129  df-fv 5135  df-riota 5734  df-ov 5781  df-oprab 5782  df-mpo 5783  df-pnf 7822  df-mnf 7823  df-xr 7824  df-ltxr 7825  df-le 7826  df-sub 7955  df-neg 7956  df-inn 8741  df-z 9075
This theorem is referenced by:  elnnz1  9097  znegcl  9105  nnleltp1  9133  nnltp1le  9134  elz2  9142  nnlem1lt  9155  nnltlem1  9156  nnm1ge0  9157  prime  9170  nneo  9174  zeo  9176  btwnz  9190  indstr  9411  eluz2b2  9420  elnn1uz2  9424  qaddcl  9450  qreccl  9457  elpqb  9464  elfz1end  9862  fznatpl1  9883  fznn  9896  elfz1b  9897  elfzo0  9986  fzo1fzo0n0  9987  elfzo0z  9988  elfzo1  9994  ubmelm1fzo  10030  intfracq  10120  zmodcl  10144  zmodfz  10146  zmodfzo  10147  zmodid2  10152  zmodidfzo  10153  modfzo0difsn  10195  mulexpzap  10360  nnesq  10438  expnlbnd  10443  expnlbnd2  10444  facdiv  10512  faclbnd  10515  bc0k  10530  bcval5  10537  seq3coll  10613  caucvgrelemcau  10780  resqrexlemlo  10813  resqrexlemcalc3  10816  resqrexlemgt0  10820  absexpzap  10880  climuni  11090  fsum3  11184  arisum  11295  trireciplem  11297  expcnvap0  11299  geo2sum  11311  geo2lim  11313  0.999...  11318  geoihalfsum  11319  cvgratz  11329  dvdsval3  11524  nndivdvds  11526  modmulconst  11552  dvdsle  11569  dvdsssfz1  11577  fzm1ndvds  11581  dvdsfac  11585  oexpneg  11601  nnoddm1d2  11634  divalg2  11650  divalgmod  11651  modremain  11653  ndvdsadd  11655  nndvdslegcd  11681  divgcdz  11687  divgcdnn  11690  divgcdnnr  11691  modgcd  11706  gcddiv  11734  gcdmultiple  11735  gcdmultiplez  11736  gcdzeq  11737  gcdeq  11738  rpmulgcd  11741  rplpwr  11742  rppwr  11743  sqgcd  11744  dvdssqlem  11745  dvdssq  11746  eucalginv  11764  lcmgcdlem  11785  lcmgcdnn  11790  lcmass  11793  coprmgcdb  11796  qredeq  11804  qredeu  11805  cncongr1  11811  cncongr2  11812  1idssfct  11823  isprm2lem  11824  isprm3  11826  isprm4  11827  prmind2  11828  divgcdodd  11848  isprm6  11852  sqrt2irr  11867  pw2dvds  11871  sqrt2irraplemnn  11884  divnumden  11901  divdenle  11902  nn0gcdsq  11905  phivalfi  11915  phicl2  11917  phiprmpw  11925  hashgcdlem  11930  hashgcdeq  11931  oddennn  11932  evenennn  11933  unennn  11937  rpcxproot  13033  logbgcd1irr  13083  trilpolemcl  13388
  Copyright terms: Public domain W3C validator