Theorem zsubcld 12440

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7284   − cmin 11214  ℤcz 12328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-nn 11983  df-n0 12243  df-z 12329

This theorem is referenced by:  eluzmn  12598  uzsubsubfz  13287  fzm1  13345  eluzgtdifelfzo  13458  ubmelm1fzo  13492  elfznelfzo  13501  intfracq  13588  modsubdir  13669  modsumfzodifsn  13673  zesq  13950  bcval5  14041  ccatsymb  14296  swrdfv2  14383  ccatswrd  14390  cshwidxmod  14525  2cshwcshw  14547  cshwcsh2id  14550  fzomaxdiflem  15063  iseralt  15405  fsum0diaglem  15497  mptfzshft  15499  pwm1geoser  15590  mertenslem1  15605  fprodrev  15696  eirrlem  15922  fzocongeq  16042  3dvds  16049  modremain  16126  bitsfzolem  16150  bitsmod  16152  bitscmp  16154  bitsinv1lem  16157  sadaddlem  16182  bezoutlem3  16258  cncongr1  16381  hashdvds  16485  crth  16488  eulerthlem2  16492  prmdiveq  16496  modprm0  16515  pythagtriplem4  16529  pythagtriplem6  16531  pythagtriplem7  16532  pythagtriplem11  16535  pythagtriplem13  16537  pythagtriplem15  16539  pcqcl  16566  pcaddlem  16598  pcbc  16610  gzmulcl  16648  4sqlem5  16652  4sqlem8  16655  4sqlem11  16665  4sqlem12  16666  4sqlem14  16668  4sqlem16  16670  mndodconglem  19158  sylow1lem1  19212  sylow1lem3  19214  gsummptshft  19546  ablsimpgfindlem1  19719  znf1o  20768  zdis  23988  plydivex  25466  aaliou3lem8  25514  basellem3  26241  bcmono  26434  bcmax  26435  bposlem1  26441  lgsmod  26480  lgsdirprm  26488  lgsqrlem2  26504  gausslemma2dlem0h  26520  gausslemma2dlem1a  26522  gausslemma2dlem5a  26527  lgseisenlem1  26532  lgseisenlem2  26533  lgsquadlem1  26537  2lgslem2  26552  2sqlem4  26578  2sqlem8  26583  2sqmod  26593  pntrlog2bndlem1  26734  crctcshwlkn0lem3  28186  crctcshwlkn0lem4  28187  crctcshwlkn0lem6  28189  crctcshwlkn0  28195  clwlkclwwlklem2a1  28365  clwlkclwwlklem2fv1  28368  clwlkclwwlklem2a4  28370  clwlkclwwlklem2a  28371  fzspl  31120  fzsplit3  31124  ltesubnnd  31145  pfxlsw2ccat  31233  wrdt2ind  31234  swrdrn3  31236  cshwrnid  31242  cycpmco2lem6  31407  cycpmco2lem7  31408  archirngz  31452  znfermltl  31571  smatrcl  31755  ballotlemfp1  32467  ballotlemimin  32481  ballotlemic  32482  ballotlem1c  32483  ballotlemfrceq  32504  ballotlemfrcn0  32505  signsplypnf  32538  signslema  32550  reprsuc  32604  breprexplema  32619  breprexplemc  32621  circlemeth  32629  revpfxsfxrev  33086  bcprod  33713  fwddifnp1  34476  fzsplitnd  39998  lcmineqlem4  40047  lcmineqlem23  40066  dvrelogpow2b  40083  aks4d1p3  40093  aks4d1p7  40098  aks4d1p8  40102  aks4d1p9  40103  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  metakunt1  40132  metakunt3  40134  metakunt7  40138  metakunt15  40146  metakunt16  40147  metakunt19  40150  metakunt21  40152  metakunt22  40153  metakunt24  40155  metakunt25  40156  metakunt27  40158  metakunt28  40159  metakunt29  40160  metakunt30  40161  metakunt32  40163  metakunt33  40164  flt4lem3  40492  lzenom  40599  irrapxlem3  40653  pellexlem5  40662  rmspecnonsq  40736  congtr  40794  congmul  40796  congsym  40797  congrep  40802  acongrep  40809  acongeq  40812  dvdsacongtr  40813  jm2.18  40817  jm2.23  40825  jm2.20nn  40826  jm2.25  40828  jm2.26a  40829  jm2.26lem3  40830  jm2.27a  40834  jm2.27c  40836  jm3.1lem3  40848  jm3.1  40849  expdiophlem1  40850  hashnzfzclim  41947  binomcxplemnn0  41974  oddfl  42823  fmul01lt1lem2  43133  sumnnodd  43178  dvnmul  43491  dvnprodlem1  43494  dvnprodlem2  43495  stoweidlem26  43574  wallispilem4  43616  fourierdlem26  43681  fourierdlem41  43696  fourierdlem42  43697  fourierdlem48  43702  fouriersw  43779  elaa2lem  43781  etransclem3  43785  etransclem7  43789  etransclem10  43792  etransclem15  43797  etransclem20  43802  etransclem21  43803  etransclem22  43804  etransclem24  43806  etransclem25  43807  etransclem27  43809  etransclem35  43817  etransclem48  43830  2elfz2melfz  44821  goldbachthlem2  45009  2pwp1prm  45052  fppr2odd  45194  fpprwpprb  45203  altgsumbcALT  45700  digexp  45964  dignn0flhalflem1  45972  upwordnul  46526