Theorem zsubcld 12832

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  (class class class)co 7440   − cmin 11565  ℤcz 12717

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300  ax-pre-mulgt0 11301

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-om 7899  df-2nd 8023  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-er 8742  df-en 8999  df-dom 9000  df-sdom 9001  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373  df-sub 11567  df-neg 11568  df-nn 12360  df-n0 12631  df-z 12718

This theorem is used by:  eluzmn  12996  eluzsub  13019  uzsubsubfz  13704  fzm1  13765  eluzgtdifelfzo  13886  ubmelm1fzo  13922  elfznelfzo  13932  intfracq  14023  modsubdir  14107  modsumfzodifsn  14111  zesq  14394  bcval5  14486  ccatsymb  14752  swrdrn3  14827  swrdfv2  14836  ccatswrd  14843  revpfxsfxrev  14942  cshwidxmod  14979  2cshwcshw  15001  cshwcsh2id  15004  fzomaxdiflem  15536  iseralt  15878  fsum0diaglem  15968  mptfzshft  15970  pwm1geoser  16064  mertenslem1  16079  fprodrev  16170  eirrlem  16398  fzocongeq  16520  3dvds  16527  modremain  16604  bitsfzolem  16630  bitsmod  16632  bitscmp  16634  bitsinv1lem  16637  sadaddlem  16662  bezoutlem3  16740  cncongr1  16868  hashdvds  16978  crth  16981  eulerthlem2  16985  prmdiveq  16989  modprm0  17009  pythagtriplem4  17023  pythagtriplem6  17025  pythagtriplem7  17026  pythagtriplem11  17029  pythagtriplem13  17031  pythagtriplem15  17033  pcqcl  17060  pcaddlem  17092  pcbc  17104  gzmulcl  17142  4sqlem5  17146  4sqlem8  17149  4sqlem11  17159  4sqlem12  17160  4sqlem14  17162  4sqlem16  17164  chnub  18822  mndodconglem  19782  sylow1lem1  19839  sylow1lem3  19841  gsummptshft  20177  ablsimpgfindlem1  20350  pzriprnglem10  21823  fermltlchr  21862  znf1o  21884  zdis  25163  plydivex  26645  aaliou3lem8  26699  basellem3  27437  bcmono  27631  bcmax  27632  bposlem1  27638  lgsmod  27677  lgsdirprm  27685  lgsqrlem2  27701  gausslemma2dlem0h  27717  gausslemma2dlem1a  27719  gausslemma2dlem5a  27724  lgseisenlem1  27729  lgseisenlem2  27730  lgsquadlem1  27734  2lgslem2  27749  2sqlem4  27775  2sqlem8  27780  2sqmod  27790  pntrlog2bndlem1  27931  flt4lem3  28005  crctcshwlkn0lem3  30428  crctcshwlkn0lem4  30429  crctcshwlkn0lem6  30431  crctcshwlkn0  30437  clwlkclwwlklem2a1  30610  clwlkclwwlklem2fv1  30613  clwlkclwwlklem2a4  30615  clwlkclwwlklem2a  30616  fzspl  33448  fzsplit3  33452  ltesubnnd  33481  pfxlsw2ccat  33580  wrdt2ind  33583  cshwrnid  33589  cycpmco2lem6  33759  cycpmco2lem7  33760  archirngz  33817  znfermltl  33989  cos9thpiminplylem2  34482  smatrcl  34495  ballotlemfp1  35191  ballotlemimin  35205  ballotlemic  35206  ballotlem1c  35207  ballotlemfrceq  35228  ballotlemfrcn0  35229  signsplypnf  35246  signslema  35258  reprsuc  35311  breprexplema  35326  breprexplemc  35328  circlemeth  35336  bcprod  36680  fwddifnp1  37107  fzsplitnd  43223  lcmineqlem4  43273  lcmineqlem23  43292  dvrelogpow2b  43309  aks4d1p3  43319  aks4d1p7  43324  aks4d1p8  43328  aks4d1p9  43329  posbezout  43341  primrootspoweq0  43347  hashscontpow1  43362  aks6d1c2  43371  aks6d1c5lem1  43377  aks6d1c5lem3  43378  aks6d1c5lem2  43379  sticksstones10  43396  sticksstones12a  43398  sticksstones12  43399  aks6d1c6lem3  43413  bcled  43419  bcle2d  43420  aks6d1c7lem2  43422  unitscyglem2  43437  unitscyglem4  43439  unitscyglem5  43440  lzenom  43972  irrapxlem3  44022  pellexlem5  44031  rmspecnonsq  44105  congtr  44163  congmul  44165  congsym  44166  congrep  44171  acongrep  44178  acongeq  44181  dvdsacongtr  44182  jm2.18  44186  jm2.23  44194  jm2.20nn  44195  jm2.25  44197  jm2.26a  44198  jm2.26lem3  44199  jm2.27a  44203  jm2.27c  44205  jm3.1lem3  44217  jm3.1  44218  expdiophlem1  44219  hashnzfzclim  45496  binomcxplemnn0  45523  oddfl  46497  fmul01lt1lem2  46800  sumnnodd  46845  dvnmul  47156  dvnprodlem1  47159  dvnprodlem2  47160  stoweidlem26  47239  wallispilem4  47281  fourierdlem26  47346  fourierdlem41  47361  fourierdlem42  47362  fourierdlem48  47367  fouriersw  47444  elaa2lem  47446  etransclem3  47450  etransclem7  47454  etransclem10  47457  etransclem15  47462  etransclem20  47467  etransclem21  47468  etransclem22  47469  etransclem24  47471  etransclem25  47472  etransclem27  47474  etransclem35  47482  etransclem48  47495  2elfz2melfz  48591  m1modne  48627  minusmod5ne  48628  submodlt  48629  goldbachthlem2  48834  2pwp1prm  48877  fppr2odd  49032  fpprwpprb  49041  gpgvtx0  49354  gpgvtx1  49355  gpgedgvtx1  49363  gpg3nbgrvtx0  49377  pgnbgreunbgrlem2lem1  49415  pgnbgreunbgrlem2lem2  49416  pgnbgreunbgrlem2lem3  49417  altgsumbcALT  49668  digexp  49922  dignn0flhalflem1  49930