Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mulm1 | Structured version Visualization version GIF version |
Description: Product with minus one is negative. (Contributed by NM, 16-Nov-1999.) |
Ref | Expression |
---|---|
mulm1 | ⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1cn 10876 | . . 3 ⊢ 1 ∈ ℂ | |
2 | mulneg1 11357 | . . 3 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (-1 · 𝐴) = -(1 · 𝐴)) | |
3 | 1, 2 | mpan 686 | . 2 ⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -(1 · 𝐴)) |
4 | mulid2 10921 | . . 3 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | |
5 | 4 | negeqd 11161 | . 2 ⊢ (𝐴 ∈ ℂ → -(1 · 𝐴) = -𝐴) |
6 | 3, 5 | eqtrd 2777 | 1 ⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2107 (class class class)co 7260 ℂcc 10816 1c1 10819 · cmul 10823 -cneg 11152 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2708 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7571 ax-resscn 10875 ax-1cn 10876 ax-icn 10877 ax-addcl 10878 ax-addrcl 10879 ax-mulcl 10880 ax-mulrcl 10881 ax-mulcom 10882 ax-addass 10883 ax-mulass 10884 ax-distr 10885 ax-i2m1 10886 ax-1ne0 10887 ax-1rid 10888 ax-rnegex 10889 ax-rrecex 10890 ax-cnre 10891 ax-pre-lttri 10892 ax-pre-lttrn 10893 ax-pre-ltadd 10894 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3067 df-rex 3068 df-reu 3069 df-rab 3071 df-v 3429 df-sbc 3717 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-nul 4259 df-if 4462 df-pw 4537 df-sn 4564 df-pr 4566 df-op 4570 df-uni 4842 df-br 5076 df-opab 5138 df-mpt 5159 df-id 5485 df-po 5499 df-so 5500 df-xp 5591 df-rel 5592 df-cnv 5593 df-co 5594 df-dm 5595 df-rn 5596 df-res 5597 df-ima 5598 df-iota 6381 df-fun 6425 df-fn 6426 df-f 6427 df-f1 6428 df-fo 6429 df-f1o 6430 df-fv 6431 df-riota 7217 df-ov 7263 df-oprab 7264 df-mpo 7265 df-er 8461 df-en 8697 df-dom 8698 df-sdom 8699 df-pnf 10958 df-mnf 10959 df-ltxr 10961 df-sub 11153 df-neg 11154 |
This theorem is referenced by: addneg1mul 11363 mulm1i 11366 mulm1d 11373 div2neg 11644 sqrtneglem 14922 sqreulem 15015 sinhval 15807 coshval 15808 demoivreALT 15854 sinmpi 25587 cosmpi 25588 sinppi 25589 cosppi 25590 cxpsqrt 25801 relogbdiv 25872 angneg 25896 lgsdir2lem4 26419 cnnvm 28985 cncph 29122 hvm1neg 29335 hvsubdistr2 29353 lnfnsubi 30349 dvasin 35830 lcmineqlem1 40007 |
Copyright terms: Public domain | W3C validator |