Theorem zsubcld 12725

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7431   − cmin 11490  ℤcz 12611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-n0 12525  df-z 12612

This theorem is referenced by:  eluzmn  12883  eluzsub  12906  uzsubsubfz  13583  fzm1  13644  eluzgtdifelfzo  13763  ubmelm1fzo  13799  elfznelfzo  13808  intfracq  13896  modsubdir  13978  modsumfzodifsn  13982  zesq  14262  bcval5  14354  ccatsymb  14617  swrdfv2  14696  ccatswrd  14703  cshwidxmod  14838  2cshwcshw  14861  cshwcsh2id  14864  fzomaxdiflem  15378  iseralt  15718  fsum0diaglem  15809  mptfzshft  15811  pwm1geoser  15902  mertenslem1  15917  fprodrev  16010  eirrlem  16237  fzocongeq  16358  3dvds  16365  modremain  16442  bitsfzolem  16468  bitsmod  16470  bitscmp  16472  bitsinv1lem  16475  sadaddlem  16500  bezoutlem3  16575  cncongr1  16701  hashdvds  16809  crth  16812  eulerthlem2  16816  prmdiveq  16820  modprm0  16839  pythagtriplem4  16853  pythagtriplem6  16855  pythagtriplem7  16856  pythagtriplem11  16859  pythagtriplem13  16861  pythagtriplem15  16863  pcqcl  16890  pcaddlem  16922  pcbc  16934  gzmulcl  16972  4sqlem5  16976  4sqlem8  16979  4sqlem11  16989  4sqlem12  16990  4sqlem14  16992  4sqlem16  16994  mndodconglem  19574  sylow1lem1  19631  sylow1lem3  19633  gsummptshft  19969  ablsimpgfindlem1  20142  pzriprnglem10  21519  fermltlchr  21562  znf1o  21588  zdis  24852  plydivex  26354  aaliou3lem8  26402  basellem3  27141  bcmono  27336  bcmax  27337  bposlem1  27343  lgsmod  27382  lgsdirprm  27390  lgsqrlem2  27406  gausslemma2dlem0h  27422  gausslemma2dlem1a  27424  gausslemma2dlem5a  27429  lgseisenlem1  27434  lgseisenlem2  27435  lgsquadlem1  27439  2lgslem2  27454  2sqlem4  27480  2sqlem8  27485  2sqmod  27495  pntrlog2bndlem1  27636  crctcshwlkn0lem3  29842  crctcshwlkn0lem4  29843  crctcshwlkn0lem6  29845  crctcshwlkn0  29851  clwlkclwwlklem2a1  30021  clwlkclwwlklem2fv1  30024  clwlkclwwlklem2a4  30026  clwlkclwwlklem2a  30027  fzspl  32798  fzsplit3  32802  ltesubnnd  32829  pfxlsw2ccat  32920  wrdt2ind  32923  swrdrn3  32925  cshwrnid  32931  chnub  32986  cycpmco2lem6  33134  cycpmco2lem7  33135  archirngz  33179  znfermltl  33374  smatrcl  33757  ballotlemfp1  34473  ballotlemimin  34487  ballotlemic  34488  ballotlem1c  34489  ballotlemfrceq  34510  ballotlemfrcn0  34511  signsplypnf  34544  signslema  34556  reprsuc  34609  breprexplema  34624  breprexplemc  34626  circlemeth  34634  revpfxsfxrev  35100  bcprod  35718  fwddifnp1  36147  fzsplitnd  41964  lcmineqlem4  42014  lcmineqlem23  42033  dvrelogpow2b  42050  aks4d1p3  42060  aks4d1p7  42065  aks4d1p8  42069  aks4d1p9  42070  posbezout  42082  primrootspoweq0  42088  hashscontpow1  42103  aks6d1c2  42112  aks6d1c5lem1  42118  aks6d1c5lem3  42119  aks6d1c5lem2  42120  sticksstones10  42137  sticksstones12a  42139  sticksstones12  42140  aks6d1c6lem3  42154  bcled  42160  bcle2d  42161  aks6d1c7lem2  42163  unitscyglem2  42178  unitscyglem4  42180  unitscyglem5  42181  metakunt1  42187  metakunt3  42189  metakunt7  42193  metakunt15  42201  metakunt16  42202  metakunt19  42205  metakunt21  42207  metakunt22  42208  metakunt24  42210  metakunt25  42211  metakunt27  42213  metakunt28  42214  metakunt29  42215  metakunt30  42216  metakunt32  42218  metakunt33  42219  flt4lem3  42635  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  44318  binomcxplemnn0  44345  oddfl  45228  fmul01lt1lem2  45541  sumnnodd  45586  dvnmul  45899  dvnprodlem1  45902  dvnprodlem2  45903  stoweidlem26  45982  wallispilem4  46024  fourierdlem26  46089  fourierdlem41  46104  fourierdlem42  46105  fourierdlem48  46110  fouriersw  46187  elaa2lem  46189  etransclem3  46193  etransclem7  46197  etransclem10  46200  etransclem15  46205  etransclem20  46210  etransclem21  46211  etransclem22  46212  etransclem24  46214  etransclem25  46215  etransclem27  46217  etransclem35  46225  etransclem48  46238  upwordnul  46834  2elfz2melfz  47268  m1modne  47288  minusmod5ne  47289  submodlt  47290  goldbachthlem2  47471  2pwp1prm  47514  fppr2odd  47656  fpprwpprb  47665  gpgvtx0  47944  gpgvtx1  47945  gpgedgvtx1  47955  gpg3nbgrvtx0  47967  altgsumbcALT  48198  digexp  48457  dignn0flhalflem1  48465