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

Theorem subcl 10128
Description: Closure law for subtraction. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 21-Dec-2013.)
Assertion
Ref Expression
subcl ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐵) ∈ ℂ)

Proof of Theorem subcl
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 subval 10120 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐵) = (𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴))
2 negeu 10119 . . . 4 ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
32ancoms 467 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)
4 riotacl 6500 . . 3 (∃!𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴 → (𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
53, 4syl 17 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴) ∈ ℂ)
61, 5eqeltrd 2684 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  ∃!wreu 2894  crio 6485  (class class class)co 6524  cc 9787   + caddc 9792  cmin 10114
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-opab 4635  df-mpt 4636  df-id 4940  df-po 4946  df-so 4947  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-er 7603  df-en 7816  df-dom 7817  df-sdom 7818  df-pnf 9929  df-mnf 9930  df-ltxr 9932  df-sub 10116
This theorem is referenced by:  negcl  10129  subf  10131  pncan3  10137  npcan  10138  addsubass  10139  addsub  10140  addsub12  10142  addsubeq4  10144  npncan  10150  nppcan  10151  nnpcan  10152  nppcan3  10153  subcan2  10154  subsub2  10157  subsub4  10162  nnncan  10164  nnncan1  10165  nnncan2  10166  npncan3  10167  addsub4  10172  subadd4  10173  peano2cnm  10195  subcli  10205  subcld  10240  subeqrev  10301  subdi  10311  subdir  10312  mulsub2  10321  recextlem1  10503  recex  10505  mulcan1g  10526  div2sub  10696  cju  10860  halfaddsubcl  11108  halfaddsub  11109  iccf1o  12140  modsumfzodifsn  12557  sersub  12658  sqsubswap  12738  subsq  12786  subsq2  12787  bcn2  12920  swrdccatin12lem2b  13280  swrdccatin12lem2  13283  shftval2  13606  2shfti  13611  sqabssub  13814  abssub  13857  abs3dif  13862  abs2dif  13863  abs2difabs  13865  climuni  14074  cjcn2  14121  recn2  14122  imcn2  14123  o1sub  14137  climsub  14155  caucvgr  14197  iseralt  14206  fsum0diag2  14300  arisum2  14375  geoserg  14380  geolim  14383  geolim2  14384  georeclim  14385  geo2sum  14386  geoisum1c  14393  fallfacval2  14524  fallfacval3  14525  fallfaccl  14529  risefallfac  14537  fallfacp1  14543  0fallfac  14550  binomfallfaclem2  14553  bpoly2  14570  bpoly3  14571  fsumcube  14573  tanadd  14679  addsin  14682  fzocongeq  14827  odd2np1  14846  divalglem9  14905  phiprm  15263  pythagtriplem4  15305  pythagtriplem12  15312  pythagtriplem14  15314  pythagtriplem16  15316  fldivp1  15382  4sqlem19  15448  vdwapun  15459  vdwlem6  15471  xrsdsreclb  19555  cnmet  22314  icccvx  22485  reparphti  22533  pcorevlem  22562  cncmet  22841  dveflem  23460  dvef  23461  dv11cn  23482  coeeulem  23698  geolim3  23812  abelthlem2  23904  abelthlem7  23910  efimpi  23961  ptolemy  23966  tangtx  23975  abssinper  23988  cosne0  23994  tanregt0  24003  eflogeq  24066  logneg2  24079  advlogexp  24115  logtayl  24120  logtayl2  24122  ang180lem1  24253  ang180lem2  24254  ang180lem3  24255  lawcos  24260  pythag  24261  isosctrlem1  24262  isosctrlem2  24263  asinlem  24309  asinlem2  24310  asinlem3a  24311  asinlem3  24312  asinf  24313  acosf  24315  atanf  24321  asinneg  24327  efiasin  24329  sinasin  24330  asinsin  24333  acoscos  24334  asinbnd  24340  cosasin  24345  atanneg  24348  atancj  24351  efiatan  24353  atanlogaddlem  24354  atanlogadd  24355  atanlogsublem  24356  atanlogsub  24357  efiatan2  24358  2efiatan  24359  cosatan  24362  atantan  24364  atanbndlem  24366  atans2  24372  dvatan  24376  atantayl  24378  atantayl2  24379  birthdaylem2  24393  scvxcvx  24426  basellem8  24528  1sgm2ppw  24639  logfacbnd3  24662  logfacrlim  24663  perfect1  24667  dchrsum2  24707  sumdchr2  24709  bposlem9  24731  lgsquad2  24825  rplogsumlem1  24887  dchrmusum2  24897  log2sumbnd  24947  pntrsumo1  24968  brbtwn2  25500  colinearalg  25505  axcgrid  25511  axsegconlem1  25512  ax5seglem1  25523  ax5seglem2  25524  ax5seglem3  25526  ax5seglem5  25528  ax5seglem9  25532  axbtwnid  25534  axeuclidlem  25557  axcontlem2  25560  axcontlem4  25562  axcontlem7  25565  axcontlem8  25566  hvmulcan2  27117  subfacp1lem6  30224  cvxscon  30282  rescon  30285  sinccvglem  30623  sin2h  32369  tan2h  32371  itg2addnclem3  32433  ftc1anclem4  32458  ftc1anclem5  32459  ftc1anclem6  32460  ftc1anclem7  32461  ftc1anc  32463  dvasin  32466  dvacos  32467  rmspecsqrtnq  36288  rmspecsqrtnqOLD  36289  jm2.17a  36345  acongeq  36368  jm2.27c  36392  lhe4.4ex1a  37350  dvconstbi  37355  abssubrp  38228  pfxccatin12lem1  40088  pfxccatin12lem2  40089  cnambpcma  40165  crctcsh1wlkn0lem6  41017  eucrctshift  41410
  Copyright terms: Public domain W3C validator