Theorem subcld 11505

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   − cmin 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  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 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184  df-sub 11379

This theorem is referenced by:  subsubadd23  11557  addsubsub23  11558  pnpncand  11571  muleqadd  11794  lineq  11992  modmuladdnn0  13877  hashfz  14389  hashfzo  14391  hashf1lem2  14418  hashf1  14419  ccatswrd  14631  pfxccatin12lem2  14693  crre  15076  remim  15079  remullem  15090  abs3lem  15301  caubnd2  15320  bhmafibid1cn  15428  bhmafibid2cn  15429  bhmafibid2  15431  rlimuni  15512  climuni  15514  rlimcld2  15540  rlimrege0  15541  rlimrecl  15542  mulcn2  15558  reccn2  15559  cn1lem  15560  o1sub  15578  rlimo1  15579  o1dif  15592  rlimsqzlem  15611  caucvgrlem2  15637  iseralt  15647  fsumparts  15769  cvgcmpce  15781  incexclem  15801  arisum2  15826  geoserg  15831  pwdif  15833  geo2sum2  15839  fallfacfwd  16001  binomfallfaclem2  16005  bpolycl  16017  bpoly3  16023  bpoly4  16024  fsumcube  16025  sinf  16091  tanval2  16100  tanval3  16101  sinneg  16113  efival  16119  sinhval  16121  bitsinv1lem  16410  bitsres  16442  pythagtriplem1  16787  pythagtriplem14  16799  pythagtriplem17  16802  dvdsprmpweqle  16857  4sqlem5  16913  mul4sqlem  16924  4sqlem17  16932  vdwlem5  16956  vdwlem6  16957  vdwlem8  16959  blcvx  24763  recld2  24780  addcnlem  24830  cnllycmp  24923  cphipval2  25208  4cphipval2  25209  cphipval  25210  ipcnlem2  25211  rrxmval  25372  rrxmetlem  25374  pjthlem1  25404  ovollb2lem  25455  itgcnlem  25757  dvlem  25863  dvconst  25884  dvid  25885  dvcnp2  25887  dvaddbr  25905  dvmulbr  25906  dvcobr  25913  dvcjbr  25916  dvrec  25922  dvmptim  25937  dvcnvlem  25943  dveflem  25946  dvsincos  25948  cmvth  25958  dvlip  25960  dvlipcn  25961  c1liplem1  25963  dveq0  25967  dv11cn  25968  dvle  25974  lhop1lem  25980  dvfsumabs  25990  dvfsumlem1  25993  dvfsumlem2  25994  dvfsumrlim  25998  dvfsumrlim2  25999  ftc1lem4  26006  ftc1lem5  26007  ftc2  26011  dgrcolem2  26239  plydiveu  26264  aaliou2b  26307  taylfvallem1  26322  taylply2  26333  dvtaylp  26335  dvntaylp  26336  taylthlem1  26338  taylthlem2  26339  ulmbdd  26363  ulmcn  26364  ulmdvlem1  26365  mtest  26369  iblulm  26372  itgulm  26373  abelthlem9  26405  ptolemy  26460  tangtx  26469  sineq0  26488  efeq1  26492  efif1olem4  26509  tanarg  26583  logcnlem3  26608  logcnlem4  26609  advlogexp  26619  efopn  26622  cxpcn3lem  26711  cxpeq  26721  ang180lem4  26776  ang180lem5  26777  ang180  26778  isosctrlem2  26783  isosctrlem3  26784  isosctr  26785  ssscongptld  26786  affineequiv  26787  affineequiv2  26788  affineequiv3  26789  affineequiv4  26790  affineequivne  26791  angpieqvdlem  26792  angpieqvdlem2  26793  angpined  26794  angpieqvd  26795  chordthmlem  26796  chordthmlem2  26797  chordthmlem3  26798  chordthmlem4  26799  chordthmlem5  26800  heron  26802  quad2  26803  quad  26804  dcubic1lem  26807  dcubic  26810  mcubic  26811  cubic2  26812  cubic  26813  dquartlem1  26815  dquartlem2  26816  dquart  26817  quart1cl  26818  quart1lem  26819  quart1  26820  quartlem2  26822  quartlem4  26824  quart  26825  atanf  26844  sinasin  26853  asinsin  26856  atanneg  26871  atancj  26874  efiatan  26876  atanlogsub  26880  efiatan2  26881  2efiatan  26882  atanbndlem  26889  dvatan  26899  atantayl  26901  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem5  26996  lgamgulmlem6  26997  lgamgulm2  26999  lgamucov  27001  lgamcvg2  27018  gamcvg  27019  gamcvg2lem  27022  ftalem2  27037  logfacrlim  27187  logexprlim  27188  lgsdirprm  27294  gausslemma2dlem1a  27328  gausslemma2dlem4  27332  2sqmod  27399  addsq2nreurex  27407  vmadivsum  27445  rpvmasumlem  27450  dchrisumlem2  27453  dchrisumlem3  27454  dchrmusum2  27457  dchrvmasumlem2  27461  dchrvmasumlem3  27462  dchrvmasumiflem1  27464  rpvmasum2  27475  dchrisum0lem1b  27478  dchrisum0lem1  27479  dchrisum0lem2a  27480  rplogsum  27490  mudivsum  27493  mulogsumlem  27494  mulogsum  27495  mulog2sumlem1  27497  mulog2sumlem2  27498  mulog2sumlem3  27499  vmalogdivsum2  27501  vmalogdivsum  27502  2vmadivsumlem  27503  selberglem1  27508  selberglem2  27509  selberg2lem  27513  selberg2  27514  selberg3lem1  27520  selberg4lem1  27523  selberg4  27524  pntrsumo1  27528  selberg3r  27532  selberg34r  27534  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntibndlem2  27554  pntlemf  27568  pntlemo  27570  ttgcontlem1  28953  brbtwn2  28974  colinearalglem1  28975  colinearalglem2  28976  colinearalg  28979  axsegconlem1  28986  ax5seglem1  28997  ax5seglem2  28998  ax5seglem6  29003  ax5seglem9  29006  axlowdimlem17  29027  axcontlem7  29039  axcontlem8  29040  clwlkclwwlk  30072  clwwlknonex2lem1  30177  2clwwlk2clwwlk  30420  numclwwlk3lem1  30452  smcnlem  30768  ipval2  30778  4ipval2  30779  dipcj  30785  pjhthlem1  31462  submuladdd  32813  binom2subadd  32814  pythagreim  32818  quad3d  32822  lt2addrd  32823  bcm1n  32868  cycpmco2lem5  33191  cycpmco2lem6  33192  vietalem  33723  constrrtll  33875  constrrtlc1  33876  constrrtcclem  33878  constrrtcc  33879  constrsslem  33885  constrconj  33889  constrfin  33890  constrelextdg2  33891  constraddcl  33906  iconstr  33910  constrremulcl  33911  constrrecl  33913  constrmulcl  33915  constrreinvcl  33916  constrresqrtcl  33921  cos9thpiminplylem2  33927  cos9thpiminplylem3  33928  sqsscirc2  34053  signslema  34706  circlemeth  34784  logdivsqrle  34794  revpfxsfxrev  35298  revwlk  35307  subfaclim  35370  divcnvlin  35915  iprodgam  35924  dnicld1  36732  dnibndlem2  36739  dnibndlem3  36740  dnibndlem6  36743  dnibndlem9  36746  dnibndlem10  36747  dnibndlem11  36748  unblimceq0  36767  unbdqndv2lem1  36769  unbdqndv2lem2  36770  knoppndvlem11  36782  knoppndvlem15  36786  knoppndvlem17  36788  knoppndvlem21  36792  bj-bary1lem  37624  bj-bary1lem1  37625  bj-bary1  37626  qdiff  37641  ftc1cnnclem  38012  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  ftc2nc  38023  areacirclem1  38029  areacirclem4  38032  areacirc  38034  cntotbnd  38117  lcmineqlem8  42475  lcmineqlem10  42477  lcmineqlem11  42478  lcmineqlem12  42479  lcmineqlem23  42490  aks4d1p1  42515  aks6d1c5lem1  42575  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  sticksstones22  42607  bcle2d  42618  mvrrsubd  42706  lsubrotld  42709  lsubswap23d  42711  nicomachus  42744  sumcubes  42745  ef11d  42771  tanhalfpim  42781  sinpim  42782  cospim  42783  dffltz  43067  fltnltalem  43095  rencldnfilem  43248  pellexlem2  43258  pellexlem6  43262  pell1234qrne0  43281  pell1234qrmulcl  43283  rmyluc  43365  jm2.18  43416  jm2.19  43421  areaquad  43644  lhe4.4ex1a  44756  bcc0  44767  bccp1k  44768  bccm1k  44769  binomcxplemwb  44775  binomcxplemnn0  44776  binomcxplemrat  44777  binomcxplemfrat  44778  binomcxplemdvbinom  44780  binomcxplemnotnn0  44783  isosctrlem1ALT  45360  sineq0ALT  45363  oddfl  45711  dstregt0  45715  subadd4b  45716  sub31  45723  fzisoeu  45733  absnpncan2d  45735  absnpncan3d  45740  supxrgelem  45767  absimlere  45907  cvgcaule  45919  mullimc  46046  ellimcabssub0  46047  mullimcf  46053  limcrecl  46059  lptre2pt  46068  limcleqr  46072  neglimc  46075  addlimc  46076  0ellimcdiv  46077  limclner  46079  reclimc  46081  climleltrp  46104  climisp  46174  climxrrelem  46177  climxrre  46178  cnrefiisplem  46257  climxlim2lem  46273  fprodsubrecnncnvlem  46335  fperdvper  46347  dvdivbd  46351  dvbdfbdioolem2  46357  ioodvbdlimc1lem1  46359  volioc  46400  volico  46411  stoweidlem1  46429  stoweidlem11  46439  stoweidlem13  46441  stoweidlem26  46454  stoweid  46491  wallispi  46498  wallispi2lem1  46499  wallispi2lem2  46500  wallispi2  46501  stirlinglem1  46502  stirlinglem4  46505  stirlinglem5  46506  stirlinglem7  46508  stirlinglem11  46512  dirkertrigeqlem2  46527  fourierdlem4  46539  fourierdlem26  46561  fourierdlem30  46565  fourierdlem42  46577  fourierdlem63  46597  fourierdlem65  46599  fourierdlem72  46606  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem80  46614  fourierdlem81  46615  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem107  46641  fourierdlem109  46643  fouriersw  46659  etransclem1  46663  etransclem4  46666  etransclem8  46670  etransclem18  46680  etransclem20  46682  etransclem21  46683  etransclem23  46685  etransclem35  46697  etransclem46  46708  rrxtopnfi  46715  rrndistlt  46718  sge0gtfsumgt  46871  hoidmv1lelem2  47020  hoidmvlelem2  47024  smfmullem1  47219  sigarmf  47282  sigarms  47284  sigarexp  47287  sigardiv  47289  sigarcol  47292  sharhght  47293  sigaradd  47294  cevathlem2  47296  cevath  47297  sin5tlem3  47323  sin5tlem4  47324  sin5tlem5  47325  cos5t  47327  resubcnnred  47752  fldivmod  47792  ceildivmod  47793  fmtnorec2lem  48005  fmtnorec3  48011  fmtnorec4  48012  lighneallem3  48070  quad1  48096  requad01  48097  requad2  48099  fppr2odd  48207  dignn0flhalflem2  49092  affinecomb2  49179  1subrec1sub  49181  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  rrx2vlinest  49217  rrx2linest  49218  line2  49228  itsclc0yqsollem1  49238  itsclc0yqsol  49240  itscnhlc0xyqsol  49241  itschlc0xyqsol1  49242  itschlc0xyqsol  49243  itsclc0xyqsolr  49245  2itscplem1  49254  2itscplem2  49255  2itscplem3  49256  itscnhlinecirc02plem1  49258  inlinecirc02plem  49262  sinhpcosh  50215  i2linesd  50254