Theorem zsubcld 12667

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 12600	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 − 𝐵) ∈ ℤ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7405   − cmin 11440  ℤcz 12554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-n0 12469  df-z 12555

This theorem is referenced by:  eluzmn  12825  eluzsub  12848  uzsubsubfz  13519  fzm1  13577  eluzgtdifelfzo  13690  ubmelm1fzo  13724  elfznelfzo  13733  intfracq  13820  modsubdir  13901  modsumfzodifsn  13905  zesq  14185  bcval5  14274  ccatsymb  14528  swrdfv2  14607  ccatswrd  14614  cshwidxmod  14749  2cshwcshw  14772  cshwcsh2id  14775  fzomaxdiflem  15285  iseralt  15627  fsum0diaglem  15718  mptfzshft  15720  pwm1geoser  15811  mertenslem1  15826  fprodrev  15917  eirrlem  16143  fzocongeq  16263  3dvds  16270  modremain  16347  bitsfzolem  16371  bitsmod  16373  bitscmp  16375  bitsinv1lem  16378  sadaddlem  16403  bezoutlem3  16479  cncongr1  16600  hashdvds  16704  crth  16707  eulerthlem2  16711  prmdiveq  16715  modprm0  16734  pythagtriplem4  16748  pythagtriplem6  16750  pythagtriplem7  16751  pythagtriplem11  16754  pythagtriplem13  16756  pythagtriplem15  16758  pcqcl  16785  pcaddlem  16817  pcbc  16829  gzmulcl  16867  4sqlem5  16871  4sqlem8  16874  4sqlem11  16884  4sqlem12  16885  4sqlem14  16887  4sqlem16  16889  mndodconglem  19403  sylow1lem1  19460  sylow1lem3  19462  gsummptshft  19798  ablsimpgfindlem1  19971  znf1o  21098  zdis  24323  plydivex  25801  aaliou3lem8  25849  basellem3  26576  bcmono  26769  bcmax  26770  bposlem1  26776  lgsmod  26815  lgsdirprm  26823  lgsqrlem2  26839  gausslemma2dlem0h  26855  gausslemma2dlem1a  26857  gausslemma2dlem5a  26862  lgseisenlem1  26867  lgseisenlem2  26868  lgsquadlem1  26872  2lgslem2  26887  2sqlem4  26913  2sqlem8  26918  2sqmod  26928  pntrlog2bndlem1  27069  crctcshwlkn0lem3  29055  crctcshwlkn0lem4  29056  crctcshwlkn0lem6  29058  crctcshwlkn0  29064  clwlkclwwlklem2a1  29234  clwlkclwwlklem2fv1  29237  clwlkclwwlklem2a4  29239  clwlkclwwlklem2a  29240  fzspl  31988  fzsplit3  31992  ltesubnnd  32015  pfxlsw2ccat  32103  wrdt2ind  32104  swrdrn3  32106  cshwrnid  32112  cycpmco2lem6  32277  cycpmco2lem7  32278  archirngz  32322  fermltlchr  32466  znfermltl  32467  smatrcl  32764  ballotlemfp1  33478  ballotlemimin  33492  ballotlemic  33493  ballotlem1c  33494  ballotlemfrceq  33515  ballotlemfrcn0  33516  signsplypnf  33549  signslema  33561  reprsuc  33615  breprexplema  33630  breprexplemc  33632  circlemeth  33640  revpfxsfxrev  34094  bcprod  34696  fwddifnp1  35125  fzsplitnd  40836  lcmineqlem4  40885  lcmineqlem23  40904  dvrelogpow2b  40921  aks4d1p3  40931  aks4d1p7  40936  aks4d1p8  40940  aks4d1p9  40941  sticksstones10  40959  sticksstones12a  40961  sticksstones12  40962  metakunt1  40973  metakunt3  40975  metakunt7  40979  metakunt15  40987  metakunt16  40988  metakunt19  40991  metakunt21  40993  metakunt22  40994  metakunt24  40996  metakunt25  40997  metakunt27  40999  metakunt28  41000  metakunt29  41001  metakunt30  41002  metakunt32  41004  metakunt33  41005  flt4lem3  41386  lzenom  41493  irrapxlem3  41547  pellexlem5  41556  rmspecnonsq  41630  congtr  41689  congmul  41691  congsym  41692  congrep  41697  acongrep  41704  acongeq  41707  dvdsacongtr  41708  jm2.18  41712  jm2.23  41720  jm2.20nn  41721  jm2.25  41723  jm2.26a  41724  jm2.26lem3  41725  jm2.27a  41729  jm2.27c  41731  jm3.1lem3  41743  jm3.1  41744  expdiophlem1  41745  hashnzfzclim  43066  binomcxplemnn0  43093  oddfl  43973  fmul01lt1lem2  44287  sumnnodd  44332  dvnmul  44645  dvnprodlem1  44648  dvnprodlem2  44649  stoweidlem26  44728  wallispilem4  44770  fourierdlem26  44835  fourierdlem41  44850  fourierdlem42  44851  fourierdlem48  44856  fouriersw  44933  elaa2lem  44935  etransclem3  44939  etransclem7  44943  etransclem10  44946  etransclem15  44951  etransclem20  44956  etransclem21  44957  etransclem22  44958  etransclem24  44960  etransclem25  44961  etransclem27  44963  etransclem35  44971  etransclem48  44984  upwordnul  45580  2elfz2melfz  46012  goldbachthlem2  46200  2pwp1prm  46243  fppr2odd  46385  fpprwpprb  46394  altgsumbcALT  46982  digexp  47246  dignn0flhalflem1  47254