Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > neg1mulneg1e1 | Structured version Visualization version GIF version |
Description: -1 · -1 is 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
neg1mulneg1e1 | ⊢ (-1 · -1) = 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1cn 10647 | . . 3 ⊢ 1 ∈ ℂ | |
2 | 1, 1 | mul2negi 11140 | . 2 ⊢ (-1 · -1) = (1 · 1) |
3 | 1t1e1 11850 | . 2 ⊢ (1 · 1) = 1 | |
4 | 2, 3 | eqtri 2782 | 1 ⊢ (-1 · -1) = 1 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 (class class class)co 7157 1c1 10590 · cmul 10594 -cneg 10923 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-sep 5174 ax-nul 5181 ax-pow 5239 ax-pr 5303 ax-un 7466 ax-resscn 10646 ax-1cn 10647 ax-icn 10648 ax-addcl 10649 ax-addrcl 10650 ax-mulcl 10651 ax-mulrcl 10652 ax-mulcom 10653 ax-addass 10654 ax-mulass 10655 ax-distr 10656 ax-i2m1 10657 ax-1ne0 10658 ax-1rid 10659 ax-rnegex 10660 ax-rrecex 10661 ax-cnre 10662 ax-pre-lttri 10663 ax-pre-lttrn 10664 ax-pre-ltadd 10665 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2902 df-ne 2953 df-nel 3057 df-ral 3076 df-rex 3077 df-reu 3078 df-rab 3080 df-v 3412 df-sbc 3700 df-csb 3809 df-dif 3864 df-un 3866 df-in 3868 df-ss 3878 df-nul 4229 df-if 4425 df-pw 4500 df-sn 4527 df-pr 4529 df-op 4533 df-uni 4803 df-br 5038 df-opab 5100 df-mpt 5118 df-id 5435 df-po 5448 df-so 5449 df-xp 5535 df-rel 5536 df-cnv 5537 df-co 5538 df-dm 5539 df-rn 5540 df-res 5541 df-ima 5542 df-iota 6300 df-fun 6343 df-fn 6344 df-f 6345 df-f1 6346 df-fo 6347 df-f1o 6348 df-fv 6349 df-riota 7115 df-ov 7160 df-oprab 7161 df-mpo 7162 df-er 8306 df-en 8542 df-dom 8543 df-sdom 8544 df-pnf 10729 df-mnf 10730 df-ltxr 10732 df-sub 10924 df-neg 10925 |
This theorem is referenced by: m1expeven 13540 cnmsgnsubg 20357 evpmodpmf1o 20376 clmnegneg 23820 plydivlem1 25003 lgsneg 26019 lgsdilem 26022 lgsdir2lem4 26026 lgsdir2 26028 ipdirilem 28726 hvnegdii 28959 honegneg 29703 1neg1t1neg1 30610 odpmco 30895 cyc3evpm 30957 sgnmul 32042 signswch 32073 sqrtcval 40760 modexp2m1d 44557 |
Copyright terms: Public domain | W3C validator |