Theorem mulm1d 11594

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 11583	. 2 ⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (-1 · 𝐴) = -𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7361  ℂcc 11029  1c1 11032   · cmul 11036  -cneg 11370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7683  ax-resscn 11088  ax-1cn 11089  ax-icn 11090  ax-addcl 11091  ax-addrcl 11092  ax-mulcl 11093  ax-mulrcl 11094  ax-mulcom 11095  ax-addass 11096  ax-mulass 11097  ax-distr 11098  ax-i2m1 11099  ax-1ne0 11100  ax-1rid 11101  ax-rnegex 11102  ax-rrecex 11103  ax-cnre 11104  ax-pre-lttri 11105  ax-pre-lttrn 11106  ax-pre-ltadd 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-pnf 11173  df-mnf 11174  df-ltxr 11176  df-sub 11371  df-neg 11372

This theorem is referenced by:  recextlem1  11772  ofnegsub  12148  modnegd  13854  modsumfzodifsn  13872  m1expcl2  14013  remullem  15056  sqrtneglem  15194  iseraltlem2  15611  iseraltlem3  15612  fsumneg  15715  incexclem  15764  incexc  15765  risefallfac  15952  efi4p  16067  cosadd  16095  absefib  16128  efieq1re  16129  pwp1fsum  16323  bitsinv1lem  16373  bezoutlem1  16471  pythagtriplem4  16752  negcncf  24876  negcncfOLD  24877  mbfneg  25612  itg1sub  25671  itgcnlem  25752  i1fibl  25770  itgitg1  25771  itgmulc2  25796  dvmptneg  25931  dvlipcn  25960  lhop2  25981  logneg  26558  lognegb  26560  tanarg  26589  logtayl  26630  logtayl2  26632  asinlem  26839  asinlem2  26840  asinsin  26863  efiatan2  26888  2efiatan  26889  atandmtan  26891  atantan  26894  atans2  26902  dvatan  26906  basellem5  27056  lgsdir2lem4  27300  gausslemma2dlem5a  27342  lgseisenlem1  27347  lgseisenlem2  27348  rpvmasum2  27484  ostth3  27610  smcnlem  30777  ipval2  30787  dipsubdir  30928  his2sub  31172  pythagreim  32828  quad3d  32832  constrnegcl  33933  qqhval2lem  34151  fwddifnp1  36372  itgmulc2nc  37902  ftc1anclem5  37911  areacirclem1  37922  lcmineqlem8  42369  readvrec  42695  negexpidd  43002  3cubeslem3r  43007  mzpsubmpt  43063  rmym1  43255  rngunsnply  43489  reabssgn  43955  sqrtcval  43960  expgrowth  44654  isumneg  45925  climneg  45933  stoweidlem22  46343  stirlinglem5  46399  fourierdlem97  46524  sqwvfourb  46550  etransclem46  46601  smfneg  47124  sharhght  47186  sigaradd  47187  altgsumbcALT  48676