Theorem subcld 9831

Description: Closure law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
negidd.1	|- ( ph -> A e. CC )
pncand.2	|- ( ph -> B e. CC )

Assertion

Ref	Expression
subcld	|- ( ph -> ( A - B ) e. CC )

Proof of Theorem subcld

Step	Hyp	Ref	Expression
1		negidd.1	. 2 |- ( ph -> A e. CC )
2		pncand.2	. 2 |- ( ph -> B e. CC )
3		subcl 9721	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
4	1, 2, 3	syl2anc 661	1 |- ( ph -> ( A - B ) e. CC )

Syntax hints:   -> wi 4   e. wcel 1758  (class class class)co 6201   CCcc 9392   - cmin 9707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483  ax-resscn 9451  ax-1cn 9452  ax-icn 9453  ax-addcl 9454  ax-addrcl 9455  ax-mulcl 9456  ax-mulrcl 9457  ax-mulcom 9458  ax-addass 9459  ax-mulass 9460  ax-distr 9461  ax-i2m1 9462  ax-1ne0 9463  ax-1rid 9464  ax-rnegex 9465  ax-rrecex 9466  ax-cnre 9467  ax-pre-lttri 9468  ax-pre-lttrn 9469  ax-pre-ltadd 9470

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-br 4402  df-opab 4460  df-mpt 4461  df-id 4745  df-po 4750  df-so 4751  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-riota 6162  df-ov 6204  df-oprab 6205  df-mpt2 6206  df-er 7212  df-en 7422  df-dom 7423  df-sdom 7424  df-pnf 9532  df-mnf 9533  df-ltxr 9535  df-sub 9709

This theorem is referenced by:  muleqadd  10092  hashfz  12307  hashfzo  12309  hashf1lem2  12328  hashf1  12329  ccatswrd  12469  crre  12722  remim  12725  remullem  12736  abs3lem  12945  caubnd2  12964  rlimuni  13147  climuni  13149  rlimcld2  13175  rlimrege0  13176  rlimrecl  13177  mulcn2  13192  reccn2  13193  cn1lem  13194  o1sub  13212  rlimo1  13213  o1dif  13226  rlimsqzlem  13245  caucvgrlem2  13271  iseralt  13281  fsumparts  13388  cvgcmpce  13400  incexclem  13418  arisum2  13442  geoserg  13447  geo2sum2  13453  sinf  13527  tanval2  13536  tanval3  13537  sinneg  13549  efival  13555  sinhval  13557  bitsinv1lem  13756  bitsres  13788  pythagtriplem1  14002  pythagtriplem14  14014  pythagtriplem17  14017  4sqlem5  14122  mul4sqlem  14133  4sqlem17  14141  vdwlem5  14165  vdwlem6  14166  vdwlem8  14168  blcvx  20508  recld2  20524  addcnlem  20573  cnllycmp  20661  ipcnlem2  20889  rrxmval  21037  rrxmetlem  21039  pjthlem1  21057  ovollb2lem  21104  itgcnlem  21401  dvlem  21505  dvconst  21525  dvid  21526  dvcnp2  21528  dvaddbr  21546  dvmulbr  21547  dvcobr  21554  dvcjbr  21557  dvrec  21563  dvmptim  21578  dvcnvlem  21582  dveflem  21585  dvsincos  21587  cmvth  21597  dvlip  21599  dvlipcn  21600  c1liplem1  21602  dveq0  21606  dv11cn  21607  dvle  21613  lhop1lem  21619  dvfsumabs  21629  dvfsumlem1  21632  dvfsumlem2  21633  dvfsumrlim  21637  dvfsumrlim2  21638  ftc1lem4  21645  ftc1lem5  21646  ftc2  21650  dgrcolem2  21875  plydiveu  21898  aaliou2b  21941  taylfvallem1  21956  taylply2  21967  dvtaylp  21969  dvntaylp  21970  taylthlem1  21972  taylthlem2  21973  ulmbdd  21997  ulmcn  21998  ulmdvlem1  21999  mtest  22003  iblulm  22006  itgulm  22007  abelthlem9  22039  ptolemy  22092  tangtx  22101  sineq0  22117  efeq1  22119  efif1olem4  22135  tanarg  22202  logcnlem3  22223  logcnlem4  22224  advlogexp  22234  efopn  22237  cxpcn3lem  22319  cxpeq  22329  ang180lem4  22342  ang180lem5  22343  ang180  22344  isosctrlem2  22351  isosctrlem3  22352  isosctr  22353  ssscongptld  22354  affineequiv  22355  affineequiv2  22356  angpieqvdlem  22357  angpieqvdlem2  22358  angpined  22359  angpieqvd  22360  chordthmlem  22361  chordthmlem2  22362  chordthmlem3  22363  chordthmlem4  22364  chordthmlem5  22365  heron  22367  quad2  22368  quad  22369  dcubic1lem  22372  dcubic  22375  mcubic  22376  cubic2  22377  cubic  22378  dquartlem1  22380  dquartlem2  22381  dquart  22382  quart1cl  22383  quart1lem  22384  quart1  22385  quartlem2  22387  quartlem4  22389  quart  22390  atanf  22409  sinasin  22418  asinsin  22421  atanneg  22436  atancj  22439  efiatan  22441  atanlogsub  22445  efiatan2  22446  2efiatan  22447  atanbndlem  22454  dvatan  22464  atantayl  22466  ftalem2  22545  logfacrlim  22697  logexprlim  22698  lgsdirprm  22802  vmadivsum  22865  rpvmasumlem  22870  dchrisumlem2  22873  dchrisumlem3  22874  dchrmusum2  22877  dchrvmasumlem2  22881  dchrvmasumlem3  22882  dchrvmasumiflem1  22884  rpvmasum2  22895  dchrisum0lem1b  22898  dchrisum0lem1  22899  dchrisum0lem2a  22900  rplogsum  22910  mudivsum  22913  mulogsumlem  22914  mulogsum  22915  mulog2sumlem1  22917  mulog2sumlem2  22918  mulog2sumlem3  22919  vmalogdivsum2  22921  vmalogdivsum  22922  2vmadivsumlem  22923  selberglem1  22928  selberglem2  22929  selberg2lem  22933  selberg2  22934  selberg3lem1  22940  selberg4lem1  22943  selberg4  22944  pntrsumo1  22948  selberg3r  22952  selberg34r  22954  pntrlog2bndlem1  22960  pntrlog2bndlem2  22961  pntrlog2bndlem3  22962  pntrlog2bndlem4  22963  pntrlog2bndlem5  22964  pntibndlem2  22974  pntlemf  22988  pntlemo  22990  ttgcontlem1  23284  brbtwn2  23304  colinearalglem1  23305  colinearalglem2  23306  colinearalg  23309  axsegconlem1  23316  ax5seglem2  23328  ax5seglem6  23333  ax5seglem9  23336  axlowdimlem17  23357  axcontlem7  23369  axcontlem8  23370  cusgrasizeinds  23537  smcnlem  24245  ipval2  24255  4ipval2  24256  4ipval3  24260  dipcj  24265  pjhthlem1  24947  lt2addrd  26188  bcm1n  26225  sqsscirc2  26485  signslema  27108  lgamgulmlem2  27161  lgamgulmlem3  27162  lgamgulmlem5  27164  lgamgulmlem6  27165  lgamgulm2  27167  lgamucov  27169  lgamcvg2  27186  gamcvg  27187  gamcvg2lem  27190  subfaclim  27221  pnpncand  27539  divcnvlin  27544  iprodgam  27651  fallfacfwd  27684  binomfallfaclem2  27688  bpolycl  28340  bpoly3  28346  bpoly4  28347  fsumcube  28348  ftc1cnnclem  28614  ftc1anclem7  28622  ftc1anclem8  28623  ftc1anc  28624  ftc2nc  28625  areacirclem1  28633  areacirclem4  28636  areacirc  28638  cntotbnd  28844  rencldnfilem  29308  pellexlem2  29320  pellexlem6  29324  pell1234qrne0  29343  pell1234qrmulcl  29345  rmyluc  29427  jm2.18  29486  jm2.19  29491  areaquad  29741  lhe4.4ex1a  29752  stoweidlem1  29945  stoweidlem11  29955  stoweidlem13  29957  stoweidlem26  29970  stoweid  30007  wallispi  30014  wallispi2lem1  30015  wallispi2lem2  30016  wallispi2  30017  stirlinglem1  30018  stirlinglem4  30021  stirlinglem5  30022  stirlinglem7  30024  stirlinglem11  30028  sigarmf  30039  sigarms  30041  sigarexp  30044  sigardiv  30046  sigarcol  30049  sharhght  30050  sigaradd  30051  cevathlem2  30053  cevath  30054  kcnktkm1cn  30319  clwlkisclwwlk  30600  frghash2spot  30805  usgreghash2spotv  30808  frgregordn0  30812  numclwlk3lem3  30815  numclwlk1lem2fo  30837  sinhpcosh  31404  i2linesd  31464  isosctrlem1ALT  32003  sineq0ALT  32006  bj-lineq  32936  bj-bary1lem  32938  bj-bary1lem1  32939  bj-bary1  32940