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 602	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
5		znegcl 12553	. . 3 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
6		zaddcl 12558	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
7	5, 6	sylan2 599	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
8	4, 7	eqeltrrd 2840	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  (class class class)co 7356  ℂ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 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 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  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 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 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  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  26193  aaliou3lem1  26326  aaliou3lem2  26327  efif1olem2  26525  wilthlem2  27050  basellem2  27063  dchrptlem1  27245  bposlem6  27270  gausslemma2dlem6  27353  lgsquadlem1  27361  crctcshwlkn0lem7  29902  crctcshwlkn0  29907  clwlkclwwlklem2fv2  30084  ballotlemfelz  34675  fwddifnp1  36393  knoppndvlem2  36819  poimirlem28  38015  lcmineqlem1  42514  irrapxlem1  43267  jm2.24nn  43404  congtr  43410  congadd  43411  congmul  43412  congabseq  43419  acongeq  43428  jm2.26a  43445  jm2.15nn0  43448  jm2.27c  43452  jm3.1  43465  2elfz2melfz  47781  elfzlble  47783  elfzelfzlble  47784  subsubelfzo0  47790  submodaddmod  47810  difltmodne  47811  submodneaddmod  47820  modmkpkne  47830  mod2addne  47833  altgsumbc  48843  altgsumbcALT  48844  zlmodzxzsub  48851