Theorem neg1mulneg1e1 11901

Description: -1 · -1 is 1. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
neg1mulneg1e1	⊢ (-1 · -1) = 1

Proof of Theorem neg1mulneg1e1

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

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