Theorem zsubcl 12635

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 12595	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
2		zcn 12595	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
3		negsub 11505	. . 3 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
4	1, 2, 3	syl2an 607	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
5		znegcl 12628	. . 3 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
6		zaddcl 12633	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
7	5, 6	sylan2 604	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
8	4, 7	eqeltrrd 2870	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  (class class class)co 7411  ℂcc 11097   + caddc 11102   − cmin 11440  -cneg 11441  ℤcz 12590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-nn 12233  df-n0 12504  df-z 12591

This theorem is referenced by:  peano2zm  12636  zrevaddcl  12638  znnsub  12639  znn0sub  12640  nzadd  12641  zneo  12678  zsubcld  12704  subeluzsub  12894  fzen  13568  uzsubsubfz  13573  fzrev  13614  fzrev2  13615  fzrevral2  13640  fzshftral  13642  fz0fzdiffz0  13664  difelfzle  13668  difelfznle  13669  fzo0n  13709  fzonfzoufzol  13799  elfzomelpfzo  13800  zmodcl  13923  addmodlteq  13981  fzen2  14004  facndiv  14323  bccmpl  14344  bcval5  14353  bcpasc  14356  hashfz  14463  swrdspsleq  14702  pfxccatin12lem4  14762  pfxccatin12lem2a  14763  pfxccatin12lem1  14764  pfxccatin12lem2  14767  swrdccat  14771  repswswrd  14820  cshwsublen  14832  cshwidxmodr  14840  2cshwid  14850  3cshw  14854  cshweqdif2  14855  2cshwcshw  14861  cshwcshid  14863  seqshft  15121  isercoll2  15719  zfallfaccl  16074  binomrisefac  16095  bpolydiflem  16107  moddvds  16320  modmulconst  16345  dvds2sub  16348  dvdssub2  16358  dvdssubr  16362  fzocongeq  16381  3dvds  16388  odd2np1  16398  omoe  16421  omeo  16423  divalglem0  16450  divalglem4  16453  divalglem9  16458  divalgb  16461  divalgmod  16463  ndvdsadd  16467  nn0seqcvgd  16627  congr  16721  cncongr1  16724  cncongr2  16725  eulerthlem2  16840  prmdiv  16843  prmdiveq  16844  pythagtriplem4  16878  pythagtriplem8  16882  difsqpwdvds  16946  prmgaplem7  17116  mod2xnegi  17130  cshwshashlem2  17155  chnub  18677  mndodcongi  19612  odcong  19618  odf1  19631  odf1o1  19641  efgredleme  19812  srgbinomlem4  20310  plyeq0lem  26335  aaliou3lem1  26471  aaliou3lem2  26472  efif1olem2  26673  wilthlem2  27198  basellem2  27211  dchrptlem1  27393  bposlem6  27418  gausslemma2dlem6  27501  lgsquadlem1  27509  crctcshwlkn0lem7  30105  crctcshwlkn0  30110  clwlkclwwlklem2fv2  30287  ballotlemfelz  34825  fwddifnp1  36555  knoppndvlem2  36990  poimirlem28  38186  lcmineqlem1  42685  irrapxlem1  43440  jm2.24nn  43577  congtr  43583  congadd  43584  congmul  43585  congabseq  43592  acongeq  43601  jm2.26a  43618  jm2.15nn0  43621  jm2.27c  43625  jm3.1  43638  2elfz2melfz  47943  elfzlble  47945  elfzelfzlble  47946  subsubelfzo0  47952  submodaddmod  47972  difltmodne  47973  submodneaddmod  47982  modmkpkne  47992  mod2addne  47995  altgsumbc  49016  altgsumbcALT  49017  zlmodzxzsub  49024