Theorem zsubcl 12601

Description: Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)

Assertion

Ref	Expression
zsubcl	⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ)

Proof of Theorem zsubcl

Step	Hyp	Ref	Expression
1		zcn 12560	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
2		zcn 12560	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
3		negsub 11505	. . 3 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
4	1, 2, 3	syl2an 597	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
5		znegcl 12594	. . 3 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
6		zaddcl 12599	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
7	5, 6	sylan2 594	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
8	4, 7	eqeltrrd 2835	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  (class class class)co 7406  ℂcc 11105   + caddc 11110   − cmin 11441  -cneg 11442  ℤcz 12555

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 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184

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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-nn 12210  df-n0 12470  df-z 12556

This theorem is referenced by:  peano2zm  12602  zrevaddcl  12604  znnsub  12605  znn0sub  12606  nzadd  12607  zneo  12642  zsubcld  12668  eluzsubiOLD  12853  subeluzsub  12856  fzen  13515  uzsubsubfz  13520  fzrev  13561  fzrev2  13562  fzrevral2  13584  fzshftral  13586  fz0fzdiffz0  13607  difelfzle  13611  difelfznle  13612  fzo0n  13651  fzonfzoufzol  13732  elfzomelpfzo  13733  zmodcl  13853  addmodlteq  13908  fzen2  13931  facndiv  14245  bccmpl  14266  bcval5  14275  bcpasc  14278  hashfz  14384  swrdspsleq  14612  pfxccatin12lem4  14673  pfxccatin12lem2a  14674  pfxccatin12lem1  14675  pfxccatin12lem2  14678  swrdccat  14682  repswswrd  14731  cshwsublen  14743  cshwidxmodr  14751  2cshwid  14761  3cshw  14765  cshweqdif2  14766  2cshwcshw  14773  cshwcshid  14775  seqshft  15029  isercoll2  15612  zfallfaccl  15962  binomrisefac  15983  bpolydiflem  15995  moddvds  16205  modmulconst  16228  dvds2sub  16231  dvdssub2  16241  dvdssubr  16245  fzocongeq  16264  3dvds  16271  odd2np1  16281  omoe  16304  omeo  16306  divalglem0  16333  divalglem4  16336  divalglem9  16341  divalgb  16344  divalgmod  16346  ndvdsadd  16350  nn0seqcvgd  16504  congr  16598  cncongr1  16601  cncongr2  16602  eulerthlem2  16712  prmdiv  16715  prmdiveq  16716  pythagtriplem4  16749  pythagtriplem8  16753  difsqpwdvds  16817  prmgaplem7  16987  mod2xnegi  17001  cshwshashlem2  17027  mndodcongi  19406  odcong  19412  odf1  19425  odf1o1  19435  efgredleme  19606  srgbinomlem4  20046  plyeq0lem  25716  aaliou3lem1  25847  aaliou3lem2  25848  efif1olem2  26044  wilthlem2  26563  basellem2  26576  dchrptlem1  26757  bposlem6  26782  gausslemma2dlem6  26865  lgsquadlem1  26873  crctcshwlkn0lem7  29060  crctcshwlkn0  29065  clwlkclwwlklem2fv2  29239  ballotlemfelz  33478  fwddifnp1  35126  knoppndvlem2  35378  poimirlem28  36505  lcmineqlem1  40883  irrapxlem1  41546  jm2.24nn  41684  congtr  41690  congadd  41691  congmul  41692  congabseq  41699  acongeq  41708  jm2.26a  41725  jm2.15nn0  41728  jm2.27c  41732  jm3.1  41745  2elfz2melfz  46013  elfzlble  46015  elfzelfzlble  46016  subsubelfzo0  46021  altgsumbc  46982  altgsumbcALT  46983  zlmodzxzsub  46990