MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  subcld Structured version   Visualization version   GIF version

Theorem subcld 10986
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
StepHypRef Expression
1 negidd.1 . 2 (𝜑𝐴 ∈ ℂ)
2 pncand.2 . 2 (𝜑𝐵 ∈ ℂ)
3 subcl 10874 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐵) ∈ ℂ)
41, 2, 3syl2anc 587 1 (𝜑 → (𝐴𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  (class class class)co 7135  cc 10524  cmin 10859
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-po 5438  df-so 5439  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-ltxr 10669  df-sub 10861
This theorem is referenced by:  pnpncand  11050  muleqadd  11273  lineq  11466  modmuladdnn0  13278  hashfz  13784  hashfzo  13786  hashf1lem2  13810  hashf1  13811  ccatswrd  14021  pfxccatin12lem2  14084  crre  14465  remim  14468  remullem  14479  abs3lem  14690  caubnd2  14709  bhmafibid1cn  14815  bhmafibid2cn  14816  bhmafibid2  14818  rlimuni  14899  climuni  14901  rlimcld2  14927  rlimrege0  14928  rlimrecl  14929  mulcn2  14944  reccn2  14945  cn1lem  14946  o1sub  14964  rlimo1  14965  o1dif  14978  rlimsqzlem  14997  caucvgrlem2  15023  iseralt  15033  fsumparts  15153  cvgcmpce  15165  incexclem  15183  arisum2  15208  geoserg  15213  pwdif  15215  geo2sum2  15222  fallfacfwd  15382  binomfallfaclem2  15386  bpolycl  15398  bpoly3  15404  bpoly4  15405  fsumcube  15406  sinf  15469  tanval2  15478  tanval3  15479  sinneg  15491  efival  15497  sinhval  15499  bitsinv1lem  15780  bitsres  15812  pythagtriplem1  16143  pythagtriplem14  16155  pythagtriplem17  16158  dvdsprmpweqle  16212  4sqlem5  16268  mul4sqlem  16279  4sqlem17  16287  vdwlem5  16311  vdwlem6  16312  vdwlem8  16314  blcvx  23403  recld2  23419  addcnlem  23469  cnllycmp  23561  cphipval2  23845  4cphipval2  23846  cphipval  23847  ipcnlem2  23848  rrxmval  24009  rrxmetlem  24011  pjthlem1  24041  ovollb2lem  24092  itgcnlem  24393  dvlem  24499  dvconst  24520  dvid  24521  dvcnp2  24523  dvaddbr  24541  dvmulbr  24542  dvcobr  24549  dvcjbr  24552  dvrec  24558  dvmptim  24573  dvcnvlem  24579  dveflem  24582  dvsincos  24584  cmvth  24594  dvlip  24596  dvlipcn  24597  c1liplem1  24599  dveq0  24603  dv11cn  24604  dvle  24610  lhop1lem  24616  dvfsumabs  24626  dvfsumlem1  24629  dvfsumlem2  24630  dvfsumrlim  24634  dvfsumrlim2  24635  ftc1lem4  24642  ftc1lem5  24643  ftc2  24647  dgrcolem2  24871  plydiveu  24894  aaliou2b  24937  taylfvallem1  24952  taylply2  24963  dvtaylp  24965  dvntaylp  24966  taylthlem1  24968  taylthlem2  24969  ulmbdd  24993  ulmcn  24994  ulmdvlem1  24995  mtest  24999  iblulm  25002  itgulm  25003  abelthlem9  25035  ptolemy  25089  tangtx  25098  sineq0  25116  efeq1  25120  efif1olem4  25137  tanarg  25210  logcnlem3  25235  logcnlem4  25236  advlogexp  25246  efopn  25249  cxpcn3lem  25336  cxpeq  25346  ang180lem4  25398  ang180lem5  25399  ang180  25400  isosctrlem2  25405  isosctrlem3  25406  isosctr  25407  ssscongptld  25408  affineequiv  25409  affineequiv2  25410  affineequiv3  25411  affineequiv4  25412  affineequivne  25413  angpieqvdlem  25414  angpieqvdlem2  25415  angpined  25416  angpieqvd  25417  chordthmlem  25418  chordthmlem2  25419  chordthmlem3  25420  chordthmlem4  25421  chordthmlem5  25422  heron  25424  quad2  25425  quad  25426  dcubic1lem  25429  dcubic  25432  mcubic  25433  cubic2  25434  cubic  25435  dquartlem1  25437  dquartlem2  25438  dquart  25439  quart1cl  25440  quart1lem  25441  quart1  25442  quartlem2  25444  quartlem4  25446  quart  25447  atanf  25466  sinasin  25475  asinsin  25478  atanneg  25493  atancj  25496  efiatan  25498  atanlogsub  25502  efiatan2  25503  2efiatan  25504  atanbndlem  25511  dvatan  25521  atantayl  25523  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamgulmlem5  25618  lgamgulmlem6  25619  lgamgulm2  25621  lgamucov  25623  lgamcvg2  25640  gamcvg  25641  gamcvg2lem  25644  ftalem2  25659  logfacrlim  25808  logexprlim  25809  lgsdirprm  25915  gausslemma2dlem1a  25949  gausslemma2dlem4  25953  2sqmod  26020  addsq2nreurex  26028  vmadivsum  26066  rpvmasumlem  26071  dchrisumlem2  26074  dchrisumlem3  26075  dchrmusum2  26078  dchrvmasumlem2  26082  dchrvmasumlem3  26083  dchrvmasumiflem1  26085  rpvmasum2  26096  dchrisum0lem1b  26099  dchrisum0lem1  26100  dchrisum0lem2a  26101  rplogsum  26111  mudivsum  26114  mulogsumlem  26115  mulogsum  26116  mulog2sumlem1  26118  mulog2sumlem2  26119  mulog2sumlem3  26120  vmalogdivsum2  26122  vmalogdivsum  26123  2vmadivsumlem  26124  selberglem1  26129  selberglem2  26130  selberg2lem  26134  selberg2  26135  selberg3lem1  26141  selberg4lem1  26144  selberg4  26145  pntrsumo1  26149  selberg3r  26153  selberg34r  26155  pntrlog2bndlem1  26161  pntrlog2bndlem2  26162  pntrlog2bndlem3  26163  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntibndlem2  26175  pntlemf  26189  pntlemo  26191  ttgcontlem1  26679  brbtwn2  26699  colinearalglem1  26700  colinearalglem2  26701  colinearalg  26704  axsegconlem1  26711  ax5seglem1  26722  ax5seglem2  26723  ax5seglem6  26728  ax5seglem9  26731  axlowdimlem17  26752  axcontlem7  26764  axcontlem8  26765  clwlkclwwlk  27787  clwwlknonex2lem1  27892  2clwwlk2clwwlk  28135  numclwwlk3lem1  28167  smcnlem  28480  ipval2  28490  4ipval2  28491  dipcj  28497  pjhthlem1  29174  lt2addrd  30501  bcm1n  30544  cycpmco2lem5  30822  cycpmco2lem6  30823  sqsscirc2  31262  signslema  31942  circlemeth  32021  logdivsqrle  32031  revpfxsfxrev  32472  revwlk  32481  subfaclim  32545  divcnvlin  33074  iprodgam  33084  dnicld1  33921  dnibndlem2  33928  dnibndlem3  33929  dnibndlem6  33932  dnibndlem9  33935  dnibndlem10  33936  dnibndlem11  33937  unblimceq0  33956  unbdqndv2lem1  33958  unbdqndv2lem2  33959  knoppndvlem11  33971  knoppndvlem15  33975  knoppndvlem17  33977  knoppndvlem21  33981  bj-bary1lem  34721  bj-bary1lem1  34722  bj-bary1  34723  ftc1cnnclem  35125  ftc1anclem7  35133  ftc1anclem8  35134  ftc1anc  35135  ftc2nc  35136  areacirclem1  35142  areacirclem4  35145  areacirc  35147  cntotbnd  35231  lcmineqlem8  39321  lcmineqlem10  39323  lcmineqlem11  39324  lcmineqlem12  39325  lcmineqlem23  39336  metakunt15  39359  metakunt16  39360  metakunt29  39373  metakunt30  39374  dffltz  39610  fltnltalem  39613  rencldnfilem  39756  pellexlem2  39766  pellexlem6  39770  pell1234qrne0  39789  pell1234qrmulcl  39791  rmyluc  39873  jm2.18  39924  jm2.19  39929  areaquad  40161  lhe4.4ex1a  41028  bcc0  41039  bccp1k  41040  bccm1k  41041  binomcxplemwb  41047  binomcxplemnn0  41048  binomcxplemrat  41049  binomcxplemfrat  41050  binomcxplemdvbinom  41052  binomcxplemnotnn0  41055  isosctrlem1ALT  41635  sineq0ALT  41638  oddfl  41903  dstregt0  41907  subadd4b  41908  sub31  41917  fzisoeu  41927  absnpncan2d  41929  absnpncan3d  41934  supxrgelem  41964  absimlere  42114  mullimc  42253  ellimcabssub0  42254  mullimcf  42260  limcrecl  42266  lptre2pt  42277  limcleqr  42281  neglimc  42284  addlimc  42285  0ellimcdiv  42286  limclner  42288  reclimc  42290  climleltrp  42313  climisp  42383  climxrrelem  42386  climxrre  42387  cnrefiisplem  42466  climxlim2lem  42482  fprodsubrecnncnvlem  42544  fperdvper  42556  dvdivbd  42560  dvbdfbdioolem2  42566  ioodvbdlimc1lem1  42568  volioc  42609  volico  42620  stoweidlem1  42638  stoweidlem11  42648  stoweidlem13  42650  stoweidlem26  42663  stoweid  42700  wallispi  42707  wallispi2lem1  42708  wallispi2lem2  42709  wallispi2  42710  stirlinglem1  42711  stirlinglem4  42714  stirlinglem5  42715  stirlinglem7  42717  stirlinglem11  42721  dirkertrigeqlem2  42736  fourierdlem4  42748  fourierdlem26  42770  fourierdlem30  42774  fourierdlem42  42786  fourierdlem63  42806  fourierdlem65  42808  fourierdlem72  42815  fourierdlem74  42817  fourierdlem75  42818  fourierdlem76  42819  fourierdlem80  42823  fourierdlem81  42824  fourierdlem89  42832  fourierdlem90  42833  fourierdlem91  42834  fourierdlem107  42850  fourierdlem109  42852  fouriersw  42868  etransclem1  42872  etransclem4  42875  etransclem8  42879  etransclem18  42889  etransclem20  42891  etransclem21  42892  etransclem23  42894  etransclem35  42906  etransclem46  42917  rrxtopnfi  42924  rrndistlt  42927  sge0gtfsumgt  43077  hoidmv1lelem2  43226  hoidmvlelem2  43230  smfmullem1  43418  sigarmf  43463  sigarms  43465  sigarexp  43468  sigardiv  43470  sigarcol  43473  sharhght  43474  sigaradd  43475  cevathlem2  43477  cevath  43478  resubcnnred  43856  fmtnorec2lem  44054  fmtnorec3  44060  fmtnorec4  44061  lighneallem3  44120  quad1  44133  requad01  44134  requad2  44136  fppr2odd  44244  fldivmod  44927  dignn0flhalflem2  45025  affinecomb2  45112  1subrec1sub  45114  eenglngeehlnmlem1  45146  eenglngeehlnmlem2  45147  rrx2vlinest  45150  rrx2linest  45151  line2  45161  itsclc0yqsollem1  45171  itsclc0yqsol  45173  itscnhlc0xyqsol  45174  itschlc0xyqsol1  45175  itschlc0xyqsol  45176  itsclc0xyqsolr  45178  2itscplem1  45187  2itscplem2  45188  2itscplem3  45189  itscnhlinecirc02plem1  45191  inlinecirc02plem  45195  sinhpcosh  45261  i2linesd  45302
  Copyright terms: Public domain W3C validator