Theorem mulm1d 11670

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2143  (class class class)co 7410  ℂcc 11102  1c1 11105   · cmul 11109  -cneg 11446

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11161  ax-1cn 11162  ax-icn 11163  ax-addcl 11164  ax-addrcl 11165  ax-mulcl 11166  ax-mulrcl 11167  ax-mulcom 11168  ax-addass 11169  ax-mulass 11170  ax-distr 11171  ax-i2m1 11172  ax-1ne0 11173  ax-1rid 11174  ax-rnegex 11175  ax-rrecex 11176  ax-cnre 11177  ax-pre-lttri 11178  ax-pre-lttrn 11179  ax-pre-ltadd 11180

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11249  df-mnf 11250  df-ltxr 11252  df-sub 11447  df-neg 11448

This theorem is used by:  recextlem1  11848  ofnegsub  12220  modnegd  13967  modsumfzodifsn  13985  m1expcl2  14126  remullem  15184  sqrtneglem  15322  iseraltlem2  15739  iseraltlem3  15740  fsumneg  15843  incexclem  15895  incexc  15896  risefallfac  16083  efi4p  16197  cosadd  16225  absefib  16258  efieq1re  16259  pwp1fsum  16453  bitsinv1lem  16503  bezoutlem1  16601  pythagtriplem4  16883  negcncf  25090  mbfneg  25818  itg1sub  25877  itgcnlem  25958  i1fibl  25976  itgitg1  25977  itgmulc2  26002  dvmptneg  26134  dvlipcn  26162  lhop2  26183  logneg  26762  lognegb  26764  tanarg  26793  logtayl  26834  logtayl2  26836  asinlem  27042  asinlem2  27043  asinsin  27066  efiatan2  27091  2efiatan  27092  atandmtan  27094  atantan  27097  atans2  27105  dvatan  27109  basellem5  27258  lgsdir2lem4  27501  gausslemma2dlem5a  27543  lgseisenlem1  27548  lgseisenlem2  27549  rpvmasum2  27685  ostth3  27811  smcnlem  31058  ipval2  31068  dipsubdir  31209  his2sub  31453  pythagreim  33099  quad3d  33103  constrnegcl  34162  qqhval2lem  34380  fwddifnp1  36665  itgmulc2nc  38367  ftc1anclem5  38376  areacirclem1  38387  lcmineqlem8  42831  readvrec  43151  negexpidd  43441  3cubeslem3r  43446  mzpsubmpt  43502  rmym1  43690  rngunsnply  43924  reabssgn  44390  sqrtcval  44395  expgrowth  45073  isumneg  46346  climneg  46354  stoweidlem22  46764  stirlinglem5  46820  fourierdlem97  46945  sqwvfourb  46971  etransclem46  47022  smfneg  47545  sharhght  47607  sigaradd  47608  altgsumbcALT  49161