Theorem zsubcl 12018

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 11980	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
2		zcn 11980	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
3		negsub 10927	. . 3 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
4	1, 2, 3	syl2an 597	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
5		znegcl 12011	. . 3 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
6		zaddcl 12016	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
7	5, 6	sylan2 594	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
8	4, 7	eqeltrrd 2913	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1536   ∈ wcel 2113  (class class class)co 7149  ℂcc 10528   + caddc 10533   − cmin 10863  -cneg 10864  ℤcz 11975

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5323  ax-un 7454  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-nel 3123  df-ral 3142  df-rex 3143  df-reu 3144  df-rab 3146  df-v 3493  df-sbc 3769  df-csb 3877  df-dif 3932  df-un 3934  df-in 3936  df-ss 3945  df-pss 3947  df-nul 4285  df-if 4461  df-pw 4534  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-om 7574  df-wrecs 7940  df-recs 8001  df-rdg 8039  df-er 8282  df-en 8503  df-dom 8504  df-sdom 8505  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-nn 11632  df-n0 11892  df-z 11976

This theorem is referenced by:  peano2zm  12019  zrevaddcl  12021  znnsub  12022  znn0sub  12023  nzadd  12024  zneo  12059  zsubcld  12086  eluzsubi  12266  subeluzsub  12269  fzen  12921  uzsubsubfz  12926  fzrev  12967  fzrev2  12968  fzrevral2  12990  fzshftral  12992  fz0fzdiffz0  13013  difelfzle  13017  difelfznle  13018  fzo0n  13056  fzonfzoufzol  13137  elfzomelpfzo  13138  zmodcl  13256  addmodlteq  13311  fzen2  13334  facndiv  13645  bccmpl  13666  bcval5  13675  bcpasc  13678  hashfz  13785  swrdspsleq  14022  pfxccatin12lem4  14083  pfxccatin12lem2a  14084  pfxccatin12lem1  14085  pfxccatin12lem2  14088  swrdccat  14092  repswswrd  14141  cshwsublen  14153  cshwidxmodr  14161  2cshwid  14171  3cshw  14175  cshweqdif2  14176  2cshwcshw  14182  cshwcshid  14184  seqshft  14439  isercoll2  15020  zfallfaccl  15370  binomrisefac  15391  bpolydiflem  15403  moddvds  15613  modmulconst  15636  dvds2sub  15639  dvdssub2  15646  dvdssubr  15650  fzocongeq  15669  3dvds  15675  odd2np1  15685  omoe  15708  omeo  15710  divalglem0  15739  divalglem4  15742  divalglem9  15747  divalgb  15750  divalgmod  15752  ndvdsadd  15756  nn0seqcvgd  15909  congr  16003  cncongr1  16006  cncongr2  16007  eulerthlem2  16114  prmdiv  16117  prmdiveq  16118  pythagtriplem4  16151  pythagtriplem8  16155  difsqpwdvds  16218  prmgaplem7  16388  mod2xnegi  16402  cshwshashlem2  16425  mndodcongi  18666  odcong  18672  odf1  18684  odf1o1  18692  efgredleme  18864  srgbinomlem4  19288  plyeq0lem  24798  aaliou3lem1  24929  aaliou3lem2  24930  efif1olem2  25125  wilthlem2  25644  basellem2  25657  dchrptlem1  25838  bposlem6  25863  gausslemma2dlem6  25946  lgsquadlem1  25954  crctcshwlkn0lem7  27592  crctcshwlkn0  27597  clwlkclwwlklem2fv2  27772  ballotlemfelz  31769  fwddifnp1  33647  knoppndvlem2  33873  poimirlem28  34955  lcmineqlem1  39157  irrapxlem1  39495  jm2.24nn  39632  congtr  39638  congadd  39639  congmul  39640  congabseq  39647  acongeq  39656  jm2.26a  39673  jm2.15nn0  39676  jm2.27c  39680  jm3.1  39693  2elfz2melfz  43592  elfzlble  43594  elfzelfzlble  43595  subsubelfzo0  43600  altgsumbc  44474  altgsumbcALT  44475  zlmodzxzsub  44482