Theorem nnz 12640

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 12268	. 2 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
2		3mix2 1350	. 2 ⊢ (𝑁 ∈ ℕ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
3		elz 12621	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
4	1, 2, 3	sylanbrc 595	1 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102   = wceq 1570   ∈ wcel 2145  ℝcr 11127  0cc0 11128  -cneg 11470  ℕcn 12261  ℤcz 12619

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-i2m1 11196  ax-1ne0 11197  ax-rrecex 11200  ax-cnre 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-om 7867  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-neg 11472  df-nn 12262  df-z 12620

This theorem is used by:  nnssz  12641  elnnz1  12648  znegcl  12657  nnleltp1  12680  nnltp1le  12681  nnlem1lt  12691  nnltlem1  12692  nnm1ge0  12693  prime  12706  nneo  12709  zeo  12711  btwnz  12728  eluz2b2  12974  qaddcl  13019  qreccl  13023  elpqb  13030  elfz1end  13613  fznatpl1  13637  fznn  13651  elfz1b  13652  elfzo0  13760  elfzo0z  13761  elfzo1  13772  fzo1fzo0n0  13775  elfzom1p1elfzo  13805  ubmelm1fzo  13823  quoremz  13920  intfracq  13924  fznnfl  13927  zmodcl  13956  zmodfz  13958  zmodfzo  13959  zmodid2  13964  zmodidfzo  13965  modfzo0difsn  14011  expnnval  14132  mulexpz  14170  nnesq  14295  expnlbnd  14301  expnlbnd2  14302  digit2  14304  faclbnd  14358  bc0k  14379  bcval5  14386  fz1isolem  14530  seqcoll  14533  ccatval21sw  14655  lswccatn0lsw  14662  cshwidxmod  14878  cshwidxn  14884  absexpz  15396  climuni  15643  isercoll  15759  climcnds  15944  arisum  15953  trireciplem  15955  expcnv  15957  pwdif  15961  geo2sum  15966  geo2lim  15968  0.999...  15974  geoihalfsum  15975  rpnnen2lem6  16313  rpnnen2lem9  16316  rpnnen2lem10  16317  dvdsval3  16352  nndivdvds  16357  modmulconst  16384  dvdsle  16406  dvdsssfz1  16414  fzm1ndvds  16418  dvdsfac  16422  mulmoddvds  16426  oexpneg  16441  nnoddm1d2  16482  pwp1fsum  16487  divalg2  16501  divalgmod  16502  modremain  16504  ndvdsadd  16506  nndvdslegcd  16601  divgcdz  16607  divgcdnn  16611  divgcdnnr  16612  modgcd  16628  gcdmultiple  16632  gcddiv  16647  gcdzeq  16648  gcdeq  16649  rpmulgcd  16653  rplpwr  16654  rprpwr  16655  nn0rppwr  16657  sqgcd  16658  nn0expgcd  16660  dvdssqlem  16662  dvdssq  16663  eucalginv  16680  lcmgcdlem  16702  lcmgcdnn  16707  lcmass  16710  lcmftp  16732  lcmfunsnlem2lem1  16734  coprmgcdb  16745  qredeq  16753  qredeu  16754  coprmprod  16757  coprmproddvdslem  16758  coprmproddvds  16759  cncongr1  16763  cncongr2  16764  1idssfct  16776  isprm2lem  16777  isprm3  16779  prmind2  16781  ge2nprmge4  16798  divgcdodd  16807  isprm6  16811  ncoprmlnprm  16825  divnumden  16845  divdenle  16846  nn0gcdsq  16849  phicl2  16865  phiprmpw  16873  eulerthlem2  16879  hashgcdlem  16885  hashgcdeq  16887  phisum  16888  nnoddn2prm  16909  pythagtriplem3  16916  pythagtriplem4  16917  pythagtriplem6  16919  pythagtriplem7  16920  pythagtriplem8  16921  pythagtriplem9  16922  pythagtriplem11  16923  pythagtriplem13  16925  pythagtriplem15  16927  pythagtriplem19  16931  pythagtrip  16932  iserodd  16933  pclem  16936  pccl  16947  pcdiv  16950  pcqcl  16954  pcdvds  16962  pcndvds  16964  pcndvds2  16966  pcelnn  16968  pcz  16979  pcmpt  16990  fldivp1  16995  pcfac  16997  infpnlem1  17008  prmunb  17012  prmreclem1  17014  1arith  17025  ram0  17120  prmdvdsprmo  17140  prmgaplem4  17152  prmgaplem6  17154  prmgaplem7  17155  cshwshashlem2  17194  setsstruct2  17272  mulgnn  19204  mulgaddcom  19227  mulginvcom  19228  mulgmodid  19242  ghmmulg  19361  dfod2  19697  gexdvds  19717  gexnnod  19721  gexex  19986  mulgass2  20457  qsssubdrg  21645  prmirredlem  21691  znidomb  21780  znrrg  21784  chfacfisf  23085  chfacfisfcpmat  23086  chfacfscmul0  23089  chfacfpmmul0  23093  cayhamlem1  23097  cpmadugsumlemF  23107  lmmo  23611  1stckgenlem  23785  imasdsf1olem  24605  clmmulg  25335  cmetcaulem  25522  ovolunlem1a  25730  ovolicc2lem4  25754  mbfi1fseqlem6  25954  dvexp3  26212  dgreq0  26498  elqaalem2  26559  aaliou3lem1  26585  aaliou3lem2  26586  aaliou3lem3  26587  aaliou3lem9  26593  pserdvlem2  26671  logtayl2  26907  root1eq1  27000  root1cj  27001  zrtdvds  27004  logbgcd1irr  27039  atantayl2  27183  birthdaylem2  27197  birthdaylem3  27198  emcllem5  27244  basellem2  27326  basellem3  27327  basellem5  27329  issqf  27380  sgmnncl  27391  prmorcht  27422  mumullem1  27423  mumullem2  27424  sqff1o  27426  dvdsflsumcom  27432  muinv  27437  vmalelog  27449  chtublem  27455  vmasum  27460  logfac2  27461  logfaclbnd  27466  bclbnd  27524  bposlem5  27532  lgsval4a  27563  lgssq2  27582  lgsdchr  27599  gausslemma2dlem0c  27602  gausslemma2dlem0e  27604  gausslemma2dlem1a  27609  gausslemma2dlem5  27615  lgsquadlem1  27624  lgsquadlem2  27625  lgsquad3  27631  2lgslem1a1  27633  2lgslem3  27648  2lgsoddprm  27660  2sqnn  27683  2sqreunnltlem  27694  rplogsumlem1  27728  rplogsumlem2  27729  dchrisumlem2  27734  dchrmusumlema  27737  dchrmusum2  27738  dchrvmasumiflem1  27745  dchrvmaeq0  27748  dchrisum0flblem2  27753  dchrisum0re  27757  dchrisum0lema  27758  dchrisum0lem1b  27759  dchrisum0lem2a  27761  logdivbnd  27800  pntrsumbnd2  27811  ostth2lem1  27862  ostth2lem3  27879  ostth3  27882  axlowdimlem13  29419  crctcshwlkn0lem4  30289  crctcshwlkn0lem5  30290  crctcshwlkn0lem7  30292  wlkiswwlksupgr2  30353  clwwisshclwwslem  30492  clwwlkinwwlk  30518  clwwlkel  30524  clwwlkf  30525  wwlksubclwwlk  30536  clwwlkvbij  30591  eucrctshift  30731  eucrct2eupth  30733  numclwlk2lem2f  30865  bcm1n  33274  pnfinf  33631  isarchiofld  33647  1fldgenq  33771  rearchi  33794  submat1n  34323  lmatfvlem  34333  esumcvg  34604  oddpwdc  34873  fibp1  34920  chtvalz  35145  nnltp1ne  35723  erdszelem7  35784  climuzcnv  36258  elfzm12  36262  bcprod  36325  nn0prpwlem  36949  knoppndvlem1  37217  knoppndvlem2  37218  knoppndvlem7  37223  knoppndvlem18  37234  poimirlem13  38390  poimirlem14  38391  mblfinlem2  38415  fzmul  38499  incsequz  38506  geomcau  38517  heibor1lem  38567  bfplem2  38581  lcmfunnnd  42886  posbezout  42974  unitscyglem4  43072  dvdsexpnn  43216  dvdsexpnn0  43217  fimgmcyc  43424  fzsplit1nn0  43607  irrapxlem1  43671  pellexlem5  43682  rmynn  43805  jm2.24nn  43808  jm2.17c  43811  congrep  43822  congabseq  43823  acongrep  43829  acongeq  43832  jm2.18  43837  jm2.23  43845  jm2.20nn  43846  jm2.26lem3  43850  jm2.26  43851  jm2.15nn0  43852  jm2.16nn0  43853  jm2.27dlem2  43859  rmydioph  43863  jm3.1  43869  expdiophlem1  43870  expdioph  43872  idomodle  44040  proot1ex  44045  nznngen  45148  sumnnodd  46468  stoweidlem7  46843  stoweidlem17  46853  wallispilem4  46904  stirlinglem2  46911  stirlinglem3  46912  stirlinglem4  46913  stirlinglem12  46921  stirlinglem13  46922  stirlinglem14  46923  stirlinglem15  46924  stirlingr  46926  dirkertrigeqlem1  46934  fouriersw  47067  ovnsubaddlem1  47406  sqrtnnaa  47739  subsubelfzo0  48223  2ffzoeq  48224  nnmul2  48226  ceilhalfelfzo1  48230  2tceilhalfelfzo1  48232  difltmodne  48244  addmodne  48246  submodlt  48252  facnn0dvdsfac  48281  muldvdsfacgt  48282  iccpartres  48326  iccpartipre  48329  iccpartltu  48333  iccelpart  48341  odz2prm2pw  48474  fmtnoprmfac2lem1  48477  2pwp1prm  48500  lighneallem2  48517  lighneallem4  48521  lighneal  48522  proththd  48525  nneoALTV  48596  divgcdoddALTV  48606  fpprmod  48651  fppr2odd  48655  dfwppr  48662  fpprwppr  48663  fpprwpprb  48664  gbowge7  48687  gbege6  48689  gpg3kgrtriexlem2  49008  gpg3kgrtriexlem3  49009  gpg3kgrtriexlem5  49011  gpg3kgrtriexlem6  49012  altgsumbc  49290  altgsumbcALT  49291  pw2m1lepw2m1  49458  nnpw2even  49467  nnlog2ge0lt1  49504  logbpw2m1  49505  blenpw2m1  49517  nnpw2blenfzo  49519  nnpw2pmod  49521  nnpw2p  49524  blengt1fldiv2p1  49531  dignn0fr  49539  dignn0flhalflem1  49553  dignn0flhalflem2  49554  nn0sumshdiglemA  49557  nn0sumshdiglemB  49558