Theorem nnz 12543

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

Step	Hyp	Ref	Expression
1		nnre 12179	. 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		3mix2 1338	. 2 ⊢ (𝑁 ∈ ℕ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
3		elz 12524	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
4	1, 2, 3	sylanbrc 589	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∨ w3o 1091   = wceq 1547   ∈ wcel 2119  ℝcr 11035  0cc0 11036  -cneg 11376  ℕcn 12172  ℤcz 12522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-i2m1 11104  ax-1ne0 11105  ax-rrecex 11108  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-om 7814  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-neg 11378  df-nn 12173  df-z 12523

This theorem is referenced by:  nnssz  12544  elnnz1  12551  znegcl  12560  nnleltp1  12582  nnltp1le  12583  nnlem1lt  12593  nnltlem1  12594  nnm1ge0  12595  prime  12608  nneo  12611  zeo  12613  btwnz  12630  eluz2b2  12869  qaddcl  12913  qreccl  12917  elpqb  12924  elfz1end  13506  fznatpl1  13530  fznn  13544  elfz1b  13545  elfzo0  13653  elfzo0z  13654  elfzo1  13665  fzo1fzo0n0  13668  elfzom1p1elfzo  13698  ubmelm1fzo  13716  quoremz  13812  intfracq  13816  fznnfl  13819  zmodcl  13848  zmodfz  13850  zmodfzo  13851  zmodid2  13856  zmodidfzo  13857  modfzo0difsn  13903  expnnval  14024  mulexpz  14062  nnesq  14187  expnlbnd  14193  expnlbnd2  14194  digit2  14196  faclbnd  14250  bc0k  14271  bcval5  14278  fz1isolem  14421  seqcoll  14424  ccatval21sw  14546  lswccatn0lsw  14552  cshwidxmod  14763  cshwidxn  14769  absexpz  15265  climuni  15512  isercoll  15628  climcnds  15814  arisum  15823  trireciplem  15825  expcnv  15827  pwdif  15831  geo2sum  15836  geo2lim  15838  0.999...  15844  geoihalfsum  15845  rpnnen2lem6  16184  rpnnen2lem9  16187  rpnnen2lem10  16188  dvdsval3  16223  nndivdvds  16228  modmulconst  16255  dvdsle  16277  dvdsssfz1  16285  fzm1ndvds  16289  dvdsfac  16293  mulmoddvds  16297  oexpneg  16312  nnoddm1d2  16353  pwp1fsum  16358  divalg2  16372  divalgmod  16373  modremain  16375  ndvdsadd  16377  nndvdslegcd  16472  divgcdz  16478  divgcdnn  16482  divgcdnnr  16483  modgcd  16499  gcdmultiple  16503  gcddiv  16518  gcdzeq  16519  gcdeq  16520  rpmulgcd  16524  rplpwr  16525  rprpwr  16526  nn0rppwr  16528  sqgcd  16529  nn0expgcd  16531  dvdssqlem  16533  dvdssq  16534  eucalginv  16551  lcmgcdlem  16573  lcmgcdnn  16578  lcmass  16581  lcmftp  16603  lcmfunsnlem2lem1  16605  coprmgcdb  16616  qredeq  16624  qredeu  16625  coprmprod  16628  coprmproddvdslem  16629  coprmproddvds  16630  cncongr1  16634  cncongr2  16635  1idssfct  16647  isprm2lem  16648  isprm3  16650  prmind2  16652  ge2nprmge4  16669  divgcdodd  16678  isprm6  16682  ncoprmlnprm  16696  divnumden  16716  divdenle  16717  nn0gcdsq  16720  phicl2  16736  phiprmpw  16744  eulerthlem2  16750  hashgcdlem  16756  hashgcdeq  16758  phisum  16759  nnoddn2prm  16780  pythagtriplem3  16787  pythagtriplem4  16788  pythagtriplem6  16790  pythagtriplem7  16791  pythagtriplem8  16792  pythagtriplem9  16793  pythagtriplem11  16794  pythagtriplem13  16796  pythagtriplem15  16798  pythagtriplem19  16802  pythagtrip  16803  iserodd  16804  pclem  16807  pccl  16818  pcdiv  16821  pcqcl  16825  pcdvds  16833  pcndvds  16835  pcndvds2  16837  pcelnn  16839  pcz  16850  pcmpt  16861  fldivp1  16866  pcfac  16868  infpnlem1  16879  prmunb  16883  prmreclem1  16885  1arith  16896  ram0  16991  prmdvdsprmo  17011  prmgaplem4  17023  prmgaplem6  17025  prmgaplem7  17026  cshwshashlem2  17065  setsstruct2  17142  mulgnn  19049  mulgaddcom  19072  mulginvcom  19073  mulgmodid  19087  ghmmulg  19201  dfod2  19537  gexdvds  19557  gexnnod  19561  gexex  19826  mulgass2  20288  qsssubdrg  21408  prmirredlem  21454  znidomb  21543  znrrg  21547  chfacfisf  22844  chfacfisfcpmat  22845  chfacfscmul0  22848  chfacfpmmul0  22852  cayhamlem1  22856  cpmadugsumlemF  22866  lmmo  23370  1stckgenlem  23543  imasdsf1olem  24363  clmmulg  25093  cmetcaulem  25280  ovolunlem1a  25488  ovolicc2lem4  25512  mbfi1fseqlem6  25712  dvexp3  25970  dgreq0  26255  elqaalem2  26311  aaliou3lem1  26333  aaliou3lem2  26334  aaliou3lem3  26335  aaliou3lem9  26341  pserdvlem2  26418  logtayl2  26651  root1eq1  26744  root1cj  26745  zrtdvds  26748  logbgcd1irr  26783  atantayl2  26927  birthdaylem2  26941  birthdaylem3  26942  emcllem5  26988  basellem2  27070  basellem3  27071  basellem5  27073  issqf  27124  sgmnncl  27135  prmorcht  27166  mumullem1  27167  mumullem2  27168  sqff1o  27170  dvdsflsumcom  27176  muinv  27181  vmalelog  27193  chtublem  27199  vmasum  27204  logfac2  27205  logfaclbnd  27210  bclbnd  27268  bposlem5  27276  lgsval4a  27307  lgssq2  27326  lgsdchr  27343  gausslemma2dlem0c  27346  gausslemma2dlem0e  27348  gausslemma2dlem1a  27353  gausslemma2dlem5  27359  lgsquadlem1  27368  lgsquadlem2  27369  lgsquad3  27375  2lgslem1a1  27377  2lgslem3  27392  2lgsoddprm  27404  2sqnn  27427  2sqreunnltlem  27438  rplogsumlem1  27472  rplogsumlem2  27473  dchrisumlem2  27478  dchrmusumlema  27481  dchrmusum2  27482  dchrvmasumiflem1  27489  dchrvmaeq0  27492  dchrisum0flblem2  27497  dchrisum0re  27501  dchrisum0lema  27502  dchrisum0lem1b  27503  dchrisum0lem2a  27505  logdivbnd  27544  pntrsumbnd2  27555  ostth2lem1  27606  ostth2lem3  27623  ostth3  27626  axlowdimlem13  29048  crctcshwlkn0lem4  29906  crctcshwlkn0lem5  29907  crctcshwlkn0lem7  29909  wlkiswwlksupgr2  29970  clwwisshclwwslem  30109  clwwlkinwwlk  30135  clwwlkel  30141  clwwlkf  30142  wwlksubclwwlk  30153  clwwlkvbij  30208  eucrctshift  30338  eucrct2eupth  30340  numclwlk2lem2f  30472  bcm1n  32894  pnfinf  33271  isarchiofld  33287  1fldgenq  33413  rearchi  33436  submat1n  33996  lmatfvlem  34006  esumcvg  34277  oddpwdc  34545  fibp1  34592  chtvalz  34820  nnltp1ne  35346  erdszelem7  35432  climuzcnv  35906  elfzm12  35910  bcprod  35973  nn0prpwlem  36557  knoppndvlem1  36825  knoppndvlem2  36826  knoppndvlem7  36831  knoppndvlem18  36842  poimirlem13  38007  poimirlem14  38008  mblfinlem2  38032  fzmul  38115  incsequz  38122  geomcau  38133  heibor1lem  38183  bfplem2  38197  lcmfunnnd  42504  posbezout  42592  unitscyglem4  42690  dvdsexpnn  42817  dvdsexpnn0  42818  fimgmcyc  43027  fzsplit1nn0  43210  irrapxlem1  43274  pellexlem5  43285  rmynn  43408  jm2.24nn  43411  jm2.17c  43414  congrep  43425  congabseq  43426  acongrep  43432  acongeq  43435  jm2.18  43440  jm2.23  43448  jm2.20nn  43449  jm2.26lem3  43453  jm2.26  43454  jm2.15nn0  43455  jm2.16nn0  43456  jm2.27dlem2  43462  rmydioph  43466  jm3.1  43472  expdiophlem1  43473  expdioph  43475  idomodle  43643  proot1ex  43648  nznngen  44767  sumnnodd  46082  stoweidlem7  46457  stoweidlem17  46467  wallispilem4  46518  stirlinglem2  46525  stirlinglem3  46526  stirlinglem4  46527  stirlinglem12  46535  stirlinglem13  46536  stirlinglem14  46537  stirlinglem15  46538  stirlingr  46540  dirkertrigeqlem1  46548  fouriersw  46681  ovnsubaddlem1  47020  nthrucw  47338  subsubelfzo0  47797  2ffzoeq  47798  nnmul2  47800  ceilhalfelfzo1  47804  2tceilhalfelfzo1  47806  difltmodne  47818  addmodne  47820  submodlt  47826  facnn0dvdsfac  47855  muldvdsfacgt  47856  iccpartres  47900  iccpartipre  47903  iccpartltu  47907  iccelpart  47915  odz2prm2pw  48048  fmtnoprmfac2lem1  48051  2pwp1prm  48074  lighneallem2  48091  lighneallem4  48095  lighneal  48096  proththd  48099  nneoALTV  48170  divgcdoddALTV  48180  fpprmod  48225  fppr2odd  48229  dfwppr  48236  fpprwppr  48237  fpprwpprb  48238  gbowge7  48261  gbege6  48263  gpg3kgrtriexlem2  48582  gpg3kgrtriexlem3  48583  gpg3kgrtriexlem5  48585  gpg3kgrtriexlem6  48586  altgsumbc  48850  altgsumbcALT  48851  pw2m1lepw2m1  49018  nnpw2even  49027  nnlog2ge0lt1  49064  logbpw2m1  49065  blenpw2m1  49077  nnpw2blenfzo  49079  nnpw2pmod  49081  nnpw2p  49084  blengt1fldiv2p1  49091  dignn0fr  49099  dignn0flhalflem1  49113  dignn0flhalflem2  49114  nn0sumshdiglemA  49117  nn0sumshdiglemB  49118