Theorem subcld 11472

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 11359	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004   − cmin 11344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-ltxr 11151  df-sub 11346

This theorem is referenced by:  subsubadd23  11524  addsubsub23  11525  pnpncand  11538  muleqadd  11761  lineq  11958  modmuladdnn0  13822  hashfz  14334  hashfzo  14336  hashf1lem2  14363  hashf1  14364  ccatswrd  14576  pfxccatin12lem2  14638  crre  15021  remim  15024  remullem  15035  abs3lem  15246  caubnd2  15265  bhmafibid1cn  15373  bhmafibid2cn  15374  bhmafibid2  15376  rlimuni  15457  climuni  15459  rlimcld2  15485  rlimrege0  15486  rlimrecl  15487  mulcn2  15503  reccn2  15504  cn1lem  15505  o1sub  15523  rlimo1  15524  o1dif  15537  rlimsqzlem  15556  caucvgrlem2  15582  iseralt  15592  fsumparts  15713  cvgcmpce  15725  incexclem  15743  arisum2  15768  geoserg  15773  pwdif  15775  geo2sum2  15781  fallfacfwd  15943  binomfallfaclem2  15947  bpolycl  15959  bpoly3  15965  bpoly4  15966  fsumcube  15967  sinf  16033  tanval2  16042  tanval3  16043  sinneg  16055  efival  16061  sinhval  16063  bitsinv1lem  16352  bitsres  16384  pythagtriplem1  16728  pythagtriplem14  16740  pythagtriplem17  16743  dvdsprmpweqle  16798  4sqlem5  16854  mul4sqlem  16865  4sqlem17  16873  vdwlem5  16897  vdwlem6  16898  vdwlem8  16900  blcvx  24713  recld2  24730  addcnlem  24780  cnllycmp  24882  cphipval2  25168  4cphipval2  25169  cphipval  25170  ipcnlem2  25171  rrxmval  25332  rrxmetlem  25334  pjthlem1  25364  ovollb2lem  25416  itgcnlem  25718  dvlem  25824  dvconst  25845  dvid  25846  dvcnp2  25848  dvcnp2OLD  25849  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvcobr  25876  dvcobrOLD  25877  dvcjbr  25880  dvrec  25886  dvmptim  25901  dvcnvlem  25907  dveflem  25910  dvsincos  25912  cmvth  25922  cmvthOLD  25923  dvlip  25925  dvlipcn  25926  c1liplem1  25928  dveq0  25932  dv11cn  25933  dvle  25939  lhop1lem  25945  dvfsumabs  25956  dvfsumlem1  25959  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumrlim  25965  dvfsumrlim2  25966  ftc1lem4  25973  ftc1lem5  25974  ftc2  25978  dgrcolem2  26207  plydiveu  26233  aaliou2b  26276  taylfvallem1  26291  taylply2  26302  taylply2OLD  26303  dvtaylp  26305  dvntaylp  26306  taylthlem1  26308  taylthlem2  26309  taylthlem2OLD  26310  ulmbdd  26334  ulmcn  26335  ulmdvlem1  26336  mtest  26340  iblulm  26343  itgulm  26344  abelthlem9  26377  ptolemy  26432  tangtx  26441  sineq0  26460  efeq1  26464  efif1olem4  26481  tanarg  26555  logcnlem3  26580  logcnlem4  26581  advlogexp  26591  efopn  26594  cxpcn3lem  26684  cxpeq  26694  ang180lem4  26749  ang180lem5  26750  ang180  26751  isosctrlem2  26756  isosctrlem3  26757  isosctr  26758  ssscongptld  26759  affineequiv  26760  affineequiv2  26761  affineequiv3  26762  affineequiv4  26763  affineequivne  26764  angpieqvdlem  26765  angpieqvdlem2  26766  angpined  26767  angpieqvd  26768  chordthmlem  26769  chordthmlem2  26770  chordthmlem3  26771  chordthmlem4  26772  chordthmlem5  26773  heron  26775  quad2  26776  quad  26777  dcubic1lem  26780  dcubic  26783  mcubic  26784  cubic2  26785  cubic  26786  dquartlem1  26788  dquartlem2  26789  dquart  26790  quart1cl  26791  quart1lem  26792  quart1  26793  quartlem2  26795  quartlem4  26797  quart  26798  atanf  26817  sinasin  26826  asinsin  26829  atanneg  26844  atancj  26847  efiatan  26849  atanlogsub  26853  efiatan2  26854  2efiatan  26855  atanbndlem  26862  dvatan  26872  atantayl  26874  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamgulmlem5  26970  lgamgulmlem6  26971  lgamgulm2  26973  lgamucov  26975  lgamcvg2  26992  gamcvg  26993  gamcvg2lem  26996  ftalem2  27011  logfacrlim  27162  logexprlim  27163  lgsdirprm  27269  gausslemma2dlem1a  27303  gausslemma2dlem4  27307  2sqmod  27374  addsq2nreurex  27382  vmadivsum  27420  rpvmasumlem  27425  dchrisumlem2  27428  dchrisumlem3  27429  dchrmusum2  27432  dchrvmasumlem2  27436  dchrvmasumlem3  27437  dchrvmasumiflem1  27439  rpvmasum2  27450  dchrisum0lem1b  27453  dchrisum0lem1  27454  dchrisum0lem2a  27455  rplogsum  27465  mudivsum  27468  mulogsumlem  27469  mulogsum  27470  mulog2sumlem1  27472  mulog2sumlem2  27473  mulog2sumlem3  27474  vmalogdivsum2  27476  vmalogdivsum  27477  2vmadivsumlem  27478  selberglem1  27483  selberglem2  27484  selberg2lem  27488  selberg2  27489  selberg3lem1  27495  selberg4lem1  27498  selberg4  27499  pntrsumo1  27503  selberg3r  27507  selberg34r  27509  pntrlog2bndlem1  27515  pntrlog2bndlem2  27516  pntrlog2bndlem3  27517  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntibndlem2  27529  pntlemf  27543  pntlemo  27545  ttgcontlem1  28863  brbtwn2  28883  colinearalglem1  28884  colinearalglem2  28885  colinearalg  28888  axsegconlem1  28895  ax5seglem1  28906  ax5seglem2  28907  ax5seglem6  28912  ax5seglem9  28915  axlowdimlem17  28936  axcontlem7  28948  axcontlem8  28949  clwlkclwwlk  29982  clwwlknonex2lem1  30087  2clwwlk2clwwlk  30330  numclwwlk3lem1  30362  smcnlem  30677  ipval2  30687  4ipval2  30688  dipcj  30694  pjhthlem1  31371  submuladdd  32723  binom2subadd  32725  pythagreim  32729  quad3d  32733  lt2addrd  32734  bcm1n  32777  cycpmco2lem5  33099  cycpmco2lem6  33100  constrrtll  33744  constrrtlc1  33745  constrrtcclem  33747  constrrtcc  33748  constrsslem  33754  constrconj  33758  constrfin  33759  constrelextdg2  33760  constraddcl  33775  iconstr  33779  constrremulcl  33780  constrrecl  33782  constrmulcl  33784  constrreinvcl  33785  constrresqrtcl  33790  cos9thpiminplylem2  33796  cos9thpiminplylem3  33797  sqsscirc2  33922  signslema  34575  circlemeth  34653  logdivsqrle  34663  revpfxsfxrev  35160  revwlk  35169  subfaclim  35232  divcnvlin  35777  iprodgam  35786  dnicld1  36516  dnibndlem2  36523  dnibndlem3  36524  dnibndlem6  36527  dnibndlem9  36530  dnibndlem10  36531  dnibndlem11  36532  unblimceq0  36551  unbdqndv2lem1  36553  unbdqndv2lem2  36554  knoppndvlem11  36566  knoppndvlem15  36570  knoppndvlem17  36572  knoppndvlem21  36576  bj-bary1lem  37354  bj-bary1lem1  37355  bj-bary1  37356  ftc1cnnclem  37741  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751  ftc2nc  37752  areacirclem1  37758  areacirclem4  37761  areacirc  37763  cntotbnd  37846  lcmineqlem8  42139  lcmineqlem10  42141  lcmineqlem11  42142  lcmineqlem12  42143  lcmineqlem23  42154  aks4d1p1  42179  aks6d1c5lem1  42239  sticksstones10  42258  sticksstones12a  42260  sticksstones12  42261  sticksstones22  42271  bcle2d  42282  mvrrsubd  42377  lsubrotld  42380  lsubswap23d  42382  nicomachus  42415  sumcubes  42416  ef11d  42442  tanhalfpim  42452  sinpim  42453  cospim  42454  dffltz  42737  fltnltalem  42765  rencldnfilem  42923  pellexlem2  42933  pellexlem6  42937  pell1234qrne0  42956  pell1234qrmulcl  42958  rmyluc  43040  jm2.18  43091  jm2.19  43096  areaquad  43319  lhe4.4ex1a  44432  bcc0  44443  bccp1k  44444  bccm1k  44445  binomcxplemwb  44451  binomcxplemnn0  44452  binomcxplemrat  44453  binomcxplemfrat  44454  binomcxplemdvbinom  44456  binomcxplemnotnn0  44459  isosctrlem1ALT  45036  sineq0ALT  45039  oddfl  45389  dstregt0  45393  subadd4b  45394  sub31  45401  fzisoeu  45411  absnpncan2d  45413  absnpncan3d  45418  supxrgelem  45446  absimlere  45587  cvgcaule  45599  mullimc  45726  ellimcabssub0  45727  mullimcf  45733  limcrecl  45739  lptre2pt  45748  limcleqr  45752  neglimc  45755  addlimc  45756  0ellimcdiv  45757  limclner  45759  reclimc  45761  climleltrp  45784  climisp  45854  climxrrelem  45857  climxrre  45858  cnrefiisplem  45937  climxlim2lem  45953  fprodsubrecnncnvlem  46015  fperdvper  46027  dvdivbd  46031  dvbdfbdioolem2  46037  ioodvbdlimc1lem1  46039  volioc  46080  volico  46091  stoweidlem1  46109  stoweidlem11  46119  stoweidlem13  46121  stoweidlem26  46134  stoweid  46171  wallispi  46178  wallispi2lem1  46179  wallispi2lem2  46180  wallispi2  46181  stirlinglem1  46182  stirlinglem4  46185  stirlinglem5  46186  stirlinglem7  46188  stirlinglem11  46192  dirkertrigeqlem2  46207  fourierdlem4  46219  fourierdlem26  46241  fourierdlem30  46245  fourierdlem42  46257  fourierdlem63  46277  fourierdlem65  46279  fourierdlem72  46286  fourierdlem74  46288  fourierdlem75  46289  fourierdlem76  46290  fourierdlem80  46294  fourierdlem81  46295  fourierdlem89  46303  fourierdlem90  46304  fourierdlem91  46305  fourierdlem107  46321  fourierdlem109  46323  fouriersw  46339  etransclem1  46343  etransclem4  46346  etransclem8  46350  etransclem18  46360  etransclem20  46362  etransclem21  46363  etransclem23  46365  etransclem35  46377  etransclem46  46388  rrxtopnfi  46395  rrndistlt  46398  sge0gtfsumgt  46551  hoidmv1lelem2  46700  hoidmvlelem2  46704  smfmullem1  46899  sigarmf  46962  sigarms  46964  sigarexp  46967  sigardiv  46969  sigarcol  46972  sharhght  46973  sigaradd  46974  cevathlem2  46976  cevath  46977  resubcnnred  47414  fldivmod  47448  ceildivmod  47449  fmtnorec2lem  47652  fmtnorec3  47658  fmtnorec4  47659  lighneallem3  47717  quad1  47730  requad01  47731  requad2  47733  fppr2odd  47841  dignn0flhalflem2  48727  affinecomb2  48814  1subrec1sub  48816  eenglngeehlnmlem1  48848  eenglngeehlnmlem2  48849  rrx2vlinest  48852  rrx2linest  48853  line2  48863  itsclc0yqsollem1  48873  itsclc0yqsol  48875  itscnhlc0xyqsol  48876  itschlc0xyqsol1  48877  itschlc0xyqsol  48878  itsclc0xyqsolr  48880  2itscplem1  48889  2itscplem2  48890  2itscplem3  48891  itscnhlinecirc02plem1  48893  inlinecirc02plem  48897  sinhpcosh  49851  i2linesd  49890