Theorem subcld 11509

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042   − cmin 11381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-ltxr 11189  df-sub 11383

This theorem is referenced by:  subsubadd23  11561  addsubsub23  11562  pnpncand  11575  muleqadd  11798  lineq  11995  modmuladdnn0  13856  hashfz  14368  hashfzo  14370  hashf1lem2  14397  hashf1  14398  ccatswrd  14609  pfxccatin12lem2  14672  crre  15056  remim  15059  remullem  15070  abs3lem  15281  caubnd2  15300  bhmafibid1cn  15408  bhmafibid2cn  15409  bhmafibid2  15411  rlimuni  15492  climuni  15494  rlimcld2  15520  rlimrege0  15521  rlimrecl  15522  mulcn2  15538  reccn2  15539  cn1lem  15540  o1sub  15558  rlimo1  15559  o1dif  15572  rlimsqzlem  15591  caucvgrlem2  15617  iseralt  15627  fsumparts  15748  cvgcmpce  15760  incexclem  15778  arisum2  15803  geoserg  15808  pwdif  15810  geo2sum2  15816  fallfacfwd  15978  binomfallfaclem2  15982  bpolycl  15994  bpoly3  16000  bpoly4  16001  fsumcube  16002  sinf  16068  tanval2  16077  tanval3  16078  sinneg  16090  efival  16096  sinhval  16098  bitsinv1lem  16387  bitsres  16419  pythagtriplem1  16763  pythagtriplem14  16775  pythagtriplem17  16778  dvdsprmpweqle  16833  4sqlem5  16889  mul4sqlem  16900  4sqlem17  16908  vdwlem5  16932  vdwlem6  16933  vdwlem8  16935  blcvx  24719  recld2  24736  addcnlem  24786  cnllycmp  24888  cphipval2  25174  4cphipval2  25175  cphipval  25176  ipcnlem2  25177  rrxmval  25338  rrxmetlem  25340  pjthlem1  25370  ovollb2lem  25422  itgcnlem  25724  dvlem  25830  dvconst  25851  dvid  25852  dvcnp2  25854  dvcnp2OLD  25855  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  dvcobr  25882  dvcobrOLD  25883  dvcjbr  25886  dvrec  25892  dvmptim  25907  dvcnvlem  25913  dveflem  25916  dvsincos  25918  cmvth  25928  cmvthOLD  25929  dvlip  25931  dvlipcn  25932  c1liplem1  25934  dveq0  25938  dv11cn  25939  dvle  25945  lhop1lem  25951  dvfsumabs  25962  dvfsumlem1  25965  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsumrlim  25971  dvfsumrlim2  25972  ftc1lem4  25979  ftc1lem5  25980  ftc2  25984  dgrcolem2  26213  plydiveu  26239  aaliou2b  26282  taylfvallem1  26297  taylply2  26308  taylply2OLD  26309  dvtaylp  26311  dvntaylp  26312  taylthlem1  26314  taylthlem2  26315  taylthlem2OLD  26316  ulmbdd  26340  ulmcn  26341  ulmdvlem1  26342  mtest  26346  iblulm  26349  itgulm  26350  abelthlem9  26383  ptolemy  26438  tangtx  26447  sineq0  26466  efeq1  26470  efif1olem4  26487  tanarg  26561  logcnlem3  26586  logcnlem4  26587  advlogexp  26597  efopn  26600  cxpcn3lem  26690  cxpeq  26700  ang180lem4  26755  ang180lem5  26756  ang180  26757  isosctrlem2  26762  isosctrlem3  26763  isosctr  26764  ssscongptld  26765  affineequiv  26766  affineequiv2  26767  affineequiv3  26768  affineequiv4  26769  affineequivne  26770  angpieqvdlem  26771  angpieqvdlem2  26772  angpined  26773  angpieqvd  26774  chordthmlem  26775  chordthmlem2  26776  chordthmlem3  26777  chordthmlem4  26778  chordthmlem5  26779  heron  26781  quad2  26782  quad  26783  dcubic1lem  26786  dcubic  26789  mcubic  26790  cubic2  26791  cubic  26792  dquartlem1  26794  dquartlem2  26795  dquart  26796  quart1cl  26797  quart1lem  26798  quart1  26799  quartlem2  26801  quartlem4  26803  quart  26804  atanf  26823  sinasin  26832  asinsin  26835  atanneg  26850  atancj  26853  efiatan  26855  atanlogsub  26859  efiatan2  26860  2efiatan  26861  atanbndlem  26868  dvatan  26878  atantayl  26880  lgamgulmlem2  26973  lgamgulmlem3  26974  lgamgulmlem5  26976  lgamgulmlem6  26977  lgamgulm2  26979  lgamucov  26981  lgamcvg2  26998  gamcvg  26999  gamcvg2lem  27002  ftalem2  27017  logfacrlim  27168  logexprlim  27169  lgsdirprm  27275  gausslemma2dlem1a  27309  gausslemma2dlem4  27313  2sqmod  27380  addsq2nreurex  27388  vmadivsum  27426  rpvmasumlem  27431  dchrisumlem2  27434  dchrisumlem3  27435  dchrmusum2  27438  dchrvmasumlem2  27442  dchrvmasumlem3  27443  dchrvmasumiflem1  27445  rpvmasum2  27456  dchrisum0lem1b  27459  dchrisum0lem1  27460  dchrisum0lem2a  27461  rplogsum  27471  mudivsum  27474  mulogsumlem  27475  mulogsum  27476  mulog2sumlem1  27478  mulog2sumlem2  27479  mulog2sumlem3  27480  vmalogdivsum2  27482  vmalogdivsum  27483  2vmadivsumlem  27484  selberglem1  27489  selberglem2  27490  selberg2lem  27494  selberg2  27495  selberg3lem1  27501  selberg4lem1  27504  selberg4  27505  pntrsumo1  27509  selberg3r  27513  selberg34r  27515  pntrlog2bndlem1  27521  pntrlog2bndlem2  27522  pntrlog2bndlem3  27523  pntrlog2bndlem4  27524  pntrlog2bndlem5  27525  pntibndlem2  27535  pntlemf  27549  pntlemo  27551  ttgcontlem1  28865  brbtwn2  28885  colinearalglem1  28886  colinearalglem2  28887  colinearalg  28890  axsegconlem1  28897  ax5seglem1  28908  ax5seglem2  28909  ax5seglem6  28914  ax5seglem9  28917  axlowdimlem17  28938  axcontlem7  28950  axcontlem8  28951  clwlkclwwlk  29981  clwwlknonex2lem1  30086  2clwwlk2clwwlk  30329  numclwwlk3lem1  30361  smcnlem  30676  ipval2  30686  4ipval2  30687  dipcj  30693  pjhthlem1  31370  submuladdd  32713  binom2subadd  32715  pythagreim  32719  quad3d  32723  lt2addrd  32724  bcm1n  32768  cycpmco2lem5  33102  cycpmco2lem6  33103  constrrtll  33714  constrrtlc1  33715  constrrtcclem  33717  constrrtcc  33718  constrsslem  33724  constrconj  33728  constrfin  33729  constrelextdg2  33730  constraddcl  33745  iconstr  33749  constrremulcl  33750  constrrecl  33752  constrmulcl  33754  constrreinvcl  33755  constrresqrtcl  33760  cos9thpiminplylem2  33766  cos9thpiminplylem3  33767  sqsscirc2  33892  signslema  34546  circlemeth  34624  logdivsqrle  34634  revpfxsfxrev  35096  revwlk  35105  subfaclim  35168  divcnvlin  35713  iprodgam  35722  dnicld1  36453  dnibndlem2  36460  dnibndlem3  36461  dnibndlem6  36464  dnibndlem9  36467  dnibndlem10  36468  dnibndlem11  36469  unblimceq0  36488  unbdqndv2lem1  36490  unbdqndv2lem2  36491  knoppndvlem11  36503  knoppndvlem15  36507  knoppndvlem17  36509  knoppndvlem21  36513  bj-bary1lem  37291  bj-bary1lem1  37292  bj-bary1  37293  ftc1cnnclem  37678  ftc1anclem7  37686  ftc1anclem8  37687  ftc1anc  37688  ftc2nc  37689  areacirclem1  37695  areacirclem4  37698  areacirc  37700  cntotbnd  37783  lcmineqlem8  42017  lcmineqlem10  42019  lcmineqlem11  42020  lcmineqlem12  42021  lcmineqlem23  42032  aks4d1p1  42057  aks6d1c5lem1  42117  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones22  42149  bcle2d  42160  mvrrsubd  42255  lsubrotld  42258  lsubswap23d  42260  nicomachus  42293  sumcubes  42294  ef11d  42320  tanhalfpim  42330  sinpim  42331  cospim  42332  dffltz  42615  fltnltalem  42643  rencldnfilem  42801  pellexlem2  42811  pellexlem6  42815  pell1234qrne0  42834  pell1234qrmulcl  42836  rmyluc  42919  jm2.18  42970  jm2.19  42975  areaquad  43198  lhe4.4ex1a  44311  bcc0  44322  bccp1k  44323  bccm1k  44324  binomcxplemwb  44330  binomcxplemnn0  44331  binomcxplemrat  44332  binomcxplemfrat  44333  binomcxplemdvbinom  44335  binomcxplemnotnn0  44338  isosctrlem1ALT  44916  sineq0ALT  44919  oddfl  45269  dstregt0  45273  subadd4b  45274  sub31  45281  fzisoeu  45291  absnpncan2d  45293  absnpncan3d  45298  supxrgelem  45326  absimlere  45468  cvgcaule  45480  mullimc  45607  ellimcabssub0  45608  mullimcf  45614  limcrecl  45620  lptre2pt  45631  limcleqr  45635  neglimc  45638  addlimc  45639  0ellimcdiv  45640  limclner  45642  reclimc  45644  climleltrp  45667  climisp  45737  climxrrelem  45740  climxrre  45741  cnrefiisplem  45820  climxlim2lem  45836  fprodsubrecnncnvlem  45898  fperdvper  45910  dvdivbd  45914  dvbdfbdioolem2  45920  ioodvbdlimc1lem1  45922  volioc  45963  volico  45974  stoweidlem1  45992  stoweidlem11  46002  stoweidlem13  46004  stoweidlem26  46017  stoweid  46054  wallispi  46061  wallispi2lem1  46062  wallispi2lem2  46063  wallispi2  46064  stirlinglem1  46065  stirlinglem4  46068  stirlinglem5  46069  stirlinglem7  46071  stirlinglem11  46075  dirkertrigeqlem2  46090  fourierdlem4  46102  fourierdlem26  46124  fourierdlem30  46128  fourierdlem42  46140  fourierdlem63  46160  fourierdlem65  46162  fourierdlem72  46169  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem80  46177  fourierdlem81  46178  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem107  46204  fourierdlem109  46206  fouriersw  46222  etransclem1  46226  etransclem4  46229  etransclem8  46233  etransclem18  46243  etransclem20  46245  etransclem21  46246  etransclem23  46248  etransclem35  46260  etransclem46  46271  rrxtopnfi  46278  rrndistlt  46281  sge0gtfsumgt  46434  hoidmv1lelem2  46583  hoidmvlelem2  46587  smfmullem1  46782  sigarmf  46845  sigarms  46847  sigarexp  46850  sigardiv  46852  sigarcol  46855  sharhght  46856  sigaradd  46857  cevathlem2  46859  cevath  46860  resubcnnred  47298  fldivmod  47332  ceildivmod  47333  fmtnorec2lem  47536  fmtnorec3  47542  fmtnorec4  47543  lighneallem3  47601  quad1  47614  requad01  47615  requad2  47617  fppr2odd  47725  dignn0flhalflem2  48598  affinecomb2  48685  1subrec1sub  48687  eenglngeehlnmlem1  48719  eenglngeehlnmlem2  48720  rrx2vlinest  48723  rrx2linest  48724  line2  48734  itsclc0yqsollem1  48744  itsclc0yqsol  48746  itscnhlc0xyqsol  48747  itschlc0xyqsol1  48748  itschlc0xyqsol  48749  itsclc0xyqsolr  48751  2itscplem1  48760  2itscplem2  48761  2itscplem3  48762  itscnhlinecirc02plem1  48764  inlinecirc02plem  48768  sinhpcosh  49722  i2linesd  49761