MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zsubcld Structured version   Visualization version   GIF version

Theorem zsubcld 12081
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
StepHypRef Expression
1 zred.1 . 2 (𝜑𝐴 ∈ ℤ)
2 zaddcld.1 . 2 (𝜑𝐵 ∈ ℤ)
3 zsubcl 12013 . 2 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴𝐵) ∈ ℤ)
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴𝐵) ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  (class class class)co 7148  cmin 10859  cz 11970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-n0 11887  df-z 11971
This theorem is referenced by:  eluzmn  12239  uzsubsubfz  12919  fzm1  12977  eluzgtdifelfzo  13089  ubmelm1fzo  13123  elfznelfzo  13132  intfracq  13217  modsubdir  13298  modsumfzodifsn  13302  zesq  13577  bcval5  13668  ccatsymb  13926  swrdfv2  14013  ccatswrd  14020  cshwidxmod  14155  2cshwcshw  14177  cshwcsh2id  14180  fzomaxdiflem  14692  iseralt  15031  fsum0diaglem  15121  mptfzshft  15123  pwm1geoser  15214  mertenslem1  15230  eirrlem  15547  fzocongeq  15664  3dvds  15670  modremain  15749  bitsfzolem  15773  bitsmod  15775  bitscmp  15777  bitsinv1lem  15780  sadaddlem  15805  bezoutlem3  15879  cncongr1  16001  hashdvds  16102  crth  16105  eulerthlem2  16109  prmdiveq  16113  modprm0  16132  pythagtriplem4  16146  pythagtriplem6  16148  pythagtriplem7  16149  pythagtriplem11  16152  pythagtriplem13  16154  pythagtriplem15  16156  pcqcl  16183  pcaddlem  16214  pcbc  16226  gzmulcl  16264  4sqlem5  16268  4sqlem8  16271  4sqlem11  16281  4sqlem12  16282  4sqlem14  16284  4sqlem16  16286  mndodconglem  18589  sylow1lem1  18643  sylow1lem3  18645  gsummptshft  18976  ablsimpgfindlem1  19149  znf1o  20614  zdis  23339  plydivex  24801  aaliou3lem8  24849  basellem3  25574  bcmono  25767  bcmax  25768  bposlem1  25774  lgsmod  25813  lgsdirprm  25821  lgsqrlem2  25837  gausslemma2dlem0h  25853  gausslemma2dlem1a  25855  gausslemma2dlem5a  25860  lgseisenlem1  25865  lgseisenlem2  25866  lgsquadlem1  25870  2lgslem2  25885  2sqlem4  25911  2sqlem8  25916  2sqmod  25926  pntrlog2bndlem1  26067  crctcshwlkn0lem3  27504  crctcshwlkn0lem4  27505  crctcshwlkn0lem6  27507  crctcshwlkn0  27513  clwlkclwwlklem2a1  27684  clwlkclwwlklem2fv1  27687  clwlkclwwlklem2a4  27689  clwlkclwwlklem2a  27690  fzspl  30426  fzsplit3  30430  ltesubnnd  30452  pfxlsw2ccat  30540  wrdt2ind  30541  swrdrn3  30543  cshwrnid  30549  cycpmco2lem6  30687  cycpmco2lem7  30688  archirngz  30732  smatrcl  30947  ballotlemfp1  31635  ballotlemimin  31649  ballotlemic  31650  ballotlem1c  31651  ballotlemfrceq  31672  ballotlemfrcn0  31673  signsplypnf  31706  signslema  31718  reprsuc  31772  breprexplema  31787  breprexplemc  31789  circlemeth  31797  revpfxsfxrev  32246  bcprod  32854  fwddifnp1  33510  lzenom  39232  irrapxlem3  39286  pellexlem5  39295  rmspecnonsq  39369  congtr  39427  congmul  39429  congsym  39430  congrep  39435  acongrep  39442  acongeq  39445  dvdsacongtr  39446  jm2.18  39450  jm2.23  39458  jm2.20nn  39459  jm2.25  39461  jm2.26a  39462  jm2.26lem3  39463  jm2.27a  39467  jm2.27c  39469  jm3.1lem3  39481  jm3.1  39482  expdiophlem1  39483  hashnzfzclim  40519  binomcxplemnn0  40546  oddfl  41408  fmul01lt1lem2  41731  sumnnodd  41776  dvnmul  42093  dvnprodlem1  42096  dvnprodlem2  42097  stoweidlem26  42177  wallispilem4  42219  fourierdlem26  42284  fourierdlem41  42299  fourierdlem42  42300  fourierdlem48  42305  fouriersw  42382  elaa2lem  42384  etransclem3  42388  etransclem7  42392  etransclem10  42395  etransclem15  42400  etransclem20  42405  etransclem21  42406  etransclem22  42407  etransclem24  42409  etransclem25  42410  etransclem27  42412  etransclem35  42420  etransclem48  42433  2elfz2melfz  43384  goldbachthlem2  43540  2pwp1prm  43583  fppr2odd  43728  fpprwpprb  43737  altgsumbcALT  44233  digexp  44499  dignn0flhalflem1  44507
  Copyright terms: Public domain W3C validator