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

Theorem subcl 9819
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 9811 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  =  ( iota_ x  e.  CC  ( B  +  x )  =  A ) )
2 negeu 9810 . . . 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 6253 . . 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 2529 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  -  B
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1381    e. wcel 1802   E!wreu 2793   iota_crio 6237  (class class class)co 6277   CCcc 9488    + caddc 9493    - cmin 9805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-po 4786  df-so 4787  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-er 7309  df-en 7515  df-dom 7516  df-sdom 7517  df-pnf 9628  df-mnf 9629  df-ltxr 9631  df-sub 9807
This theorem is referenced by:  negcl  9820  subf  9822  pncan3  9828  npcan  9829  addsubass  9830  addsub  9831  addsub12  9833  addsubeq4  9835  npncan  9840  nppcan  9841  nnpcan  9842  nppcan3  9843  subcan2  9844  subsub2  9847  subsub4  9852  nnncan  9854  nnncan1  9855  nnncan2  9856  npncan3  9857  addsub4  9862  subadd4  9863  peano2cnm  9885  subcli  9895  subcld  9931  subeqrev  9983  subdi  9991  subdir  9992  mulsub2  10001  recextlem1  10180  recex  10182  mulcan1g  10203  div2sub  10370  cju  10533  halfaddsubcl  10772  halfaddsub  10773  uzindOLD  10958  iccf1o  11668  sersub  12124  sqsubswap  12203  subsq  12249  subsq2  12250  bcn2  12371  swrdccatin12lem2b  12685  swrdccatin12lem2  12688  shftval2  12882  2shfti  12887  sqabssub  13090  abssub  13133  abs3dif  13138  abs2dif  13139  abs2difabs  13141  climuni  13349  cjcn2  13396  recn2  13397  imcn2  13398  o1sub  13412  climsub  13430  caucvgr  13472  iseralt  13481  fsum0diag2  13572  arisum2  13646  geoserg  13651  geolim  13653  geolim2  13654  georeclim  13655  geo2sum  13656  geoisum1c  13663  tanadd  13774  addsin  13777  fzocongeq  13912  odd2np1  13918  divalglem9  13931  phiprm  14179  pythagtriplem4  14215  pythagtriplem12  14222  pythagtriplem14  14224  pythagtriplem16  14226  fldivp1  14288  4sqlem19  14353  vdwapun  14364  vdwlem6  14376  xrsdsreclb  18333  cnmet  21145  icccvx  21316  reparphti  21363  pcorevlem  21392  cncmet  21627  dveflem  22246  dvef  22247  dv11cn  22268  coeeulem  22487  geolim3  22600  abelthlem2  22692  abelthlem7  22698  efimpi  22749  ptolemy  22754  tangtx  22763  abssinper  22776  cosne0  22782  tanregt0  22791  eflogeq  22851  logneg2  22865  advlogexp  22901  logtayl  22906  logtayl2  22908  ang180lem1  23006  ang180lem2  23007  ang180lem3  23008  lawcos  23013  pythag  23014  isosctrlem1  23017  isosctrlem2  23018  asinlem  23064  asinlem2  23065  asinlem3a  23066  asinlem3  23067  asinf  23068  acosf  23070  atanf  23076  asinneg  23082  efiasin  23084  sinasin  23085  asinsin  23088  acoscos  23089  asinbnd  23095  cosasin  23100  atanneg  23103  atancj  23106  efiatan  23108  atanlogaddlem  23109  atanlogadd  23110  atanlogsublem  23111  atanlogsub  23112  efiatan2  23113  2efiatan  23114  cosatan  23117  atantan  23119  atanbndlem  23121  atans2  23127  dvatan  23131  atantayl  23133  atantayl2  23134  birthdaylem2  23147  scvxcvx  23180  basellem8  23226  1sgm2ppw  23340  logfacbnd3  23363  logfacrlim  23364  perfect1  23368  dchrsum2  23408  sumdchr2  23410  bposlem9  23432  lgsquad2  23500  rplogsumlem1  23534  dchrmusum2  23544  log2sumbnd  23594  pntrsumo1  23615  brbtwn2  24073  colinearalg  24078  axcgrid  24084  axsegconlem1  24085  ax5seglem1  24096  ax5seglem2  24097  ax5seglem3  24099  ax5seglem5  24101  ax5seglem9  24105  axbtwnid  24107  axeuclidlem  24130  axcontlem2  24133  axcontlem4  24135  axcontlem7  24138  axcontlem8  24139  hvmulcan2  25855  subfacp1lem6  28495  cvxscon  28554  rescon  28557  sinccvglem  28904  fallfacval2  29101  fallfacval3  29102  fallfaccl  29106  risefallfac  29114  fallfacp1  29120  0fallfac  29127  binomfallfaclem2  29130  bpoly2  29787  bpoly3  29788  fsumcube  29790  sin2h  30013  tan2h  30015  itg2addnclem3  30036  ftc1anclem4  30061  ftc1anclem5  30062  ftc1anclem6  30063  ftc1anclem7  30064  ftc1anc  30066  dvasin  30071  dvacos  30072  rmspecsqrtnq  30810  jm2.17a  30866  acongeq  30889  jm2.27c  30917  lhe4.4ex1a  31203  dvconstbi  31208  abssubrp  31402  cnambpcma  32149
  Copyright terms: Public domain W3C validator