Theorem negcl 11221

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 11208	. 2 ⊢ -𝐴 = (0 − 𝐴)
2		0cn 10968	. . 3 ⊢ 0 ∈ ℂ
3		subcl 11220	. . 3 ⊢ ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (0 − 𝐴) ∈ ℂ)
4	2, 3	mpan 687	. 2 ⊢ (𝐴 ∈ ℂ → (0 − 𝐴) ∈ ℂ)
5	1, 4	eqeltrid 2845	1 ⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2110  (class class class)co 7271  ℂcc 10870  0cc0 10872   − cmin 11205  -cneg 11206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582  ax-resscn 10929  ax-1cn 10930  ax-icn 10931  ax-addcl 10932  ax-addrcl 10933  ax-mulcl 10934  ax-mulrcl 10935  ax-mulcom 10936  ax-addass 10937  ax-mulass 10938  ax-distr 10939  ax-i2m1 10940  ax-1ne0 10941  ax-1rid 10942  ax-rnegex 10943  ax-rrecex 10944  ax-cnre 10945  ax-pre-lttri 10946  ax-pre-lttrn 10947  ax-pre-ltadd 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-riota 7228  df-ov 7274  df-oprab 7275  df-mpo 7276  df-er 8481  df-en 8717  df-dom 8718  df-sdom 8719  df-pnf 11012  df-mnf 11013  df-ltxr 11015  df-sub 11207  df-neg 11208

This theorem is referenced by:  negicn  11222  negcon1  11273  negdi  11278  negdi2  11279  negsubdi2  11280  neg2sub  11281  negcli  11289  negcld  11319  mulneg2  11412  mul2neg  11414  mulsub  11418  divneg  11667  divsubdir  11669  divsubdiv  11691  eqneg  11695  div2neg  11698  divneg2  11699  zeo  12406  sqneg  13834  binom2sub  13933  shftval4  14786  shftcan1  14792  shftcan2  14793  crim  14824  resub  14836  imsub  14844  cjneg  14856  cjsub  14858  absneg  14987  abs2dif2  15043  sqreulem  15069  sqreu  15070  subcn2  15302  risefallfac  15732  fallrisefac  15733  fallfac0  15736  binomrisefac  15750  efcan  15803  efne0  15804  efneg  15805  efsub  15807  sinneg  15853  cosneg  15854  tanneg  15855  efmival  15860  sinhval  15861  coshval  15862  sinsub  15875  cossub  15876  sincossq  15883  cnaddablx  19467  cnaddabl  19468  cnaddinv  19470  cncrng  20617  cnfldneg  20622  cnlmod  24301  cnstrcvs  24302  cncvs  24306  plyremlem  25462  reeff1o  25604  sin2pim  25640  cos2pim  25641  cxpsub  25835  cxpsqrt  25856  logrec  25911  asinlem3  26019  asinneg  26034  acosneg  26035  sinasin  26037  asinsin  26040  cosasin  26052  atantan  26071  cnaddabloOLD  28939  hvsubdistr2  29408  spanunsni  29937  ltflcei  35761  dvasin  35857  lcmineqlem1  40034  sqrtcvallem4  41217  sub2times  42783  cosknegpi  43381  etransclem18  43764  etransclem46  43792  addsubeq0  44757  altgsumbcALT  45658  1subrec1sub  46020  sinhpcosh  46411