Theorem subcld 9936

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 9824	. 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 1804  (class class class)co 6281   CCcc 9493   - cmin 9810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-po 4790  df-so 4791  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-ltxr 9636  df-sub 9812

This theorem is referenced by:  pnpncand  9988  muleqadd  10200  hashfz  12467  hashfzo  12469  hashf1lem2  12487  hashf1  12488  ccatswrd  12663  crre  12929  remim  12932  remullem  12943  abs3lem  13153  caubnd2  13172  rlimuni  13355  climuni  13357  rlimcld2  13383  rlimrege0  13384  rlimrecl  13385  mulcn2  13400  reccn2  13401  cn1lem  13402  o1sub  13420  rlimo1  13421  o1dif  13434  rlimsqzlem  13453  caucvgrlem2  13479  iseralt  13489  fsumparts  13602  cvgcmpce  13614  incexclem  13630  arisum2  13654  geoserg  13659  geo2sum2  13665  sinf  13841  tanval2  13850  tanval3  13851  sinneg  13863  efival  13869  sinhval  13871  bitsinv1lem  14073  bitsres  14105  pythagtriplem1  14322  pythagtriplem14  14334  pythagtriplem17  14337  4sqlem5  14442  mul4sqlem  14453  4sqlem17  14461  vdwlem5  14485  vdwlem6  14486  vdwlem8  14488  blcvx  21281  recld2  21297  addcnlem  21346  cnllycmp  21434  ipcnlem2  21662  rrxmval  21810  rrxmetlem  21812  pjthlem1  21830  ovollb2lem  21877  itgcnlem  22174  dvlem  22278  dvconst  22298  dvid  22299  dvcnp2  22301  dvaddbr  22319  dvmulbr  22320  dvcobr  22327  dvcjbr  22330  dvrec  22336  dvmptim  22351  dvcnvlem  22355  dveflem  22358  dvsincos  22360  cmvth  22370  dvlip  22372  dvlipcn  22373  c1liplem1  22375  dveq0  22379  dv11cn  22380  dvle  22386  lhop1lem  22392  dvfsumabs  22402  dvfsumlem1  22405  dvfsumlem2  22406  dvfsumrlim  22410  dvfsumrlim2  22411  ftc1lem4  22418  ftc1lem5  22419  ftc2  22423  dgrcolem2  22649  plydiveu  22672  aaliou2b  22715  taylfvallem1  22730  taylply2  22741  dvtaylp  22743  dvntaylp  22744  taylthlem1  22746  taylthlem2  22747  ulmbdd  22771  ulmcn  22772  ulmdvlem1  22773  mtest  22777  iblulm  22780  itgulm  22781  abelthlem9  22813  ptolemy  22867  tangtx  22876  sineq0  22892  efeq1  22894  efif1olem4  22910  tanarg  22982  logcnlem3  23003  logcnlem4  23004  advlogexp  23014  efopn  23017  cxpcn3lem  23099  cxpeq  23109  ang180lem4  23122  ang180lem5  23123  ang180  23124  isosctrlem2  23131  isosctrlem3  23132  isosctr  23133  ssscongptld  23134  affineequiv  23135  affineequiv2  23136  angpieqvdlem  23137  angpieqvdlem2  23138  angpined  23139  angpieqvd  23140  chordthmlem  23141  chordthmlem2  23142  chordthmlem3  23143  chordthmlem4  23144  chordthmlem5  23145  heron  23147  quad2  23148  quad  23149  dcubic1lem  23152  dcubic  23155  mcubic  23156  cubic2  23157  cubic  23158  dquartlem1  23160  dquartlem2  23161  dquart  23162  quart1cl  23163  quart1lem  23164  quart1  23165  quartlem2  23167  quartlem4  23169  quart  23170  atanf  23189  sinasin  23198  asinsin  23201  atanneg  23216  atancj  23219  efiatan  23221  atanlogsub  23225  efiatan2  23226  2efiatan  23227  atanbndlem  23234  dvatan  23244  atantayl  23246  ftalem2  23325  logfacrlim  23477  logexprlim  23478  lgsdirprm  23582  vmadivsum  23645  rpvmasumlem  23650  dchrisumlem2  23653  dchrisumlem3  23654  dchrmusum2  23657  dchrvmasumlem2  23661  dchrvmasumlem3  23662  dchrvmasumiflem1  23664  rpvmasum2  23675  dchrisum0lem1b  23678  dchrisum0lem1  23679  dchrisum0lem2a  23680  rplogsum  23690  mudivsum  23693  mulogsumlem  23694  mulogsum  23695  mulog2sumlem1  23697  mulog2sumlem2  23698  mulog2sumlem3  23699  vmalogdivsum2  23701  vmalogdivsum  23702  2vmadivsumlem  23703  selberglem1  23708  selberglem2  23709  selberg2lem  23713  selberg2  23714  selberg3lem1  23720  selberg4lem1  23723  selberg4  23724  pntrsumo1  23728  selberg3r  23732  selberg34r  23734  pntrlog2bndlem1  23740  pntrlog2bndlem2  23741  pntrlog2bndlem3  23742  pntrlog2bndlem4  23743  pntrlog2bndlem5  23744  pntibndlem2  23754  pntlemf  23768  pntlemo  23770  ttgcontlem1  24166  brbtwn2  24186  colinearalglem1  24187  colinearalglem2  24188  colinearalg  24191  axsegconlem1  24198  ax5seglem2  24210  ax5seglem6  24215  ax5seglem9  24218  axlowdimlem17  24239  axcontlem7  24251  axcontlem8  24252  cusgrasizeinds  24454  clwlkisclwwlk  24767  frghash2spot  25041  usgreghash2spotv  25044  frgregordn0  25048  numclwlk3lem3  25051  numclwlk1lem2fo  25073  smcnlem  25585  ipval2  25595  4ipval2  25596  4ipval3  25600  dipcj  25605  pjhthlem1  26287  lt2addrd  27541  bcm1n  27578  bhmafibid2  27611  2sqmod  27614  sqsscirc2  27869  signslema  28497  lgamgulmlem2  28550  lgamgulmlem3  28551  lgamgulmlem5  28553  lgamgulmlem6  28554  lgamgulm2  28556  lgamucov  28558  lgamcvg2  28575  gamcvg  28576  gamcvg2lem  28579  subfaclim  28610  divcnvlin  29096  iprodgam  29101  fallfacfwd  29134  binomfallfaclem2  29138  bpolycl  29790  bpoly3  29796  bpoly4  29797  fsumcube  29798  ftc1cnnclem  30064  ftc1anclem7  30072  ftc1anclem8  30073  ftc1anc  30074  ftc2nc  30075  areacirclem1  30083  areacirclem4  30086  areacirc  30088  cntotbnd  30268  rencldnfilem  30730  pellexlem2  30742  pellexlem6  30746  pell1234qrne0  30765  pell1234qrmulcl  30767  rmyluc  30849  jm2.18  30906  jm2.19  30911  areaquad  31160  lhe4.4ex1a  31210  oddfl  31413  dstregt0  31417  subadd4b  31418  sub31  31433  fzisoeu  31454  absnpncan2d  31456  absnpncan3d  31461  subdir2d  31465  mullimc  31576  ellimcabssub0  31577  mullimcf  31583  limcrecl  31589  lptre2pt  31600  limcleqr  31604  neglimc  31607  addlimc  31608  0ellimcdiv  31609  limclner  31611  reclimc  31613  fperdvper  31669  dvdivbd  31674  dvbdfbdioolem2  31680  ioodvbdlimc1lem1  31682  volioc  31725  stoweidlem1  31737  stoweidlem11  31747  stoweidlem13  31749  stoweidlem26  31762  stoweid  31799  wallispi  31806  wallispi2lem1  31807  wallispi2lem2  31808  wallispi2  31809  stirlinglem1  31810  stirlinglem4  31813  stirlinglem5  31814  stirlinglem7  31816  stirlinglem11  31820  dirkertrigeqlem2  31835  fourierdlem4  31847  fourierdlem26  31869  fourierdlem30  31873  fourierdlem42  31885  fourierdlem63  31906  fourierdlem65  31908  fourierdlem72  31915  fourierdlem74  31917  fourierdlem75  31918  fourierdlem76  31919  fourierdlem80  31923  fourierdlem81  31924  fourierdlem89  31932  fourierdlem90  31933  fourierdlem91  31934  fourierdlem107  31950  fourierdlem109  31952  fouriersw  31968  etransclem1  31972  etransclem4  31975  etransclem8  31979  etransclem18  31989  etransclem20  31991  etransclem21  31992  etransclem23  31994  etransclem35  32006  etransclem46  32017  sigarmf  32025  sigarms  32027  sigarexp  32030  sigardiv  32032  sigarcol  32035  sharhght  32036  sigaradd  32037  cevathlem2  32039  cevath  32040  sinhpcosh  33004  i2linesd  33064  isosctrlem1ALT  33602  sineq0ALT  33605  bj-lineq  34552  bj-bary1lem  34554  bj-bary1lem1  34555  bj-bary1  34556