Theorem subcld 11499

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7361  ℂcc 11030   − cmin 11371

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-ltxr 11178  df-sub 11373

This theorem is referenced by:  subsubadd23  11551  addsubsub23  11552  pnpncand  11565  muleqadd  11788  lineq  11986  modmuladdnn0  13871  hashfz  14383  hashfzo  14385  hashf1lem2  14412  hashf1  14413  ccatswrd  14625  pfxccatin12lem2  14687  crre  15070  remim  15073  remullem  15084  abs3lem  15295  caubnd2  15314  bhmafibid1cn  15422  bhmafibid2cn  15423  bhmafibid2  15425  rlimuni  15506  climuni  15508  rlimcld2  15534  rlimrege0  15535  rlimrecl  15536  mulcn2  15552  reccn2  15553  cn1lem  15554  o1sub  15572  rlimo1  15573  o1dif  15586  rlimsqzlem  15605  caucvgrlem2  15631  iseralt  15641  fsumparts  15763  cvgcmpce  15775  incexclem  15795  arisum2  15820  geoserg  15825  pwdif  15827  geo2sum2  15833  fallfacfwd  15995  binomfallfaclem2  15999  bpolycl  16011  bpoly3  16017  bpoly4  16018  fsumcube  16019  sinf  16085  tanval2  16094  tanval3  16095  sinneg  16107  efival  16113  sinhval  16115  bitsinv1lem  16404  bitsres  16436  pythagtriplem1  16781  pythagtriplem14  16793  pythagtriplem17  16796  dvdsprmpweqle  16851  4sqlem5  16907  mul4sqlem  16918  4sqlem17  16926  vdwlem5  16950  vdwlem6  16951  vdwlem8  16953  blcvx  24776  recld2  24793  addcnlem  24843  cnllycmp  24936  cphipval2  25221  4cphipval2  25222  cphipval  25223  ipcnlem2  25224  rrxmval  25385  rrxmetlem  25387  pjthlem1  25417  ovollb2lem  25468  itgcnlem  25770  dvlem  25876  dvconst  25897  dvid  25898  dvcnp2  25900  dvaddbr  25918  dvmulbr  25919  dvcobr  25926  dvcjbr  25929  dvrec  25935  dvmptim  25950  dvcnvlem  25956  dveflem  25959  dvsincos  25961  cmvth  25971  dvlip  25973  dvlipcn  25974  c1liplem1  25976  dveq0  25980  dv11cn  25981  dvle  25987  lhop1lem  25993  dvfsumabs  26003  dvfsumlem1  26006  dvfsumlem2  26007  dvfsumrlim  26011  dvfsumrlim2  26012  ftc1lem4  26019  ftc1lem5  26020  ftc2  26024  dgrcolem2  26252  plydiveu  26278  aaliou2b  26321  taylfvallem1  26336  taylply2  26347  taylply2OLD  26348  dvtaylp  26350  dvntaylp  26351  taylthlem1  26353  taylthlem2  26354  taylthlem2OLD  26355  ulmbdd  26379  ulmcn  26380  ulmdvlem1  26381  mtest  26385  iblulm  26388  itgulm  26389  abelthlem9  26421  ptolemy  26476  tangtx  26485  sineq0  26504  efeq1  26508  efif1olem4  26525  tanarg  26599  logcnlem3  26624  logcnlem4  26625  advlogexp  26635  efopn  26638  cxpcn3lem  26727  cxpeq  26737  ang180lem4  26792  ang180lem5  26793  ang180  26794  isosctrlem2  26799  isosctrlem3  26800  isosctr  26801  ssscongptld  26802  affineequiv  26803  affineequiv2  26804  affineequiv3  26805  affineequiv4  26806  affineequivne  26807  angpieqvdlem  26808  angpieqvdlem2  26809  angpined  26810  angpieqvd  26811  chordthmlem  26812  chordthmlem2  26813  chordthmlem3  26814  chordthmlem4  26815  chordthmlem5  26816  heron  26818  quad2  26819  quad  26820  dcubic1lem  26823  dcubic  26826  mcubic  26827  cubic2  26828  cubic  26829  dquartlem1  26831  dquartlem2  26832  dquart  26833  quart1cl  26834  quart1lem  26835  quart1  26836  quartlem2  26838  quartlem4  26840  quart  26841  atanf  26860  sinasin  26869  asinsin  26872  atanneg  26887  atancj  26890  efiatan  26892  atanlogsub  26896  efiatan2  26897  2efiatan  26898  atanbndlem  26905  dvatan  26915  atantayl  26917  lgamgulmlem2  27010  lgamgulmlem3  27011  lgamgulmlem5  27013  lgamgulmlem6  27014  lgamgulm2  27016  lgamucov  27018  lgamcvg2  27035  gamcvg  27036  gamcvg2lem  27039  ftalem2  27054  logfacrlim  27204  logexprlim  27205  lgsdirprm  27311  gausslemma2dlem1a  27345  gausslemma2dlem4  27349  2sqmod  27416  addsq2nreurex  27424  vmadivsum  27462  rpvmasumlem  27467  dchrisumlem2  27470  dchrisumlem3  27471  dchrmusum2  27474  dchrvmasumlem2  27478  dchrvmasumlem3  27479  dchrvmasumiflem1  27481  rpvmasum2  27492  dchrisum0lem1b  27495  dchrisum0lem1  27496  dchrisum0lem2a  27497  rplogsum  27507  mudivsum  27510  mulogsumlem  27511  mulogsum  27512  mulog2sumlem1  27514  mulog2sumlem2  27515  mulog2sumlem3  27516  vmalogdivsum2  27518  vmalogdivsum  27519  2vmadivsumlem  27520  selberglem1  27525  selberglem2  27526  selberg2lem  27530  selberg2  27531  selberg3lem1  27537  selberg4lem1  27540  selberg4  27541  pntrsumo1  27545  selberg3r  27549  selberg34r  27551  pntrlog2bndlem1  27557  pntrlog2bndlem2  27558  pntrlog2bndlem3  27559  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntibndlem2  27571  pntlemf  27585  pntlemo  27587  ttgcontlem1  28970  brbtwn2  28991  colinearalglem1  28992  colinearalglem2  28993  colinearalg  28996  axsegconlem1  29003  ax5seglem1  29014  ax5seglem2  29015  ax5seglem6  29020  ax5seglem9  29023  axlowdimlem17  29044  axcontlem7  29056  axcontlem8  29057  clwlkclwwlk  30090  clwwlknonex2lem1  30195  2clwwlk2clwwlk  30438  numclwwlk3lem1  30470  smcnlem  30786  ipval2  30796  4ipval2  30797  dipcj  30803  pjhthlem1  31480  submuladdd  32831  binom2subadd  32832  pythagreim  32836  quad3d  32840  lt2addrd  32841  bcm1n  32886  cycpmco2lem5  33209  cycpmco2lem6  33210  vietalem  33741  constrrtll  33894  constrrtlc1  33895  constrrtcclem  33897  constrrtcc  33898  constrsslem  33904  constrconj  33908  constrfin  33909  constrelextdg2  33910  constraddcl  33925  iconstr  33929  constrremulcl  33930  constrrecl  33932  constrmulcl  33934  constrreinvcl  33935  constrresqrtcl  33940  cos9thpiminplylem2  33946  cos9thpiminplylem3  33947  sqsscirc2  34072  signslema  34725  circlemeth  34803  logdivsqrle  34813  revpfxsfxrev  35317  revwlk  35326  subfaclim  35389  divcnvlin  35934  iprodgam  35943  dnicld1  36751  dnibndlem2  36758  dnibndlem3  36759  dnibndlem6  36762  dnibndlem9  36765  dnibndlem10  36766  dnibndlem11  36767  unblimceq0  36786  unbdqndv2lem1  36788  unbdqndv2lem2  36789  knoppndvlem11  36801  knoppndvlem15  36805  knoppndvlem17  36807  knoppndvlem21  36811  bj-bary1lem  37643  bj-bary1lem1  37644  bj-bary1  37645  ftc1cnnclem  38029  ftc1anclem7  38037  ftc1anclem8  38038  ftc1anc  38039  ftc2nc  38040  areacirclem1  38046  areacirclem4  38049  areacirc  38051  cntotbnd  38134  lcmineqlem8  42492  lcmineqlem10  42494  lcmineqlem11  42495  lcmineqlem12  42496  lcmineqlem23  42507  aks4d1p1  42532  aks6d1c5lem1  42592  sticksstones10  42611  sticksstones12a  42613  sticksstones12  42614  sticksstones22  42624  bcle2d  42635  mvrrsubd  42723  lsubrotld  42726  lsubswap23d  42728  nicomachus  42761  sumcubes  42762  ef11d  42788  tanhalfpim  42798  sinpim  42799  cospim  42800  dffltz  43084  fltnltalem  43112  rencldnfilem  43269  pellexlem2  43279  pellexlem6  43283  pell1234qrne0  43302  pell1234qrmulcl  43304  rmyluc  43386  jm2.18  43437  jm2.19  43442  areaquad  43665  lhe4.4ex1a  44777  bcc0  44788  bccp1k  44789  bccm1k  44790  binomcxplemwb  44796  binomcxplemnn0  44797  binomcxplemrat  44798  binomcxplemfrat  44799  binomcxplemdvbinom  44801  binomcxplemnotnn0  44804  isosctrlem1ALT  45381  sineq0ALT  45384  oddfl  45732  dstregt0  45736  subadd4b  45737  sub31  45744  fzisoeu  45754  absnpncan2d  45756  absnpncan3d  45761  supxrgelem  45788  absimlere  45928  cvgcaule  45940  mullimc  46067  ellimcabssub0  46068  mullimcf  46074  limcrecl  46080  lptre2pt  46089  limcleqr  46093  neglimc  46096  addlimc  46097  0ellimcdiv  46098  limclner  46100  reclimc  46102  climleltrp  46125  climisp  46195  climxrrelem  46198  climxrre  46199  cnrefiisplem  46278  climxlim2lem  46294  fprodsubrecnncnvlem  46356  fperdvper  46368  dvdivbd  46372  dvbdfbdioolem2  46378  ioodvbdlimc1lem1  46380  volioc  46421  volico  46432  stoweidlem1  46450  stoweidlem11  46460  stoweidlem13  46462  stoweidlem26  46475  stoweid  46512  wallispi  46519  wallispi2lem1  46520  wallispi2lem2  46521  wallispi2  46522  stirlinglem1  46523  stirlinglem4  46526  stirlinglem5  46527  stirlinglem7  46529  stirlinglem11  46533  dirkertrigeqlem2  46548  fourierdlem4  46560  fourierdlem26  46582  fourierdlem30  46586  fourierdlem42  46598  fourierdlem63  46618  fourierdlem65  46620  fourierdlem72  46627  fourierdlem74  46629  fourierdlem75  46630  fourierdlem76  46631  fourierdlem80  46635  fourierdlem81  46636  fourierdlem89  46644  fourierdlem90  46645  fourierdlem91  46646  fourierdlem107  46662  fourierdlem109  46664  fouriersw  46680  etransclem1  46684  etransclem4  46687  etransclem8  46691  etransclem18  46701  etransclem20  46703  etransclem21  46704  etransclem23  46706  etransclem35  46718  etransclem46  46729  rrxtopnfi  46736  rrndistlt  46739  sge0gtfsumgt  46892  hoidmv1lelem2  47041  hoidmvlelem2  47045  smfmullem1  47240  sigarmf  47303  sigarms  47305  sigarexp  47308  sigardiv  47310  sigarcol  47313  sharhght  47314  sigaradd  47315  cevathlem2  47317  cevath  47318  sin5tlem3  47342  sin5tlem4  47343  sin5tlem5  47344  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