Theorem zsubcld 12687

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

Syntax hints:   → wi 4   ∈ wcel 2099  (class class class)co 7414   − cmin 11460  ℤcz 12574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7732  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7863  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-er 8716  df-en 8954  df-dom 8955  df-sdom 8956  df-pnf 11266  df-mnf 11267  df-xr 11268  df-ltxr 11269  df-le 11270  df-sub 11462  df-neg 11463  df-nn 12229  df-n0 12489  df-z 12575

This theorem is referenced by:  eluzmn  12845  eluzsub  12868  uzsubsubfz  13541  fzm1  13599  eluzgtdifelfzo  13712  ubmelm1fzo  13746  elfznelfzo  13755  intfracq  13842  modsubdir  13923  modsumfzodifsn  13927  zesq  14206  bcval5  14295  ccatsymb  14550  swrdfv2  14629  ccatswrd  14636  cshwidxmod  14771  2cshwcshw  14794  cshwcsh2id  14797  fzomaxdiflem  15307  iseralt  15649  fsum0diaglem  15740  mptfzshft  15742  pwm1geoser  15833  mertenslem1  15848  fprodrev  15939  eirrlem  16166  fzocongeq  16286  3dvds  16293  modremain  16370  bitsfzolem  16394  bitsmod  16396  bitscmp  16398  bitsinv1lem  16401  sadaddlem  16426  bezoutlem3  16502  cncongr1  16623  hashdvds  16729  crth  16732  eulerthlem2  16736  prmdiveq  16740  modprm0  16759  pythagtriplem4  16773  pythagtriplem6  16775  pythagtriplem7  16776  pythagtriplem11  16779  pythagtriplem13  16781  pythagtriplem15  16783  pcqcl  16810  pcaddlem  16842  pcbc  16854  gzmulcl  16892  4sqlem5  16896  4sqlem8  16899  4sqlem11  16909  4sqlem12  16910  4sqlem14  16912  4sqlem16  16914  mndodconglem  19480  sylow1lem1  19537  sylow1lem3  19539  gsummptshft  19875  ablsimpgfindlem1  20048  pzriprnglem10  21396  fermltlchr  21439  znf1o  21465  zdis  24706  plydivex  26206  aaliou3lem8  26254  basellem3  26989  bcmono  27184  bcmax  27185  bposlem1  27191  lgsmod  27230  lgsdirprm  27238  lgsqrlem2  27254  gausslemma2dlem0h  27270  gausslemma2dlem1a  27272  gausslemma2dlem5a  27277  lgseisenlem1  27282  lgseisenlem2  27283  lgsquadlem1  27287  2lgslem2  27302  2sqlem4  27328  2sqlem8  27333  2sqmod  27343  pntrlog2bndlem1  27484  crctcshwlkn0lem3  29597  crctcshwlkn0lem4  29598  crctcshwlkn0lem6  29600  crctcshwlkn0  29606  clwlkclwwlklem2a1  29776  clwlkclwwlklem2fv1  29779  clwlkclwwlklem2a4  29781  clwlkclwwlklem2a  29782  fzspl  32529  fzsplit3  32533  ltesubnnd  32554  pfxlsw2ccat  32642  wrdt2ind  32643  swrdrn3  32645  cshwrnid  32651  cycpmco2lem6  32817  cycpmco2lem7  32818  archirngz  32862  znfermltl  33005  smatrcl  33320  ballotlemfp1  34034  ballotlemimin  34048  ballotlemic  34049  ballotlem1c  34050  ballotlemfrceq  34071  ballotlemfrcn0  34072  signsplypnf  34105  signslema  34117  reprsuc  34170  breprexplema  34185  breprexplemc  34187  circlemeth  34195  revpfxsfxrev  34648  bcprod  35255  fwddifnp1  35684  fzsplitnd  41377  lcmineqlem4  41427  lcmineqlem23  41446  dvrelogpow2b  41463  aks4d1p3  41473  aks4d1p7  41478  aks4d1p8  41482  aks4d1p9  41483  posbezout  41494  hashscontpow1  41512  aks6d1c2  41520  aks6d1c5lem1  41526  aks6d1c5lem3  41527  aks6d1c5lem2  41528  sticksstones10  41546  sticksstones12a  41548  sticksstones12  41549  aks6d1c6lem3  41563  metakunt1  41564  metakunt3  41566  metakunt7  41570  metakunt15  41578  metakunt16  41579  metakunt19  41582  metakunt21  41584  metakunt22  41585  metakunt24  41587  metakunt25  41588  metakunt27  41590  metakunt28  41591  metakunt29  41592  metakunt30  41593  metakunt32  41595  metakunt33  41596  flt4lem3  41984  lzenom  42102  irrapxlem3  42156  pellexlem5  42165  rmspecnonsq  42239  congtr  42298  congmul  42300  congsym  42301  congrep  42306  acongrep  42313  acongeq  42316  dvdsacongtr  42317  jm2.18  42321  jm2.23  42329  jm2.20nn  42330  jm2.25  42332  jm2.26a  42333  jm2.26lem3  42334  jm2.27a  42338  jm2.27c  42340  jm3.1lem3  42352  jm3.1  42353  expdiophlem1  42354  hashnzfzclim  43672  binomcxplemnn0  43699  oddfl  44572  fmul01lt1lem2  44886  sumnnodd  44931  dvnmul  45244  dvnprodlem1  45247  dvnprodlem2  45248  stoweidlem26  45327  wallispilem4  45369  fourierdlem26  45434  fourierdlem41  45449  fourierdlem42  45450  fourierdlem48  45455  fouriersw  45532  elaa2lem  45534  etransclem3  45538  etransclem7  45542  etransclem10  45545  etransclem15  45550  etransclem20  45555  etransclem21  45556  etransclem22  45557  etransclem24  45559  etransclem25  45560  etransclem27  45562  etransclem35  45570  etransclem48  45583  upwordnul  46179  2elfz2melfz  46611  goldbachthlem2  46799  2pwp1prm  46842  fppr2odd  46984  fpprwpprb  46993  altgsumbcALT  47330  digexp  47593  dignn0flhalflem1  47601