Theorem zsubcld 12629

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

Syntax hints:   → wi 4   ∈ wcel 2119  (class class class)co 7356   − cmin 11368  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516

This theorem is referenced by:  eluzmn  12786  eluzsub  12809  uzsubsubfz  13491  fzm1  13552  eluzgtdifelfzo  13673  ubmelm1fzo  13709  elfznelfzo  13719  intfracq  13809  modsubdir  13893  modsumfzodifsn  13897  zesq  14179  bcval5  14271  ccatsymb  14536  swrdfv2  14615  ccatswrd  14622  cshwidxmod  14756  2cshwcshw  14778  cshwcsh2id  14781  fzomaxdiflem  15296  iseralt  15638  fsum0diaglem  15729  mptfzshft  15731  pwm1geoser  15825  mertenslem1  15840  fprodrev  15933  eirrlem  16162  fzocongeq  16284  3dvds  16291  modremain  16368  bitsfzolem  16394  bitsmod  16396  bitscmp  16398  bitsinv1lem  16401  sadaddlem  16426  bezoutlem3  16501  cncongr1  16627  hashdvds  16736  crth  16739  eulerthlem2  16743  prmdiveq  16747  modprm0  16767  pythagtriplem4  16781  pythagtriplem6  16783  pythagtriplem7  16784  pythagtriplem11  16787  pythagtriplem13  16789  pythagtriplem15  16791  pcqcl  16818  pcaddlem  16850  pcbc  16862  gzmulcl  16900  4sqlem5  16904  4sqlem8  16907  4sqlem11  16917  4sqlem12  16918  4sqlem14  16920  4sqlem16  16922  chnub  18579  mndodconglem  19507  sylow1lem1  19564  sylow1lem3  19566  gsummptshft  19902  ablsimpgfindlem1  20075  pzriprnglem10  21465  fermltlchr  21504  znf1o  21526  zdis  24800  plydivex  26281  aaliou3lem8  26329  basellem3  27064  bcmono  27258  bcmax  27259  bposlem1  27265  lgsmod  27304  lgsdirprm  27312  lgsqrlem2  27328  gausslemma2dlem0h  27344  gausslemma2dlem1a  27346  gausslemma2dlem5a  27351  lgseisenlem1  27356  lgseisenlem2  27357  lgsquadlem1  27361  2lgslem2  27376  2sqlem4  27402  2sqlem8  27407  2sqmod  27417  pntrlog2bndlem1  27558  crctcshwlkn0lem3  29898  crctcshwlkn0lem4  29899  crctcshwlkn0lem6  29901  crctcshwlkn0  29907  clwlkclwwlklem2a1  30080  clwlkclwwlklem2fv1  30083  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  fzspl  32881  fzsplit3  32885  ltesubnnd  32915  pfxlsw2ccat  33029  wrdt2ind  33032  swrdrn3  33034  cshwrnid  33040  cycpmco2lem6  33212  cycpmco2lem7  33213  archirngz  33270  znfermltl  33449  cos9thpiminplylem2  33967  smatrcl  33980  ballotlemfp1  34676  ballotlemimin  34690  ballotlemic  34691  ballotlem1c  34692  ballotlemfrceq  34713  ballotlemfrcn0  34714  signsplypnf  34734  signslema  34746  reprsuc  34799  breprexplema  34814  breprexplemc  34816  circlemeth  34824  revpfxsfxrev  35344  bcprod  35966  fwddifnp1  36393  fzsplitnd  42467  lcmineqlem4  42517  lcmineqlem23  42536  dvrelogpow2b  42553  aks4d1p3  42563  aks4d1p7  42568  aks4d1p8  42572  aks4d1p9  42573  posbezout  42585  primrootspoweq0  42591  hashscontpow1  42606  aks6d1c2  42615  aks6d1c5lem1  42621  aks6d1c5lem3  42622  aks6d1c5lem2  42623  sticksstones10  42640  sticksstones12a  42642  sticksstones12  42643  aks6d1c6lem3  42657  bcled  42663  bcle2d  42664  aks6d1c7lem2  42666  unitscyglem2  42681  unitscyglem4  42683  unitscyglem5  42684  flt4lem3  43098  lzenom  43219  irrapxlem3  43269  pellexlem5  43278  rmspecnonsq  43352  congtr  43410  congmul  43412  congsym  43413  congrep  43418  acongrep  43425  acongeq  43428  dvdsacongtr  43429  jm2.18  43433  jm2.23  43441  jm2.20nn  43442  jm2.25  43444  jm2.26a  43445  jm2.26lem3  43446  jm2.27a  43450  jm2.27c  43452  jm3.1lem3  43464  jm3.1  43465  expdiophlem1  43466  hashnzfzclim  44766  binomcxplemnn0  44793  oddfl  45726  fmul01lt1lem2  46030  sumnnodd  46075  dvnmul  46386  dvnprodlem1  46389  dvnprodlem2  46390  stoweidlem26  46469  wallispilem4  46511  fourierdlem26  46576  fourierdlem41  46591  fourierdlem42  46592  fourierdlem48  46597  fouriersw  46674  elaa2lem  46676  etransclem3  46680  etransclem7  46684  etransclem10  46687  etransclem15  46692  etransclem20  46697  etransclem21  46698  etransclem22  46699  etransclem24  46701  etransclem25  46702  etransclem27  46704  etransclem35  46712  etransclem48  46725  2elfz2melfz  47781  m1modne  47817  minusmod5ne  47818  submodlt  47819  goldbachthlem2  48024  2pwp1prm  48067  fppr2odd  48222  fpprwpprb  48231  gpgvtx0  48544  gpgvtx1  48545  gpgedgvtx1  48553  gpg3nbgrvtx0  48567  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  altgsumbcALT  48844  digexp  49098  dignn0flhalflem1  49106