Theorem zsubcld 9574

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6001   − cmin 8317  ℤcz 9446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8090  ax-resscn 8091  ax-1cn 8092  ax-1re 8093  ax-icn 8094  ax-addcl 8095  ax-addrcl 8096  ax-mulcl 8097  ax-addcom 8099  ax-addass 8101  ax-distr 8103  ax-i2m1 8104  ax-0lt1 8105  ax-0id 8107  ax-rnegex 8108  ax-cnre 8110  ax-pre-ltirr 8111  ax-pre-ltwlin 8112  ax-pre-lttrn 8113  ax-pre-ltadd 8115

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-opab 4146  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-iota 5278  df-fun 5320  df-fv 5326  df-riota 5954  df-ov 6004  df-oprab 6005  df-mpo 6006  df-pnf 8183  df-mnf 8184  df-xr 8185  df-ltxr 8186  df-le 8187  df-sub 8319  df-neg 8320  df-inn 9111  df-n0 9370  df-z 9447

This theorem is referenced by:  eluzsub  9752  uzm1  9753  uzsubsubfz  10243  fzm1  10296  eluzgtdifelfzo  10403  ubmelm1fzo  10432  intfracq  10542  modqsubdir  10615  modsumfzodifsn  10618  addmodlteq  10620  uzennn  10658  seq3f1olemqsumkj  10733  zesq  10880  bcval5  10985  hashfz  11043  ccatlen  11130  ccatval2  11133  ccatvalfn  11136  ccatsymb  11137  swrdval  11180  swrdclg  11182  swrdlen  11184  swrdfv2  11195  swrdwrdsymbg  11196  swrdspsleq  11199  ccatswrd  11202  pfxval  11206  fnpfx  11209  wrdind  11254  wrd2ind  11255  pfxccatin12  11265  swrdccat  11267  seq3shft  11349  resqrexlemnmsq  11528  resqrexlemcvg  11530  fzomaxdiflem  11623  fsum0diaglem  11951  fisum0diag  11952  mptfzshft  11953  fsumrev  11954  fsumshft  11955  fisum0diag2  11958  geo2sum  12025  cvgratnnlemabsle  12038  cvgratnnlemsumlt  12039  cvgratz  12043  mertenslemub  12045  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  fprodshft  12129  fprodrev  12130  fprod0diagfz  12139  eirraplem  12288  dvdsaddre2b  12352  fzocongeq  12369  3dvds  12375  modremain  12440  bitsfzolem  12465  bitsmod  12467  bitscmp  12469  bitsinv1lem  12472  bezoutlemnewy  12517  uzwodc  12558  cncongr1  12625  prmind2  12642  pw2dvds  12688  hashdvds  12743  phiprmpw  12744  crth  12746  eulerthlemh  12753  eulerthlemth  12754  prmdiveq  12758  modprm0  12777  pythagtriplem2  12789  pythagtriplem4  12791  pythagtriplem6  12793  pythagtriplem7  12794  pythagtriplem11  12797  pythagtriplem13  12799  pythagtriplem15  12801  pythagtriplem16  12802  pythagtrip  12806  pceu  12818  pcdiv  12825  pcqcl  12829  pcaddlem  12862  pcbc  12874  gzmulcl  12901  4sqlem5  12905  4sqlem8  12908  4sqlemffi  12919  4sqleminfi  12920  4sqlem11  12924  4sqlem12  12925  4sqlem14  12927  4sqlem16  12929  zndvds  14613  znf1o  14615  plymullem1  15422  mersenne  15671  lgsval  15683  lgsfvalg  15684  lgsmod  15705  lgsdirprm  15713  gausslemma2dlem0h  15735  gausslemma2dlem1a  15737  gausslemma2dlem1cl  15738  gausslemma2dlem3  15742  gausslemma2dlem4  15743  gausslemma2dlem5a  15744  lgseisenlem1  15749  lgseisenlem2  15750  lgsquadlem1  15756  2lgslem2  15771  2sqlem4  15797  2sqlem8  15802  nconstwlpolemgt0  16432