Theorem zsubcl 12582

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 12541	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
2		zcn 12541	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
3		negsub 11477	. . 3 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
4	1, 2, 3	syl2an 596	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
5		znegcl 12575	. . 3 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
6		zaddcl 12580	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
7	5, 6	sylan2 593	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
8	4, 7	eqeltrrd 2830	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   + caddc 11078   − cmin 11412  -cneg 11413  ℤcz 12536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-nn 12194  df-n0 12450  df-z 12537

This theorem is referenced by:  peano2zm  12583  zrevaddcl  12585  znnsub  12586  znn0sub  12587  nzadd  12588  zneo  12624  zsubcld  12650  eluzsubiOLD  12834  subeluzsub  12837  fzen  13509  uzsubsubfz  13514  fzrev  13555  fzrev2  13556  fzrevral2  13581  fzshftral  13583  fz0fzdiffz0  13605  difelfzle  13609  difelfznle  13610  fzo0n  13649  fzonfzoufzol  13738  elfzomelpfzo  13739  zmodcl  13860  addmodlteq  13918  fzen2  13941  facndiv  14260  bccmpl  14281  bcval5  14290  bcpasc  14293  hashfz  14399  swrdspsleq  14637  pfxccatin12lem4  14698  pfxccatin12lem2a  14699  pfxccatin12lem1  14700  pfxccatin12lem2  14703  swrdccat  14707  repswswrd  14756  cshwsublen  14768  cshwidxmodr  14776  2cshwid  14786  3cshw  14790  cshweqdif2  14791  2cshwcshw  14798  cshwcshid  14800  seqshft  15058  isercoll2  15642  zfallfaccl  15994  binomrisefac  16015  bpolydiflem  16027  moddvds  16240  modmulconst  16265  dvds2sub  16268  dvdssub2  16278  dvdssubr  16282  fzocongeq  16301  3dvds  16308  odd2np1  16318  omoe  16341  omeo  16343  divalglem0  16370  divalglem4  16373  divalglem9  16378  divalgb  16381  divalgmod  16383  ndvdsadd  16387  nn0seqcvgd  16547  congr  16641  cncongr1  16644  cncongr2  16645  eulerthlem2  16759  prmdiv  16762  prmdiveq  16763  pythagtriplem4  16797  pythagtriplem8  16801  difsqpwdvds  16865  prmgaplem7  17035  mod2xnegi  17049  cshwshashlem2  17074  mndodcongi  19480  odcong  19486  odf1  19499  odf1o1  19509  efgredleme  19680  srgbinomlem4  20145  plyeq0lem  26122  aaliou3lem1  26257  aaliou3lem2  26258  efif1olem2  26459  wilthlem2  26986  basellem2  26999  dchrptlem1  27182  bposlem6  27207  gausslemma2dlem6  27290  lgsquadlem1  27298  crctcshwlkn0lem7  29753  crctcshwlkn0  29758  clwlkclwwlklem2fv2  29932  chnub  32945  ballotlemfelz  34489  fwddifnp1  36160  knoppndvlem2  36508  poimirlem28  37649  lcmineqlem1  42024  irrapxlem1  42817  jm2.24nn  42955  congtr  42961  congadd  42962  congmul  42963  congabseq  42970  acongeq  42979  jm2.26a  42996  jm2.15nn0  42999  jm2.27c  43003  jm3.1  43016  2elfz2melfz  47323  elfzlble  47325  elfzelfzlble  47326  subsubelfzo0  47331  submodaddmod  47346  difltmodne  47347  submodneaddmod  47356  modmkpkne  47366  mod2addne  47369  altgsumbc  48344  altgsumbcALT  48345  zlmodzxzsub  48352