Theorem subcld 11496

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

Syntax hints:   → wi 4   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027   − cmin 11368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-po 5526  df-so 5527  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-sub 11370

This theorem is referenced by:  subsubadd23  11548  addsubsub23  11549  pnpncand  11562  muleqadd  11785  lineq  11983  modmuladdnn0  13868  hashfz  14380  hashfzo  14382  hashf1lem2  14409  hashf1  14410  ccatswrd  14622  pfxccatin12lem2  14684  crre  15067  remim  15070  remullem  15081  abs3lem  15292  caubnd2  15311  bhmafibid1cn  15419  bhmafibid2cn  15420  bhmafibid2  15422  rlimuni  15503  climuni  15505  rlimcld2  15531  rlimrege0  15532  rlimrecl  15533  mulcn2  15549  reccn2  15550  cn1lem  15551  o1sub  15569  rlimo1  15570  o1dif  15583  rlimsqzlem  15602  caucvgrlem2  15628  iseralt  15638  fsumparts  15760  cvgcmpce  15772  incexclem  15792  arisum2  15817  geoserg  15822  pwdif  15824  geo2sum2  15830  fallfacfwd  15992  binomfallfaclem2  15996  bpolycl  16008  bpoly3  16014  bpoly4  16015  fsumcube  16016  sinf  16082  tanval2  16091  tanval3  16092  sinneg  16104  efival  16110  sinhval  16112  bitsinv1lem  16401  bitsres  16433  pythagtriplem1  16778  pythagtriplem14  16790  pythagtriplem17  16793  dvdsprmpweqle  16848  4sqlem5  16904  mul4sqlem  16915  4sqlem17  16923  vdwlem5  16947  vdwlem6  16948  vdwlem8  16950  blcvx  24781  recld2  24798  addcnlem  24848  cnllycmp  24941  cphipval2  25226  4cphipval2  25227  cphipval  25228  ipcnlem2  25229  rrxmval  25390  rrxmetlem  25392  pjthlem1  25422  ovollb2lem  25473  itgcnlem  25775  dvlem  25881  dvconst  25902  dvid  25903  dvcnp2  25905  dvaddbr  25923  dvmulbr  25924  dvcobr  25931  dvcjbr  25934  dvrec  25940  dvmptim  25955  dvcnvlem  25961  dveflem  25964  dvsincos  25966  cmvth  25976  dvlip  25978  dvlipcn  25979  c1liplem1  25981  dveq0  25985  dv11cn  25986  dvle  25992  lhop1lem  25998  dvfsumabs  26008  dvfsumlem1  26011  dvfsumlem2  26012  dvfsumrlim  26016  dvfsumrlim2  26017  ftc1lem4  26024  ftc1lem5  26025  ftc2  26029  dgrcolem2  26257  plydiveu  26282  aaliou2b  26325  taylfvallem1  26340  taylply2  26351  dvtaylp  26353  dvntaylp  26354  taylthlem1  26356  taylthlem2  26357  ulmbdd  26381  ulmcn  26382  ulmdvlem1  26383  mtest  26387  iblulm  26390  itgulm  26391  abelthlem9  26423  ptolemy  26478  tangtx  26487  sineq0  26506  efeq1  26510  efif1olem4  26527  tanarg  26601  logcnlem3  26626  logcnlem4  26627  advlogexp  26637  efopn  26640  cxpcn3lem  26729  cxpeq  26739  ang180lem4  26794  ang180lem5  26795  ang180  26796  isosctrlem2  26801  isosctrlem3  26802  isosctr  26803  ssscongptld  26804  affineequiv  26805  affineequiv2  26806  affineequiv3  26807  affineequiv4  26808  affineequivne  26809  angpieqvdlem  26810  angpieqvdlem2  26811  angpined  26812  angpieqvd  26813  chordthmlem  26814  chordthmlem2  26815  chordthmlem3  26816  chordthmlem4  26817  chordthmlem5  26818  heron  26820  quad2  26821  quad  26822  dcubic1lem  26825  dcubic  26828  mcubic  26829  cubic2  26830  cubic  26831  dquartlem1  26833  dquartlem2  26834  dquart  26835  quart1cl  26836  quart1lem  26837  quart1  26838  quartlem2  26840  quartlem4  26842  quart  26843  atanf  26862  sinasin  26871  asinsin  26874  atanneg  26889  atancj  26892  efiatan  26894  atanlogsub  26898  efiatan2  26899  2efiatan  26900  atanbndlem  26907  dvatan  26917  atantayl  26919  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem5  27014  lgamgulmlem6  27015  lgamgulm2  27017  lgamucov  27019  lgamcvg2  27036  gamcvg  27037  gamcvg2lem  27040  ftalem2  27055  logfacrlim  27205  logexprlim  27206  lgsdirprm  27312  gausslemma2dlem1a  27346  gausslemma2dlem4  27350  2sqmod  27417  addsq2nreurex  27425  vmadivsum  27463  rpvmasumlem  27468  dchrisumlem2  27471  dchrisumlem3  27472  dchrmusum2  27475  dchrvmasumlem2  27479  dchrvmasumlem3  27480  dchrvmasumiflem1  27482  rpvmasum2  27493  dchrisum0lem1b  27496  dchrisum0lem1  27497  dchrisum0lem2a  27498  rplogsum  27508  mudivsum  27511  mulogsumlem  27512  mulogsum  27513  mulog2sumlem1  27515  mulog2sumlem2  27516  mulog2sumlem3  27517  vmalogdivsum2  27519  vmalogdivsum  27520  2vmadivsumlem  27521  selberglem1  27526  selberglem2  27527  selberg2lem  27531  selberg2  27532  selberg3lem1  27538  selberg4lem1  27541  selberg4  27542  pntrsumo1  27546  selberg3r  27550  selberg34r  27552  pntrlog2bndlem1  27558  pntrlog2bndlem2  27559  pntrlog2bndlem3  27560  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntibndlem2  27572  pntlemf  27586  pntlemo  27588  ttgcontlem1  28971  brbtwn2  28992  colinearalglem1  28993  colinearalglem2  28994  colinearalg  28997  axsegconlem1  29004  ax5seglem1  29015  ax5seglem2  29016  ax5seglem6  29021  ax5seglem9  29024  axlowdimlem17  29045  axcontlem7  29057  axcontlem8  29058  clwlkclwwlk  30090  clwwlknonex2lem1  30195  2clwwlk2clwwlk  30438  numclwwlk3lem1  30470  smcnlem  30786  ipval2  30796  4ipval2  30797  dipcj  30803  pjhthlem1  31480  submuladdd  32832  binom2subadd  32833  pythagreim  32837  quad3d  32841  lt2addrd  32842  bcm1n  32887  cycpmco2lem5  33211  cycpmco2lem6  33212  vietalem  33763  constrrtll  33915  constrrtlc1  33916  constrrtcclem  33918  constrrtcc  33919  constrsslem  33925  constrconj  33929  constrfin  33930  constrelextdg2  33931  constraddcl  33946  iconstr  33950  constrremulcl  33951  constrrecl  33953  constrmulcl  33955  constrreinvcl  33956  constrresqrtcl  33961  cos9thpiminplylem2  33967  cos9thpiminplylem3  33968  sqsscirc2  34093  signslema  34746  circlemeth  34824  logdivsqrle  34834  revpfxsfxrev  35344  revwlk  35353  subfaclim  35416  divcnvlin  35961  iprodgam  35970  dnicld1  36778  dnibndlem2  36785  dnibndlem3  36786  dnibndlem6  36789  dnibndlem9  36792  dnibndlem10  36793  dnibndlem11  36794  unblimceq0  36813  unbdqndv2lem1  36815  unbdqndv2lem2  36816  knoppndvlem11  36828  knoppndvlem15  36832  knoppndvlem17  36834  knoppndvlem21  36838  bj-bary1lem  37670  bj-bary1lem1  37671  bj-bary1  37672  qdiff  37687  ftc1cnnclem  38058  ftc1anclem7  38066  ftc1anclem8  38067  ftc1anc  38068  ftc2nc  38069  areacirclem1  38075  areacirclem4  38078  areacirc  38080  cntotbnd  38163  lcmineqlem8  42521  lcmineqlem10  42523  lcmineqlem11  42524  lcmineqlem12  42525  lcmineqlem23  42536  aks4d1p1  42561  aks6d1c5lem1  42621  sticksstones10  42640  sticksstones12a  42642  sticksstones12  42643  sticksstones22  42653  bcle2d  42664  mvrrsubd  42751  lsubrotld  42754  lsubswap23d  42756  nicomachus  42789  sumcubes  42790  ef11d  42816  tanhalfpim  42826  sinpim  42827  cospim  42828  dffltz  43084  fltnltalem  43112  rencldnfilem  43265  pellexlem2  43275  pellexlem6  43279  pell1234qrne0  43298  pell1234qrmulcl  43300  rmyluc  43382  jm2.18  43433  jm2.19  43438  areaquad  43661  lhe4.4ex1a  44773  bcc0  44784  bccp1k  44785  bccm1k  44786  binomcxplemwb  44792  binomcxplemnn0  44793  binomcxplemrat  44794  binomcxplemfrat  44795  binomcxplemdvbinom  44797  binomcxplemnotnn0  44800  isosctrlem1ALT  45377  sineq0ALT  45380  oddfl  45726  dstregt0  45730  subadd4b  45731  sub31  45738  fzisoeu  45748  absnpncan2d  45750  absnpncan3d  45755  supxrgelem  45782  absimlere  45922  cvgcaule  45934  mullimc  46061  ellimcabssub0  46062  mullimcf  46068  limcrecl  46074  lptre2pt  46083  limcleqr  46087  neglimc  46090  addlimc  46091  0ellimcdiv  46092  limclner  46094  reclimc  46096  climleltrp  46119  climisp  46189  climxrrelem  46192  climxrre  46193  cnrefiisplem  46272  climxlim2lem  46288  fprodsubrecnncnvlem  46350  fperdvper  46362  dvdivbd  46366  dvbdfbdioolem2  46372  ioodvbdlimc1lem1  46374  volioc  46415  volico  46426  stoweidlem1  46444  stoweidlem11  46454  stoweidlem13  46456  stoweidlem26  46469  stoweid  46506  wallispi  46513  wallispi2lem1  46514  wallispi2lem2  46515  wallispi2  46516  stirlinglem1  46517  stirlinglem4  46520  stirlinglem5  46521  stirlinglem7  46523  stirlinglem11  46527  dirkertrigeqlem2  46542  fourierdlem4  46554  fourierdlem26  46576  fourierdlem30  46580  fourierdlem42  46592  fourierdlem63  46612  fourierdlem65  46614  fourierdlem72  46621  fourierdlem74  46623  fourierdlem75  46624  fourierdlem76  46625  fourierdlem80  46629  fourierdlem81  46630  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  fourierdlem107  46656  fourierdlem109  46658  fouriersw  46674  etransclem1  46678  etransclem4  46681  etransclem8  46685  etransclem18  46695  etransclem20  46697  etransclem21  46698  etransclem23  46700  etransclem35  46712  etransclem46  46723  rrxtopnfi  46730  rrndistlt  46733  sge0gtfsumgt  46886  hoidmv1lelem2  47035  hoidmvlelem2  47039  smfmullem1  47234  sigarmf  47297  sigarms  47299  sigarexp  47302  sigardiv  47304  sigarcol  47307  sharhght  47308  sigaradd  47309  cevathlem2  47311  cevath  47312  sin5tlem3  47338  sin5tlem4  47339  sin5tlem5  47340  cos5t  47342  resubcnnred  47767  fldivmod  47807  ceildivmod  47808  fmtnorec2lem  48020  fmtnorec3  48026  fmtnorec4  48027  lighneallem3  48085  quad1  48111  requad01  48112  requad2  48114  fppr2odd  48222  dignn0flhalflem2  49107  affinecomb2  49194  1subrec1sub  49196  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  rrx2vlinest  49232  rrx2linest  49233  line2  49243  itsclc0yqsollem1  49253  itsclc0yqsol  49255  itscnhlc0xyqsol  49256  itschlc0xyqsol1  49257  itschlc0xyqsol  49258  itsclc0xyqsolr  49260  2itscplem1  49269  2itscplem2  49270  2itscplem3  49271  itscnhlinecirc02plem1  49273  inlinecirc02plem  49277  sinhpcosh  50230  i2linesd  50269