Theorem subcld 11262

Description: Closure law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
pncand.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
subcld	⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)

Proof of Theorem subcld

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		pncand.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		subcl 11150	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 583	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   − cmin 11135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945  df-sub 11137

This theorem is referenced by:  pnpncand  11326  muleqadd  11549  lineq  11742  modmuladdnn0  13563  hashfz  14070  hashfzo  14072  hashf1lem2  14098  hashf1  14099  ccatswrd  14309  pfxccatin12lem2  14372  crre  14753  remim  14756  remullem  14767  abs3lem  14978  caubnd2  14997  bhmafibid1cn  15103  bhmafibid2cn  15104  bhmafibid2  15106  rlimuni  15187  climuni  15189  rlimcld2  15215  rlimrege0  15216  rlimrecl  15217  mulcn2  15233  reccn2  15234  cn1lem  15235  o1sub  15253  rlimo1  15254  o1dif  15267  rlimsqzlem  15288  caucvgrlem2  15314  iseralt  15324  fsumparts  15446  cvgcmpce  15458  incexclem  15476  arisum2  15501  geoserg  15506  pwdif  15508  geo2sum2  15514  fallfacfwd  15674  binomfallfaclem2  15678  bpolycl  15690  bpoly3  15696  bpoly4  15697  fsumcube  15698  sinf  15761  tanval2  15770  tanval3  15771  sinneg  15783  efival  15789  sinhval  15791  bitsinv1lem  16076  bitsres  16108  pythagtriplem1  16445  pythagtriplem14  16457  pythagtriplem17  16460  dvdsprmpweqle  16515  4sqlem5  16571  mul4sqlem  16582  4sqlem17  16590  vdwlem5  16614  vdwlem6  16615  vdwlem8  16617  blcvx  23867  recld2  23883  addcnlem  23933  cnllycmp  24025  cphipval2  24310  4cphipval2  24311  cphipval  24312  ipcnlem2  24313  rrxmval  24474  rrxmetlem  24476  pjthlem1  24506  ovollb2lem  24557  itgcnlem  24859  dvlem  24965  dvconst  24986  dvid  24987  dvcnp2  24989  dvaddbr  25007  dvmulbr  25008  dvcobr  25015  dvcjbr  25018  dvrec  25024  dvmptim  25039  dvcnvlem  25045  dveflem  25048  dvsincos  25050  cmvth  25060  dvlip  25062  dvlipcn  25063  c1liplem1  25065  dveq0  25069  dv11cn  25070  dvle  25076  lhop1lem  25082  dvfsumabs  25092  dvfsumlem1  25095  dvfsumlem2  25096  dvfsumrlim  25100  dvfsumrlim2  25101  ftc1lem4  25108  ftc1lem5  25109  ftc2  25113  dgrcolem2  25340  plydiveu  25363  aaliou2b  25406  taylfvallem1  25421  taylply2  25432  dvtaylp  25434  dvntaylp  25435  taylthlem1  25437  taylthlem2  25438  ulmbdd  25462  ulmcn  25463  ulmdvlem1  25464  mtest  25468  iblulm  25471  itgulm  25472  abelthlem9  25504  ptolemy  25558  tangtx  25567  sineq0  25585  efeq1  25589  efif1olem4  25606  tanarg  25679  logcnlem3  25704  logcnlem4  25705  advlogexp  25715  efopn  25718  cxpcn3lem  25805  cxpeq  25815  ang180lem4  25867  ang180lem5  25868  ang180  25869  isosctrlem2  25874  isosctrlem3  25875  isosctr  25876  ssscongptld  25877  affineequiv  25878  affineequiv2  25879  affineequiv3  25880  affineequiv4  25881  affineequivne  25882  angpieqvdlem  25883  angpieqvdlem2  25884  angpined  25885  angpieqvd  25886  chordthmlem  25887  chordthmlem2  25888  chordthmlem3  25889  chordthmlem4  25890  chordthmlem5  25891  heron  25893  quad2  25894  quad  25895  dcubic1lem  25898  dcubic  25901  mcubic  25902  cubic2  25903  cubic  25904  dquartlem1  25906  dquartlem2  25907  dquart  25908  quart1cl  25909  quart1lem  25910  quart1  25911  quartlem2  25913  quartlem4  25915  quart  25916  atanf  25935  sinasin  25944  asinsin  25947  atanneg  25962  atancj  25965  efiatan  25967  atanlogsub  25971  efiatan2  25972  2efiatan  25973  atanbndlem  25980  dvatan  25990  atantayl  25992  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem5  26087  lgamgulmlem6  26088  lgamgulm2  26090  lgamucov  26092  lgamcvg2  26109  gamcvg  26110  gamcvg2lem  26113  ftalem2  26128  logfacrlim  26277  logexprlim  26278  lgsdirprm  26384  gausslemma2dlem1a  26418  gausslemma2dlem4  26422  2sqmod  26489  addsq2nreurex  26497  vmadivsum  26535  rpvmasumlem  26540  dchrisumlem2  26543  dchrisumlem3  26544  dchrmusum2  26547  dchrvmasumlem2  26551  dchrvmasumlem3  26552  dchrvmasumiflem1  26554  rpvmasum2  26565  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2a  26570  rplogsum  26580  mudivsum  26583  mulogsumlem  26584  mulogsum  26585  mulog2sumlem1  26587  mulog2sumlem2  26588  mulog2sumlem3  26589  vmalogdivsum2  26591  vmalogdivsum  26592  2vmadivsumlem  26593  selberglem1  26598  selberglem2  26599  selberg2lem  26603  selberg2  26604  selberg3lem1  26610  selberg4lem1  26613  selberg4  26614  pntrsumo1  26618  selberg3r  26622  selberg34r  26624  pntrlog2bndlem1  26630  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntibndlem2  26644  pntlemf  26658  pntlemo  26660  ttgcontlem1  27155  brbtwn2  27176  colinearalglem1  27177  colinearalglem2  27178  colinearalg  27181  axsegconlem1  27188  ax5seglem1  27199  ax5seglem2  27200  ax5seglem6  27205  ax5seglem9  27208  axlowdimlem17  27229  axcontlem7  27241  axcontlem8  27242  clwlkclwwlk  28267  clwwlknonex2lem1  28372  2clwwlk2clwwlk  28615  numclwwlk3lem1  28647  smcnlem  28960  ipval2  28970  4ipval2  28971  dipcj  28977  pjhthlem1  29654  lt2addrd  30976  bcm1n  31018  cycpmco2lem5  31299  cycpmco2lem6  31300  sqsscirc2  31761  signslema  32441  circlemeth  32520  logdivsqrle  32530  revpfxsfxrev  32977  revwlk  32986  subfaclim  33050  divcnvlin  33604  iprodgam  33614  dnicld1  34579  dnibndlem2  34586  dnibndlem3  34587  dnibndlem6  34590  dnibndlem9  34593  dnibndlem10  34594  dnibndlem11  34595  unblimceq0  34614  unbdqndv2lem1  34616  unbdqndv2lem2  34617  knoppndvlem11  34629  knoppndvlem15  34633  knoppndvlem17  34635  knoppndvlem21  34639  bj-bary1lem  35408  bj-bary1lem1  35409  bj-bary1  35410  ftc1cnnclem  35775  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  ftc2nc  35786  areacirclem1  35792  areacirclem4  35795  areacirc  35797  cntotbnd  35881  lcmineqlem8  39972  lcmineqlem10  39974  lcmineqlem11  39975  lcmineqlem12  39976  lcmineqlem23  39987  aks4d1p1  40012  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  sticksstones22  40052  metakunt15  40067  metakunt16  40068  metakunt29  40081  metakunt30  40082  mvrrsubd  40224  lsubrotld  40227  lsubcom23d  40228  dffltz  40387  fltnltalem  40415  rencldnfilem  40558  pellexlem2  40568  pellexlem6  40572  pell1234qrne0  40591  pell1234qrmulcl  40593  rmyluc  40675  jm2.18  40726  jm2.19  40731  areaquad  40963  lhe4.4ex1a  41836  bcc0  41847  bccp1k  41848  bccm1k  41849  binomcxplemwb  41855  binomcxplemnn0  41856  binomcxplemrat  41857  binomcxplemfrat  41858  binomcxplemdvbinom  41860  binomcxplemnotnn0  41863  isosctrlem1ALT  42443  sineq0ALT  42446  oddfl  42705  dstregt0  42709  subadd4b  42710  sub31  42719  fzisoeu  42729  absnpncan2d  42731  absnpncan3d  42736  supxrgelem  42766  absimlere  42910  mullimc  43047  ellimcabssub0  43048  mullimcf  43054  limcrecl  43060  lptre2pt  43071  limcleqr  43075  neglimc  43078  addlimc  43079  0ellimcdiv  43080  limclner  43082  reclimc  43084  climleltrp  43107  climisp  43177  climxrrelem  43180  climxrre  43181  cnrefiisplem  43260  climxlim2lem  43276  fprodsubrecnncnvlem  43338  fperdvper  43350  dvdivbd  43354  dvbdfbdioolem2  43360  ioodvbdlimc1lem1  43362  volioc  43403  volico  43414  stoweidlem1  43432  stoweidlem11  43442  stoweidlem13  43444  stoweidlem26  43457  stoweid  43494  wallispi  43501  wallispi2lem1  43502  wallispi2lem2  43503  wallispi2  43504  stirlinglem1  43505  stirlinglem4  43508  stirlinglem5  43509  stirlinglem7  43511  stirlinglem11  43515  dirkertrigeqlem2  43530  fourierdlem4  43542  fourierdlem26  43564  fourierdlem30  43568  fourierdlem42  43580  fourierdlem63  43600  fourierdlem65  43602  fourierdlem72  43609  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem80  43617  fourierdlem81  43618  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem107  43644  fourierdlem109  43646  fouriersw  43662  etransclem1  43666  etransclem4  43669  etransclem8  43673  etransclem18  43683  etransclem20  43685  etransclem21  43686  etransclem23  43688  etransclem35  43700  etransclem46  43711  rrxtopnfi  43718  rrndistlt  43721  sge0gtfsumgt  43871  hoidmv1lelem2  44020  hoidmvlelem2  44024  smfmullem1  44212  sigarmf  44257  sigarms  44259  sigarexp  44262  sigardiv  44264  sigarcol  44267  sharhght  44268  sigaradd  44269  cevathlem2  44271  cevath  44272  resubcnnred  44684  fmtnorec2lem  44882  fmtnorec3  44888  fmtnorec4  44889  lighneallem3  44947  quad1  44960  requad01  44961  requad2  44963  fppr2odd  45071  fldivmod  45752  dignn0flhalflem2  45850  affinecomb2  45937  1subrec1sub  45939  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  rrx2vlinest  45975  rrx2linest  45976  line2  45986  itsclc0yqsollem1  45996  itsclc0yqsol  45998  itscnhlc0xyqsol  45999  itschlc0xyqsol1  46000  itschlc0xyqsol  46001  itsclc0xyqsolr  46003  2itscplem1  46012  2itscplem2  46013  2itscplem3  46014  itscnhlinecirc02plem1  46016  inlinecirc02plem  46020  sinhpcosh  46328  i2linesd  46369