Theorem subcld 11540

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   − cmin 11412

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220  df-sub 11414

This theorem is referenced by:  subsubadd23  11592  addsubsub23  11593  pnpncand  11606  muleqadd  11829  lineq  12026  modmuladdnn0  13887  hashfz  14399  hashfzo  14401  hashf1lem2  14428  hashf1  14429  ccatswrd  14640  pfxccatin12lem2  14703  crre  15087  remim  15090  remullem  15101  abs3lem  15312  caubnd2  15331  bhmafibid1cn  15439  bhmafibid2cn  15440  bhmafibid2  15442  rlimuni  15523  climuni  15525  rlimcld2  15551  rlimrege0  15552  rlimrecl  15553  mulcn2  15569  reccn2  15570  cn1lem  15571  o1sub  15589  rlimo1  15590  o1dif  15603  rlimsqzlem  15622  caucvgrlem2  15648  iseralt  15658  fsumparts  15779  cvgcmpce  15791  incexclem  15809  arisum2  15834  geoserg  15839  pwdif  15841  geo2sum2  15847  fallfacfwd  16009  binomfallfaclem2  16013  bpolycl  16025  bpoly3  16031  bpoly4  16032  fsumcube  16033  sinf  16099  tanval2  16108  tanval3  16109  sinneg  16121  efival  16127  sinhval  16129  bitsinv1lem  16418  bitsres  16450  pythagtriplem1  16794  pythagtriplem14  16806  pythagtriplem17  16809  dvdsprmpweqle  16864  4sqlem5  16920  mul4sqlem  16931  4sqlem17  16939  vdwlem5  16963  vdwlem6  16964  vdwlem8  16966  blcvx  24693  recld2  24710  addcnlem  24760  cnllycmp  24862  cphipval2  25148  4cphipval2  25149  cphipval  25150  ipcnlem2  25151  rrxmval  25312  rrxmetlem  25314  pjthlem1  25344  ovollb2lem  25396  itgcnlem  25698  dvlem  25804  dvconst  25825  dvid  25826  dvcnp2  25828  dvcnp2OLD  25829  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcobr  25856  dvcobrOLD  25857  dvcjbr  25860  dvrec  25866  dvmptim  25881  dvcnvlem  25887  dveflem  25890  dvsincos  25892  cmvth  25902  cmvthOLD  25903  dvlip  25905  dvlipcn  25906  c1liplem1  25908  dveq0  25912  dv11cn  25913  dvle  25919  lhop1lem  25925  dvfsumabs  25936  dvfsumlem1  25939  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumrlim  25945  dvfsumrlim2  25946  ftc1lem4  25953  ftc1lem5  25954  ftc2  25958  dgrcolem2  26187  plydiveu  26213  aaliou2b  26256  taylfvallem1  26271  taylply2  26282  taylply2OLD  26283  dvtaylp  26285  dvntaylp  26286  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulmbdd  26314  ulmcn  26315  ulmdvlem1  26316  mtest  26320  iblulm  26323  itgulm  26324  abelthlem9  26357  ptolemy  26412  tangtx  26421  sineq0  26440  efeq1  26444  efif1olem4  26461  tanarg  26535  logcnlem3  26560  logcnlem4  26561  advlogexp  26571  efopn  26574  cxpcn3lem  26664  cxpeq  26674  ang180lem4  26729  ang180lem5  26730  ang180  26731  isosctrlem2  26736  isosctrlem3  26737  isosctr  26738  ssscongptld  26739  affineequiv  26740  affineequiv2  26741  affineequiv3  26742  affineequiv4  26743  affineequivne  26744  angpieqvdlem  26745  angpieqvdlem2  26746  angpined  26747  angpieqvd  26748  chordthmlem  26749  chordthmlem2  26750  chordthmlem3  26751  chordthmlem4  26752  chordthmlem5  26753  heron  26755  quad2  26756  quad  26757  dcubic1lem  26760  dcubic  26763  mcubic  26764  cubic2  26765  cubic  26766  dquartlem1  26768  dquartlem2  26769  dquart  26770  quart1cl  26771  quart1lem  26772  quart1  26773  quartlem2  26775  quartlem4  26777  quart  26778  atanf  26797  sinasin  26806  asinsin  26809  atanneg  26824  atancj  26827  efiatan  26829  atanlogsub  26833  efiatan2  26834  2efiatan  26835  atanbndlem  26842  dvatan  26852  atantayl  26854  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamgulmlem5  26950  lgamgulmlem6  26951  lgamgulm2  26953  lgamucov  26955  lgamcvg2  26972  gamcvg  26973  gamcvg2lem  26976  ftalem2  26991  logfacrlim  27142  logexprlim  27143  lgsdirprm  27249  gausslemma2dlem1a  27283  gausslemma2dlem4  27287  2sqmod  27354  addsq2nreurex  27362  vmadivsum  27400  rpvmasumlem  27405  dchrisumlem2  27408  dchrisumlem3  27409  dchrmusum2  27412  dchrvmasumlem2  27416  dchrvmasumlem3  27417  dchrvmasumiflem1  27419  rpvmasum2  27430  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2a  27435  rplogsum  27445  mudivsum  27448  mulogsumlem  27449  mulogsum  27450  mulog2sumlem1  27452  mulog2sumlem2  27453  mulog2sumlem3  27454  vmalogdivsum2  27456  vmalogdivsum  27457  2vmadivsumlem  27458  selberglem1  27463  selberglem2  27464  selberg2lem  27468  selberg2  27469  selberg3lem1  27475  selberg4lem1  27478  selberg4  27479  pntrsumo1  27483  selberg3r  27487  selberg34r  27489  pntrlog2bndlem1  27495  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntibndlem2  27509  pntlemf  27523  pntlemo  27525  ttgcontlem1  28819  brbtwn2  28839  colinearalglem1  28840  colinearalglem2  28841  colinearalg  28844  axsegconlem1  28851  ax5seglem1  28862  ax5seglem2  28863  ax5seglem6  28868  ax5seglem9  28871  axlowdimlem17  28892  axcontlem7  28904  axcontlem8  28905  clwlkclwwlk  29938  clwwlknonex2lem1  30043  2clwwlk2clwwlk  30286  numclwwlk3lem1  30318  smcnlem  30633  ipval2  30643  4ipval2  30644  dipcj  30650  pjhthlem1  31327  submuladdd  32670  binom2subadd  32672  pythagreim  32676  quad3d  32680  lt2addrd  32681  bcm1n  32725  cycpmco2lem5  33094  cycpmco2lem6  33095  constrrtll  33728  constrrtlc1  33729  constrrtcclem  33731  constrrtcc  33732  constrsslem  33738  constrconj  33742  constrfin  33743  constrelextdg2  33744  constraddcl  33759  iconstr  33763  constrremulcl  33764  constrrecl  33766  constrmulcl  33768  constrreinvcl  33769  constrresqrtcl  33774  cos9thpiminplylem2  33780  cos9thpiminplylem3  33781  sqsscirc2  33906  signslema  34560  circlemeth  34638  logdivsqrle  34648  revpfxsfxrev  35110  revwlk  35119  subfaclim  35182  divcnvlin  35727  iprodgam  35736  dnicld1  36467  dnibndlem2  36474  dnibndlem3  36475  dnibndlem6  36478  dnibndlem9  36481  dnibndlem10  36482  dnibndlem11  36483  unblimceq0  36502  unbdqndv2lem1  36504  unbdqndv2lem2  36505  knoppndvlem11  36517  knoppndvlem15  36521  knoppndvlem17  36523  knoppndvlem21  36527  bj-bary1lem  37305  bj-bary1lem1  37306  bj-bary1  37307  ftc1cnnclem  37692  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  ftc2nc  37703  areacirclem1  37709  areacirclem4  37712  areacirc  37714  cntotbnd  37797  lcmineqlem8  42031  lcmineqlem10  42033  lcmineqlem11  42034  lcmineqlem12  42035  lcmineqlem23  42046  aks4d1p1  42071  aks6d1c5lem1  42131  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  sticksstones22  42163  bcle2d  42174  mvrrsubd  42269  lsubrotld  42272  lsubswap23d  42274  nicomachus  42307  sumcubes  42308  ef11d  42334  tanhalfpim  42344  sinpim  42345  cospim  42346  dffltz  42629  fltnltalem  42657  rencldnfilem  42815  pellexlem2  42825  pellexlem6  42829  pell1234qrne0  42848  pell1234qrmulcl  42850  rmyluc  42933  jm2.18  42984  jm2.19  42989  areaquad  43212  lhe4.4ex1a  44325  bcc0  44336  bccp1k  44337  bccm1k  44338  binomcxplemwb  44344  binomcxplemnn0  44345  binomcxplemrat  44346  binomcxplemfrat  44347  binomcxplemdvbinom  44349  binomcxplemnotnn0  44352  isosctrlem1ALT  44930  sineq0ALT  44933  oddfl  45283  dstregt0  45287  subadd4b  45288  sub31  45295  fzisoeu  45305  absnpncan2d  45307  absnpncan3d  45312  supxrgelem  45340  absimlere  45482  cvgcaule  45494  mullimc  45621  ellimcabssub0  45622  mullimcf  45628  limcrecl  45634  lptre2pt  45645  limcleqr  45649  neglimc  45652  addlimc  45653  0ellimcdiv  45654  limclner  45656  reclimc  45658  climleltrp  45681  climisp  45751  climxrrelem  45754  climxrre  45755  cnrefiisplem  45834  climxlim2lem  45850  fprodsubrecnncnvlem  45912  fperdvper  45924  dvdivbd  45928  dvbdfbdioolem2  45934  ioodvbdlimc1lem1  45936  volioc  45977  volico  45988  stoweidlem1  46006  stoweidlem11  46016  stoweidlem13  46018  stoweidlem26  46031  stoweid  46068  wallispi  46075  wallispi2lem1  46076  wallispi2lem2  46077  wallispi2  46078  stirlinglem1  46079  stirlinglem4  46082  stirlinglem5  46083  stirlinglem7  46085  stirlinglem11  46089  dirkertrigeqlem2  46104  fourierdlem4  46116  fourierdlem26  46138  fourierdlem30  46142  fourierdlem42  46154  fourierdlem63  46174  fourierdlem65  46176  fourierdlem72  46183  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem80  46191  fourierdlem81  46192  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem107  46218  fourierdlem109  46220  fouriersw  46236  etransclem1  46240  etransclem4  46243  etransclem8  46247  etransclem18  46257  etransclem20  46259  etransclem21  46260  etransclem23  46262  etransclem35  46274  etransclem46  46285  rrxtopnfi  46292  rrndistlt  46295  sge0gtfsumgt  46448  hoidmv1lelem2  46597  hoidmvlelem2  46601  smfmullem1  46796  sigarmf  46859  sigarms  46861  sigarexp  46864  sigardiv  46866  sigarcol  46869  sharhght  46870  sigaradd  46871  cevathlem2  46873  cevath  46874  resubcnnred  47309  fldivmod  47343  ceildivmod  47344  fmtnorec2lem  47547  fmtnorec3  47553  fmtnorec4  47554  lighneallem3  47612  quad1  47625  requad01  47626  requad2  47628  fppr2odd  47736  dignn0flhalflem2  48609  affinecomb2  48696  1subrec1sub  48698  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  rrx2vlinest  48734  rrx2linest  48735  line2  48745  itsclc0yqsollem1  48755  itsclc0yqsol  48757  itscnhlc0xyqsol  48758  itschlc0xyqsol1  48759  itschlc0xyqsol  48760  itsclc0xyqsolr  48762  2itscplem1  48771  2itscplem2  48772  2itscplem3  48773  itscnhlinecirc02plem1  48775  inlinecirc02plem  48779  sinhpcosh  49733  i2linesd  49772