Theorem negcl 11380

Description: Closure law for negative. (Contributed by NM, 6-Aug-2003.)

Assertion

Ref	Expression
negcl	⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)

Proof of Theorem negcl

Step	Hyp	Ref	Expression
1		df-neg 11367	. 2 ⊢ -𝐴 = (0 − 𝐴)
2		0cn 11124	. . 3 ⊢ 0 ∈ ℂ
3		subcl 11379	. . 3 ⊢ ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (0 − 𝐴) ∈ ℂ)
4	2, 3	mpan 690	. 2 ⊢ (𝐴 ∈ ℂ → (0 − 𝐴) ∈ ℂ)
5	1, 4	eqeltrid 2840	1 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  0cc0 11026   − cmin 11364  -cneg 11365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-ltxr 11171  df-sub 11366  df-neg 11367

This theorem is referenced by:  negicn  11381  negcon1  11433  negdi  11438  negdi2  11439  negsubdi2  11440  neg2sub  11441  negcli  11449  negcld  11479  mulneg2  11574  mul2neg  11576  mulsub  11580  divneg  11833  divsubdir  11835  divsubdiv  11857  eqneg  11861  div2neg  11864  divneg2  11865  zeo  12578  sqneg  14038  binom2sub  14143  shftval4  15000  shftcan1  15006  shftcan2  15007  crim  15038  resub  15050  imsub  15058  cjneg  15070  cjsub  15072  absneg  15200  abs2dif2  15257  sqreulem  15283  sqreu  15284  subcn2  15518  risefallfac  15947  fallrisefac  15948  fallfac0  15951  binomrisefac  15965  efcan  16019  efne0OLD  16022  efneg  16023  efsub  16025  sinneg  16071  cosneg  16072  tanneg  16073  efmival  16078  sinhval  16079  coshval  16080  sinsub  16093  cossub  16094  sincossq  16101  cnaddablx  19797  cnaddabl  19798  cnaddinv  19800  cncrng  21343  cncrngOLD  21344  cnfldneg  21350  cnlmod  25096  cnstrcvs  25097  cncvs  25101  plyremlem  26268  reeff1o  26413  sin2pim  26450  cos2pim  26451  cxpsub  26647  cxpsqrt  26668  logrec  26729  asinlem3  26837  asinneg  26852  acosneg  26853  sinasin  26855  asinsin  26858  cosasin  26870  atantan  26889  cnaddabloOLD  30656  hvsubdistr2  31125  spanunsni  31654  ltflcei  37809  dvasin  37905  lcmineqlem1  42283  sqrtcvallem4  43880  sub2times  45521  cosknegpi  46113  etransclem18  46496  etransclem46  46524  addsubeq0  47542  altgsumbcALT  48599  1subrec1sub  48951  sinhpcosh  49985