Theorem subcld 11490

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7356  ℂcc 11022   − cmin 11362

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-ltxr 11169  df-sub 11364

This theorem is referenced by:  subsubadd23  11542  addsubsub23  11543  pnpncand  11556  muleqadd  11779  lineq  11976  modmuladdnn0  13836  hashfz  14348  hashfzo  14350  hashf1lem2  14377  hashf1  14378  ccatswrd  14590  pfxccatin12lem2  14652  crre  15035  remim  15038  remullem  15049  abs3lem  15260  caubnd2  15279  bhmafibid1cn  15387  bhmafibid2cn  15388  bhmafibid2  15390  rlimuni  15471  climuni  15473  rlimcld2  15499  rlimrege0  15500  rlimrecl  15501  mulcn2  15517  reccn2  15518  cn1lem  15519  o1sub  15537  rlimo1  15538  o1dif  15551  rlimsqzlem  15570  caucvgrlem2  15596  iseralt  15606  fsumparts  15727  cvgcmpce  15739  incexclem  15757  arisum2  15782  geoserg  15787  pwdif  15789  geo2sum2  15795  fallfacfwd  15957  binomfallfaclem2  15961  bpolycl  15973  bpoly3  15979  bpoly4  15980  fsumcube  15981  sinf  16047  tanval2  16056  tanval3  16057  sinneg  16069  efival  16075  sinhval  16077  bitsinv1lem  16366  bitsres  16398  pythagtriplem1  16742  pythagtriplem14  16754  pythagtriplem17  16757  dvdsprmpweqle  16812  4sqlem5  16868  mul4sqlem  16879  4sqlem17  16887  vdwlem5  16911  vdwlem6  16912  vdwlem8  16914  blcvx  24740  recld2  24757  addcnlem  24807  cnllycmp  24909  cphipval2  25195  4cphipval2  25196  cphipval  25197  ipcnlem2  25198  rrxmval  25359  rrxmetlem  25361  pjthlem1  25391  ovollb2lem  25443  itgcnlem  25745  dvlem  25851  dvconst  25872  dvid  25873  dvcnp2  25875  dvcnp2OLD  25876  dvaddbr  25894  dvmulbr  25895  dvmulbrOLD  25896  dvcobr  25903  dvcobrOLD  25904  dvcjbr  25907  dvrec  25913  dvmptim  25928  dvcnvlem  25934  dveflem  25937  dvsincos  25939  cmvth  25949  cmvthOLD  25950  dvlip  25952  dvlipcn  25953  c1liplem1  25955  dveq0  25959  dv11cn  25960  dvle  25966  lhop1lem  25972  dvfsumabs  25983  dvfsumlem1  25986  dvfsumlem2  25987  dvfsumlem2OLD  25988  dvfsumrlim  25992  dvfsumrlim2  25993  ftc1lem4  26000  ftc1lem5  26001  ftc2  26005  dgrcolem2  26234  plydiveu  26260  aaliou2b  26303  taylfvallem1  26318  taylply2  26329  taylply2OLD  26330  dvtaylp  26332  dvntaylp  26333  taylthlem1  26335  taylthlem2  26336  taylthlem2OLD  26337  ulmbdd  26361  ulmcn  26362  ulmdvlem1  26363  mtest  26367  iblulm  26370  itgulm  26371  abelthlem9  26404  ptolemy  26459  tangtx  26468  sineq0  26487  efeq1  26491  efif1olem4  26508  tanarg  26582  logcnlem3  26607  logcnlem4  26608  advlogexp  26618  efopn  26621  cxpcn3lem  26711  cxpeq  26721  ang180lem4  26776  ang180lem5  26777  ang180  26778  isosctrlem2  26783  isosctrlem3  26784  isosctr  26785  ssscongptld  26786  affineequiv  26787  affineequiv2  26788  affineequiv3  26789  affineequiv4  26790  affineequivne  26791  angpieqvdlem  26792  angpieqvdlem2  26793  angpined  26794  angpieqvd  26795  chordthmlem  26796  chordthmlem2  26797  chordthmlem3  26798  chordthmlem4  26799  chordthmlem5  26800  heron  26802  quad2  26803  quad  26804  dcubic1lem  26807  dcubic  26810  mcubic  26811  cubic2  26812  cubic  26813  dquartlem1  26815  dquartlem2  26816  dquart  26817  quart1cl  26818  quart1lem  26819  quart1  26820  quartlem2  26822  quartlem4  26824  quart  26825  atanf  26844  sinasin  26853  asinsin  26856  atanneg  26871  atancj  26874  efiatan  26876  atanlogsub  26880  efiatan2  26881  2efiatan  26882  atanbndlem  26889  dvatan  26899  atantayl  26901  lgamgulmlem2  26994  lgamgulmlem3  26995  lgamgulmlem5  26997  lgamgulmlem6  26998  lgamgulm2  27000  lgamucov  27002  lgamcvg2  27019  gamcvg  27020  gamcvg2lem  27023  ftalem2  27038  logfacrlim  27189  logexprlim  27190  lgsdirprm  27296  gausslemma2dlem1a  27330  gausslemma2dlem4  27334  2sqmod  27401  addsq2nreurex  27409  vmadivsum  27447  rpvmasumlem  27452  dchrisumlem2  27455  dchrisumlem3  27456  dchrmusum2  27459  dchrvmasumlem2  27463  dchrvmasumlem3  27464  dchrvmasumiflem1  27466  rpvmasum2  27477  dchrisum0lem1b  27480  dchrisum0lem1  27481  dchrisum0lem2a  27482  rplogsum  27492  mudivsum  27495  mulogsumlem  27496  mulogsum  27497  mulog2sumlem1  27499  mulog2sumlem2  27500  mulog2sumlem3  27501  vmalogdivsum2  27503  vmalogdivsum  27504  2vmadivsumlem  27505  selberglem1  27510  selberglem2  27511  selberg2lem  27515  selberg2  27516  selberg3lem1  27522  selberg4lem1  27525  selberg4  27526  pntrsumo1  27530  selberg3r  27534  selberg34r  27536  pntrlog2bndlem1  27542  pntrlog2bndlem2  27543  pntrlog2bndlem3  27544  pntrlog2bndlem4  27545  pntrlog2bndlem5  27546  pntibndlem2  27556  pntlemf  27570  pntlemo  27572  ttgcontlem1  28906  brbtwn2  28927  colinearalglem1  28928  colinearalglem2  28929  colinearalg  28932  axsegconlem1  28939  ax5seglem1  28950  ax5seglem2  28951  ax5seglem6  28956  ax5seglem9  28959  axlowdimlem17  28980  axcontlem7  28992  axcontlem8  28993  clwlkclwwlk  30026  clwwlknonex2lem1  30131  2clwwlk2clwwlk  30374  numclwwlk3lem1  30406  smcnlem  30721  ipval2  30731  4ipval2  30732  dipcj  30738  pjhthlem1  31415  submuladdd  32768  binom2subadd  32770  pythagreim  32774  quad3d  32778  lt2addrd  32779  bcm1n  32824  cycpmco2lem5  33161  cycpmco2lem6  33162  vietalem  33684  constrrtll  33837  constrrtlc1  33838  constrrtcclem  33840  constrrtcc  33841  constrsslem  33847  constrconj  33851  constrfin  33852  constrelextdg2  33853  constraddcl  33868  iconstr  33872  constrremulcl  33873  constrrecl  33875  constrmulcl  33877  constrreinvcl  33878  constrresqrtcl  33883  cos9thpiminplylem2  33889  cos9thpiminplylem3  33890  sqsscirc2  34015  signslema  34668  circlemeth  34746  logdivsqrle  34756  revpfxsfxrev  35259  revwlk  35268  subfaclim  35331  divcnvlin  35876  iprodgam  35885  dnicld1  36615  dnibndlem2  36622  dnibndlem3  36623  dnibndlem6  36626  dnibndlem9  36629  dnibndlem10  36630  dnibndlem11  36631  unblimceq0  36650  unbdqndv2lem1  36652  unbdqndv2lem2  36653  knoppndvlem11  36665  knoppndvlem15  36669  knoppndvlem17  36671  knoppndvlem21  36675  bj-bary1lem  37454  bj-bary1lem1  37455  bj-bary1  37456  ftc1cnnclem  37831  ftc1anclem7  37839  ftc1anclem8  37840  ftc1anc  37841  ftc2nc  37842  areacirclem1  37848  areacirclem4  37851  areacirc  37853  cntotbnd  37936  lcmineqlem8  42229  lcmineqlem10  42231  lcmineqlem11  42232  lcmineqlem12  42233  lcmineqlem23  42244  aks4d1p1  42269  aks6d1c5lem1  42329  sticksstones10  42348  sticksstones12a  42350  sticksstones12  42351  sticksstones22  42361  bcle2d  42372  mvrrsubd  42471  lsubrotld  42474  lsubswap23d  42476  nicomachus  42509  sumcubes  42510  ef11d  42536  tanhalfpim  42546  sinpim  42547  cospim  42548  dffltz  42819  fltnltalem  42847  rencldnfilem  43004  pellexlem2  43014  pellexlem6  43018  pell1234qrne0  43037  pell1234qrmulcl  43039  rmyluc  43121  jm2.18  43172  jm2.19  43177  areaquad  43400  lhe4.4ex1a  44512  bcc0  44523  bccp1k  44524  bccm1k  44525  binomcxplemwb  44531  binomcxplemnn0  44532  binomcxplemrat  44533  binomcxplemfrat  44534  binomcxplemdvbinom  44536  binomcxplemnotnn0  44539  isosctrlem1ALT  45116  sineq0ALT  45119  oddfl  45468  dstregt0  45472  subadd4b  45473  sub31  45480  fzisoeu  45490  absnpncan2d  45492  absnpncan3d  45497  supxrgelem  45524  absimlere  45665  cvgcaule  45677  mullimc  45804  ellimcabssub0  45805  mullimcf  45811  limcrecl  45817  lptre2pt  45826  limcleqr  45830  neglimc  45833  addlimc  45834  0ellimcdiv  45835  limclner  45837  reclimc  45839  climleltrp  45862  climisp  45932  climxrrelem  45935  climxrre  45936  cnrefiisplem  46015  climxlim2lem  46031  fprodsubrecnncnvlem  46093  fperdvper  46105  dvdivbd  46109  dvbdfbdioolem2  46115  ioodvbdlimc1lem1  46117  volioc  46158  volico  46169  stoweidlem1  46187  stoweidlem11  46197  stoweidlem13  46199  stoweidlem26  46212  stoweid  46249  wallispi  46256  wallispi2lem1  46257  wallispi2lem2  46258  wallispi2  46259  stirlinglem1  46260  stirlinglem4  46263  stirlinglem5  46264  stirlinglem7  46266  stirlinglem11  46270  dirkertrigeqlem2  46285  fourierdlem4  46297  fourierdlem26  46319  fourierdlem30  46323  fourierdlem42  46335  fourierdlem63  46355  fourierdlem65  46357  fourierdlem72  46364  fourierdlem74  46366  fourierdlem75  46367  fourierdlem76  46368  fourierdlem80  46372  fourierdlem81  46373  fourierdlem89  46381  fourierdlem90  46382  fourierdlem91  46383  fourierdlem107  46399  fourierdlem109  46401  fouriersw  46417  etransclem1  46421  etransclem4  46424  etransclem8  46428  etransclem18  46438  etransclem20  46440  etransclem21  46441  etransclem23  46443  etransclem35  46455  etransclem46  46466  rrxtopnfi  46473  rrndistlt  46476  sge0gtfsumgt  46629  hoidmv1lelem2  46778  hoidmvlelem2  46782  smfmullem1  46977  sigarmf  47040  sigarms  47042  sigarexp  47045  sigardiv  47047  sigarcol  47050  sharhght  47051  sigaradd  47052  cevathlem2  47054  cevath  47055  resubcnnred  47492  fldivmod  47526  ceildivmod  47527  fmtnorec2lem  47730  fmtnorec3  47736  fmtnorec4  47737  lighneallem3  47795  quad1  47808  requad01  47809  requad2  47811  fppr2odd  47919  dignn0flhalflem2  48804  affinecomb2  48891  1subrec1sub  48893  eenglngeehlnmlem1  48925  eenglngeehlnmlem2  48926  rrx2vlinest  48929  rrx2linest  48930  line2  48940  itsclc0yqsollem1  48950  itsclc0yqsol  48952  itscnhlc0xyqsol  48953  itschlc0xyqsol1  48954  itschlc0xyqsol  48955  itsclc0xyqsolr  48957  2itscplem1  48966  2itscplem2  48967  2itscplem3  48968  itscnhlinecirc02plem1  48970  inlinecirc02plem  48974  sinhpcosh  49927  i2linesd  49966