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

Theorem subcl 9810
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 9802 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  =  ( iota_ x  e.  CC  ( B  +  x )  =  A ) )
2 negeu 9801 . . . 4  |-  ( ( B  e.  CC  /\  A  e.  CC )  ->  E! x  e.  CC  ( B  +  x
)  =  A )
32ancoms 451 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  E! x  e.  CC  ( B  +  x
)  =  A )
4 riotacl 6246 . . 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 2542 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1398    e. wcel 1823   E!wreu 2806   iota_crio 6231  (class class class)co 6270   CCcc 9479    + caddc 9484    - cmin 9796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-po 4789  df-so 4790  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-ltxr 9622  df-sub 9798
This theorem is referenced by:  negcl  9811  subf  9813  pncan3  9819  npcan  9820  addsubass  9821  addsub  9822  addsub12  9824  addsubeq4  9826  npncan  9831  nppcan  9832  nnpcan  9833  nppcan3  9834  subcan2  9835  subsub2  9838  subsub4  9843  nnncan  9845  nnncan1  9846  nnncan2  9847  npncan3  9848  addsub4  9853  subadd4  9854  peano2cnm  9876  subcli  9886  subcld  9922  subeqrev  9978  subdi  9986  subdir  9987  mulsub2  9996  recextlem1  10175  recex  10177  mulcan1g  10198  div2sub  10365  cju  10527  halfaddsubcl  10767  halfaddsub  10768  uzindOLD  10953  iccf1o  11667  sersub  12132  sqsubswap  12211  subsq  12257  subsq2  12258  bcn2  12379  swrdccatin12lem2b  12702  swrdccatin12lem2  12705  shftval2  12990  2shfti  12995  sqabssub  13198  abssub  13241  abs3dif  13246  abs2dif  13247  abs2difabs  13249  climuni  13457  cjcn2  13504  recn2  13505  imcn2  13506  o1sub  13520  climsub  13538  caucvgr  13580  iseralt  13589  fsum0diag2  13680  arisum2  13754  geoserg  13759  geolim  13761  geolim2  13762  georeclim  13763  geo2sum  13764  geoisum1c  13771  tanadd  13984  addsin  13987  fzocongeq  14124  odd2np1  14130  divalglem9  14143  phiprm  14391  pythagtriplem4  14427  pythagtriplem12  14434  pythagtriplem14  14436  pythagtriplem16  14438  fldivp1  14500  4sqlem19  14565  vdwapun  14576  vdwlem6  14588  xrsdsreclb  18660  cnmet  21445  icccvx  21616  reparphti  21663  pcorevlem  21692  cncmet  21927  dveflem  22546  dvef  22547  dv11cn  22568  coeeulem  22787  geolim3  22901  abelthlem2  22993  abelthlem7  22999  efimpi  23050  ptolemy  23055  tangtx  23064  abssinper  23077  cosne0  23083  tanregt0  23092  eflogeq  23155  logneg2  23168  advlogexp  23204  logtayl  23209  logtayl2  23211  ang180lem1  23340  ang180lem2  23341  ang180lem3  23342  lawcos  23347  pythag  23348  isosctrlem1  23349  isosctrlem2  23350  asinlem  23396  asinlem2  23397  asinlem3a  23398  asinlem3  23399  asinf  23400  acosf  23402  atanf  23408  asinneg  23414  efiasin  23416  sinasin  23417  asinsin  23420  acoscos  23421  asinbnd  23427  cosasin  23432  atanneg  23435  atancj  23438  efiatan  23440  atanlogaddlem  23441  atanlogadd  23442  atanlogsublem  23443  atanlogsub  23444  efiatan2  23445  2efiatan  23446  cosatan  23449  atantan  23451  atanbndlem  23453  atans2  23459  dvatan  23463  atantayl  23465  atantayl2  23466  birthdaylem2  23480  scvxcvx  23513  basellem8  23559  1sgm2ppw  23673  logfacbnd3  23696  logfacrlim  23697  perfect1  23701  dchrsum2  23741  sumdchr2  23743  bposlem9  23765  lgsquad2  23833  rplogsumlem1  23867  dchrmusum2  23877  log2sumbnd  23927  pntrsumo1  23948  brbtwn2  24410  colinearalg  24415  axcgrid  24421  axsegconlem1  24422  ax5seglem1  24433  ax5seglem2  24434  ax5seglem3  24436  ax5seglem5  24438  ax5seglem9  24442  axbtwnid  24444  axeuclidlem  24467  axcontlem2  24470  axcontlem4  24472  axcontlem7  24475  axcontlem8  24476  hvmulcan2  26188  subfacp1lem6  28893  cvxscon  28952  rescon  28955  sinccvglem  29302  fallfacval2  29374  fallfacval3  29375  fallfaccl  29379  risefallfac  29387  fallfacp1  29393  0fallfac  29400  binomfallfaclem2  29403  bpoly2  30047  bpoly3  30048  fsumcube  30050  sin2h  30285  tan2h  30287  itg2addnclem3  30308  ftc1anclem4  30333  ftc1anclem5  30334  ftc1anclem6  30335  ftc1anclem7  30336  ftc1anc  30338  dvasin  30343  dvacos  30344  rmspecsqrtnq  31081  jm2.17a  31137  acongeq  31160  jm2.27c  31188  lhe4.4ex1a  31475  dvconstbi  31480  abssubrp  31697  pfxccatin12lem1  32651  pfxccatin12lem2  32652  cnambpcma  32689
  Copyright terms: Public domain W3C validator