Theorem subcld 11533

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   − cmin 11405

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213  df-sub 11407

This theorem is referenced by:  subsubadd23  11585  addsubsub23  11586  pnpncand  11599  muleqadd  11822  lineq  12019  modmuladdnn0  13880  hashfz  14392  hashfzo  14394  hashf1lem2  14421  hashf1  14422  ccatswrd  14633  pfxccatin12lem2  14696  crre  15080  remim  15083  remullem  15094  abs3lem  15305  caubnd2  15324  bhmafibid1cn  15432  bhmafibid2cn  15433  bhmafibid2  15435  rlimuni  15516  climuni  15518  rlimcld2  15544  rlimrege0  15545  rlimrecl  15546  mulcn2  15562  reccn2  15563  cn1lem  15564  o1sub  15582  rlimo1  15583  o1dif  15596  rlimsqzlem  15615  caucvgrlem2  15641  iseralt  15651  fsumparts  15772  cvgcmpce  15784  incexclem  15802  arisum2  15827  geoserg  15832  pwdif  15834  geo2sum2  15840  fallfacfwd  16002  binomfallfaclem2  16006  bpolycl  16018  bpoly3  16024  bpoly4  16025  fsumcube  16026  sinf  16092  tanval2  16101  tanval3  16102  sinneg  16114  efival  16120  sinhval  16122  bitsinv1lem  16411  bitsres  16443  pythagtriplem1  16787  pythagtriplem14  16799  pythagtriplem17  16802  dvdsprmpweqle  16857  4sqlem5  16913  mul4sqlem  16924  4sqlem17  16932  vdwlem5  16956  vdwlem6  16957  vdwlem8  16959  blcvx  24686  recld2  24703  addcnlem  24753  cnllycmp  24855  cphipval2  25141  4cphipval2  25142  cphipval  25143  ipcnlem2  25144  rrxmval  25305  rrxmetlem  25307  pjthlem1  25337  ovollb2lem  25389  itgcnlem  25691  dvlem  25797  dvconst  25818  dvid  25819  dvcnp2  25821  dvcnp2OLD  25822  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcobr  25849  dvcobrOLD  25850  dvcjbr  25853  dvrec  25859  dvmptim  25874  dvcnvlem  25880  dveflem  25883  dvsincos  25885  cmvth  25895  cmvthOLD  25896  dvlip  25898  dvlipcn  25899  c1liplem1  25901  dveq0  25905  dv11cn  25906  dvle  25912  lhop1lem  25918  dvfsumabs  25929  dvfsumlem1  25932  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumrlim  25938  dvfsumrlim2  25939  ftc1lem4  25946  ftc1lem5  25947  ftc2  25951  dgrcolem2  26180  plydiveu  26206  aaliou2b  26249  taylfvallem1  26264  taylply2  26275  taylply2OLD  26276  dvtaylp  26278  dvntaylp  26279  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmbdd  26307  ulmcn  26308  ulmdvlem1  26309  mtest  26313  iblulm  26316  itgulm  26317  abelthlem9  26350  ptolemy  26405  tangtx  26414  sineq0  26433  efeq1  26437  efif1olem4  26454  tanarg  26528  logcnlem3  26553  logcnlem4  26554  advlogexp  26564  efopn  26567  cxpcn3lem  26657  cxpeq  26667  ang180lem4  26722  ang180lem5  26723  ang180  26724  isosctrlem2  26729  isosctrlem3  26730  isosctr  26731  ssscongptld  26732  affineequiv  26733  affineequiv2  26734  affineequiv3  26735  affineequiv4  26736  affineequivne  26737  angpieqvdlem  26738  angpieqvdlem2  26739  angpined  26740  angpieqvd  26741  chordthmlem  26742  chordthmlem2  26743  chordthmlem3  26744  chordthmlem4  26745  chordthmlem5  26746  heron  26748  quad2  26749  quad  26750  dcubic1lem  26753  dcubic  26756  mcubic  26757  cubic2  26758  cubic  26759  dquartlem1  26761  dquartlem2  26762  dquart  26763  quart1cl  26764  quart1lem  26765  quart1  26766  quartlem2  26768  quartlem4  26770  quart  26771  atanf  26790  sinasin  26799  asinsin  26802  atanneg  26817  atancj  26820  efiatan  26822  atanlogsub  26826  efiatan2  26827  2efiatan  26828  atanbndlem  26835  dvatan  26845  atantayl  26847  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem5  26943  lgamgulmlem6  26944  lgamgulm2  26946  lgamucov  26948  lgamcvg2  26965  gamcvg  26966  gamcvg2lem  26969  ftalem2  26984  logfacrlim  27135  logexprlim  27136  lgsdirprm  27242  gausslemma2dlem1a  27276  gausslemma2dlem4  27280  2sqmod  27347  addsq2nreurex  27355  vmadivsum  27393  rpvmasumlem  27398  dchrisumlem2  27401  dchrisumlem3  27402  dchrmusum2  27405  dchrvmasumlem2  27409  dchrvmasumlem3  27410  dchrvmasumiflem1  27412  rpvmasum2  27423  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2a  27428  rplogsum  27438  mudivsum  27441  mulogsumlem  27442  mulogsum  27443  mulog2sumlem1  27445  mulog2sumlem2  27446  mulog2sumlem3  27447  vmalogdivsum2  27449  vmalogdivsum  27450  2vmadivsumlem  27451  selberglem1  27456  selberglem2  27457  selberg2lem  27461  selberg2  27462  selberg3lem1  27468  selberg4lem1  27471  selberg4  27472  pntrsumo1  27476  selberg3r  27480  selberg34r  27482  pntrlog2bndlem1  27488  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntibndlem2  27502  pntlemf  27516  pntlemo  27518  ttgcontlem1  28812  brbtwn2  28832  colinearalglem1  28833  colinearalglem2  28834  colinearalg  28837  axsegconlem1  28844  ax5seglem1  28855  ax5seglem2  28856  ax5seglem6  28861  ax5seglem9  28864  axlowdimlem17  28885  axcontlem7  28897  axcontlem8  28898  clwlkclwwlk  29931  clwwlknonex2lem1  30036  2clwwlk2clwwlk  30279  numclwwlk3lem1  30311  smcnlem  30626  ipval2  30636  4ipval2  30637  dipcj  30643  pjhthlem1  31320  submuladdd  32663  binom2subadd  32665  pythagreim  32669  quad3d  32673  lt2addrd  32674  bcm1n  32718  cycpmco2lem5  33087  cycpmco2lem6  33088  constrrtll  33721  constrrtlc1  33722  constrrtcclem  33724  constrrtcc  33725  constrsslem  33731  constrconj  33735  constrfin  33736  constrelextdg2  33737  constraddcl  33752  iconstr  33756  constrremulcl  33757  constrrecl  33759  constrmulcl  33761  constrreinvcl  33762  constrresqrtcl  33767  cos9thpiminplylem2  33773  cos9thpiminplylem3  33774  sqsscirc2  33899  signslema  34553  circlemeth  34631  logdivsqrle  34641  revpfxsfxrev  35103  revwlk  35112  subfaclim  35175  divcnvlin  35720  iprodgam  35729  dnicld1  36460  dnibndlem2  36467  dnibndlem3  36468  dnibndlem6  36471  dnibndlem9  36474  dnibndlem10  36475  dnibndlem11  36476  unblimceq0  36495  unbdqndv2lem1  36497  unbdqndv2lem2  36498  knoppndvlem11  36510  knoppndvlem15  36514  knoppndvlem17  36516  knoppndvlem21  36520  bj-bary1lem  37298  bj-bary1lem1  37299  bj-bary1  37300  ftc1cnnclem  37685  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  ftc2nc  37696  areacirclem1  37702  areacirclem4  37705  areacirc  37707  cntotbnd  37790  lcmineqlem8  42024  lcmineqlem10  42026  lcmineqlem11  42027  lcmineqlem12  42028  lcmineqlem23  42039  aks4d1p1  42064  aks6d1c5lem1  42124  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  sticksstones22  42156  bcle2d  42167  mvrrsubd  42262  lsubrotld  42265  lsubswap23d  42267  nicomachus  42300  sumcubes  42301  ef11d  42327  tanhalfpim  42337  sinpim  42338  cospim  42339  dffltz  42622  fltnltalem  42650  rencldnfilem  42808  pellexlem2  42818  pellexlem6  42822  pell1234qrne0  42841  pell1234qrmulcl  42843  rmyluc  42926  jm2.18  42977  jm2.19  42982  areaquad  43205  lhe4.4ex1a  44318  bcc0  44329  bccp1k  44330  bccm1k  44331  binomcxplemwb  44337  binomcxplemnn0  44338  binomcxplemrat  44339  binomcxplemfrat  44340  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  isosctrlem1ALT  44923  sineq0ALT  44926  oddfl  45276  dstregt0  45280  subadd4b  45281  sub31  45288  fzisoeu  45298  absnpncan2d  45300  absnpncan3d  45305  supxrgelem  45333  absimlere  45475  cvgcaule  45487  mullimc  45614  ellimcabssub0  45615  mullimcf  45621  limcrecl  45627  lptre2pt  45638  limcleqr  45642  neglimc  45645  addlimc  45646  0ellimcdiv  45647  limclner  45649  reclimc  45651  climleltrp  45674  climisp  45744  climxrrelem  45747  climxrre  45748  cnrefiisplem  45827  climxlim2lem  45843  fprodsubrecnncnvlem  45905  fperdvper  45917  dvdivbd  45921  dvbdfbdioolem2  45927  ioodvbdlimc1lem1  45929  volioc  45970  volico  45981  stoweidlem1  45999  stoweidlem11  46009  stoweidlem13  46011  stoweidlem26  46024  stoweid  46061  wallispi  46068  wallispi2lem1  46069  wallispi2lem2  46070  wallispi2  46071  stirlinglem1  46072  stirlinglem4  46075  stirlinglem5  46076  stirlinglem7  46078  stirlinglem11  46082  dirkertrigeqlem2  46097  fourierdlem4  46109  fourierdlem26  46131  fourierdlem30  46135  fourierdlem42  46147  fourierdlem63  46167  fourierdlem65  46169  fourierdlem72  46176  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem80  46184  fourierdlem81  46185  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem107  46211  fourierdlem109  46213  fouriersw  46229  etransclem1  46233  etransclem4  46236  etransclem8  46240  etransclem18  46250  etransclem20  46252  etransclem21  46253  etransclem23  46255  etransclem35  46267  etransclem46  46278  rrxtopnfi  46285  rrndistlt  46288  sge0gtfsumgt  46441  hoidmv1lelem2  46590  hoidmvlelem2  46594  smfmullem1  46789  sigarmf  46852  sigarms  46854  sigarexp  46857  sigardiv  46859  sigarcol  46862  sharhght  46863  sigaradd  46864  cevathlem2  46866  cevath  46867  resubcnnred  47305  fldivmod  47339  ceildivmod  47340  fmtnorec2lem  47543  fmtnorec3  47549  fmtnorec4  47550  lighneallem3  47608  quad1  47621  requad01  47622  requad2  47624  fppr2odd  47732  dignn0flhalflem2  48605  affinecomb2  48692  1subrec1sub  48694  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  rrx2vlinest  48730  rrx2linest  48731  line2  48741  itsclc0yqsollem1  48751  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itschlc0xyqsol1  48755  itschlc0xyqsol  48756  itsclc0xyqsolr  48758  2itscplem1  48767  2itscplem2  48768  2itscplem3  48769  itscnhlinecirc02plem1  48771  inlinecirc02plem  48775  sinhpcosh  49729  i2linesd  49768