Theorem zsubcl 12551

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 12510	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
2		zcn 12510	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
3		negsub 11446	. . 3 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
4	1, 2, 3	syl2an 596	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
5		znegcl 12544	. . 3 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
6		zaddcl 12549	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
7	5, 6	sylan2 593	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
8	4, 7	eqeltrrd 2829	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042   + caddc 11047   − cmin 11381  -cneg 11382  ℤcz 12505

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 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-nn 12163  df-n0 12419  df-z 12506

This theorem is referenced by:  peano2zm  12552  zrevaddcl  12554  znnsub  12555  znn0sub  12556  nzadd  12557  zneo  12593  zsubcld  12619  eluzsubiOLD  12803  subeluzsub  12806  fzen  13478  uzsubsubfz  13483  fzrev  13524  fzrev2  13525  fzrevral2  13550  fzshftral  13552  fz0fzdiffz0  13574  difelfzle  13578  difelfznle  13579  fzo0n  13618  fzonfzoufzol  13707  elfzomelpfzo  13708  zmodcl  13829  addmodlteq  13887  fzen2  13910  facndiv  14229  bccmpl  14250  bcval5  14259  bcpasc  14262  hashfz  14368  swrdspsleq  14606  pfxccatin12lem4  14667  pfxccatin12lem2a  14668  pfxccatin12lem1  14669  pfxccatin12lem2  14672  swrdccat  14676  repswswrd  14725  cshwsublen  14737  cshwidxmodr  14745  2cshwid  14755  3cshw  14759  cshweqdif2  14760  2cshwcshw  14767  cshwcshid  14769  seqshft  15027  isercoll2  15611  zfallfaccl  15963  binomrisefac  15984  bpolydiflem  15996  moddvds  16209  modmulconst  16234  dvds2sub  16237  dvdssub2  16247  dvdssubr  16251  fzocongeq  16270  3dvds  16277  odd2np1  16287  omoe  16310  omeo  16312  divalglem0  16339  divalglem4  16342  divalglem9  16347  divalgb  16350  divalgmod  16352  ndvdsadd  16356  nn0seqcvgd  16516  congr  16610  cncongr1  16613  cncongr2  16614  eulerthlem2  16728  prmdiv  16731  prmdiveq  16732  pythagtriplem4  16766  pythagtriplem8  16770  difsqpwdvds  16834  prmgaplem7  17004  mod2xnegi  17018  cshwshashlem2  17043  mndodcongi  19449  odcong  19455  odf1  19468  odf1o1  19478  efgredleme  19649  srgbinomlem4  20114  plyeq0lem  26091  aaliou3lem1  26226  aaliou3lem2  26227  efif1olem2  26428  wilthlem2  26955  basellem2  26968  dchrptlem1  27151  bposlem6  27176  gausslemma2dlem6  27259  lgsquadlem1  27267  crctcshwlkn0lem7  29719  crctcshwlkn0  29724  clwlkclwwlklem2fv2  29898  chnub  32911  ballotlemfelz  34455  fwddifnp1  36126  knoppndvlem2  36474  poimirlem28  37615  lcmineqlem1  41990  irrapxlem1  42783  jm2.24nn  42921  congtr  42927  congadd  42928  congmul  42929  congabseq  42936  acongeq  42945  jm2.26a  42962  jm2.15nn0  42965  jm2.27c  42969  jm3.1  42982  2elfz2melfz  47292  elfzlble  47294  elfzelfzlble  47295  subsubelfzo0  47300  submodaddmod  47315  difltmodne  47316  submodneaddmod  47325  modmkpkne  47335  mod2addne  47338  altgsumbc  48313  altgsumbcALT  48314  zlmodzxzsub  48321