Theorem subcld 9932

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

Syntax hints:   -> wi 4   e. wcel 1872  (class class class)co 6244   CCcc 9483   - cmin 9806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-po 4712  df-so 4713  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-er 7313  df-en 7520  df-dom 7521  df-sdom 7522  df-pnf 9623  df-mnf 9624  df-ltxr 9626  df-sub 9808

This theorem is referenced by:  pnpncand  9987  muleqadd  10202  hashfz  12542  hashfzo  12544  hashf1lem2  12562  hashf1  12563  ccatswrd  12753  crre  13116  remim  13119  remullem  13130  abs3lem  13340  caubnd2  13359  rlimuni  13552  climuni  13554  rlimcld2  13580  rlimrege0  13581  rlimrecl  13582  mulcn2  13597  reccn2  13598  cn1lem  13599  o1sub  13617  rlimo1  13618  o1dif  13631  rlimsqzlem  13650  caucvgrlem2  13678  iseralt  13689  fsumparts  13804  cvgcmpce  13816  incexclem  13832  arisum2  13857  geoserg  13862  geo2sum2  13868  fallfacfwd  14027  binomfallfaclem2  14031  bpolycl  14043  bpoly3  14049  bpoly4  14050  fsumcube  14051  sinf  14116  tanval2  14125  tanval3  14126  sinneg  14138  efival  14144  sinhval  14146  bitsinv1lem  14353  bitsres  14385  pythagtriplem1  14704  pythagtriplem14  14716  pythagtriplem17  14719  4sqlem5  14824  mul4sqlem  14835  4sqlem17OLD  14843  4sqlem17  14849  vdwlem5  14873  vdwlem6  14874  vdwlem8  14876  blcvx  21753  recld2  21769  addcnlem  21833  cnllycmp  21921  ipcnlem2  22152  rrxmval  22296  rrxmetlem  22298  pjthlem1  22328  ovollb2lem  22378  itgcnlem  22684  dvlem  22788  dvconst  22808  dvid  22809  dvcnp2  22811  dvaddbr  22829  dvmulbr  22830  dvcobr  22837  dvcjbr  22840  dvrec  22846  dvmptim  22861  dvcnvlem  22865  dveflem  22868  dvsincos  22870  cmvth  22880  dvlip  22882  dvlipcn  22883  c1liplem1  22885  dveq0  22889  dv11cn  22890  dvle  22896  lhop1lem  22902  dvfsumabs  22912  dvfsumlem1  22915  dvfsumlem2  22916  dvfsumrlim  22920  dvfsumrlim2  22921  ftc1lem4  22928  ftc1lem5  22929  ftc2  22933  dgrcolem2  23165  plydiveu  23188  aaliou2b  23234  taylfvallem1  23249  taylply2  23260  dvtaylp  23262  dvntaylp  23263  taylthlem1  23265  taylthlem2  23266  ulmbdd  23290  ulmcn  23291  ulmdvlem1  23292  mtest  23296  iblulm  23299  itgulm  23300  abelthlem9  23332  ptolemy  23388  tangtx  23397  sineq0  23413  efeq1  23415  efif1olem4  23431  tanarg  23505  logcnlem3  23526  logcnlem4  23527  advlogexp  23537  efopn  23540  cxpcn3lem  23624  cxpeq  23634  ang180lem4  23678  ang180lem5  23679  ang180  23680  isosctrlem2  23685  isosctrlem3  23686  isosctr  23687  ssscongptld  23688  affineequiv  23689  affineequiv2  23690  angpieqvdlem  23691  angpieqvdlem2  23692  angpined  23693  angpieqvd  23694  chordthmlem  23695  chordthmlem2  23696  chordthmlem3  23697  chordthmlem4  23698  chordthmlem5  23699  heron  23701  quad2  23702  quad  23703  dcubic1lem  23706  dcubic  23709  mcubic  23710  cubic2  23711  cubic  23712  dquartlem1  23714  dquartlem2  23715  dquart  23716  quart1cl  23717  quart1lem  23718  quart1  23719  quartlem2  23721  quartlem4  23723  quart  23724  atanf  23743  sinasin  23752  asinsin  23755  atanneg  23770  atancj  23773  efiatan  23775  atanlogsub  23779  efiatan2  23780  2efiatan  23781  atanbndlem  23788  dvatan  23798  atantayl  23800  lgamgulmlem2  23892  lgamgulmlem3  23893  lgamgulmlem5  23895  lgamgulmlem6  23896  lgamgulm2  23898  lgamucov  23900  lgamcvg2  23917  gamcvg  23918  gamcvg2lem  23921  ftalem2  23935  logfacrlim  24089  logexprlim  24090  lgsdirprm  24194  vmadivsum  24257  rpvmasumlem  24262  dchrisumlem2  24265  dchrisumlem3  24266  dchrmusum2  24269  dchrvmasumlem2  24273  dchrvmasumlem3  24274  dchrvmasumiflem1  24276  rpvmasum2  24287  dchrisum0lem1b  24290  dchrisum0lem1  24291  dchrisum0lem2a  24292  rplogsum  24302  mudivsum  24305  mulogsumlem  24306  mulogsum  24307  mulog2sumlem1  24309  mulog2sumlem2  24310  mulog2sumlem3  24311  vmalogdivsum2  24313  vmalogdivsum  24314  2vmadivsumlem  24315  selberglem1  24320  selberglem2  24321  selberg2lem  24325  selberg2  24326  selberg3lem1  24332  selberg4lem1  24335  selberg4  24336  pntrsumo1  24340  selberg3r  24344  selberg34r  24346  pntrlog2bndlem1  24352  pntrlog2bndlem2  24353  pntrlog2bndlem3  24354  pntrlog2bndlem4  24355  pntrlog2bndlem5  24356  pntibndlem2  24366  pntlemf  24380  pntlemo  24382  ttgcontlem1  24852  brbtwn2  24872  colinearalglem1  24873  colinearalglem2  24874  colinearalg  24877  axsegconlem1  24884  ax5seglem2  24896  ax5seglem6  24901  ax5seglem9  24904  axlowdimlem17  24925  axcontlem7  24937  axcontlem8  24938  cusgrasizeinds  25141  clwlkisclwwlk  25454  frghash2spot  25728  usgreghash2spotv  25731  frgregordn0  25735  numclwlk3lem3  25738  numclwlk1lem2fo  25760  smcnlem  26270  ipval2  26280  4ipval2  26281  4ipval3  26285  dipcj  26290  pjhthlem1  26981  lt2addrd  28271  bcm1n  28316  bhmafibid2  28352  2sqmod  28355  sqsscirc2  28662  signslema  29398  subfaclim  29858  divcnvlin  30313  iprodgam  30324  bj-lineq  31620  bj-bary1lem  31622  bj-bary1lem1  31623  bj-bary1  31624  ftc1cnnclem  31922  ftc1anclem7  31930  ftc1anclem8  31931  ftc1anc  31932  ftc2nc  31933  areacirclem1  31939  areacirclem4  31942  areacirc  31944  cntotbnd  32035  rencldnfilem  35575  pellexlem2  35587  pellexlem6  35591  pell1234qrne0  35612  pell1234qrmulcl  35614  rmyluc  35698  jm2.18  35756  jm2.19  35761  areaquad  36014  lhe4.4ex1a  36591  bcc0  36602  bccp1k  36603  bccm1k  36604  binomcxplemwb  36610  binomcxplemnn0  36611  binomcxplemrat  36612  binomcxplemfrat  36613  binomcxplemdvbinom  36615  binomcxplemnotnn0  36618  isosctrlem1ALT  37247  sineq0ALT  37250  oddfl  37384  dstregt0  37388  subadd4b  37389  sub31  37401  fzisoeu  37415  absnpncan2d  37417  absnpncan3d  37422  subdir2d  37426  supxrgelem  37457  mullimc  37579  ellimcabssub0  37580  mullimcf  37586  limcrecl  37592  lptre2pt  37603  limcleqr  37608  neglimc  37611  addlimc  37612  0ellimcdiv  37613  limclner  37615  reclimc  37617  fperdvper  37673  dvdivbd  37678  dvbdfbdioolem2  37684  ioodvbdlimc1lem1  37686  ioodvbdlimc1lem1OLD  37688  volioc  37732  stoweidlem1  37744  stoweidlem11  37754  stoweidlem13  37756  stoweidlem26  37769  stoweid  37808  wallispi  37815  wallispi2lem1  37816  wallispi2lem2  37817  wallispi2  37818  stirlinglem1  37819  stirlinglem4  37822  stirlinglem5  37823  stirlinglem7  37825  stirlinglem11  37829  dirkertrigeqlem2  37844  fourierdlem4  37856  fourierdlem26  37878  fourierdlem30  37882  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem63  37916  fourierdlem65  37918  fourierdlem72  37925  fourierdlem74  37927  fourierdlem75  37928  fourierdlem76  37929  fourierdlem80  37933  fourierdlem81  37934  fourierdlem89  37942  fourierdlem90  37943  fourierdlem91  37944  fourierdlem107  37960  fourierdlem109  37962  fouriersw  37978  etransclem1  37983  etransclem4  37986  etransclem8  37990  etransclem18  38000  etransclem20  38002  etransclem21  38003  etransclem23  38005  etransclem35  38017  etransclem46  38028  sge0gtfsumgt  38136  volico  38210  hoidmv1lelem2  38261  hoidmvlelem2  38265  sigarmf  38277  sigarms  38279  sigarexp  38282  sigardiv  38284  sigarcol  38287  sharhght  38288  sigaradd  38289  cevathlem2  38291  cevath  38292  pfxccatin12lem2  38778  fldivmod  39914  dignn0flhalflem2  40020  sinhpcosh  40053  i2linesd  40111