Theorem zsubcld 12808

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  (class class class)co 7420   − cmin 11541  ℤcz 12693

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-nn 12336  df-n0 12607  df-z 12694

This theorem is used by:  eluzmn  12972  eluzsub  12995  uzsubsubfz  13680  fzm1  13741  eluzgtdifelfzo  13862  ubmelm1fzo  13898  elfznelfzo  13908  intfracq  13999  modsubdir  14083  modsumfzodifsn  14087  zesq  14370  bcval5  14462  ccatsymb  14728  swrdrn3  14802  swrdfv2  14811  ccatswrd  14818  revpfxsfxrev  14917  cshwidxmod  14954  2cshwcshw  14976  cshwcsh2id  14979  fzomaxdiflem  15510  iseralt  15852  fsum0diaglem  15942  mptfzshft  15944  pwm1geoser  16038  mertenslem1  16053  fprodrev  16144  eirrlem  16372  fzocongeq  16494  3dvds  16501  modremain  16578  bitsfzolem  16604  bitsmod  16606  bitscmp  16608  bitsinv1lem  16611  sadaddlem  16636  bezoutlem3  16714  cncongr1  16842  hashdvds  16952  crth  16955  eulerthlem2  16959  prmdiveq  16963  modprm0  16983  pythagtriplem4  16997  pythagtriplem6  16999  pythagtriplem7  17000  pythagtriplem11  17003  pythagtriplem13  17005  pythagtriplem15  17007  pcqcl  17034  pcaddlem  17066  pcbc  17078  gzmulcl  17116  4sqlem5  17120  4sqlem8  17123  4sqlem11  17133  4sqlem12  17134  4sqlem14  17136  4sqlem16  17138  chnub  18796  mndodconglem  19755  sylow1lem1  19812  sylow1lem3  19814  gsummptshft  20150  ablsimpgfindlem1  20323  pzriprnglem10  21796  fermltlchr  21835  znf1o  21857  zdis  25136  plydivex  26618  aaliou3lem8  26672  basellem3  27410  bcmono  27604  bcmax  27605  bposlem1  27611  lgsmod  27650  lgsdirprm  27658  lgsqrlem2  27674  gausslemma2dlem0h  27690  gausslemma2dlem1a  27692  gausslemma2dlem5a  27697  lgseisenlem1  27702  lgseisenlem2  27703  lgsquadlem1  27707  2lgslem2  27722  2sqlem4  27748  2sqlem8  27753  2sqmod  27763  pntrlog2bndlem1  27904  flt4lem3  27978  crctcshwlkn0lem3  30401  crctcshwlkn0lem4  30402  crctcshwlkn0lem6  30404  crctcshwlkn0  30410  clwlkclwwlklem2a1  30583  clwlkclwwlklem2fv1  30586  clwlkclwwlklem2a4  30588  clwlkclwwlklem2a  30589  fzspl  33381  fzsplit3  33385  ltesubnnd  33414  pfxlsw2ccat  33513  wrdt2ind  33516  cshwrnid  33522  cycpmco2lem6  33692  cycpmco2lem7  33693  archirngz  33750  znfermltl  33922  cos9thpiminplylem2  34415  smatrcl  34428  ballotlemfp1  35124  ballotlemimin  35138  ballotlemic  35139  ballotlem1c  35140  ballotlemfrceq  35161  ballotlemfrcn0  35162  signsplypnf  35179  signslema  35191  reprsuc  35244  breprexplema  35259  breprexplemc  35261  circlemeth  35269  bcprod  36503  fwddifnp1  36930  fzsplitnd  43033  lcmineqlem4  43083  lcmineqlem23  43102  dvrelogpow2b  43119  aks4d1p3  43129  aks4d1p7  43134  aks4d1p8  43138  aks4d1p9  43139  posbezout  43151  primrootspoweq0  43157  hashscontpow1  43172  aks6d1c2  43181  aks6d1c5lem1  43187  aks6d1c5lem3  43188  aks6d1c5lem2  43189  sticksstones10  43206  sticksstones12a  43208  sticksstones12  43209  aks6d1c6lem3  43223  bcled  43229  bcle2d  43230  aks6d1c7lem2  43232  unitscyglem2  43247  unitscyglem4  43249  unitscyglem5  43250  lzenom  43781  irrapxlem3  43831  pellexlem5  43840  rmspecnonsq  43914  congtr  43972  congmul  43974  congsym  43975  congrep  43980  acongrep  43987  acongeq  43990  dvdsacongtr  43991  jm2.18  43995  jm2.23  44003  jm2.20nn  44004  jm2.25  44006  jm2.26a  44007  jm2.26lem3  44008  jm2.27a  44012  jm2.27c  44014  jm3.1lem3  44026  jm3.1  44027  expdiophlem1  44028  hashnzfzclim  45306  binomcxplemnn0  45333  oddfl  46294  fmul01lt1lem2  46597  sumnnodd  46642  dvnmul  46953  dvnprodlem1  46956  dvnprodlem2  46957  stoweidlem26  47036  wallispilem4  47078  fourierdlem26  47143  fourierdlem41  47158  fourierdlem42  47159  fourierdlem48  47164  fouriersw  47241  elaa2lem  47243  etransclem3  47247  etransclem7  47251  etransclem10  47254  etransclem15  47259  etransclem20  47264  etransclem21  47265  etransclem22  47266  etransclem24  47268  etransclem25  47269  etransclem27  47271  etransclem35  47279  etransclem48  47292  2elfz2melfz  48388  m1modne  48424  minusmod5ne  48425  submodlt  48426  goldbachthlem2  48631  2pwp1prm  48674  fppr2odd  48829  fpprwpprb  48838  gpgvtx0  49151  gpgvtx1  49152  gpgedgvtx1  49160  gpg3nbgrvtx0  49174  pgnbgreunbgrlem2lem1  49212  pgnbgreunbgrlem2lem2  49213  pgnbgreunbgrlem2lem3  49214  altgsumbcALT  49465  digexp  49719  dignn0flhalflem1  49727