Theorem zsubcl 12408

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 12370	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
2		zcn 12370	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
3		negsub 11315	. . 3 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
4	1, 2, 3	syl2an 597	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) = (𝑀 − 𝑁))
5		znegcl 12401	. . 3 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
6		zaddcl 12406	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ -𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
7	5, 6	sylan2 594	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) ∈ ℤ)
8	4, 7	eqeltrrd 2838	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1539   ∈ wcel 2104  (class class class)co 7307  ℂcc 10915   + caddc 10920   − cmin 11251  -cneg 11252  ℤcz 12365

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-resscn 10974  ax-1cn 10975  ax-icn 10976  ax-addcl 10977  ax-addrcl 10978  ax-mulcl 10979  ax-mulrcl 10980  ax-mulcom 10981  ax-addass 10982  ax-mulass 10983  ax-distr 10984  ax-i2m1 10985  ax-1ne0 10986  ax-1rid 10987  ax-rnegex 10988  ax-rrecex 10989  ax-cnre 10990  ax-pre-lttri 10991  ax-pre-lttrn 10992  ax-pre-ltadd 10993  ax-pre-mulgt0 10994

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-riota 7264  df-ov 7310  df-oprab 7311  df-mpo 7312  df-om 7745  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-er 8529  df-en 8765  df-dom 8766  df-sdom 8767  df-pnf 11057  df-mnf 11058  df-xr 11059  df-ltxr 11060  df-le 11061  df-sub 11253  df-neg 11254  df-nn 12020  df-n0 12280  df-z 12366

This theorem is referenced by:  peano2zm  12409  zrevaddcl  12411  znnsub  12412  znn0sub  12413  nzadd  12414  zneo  12449  zsubcld  12477  eluzsubi  12658  subeluzsub  12661  fzen  13319  uzsubsubfz  13324  fzrev  13365  fzrev2  13366  fzrevral2  13388  fzshftral  13390  fz0fzdiffz0  13411  difelfzle  13415  difelfznle  13416  fzo0n  13455  fzonfzoufzol  13536  elfzomelpfzo  13537  zmodcl  13657  addmodlteq  13712  fzen2  13735  facndiv  14048  bccmpl  14069  bcval5  14078  bcpasc  14081  hashfz  14187  swrdspsleq  14423  pfxccatin12lem4  14484  pfxccatin12lem2a  14485  pfxccatin12lem1  14486  pfxccatin12lem2  14489  swrdccat  14493  repswswrd  14542  cshwsublen  14554  cshwidxmodr  14562  2cshwid  14572  3cshw  14576  cshweqdif2  14577  2cshwcshw  14583  cshwcshid  14585  seqshft  14841  isercoll2  15425  zfallfaccl  15776  binomrisefac  15797  bpolydiflem  15809  moddvds  16019  modmulconst  16042  dvds2sub  16045  dvdssub2  16055  dvdssubr  16059  fzocongeq  16078  3dvds  16085  odd2np1  16095  omoe  16118  omeo  16120  divalglem0  16147  divalglem4  16150  divalglem9  16155  divalgb  16158  divalgmod  16160  ndvdsadd  16164  nn0seqcvgd  16320  congr  16414  cncongr1  16417  cncongr2  16418  eulerthlem2  16528  prmdiv  16531  prmdiveq  16532  pythagtriplem4  16565  pythagtriplem8  16569  difsqpwdvds  16633  prmgaplem7  16803  mod2xnegi  16817  cshwshashlem2  16843  mndodcongi  19196  odcong  19202  odf1  19214  odf1o1  19222  efgredleme  19394  srgbinomlem4  19824  plyeq0lem  25416  aaliou3lem1  25547  aaliou3lem2  25548  efif1olem2  25744  wilthlem2  26263  basellem2  26276  dchrptlem1  26457  bposlem6  26482  gausslemma2dlem6  26565  lgsquadlem1  26573  crctcshwlkn0lem7  28226  crctcshwlkn0  28231  clwlkclwwlklem2fv2  28405  ballotlemfelz  32502  fwddifnp1  34512  knoppndvlem2  34738  poimirlem28  35849  lcmineqlem1  40079  irrapxlem1  40681  jm2.24nn  40819  congtr  40825  congadd  40826  congmul  40827  congabseq  40834  acongeq  40843  jm2.26a  40860  jm2.15nn0  40863  jm2.27c  40867  jm3.1  40880  2elfz2melfz  44868  elfzlble  44870  elfzelfzlble  44871  subsubelfzo0  44876  altgsumbc  45746  altgsumbcALT  45747  zlmodzxzsub  45754