Theorem subcld 11341

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878   − cmin 11214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-ltxr 11023  df-sub 11216

This theorem is referenced by:  pnpncand  11405  muleqadd  11628  lineq  11821  modmuladdnn0  13644  hashfz  14151  hashfzo  14153  hashf1lem2  14179  hashf1  14180  ccatswrd  14390  pfxccatin12lem2  14453  crre  14834  remim  14837  remullem  14848  abs3lem  15059  caubnd2  15078  bhmafibid1cn  15184  bhmafibid2cn  15185  bhmafibid2  15187  rlimuni  15268  climuni  15270  rlimcld2  15296  rlimrege0  15297  rlimrecl  15298  mulcn2  15314  reccn2  15315  cn1lem  15316  o1sub  15334  rlimo1  15335  o1dif  15348  rlimsqzlem  15369  caucvgrlem2  15395  iseralt  15405  fsumparts  15527  cvgcmpce  15539  incexclem  15557  arisum2  15582  geoserg  15587  pwdif  15589  geo2sum2  15595  fallfacfwd  15755  binomfallfaclem2  15759  bpolycl  15771  bpoly3  15777  bpoly4  15778  fsumcube  15779  sinf  15842  tanval2  15851  tanval3  15852  sinneg  15864  efival  15870  sinhval  15872  bitsinv1lem  16157  bitsres  16189  pythagtriplem1  16526  pythagtriplem14  16538  pythagtriplem17  16541  dvdsprmpweqle  16596  4sqlem5  16652  mul4sqlem  16663  4sqlem17  16671  vdwlem5  16695  vdwlem6  16696  vdwlem8  16698  blcvx  23970  recld2  23986  addcnlem  24036  cnllycmp  24128  cphipval2  24414  4cphipval2  24415  cphipval  24416  ipcnlem2  24417  rrxmval  24578  rrxmetlem  24580  pjthlem1  24610  ovollb2lem  24661  itgcnlem  24963  dvlem  25069  dvconst  25090  dvid  25091  dvcnp2  25093  dvaddbr  25111  dvmulbr  25112  dvcobr  25119  dvcjbr  25122  dvrec  25128  dvmptim  25143  dvcnvlem  25149  dveflem  25152  dvsincos  25154  cmvth  25164  dvlip  25166  dvlipcn  25167  c1liplem1  25169  dveq0  25173  dv11cn  25174  dvle  25180  lhop1lem  25186  dvfsumabs  25196  dvfsumlem1  25199  dvfsumlem2  25200  dvfsumrlim  25204  dvfsumrlim2  25205  ftc1lem4  25212  ftc1lem5  25213  ftc2  25217  dgrcolem2  25444  plydiveu  25467  aaliou2b  25510  taylfvallem1  25525  taylply2  25536  dvtaylp  25538  dvntaylp  25539  taylthlem1  25541  taylthlem2  25542  ulmbdd  25566  ulmcn  25567  ulmdvlem1  25568  mtest  25572  iblulm  25575  itgulm  25576  abelthlem9  25608  ptolemy  25662  tangtx  25671  sineq0  25689  efeq1  25693  efif1olem4  25710  tanarg  25783  logcnlem3  25808  logcnlem4  25809  advlogexp  25819  efopn  25822  cxpcn3lem  25909  cxpeq  25919  ang180lem4  25971  ang180lem5  25972  ang180  25973  isosctrlem2  25978  isosctrlem3  25979  isosctr  25980  ssscongptld  25981  affineequiv  25982  affineequiv2  25983  affineequiv3  25984  affineequiv4  25985  affineequivne  25986  angpieqvdlem  25987  angpieqvdlem2  25988  angpined  25989  angpieqvd  25990  chordthmlem  25991  chordthmlem2  25992  chordthmlem3  25993  chordthmlem4  25994  chordthmlem5  25995  heron  25997  quad2  25998  quad  25999  dcubic1lem  26002  dcubic  26005  mcubic  26006  cubic2  26007  cubic  26008  dquartlem1  26010  dquartlem2  26011  dquart  26012  quart1cl  26013  quart1lem  26014  quart1  26015  quartlem2  26017  quartlem4  26019  quart  26020  atanf  26039  sinasin  26048  asinsin  26051  atanneg  26066  atancj  26069  efiatan  26071  atanlogsub  26075  efiatan2  26076  2efiatan  26077  atanbndlem  26084  dvatan  26094  atantayl  26096  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem5  26191  lgamgulmlem6  26192  lgamgulm2  26194  lgamucov  26196  lgamcvg2  26213  gamcvg  26214  gamcvg2lem  26217  ftalem2  26232  logfacrlim  26381  logexprlim  26382  lgsdirprm  26488  gausslemma2dlem1a  26522  gausslemma2dlem4  26526  2sqmod  26593  addsq2nreurex  26601  vmadivsum  26639  rpvmasumlem  26644  dchrisumlem2  26647  dchrisumlem3  26648  dchrmusum2  26651  dchrvmasumlem2  26655  dchrvmasumlem3  26656  dchrvmasumiflem1  26658  rpvmasum2  26669  dchrisum0lem1b  26672  dchrisum0lem1  26673  dchrisum0lem2a  26674  rplogsum  26684  mudivsum  26687  mulogsumlem  26688  mulogsum  26689  mulog2sumlem1  26691  mulog2sumlem2  26692  mulog2sumlem3  26693  vmalogdivsum2  26695  vmalogdivsum  26696  2vmadivsumlem  26697  selberglem1  26702  selberglem2  26703  selberg2lem  26707  selberg2  26708  selberg3lem1  26714  selberg4lem1  26717  selberg4  26718  pntrsumo1  26722  selberg3r  26726  selberg34r  26728  pntrlog2bndlem1  26734  pntrlog2bndlem2  26735  pntrlog2bndlem3  26736  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntibndlem2  26748  pntlemf  26762  pntlemo  26764  ttgcontlem1  27261  brbtwn2  27282  colinearalglem1  27283  colinearalglem2  27284  colinearalg  27287  axsegconlem1  27294  ax5seglem1  27305  ax5seglem2  27306  ax5seglem6  27311  ax5seglem9  27314  axlowdimlem17  27335  axcontlem7  27347  axcontlem8  27348  clwlkclwwlk  28375  clwwlknonex2lem1  28480  2clwwlk2clwwlk  28723  numclwwlk3lem1  28755  smcnlem  29068  ipval2  29078  4ipval2  29079  dipcj  29085  pjhthlem1  29762  lt2addrd  31083  bcm1n  31125  cycpmco2lem5  31406  cycpmco2lem6  31407  sqsscirc2  31868  signslema  32550  circlemeth  32629  logdivsqrle  32639  revpfxsfxrev  33086  revwlk  33095  subfaclim  33159  divcnvlin  33707  iprodgam  33717  dnicld1  34661  dnibndlem2  34668  dnibndlem3  34669  dnibndlem6  34672  dnibndlem9  34675  dnibndlem10  34676  dnibndlem11  34677  unblimceq0  34696  unbdqndv2lem1  34698  unbdqndv2lem2  34699  knoppndvlem11  34711  knoppndvlem15  34715  knoppndvlem17  34717  knoppndvlem21  34721  bj-bary1lem  35490  bj-bary1lem1  35491  bj-bary1  35492  ftc1cnnclem  35857  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  ftc2nc  35868  areacirclem1  35874  areacirclem4  35877  areacirc  35879  cntotbnd  35963  lcmineqlem8  40051  lcmineqlem10  40053  lcmineqlem11  40054  lcmineqlem12  40055  lcmineqlem23  40066  aks4d1p1  40091  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  sticksstones22  40131  metakunt15  40146  metakunt16  40147  metakunt29  40160  metakunt30  40161  mvrrsubd  40310  lsubrotld  40313  lsubcom23d  40314  dffltz  40478  fltnltalem  40506  rencldnfilem  40649  pellexlem2  40659  pellexlem6  40663  pell1234qrne0  40682  pell1234qrmulcl  40684  rmyluc  40766  jm2.18  40817  jm2.19  40822  areaquad  41054  lhe4.4ex1a  41954  bcc0  41965  bccp1k  41966  bccm1k  41967  binomcxplemwb  41973  binomcxplemnn0  41974  binomcxplemrat  41975  binomcxplemfrat  41976  binomcxplemdvbinom  41978  binomcxplemnotnn0  41981  isosctrlem1ALT  42561  sineq0ALT  42564  oddfl  42823  dstregt0  42827  subadd4b  42828  sub31  42836  fzisoeu  42846  absnpncan2d  42848  absnpncan3d  42853  supxrgelem  42883  absimlere  43027  mullimc  43164  ellimcabssub0  43165  mullimcf  43171  limcrecl  43177  lptre2pt  43188  limcleqr  43192  neglimc  43195  addlimc  43196  0ellimcdiv  43197  limclner  43199  reclimc  43201  climleltrp  43224  climisp  43294  climxrrelem  43297  climxrre  43298  cnrefiisplem  43377  climxlim2lem  43393  fprodsubrecnncnvlem  43455  fperdvper  43467  dvdivbd  43471  dvbdfbdioolem2  43477  ioodvbdlimc1lem1  43479  volioc  43520  volico  43531  stoweidlem1  43549  stoweidlem11  43559  stoweidlem13  43561  stoweidlem26  43574  stoweid  43611  wallispi  43618  wallispi2lem1  43619  wallispi2lem2  43620  wallispi2  43621  stirlinglem1  43622  stirlinglem4  43625  stirlinglem5  43626  stirlinglem7  43628  stirlinglem11  43632  dirkertrigeqlem2  43647  fourierdlem4  43659  fourierdlem26  43681  fourierdlem30  43685  fourierdlem42  43697  fourierdlem63  43717  fourierdlem65  43719  fourierdlem72  43726  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem80  43734  fourierdlem81  43735  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem107  43761  fourierdlem109  43763  fouriersw  43779  etransclem1  43783  etransclem4  43786  etransclem8  43790  etransclem18  43800  etransclem20  43802  etransclem21  43803  etransclem23  43805  etransclem35  43817  etransclem46  43828  rrxtopnfi  43835  rrndistlt  43838  sge0gtfsumgt  43988  hoidmv1lelem2  44137  hoidmvlelem2  44141  smfmullem1  44336  sigarmf  44381  sigarms  44383  sigarexp  44386  sigardiv  44388  sigarcol  44391  sharhght  44392  sigaradd  44393  cevathlem2  44395  cevath  44396  resubcnnred  44807  fmtnorec2lem  45005  fmtnorec3  45011  fmtnorec4  45012  lighneallem3  45070  quad1  45083  requad01  45084  requad2  45086  fppr2odd  45194  fldivmod  45875  dignn0flhalflem2  45973  affinecomb2  46060  1subrec1sub  46062  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  rrx2vlinest  46098  rrx2linest  46099  line2  46109  itsclc0yqsollem1  46119  itsclc0yqsol  46121  itscnhlc0xyqsol  46122  itschlc0xyqsol1  46123  itschlc0xyqsol  46124  itsclc0xyqsolr  46126  2itscplem1  46135  2itscplem2  46136  2itscplem3  46137  itscnhlinecirc02plem1  46139  inlinecirc02plem  46143  sinhpcosh  46453  i2linesd  46494