Theorem zsubcld 12605

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7360   − cmin 11368  ℤcz 12492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106  ax-pre-mulgt0 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12150  df-n0 12406  df-z 12493

This theorem is referenced by:  eluzmn  12762  eluzsub  12785  uzsubsubfz  13466  fzm1  13527  eluzgtdifelfzo  13647  ubmelm1fzo  13683  elfznelfzo  13693  intfracq  13783  modsubdir  13867  modsumfzodifsn  13871  zesq  14153  bcval5  14245  ccatsymb  14510  swrdfv2  14589  ccatswrd  14596  cshwidxmod  14730  2cshwcshw  14752  cshwcsh2id  14755  fzomaxdiflem  15270  iseralt  15612  fsum0diaglem  15703  mptfzshft  15705  pwm1geoser  15796  mertenslem1  15811  fprodrev  15904  eirrlem  16133  fzocongeq  16255  3dvds  16262  modremain  16339  bitsfzolem  16365  bitsmod  16367  bitscmp  16369  bitsinv1lem  16372  sadaddlem  16397  bezoutlem3  16472  cncongr1  16598  hashdvds  16706  crth  16709  eulerthlem2  16713  prmdiveq  16717  modprm0  16737  pythagtriplem4  16751  pythagtriplem6  16753  pythagtriplem7  16754  pythagtriplem11  16757  pythagtriplem13  16759  pythagtriplem15  16761  pcqcl  16788  pcaddlem  16820  pcbc  16832  gzmulcl  16870  4sqlem5  16874  4sqlem8  16877  4sqlem11  16887  4sqlem12  16888  4sqlem14  16890  4sqlem16  16892  chnub  18549  mndodconglem  19474  sylow1lem1  19531  sylow1lem3  19533  gsummptshft  19869  ablsimpgfindlem1  20042  pzriprnglem10  21449  fermltlchr  21488  znf1o  21510  zdis  24765  plydivex  26265  aaliou3lem8  26313  basellem3  27053  bcmono  27248  bcmax  27249  bposlem1  27255  lgsmod  27294  lgsdirprm  27302  lgsqrlem2  27318  gausslemma2dlem0h  27334  gausslemma2dlem1a  27336  gausslemma2dlem5a  27341  lgseisenlem1  27346  lgseisenlem2  27347  lgsquadlem1  27351  2lgslem2  27366  2sqlem4  27392  2sqlem8  27397  2sqmod  27407  pntrlog2bndlem1  27548  crctcshwlkn0lem3  29889  crctcshwlkn0lem4  29890  crctcshwlkn0lem6  29892  crctcshwlkn0  29898  clwlkclwwlklem2a1  30071  clwlkclwwlklem2fv1  30074  clwlkclwwlklem2a4  30076  clwlkclwwlklem2a  30077  fzspl  32871  fzsplit3  32875  ltesubnnd  32905  pfxlsw2ccat  33034  wrdt2ind  33037  swrdrn3  33039  cshwrnid  33045  cycpmco2lem6  33215  cycpmco2lem7  33216  archirngz  33273  znfermltl  33449  cos9thpiminplylem2  33942  smatrcl  33955  ballotlemfp1  34651  ballotlemimin  34665  ballotlemic  34666  ballotlem1c  34667  ballotlemfrceq  34688  ballotlemfrcn0  34689  signsplypnf  34709  signslema  34721  reprsuc  34774  breprexplema  34789  breprexplemc  34791  circlemeth  34799  revpfxsfxrev  35312  bcprod  35934  fwddifnp1  36361  fzsplitnd  42304  lcmineqlem4  42354  lcmineqlem23  42373  dvrelogpow2b  42390  aks4d1p3  42400  aks4d1p7  42405  aks4d1p8  42409  aks4d1p9  42410  posbezout  42422  primrootspoweq0  42428  hashscontpow1  42443  aks6d1c2  42452  aks6d1c5lem1  42458  aks6d1c5lem3  42459  aks6d1c5lem2  42460  sticksstones10  42477  sticksstones12a  42479  sticksstones12  42480  aks6d1c6lem3  42494  bcled  42500  bcle2d  42501  aks6d1c7lem2  42503  unitscyglem2  42518  unitscyglem4  42520  unitscyglem5  42521  flt4lem3  42958  lzenom  43079  irrapxlem3  43133  pellexlem5  43142  rmspecnonsq  43216  congtr  43274  congmul  43276  congsym  43277  congrep  43282  acongrep  43289  acongeq  43292  dvdsacongtr  43293  jm2.18  43297  jm2.23  43305  jm2.20nn  43306  jm2.25  43308  jm2.26a  43309  jm2.26lem3  43310  jm2.27a  43314  jm2.27c  43316  jm3.1lem3  43328  jm3.1  43329  expdiophlem1  43330  hashnzfzclim  44630  binomcxplemnn0  44657  oddfl  45593  fmul01lt1lem2  45898  sumnnodd  45943  dvnmul  46254  dvnprodlem1  46257  dvnprodlem2  46258  stoweidlem26  46337  wallispilem4  46379  fourierdlem26  46444  fourierdlem41  46459  fourierdlem42  46460  fourierdlem48  46465  fouriersw  46542  elaa2lem  46544  etransclem3  46548  etransclem7  46552  etransclem10  46555  etransclem15  46560  etransclem20  46565  etransclem21  46566  etransclem22  46567  etransclem24  46569  etransclem25  46570  etransclem27  46572  etransclem35  46580  etransclem48  46593  2elfz2melfz  47631  m1modne  47661  minusmod5ne  47662  submodlt  47663  goldbachthlem2  47859  2pwp1prm  47902  fppr2odd  48044  fpprwpprb  48053  gpgvtx0  48366  gpgvtx1  48367  gpgedgvtx1  48375  gpg3nbgrvtx0  48389  pgnbgreunbgrlem2lem1  48427  pgnbgreunbgrlem2lem2  48428  pgnbgreunbgrlem2lem3  48429  altgsumbcALT  48666  digexp  48920  dignn0flhalflem1  48928