Theorem zsubcld 12710

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7413   − cmin 11474  ℤcz 12596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-resscn 11194  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-addrcl 11198  ax-mulcl 11199  ax-mulrcl 11200  ax-mulcom 11201  ax-addass 11202  ax-mulass 11203  ax-distr 11204  ax-i2m1 11205  ax-1ne0 11206  ax-1rid 11207  ax-rnegex 11208  ax-rrecex 11209  ax-cnre 11210  ax-pre-lttri 11211  ax-pre-lttrn 11212  ax-pre-ltadd 11213  ax-pre-mulgt0 11214

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7870  df-2nd 7997  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-er 8727  df-en 8968  df-dom 8969  df-sdom 8970  df-pnf 11279  df-mnf 11280  df-xr 11281  df-ltxr 11282  df-le 11283  df-sub 11476  df-neg 11477  df-nn 12249  df-n0 12510  df-z 12597

This theorem is referenced by:  eluzmn  12867  eluzsub  12890  uzsubsubfz  13568  fzm1  13629  eluzgtdifelfzo  13748  ubmelm1fzo  13784  elfznelfzo  13793  intfracq  13881  modsubdir  13963  modsumfzodifsn  13967  zesq  14247  bcval5  14339  ccatsymb  14602  swrdfv2  14681  ccatswrd  14688  cshwidxmod  14823  2cshwcshw  14846  cshwcsh2id  14849  fzomaxdiflem  15363  iseralt  15703  fsum0diaglem  15794  mptfzshft  15796  pwm1geoser  15887  mertenslem1  15902  fprodrev  15995  eirrlem  16222  fzocongeq  16343  3dvds  16350  modremain  16427  bitsfzolem  16453  bitsmod  16455  bitscmp  16457  bitsinv1lem  16460  sadaddlem  16485  bezoutlem3  16560  cncongr1  16686  hashdvds  16794  crth  16797  eulerthlem2  16801  prmdiveq  16805  modprm0  16825  pythagtriplem4  16839  pythagtriplem6  16841  pythagtriplem7  16842  pythagtriplem11  16845  pythagtriplem13  16847  pythagtriplem15  16849  pcqcl  16876  pcaddlem  16908  pcbc  16920  gzmulcl  16958  4sqlem5  16962  4sqlem8  16965  4sqlem11  16975  4sqlem12  16976  4sqlem14  16978  4sqlem16  16980  mndodconglem  19527  sylow1lem1  19584  sylow1lem3  19586  gsummptshft  19922  ablsimpgfindlem1  20095  pzriprnglem10  21463  fermltlchr  21502  znf1o  21524  zdis  24774  plydivex  26275  aaliou3lem8  26323  basellem3  27062  bcmono  27257  bcmax  27258  bposlem1  27264  lgsmod  27303  lgsdirprm  27311  lgsqrlem2  27327  gausslemma2dlem0h  27343  gausslemma2dlem1a  27345  gausslemma2dlem5a  27350  lgseisenlem1  27355  lgseisenlem2  27356  lgsquadlem1  27360  2lgslem2  27375  2sqlem4  27401  2sqlem8  27406  2sqmod  27416  pntrlog2bndlem1  27557  crctcshwlkn0lem3  29760  crctcshwlkn0lem4  29761  crctcshwlkn0lem6  29763  crctcshwlkn0  29769  clwlkclwwlklem2a1  29939  clwlkclwwlklem2fv1  29942  clwlkclwwlklem2a4  29944  clwlkclwwlklem2a  29945  fzspl  32730  fzsplit3  32734  ltesubnnd  32764  pfxlsw2ccat  32875  wrdt2ind  32878  swrdrn3  32880  cshwrnid  32886  chnub  32941  cycpmco2lem6  33090  cycpmco2lem7  33091  archirngz  33135  znfermltl  33329  smatrcl  33754  ballotlemfp1  34453  ballotlemimin  34467  ballotlemic  34468  ballotlem1c  34469  ballotlemfrceq  34490  ballotlemfrcn0  34491  signsplypnf  34524  signslema  34536  reprsuc  34589  breprexplema  34604  breprexplemc  34606  circlemeth  34614  revpfxsfxrev  35080  bcprod  35697  fwddifnp1  36125  fzsplitnd  41942  lcmineqlem4  41992  lcmineqlem23  42011  dvrelogpow2b  42028  aks4d1p3  42038  aks4d1p7  42043  aks4d1p8  42047  aks4d1p9  42048  posbezout  42060  primrootspoweq0  42066  hashscontpow1  42081  aks6d1c2  42090  aks6d1c5lem1  42096  aks6d1c5lem3  42097  aks6d1c5lem2  42098  sticksstones10  42115  sticksstones12a  42117  sticksstones12  42118  aks6d1c6lem3  42132  bcled  42138  bcle2d  42139  aks6d1c7lem2  42141  unitscyglem2  42156  unitscyglem4  42158  unitscyglem5  42159  metakunt1  42165  metakunt3  42167  metakunt7  42171  metakunt15  42179  metakunt16  42180  metakunt19  42183  metakunt21  42185  metakunt22  42186  metakunt24  42188  metakunt25  42189  metakunt27  42191  metakunt28  42192  metakunt29  42193  metakunt30  42194  metakunt32  42196  metakunt33  42197  flt4lem3  42621  lzenom  42744  irrapxlem3  42798  pellexlem5  42807  rmspecnonsq  42881  congtr  42940  congmul  42942  congsym  42943  congrep  42948  acongrep  42955  acongeq  42958  dvdsacongtr  42959  jm2.18  42963  jm2.23  42971  jm2.20nn  42972  jm2.25  42974  jm2.26a  42975  jm2.26lem3  42976  jm2.27a  42980  jm2.27c  42982  jm3.1lem3  42994  jm3.1  42995  expdiophlem1  42996  hashnzfzclim  44298  binomcxplemnn0  44325  oddfl  45246  fmul01lt1lem2  45557  sumnnodd  45602  dvnmul  45915  dvnprodlem1  45918  dvnprodlem2  45919  stoweidlem26  45998  wallispilem4  46040  fourierdlem26  46105  fourierdlem41  46120  fourierdlem42  46121  fourierdlem48  46126  fouriersw  46203  elaa2lem  46205  etransclem3  46209  etransclem7  46213  etransclem10  46216  etransclem15  46221  etransclem20  46226  etransclem21  46227  etransclem22  46228  etransclem24  46230  etransclem25  46231  etransclem27  46233  etransclem35  46241  etransclem48  46254  upwordnul  46852  2elfz2melfz  47288  m1modne  47308  minusmod5ne  47309  submodlt  47310  goldbachthlem2  47491  2pwp1prm  47534  fppr2odd  47676  fpprwpprb  47685  gpgvtx0  47966  gpgvtx1  47967  gpgedgvtx1  47978  gpg3nbgrvtx0  47990  altgsumbcALT  48227  digexp  48486  dignn0flhalflem1  48494