MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnz Structured version   Visualization version   GIF version

Theorem nnz 12527
Description: A positive integer is an integer. (Contributed by NM, 9-May-2004.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 29-Nov-2022.)
Assertion
Ref Expression
nnz (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Proof of Theorem nnz
StepHypRef Expression
1 nnre 12167 . 2 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2 3mix2 1332 . 2 (𝑁 ∈ ℕ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
3 elz 12508 . 2 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
41, 2, 3sylanbrc 584 1 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1087   = wceq 1542  wcel 2107  cr 11057  0cc0 11058  -cneg 11393  cn 12160  cz 12506
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-i2m1 11126  ax-1ne0 11127  ax-rrecex 11130  ax-cnre 11131
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-neg 11395  df-nn 12161  df-z 12507
This theorem is referenced by:  nnssz  12528  elnnz1  12536  znegcl  12545  nnleltp1  12565  nnltp1le  12566  nnlem1lt  12576  nnltlem1  12577  nnm1ge0  12578  prime  12591  nneo  12594  zeo  12596  btwnz  12613  eluz2b2  12853  qaddcl  12897  qreccl  12901  elpqb  12908  elfz1end  13478  fznatpl1  13502  fznn  13516  elfz1b  13517  elfzo0  13620  elfzo0z  13621  elfzo1  13629  fzo1fzo0n0  13630  elfzom1p1elfzo  13659  ubmelm1fzo  13675  quoremz  13767  intfracq  13771  fznnfl  13774  zmodcl  13803  zmodfz  13805  zmodfzo  13806  zmodid2  13811  zmodidfzo  13812  modfzo0difsn  13855  expnnval  13977  mulexpz  14015  nnesq  14137  expnlbnd  14143  expnlbnd2  14144  digit2  14146  faclbnd  14197  bc0k  14218  bcval5  14225  fz1isolem  14367  seqcoll  14370  ccatval21sw  14480  lswccatn0lsw  14486  cshwidxmod  14698  cshwidxn  14704  absexpz  15197  climuni  15441  isercoll  15559  climcnds  15743  arisum  15752  trireciplem  15754  expcnv  15756  pwdif  15760  geo2sum  15765  geo2lim  15767  0.999...  15773  geoihalfsum  15774  rpnnen2lem6  16108  rpnnen2lem9  16111  rpnnen2lem10  16112  dvdsval3  16147  nndivdvds  16152  modmulconst  16177  dvdsle  16199  dvdsssfz1  16207  fzm1ndvds  16211  dvdsfac  16215  mulmoddvds  16219  oexpneg  16234  nnoddm1d2  16275  pwp1fsum  16280  divalg2  16294  divalgmod  16295  modremain  16297  ndvdsadd  16299  nndvdslegcd  16392  divgcdz  16398  divgcdnn  16402  divgcdnnr  16403  modgcd  16420  gcdmultiple  16424  gcddiv  16439  gcdzeq  16440  gcdeq  16441  rpmulgcd  16444  rplpwr  16445  rprpwr  16446  sqgcd  16448  dvdssqlem  16449  dvdssq  16450  eucalginv  16467  lcmgcdlem  16489  lcmgcdnn  16494  lcmass  16497  lcmftp  16519  lcmfunsnlem2lem1  16521  coprmgcdb  16532  qredeq  16540  qredeu  16541  coprmprod  16544  coprmproddvdslem  16545  coprmproddvds  16546  cncongr1  16550  cncongr2  16551  1idssfct  16563  isprm2lem  16564  isprm3  16566  prmind2  16568  ge2nprmge4  16584  divgcdodd  16593  isprm6  16597  ncoprmlnprm  16610  divnumden  16630  divdenle  16631  nn0gcdsq  16634  phicl2  16647  phiprmpw  16655  eulerthlem2  16661  hashgcdlem  16667  hashgcdeq  16668  phisum  16669  nnoddn2prm  16690  pythagtriplem3  16697  pythagtriplem4  16698  pythagtriplem6  16700  pythagtriplem7  16701  pythagtriplem8  16702  pythagtriplem9  16703  pythagtriplem11  16704  pythagtriplem13  16706  pythagtriplem15  16708  pythagtriplem19  16712  pythagtrip  16713  iserodd  16714  pclem  16717  pccl  16728  pcdiv  16731  pcqcl  16735  pcdvds  16743  pcndvds  16745  pcndvds2  16747  pcelnn  16749  pcz  16760  pcmpt  16771  fldivp1  16776  pcfac  16778  infpnlem1  16789  prmunb  16793  prmreclem1  16795  1arith  16806  ram0  16901  prmdvdsprmo  16921  prmgaplem4  16933  prmgaplem6  16935  prmgaplem7  16936  cshwshashlem2  16976  setsstruct2  17053  mulgnn  18887  mulgaddcom  18907  mulginvcom  18908  mulgmodid  18922  ghmmulg  19027  dfod2  19353  gexdvds  19373  gexnnod  19377  gexex  19638  mulgass2  20032  qsssubdrg  20872  prmirredlem  20909  znidomb  20984  znrrg  20988  chfacfisf  22219  chfacfisfcpmat  22220  chfacfscmul0  22223  chfacfpmmul0  22227  cayhamlem1  22231  cpmadugsumlemF  22241  lmmo  22747  1stckgenlem  22920  imasdsf1olem  23742  clmmulg  24480  cmetcaulem  24668  ovolunlem1a  24876  ovolicc2lem4  24900  mbfi1fseqlem6  25101  dvexp3  25358  dgreq0  25642  elqaalem2  25696  aaliou3lem1  25718  aaliou3lem2  25719  aaliou3lem3  25720  aaliou3lem9  25726  pserdvlem2  25803  logtayl2  26033  root1eq1  26124  root1cj  26125  logbgcd1irr  26160  atantayl2  26304  birthdaylem2  26318  birthdaylem3  26319  emcllem5  26365  basellem2  26447  basellem3  26448  basellem5  26450  issqf  26501  sgmnncl  26512  prmorcht  26543  mumullem1  26544  mumullem2  26545  sqff1o  26547  dvdsflsumcom  26553  muinv  26558  vmalelog  26569  chtublem  26575  vmasum  26580  logfac2  26581  logfaclbnd  26586  bclbnd  26644  bposlem5  26652  lgsval4a  26683  lgssq2  26702  lgsdchr  26719  gausslemma2dlem0c  26722  gausslemma2dlem0e  26724  gausslemma2dlem1a  26729  gausslemma2dlem5  26735  lgsquadlem1  26744  lgsquadlem2  26745  lgsquad3  26751  2lgslem1a1  26753  2lgslem3  26768  2lgsoddprm  26780  2sqnn  26803  2sqreunnltlem  26814  rplogsumlem1  26848  rplogsumlem2  26849  dchrisumlem2  26854  dchrmusumlema  26857  dchrmusum2  26858  dchrvmasumiflem1  26865  dchrvmaeq0  26868  dchrisum0flblem2  26873  dchrisum0re  26877  dchrisum0lema  26878  dchrisum0lem1b  26879  dchrisum0lem2a  26881  logdivbnd  26920  pntrsumbnd2  26931  ostth2lem1  26982  ostth2lem3  26999  ostth3  27002  axlowdimlem13  27945  crctcshwlkn0lem4  28800  crctcshwlkn0lem5  28801  crctcshwlkn0lem7  28803  wlkiswwlksupgr2  28864  clwwisshclwwslem  29000  clwwlkinwwlk  29026  clwwlkel  29032  clwwlkf  29033  wwlksubclwwlk  29044  clwwlkvbij  29099  eucrctshift  29229  eucrct2eupth  29231  numclwlk2lem2f  29363  bcm1n  31740  pnfinf  32061  1fldgenq  32129  isarchiofld  32152  rearchi  32178  submat1n  32426  lmatfvlem  32436  esumcvg  32725  oddpwdc  32994  fibp1  33041  chtvalz  33282  nnltp1ne  33741  erdszelem7  33831  climuzcnv  34299  elfzm12  34303  bcprod  34350  nn0prpwlem  34823  knoppndvlem1  35004  knoppndvlem2  35005  knoppndvlem7  35010  knoppndvlem18  35021  poimirlem13  36120  poimirlem14  36121  mblfinlem2  36145  fzmul  36229  incsequz  36236  geomcau  36247  heibor1lem  36297  bfplem2  36311  lcmfunnnd  40498  metakunt16  40621  metakunt26  40631  nn0rppwr  40848  nn0expgcd  40850  dvdsexpnn  40855  dvdsexpnn0  40856  zrtdvds  40861  fzsplit1nn0  41106  irrapxlem1  41174  pellexlem5  41185  rmynn  41309  jm2.24nn  41312  jm2.17c  41315  congrep  41326  congabseq  41327  acongrep  41333  acongeq  41336  jm2.18  41341  jm2.23  41349  jm2.20nn  41350  jm2.26lem3  41354  jm2.26  41355  jm2.15nn0  41356  jm2.16nn0  41357  jm2.27dlem2  41363  rmydioph  41367  jm3.1  41373  expdiophlem1  41374  expdioph  41376  idomodle  41552  proot1ex  41557  nznngen  42670  sumnnodd  43945  stoweidlem7  44322  stoweidlem17  44332  wallispilem4  44383  stirlinglem2  44390  stirlinglem3  44391  stirlinglem4  44392  stirlinglem12  44400  stirlinglem13  44401  stirlinglem14  44402  stirlinglem15  44403  stirlingr  44405  dirkertrigeqlem1  44413  fouriersw  44546  ovnsubaddlem1  44885  subsubelfzo0  45632  2ffzoeq  45634  iccpartres  45684  iccpartipre  45687  iccpartltu  45691  iccelpart  45699  odz2prm2pw  45829  fmtnoprmfac2lem1  45832  2pwp1prm  45855  lighneallem2  45872  lighneallem4  45876  lighneal  45877  proththd  45880  nneoALTV  45938  divgcdoddALTV  45948  fpprmod  45993  fppr2odd  45997  dfwppr  46004  fpprwppr  46005  fpprwpprb  46006  gbowge7  46029  gbege6  46031  altgsumbc  46502  altgsumbcALT  46503  pw2m1lepw2m1  46675  nnpw2even  46689  nnlog2ge0lt1  46726  logbpw2m1  46727  blenpw2m1  46739  nnpw2blenfzo  46741  nnpw2pmod  46743  nnpw2p  46746  blengt1fldiv2p1  46753  dignn0fr  46761  dignn0flhalflem1  46775  dignn0flhalflem2  46776  nn0sumshdiglemA  46779  nn0sumshdiglemB  46780
  Copyright terms: Public domain W3C validator