Theorem mulneg1t 5391

Description: Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18.

Assertion

Ref	Expression
mulneg1t	|- ((A e. CC /\ B e. CC) -> (-uA x. B) = -u(A x. B))

Proof of Theorem mulneg1t

Step	Hyp	Ref	Expression
1		negeq 5299	. . . 4 |- (A = if(A e. CC, A, 0) -> -uA = -uif(A e. CC, A, 0))
2	1	opreq1d 3928	. . 3 |- (A = if(A e. CC, A, 0) -> (-uA x. B) = (-uif(A e. CC, A, 0) x. B))
3		opreq1 3921	. . . 4 |- (A = if(A e. CC, A, 0) -> (A x. B) = (if(A e. CC, A, 0) x. B))
4	3	negeqd 5301	. . 3 |- (A = if(A e. CC, A, 0) -> -u(A x. B) = -u(if(A e. CC, A, 0) x. B))
5	2, 4	eqeq12d 1467	. 2 |- (A = if(A e. CC, A, 0) -> ((-uA x. B) = -u(A x. B) <-> (-uif(A e. CC, A, 0) x. B) = -u(if(A e. CC, A, 0) x. B)))
6		opreq2 3922	. . 3 |- (B = if(B e. CC, B, 0) -> (-uif(A e. CC, A, 0) x. B) = (-uif(A e. CC, A, 0) x. if(B e. CC, B, 0)))
7		opreq2 3922	. . . 4 |- (B = if(B e. CC, B, 0) -> (if(A e. CC, A, 0) x. B) = (if(A e. CC, A, 0) x. if(B e. CC, B, 0)))
8	7	negeqd 5301	. . 3 |- (B = if(B e. CC, B, 0) -> -u(if(A e. CC, A, 0) x. B) = -u(if(A e. CC, A, 0) x. if(B e. CC, B, 0)))
9	6, 8	eqeq12d 1467	. 2 |- (B = if(B e. CC, B, 0) -> ((-uif(A e. CC, A, 0) x. B) = -u(if(A e. CC, A, 0) x. B) <-> (-uif(A e. CC, A, 0) x. if(B e. CC, B, 0)) = -u(if(A e. CC, A, 0) x. if(B e. CC, B, 0))))
10		0cn 5268	. . . 4 |- 0 e. CC
11	10	elimel 2370	. . 3 |- if(A e. CC, A, 0) e. CC
12	10	elimel 2370	. . 3 |- if(B e. CC, B, 0) e. CC
13	11, 12	mulneg1 5385	. 2 |- (-uif(A e. CC, A, 0) x. if(B e. CC, B, 0)) = -u(if(A e. CC, A, 0) x. if(B e. CC, B, 0))
14	5, 9, 13	dedth2h 2363	1 |- ((A e. CC /\ B e. CC) -> (-uA x. B) = -u(A x. B))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 1099   e. wcel 1104  ifcif 2337  (class class class)co 3916  CCcc 5172  0cc0 5174   x. cmul 5179  -ucneg 5233

This theorem is referenced by:  mulneg2t 5392  mulneg12t 5393  mulm1t 5411  divnegt 5698  zmulclt 6095  discrlem3 6556  cjreimt 6731  cjreim2t 6732  geolimilem 7138  subcost 7370  ipval2 8244  ipasslem2 8375  sinperlem2 8551

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-12 1103  ax-13 1106  ax-14 1107  ax-11 1124  ax-10o 1125  ax-10 1126  ax-17 1191  ax-16 1195  ax-11o 1203  ax-ext 1438  ax-rep 2666  ax-sep 2676  ax-nul 2683  ax-pow 2715  ax-pr 2752  ax-un 2836  ax-inf2 4565

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-3an 774  df-ex 957  df-sb 1157  df-eu 1361  df-mo 1362  df-clab 1443  df-cleq 1448  df-clel 1451  df-ne 1565  df-ral 1627  df-rex 1628  df-reu 1629  df-rab 1630  df-v 1789  df-sbc 1918  df-csb 1978  df-dif 2025  df-un 2026  df-in 2027  df-ss 2029  df-pss 2031  df-nul 2257  df-if 2338  df-pw 2378  df-sn 2388  df-pr 2389  df-tp 2391  df-op 2392  df-uni 2477  df-int 2507  df-iun 2541  df-br 2593  df-opab 2640  df-tr 2654  df-eprel 2800  df-id 2803  df-po 2810  df-so 2820  df-fr 2886  df-we 2903  df-ord 2920  df-on 2921  df-lim 2922  df-suc 2923  df-om 3101  df-xp 3153  df-rel 3154  df-cnv 3155  df-co 3156  df-dm 3157  df-rn 3158  df-res 3159  df-ima 3160  df-fun 3161  df-fn 3162  df-f 3163  df-fv 3167  df-rdg 3885  df-opr 3918  df-oprab 3919  df-1st 4031  df-2nd 4032  df-1o 4085  df-oadd 4087  df-omul 4088  df-er 4213  df-ec 4215  df-qs 4218  df-ni 4940  df-pli 4941  df-mi 4942  df-lti 4943  df-plpq 4975  df-mpq 4976  df-enq 4977  df-nq 4978  df-plq 4979  df-mq 4980  df-rq 4981  df-ltq 4982  df-1q 4983  df-np 5026  df-1p 5027  df-plp 5028  df-mp 5029  df-ltp 5030  df-plpr 5104  df-mpr 5105  df-enr 5106  df-nr 5107  df-plr 5108  df-mr 5109  df-0r 5111  df-1r 5112  df-m1r 5113  df-c 5180  df-0 5181  df-1 5182  df-i 5183  df-r 5184  df-plus 5185  df-mul 5186  df-sub 5296  df-neg 5298

Copyright terms: Public domain