Theorem subcld 9711

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 9601	. 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 1756  (class class class)co 6086   CCcc 9272   - cmin 9587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-po 4636  df-so 4637  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-ltxr 9415  df-sub 9589

This theorem is referenced by:  muleqadd  9972  hashfz  12180  hashfzo  12182  hashf1lem2  12201  hashf1  12202  ccatswrd  12342  crre  12595  remim  12598  remullem  12609  abs3lem  12818  caubnd2  12837  rlimuni  13020  climuni  13022  rlimcld2  13048  rlimrege0  13049  rlimrecl  13050  mulcn2  13065  reccn2  13066  cn1lem  13067  o1sub  13085  rlimo1  13086  o1dif  13099  rlimsqzlem  13118  caucvgrlem2  13144  iseralt  13154  fsumparts  13261  cvgcmpce  13273  incexclem  13291  arisum2  13315  geoserg  13320  geo2sum2  13326  sinf  13400  tanval2  13409  tanval3  13410  sinneg  13422  efival  13428  sinhval  13430  bitsinv1lem  13629  bitsres  13661  pythagtriplem1  13875  pythagtriplem14  13887  pythagtriplem17  13890  4sqlem5  13995  mul4sqlem  14006  4sqlem17  14014  vdwlem5  14038  vdwlem6  14039  vdwlem8  14041  blcvx  20350  recld2  20366  addcnlem  20415  cnllycmp  20503  ipcnlem2  20731  rrxmval  20879  rrxmetlem  20881  pjthlem1  20899  ovollb2lem  20946  itgcnlem  21242  dvlem  21346  dvconst  21366  dvid  21367  dvcnp2  21369  dvaddbr  21387  dvmulbr  21388  dvcobr  21395  dvcjbr  21398  dvrec  21404  dvmptim  21419  dvcnvlem  21423  dveflem  21426  dvsincos  21428  cmvth  21438  dvlip  21440  dvlipcn  21441  c1liplem1  21443  dveq0  21447  dv11cn  21448  dvle  21454  lhop1lem  21460  dvfsumabs  21470  dvfsumlem1  21473  dvfsumlem2  21474  dvfsumrlim  21478  dvfsumrlim2  21479  ftc1lem4  21486  ftc1lem5  21487  ftc2  21491  dgrcolem2  21716  plydiveu  21739  aaliou2b  21782  taylfvallem1  21797  taylply2  21808  dvtaylp  21810  dvntaylp  21811  taylthlem1  21813  taylthlem2  21814  ulmbdd  21838  ulmcn  21839  ulmdvlem1  21840  mtest  21844  iblulm  21847  itgulm  21848  abelthlem9  21880  ptolemy  21933  tangtx  21942  sineq0  21958  efeq1  21960  efif1olem4  21976  tanarg  22043  logcnlem3  22064  logcnlem4  22065  advlogexp  22075  efopn  22078  cxpcn3lem  22160  cxpeq  22170  ang180lem4  22183  ang180lem5  22184  ang180  22185  isosctrlem2  22192  isosctrlem3  22193  isosctr  22194  ssscongptld  22195  affineequiv  22196  affineequiv2  22197  angpieqvdlem  22198  angpieqvdlem2  22199  angpined  22200  angpieqvd  22201  chordthmlem  22202  chordthmlem2  22203  chordthmlem3  22204  chordthmlem4  22205  chordthmlem5  22206  heron  22208  quad2  22209  quad  22210  dcubic1lem  22213  dcubic  22216  mcubic  22217  cubic2  22218  cubic  22219  dquartlem1  22221  dquartlem2  22222  dquart  22223  quart1cl  22224  quart1lem  22225  quart1  22226  quartlem2  22228  quartlem4  22230  quart  22231  atanf  22250  sinasin  22259  asinsin  22262  atanneg  22277  atancj  22280  efiatan  22282  atanlogsub  22286  efiatan2  22287  2efiatan  22288  atanbndlem  22295  dvatan  22305  atantayl  22307  ftalem2  22386  logfacrlim  22538  logexprlim  22539  lgsdirprm  22643  vmadivsum  22706  rpvmasumlem  22711  dchrisumlem2  22714  dchrisumlem3  22715  dchrmusum2  22718  dchrvmasumlem2  22722  dchrvmasumlem3  22723  dchrvmasumiflem1  22725  rpvmasum2  22736  dchrisum0lem1b  22739  dchrisum0lem1  22740  dchrisum0lem2a  22741  rplogsum  22751  mudivsum  22754  mulogsumlem  22755  mulogsum  22756  mulog2sumlem1  22758  mulog2sumlem2  22759  mulog2sumlem3  22760  vmalogdivsum2  22762  vmalogdivsum  22763  2vmadivsumlem  22764  selberglem1  22769  selberglem2  22770  selberg2lem  22774  selberg2  22775  selberg3lem1  22781  selberg4lem1  22784  selberg4  22785  pntrsumo1  22789  selberg3r  22793  selberg34r  22795  pntrlog2bndlem1  22801  pntrlog2bndlem2  22802  pntrlog2bndlem3  22803  pntrlog2bndlem4  22804  pntrlog2bndlem5  22805  pntibndlem2  22815  pntlemf  22829  pntlemo  22831  ttgcontlem1  23082  brbtwn2  23102  colinearalglem1  23103  colinearalglem2  23104  colinearalg  23107  axsegconlem1  23114  ax5seglem2  23126  ax5seglem6  23131  ax5seglem9  23134  axlowdimlem17  23155  axcontlem7  23167  axcontlem8  23168  cusgrasizeinds  23335  smcnlem  24043  ipval2  24053  4ipval2  24054  4ipval3  24058  dipcj  24063  pjhthlem1  24745  lt2addrd  25987  bcm1n  26030  sqsscirc2  26291  signslema  26915  lgamgulmlem2  26968  lgamgulmlem3  26969  lgamgulmlem5  26971  lgamgulmlem6  26972  lgamgulm2  26974  lgamucov  26976  lgamcvg2  26993  gamcvg  26994  gamcvg2lem  26997  subfaclim  27028  pnpncand  27345  divcnvlin  27350  iprodgam  27457  fallfacfwd  27490  binomfallfaclem2  27494  bpolycl  28146  bpoly3  28152  bpoly4  28153  fsumcube  28154  ftc1cnnclem  28418  ftc1anclem7  28426  ftc1anclem8  28427  ftc1anc  28428  ftc2nc  28429  areacirclem1  28437  areacirclem4  28440  areacirc  28442  cntotbnd  28648  rencldnfilem  29112  pellexlem2  29124  pellexlem6  29128  pell1234qrne0  29147  pell1234qrmulcl  29149  rmyluc  29231  jm2.18  29290  jm2.19  29295  areaquad  29545  lhe4.4ex1a  29556  stoweidlem1  29749  stoweidlem11  29759  stoweidlem13  29761  stoweidlem26  29774  stoweid  29811  wallispi  29818  wallispi2lem1  29819  wallispi2lem2  29820  wallispi2  29821  stirlinglem1  29822  stirlinglem4  29825  stirlinglem5  29826  stirlinglem7  29828  stirlinglem11  29832  sigarmf  29843  sigarms  29845  sigarexp  29848  sigardiv  29850  sigarcol  29853  sharhght  29854  sigaradd  29855  cevathlem2  29857  cevath  29858  kcnktkm1cn  30123  clwlkisclwwlk  30404  frghash2spot  30609  usgreghash2spotv  30612  frgregordn0  30616  numclwlk3lem3  30619  numclwlk1lem2fo  30641  sinhpcosh  30964  i2linesd  31018  isosctrlem1ALT  31557  sineq0ALT  31560  bj-lineq  32439  bj-bary1lem  32441  bj-bary1lem1  32442  bj-bary1  32443