Theorem mulm1d 10893

Description: Product with minus one is negative. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
mulm1d.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
mulm1d	⊢ (𝜑 → (-1 · 𝐴) = -𝐴)

Proof of Theorem mulm1d

Step	Hyp	Ref	Expression
1		mulm1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulm1 10882	. 2 ⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (-1 · 𝐴) = -𝐴)

Syntax hints:   → wi 4   = wceq 1507   ∈ wcel 2050  (class class class)co 6976  ℂcc 10333  1c1 10336   · cmul 10340  -cneg 10671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3418  df-sbc 3683  df-csb 3788  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-mpt 5009  df-id 5312  df-po 5326  df-so 5327  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-er 8089  df-en 8307  df-dom 8308  df-sdom 8309  df-pnf 10476  df-mnf 10477  df-ltxr 10479  df-sub 10672  df-neg 10673

This theorem is referenced by:  recextlem1  11071  ofnegsub  11437  modnegd  13109  modsumfzodifsn  13127  m1expcl2  13266  remullem  14348  sqrtneglem  14487  iseraltlem2  14900  iseraltlem3  14901  fsumneg  15002  incexclem  15051  incexc  15052  risefallfac  15238  efi4p  15350  cosadd  15378  absefib  15411  efieq1re  15412  pwp1fsum  15602  bitsinv1lem  15650  bezoutlem1  15743  pythagtriplem4  16012  negcncf  23229  mbfneg  23954  itg1sub  24013  itgcnlem  24093  i1fibl  24111  itgitg1  24112  itgmulc2  24137  dvmptneg  24266  dvlipcn  24294  lhop2  24315  logneg  24872  lognegb  24874  tanarg  24903  logtayl  24944  logtayl2  24946  asinlem  25147  asinlem2  25148  asinsin  25171  efiatan2  25196  2efiatan  25197  atandmtan  25199  atantan  25202  atans2  25210  dvatan  25214  basellem5  25364  lgsdir2lem4  25606  gausslemma2dlem5a  25648  lgseisenlem1  25653  lgseisenlem2  25654  rpvmasum2  25790  ostth3  25916  smcnlem  28251  ipval2  28261  dipsubdir  28402  his2sub  28648  qqhval2lem  30863  fwddifnp1  33144  itgmulc2nc  34398  ftc1anclem5  34409  areacirclem1  34420  mzpsubmpt  38732  rmym1  38925  rngunsnply  39166  expgrowth  40080  isumneg  41312  climneg  41320  stoweidlem22  41736  stirlinglem5  41792  fourierdlem97  41917  sqwvfourb  41943  etransclem46  41994  smfneg  42507  sharhght  42551  sigaradd  42552  altgsumbcALT  43763