Theorem zsubcld 12711

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 595	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  (class class class)co 7412   − cmin 11447  ℤcz 12597

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7861  df-2nd 7985  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-rdg 8395  df-er 8692  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11449  df-neg 11450  df-nn 12240  df-n0 12511  df-z 12598

This theorem is used by:  eluzmn  12875  eluzsub  12898  uzsubsubfz  13581  fzm1  13642  eluzgtdifelfzo  13763  ubmelm1fzo  13799  elfznelfzo  13809  intfracq  13899  modsubdir  13983  modsumfzodifsn  13987  zesq  14269  bcval5  14361  ccatsymb  14627  swrdfv2  14706  ccatswrd  14713  cshwidxmod  14847  2cshwcshw  14869  cshwcsh2id  14872  fzomaxdiflem  15401  iseralt  15743  fsum0diaglem  15834  mptfzshft  15836  pwm1geoser  15930  mertenslem1  15945  fprodrev  16038  eirrlem  16266  fzocongeq  16388  3dvds  16395  modremain  16472  bitsfzolem  16498  bitsmod  16500  bitscmp  16502  bitsinv1lem  16505  sadaddlem  16530  bezoutlem3  16605  cncongr1  16731  hashdvds  16840  crth  16843  eulerthlem2  16847  prmdiveq  16851  modprm0  16871  pythagtriplem4  16885  pythagtriplem6  16887  pythagtriplem7  16888  pythagtriplem11  16891  pythagtriplem13  16893  pythagtriplem15  16895  pcqcl  16922  pcaddlem  16954  pcbc  16966  gzmulcl  17004  4sqlem5  17008  4sqlem8  17011  4sqlem11  17021  4sqlem12  17022  4sqlem14  17024  4sqlem16  17026  chnub  18684  mndodconglem  19617  sylow1lem1  19674  sylow1lem3  19676  gsummptshft  20012  ablsimpgfindlem1  20185  pzriprnglem10  21651  fermltlchr  21690  znf1o  21712  zdis  24985  plydivex  26469  aaliou3lem8  26519  basellem3  27258  bcmono  27452  bcmax  27453  bposlem1  27459  lgsmod  27498  lgsdirprm  27506  lgsqrlem2  27522  gausslemma2dlem0h  27538  gausslemma2dlem1a  27540  gausslemma2dlem5a  27545  lgseisenlem1  27550  lgseisenlem2  27551  lgsquadlem1  27555  2lgslem2  27570  2sqlem4  27596  2sqlem8  27601  2sqmod  27611  pntrlog2bndlem1  27752  crctcshwlkn0lem3  30172  crctcshwlkn0lem4  30173  crctcshwlkn0lem6  30175  crctcshwlkn0  30181  clwlkclwwlklem2a1  30354  clwlkclwwlklem2fv1  30357  clwlkclwwlklem2a4  30359  clwlkclwwlklem2a  30360  fzspl  33145  fzsplit3  33149  ltesubnnd  33178  pfxlsw2ccat  33279  wrdt2ind  33282  swrdrn3  33284  cshwrnid  33290  cycpmco2lem6  33460  cycpmco2lem7  33461  archirngz  33518  znfermltl  33690  cos9thpiminplylem2  34182  smatrcl  34195  ballotlemfp1  34891  ballotlemimin  34905  ballotlemic  34906  ballotlem1c  34907  ballotlemfrceq  34928  ballotlemfrcn0  34929  signsplypnf  34946  signslema  34958  reprsuc  35011  breprexplema  35026  breprexplemc  35028  circlemeth  35036  revpfxsfxrev  35615  bcprod  36238  fwddifnp1  36665  fzsplitnd  42777  lcmineqlem4  42827  lcmineqlem23  42846  dvrelogpow2b  42863  aks4d1p3  42873  aks4d1p7  42878  aks4d1p8  42882  aks4d1p9  42883  posbezout  42895  primrootspoweq0  42901  hashscontpow1  42916  aks6d1c2  42925  aks6d1c5lem1  42931  aks6d1c5lem3  42932  aks6d1c5lem2  42933  sticksstones10  42950  sticksstones12a  42952  sticksstones12  42953  aks6d1c6lem3  42967  bcled  42973  bcle2d  42974  aks6d1c7lem2  42976  unitscyglem2  42991  unitscyglem4  42993  unitscyglem5  42994  flt4lem3  43408  lzenom  43529  irrapxlem3  43579  pellexlem5  43588  rmspecnonsq  43662  congtr  43720  congmul  43722  congsym  43723  congrep  43728  acongrep  43735  acongeq  43738  dvdsacongtr  43739  jm2.18  43743  jm2.23  43751  jm2.20nn  43752  jm2.25  43754  jm2.26a  43755  jm2.26lem3  43756  jm2.27a  43760  jm2.27c  43762  jm3.1lem3  43774  jm3.1  43775  expdiophlem1  43776  hashnzfzclim  45060  binomcxplemnn0  45087  oddfl  46025  fmul01lt1lem2  46329  sumnnodd  46374  dvnmul  46685  dvnprodlem1  46688  dvnprodlem2  46689  stoweidlem26  46768  wallispilem4  46810  fourierdlem26  46875  fourierdlem41  46890  fourierdlem42  46891  fourierdlem48  46896  fouriersw  46973  elaa2lem  46975  etransclem3  46979  etransclem7  46983  etransclem10  46986  etransclem15  46991  etransclem20  46996  etransclem21  46997  etransclem22  46998  etransclem24  47000  etransclem25  47001  etransclem27  47003  etransclem35  47011  etransclem48  47024  2elfz2melfz  48083  m1modne  48119  minusmod5ne  48120  submodlt  48121  goldbachthlem2  48326  2pwp1prm  48369  fppr2odd  48524  fpprwpprb  48533  gpgvtx0  48846  gpgvtx1  48847  gpgedgvtx1  48855  gpg3nbgrvtx0  48869  pgnbgreunbgrlem2lem1  48907  pgnbgreunbgrlem2lem2  48908  pgnbgreunbgrlem2lem3  48909  altgsumbcALT  49161  digexp  49415  dignn0flhalflem1  49423