Theorem subcld 11570

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7408  ℂcc 11107   − cmin 11443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11249  df-mnf 11250  df-ltxr 11252  df-sub 11445

This theorem is referenced by:  pnpncand  11634  muleqadd  11857  lineq  12050  modmuladdnn0  13879  hashfz  14386  hashfzo  14388  hashf1lem2  14416  hashf1  14417  ccatswrd  14617  pfxccatin12lem2  14680  crre  15060  remim  15063  remullem  15074  abs3lem  15284  caubnd2  15303  bhmafibid1cn  15409  bhmafibid2cn  15410  bhmafibid2  15412  rlimuni  15493  climuni  15495  rlimcld2  15521  rlimrege0  15522  rlimrecl  15523  mulcn2  15539  reccn2  15540  cn1lem  15541  o1sub  15559  rlimo1  15560  o1dif  15573  rlimsqzlem  15594  caucvgrlem2  15620  iseralt  15630  fsumparts  15751  cvgcmpce  15763  incexclem  15781  arisum2  15806  geoserg  15811  pwdif  15813  geo2sum2  15819  fallfacfwd  15979  binomfallfaclem2  15983  bpolycl  15995  bpoly3  16001  bpoly4  16002  fsumcube  16003  sinf  16066  tanval2  16075  tanval3  16076  sinneg  16088  efival  16094  sinhval  16096  bitsinv1lem  16381  bitsres  16413  pythagtriplem1  16748  pythagtriplem14  16760  pythagtriplem17  16763  dvdsprmpweqle  16818  4sqlem5  16874  mul4sqlem  16885  4sqlem17  16893  vdwlem5  16917  vdwlem6  16918  vdwlem8  16920  blcvx  24313  recld2  24329  addcnlem  24379  cnllycmp  24471  cphipval2  24757  4cphipval2  24758  cphipval  24759  ipcnlem2  24760  rrxmval  24921  rrxmetlem  24923  pjthlem1  24953  ovollb2lem  25004  itgcnlem  25306  dvlem  25412  dvconst  25433  dvid  25434  dvcnp2  25436  dvaddbr  25454  dvmulbr  25455  dvcobr  25462  dvcjbr  25465  dvrec  25471  dvmptim  25486  dvcnvlem  25492  dveflem  25495  dvsincos  25497  cmvth  25507  dvlip  25509  dvlipcn  25510  c1liplem1  25512  dveq0  25516  dv11cn  25517  dvle  25523  lhop1lem  25529  dvfsumabs  25539  dvfsumlem1  25542  dvfsumlem2  25543  dvfsumrlim  25547  dvfsumrlim2  25548  ftc1lem4  25555  ftc1lem5  25556  ftc2  25560  dgrcolem2  25787  plydiveu  25810  aaliou2b  25853  taylfvallem1  25868  taylply2  25879  dvtaylp  25881  dvntaylp  25882  taylthlem1  25884  taylthlem2  25885  ulmbdd  25909  ulmcn  25910  ulmdvlem1  25911  mtest  25915  iblulm  25918  itgulm  25919  abelthlem9  25951  ptolemy  26005  tangtx  26014  sineq0  26032  efeq1  26036  efif1olem4  26053  tanarg  26126  logcnlem3  26151  logcnlem4  26152  advlogexp  26162  efopn  26165  cxpcn3lem  26252  cxpeq  26262  ang180lem4  26314  ang180lem5  26315  ang180  26316  isosctrlem2  26321  isosctrlem3  26322  isosctr  26323  ssscongptld  26324  affineequiv  26325  affineequiv2  26326  affineequiv3  26327  affineequiv4  26328  affineequivne  26329  angpieqvdlem  26330  angpieqvdlem2  26331  angpined  26332  angpieqvd  26333  chordthmlem  26334  chordthmlem2  26335  chordthmlem3  26336  chordthmlem4  26337  chordthmlem5  26338  heron  26340  quad2  26341  quad  26342  dcubic1lem  26345  dcubic  26348  mcubic  26349  cubic2  26350  cubic  26351  dquartlem1  26353  dquartlem2  26354  dquart  26355  quart1cl  26356  quart1lem  26357  quart1  26358  quartlem2  26360  quartlem4  26362  quart  26363  atanf  26382  sinasin  26391  asinsin  26394  atanneg  26409  atancj  26412  efiatan  26414  atanlogsub  26418  efiatan2  26419  2efiatan  26420  atanbndlem  26427  dvatan  26437  atantayl  26439  lgamgulmlem2  26531  lgamgulmlem3  26532  lgamgulmlem5  26534  lgamgulmlem6  26535  lgamgulm2  26537  lgamucov  26539  lgamcvg2  26556  gamcvg  26557  gamcvg2lem  26560  ftalem2  26575  logfacrlim  26724  logexprlim  26725  lgsdirprm  26831  gausslemma2dlem1a  26865  gausslemma2dlem4  26869  2sqmod  26936  addsq2nreurex  26944  vmadivsum  26982  rpvmasumlem  26987  dchrisumlem2  26990  dchrisumlem3  26991  dchrmusum2  26994  dchrvmasumlem2  26998  dchrvmasumlem3  26999  dchrvmasumiflem1  27001  rpvmasum2  27012  dchrisum0lem1b  27015  dchrisum0lem1  27016  dchrisum0lem2a  27017  rplogsum  27027  mudivsum  27030  mulogsumlem  27031  mulogsum  27032  mulog2sumlem1  27034  mulog2sumlem2  27035  mulog2sumlem3  27036  vmalogdivsum2  27038  vmalogdivsum  27039  2vmadivsumlem  27040  selberglem1  27045  selberglem2  27046  selberg2lem  27050  selberg2  27051  selberg3lem1  27057  selberg4lem1  27060  selberg4  27061  pntrsumo1  27065  selberg3r  27069  selberg34r  27071  pntrlog2bndlem1  27077  pntrlog2bndlem2  27078  pntrlog2bndlem3  27079  pntrlog2bndlem4  27080  pntrlog2bndlem5  27081  pntibndlem2  27091  pntlemf  27105  pntlemo  27107  ttgcontlem1  28139  brbtwn2  28160  colinearalglem1  28161  colinearalglem2  28162  colinearalg  28165  axsegconlem1  28172  ax5seglem1  28183  ax5seglem2  28184  ax5seglem6  28189  ax5seglem9  28192  axlowdimlem17  28213  axcontlem7  28225  axcontlem8  28226  clwlkclwwlk  29252  clwwlknonex2lem1  29357  2clwwlk2clwwlk  29600  numclwwlk3lem1  29632  smcnlem  29945  ipval2  29955  4ipval2  29956  dipcj  29962  pjhthlem1  30639  lt2addrd  31959  bcm1n  32001  cycpmco2lem5  32284  cycpmco2lem6  32285  sqsscirc2  32884  signslema  33568  circlemeth  33647  logdivsqrle  33657  revpfxsfxrev  34101  revwlk  34110  subfaclim  34174  divcnvlin  34697  iprodgam  34707  gg-dvcnp2  35169  gg-dvmulbr  35170  gg-dvcobr  35171  gg-cmvth  35176  gg-dvfsumlem2  35178  dnicld1  35343  dnibndlem2  35350  dnibndlem3  35351  dnibndlem6  35354  dnibndlem9  35357  dnibndlem10  35358  dnibndlem11  35359  unblimceq0  35378  unbdqndv2lem1  35380  unbdqndv2lem2  35381  knoppndvlem11  35393  knoppndvlem15  35397  knoppndvlem17  35399  knoppndvlem21  35403  bj-bary1lem  36186  bj-bary1lem1  36187  bj-bary1  36188  ftc1cnnclem  36554  ftc1anclem7  36562  ftc1anclem8  36563  ftc1anc  36564  ftc2nc  36565  areacirclem1  36571  areacirclem4  36574  areacirc  36576  cntotbnd  36659  lcmineqlem8  40896  lcmineqlem10  40898  lcmineqlem11  40899  lcmineqlem12  40900  lcmineqlem23  40911  aks4d1p1  40936  sticksstones10  40966  sticksstones12a  40968  sticksstones12  40969  sticksstones22  40979  metakunt15  40994  metakunt16  40995  metakunt29  41008  metakunt30  41009  mvrrsubd  41189  lsubrotld  41192  lsubcom23d  41193  nicomachus  41210  sumcubes  41211  dffltz  41377  fltnltalem  41405  rencldnfilem  41548  pellexlem2  41558  pellexlem6  41562  pell1234qrne0  41581  pell1234qrmulcl  41583  rmyluc  41666  jm2.18  41717  jm2.19  41722  areaquad  41955  lhe4.4ex1a  43078  bcc0  43089  bccp1k  43090  bccm1k  43091  binomcxplemwb  43097  binomcxplemnn0  43098  binomcxplemrat  43099  binomcxplemfrat  43100  binomcxplemdvbinom  43102  binomcxplemnotnn0  43105  isosctrlem1ALT  43685  sineq0ALT  43688  oddfl  43977  dstregt0  43981  subadd4b  43982  sub31  43990  fzisoeu  44000  absnpncan2d  44002  absnpncan3d  44007  supxrgelem  44037  absimlere  44180  cvgcaule  44192  mullimc  44322  ellimcabssub0  44323  mullimcf  44329  limcrecl  44335  lptre2pt  44346  limcleqr  44350  neglimc  44353  addlimc  44354  0ellimcdiv  44355  limclner  44357  reclimc  44359  climleltrp  44382  climisp  44452  climxrrelem  44455  climxrre  44456  cnrefiisplem  44535  climxlim2lem  44551  fprodsubrecnncnvlem  44613  fperdvper  44625  dvdivbd  44629  dvbdfbdioolem2  44635  ioodvbdlimc1lem1  44637  volioc  44678  volico  44689  stoweidlem1  44707  stoweidlem11  44717  stoweidlem13  44719  stoweidlem26  44732  stoweid  44769  wallispi  44776  wallispi2lem1  44777  wallispi2lem2  44778  wallispi2  44779  stirlinglem1  44780  stirlinglem4  44783  stirlinglem5  44784  stirlinglem7  44786  stirlinglem11  44790  dirkertrigeqlem2  44805  fourierdlem4  44817  fourierdlem26  44839  fourierdlem30  44843  fourierdlem42  44855  fourierdlem63  44875  fourierdlem65  44877  fourierdlem72  44884  fourierdlem74  44886  fourierdlem75  44887  fourierdlem76  44888  fourierdlem80  44892  fourierdlem81  44893  fourierdlem89  44901  fourierdlem90  44902  fourierdlem91  44903  fourierdlem107  44919  fourierdlem109  44921  fouriersw  44937  etransclem1  44941  etransclem4  44944  etransclem8  44948  etransclem18  44958  etransclem20  44960  etransclem21  44961  etransclem23  44963  etransclem35  44975  etransclem46  44986  rrxtopnfi  44993  rrndistlt  44996  sge0gtfsumgt  45149  hoidmv1lelem2  45298  hoidmvlelem2  45302  smfmullem1  45497  sigarmf  45560  sigarms  45562  sigarexp  45565  sigardiv  45567  sigarcol  45570  sharhght  45571  sigaradd  45572  cevathlem2  45574  cevath  45575  resubcnnred  46002  fmtnorec2lem  46200  fmtnorec3  46206  fmtnorec4  46207  lighneallem3  46265  quad1  46278  requad01  46279  requad2  46281  fppr2odd  46389  fldivmod  47194  dignn0flhalflem2  47292  affinecomb2  47379  1subrec1sub  47381  eenglngeehlnmlem1  47413  eenglngeehlnmlem2  47414  rrx2vlinest  47417  rrx2linest  47418  line2  47428  itsclc0yqsollem1  47438  itsclc0yqsol  47440  itscnhlc0xyqsol  47441  itschlc0xyqsol1  47442  itschlc0xyqsol  47443  itsclc0xyqsolr  47445  2itscplem1  47454  2itscplem2  47455  2itscplem3  47456  itscnhlinecirc02plem1  47458  inlinecirc02plem  47462  sinhpcosh  47775  i2linesd  47816