Theorem subcld 11669

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7420  ℂcc 11198   − cmin 11541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348  df-sub 11543

This theorem is used by:  subsubadd23  11721  addsubsub23  11722  mvrrsubd  11729  pnpncand  11737  muleqadd  11960  lineq  12154  modmuladdnn0  14058  hashfz  14572  hashfzo  14574  hashf1lem2  14601  hashf1  14602  ccatswrd  14818  pfxccatin12lem2  14880  revpfxsfxrev  14917  crre  15281  remim  15284  remullem  15295  abs3lem  15506  caubnd2  15525  bhmafibid1cn  15633  bhmafibid2cn  15634  bhmafibid2  15636  rlimuni  15717  climuni  15719  rlimcld2  15745  rlimrege0  15746  rlimrecl  15747  mulcn2  15763  reccn2  15764  cn1lem  15765  o1sub  15783  rlimo1  15784  o1dif  15797  rlimsqzlem  15816  caucvgrlem2  15842  iseralt  15852  fsumparts  15973  cvgcmpce  15985  incexclem  16005  arisum2  16030  geoserg  16035  pwdif  16037  geo2sum2  16043  fallfacfwd  16202  binomfallfaclem2  16206  bpolycl  16218  bpoly3  16224  bpoly4  16225  fsumcube  16226  sinf  16292  tanval2  16301  tanval3  16302  sinneg  16314  efival  16320  sinhval  16322  bitsinv1lem  16611  bitsres  16643  pythagtriplem1  16994  pythagtriplem14  17006  pythagtriplem17  17009  dvdsprmpweqle  17064  4sqlem5  17120  mul4sqlem  17131  4sqlem17  17139  vdwlem5  17163  vdwlem6  17164  vdwlem8  17166  blcvx  25117  recld2  25134  addcnlem  25184  cnllycmp  25277  cphipval2  25562  4cphipval2  25563  cphipval  25564  ipcnlem2  25565  rrxmval  25726  rrxmetlem  25728  pjthlem1  25758  ovollb2lem  25809  itgcnlem  26110  dvlem  26216  dvconst  26237  dvid  26238  dvcnp2  26240  dvaddbr  26258  dvmulbr  26259  dvcobr  26266  dvcjbr  26269  dvrec  26275  dvmptim  26290  dvcnvlem  26296  dveflem  26299  dvsincos  26301  cmvth  26311  dvlip  26313  dvlipcn  26314  c1liplem1  26316  dveq0  26320  dv11cn  26321  dvle  26327  lhop1lem  26333  dvfsumabs  26343  dvfsumlem1  26346  dvfsumlem2  26347  dvfsumrlim  26351  dvfsumrlim2  26352  ftc1lem4  26359  ftc1lem5  26360  ftc2  26364  dgrcolem2  26593  plydiveu  26619  aaliou2b  26668  taylfvallem1  26684  taylply2  26695  dvtaylp  26697  dvntaylp  26698  taylthlem1  26700  taylthlem2  26701  ulmbdd  26725  ulmcn  26726  ulmdvlem1  26727  mtest  26731  iblulm  26734  itgulm  26735  abelthlem9  26767  ptolemy  26825  tangtx  26834  sineq0  26852  efeq1  26856  efif1olem4  26873  tanarg  26947  logcnlem3  26972  logcnlem4  26973  advlogexp  26983  efopn  26986  cxpcn3lem  27075  cxpeq  27085  ang180lem4  27140  ang180lem5  27141  ang180  27142  isosctrlem2  27147  isosctrlem3  27148  isosctr  27149  ssscongptld  27150  affineequiv  27151  affineequiv2  27152  affineequiv3  27153  affineequiv4  27154  affineequivne  27155  angpieqvdlem  27156  angpieqvdlem2  27157  angpined  27158  angpieqvd  27159  chordthmlem  27160  chordthmlem2  27161  chordthmlem3  27162  chordthmlem4  27163  chordthmlem5  27164  heron  27166  quad2  27167  quad  27168  dcubic1lem  27171  dcubic  27174  mcubic  27175  cubic2  27176  cubic  27177  dquartlem1  27179  dquartlem2  27180  dquart  27181  quart1cl  27182  quart1lem  27183  quart1  27184  quartlem2  27186  quartlem4  27188  quart  27189  atanf  27208  sinasin  27217  asinsin  27220  atanneg  27235  atancj  27238  efiatan  27240  atanlogsub  27244  efiatan2  27245  2efiatan  27246  atanbndlem  27253  dvatan  27263  atantayl  27265  lgamgulmlem2  27357  lgamgulmlem3  27358  lgamgulmlem5  27360  lgamgulmlem6  27361  lgamgulm2  27363  lgamucov  27365  lgamcvg2  27382  gamcvg  27383  gamcvg2lem  27386  ftalem2  27401  logfacrlim  27551  logexprlim  27552  lgsdirprm  27658  gausslemma2dlem1a  27692  gausslemma2dlem4  27696  2sqmod  27763  addsq2nreurex  27771  vmadivsum  27809  rpvmasumlem  27814  dchrisumlem2  27817  dchrisumlem3  27818  dchrmusum2  27821  dchrvmasumlem2  27825  dchrvmasumlem3  27826  dchrvmasumiflem1  27828  rpvmasum2  27839  dchrisum0lem1b  27842  dchrisum0lem1  27843  dchrisum0lem2a  27844  rplogsum  27854  mudivsum  27857  mulogsumlem  27858  mulogsum  27859  mulog2sumlem1  27861  mulog2sumlem2  27862  mulog2sumlem3  27863  vmalogdivsum2  27865  vmalogdivsum  27866  2vmadivsumlem  27867  selberglem1  27872  selberglem2  27873  selberg2lem  27877  selberg2  27878  selberg3lem1  27884  selberg4lem1  27887  selberg4  27888  pntrsumo1  27892  selberg3r  27896  selberg34r  27898  pntrlog2bndlem1  27904  pntrlog2bndlem2  27905  pntrlog2bndlem3  27906  pntrlog2bndlem4  27907  pntrlog2bndlem5  27908  pntibndlem2  27918  pntlemf  27932  pntlemo  27934  ttgcontlem1  29462  brbtwn2  29483  colinearalglem1  29484  colinearalglem2  29485  colinearalg  29488  axsegconlem1  29495  ax5seglem1  29506  ax5seglem2  29507  ax5seglem6  29512  ax5seglem9  29515  axlowdimlem17  29536  axcontlem7  29548  axcontlem8  29549  revwlk  30267  clwlkclwwlk  30593  clwwlknonex2lem1  30698  2clwwlk2clwwlk  30951  numclwwlk3lem1  30983  smcnlem  31299  ipval2  31309  4ipval2  31310  dipcj  31316  pjhthlem1  31993  submuladdd  33332  binom2subadd  33333  pythagreim  33337  quad3d  33341  lt2addrd  33342  bcm1n  33387  cycpmco2lem5  33691  cycpmco2lem6  33692  vietalem  34211  constrrtll  34363  constrrtlc1  34364  constrrtcclem  34366  constrrtcc  34367  constrsslem  34373  constrconj  34377  constrfin  34378  constrelextdg2  34379  constraddcl  34394  iconstr  34398  constrremulcl  34399  constrrecl  34401  constrmulcl  34403  constrreinvcl  34404  constrresqrtcl  34409  cos9thpiminplylem2  34415  cos9thpiminplylem3  34416  sqsscirc2  34541  signslema  35191  circlemeth  35269  logdivsqrle  35279  subfaclim  35953  divcnvlin  36498  iprodgam  36507  dnicld1  37338  dnibndlem2  37345  dnibndlem3  37346  dnibndlem6  37349  dnibndlem9  37352  dnibndlem10  37353  dnibndlem11  37354  unblimceq0  37373  unbdqndv2lem1  37375  unbdqndv2lem2  37376  knoppndvlem11  37388  knoppndvlem15  37392  knoppndvlem17  37394  knoppndvlem21  37398  bj-bary1lem  38231  bj-bary1lem1  38232  bj-bary1  38233  qdiff  38248  ftc1cnnclem  38609  ftc1anclem7  38617  ftc1anclem8  38618  ftc1anc  38619  ftc2nc  38620  areacirclem1  38626  areacirclem4  38629  areacirc  38631  cntotbnd  38730  lcmineqlem8  43086  lcmineqlem10  43088  lcmineqlem11  43089  lcmineqlem12  43090  lcmineqlem23  43101  aks4d1p1  43126  aks6d1c5lem1  43186  sticksstones10  43205  sticksstones12a  43207  sticksstones12  43208  sticksstones22  43218  bcle2d  43229  quadfac  43255  lsubrotld  43334  lsubswap23d  43336  nicomachus  43369  sumcubes  43370  ef11d  43390  tanhalfpim  43400  sinpim  43401  cospim  43402  dffltz  43670  fltnltalem  43673  rencldnfilem  43826  pellexlem2  43836  pellexlem6  43840  pell1234qrne0  43859  pell1234qrmulcl  43861  rmyluc  43943  jm2.18  43994  jm2.19  43999  areaquad  44217  lhe4.4ex1a  45312  bcc0  45323  bccp1k  45324  bccm1k  45325  binomcxplemwb  45331  binomcxplemnn0  45332  binomcxplemrat  45333  binomcxplemfrat  45334  binomcxplemdvbinom  45336  binomcxplemnotnn0  45339  isosctrlem1ALT  45915  sineq0ALT  45918  oddfl  46293  dstregt0  46297  subadd4b  46298  sub31  46305  fzisoeu  46315  absnpncan2d  46317  absnpncan3d  46322  supxrgelem  46348  absimlere  46488  cvgcaule  46500  mullimc  46627  ellimcabssub0  46628  mullimcf  46634  limcrecl  46640  lptre2pt  46649  limcleqr  46653  neglimc  46656  addlimc  46657  0ellimcdiv  46658  limclner  46660  reclimc  46662  climleltrp  46685  climisp  46755  climxrrelem  46758  climxrre  46759  cnrefiisplem  46838  climxlim2lem  46854  fprodsubrecnncnvlem  46916  fperdvper  46928  dvdivbd  46932  dvbdfbdioolem2  46938  ioodvbdlimc1lem1  46940  volioc  46981  volico  46992  stoweidlem1  47010  stoweidlem11  47020  stoweidlem13  47022  stoweidlem26  47035  stoweid  47072  wallispi  47079  wallispi2lem1  47080  wallispi2lem2  47081  wallispi2  47082  stirlinglem1  47083  stirlinglem4  47086  stirlinglem5  47087  stirlinglem7  47089  stirlinglem11  47093  dirkertrigeqlem2  47108  fourierdlem4  47120  fourierdlem26  47142  fourierdlem30  47146  fourierdlem42  47158  fourierdlem63  47178  fourierdlem65  47180  fourierdlem72  47187  fourierdlem74  47189  fourierdlem75  47190  fourierdlem76  47191  fourierdlem80  47195  fourierdlem81  47196  fourierdlem89  47204  fourierdlem90  47205  fourierdlem91  47206  fourierdlem107  47222  fourierdlem109  47224  fouriersw  47240  etransclem1  47244  etransclem4  47247  etransclem8  47251  etransclem18  47261  etransclem20  47263  etransclem21  47264  etransclem23  47266  etransclem35  47278  etransclem46  47289  rrxtopnfi  47296  rrndistlt  47299  sge0gtfsumgt  47452  hoidmv1lelem2  47601  hoidmvlelem2  47605  smfmullem1  47800  sigarmf  47863  sigarms  47865  sigarexp  47868  sigardiv  47870  sigarcol  47873  sharhght  47874  sigaradd  47875  cevathlem2  47877  cevath  47878  sin5tlem3  47920  sin5tlem4  47921  sin5tlem5  47922  cos5t  47924  resubcnnred  48373  fldivmod  48413  ceildivmod  48414  fmtnorec2lem  48626  fmtnorec3  48632  fmtnorec4  48633  lighneallem3  48691  quad1  48717  requad01  48718  requad2  48720  fppr2odd  48828  dignn0flhalflem2  49727  affinecomb2  49814  1subrec1sub  49816  eenglngeehlnmlem1  49848  eenglngeehlnmlem2  49849  rrx2vlinest  49852  rrx2linest  49853  line2  49863  itsclc0yqsollem1  49873  itsclc0yqsol  49875  itscnhlc0xyqsol  49876  itschlc0xyqsol1  49877  itschlc0xyqsol  49878  itsclc0xyqsolr  49880  2itscplem1  49889  2itscplem2  49890  2itscplem3  49891  itscnhlinecirc02plem1  49893  inlinecirc02plem  49897  sinhpcosh  50832  i2linesd  50874  crossp3d  50966