![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mulneg1d | Structured version Visualization version GIF version |
Description: Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
mulm1d.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
mulnegd.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
Ref | Expression |
---|---|
mulneg1d | ⊢ (𝜑 → (-𝐴 · 𝐵) = -(𝐴 · 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mulm1d.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | mulnegd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | mulneg1 10876 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · 𝐵) = -(𝐴 · 𝐵)) | |
4 | 1, 2, 3 | syl2anc 576 | 1 ⊢ (𝜑 → (-𝐴 · 𝐵) = -(𝐴 · 𝐵)) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |