Theorem subcld 9926

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 9815	. 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 1767  (class class class)co 6282   CCcc 9486   - cmin 9801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-po 4800  df-so 4801  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-er 7308  df-en 7514  df-dom 7515  df-sdom 7516  df-pnf 9626  df-mnf 9627  df-ltxr 9629  df-sub 9803

This theorem is referenced by:  kcnktkm1cn  9984  muleqadd  10189  hashfz  12444  hashfzo  12446  hashf1lem2  12465  hashf1  12466  ccatswrd  12638  crre  12904  remim  12907  remullem  12918  abs3lem  13127  caubnd2  13146  rlimuni  13329  climuni  13331  rlimcld2  13357  rlimrege0  13358  rlimrecl  13359  mulcn2  13374  reccn2  13375  cn1lem  13376  o1sub  13394  rlimo1  13395  o1dif  13408  rlimsqzlem  13427  caucvgrlem2  13453  iseralt  13463  fsumparts  13576  cvgcmpce  13588  incexclem  13604  arisum2  13628  geoserg  13633  geo2sum2  13639  sinf  13713  tanval2  13722  tanval3  13723  sinneg  13735  efival  13741  sinhval  13743  bitsinv1lem  13943  bitsres  13975  pythagtriplem1  14192  pythagtriplem14  14204  pythagtriplem17  14207  4sqlem5  14312  mul4sqlem  14323  4sqlem17  14331  vdwlem5  14355  vdwlem6  14356  vdwlem8  14358  blcvx  21035  recld2  21051  addcnlem  21100  cnllycmp  21188  ipcnlem2  21416  rrxmval  21564  rrxmetlem  21566  pjthlem1  21584  ovollb2lem  21631  itgcnlem  21928  dvlem  22032  dvconst  22052  dvid  22053  dvcnp2  22055  dvaddbr  22073  dvmulbr  22074  dvcobr  22081  dvcjbr  22084  dvrec  22090  dvmptim  22105  dvcnvlem  22109  dveflem  22112  dvsincos  22114  cmvth  22124  dvlip  22126  dvlipcn  22127  c1liplem1  22129  dveq0  22133  dv11cn  22134  dvle  22140  lhop1lem  22146  dvfsumabs  22156  dvfsumlem1  22159  dvfsumlem2  22160  dvfsumrlim  22164  dvfsumrlim2  22165  ftc1lem4  22172  ftc1lem5  22173  ftc2  22177  dgrcolem2  22402  plydiveu  22425  aaliou2b  22468  taylfvallem1  22483  taylply2  22494  dvtaylp  22496  dvntaylp  22497  taylthlem1  22499  taylthlem2  22500  ulmbdd  22524  ulmcn  22525  ulmdvlem1  22526  mtest  22530  iblulm  22533  itgulm  22534  abelthlem9  22566  ptolemy  22619  tangtx  22628  sineq0  22644  efeq1  22646  efif1olem4  22662  tanarg  22729  logcnlem3  22750  logcnlem4  22751  advlogexp  22761  efopn  22764  cxpcn3lem  22846  cxpeq  22856  ang180lem4  22869  ang180lem5  22870  ang180  22871  isosctrlem2  22878  isosctrlem3  22879  isosctr  22880  ssscongptld  22881  affineequiv  22882  affineequiv2  22883  angpieqvdlem  22884  angpieqvdlem2  22885  angpined  22886  angpieqvd  22887  chordthmlem  22888  chordthmlem2  22889  chordthmlem3  22890  chordthmlem4  22891  chordthmlem5  22892  heron  22894  quad2  22895  quad  22896  dcubic1lem  22899  dcubic  22902  mcubic  22903  cubic2  22904  cubic  22905  dquartlem1  22907  dquartlem2  22908  dquart  22909  quart1cl  22910  quart1lem  22911  quart1  22912  quartlem2  22914  quartlem4  22916  quart  22917  atanf  22936  sinasin  22945  asinsin  22948  atanneg  22963  atancj  22966  efiatan  22968  atanlogsub  22972  efiatan2  22973  2efiatan  22974  atanbndlem  22981  dvatan  22991  atantayl  22993  ftalem2  23072  logfacrlim  23224  logexprlim  23225  lgsdirprm  23329  vmadivsum  23392  rpvmasumlem  23397  dchrisumlem2  23400  dchrisumlem3  23401  dchrmusum2  23404  dchrvmasumlem2  23408  dchrvmasumlem3  23409  dchrvmasumiflem1  23411  rpvmasum2  23422  dchrisum0lem1b  23425  dchrisum0lem1  23426  dchrisum0lem2a  23427  rplogsum  23437  mudivsum  23440  mulogsumlem  23441  mulogsum  23442  mulog2sumlem1  23444  mulog2sumlem2  23445  mulog2sumlem3  23446  vmalogdivsum2  23448  vmalogdivsum  23449  2vmadivsumlem  23450  selberglem1  23455  selberglem2  23456  selberg2lem  23460  selberg2  23461  selberg3lem1  23467  selberg4lem1  23470  selberg4  23471  pntrsumo1  23475  selberg3r  23479  selberg34r  23481  pntrlog2bndlem1  23487  pntrlog2bndlem2  23488  pntrlog2bndlem3  23489  pntrlog2bndlem4  23490  pntrlog2bndlem5  23491  pntibndlem2  23501  pntlemf  23515  pntlemo  23517  ttgcontlem1  23861  brbtwn2  23881  colinearalglem1  23882  colinearalglem2  23883  colinearalg  23886  axsegconlem1  23893  ax5seglem2  23905  ax5seglem6  23910  ax5seglem9  23913  axlowdimlem17  23934  axcontlem7  23946  axcontlem8  23947  cusgrasizeinds  24149  clwlkisclwwlk  24462  frghash2spot  24737  usgreghash2spotv  24740  frgregordn0  24744  numclwlk3lem3  24747  numclwlk1lem2fo  24769  smcnlem  25280  ipval2  25290  4ipval2  25291  4ipval3  25295  dipcj  25300  pjhthlem1  25982  lt2addrd  27228  bcm1n  27265  sqsscirc2  27524  signslema  28156  lgamgulmlem2  28209  lgamgulmlem3  28210  lgamgulmlem5  28212  lgamgulmlem6  28213  lgamgulm2  28215  lgamucov  28217  lgamcvg2  28234  gamcvg  28235  gamcvg2lem  28238  subfaclim  28269  pnpncand  28587  divcnvlin  28592  iprodgam  28699  fallfacfwd  28732  binomfallfaclem2  28736  bpolycl  29388  bpoly3  29394  bpoly4  29395  fsumcube  29396  ftc1cnnclem  29663  ftc1anclem7  29671  ftc1anclem8  29672  ftc1anc  29673  ftc2nc  29674  areacirclem1  29682  areacirclem4  29685  areacirc  29687  cntotbnd  29893  rencldnfilem  30356  pellexlem2  30368  pellexlem6  30372  pell1234qrne0  30391  pell1234qrmulcl  30393  rmyluc  30475  jm2.18  30534  jm2.19  30539  areaquad  30789  lhe4.4ex1a  30834  oddfl  31036  dstregt0  31040  subadd4b  31041  sub31  31056  absnpncand  31064  fzisoeu  31077  absnpncan2d  31079  absnpncan3d  31084  mullimc  31158  ellimcabssub0  31159  mullimcf  31165  limcrecl  31171  lptre2pt  31182  limcleqr  31186  neglimc  31189  addlimc  31190  0ellimcdiv  31191  limclner  31193  reclimc  31195  cncfshift  31212  cncfperiod  31217  fperdvper  31248  dvbdfbdioolem2  31259  ioodvbdlimc1lem1  31261  volioc  31290  stoweidlem1  31301  stoweidlem11  31311  stoweidlem13  31313  stoweidlem26  31326  stoweid  31363  wallispi  31370  wallispi2lem1  31371  wallispi2lem2  31372  wallispi2  31373  stirlinglem1  31374  stirlinglem4  31377  stirlinglem5  31378  stirlinglem7  31380  stirlinglem11  31384  dirkertrigeqlem2  31399  fourierdlem4  31411  fourierdlem26  31433  fourierdlem30  31437  fourierdlem42  31449  fourierdlem45  31452  fourierdlem63  31470  fourierdlem65  31472  fourierdlem72  31479  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem80  31487  fourierdlem81  31488  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem107  31514  fourierdlem109  31516  fouriersw  31532  sigarmf  31538  sigarms  31540  sigarexp  31543  sigardiv  31545  sigarcol  31548  sharhght  31549  sigaradd  31550  cevathlem2  31552  cevath  31553  sinhpcosh  32215  i2linesd  32275  isosctrlem1ALT  32814  sineq0ALT  32817  bj-lineq  33749  bj-bary1lem  33751  bj-bary1lem1  33752  bj-bary1  33753