Theorem mulm1d 11768

Description: Product with minus one is negative. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

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

Assertion

Ref	Expression
mulm1d	⊢ (𝜑 → ( -1 · 𝐴) = -𝐴)

Proof of Theorem mulm1d

Step	Hyp	Ref	Expression
1		mulm1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulm1 11757	. 2 ⊢ (𝐴 ∈ ℂ → ( -1 · 𝐴) = -𝐴)
3	1, 2	syl 18	1 ⊢ (𝜑 → ( -1 · 𝐴) = -𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11198  1c1 11201   · cmul 11205   -cneg 11542

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348  df-sub 11543  df-neg 11544

This theorem is used by:  recextlem1  11946  ofnegsub  12318  modnegd  14069  modsumfzodifsn  14087  m1expcl2  14228  remullem  15295  sqrtneglem  15433  iseraltlem2  15850  iseraltlem3  15851  fsumneg  15953  incexclem  16005  incexc  16006  risefallfac  16191  efi4p  16305  cosadd  16333  absefib  16366  efieq1re  16367  pwp1fsum  16561  bitsinv1lem  16611  bezoutlem1  16712  pythagtriplem4  16997  negcncf  25243  mbfneg  25971  itg1sub  26030  itgcnlem  26110  i1fibl  26128  itgitg1  26129  itgmulc2  26154  dvmptneg  26286  dvlipcn  26314  lhop2  26335  logneg  26916  lognegb  26918  tanarg  26947  logtayl  26988  logtayl2  26990  asinlem  27196  asinlem2  27197  asinsin  27220  efiatan2  27245  2efiatan  27246  atandmtan  27248  atantan  27251  atans2  27259  dvatan  27263  basellem5  27412  lgsdir2lem4  27655  gausslemma2dlem5a  27697  lgseisenlem1  27702  lgseisenlem2  27703  rpvmasum2  27839  ostth3  27965  smcnlem  31299  ipval2  31309  dipsubdir  31450  his2sub  31694  pythagreim  33379  quad3d  33383  constrnegcl  34437  qqhval2lem  34655  fwddifnp1  36972  itgmulc2nc  38649  ftc1anclem5  38658  areacirclem1  38669  lcmineqlem8  43129  readvrec  43456  negexpidd  43735  3cubeslem3r  43740  mzpsubmpt  43797  rmym1  43985  rngunsnply  44214  reabssgn  44679  sqrtcval  44684  expgrowth  45362  isumneg  46657  climneg  46665  stoweidlem22  47075  stirlinglem5  47131  fourierdlem97  47256  sqwvfourb  47282  etransclem46  47333  smfneg  47856  sharhght  47918  sigaradd  47919  altgsumbcALT  49508