Theorem zsubcld 12619

Description: Closure of subtraction of integers. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
zred.1	⊢ (𝜑 → 𝐴 ∈ ℤ)
zaddcld.1	⊢ (𝜑 → 𝐵 ∈ ℤ)

Assertion

Ref	Expression
zsubcld	⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℤ)

Proof of Theorem zsubcld

Step	Hyp	Ref	Expression
1		zred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℤ)
2		zaddcld.1	. 2 ⊢ (𝜑 → 𝐵 ∈ ℤ)
3		zsubcl 12551	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℤ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7369   − cmin 11381  ℤ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:  eluzmn  12776  eluzsub  12799  uzsubsubfz  13483  fzm1  13544  eluzgtdifelfzo  13664  ubmelm1fzo  13700  elfznelfzo  13709  intfracq  13797  modsubdir  13881  modsumfzodifsn  13885  zesq  14167  bcval5  14259  ccatsymb  14523  swrdfv2  14602  ccatswrd  14609  cshwidxmod  14744  2cshwcshw  14767  cshwcsh2id  14770  fzomaxdiflem  15285  iseralt  15627  fsum0diaglem  15718  mptfzshft  15720  pwm1geoser  15811  mertenslem1  15826  fprodrev  15919  eirrlem  16148  fzocongeq  16270  3dvds  16277  modremain  16354  bitsfzolem  16380  bitsmod  16382  bitscmp  16384  bitsinv1lem  16387  sadaddlem  16412  bezoutlem3  16487  cncongr1  16613  hashdvds  16721  crth  16724  eulerthlem2  16728  prmdiveq  16732  modprm0  16752  pythagtriplem4  16766  pythagtriplem6  16768  pythagtriplem7  16769  pythagtriplem11  16772  pythagtriplem13  16774  pythagtriplem15  16776  pcqcl  16803  pcaddlem  16835  pcbc  16847  gzmulcl  16885  4sqlem5  16889  4sqlem8  16892  4sqlem11  16902  4sqlem12  16903  4sqlem14  16905  4sqlem16  16907  mndodconglem  19455  sylow1lem1  19512  sylow1lem3  19514  gsummptshft  19850  ablsimpgfindlem1  20023  pzriprnglem10  21432  fermltlchr  21471  znf1o  21493  zdis  24738  plydivex  26238  aaliou3lem8  26286  basellem3  27026  bcmono  27221  bcmax  27222  bposlem1  27228  lgsmod  27267  lgsdirprm  27275  lgsqrlem2  27291  gausslemma2dlem0h  27307  gausslemma2dlem1a  27309  gausslemma2dlem5a  27314  lgseisenlem1  27319  lgseisenlem2  27320  lgsquadlem1  27324  2lgslem2  27339  2sqlem4  27365  2sqlem8  27370  2sqmod  27380  pntrlog2bndlem1  27521  crctcshwlkn0lem3  29792  crctcshwlkn0lem4  29793  crctcshwlkn0lem6  29795  crctcshwlkn0  29801  clwlkclwwlklem2a1  29971  clwlkclwwlklem2fv1  29974  clwlkclwwlklem2a4  29976  clwlkclwwlklem2a  29977  fzspl  32762  fzsplit3  32766  ltesubnnd  32797  pfxlsw2ccat  32922  wrdt2ind  32925  swrdrn3  32927  cshwrnid  32933  chnub  32984  cycpmco2lem6  33103  cycpmco2lem7  33104  archirngz  33158  znfermltl  33330  cos9thpiminplylem2  33766  smatrcl  33779  ballotlemfp1  34476  ballotlemimin  34490  ballotlemic  34491  ballotlem1c  34492  ballotlemfrceq  34513  ballotlemfrcn0  34514  signsplypnf  34534  signslema  34546  reprsuc  34599  breprexplema  34614  breprexplemc  34616  circlemeth  34624  revpfxsfxrev  35096  bcprod  35718  fwddifnp1  36146  fzsplitnd  41963  lcmineqlem4  42013  lcmineqlem23  42032  dvrelogpow2b  42049  aks4d1p3  42059  aks4d1p7  42064  aks4d1p8  42068  aks4d1p9  42069  posbezout  42081  primrootspoweq0  42087  hashscontpow1  42102  aks6d1c2  42111  aks6d1c5lem1  42117  aks6d1c5lem3  42118  aks6d1c5lem2  42119  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem3  42153  bcled  42159  bcle2d  42160  aks6d1c7lem2  42162  unitscyglem2  42177  unitscyglem4  42179  unitscyglem5  42180  flt4lem3  42629  lzenom  42751  irrapxlem3  42805  pellexlem5  42814  rmspecnonsq  42888  congtr  42947  congmul  42949  congsym  42950  congrep  42955  acongrep  42962  acongeq  42965  dvdsacongtr  42966  jm2.18  42970  jm2.23  42978  jm2.20nn  42979  jm2.25  42981  jm2.26a  42982  jm2.26lem3  42983  jm2.27a  42987  jm2.27c  42989  jm3.1lem3  43001  jm3.1  43002  expdiophlem1  43003  hashnzfzclim  44304  binomcxplemnn0  44331  oddfl  45269  fmul01lt1lem2  45576  sumnnodd  45621  dvnmul  45934  dvnprodlem1  45937  dvnprodlem2  45938  stoweidlem26  46017  wallispilem4  46059  fourierdlem26  46124  fourierdlem41  46139  fourierdlem42  46140  fourierdlem48  46145  fouriersw  46222  elaa2lem  46224  etransclem3  46228  etransclem7  46232  etransclem10  46235  etransclem15  46240  etransclem20  46245  etransclem21  46246  etransclem22  46247  etransclem24  46249  etransclem25  46250  etransclem27  46252  etransclem35  46260  etransclem48  46273  upwordnul  46871  2elfz2melfz  47312  m1modne  47342  minusmod5ne  47343  submodlt  47344  goldbachthlem2  47540  2pwp1prm  47583  fppr2odd  47725  fpprwpprb  47734  gpgvtx0  48037  gpgvtx1  48038  gpgedgvtx1  48046  gpg3nbgrvtx0  48060  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  pgnbgreunbgrlem2lem3  48099  altgsumbcALT  48334  digexp  48589  dignn0flhalflem1  48597