Theorem zsubcld 12752

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7448   − cmin 11520  ℤcz 12639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-n0 12554  df-z 12640

This theorem is referenced by:  eluzmn  12910  eluzsub  12933  uzsubsubfz  13606  fzm1  13664  eluzgtdifelfzo  13778  ubmelm1fzo  13813  elfznelfzo  13822  intfracq  13910  modsubdir  13991  modsumfzodifsn  13995  zesq  14275  bcval5  14367  ccatsymb  14630  swrdfv2  14709  ccatswrd  14716  cshwidxmod  14851  2cshwcshw  14874  cshwcsh2id  14877  fzomaxdiflem  15391  iseralt  15733  fsum0diaglem  15824  mptfzshft  15826  pwm1geoser  15917  mertenslem1  15932  fprodrev  16025  eirrlem  16252  fzocongeq  16372  3dvds  16379  modremain  16456  bitsfzolem  16480  bitsmod  16482  bitscmp  16484  bitsinv1lem  16487  sadaddlem  16512  bezoutlem3  16588  cncongr1  16714  hashdvds  16822  crth  16825  eulerthlem2  16829  prmdiveq  16833  modprm0  16852  pythagtriplem4  16866  pythagtriplem6  16868  pythagtriplem7  16869  pythagtriplem11  16872  pythagtriplem13  16874  pythagtriplem15  16876  pcqcl  16903  pcaddlem  16935  pcbc  16947  gzmulcl  16985  4sqlem5  16989  4sqlem8  16992  4sqlem11  17002  4sqlem12  17003  4sqlem14  17005  4sqlem16  17007  mndodconglem  19583  sylow1lem1  19640  sylow1lem3  19642  gsummptshft  19978  ablsimpgfindlem1  20151  pzriprnglem10  21524  fermltlchr  21567  znf1o  21593  zdis  24857  plydivex  26357  aaliou3lem8  26405  basellem3  27144  bcmono  27339  bcmax  27340  bposlem1  27346  lgsmod  27385  lgsdirprm  27393  lgsqrlem2  27409  gausslemma2dlem0h  27425  gausslemma2dlem1a  27427  gausslemma2dlem5a  27432  lgseisenlem1  27437  lgseisenlem2  27438  lgsquadlem1  27442  2lgslem2  27457  2sqlem4  27483  2sqlem8  27488  2sqmod  27498  pntrlog2bndlem1  27639  crctcshwlkn0lem3  29845  crctcshwlkn0lem4  29846  crctcshwlkn0lem6  29848  crctcshwlkn0  29854  clwlkclwwlklem2a1  30024  clwlkclwwlklem2fv1  30027  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  fzspl  32795  fzsplit3  32799  ltesubnnd  32826  pfxlsw2ccat  32917  wrdt2ind  32920  swrdrn3  32922  cshwrnid  32928  chnub  32984  cycpmco2lem6  33124  cycpmco2lem7  33125  archirngz  33169  znfermltl  33359  smatrcl  33742  ballotlemfp1  34456  ballotlemimin  34470  ballotlemic  34471  ballotlem1c  34472  ballotlemfrceq  34493  ballotlemfrcn0  34494  signsplypnf  34527  signslema  34539  reprsuc  34592  breprexplema  34607  breprexplemc  34609  circlemeth  34617  revpfxsfxrev  35083  bcprod  35700  fwddifnp1  36129  fzsplitnd  41939  lcmineqlem4  41989  lcmineqlem23  42008  dvrelogpow2b  42025  aks4d1p3  42035  aks4d1p7  42040  aks4d1p8  42044  aks4d1p9  42045  posbezout  42057  primrootspoweq0  42063  hashscontpow1  42078  aks6d1c2  42087  aks6d1c5lem1  42093  aks6d1c5lem3  42094  aks6d1c5lem2  42095  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  aks6d1c6lem3  42129  bcled  42135  bcle2d  42136  aks6d1c7lem2  42138  unitscyglem2  42153  unitscyglem4  42155  unitscyglem5  42156  metakunt1  42162  metakunt3  42164  metakunt7  42168  metakunt15  42176  metakunt16  42177  metakunt19  42180  metakunt21  42182  metakunt22  42183  metakunt24  42185  metakunt25  42186  metakunt27  42188  metakunt28  42189  metakunt29  42190  metakunt30  42191  metakunt32  42193  metakunt33  42194  flt4lem3  42603  lzenom  42726  irrapxlem3  42780  pellexlem5  42789  rmspecnonsq  42863  congtr  42922  congmul  42924  congsym  42925  congrep  42930  acongrep  42937  acongeq  42940  dvdsacongtr  42941  jm2.18  42945  jm2.23  42953  jm2.20nn  42954  jm2.25  42956  jm2.26a  42957  jm2.26lem3  42958  jm2.27a  42962  jm2.27c  42964  jm3.1lem3  42976  jm3.1  42977  expdiophlem1  42978  hashnzfzclim  44291  binomcxplemnn0  44318  oddfl  45192  fmul01lt1lem2  45506  sumnnodd  45551  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  stoweidlem26  45947  wallispilem4  45989  fourierdlem26  46054  fourierdlem41  46069  fourierdlem42  46070  fourierdlem48  46075  fouriersw  46152  elaa2lem  46154  etransclem3  46158  etransclem7  46162  etransclem10  46165  etransclem15  46170  etransclem20  46175  etransclem21  46176  etransclem22  46177  etransclem24  46179  etransclem25  46180  etransclem27  46182  etransclem35  46190  etransclem48  46203  upwordnul  46799  2elfz2melfz  47233  goldbachthlem2  47420  2pwp1prm  47463  fppr2odd  47605  fpprwpprb  47614  altgsumbcALT  48078  digexp  48341  dignn0flhalflem1  48349