Theorem mulneg1d 10893

Description: Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

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

Assertion

Ref	Expression
mulneg1d	⊢ (𝜑 → (-𝐴 · 𝐵) = -(𝐴 · 𝐵))

Proof of Theorem mulneg1d

Step	Hyp	Ref	Expression
1		mulm1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulnegd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		mulneg1 10876	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · 𝐵) = -(𝐴 · 𝐵))
4	1, 2, 3	syl2anc 576	1 ⊢ (𝜑 → (-𝐴 · 𝐵) = -(𝐴 · 𝐵))

Syntax hints:   → wi 4   = wceq 1508   ∈ wcel 2051  (class class class)co 6975  ℂcc 10332   · cmul 10339  -cneg 10670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-resscn 10391  ax-1cn 10392  ax-icn 10393  ax-addcl 10394  ax-addrcl 10395  ax-mulcl 10396  ax-mulrcl 10397  ax-mulcom 10398  ax-addass 10399  ax-mulass 10400  ax-distr 10401  ax-i2m1 10402  ax-1ne0 10403  ax-1rid 10404  ax-rnegex 10405  ax-rrecex 10406  ax-cnre 10407  ax-pre-lttri 10408  ax-pre-lttrn 10409  ax-pre-ltadd 10410

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-reu 3090  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-po 5323  df-so 5324  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-er 8088  df-en 8306  df-dom 8307  df-sdom 8308  df-pnf 10475  df-mnf 10476  df-ltxr 10478  df-sub 10671  df-neg 10672

This theorem is referenced by:  divsubdiv  11156  recgt0  11286  xmulneg1  12477  expmulz  13289  discr1  13414  iseraltlem3  14900  incexclem  15050  incexc  15051  mulgass  18061  cphipval  23565  mbfmulc2lem  23967  mbfmulc2  23983  itg2monolem1  24070  itgmulc2  24153  dvrecg  24289  dvmptdiv  24290  dvexp3  24294  dvfsumlem2  24343  aaliou3lem2  24651  advlogexp  24955  logtayl2  24962  dcubic2  25139  dcubic  25141  ftalem5  25372  lgsdilem  25618  2sqlem4  25715  pntrsumo1  25859  pntrlog2bndlem4  25874  brbtwn2  26410  colinearalglem4  26414  axeuclidlem  26467  logdivsqrle  31602  fwddifnp1  33180  itgmulc2nc  34434  pellexlem6  38861  jm2.19lem1  39016  jm2.19lem4  39019  jm2.19  39020  binomcxplemnotnn0  40138  sineq0ALT  40724  mulltgt0  40732  fperiodmul  41030  cosknegpi  41610  itgsinexplem1  41699  stoweidlem13  41759  stoweidlem42  41788  fourierdlem39  41892  fourierdlem41  41894  fourierdlem48  41900  fourierdlem49  41901  fourierdlem64  41916  etransclem46  42026  eenglngeehlnmlem1  44122  eenglngeehlnmlem2  44123  rrx2linest  44127  rrx2linest2  44129  line2  44137  itscnhlc0yqe  44144  itschlc0yqe  44145  itsclc0yqsol  44149  itsclinecirc0b  44159  itsclquadb  44161