Theorem subcld 10997

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   − cmin 10870

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-po 5474  df-so 5475  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-ltxr 10680  df-sub 10872

This theorem is referenced by:  pnpncand  11061  muleqadd  11284  lineq  11477  modmuladdnn0  13284  hashfz  13789  hashfzo  13791  hashf1lem2  13815  hashf1  13816  ccatswrd  14030  pfxccatin12lem2  14093  crre  14473  remim  14476  remullem  14487  abs3lem  14698  caubnd2  14717  bhmafibid1cn  14823  bhmafibid2cn  14824  bhmafibid2  14826  rlimuni  14907  climuni  14909  rlimcld2  14935  rlimrege0  14936  rlimrecl  14937  mulcn2  14952  reccn2  14953  cn1lem  14954  o1sub  14972  rlimo1  14973  o1dif  14986  rlimsqzlem  15005  caucvgrlem2  15031  iseralt  15041  fsumparts  15161  cvgcmpce  15173  incexclem  15191  arisum2  15216  geoserg  15221  pwdif  15223  geo2sum2  15230  fallfacfwd  15390  binomfallfaclem2  15394  bpolycl  15406  bpoly3  15412  bpoly4  15413  fsumcube  15414  sinf  15477  tanval2  15486  tanval3  15487  sinneg  15499  efival  15505  sinhval  15507  bitsinv1lem  15790  bitsres  15822  pythagtriplem1  16153  pythagtriplem14  16165  pythagtriplem17  16168  dvdsprmpweqle  16222  4sqlem5  16278  mul4sqlem  16289  4sqlem17  16297  vdwlem5  16321  vdwlem6  16322  vdwlem8  16324  blcvx  23406  recld2  23422  addcnlem  23472  cnllycmp  23560  cphipval2  23844  4cphipval2  23845  cphipval  23846  ipcnlem2  23847  rrxmval  24008  rrxmetlem  24010  pjthlem1  24040  ovollb2lem  24089  itgcnlem  24390  dvlem  24494  dvconst  24514  dvid  24515  dvcnp2  24517  dvaddbr  24535  dvmulbr  24536  dvcobr  24543  dvcjbr  24546  dvrec  24552  dvmptim  24567  dvcnvlem  24573  dveflem  24576  dvsincos  24578  cmvth  24588  dvlip  24590  dvlipcn  24591  c1liplem1  24593  dveq0  24597  dv11cn  24598  dvle  24604  lhop1lem  24610  dvfsumabs  24620  dvfsumlem1  24623  dvfsumlem2  24624  dvfsumrlim  24628  dvfsumrlim2  24629  ftc1lem4  24636  ftc1lem5  24637  ftc2  24641  dgrcolem2  24864  plydiveu  24887  aaliou2b  24930  taylfvallem1  24945  taylply2  24956  dvtaylp  24958  dvntaylp  24959  taylthlem1  24961  taylthlem2  24962  ulmbdd  24986  ulmcn  24987  ulmdvlem1  24988  mtest  24992  iblulm  24995  itgulm  24996  abelthlem9  25028  ptolemy  25082  tangtx  25091  sineq0  25109  efeq1  25113  efif1olem4  25129  tanarg  25202  logcnlem3  25227  logcnlem4  25228  advlogexp  25238  efopn  25241  cxpcn3lem  25328  cxpeq  25338  ang180lem4  25390  ang180lem5  25391  ang180  25392  isosctrlem2  25397  isosctrlem3  25398  isosctr  25399  ssscongptld  25400  affineequiv  25401  affineequiv2  25402  affineequiv3  25403  affineequiv4  25404  affineequivne  25405  angpieqvdlem  25406  angpieqvdlem2  25407  angpined  25408  angpieqvd  25409  chordthmlem  25410  chordthmlem2  25411  chordthmlem3  25412  chordthmlem4  25413  chordthmlem5  25414  heron  25416  quad2  25417  quad  25418  dcubic1lem  25421  dcubic  25424  mcubic  25425  cubic2  25426  cubic  25427  dquartlem1  25429  dquartlem2  25430  dquart  25431  quart1cl  25432  quart1lem  25433  quart1  25434  quartlem2  25436  quartlem4  25438  quart  25439  atanf  25458  sinasin  25467  asinsin  25470  atanneg  25485  atancj  25488  efiatan  25490  atanlogsub  25494  efiatan2  25495  2efiatan  25496  atanbndlem  25503  dvatan  25513  atantayl  25515  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem5  25610  lgamgulmlem6  25611  lgamgulm2  25613  lgamucov  25615  lgamcvg2  25632  gamcvg  25633  gamcvg2lem  25636  ftalem2  25651  logfacrlim  25800  logexprlim  25801  lgsdirprm  25907  gausslemma2dlem1a  25941  gausslemma2dlem4  25945  2sqmod  26012  addsq2nreurex  26020  vmadivsum  26058  rpvmasumlem  26063  dchrisumlem2  26066  dchrisumlem3  26067  dchrmusum2  26070  dchrvmasumlem2  26074  dchrvmasumlem3  26075  dchrvmasumiflem1  26077  rpvmasum2  26088  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2a  26093  rplogsum  26103  mudivsum  26106  mulogsumlem  26107  mulogsum  26108  mulog2sumlem1  26110  mulog2sumlem2  26111  mulog2sumlem3  26112  vmalogdivsum2  26114  vmalogdivsum  26115  2vmadivsumlem  26116  selberglem1  26121  selberglem2  26122  selberg2lem  26126  selberg2  26127  selberg3lem1  26133  selberg4lem1  26136  selberg4  26137  pntrsumo1  26141  selberg3r  26145  selberg34r  26147  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntibndlem2  26167  pntlemf  26181  pntlemo  26183  ttgcontlem1  26671  brbtwn2  26691  colinearalglem1  26692  colinearalglem2  26693  colinearalg  26696  axsegconlem1  26703  ax5seglem1  26714  ax5seglem2  26715  ax5seglem6  26720  ax5seglem9  26723  axlowdimlem17  26744  axcontlem7  26756  axcontlem8  26757  clwlkclwwlk  27780  clwwlknonex2lem1  27886  2clwwlk2clwwlk  28129  numclwwlk3lem1  28161  smcnlem  28474  ipval2  28484  4ipval2  28485  dipcj  28491  pjhthlem1  29168  lt2addrd  30475  bcm1n  30518  cycpmco2lem5  30772  cycpmco2lem6  30773  sqsscirc2  31152  signslema  31832  circlemeth  31911  logdivsqrle  31921  revpfxsfxrev  32362  revwlk  32371  subfaclim  32435  divcnvlin  32964  iprodgam  32974  dnicld1  33811  dnibndlem2  33818  dnibndlem3  33819  dnibndlem6  33822  dnibndlem9  33825  dnibndlem10  33826  dnibndlem11  33827  unblimceq0  33846  unbdqndv2lem1  33848  unbdqndv2lem2  33849  knoppndvlem11  33861  knoppndvlem15  33865  knoppndvlem17  33867  knoppndvlem21  33871  bj-bary1lem  34594  bj-bary1lem1  34595  bj-bary1  34596  ftc1cnnclem  34980  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  ftc2nc  34991  areacirclem1  34997  areacirclem4  35000  areacirc  35002  cntotbnd  35089  dffltz  39320  fltnltalem  39323  rencldnfilem  39466  pellexlem2  39476  pellexlem6  39480  pell1234qrne0  39499  pell1234qrmulcl  39501  rmyluc  39583  jm2.18  39634  jm2.19  39639  areaquad  39872  lhe4.4ex1a  40710  bcc0  40721  bccp1k  40722  bccm1k  40723  binomcxplemwb  40729  binomcxplemnn0  40730  binomcxplemrat  40731  binomcxplemfrat  40732  binomcxplemdvbinom  40734  binomcxplemnotnn0  40737  isosctrlem1ALT  41317  sineq0ALT  41320  oddfl  41592  dstregt0  41596  subadd4b  41597  sub31  41606  fzisoeu  41616  absnpncan2d  41618  absnpncan3d  41623  supxrgelem  41654  absimlere  41805  mullimc  41946  ellimcabssub0  41947  mullimcf  41953  limcrecl  41959  lptre2pt  41970  limcleqr  41974  neglimc  41977  addlimc  41978  0ellimcdiv  41979  limclner  41981  reclimc  41983  climleltrp  42006  climisp  42076  climxrrelem  42079  climxrre  42080  cnrefiisplem  42159  climxlim2lem  42175  fprodsubrecnncnvlem  42240  fperdvper  42252  dvdivbd  42257  dvbdfbdioolem2  42263  ioodvbdlimc1lem1  42265  volioc  42306  volico  42317  stoweidlem1  42335  stoweidlem11  42345  stoweidlem13  42347  stoweidlem26  42360  stoweid  42397  wallispi  42404  wallispi2lem1  42405  wallispi2lem2  42406  wallispi2  42407  stirlinglem1  42408  stirlinglem4  42411  stirlinglem5  42412  stirlinglem7  42414  stirlinglem11  42418  dirkertrigeqlem2  42433  fourierdlem4  42445  fourierdlem26  42467  fourierdlem30  42471  fourierdlem42  42483  fourierdlem63  42503  fourierdlem65  42505  fourierdlem72  42512  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem80  42520  fourierdlem81  42521  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem107  42547  fourierdlem109  42549  fouriersw  42565  etransclem1  42569  etransclem4  42572  etransclem8  42576  etransclem18  42586  etransclem20  42588  etransclem21  42589  etransclem23  42591  etransclem35  42603  etransclem46  42614  rrxtopnfi  42621  rrndistlt  42624  sge0gtfsumgt  42774  hoidmv1lelem2  42923  hoidmvlelem2  42927  smfmullem1  43115  sigarmf  43160  sigarms  43162  sigarexp  43165  sigardiv  43167  sigarcol  43170  sharhght  43171  sigaradd  43172  cevathlem2  43174  cevath  43175  resubcnnred  43553  fmtnorec2lem  43753  fmtnorec3  43759  fmtnorec4  43760  lighneallem3  43821  quad1  43834  requad01  43835  requad2  43837  fppr2odd  43945  fldivmod  44627  dignn0flhalflem2  44725  affinecomb2  44739  1subrec1sub  44741  eenglngeehlnmlem1  44773  eenglngeehlnmlem2  44774  rrx2vlinest  44777  rrx2linest  44778  line2  44788  itsclc0yqsollem1  44798  itsclc0yqsol  44800  itscnhlc0xyqsol  44801  itschlc0xyqsol1  44802  itschlc0xyqsol  44803  itsclc0xyqsolr  44805  2itscplem1  44814  2itscplem2  44815  2itscplem3  44816  itscnhlinecirc02plem1  44818  inlinecirc02plem  44822  sinhpcosh  44888  i2linesd  44929