Theorem zsubcl 12560

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 12520	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
2		zcn 12520	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
3		negsub 11433	. . 3 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
4	1, 2, 3	syl2an 597	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
5		znegcl 12553	. . 3 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
6		zaddcl 12558	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
7	5, 6	sylan2 594	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
8	4, 7	eqeltrrd 2838	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   + caddc 11032   − cmin 11368  -cneg 11369  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  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-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516

This theorem is referenced by:  peano2zm  12561  zrevaddcl  12563  znnsub  12564  znn0sub  12565  nzadd  12566  zneo  12603  zsubcld  12629  subeluzsub  12812  fzen  13486  uzsubsubfz  13491  fzrev  13532  fzrev2  13533  fzrevral2  13558  fzshftral  13560  fz0fzdiffz0  13582  difelfzle  13586  difelfznle  13587  fzo0n  13627  fzonfzoufzol  13717  elfzomelpfzo  13718  zmodcl  13841  addmodlteq  13899  fzen2  13922  facndiv  14241  bccmpl  14262  bcval5  14271  bcpasc  14274  hashfz  14380  swrdspsleq  14619  pfxccatin12lem4  14679  pfxccatin12lem2a  14680  pfxccatin12lem1  14681  pfxccatin12lem2  14684  swrdccat  14688  repswswrd  14737  cshwsublen  14749  cshwidxmodr  14757  2cshwid  14767  3cshw  14771  cshweqdif2  14772  2cshwcshw  14778  cshwcshid  14780  seqshft  15038  isercoll2  15622  zfallfaccl  15977  binomrisefac  15998  bpolydiflem  16010  moddvds  16223  modmulconst  16248  dvds2sub  16251  dvdssub2  16261  dvdssubr  16265  fzocongeq  16284  3dvds  16291  odd2np1  16301  omoe  16324  omeo  16326  divalglem0  16353  divalglem4  16356  divalglem9  16361  divalgb  16364  divalgmod  16366  ndvdsadd  16370  nn0seqcvgd  16530  congr  16624  cncongr1  16627  cncongr2  16628  eulerthlem2  16743  prmdiv  16746  prmdiveq  16747  pythagtriplem4  16781  pythagtriplem8  16785  difsqpwdvds  16849  prmgaplem7  17019  mod2xnegi  17033  cshwshashlem2  17058  chnub  18579  mndodcongi  19509  odcong  19515  odf1  19528  odf1o1  19538  efgredleme  19709  srgbinomlem4  20201  plyeq0lem  26185  aaliou3lem1  26319  aaliou3lem2  26320  efif1olem2  26520  wilthlem2  27046  basellem2  27059  dchrptlem1  27241  bposlem6  27266  gausslemma2dlem6  27349  lgsquadlem1  27357  crctcshwlkn0lem7  29899  crctcshwlkn0  29904  clwlkclwwlklem2fv2  30081  ballotlemfelz  34651  fwddifnp1  36363  knoppndvlem2  36789  poimirlem28  37983  lcmineqlem1  42482  irrapxlem1  43268  jm2.24nn  43405  congtr  43411  congadd  43412  congmul  43413  congabseq  43420  acongeq  43429  jm2.26a  43446  jm2.15nn0  43449  jm2.27c  43453  jm3.1  43466  2elfz2melfz  47778  elfzlble  47780  elfzelfzlble  47781  subsubelfzo0  47787  submodaddmod  47807  difltmodne  47808  submodneaddmod  47817  modmkpkne  47827  mod2addne  47830  altgsumbc  48840  altgsumbcALT  48841  zlmodzxzsub  48848