MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  subcl Structured version   Unicode version

Theorem subcl 9310
Description: Closure law for subtraction. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 21-Dec-2013.)
Assertion
Ref Expression
subcl  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  e.  CC )

Proof of Theorem subcl
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 subval 9302 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  =  ( iota_ x  e.  CC ( B  +  x )  =  A ) )
2 negeu 9301 . . . 4  |-  ( ( B  e.  CC  /\  A  e.  CC )  ->  E! x  e.  CC  ( B  +  x
)  =  A )
32ancoms 441 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  E! x  e.  CC  ( B  +  x
)  =  A )
4 riotacl 6567 . . 3  |-  ( E! x  e.  CC  ( B  +  x )  =  A  ->  ( iota_ x  e.  CC ( B  +  x )  =  A )  e.  CC )
53, 4syl 16 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( iota_ x  e.  CC ( B  +  x
)  =  A )  e.  CC )
61, 5eqeltrd 2512 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    e. wcel 1726   E!wreu 2709  (class class class)co 6084   iota_crio 6545   CCcc 8993    + caddc 8998    - cmin 9296
This theorem is referenced by:  negcl  9311  subf  9312  pncan3  9318  npcan  9319  addsubass  9320  addsub  9321  addsub12  9323  addsubeq4  9325  npncan  9328  nppcan  9329  nppcan3  9330  subcan2  9331  subsub2  9334  subsub4  9339  nnncan  9341  nnncan1  9342  nnncan2  9343  npncan3  9344  addsub4  9349  subadd4  9350  subcli  9381  subcld  9416  subdi  9472  subdir  9473  mulsub2  9482  recextlem1  9657  recex  9659  div2sub  9844  cju  10001  halfaddsubcl  10205  halfaddsub  10206  elnnnn0  10268  uzindOLD  10369  iccf1o  11044  sersub  11371  sqsubswap  11448  subsq  11493  subsq2  11494  bcn2  11615  shftval2  11895  2shfti  11900  sqabssub  12093  abssub  12135  abs3dif  12140  abs2dif  12141  abs2difabs  12143  climuni  12351  cjcn2  12398  recn2  12399  imcn2  12400  o1sub  12414  climsub  12432  caucvgr  12474  iseralt  12483  fsum0diag2  12571  arisum2  12645  geoserg  12650  geolim  12652  geolim2  12653  georeclim  12654  geo2sum  12655  geoisum1c  12662  tanadd  12773  addsin  12776  fzocongeq  12908  odd2np1  12913  divalglem9  12926  phiprm  13171  pythagtriplem4  13198  pythagtriplem12  13205  pythagtriplem14  13207  pythagtriplem16  13209  fldivp1  13271  4sqlem19  13336  vdwapun  13347  vdwlem6  13359  xrsdsreclb  16750  cnmet  18811  icccvx  18980  reparphti  19027  pcorevlem  19056  cncmet  19280  dveflem  19868  dvef  19869  dv11cn  19890  coeeulem  20148  geolim3  20261  abelthlem2  20353  abelthlem7  20359  efimpi  20404  ptolemy  20409  tangtx  20418  abssinper  20431  cosne0  20437  tanregt0  20446  eflogeq  20501  logneg2  20515  advlogexp  20551  logtayl  20556  logtayl2  20558  ang180lem1  20656  ang180lem2  20657  ang180lem3  20658  lawcos  20663  pythag  20664  isosctrlem1  20667  isosctrlem2  20668  asinlem  20713  asinlem2  20714  asinlem3a  20715  asinlem3  20716  asinf  20717  acosf  20719  atanf  20725  asinneg  20731  efiasin  20733  sinasin  20734  asinsin  20737  acoscos  20738  asinbnd  20744  cosasin  20749  atanneg  20752  atancj  20755  efiatan  20757  atanlogaddlem  20758  atanlogadd  20759  atanlogsublem  20760  atanlogsub  20761  efiatan2  20762  2efiatan  20763  cosatan  20766  atantan  20768  atanbndlem  20770  atans2  20776  dvatan  20780  atantayl  20782  atantayl2  20783  birthdaylem2  20796  scvxcvx  20829  basellem8  20875  1sgm2ppw  20989  logfacbnd3  21012  logfacrlim  21013  perfect1  21017  dchrsum2  21057  sumdchr2  21059  bposlem9  21081  lgsquad2  21149  rplogsumlem1  21183  dchrmusum2  21193  log2sumbnd  21243  pntrsumo1  21264  hvmulcan2  22580  subfacp1lem6  24876  cvxscon  24935  rescon  24938  sinccvglem  25114  mulcan1g  25194  subeqrev  25202  fallfacval2  25332  fallfacval3  25333  fallfaccl  25337  risefallfac  25345  fallfacp1  25351  0fallfac  25358  binomfallfaclem2  25361  brbtwn2  25849  colinearalg  25854  axcgrid  25860  axsegconlem1  25861  ax5seglem1  25872  ax5seglem2  25873  ax5seglem3  25875  ax5seglem5  25877  ax5seglem9  25881  axbtwnid  25883  axeuclidlem  25906  axcontlem2  25909  axcontlem4  25911  axcontlem7  25914  axcontlem8  25915  bpoly2  26108  bpoly3  26109  fsumcube  26111  sin2h  26250  tan2h  26252  itg2addnclem3  26272  ftc1anclem4  26297  ftc1anclem5  26298  ftc1anclem6  26299  ftc1anclem7  26300  ftc1anc  26302  rmspecsqrnq  26983  jm2.17a  27039  acongeq  27062  jm2.27c  27092  lhe4.4ex1a  27537  dvconstbi  27542  cnm1cn  28111  swrdccatin12lem3b  28243  swrdccatin12lem3  28246  cshwidx  28276  cshwidxm  28280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-po 4506  df-so 4507  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-riota 6552  df-er 6908  df-en 7113  df-dom 7114  df-sdom 7115  df-pnf 9127  df-mnf 9128  df-ltxr 9130  df-sub 9298
  Copyright terms: Public domain W3C validator