Theorem subcld 9862

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

Syntax hints:   -> wi 4   e. wcel 1836  (class class class)co 6214   CCcc 9419   - cmin 9736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-mulcom 9485  ax-addass 9486  ax-mulass 9487  ax-distr 9488  ax-i2m1 9489  ax-1ne0 9490  ax-1rid 9491  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496  ax-pre-ltadd 9497

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-reu 2749  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-po 4727  df-so 4728  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-riota 6176  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-er 7247  df-en 7454  df-dom 7455  df-sdom 7456  df-pnf 9559  df-mnf 9560  df-ltxr 9562  df-sub 9738

This theorem is referenced by:  pnpncand  9917  muleqadd  10128  hashfz  12408  hashfzo  12410  hashf1lem2  12428  hashf1  12429  ccatswrd  12611  crre  12968  remim  12971  remullem  12982  abs3lem  13192  caubnd2  13211  rlimuni  13394  climuni  13396  rlimcld2  13422  rlimrege0  13423  rlimrecl  13424  mulcn2  13439  reccn2  13440  cn1lem  13441  o1sub  13459  rlimo1  13460  o1dif  13473  rlimsqzlem  13492  caucvgrlem2  13518  iseralt  13528  fsumparts  13641  cvgcmpce  13653  incexclem  13669  arisum2  13693  geoserg  13698  geo2sum2  13704  sinf  13880  tanval2  13889  tanval3  13890  sinneg  13902  efival  13908  sinhval  13910  bitsinv1lem  14112  bitsres  14144  pythagtriplem1  14361  pythagtriplem14  14373  pythagtriplem17  14376  4sqlem5  14481  mul4sqlem  14492  4sqlem17  14500  vdwlem5  14524  vdwlem6  14525  vdwlem8  14527  blcvx  21407  recld2  21423  addcnlem  21472  cnllycmp  21560  ipcnlem2  21788  rrxmval  21936  rrxmetlem  21938  pjthlem1  21956  ovollb2lem  22003  itgcnlem  22300  dvlem  22404  dvconst  22424  dvid  22425  dvcnp2  22427  dvaddbr  22445  dvmulbr  22446  dvcobr  22453  dvcjbr  22456  dvrec  22462  dvmptim  22477  dvcnvlem  22481  dveflem  22484  dvsincos  22486  cmvth  22496  dvlip  22498  dvlipcn  22499  c1liplem1  22501  dveq0  22505  dv11cn  22506  dvle  22512  lhop1lem  22518  dvfsumabs  22528  dvfsumlem1  22531  dvfsumlem2  22532  dvfsumrlim  22536  dvfsumrlim2  22537  ftc1lem4  22544  ftc1lem5  22545  ftc2  22549  dgrcolem2  22775  plydiveu  22798  aaliou2b  22841  taylfvallem1  22856  taylply2  22867  dvtaylp  22869  dvntaylp  22870  taylthlem1  22872  taylthlem2  22873  ulmbdd  22897  ulmcn  22898  ulmdvlem1  22899  mtest  22903  iblulm  22906  itgulm  22907  abelthlem9  22939  ptolemy  22993  tangtx  23002  sineq0  23018  efeq1  23020  efif1olem4  23036  tanarg  23110  logcnlem3  23131  logcnlem4  23132  advlogexp  23142  efopn  23145  cxpcn3lem  23227  cxpeq  23237  ang180lem4  23281  ang180lem5  23282  ang180  23283  isosctrlem2  23288  isosctrlem3  23289  isosctr  23290  ssscongptld  23291  affineequiv  23292  affineequiv2  23293  angpieqvdlem  23294  angpieqvdlem2  23295  angpined  23296  angpieqvd  23297  chordthmlem  23298  chordthmlem2  23299  chordthmlem3  23300  chordthmlem4  23301  chordthmlem5  23302  heron  23304  quad2  23305  quad  23306  dcubic1lem  23309  dcubic  23312  mcubic  23313  cubic2  23314  cubic  23315  dquartlem1  23317  dquartlem2  23318  dquart  23319  quart1cl  23320  quart1lem  23321  quart1  23322  quartlem2  23324  quartlem4  23326  quart  23327  atanf  23346  sinasin  23355  asinsin  23358  atanneg  23373  atancj  23376  efiatan  23378  atanlogsub  23382  efiatan2  23383  2efiatan  23384  atanbndlem  23391  dvatan  23401  atantayl  23403  ftalem2  23483  logfacrlim  23635  logexprlim  23636  lgsdirprm  23740  vmadivsum  23803  rpvmasumlem  23808  dchrisumlem2  23811  dchrisumlem3  23812  dchrmusum2  23815  dchrvmasumlem2  23819  dchrvmasumlem3  23820  dchrvmasumiflem1  23822  rpvmasum2  23833  dchrisum0lem1b  23836  dchrisum0lem1  23837  dchrisum0lem2a  23838  rplogsum  23848  mudivsum  23851  mulogsumlem  23852  mulogsum  23853  mulog2sumlem1  23855  mulog2sumlem2  23856  mulog2sumlem3  23857  vmalogdivsum2  23859  vmalogdivsum  23860  2vmadivsumlem  23861  selberglem1  23866  selberglem2  23867  selberg2lem  23871  selberg2  23872  selberg3lem1  23878  selberg4lem1  23881  selberg4  23882  pntrsumo1  23886  selberg3r  23890  selberg34r  23892  pntrlog2bndlem1  23898  pntrlog2bndlem2  23899  pntrlog2bndlem3  23900  pntrlog2bndlem4  23901  pntrlog2bndlem5  23902  pntibndlem2  23912  pntlemf  23926  pntlemo  23928  ttgcontlem1  24330  brbtwn2  24350  colinearalglem1  24351  colinearalglem2  24352  colinearalg  24355  axsegconlem1  24362  ax5seglem2  24374  ax5seglem6  24379  ax5seglem9  24382  axlowdimlem17  24403  axcontlem7  24415  axcontlem8  24416  cusgrasizeinds  24618  clwlkisclwwlk  24931  frghash2spot  25205  usgreghash2spotv  25208  frgregordn0  25212  numclwlk3lem3  25215  numclwlk1lem2fo  25237  smcnlem  25745  ipval2  25755  4ipval2  25756  4ipval3  25760  dipcj  25765  pjhthlem1  26447  lt2addrd  27743  bcm1n  27783  bhmafibid2  27816  2sqmod  27819  sqsscirc2  28076  signslema  28738  lgamgulmlem2  28797  lgamgulmlem3  28798  lgamgulmlem5  28800  lgamgulmlem6  28801  lgamgulm2  28803  lgamucov  28805  lgamcvg2  28822  gamcvg  28823  gamcvg2lem  28826  subfaclim  28857  divcnvlin  29320  iprodgam  29327  fallfacfwd  29360  binomfallfaclem2  29364  bpolycl  30003  bpoly3  30009  bpoly4  30010  fsumcube  30011  ftc1cnnclem  30290  ftc1anclem7  30298  ftc1anclem8  30299  ftc1anc  30300  ftc2nc  30301  areacirclem1  30309  areacirclem4  30312  areacirc  30314  cntotbnd  30494  rencldnfilem  30955  pellexlem2  30967  pellexlem6  30971  pell1234qrne0  30990  pell1234qrmulcl  30992  rmyluc  31074  jm2.18  31132  jm2.19  31137  areaquad  31388  lhe4.4ex1a  31438  bcc0  31449  bccp1k  31450  bccm1k  31451  binomcxplemwb  31457  binomcxplemnn0  31458  binomcxplemrat  31459  binomcxplemfrat  31460  binomcxplemdvbinom  31462  binomcxplemnotnn0  31465  oddfl  31661  dstregt0  31665  subadd4b  31666  sub31  31681  fzisoeu  31701  absnpncan2d  31703  absnpncan3d  31708  subdir2d  31712  mullimc  31823  ellimcabssub0  31824  mullimcf  31830  limcrecl  31836  lptre2pt  31847  limcleqr  31851  neglimc  31854  addlimc  31855  0ellimcdiv  31856  limclner  31858  reclimc  31860  fperdvper  31916  dvdivbd  31921  dvbdfbdioolem2  31927  ioodvbdlimc1lem1  31929  volioc  31972  stoweidlem1  31984  stoweidlem11  31994  stoweidlem13  31996  stoweidlem26  32009  stoweid  32046  wallispi  32053  wallispi2lem1  32054  wallispi2lem2  32055  wallispi2  32056  stirlinglem1  32057  stirlinglem4  32060  stirlinglem5  32061  stirlinglem7  32063  stirlinglem11  32067  dirkertrigeqlem2  32082  fourierdlem4  32094  fourierdlem26  32116  fourierdlem30  32120  fourierdlem42  32132  fourierdlem63  32153  fourierdlem65  32155  fourierdlem72  32162  fourierdlem74  32164  fourierdlem75  32165  fourierdlem76  32166  fourierdlem80  32170  fourierdlem81  32171  fourierdlem89  32179  fourierdlem90  32180  fourierdlem91  32181  fourierdlem107  32197  fourierdlem109  32199  fouriersw  32215  etransclem1  32219  etransclem4  32222  etransclem8  32226  etransclem18  32236  etransclem20  32238  etransclem21  32239  etransclem23  32241  etransclem35  32253  etransclem46  32264  sigarmf  32272  sigarms  32274  sigarexp  32277  sigardiv  32279  sigarcol  32282  sharhght  32283  sigaradd  32284  cevathlem2  32286  cevath  32287  pfxccatin12lem2  32634  fldivmod  33366  dignn0flhalflem2  33472  sinhpcosh  33505  i2linesd  33563  isosctrlem1ALT  34116  sineq0ALT  34119  bj-lineq  35056  bj-bary1lem  35058  bj-bary1lem1  35059  bj-bary1  35060