Theorem zsubcl 12666

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 12625	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
2		zcn 12625	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
3		negsub 11565	. . 3 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
4	1, 2, 3	syl2an 594	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
5		znegcl 12659	. . 3 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
6		zaddcl 12664	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
7	5, 6	sylan2 591	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
8	4, 7	eqeltrrd 2830	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ∈ wcel 2100  (class class class)co 7428  ℂcc 11163   + caddc 11168   − cmin 11501  -cneg 11502  ℤcz 12620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5305  ax-nul 5312  ax-pow 5371  ax-pr 5435  ax-un 7749  ax-resscn 11222  ax-1cn 11223  ax-icn 11224  ax-addcl 11225  ax-addrcl 11226  ax-mulcl 11227  ax-mulrcl 11228  ax-mulcom 11229  ax-addass 11230  ax-mulass 11231  ax-distr 11232  ax-i2m1 11233  ax-1ne0 11234  ax-1rid 11235  ax-rnegex 11236  ax-rrecex 11237  ax-cnre 11238  ax-pre-lttri 11239  ax-pre-lttrn 11240  ax-pre-ltadd 11241  ax-pre-mulgt0 11242

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3787  df-csb 3903  df-dif 3960  df-un 3962  df-in 3964  df-ss 3974  df-pss 3977  df-nul 4334  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4917  df-iun 5006  df-br 5155  df-opab 5217  df-mpt 5238  df-tr 5272  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5639  df-we 5641  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6315  df-ord 6381  df-on 6382  df-lim 6383  df-suc 6384  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563  df-fv 6564  df-riota 7384  df-ov 7431  df-oprab 7432  df-mpo 7433  df-om 7883  df-2nd 8010  df-frecs 8302  df-wrecs 8333  df-recs 8407  df-rdg 8446  df-er 8740  df-en 8981  df-dom 8982  df-sdom 8983  df-pnf 11307  df-mnf 11308  df-xr 11309  df-ltxr 11310  df-le 11311  df-sub 11503  df-neg 11504  df-nn 12275  df-n0 12535  df-z 12621

This theorem is referenced by:  peano2zm  12667  zrevaddcl  12669  znnsub  12670  znn0sub  12671  nzadd  12672  zneo  12707  zsubcld  12733  eluzsubiOLD  12918  subeluzsub  12921  fzen  13582  uzsubsubfz  13587  fzrev  13628  fzrev2  13629  fzrevral2  13651  fzshftral  13653  fz0fzdiffz0  13674  difelfzle  13678  difelfznle  13679  fzo0n  13718  fzonfzoufzol  13800  elfzomelpfzo  13801  zmodcl  13922  addmodlteq  13977  fzen2  14000  facndiv  14317  bccmpl  14338  bcval5  14347  bcpasc  14350  hashfz  14456  swrdspsleq  14694  pfxccatin12lem4  14755  pfxccatin12lem2a  14756  pfxccatin12lem1  14757  pfxccatin12lem2  14760  swrdccat  14764  repswswrd  14813  cshwsublen  14825  cshwidxmodr  14833  2cshwid  14843  3cshw  14847  cshweqdif2  14848  2cshwcshw  14855  cshwcshid  14857  seqshft  15111  isercoll2  15694  zfallfaccl  16044  binomrisefac  16065  bpolydiflem  16077  moddvds  16288  modmulconst  16311  dvds2sub  16314  dvdssub2  16324  dvdssubr  16328  fzocongeq  16347  3dvds  16354  odd2np1  16364  omoe  16387  omeo  16389  divalglem0  16416  divalglem4  16419  divalglem9  16424  divalgb  16427  divalgmod  16429  ndvdsadd  16433  nn0seqcvgd  16592  congr  16686  cncongr1  16689  cncongr2  16690  eulerthlem2  16805  prmdiv  16808  prmdiveq  16809  pythagtriplem4  16842  pythagtriplem8  16846  difsqpwdvds  16910  prmgaplem7  17080  mod2xnegi  17094  cshwshashlem2  17120  mndodcongi  19563  odcong  19569  odf1  19582  odf1o1  19592  efgredleme  19763  srgbinomlem4  20234  plyeq0lem  26260  aaliou3lem1  26393  aaliou3lem2  26394  efif1olem2  26593  wilthlem2  27120  basellem2  27133  dchrptlem1  27316  bposlem6  27341  gausslemma2dlem6  27424  lgsquadlem1  27432  crctcshwlkn0lem7  29773  crctcshwlkn0  29778  clwlkclwwlklem2fv2  29952  chnub  32909  ballotlemfelz  34362  fwddifnp1  36027  knoppndvlem2  36254  poimirlem28  37386  lcmineqlem1  41765  irrapxlem1  42540  jm2.24nn  42678  congtr  42684  congadd  42685  congmul  42686  congabseq  42693  acongeq  42702  jm2.26a  42719  jm2.15nn0  42722  jm2.27c  42726  jm3.1  42739  2elfz2melfz  46991  elfzlble  46993  elfzelfzlble  46994  subsubelfzo0  46999  altgsumbc  47802  altgsumbcALT  47803  zlmodzxzsub  47810