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

Theorem subcl 9609
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 9601 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  =  ( iota_ x  e.  CC  ( B  +  x )  =  A ) )
2 negeu 9600 . . . 4  |-  ( ( B  e.  CC  /\  A  e.  CC )  ->  E! x  e.  CC  ( B  +  x
)  =  A )
32ancoms 453 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  E! x  e.  CC  ( B  +  x
)  =  A )
4 riotacl 6067 . . 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 2517 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   E!wreu 2717   iota_crio 6051  (class class class)co 6091   CCcc 9280    + caddc 9285    - cmin 9595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372  ax-resscn 9339  ax-1cn 9340  ax-icn 9341  ax-addcl 9342  ax-addrcl 9343  ax-mulcl 9344  ax-mulrcl 9345  ax-mulcom 9346  ax-addass 9347  ax-mulass 9348  ax-distr 9349  ax-i2m1 9350  ax-1ne0 9351  ax-1rid 9352  ax-rnegex 9353  ax-rrecex 9354  ax-cnre 9355  ax-pre-lttri 9356  ax-pre-lttrn 9357  ax-pre-ltadd 9358
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-po 4641  df-so 4642  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-riota 6052  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-er 7101  df-en 7311  df-dom 7312  df-sdom 7313  df-pnf 9420  df-mnf 9421  df-ltxr 9423  df-sub 9597
This theorem is referenced by:  negcl  9610  subf  9612  pncan3  9618  npcan  9619  addsubass  9620  addsub  9621  addsub12  9623  addsubeq4  9625  npncan  9630  nppcan  9631  nnpcan  9632  nppcan3  9633  subcan2  9634  subsub2  9637  subsub4  9642  nnncan  9644  nnncan1  9645  nnncan2  9646  npncan3  9647  addsub4  9652  subadd4  9653  subcli  9684  subcld  9719  subeqrev  9771  subdi  9778  subdir  9779  mulsub2  9788  recextlem1  9966  recex  9968  mulcan1g  9989  div2sub  10156  cju  10318  halfaddsubcl  10557  halfaddsub  10558  elnnnn0  10623  uzindOLD  10736  iccf1o  11429  sersub  11849  sqsubswap  11927  subsq  11973  subsq2  11974  bcn2  12095  swrdccatin12lem2b  12377  swrdccatin12lem2  12380  shftval2  12564  2shfti  12569  sqabssub  12772  abssub  12814  abs3dif  12819  abs2dif  12820  abs2difabs  12822  climuni  13030  cjcn2  13077  recn2  13078  imcn2  13079  o1sub  13093  climsub  13111  caucvgr  13153  iseralt  13162  fsum0diag2  13250  arisum2  13323  geoserg  13328  geolim  13330  geolim2  13331  georeclim  13332  geo2sum  13333  geoisum1c  13340  tanadd  13451  addsin  13454  fzocongeq  13587  odd2np1  13592  divalglem9  13605  phiprm  13852  pythagtriplem4  13886  pythagtriplem12  13893  pythagtriplem14  13895  pythagtriplem16  13897  fldivp1  13959  4sqlem19  14024  vdwapun  14035  vdwlem6  14047  xrsdsreclb  17860  cnmet  20351  icccvx  20522  reparphti  20569  pcorevlem  20598  cncmet  20833  dveflem  21451  dvef  21452  dv11cn  21473  coeeulem  21692  geolim3  21805  abelthlem2  21897  abelthlem7  21903  efimpi  21953  ptolemy  21958  tangtx  21967  abssinper  21980  cosne0  21986  tanregt0  21995  eflogeq  22050  logneg2  22064  advlogexp  22100  logtayl  22105  logtayl2  22107  ang180lem1  22205  ang180lem2  22206  ang180lem3  22207  lawcos  22212  pythag  22213  isosctrlem1  22216  isosctrlem2  22217  asinlem  22263  asinlem2  22264  asinlem3a  22265  asinlem3  22266  asinf  22267  acosf  22269  atanf  22275  asinneg  22281  efiasin  22283  sinasin  22284  asinsin  22287  acoscos  22288  asinbnd  22294  cosasin  22299  atanneg  22302  atancj  22305  efiatan  22307  atanlogaddlem  22308  atanlogadd  22309  atanlogsublem  22310  atanlogsub  22311  efiatan2  22312  2efiatan  22313  cosatan  22316  atantan  22318  atanbndlem  22320  atans2  22326  dvatan  22330  atantayl  22332  atantayl2  22333  birthdaylem2  22346  scvxcvx  22379  basellem8  22425  1sgm2ppw  22539  logfacbnd3  22562  logfacrlim  22563  perfect1  22567  dchrsum2  22607  sumdchr2  22609  bposlem9  22631  lgsquad2  22699  rplogsumlem1  22733  dchrmusum2  22743  log2sumbnd  22793  pntrsumo1  22814  brbtwn2  23151  colinearalg  23156  axcgrid  23162  axsegconlem1  23163  ax5seglem1  23174  ax5seglem2  23175  ax5seglem3  23177  ax5seglem5  23179  ax5seglem9  23183  axbtwnid  23185  axeuclidlem  23208  axcontlem2  23211  axcontlem4  23213  axcontlem7  23216  axcontlem8  23217  hvmulcan2  24475  subfacp1lem6  27073  cvxscon  27132  rescon  27135  sinccvglem  27317  fallfacval2  27514  fallfacval3  27515  fallfaccl  27519  risefallfac  27527  fallfacp1  27533  0fallfac  27540  binomfallfaclem2  27543  bpoly2  28200  bpoly3  28201  fsumcube  28203  sin2h  28422  tan2h  28424  itg2addnclem3  28445  ftc1anclem4  28470  ftc1anclem5  28471  ftc1anclem6  28472  ftc1anclem7  28473  ftc1anc  28475  dvasin  28480  dvacos  28481  rmspecsqrnq  29247  jm2.17a  29303  acongeq  29326  jm2.27c  29356  lhe4.4ex1a  29603  dvconstbi  29608  cnm1cn  30167  cnambpcma  30168
  Copyright terms: Public domain W3C validator