Theorem subcld 10011

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 9899	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
4	1, 2, 3	syl2anc 671	1 |- ( ph -> ( A - B ) e. CC )

Syntax hints:   -> wi 4   e. wcel 1897  (class class class)co 6314   CCcc 9562   - cmin 9885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-po 4773  df-so 4774  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-er 7388  df-en 7595  df-dom 7596  df-sdom 7597  df-pnf 9702  df-mnf 9703  df-ltxr 9705  df-sub 9887

This theorem is referenced by:  pnpncand  10068  muleqadd  10283  hashfz  12631  hashfzo  12633  hashf1lem2  12651  hashf1  12652  ccatswrd  12848  crre  13225  remim  13228  remullem  13239  abs3lem  13449  caubnd2  13468  rlimuni  13662  climuni  13664  rlimcld2  13690  rlimrege0  13691  rlimrecl  13692  mulcn2  13707  reccn2  13708  cn1lem  13709  o1sub  13727  rlimo1  13728  o1dif  13741  rlimsqzlem  13760  caucvgrlem2  13788  iseralt  13799  fsumparts  13914  cvgcmpce  13926  incexclem  13942  arisum2  13967  geoserg  13972  geo2sum2  13978  fallfacfwd  14137  binomfallfaclem2  14141  bpolycl  14153  bpoly3  14159  bpoly4  14160  fsumcube  14161  sinf  14226  tanval2  14235  tanval3  14236  sinneg  14248  efival  14254  sinhval  14256  bitsinv1lem  14463  bitsres  14495  pythagtriplem1  14814  pythagtriplem14  14826  pythagtriplem17  14829  4sqlem5  14934  mul4sqlem  14945  4sqlem17OLD  14953  4sqlem17  14959  vdwlem5  14983  vdwlem6  14984  vdwlem8  14986  blcvx  21864  recld2  21880  addcnlem  21944  cnllycmp  22032  ipcnlem2  22263  rrxmval  22407  rrxmetlem  22409  pjthlem1  22439  ovollb2lem  22489  itgcnlem  22795  dvlem  22899  dvconst  22919  dvid  22920  dvcnp2  22922  dvaddbr  22940  dvmulbr  22941  dvcobr  22948  dvcjbr  22951  dvrec  22957  dvmptim  22972  dvcnvlem  22976  dveflem  22979  dvsincos  22981  cmvth  22991  dvlip  22993  dvlipcn  22994  c1liplem1  22996  dveq0  23000  dv11cn  23001  dvle  23007  lhop1lem  23013  dvfsumabs  23023  dvfsumlem1  23026  dvfsumlem2  23027  dvfsumrlim  23031  dvfsumrlim2  23032  ftc1lem4  23039  ftc1lem5  23040  ftc2  23044  dgrcolem2  23276  plydiveu  23299  aaliou2b  23345  taylfvallem1  23360  taylply2  23371  dvtaylp  23373  dvntaylp  23374  taylthlem1  23376  taylthlem2  23377  ulmbdd  23401  ulmcn  23402  ulmdvlem1  23403  mtest  23407  iblulm  23410  itgulm  23411  abelthlem9  23443  ptolemy  23499  tangtx  23508  sineq0  23524  efeq1  23526  efif1olem4  23542  tanarg  23616  logcnlem3  23637  logcnlem4  23638  advlogexp  23648  efopn  23651  cxpcn3lem  23735  cxpeq  23745  ang180lem4  23789  ang180lem5  23790  ang180  23791  isosctrlem2  23796  isosctrlem3  23797  isosctr  23798  ssscongptld  23799  affineequiv  23800  affineequiv2  23801  angpieqvdlem  23802  angpieqvdlem2  23803  angpined  23804  angpieqvd  23805  chordthmlem  23806  chordthmlem2  23807  chordthmlem3  23808  chordthmlem4  23809  chordthmlem5  23810  heron  23812  quad2  23813  quad  23814  dcubic1lem  23817  dcubic  23820  mcubic  23821  cubic2  23822  cubic  23823  dquartlem1  23825  dquartlem2  23826  dquart  23827  quart1cl  23828  quart1lem  23829  quart1  23830  quartlem2  23832  quartlem4  23834  quart  23835  atanf  23854  sinasin  23863  asinsin  23866  atanneg  23881  atancj  23884  efiatan  23886  atanlogsub  23890  efiatan2  23891  2efiatan  23892  atanbndlem  23899  dvatan  23909  atantayl  23911  lgamgulmlem2  24003  lgamgulmlem3  24004  lgamgulmlem5  24006  lgamgulmlem6  24007  lgamgulm2  24009  lgamucov  24011  lgamcvg2  24028  gamcvg  24029  gamcvg2lem  24032  ftalem2  24046  logfacrlim  24200  logexprlim  24201  lgsdirprm  24305  vmadivsum  24368  rpvmasumlem  24373  dchrisumlem2  24376  dchrisumlem3  24377  dchrmusum2  24380  dchrvmasumlem2  24384  dchrvmasumlem3  24385  dchrvmasumiflem1  24387  rpvmasum2  24398  dchrisum0lem1b  24401  dchrisum0lem1  24402  dchrisum0lem2a  24403  rplogsum  24413  mudivsum  24416  mulogsumlem  24417  mulogsum  24418  mulog2sumlem1  24420  mulog2sumlem2  24421  mulog2sumlem3  24422  vmalogdivsum2  24424  vmalogdivsum  24425  2vmadivsumlem  24426  selberglem1  24431  selberglem2  24432  selberg2lem  24436  selberg2  24437  selberg3lem1  24443  selberg4lem1  24446  selberg4  24447  pntrsumo1  24451  selberg3r  24455  selberg34r  24457  pntrlog2bndlem1  24463  pntrlog2bndlem2  24464  pntrlog2bndlem3  24465  pntrlog2bndlem4  24466  pntrlog2bndlem5  24467  pntibndlem2  24477  pntlemf  24491  pntlemo  24493  ttgcontlem1  24963  brbtwn2  24983  colinearalglem1  24984  colinearalglem2  24985  colinearalg  24988  axsegconlem1  24995  ax5seglem2  25007  ax5seglem6  25012  ax5seglem9  25015  axlowdimlem17  25036  axcontlem7  25048  axcontlem8  25049  cusgrasizeinds  25252  clwlkisclwwlk  25565  frghash2spot  25839  usgreghash2spotv  25842  frgregordn0  25846  numclwlk3lem3  25849  numclwlk1lem2fo  25871  smcnlem  26381  ipval2  26391  4ipval2  26392  4ipval3  26396  dipcj  26401  pjhthlem1  27092  lt2addrd  28374  bcm1n  28419  bhmafibid2  28454  2sqmod  28457  sqsscirc2  28763  signslema  29499  subfaclim  29959  divcnvlin  30415  iprodgam  30426  bj-lineq  31757  bj-bary1lem  31759  bj-bary1lem1  31760  bj-bary1  31761  ftc1cnnclem  32059  ftc1anclem7  32067  ftc1anclem8  32068  ftc1anc  32069  ftc2nc  32070  areacirclem1  32076  areacirclem4  32079  areacirc  32081  cntotbnd  32172  rencldnfilem  35707  pellexlem2  35718  pellexlem6  35722  pell1234qrne0  35743  pell1234qrmulcl  35745  rmyluc  35829  jm2.18  35887  jm2.19  35892  areaquad  36145  lhe4.4ex1a  36721  bcc0  36732  bccp1k  36733  bccm1k  36734  binomcxplemwb  36740  binomcxplemnn0  36741  binomcxplemrat  36742  binomcxplemfrat  36743  binomcxplemdvbinom  36745  binomcxplemnotnn0  36748  isosctrlem1ALT  37370  sineq0ALT  37373  oddfl  37524  dstregt0  37528  subadd4b  37529  sub31  37541  fzisoeu  37555  absnpncan2d  37557  absnpncan3d  37562  subdir2d  37566  supxrgelem  37597  mullimc  37733  ellimcabssub0  37734  mullimcf  37740  limcrecl  37746  lptre2pt  37757  limcleqr  37762  neglimc  37765  addlimc  37766  0ellimcdiv  37767  limclner  37769  reclimc  37771  fperdvper  37827  dvdivbd  37832  dvbdfbdioolem2  37838  ioodvbdlimc1lem1  37840  ioodvbdlimc1lem1OLD  37842  volioc  37886  stoweidlem1  37898  stoweidlem11  37908  stoweidlem13  37910  stoweidlem26  37923  stoweid  37962  wallispi  37969  wallispi2lem1  37970  wallispi2lem2  37971  wallispi2  37972  stirlinglem1  37973  stirlinglem4  37976  stirlinglem5  37977  stirlinglem7  37979  stirlinglem11  37983  dirkertrigeqlem2  37998  fourierdlem4  38010  fourierdlem26  38032  fourierdlem30  38036  fourierdlem42  38049  fourierdlem42OLD  38050  fourierdlem63  38070  fourierdlem65  38072  fourierdlem72  38079  fourierdlem74  38081  fourierdlem75  38082  fourierdlem76  38083  fourierdlem80  38087  fourierdlem81  38088  fourierdlem89  38096  fourierdlem90  38097  fourierdlem91  38098  fourierdlem107  38114  fourierdlem109  38116  fouriersw  38132  etransclem1  38137  etransclem4  38140  etransclem8  38144  etransclem18  38154  etransclem20  38156  etransclem21  38157  etransclem23  38159  etransclem35  38171  etransclem46  38182  rrxtopnfi  38192  rrndistlt  38196  sge0gtfsumgt  38322  volico  38400  hoidmv1lelem2  38451  hoidmvlelem2  38455  sigarmf  38500  sigarms  38502  sigarexp  38505  sigardiv  38507  sigarcol  38510  sharhght  38511  sigaradd  38512  cevathlem2  38514  cevath  38515  pfxccatin12lem2  39004  fldivmod  40593  dignn0flhalflem2  40699  sinhpcosh  40732  i2linesd  40790