Theorem zsubcld 12643

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7387   − cmin 11405  ℤcz 12529

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-nn 12187  df-n0 12443  df-z 12530

This theorem is referenced by:  eluzmn  12800  eluzsub  12823  uzsubsubfz  13507  fzm1  13568  eluzgtdifelfzo  13688  ubmelm1fzo  13724  elfznelfzo  13733  intfracq  13821  modsubdir  13905  modsumfzodifsn  13909  zesq  14191  bcval5  14283  ccatsymb  14547  swrdfv2  14626  ccatswrd  14633  cshwidxmod  14768  2cshwcshw  14791  cshwcsh2id  14794  fzomaxdiflem  15309  iseralt  15651  fsum0diaglem  15742  mptfzshft  15744  pwm1geoser  15835  mertenslem1  15850  fprodrev  15943  eirrlem  16172  fzocongeq  16294  3dvds  16301  modremain  16378  bitsfzolem  16404  bitsmod  16406  bitscmp  16408  bitsinv1lem  16411  sadaddlem  16436  bezoutlem3  16511  cncongr1  16637  hashdvds  16745  crth  16748  eulerthlem2  16752  prmdiveq  16756  modprm0  16776  pythagtriplem4  16790  pythagtriplem6  16792  pythagtriplem7  16793  pythagtriplem11  16796  pythagtriplem13  16798  pythagtriplem15  16800  pcqcl  16827  pcaddlem  16859  pcbc  16871  gzmulcl  16909  4sqlem5  16913  4sqlem8  16916  4sqlem11  16926  4sqlem12  16927  4sqlem14  16929  4sqlem16  16931  mndodconglem  19471  sylow1lem1  19528  sylow1lem3  19530  gsummptshft  19866  ablsimpgfindlem1  20039  pzriprnglem10  21400  fermltlchr  21439  znf1o  21461  zdis  24705  plydivex  26205  aaliou3lem8  26253  basellem3  26993  bcmono  27188  bcmax  27189  bposlem1  27195  lgsmod  27234  lgsdirprm  27242  lgsqrlem2  27258  gausslemma2dlem0h  27274  gausslemma2dlem1a  27276  gausslemma2dlem5a  27281  lgseisenlem1  27286  lgseisenlem2  27287  lgsquadlem1  27291  2lgslem2  27306  2sqlem4  27332  2sqlem8  27337  2sqmod  27347  pntrlog2bndlem1  27488  crctcshwlkn0lem3  29742  crctcshwlkn0lem4  29743  crctcshwlkn0lem6  29745  crctcshwlkn0  29751  clwlkclwwlklem2a1  29921  clwlkclwwlklem2fv1  29924  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  fzspl  32712  fzsplit3  32716  ltesubnnd  32747  pfxlsw2ccat  32872  wrdt2ind  32875  swrdrn3  32877  cshwrnid  32883  chnub  32938  cycpmco2lem6  33088  cycpmco2lem7  33089  archirngz  33143  znfermltl  33337  cos9thpiminplylem2  33773  smatrcl  33786  ballotlemfp1  34483  ballotlemimin  34497  ballotlemic  34498  ballotlem1c  34499  ballotlemfrceq  34520  ballotlemfrcn0  34521  signsplypnf  34541  signslema  34553  reprsuc  34606  breprexplema  34621  breprexplemc  34623  circlemeth  34631  revpfxsfxrev  35103  bcprod  35725  fwddifnp1  36153  fzsplitnd  41970  lcmineqlem4  42020  lcmineqlem23  42039  dvrelogpow2b  42056  aks4d1p3  42066  aks4d1p7  42071  aks4d1p8  42075  aks4d1p9  42076  posbezout  42088  primrootspoweq0  42094  hashscontpow1  42109  aks6d1c2  42118  aks6d1c5lem1  42124  aks6d1c5lem3  42125  aks6d1c5lem2  42126  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  aks6d1c6lem3  42160  bcled  42166  bcle2d  42167  aks6d1c7lem2  42169  unitscyglem2  42184  unitscyglem4  42186  unitscyglem5  42187  flt4lem3  42636  lzenom  42758  irrapxlem3  42812  pellexlem5  42821  rmspecnonsq  42895  congtr  42954  congmul  42956  congsym  42957  congrep  42962  acongrep  42969  acongeq  42972  dvdsacongtr  42973  jm2.18  42977  jm2.23  42985  jm2.20nn  42986  jm2.25  42988  jm2.26a  42989  jm2.26lem3  42990  jm2.27a  42994  jm2.27c  42996  jm3.1lem3  43008  jm3.1  43009  expdiophlem1  43010  hashnzfzclim  44311  binomcxplemnn0  44338  oddfl  45276  fmul01lt1lem2  45583  sumnnodd  45628  dvnmul  45941  dvnprodlem1  45944  dvnprodlem2  45945  stoweidlem26  46024  wallispilem4  46066  fourierdlem26  46131  fourierdlem41  46146  fourierdlem42  46147  fourierdlem48  46152  fouriersw  46229  elaa2lem  46231  etransclem3  46235  etransclem7  46239  etransclem10  46242  etransclem15  46247  etransclem20  46252  etransclem21  46253  etransclem22  46254  etransclem24  46256  etransclem25  46257  etransclem27  46259  etransclem35  46267  etransclem48  46280  upwordnul  46878  2elfz2melfz  47319  m1modne  47349  minusmod5ne  47350  submodlt  47351  goldbachthlem2  47547  2pwp1prm  47590  fppr2odd  47732  fpprwpprb  47741  gpgvtx0  48044  gpgvtx1  48045  gpgedgvtx1  48053  gpg3nbgrvtx0  48067  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  altgsumbcALT  48341  digexp  48596  dignn0flhalflem1  48604