ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulneg2 GIF version

Theorem mulneg2 8348
Description: The product with a negative is the negative of the product. (Contributed by NM, 30-Jul-2004.)
Assertion
Ref Expression
mulneg2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (๐ด ยท -๐ต) = -(๐ด ยท ๐ต))

Proof of Theorem mulneg2
StepHypRef Expression
1 mulneg1 8347 . . 3 ((๐ต โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚) โ†’ (-๐ต ยท ๐ด) = -(๐ต ยท ๐ด))
21ancoms 268 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (-๐ต ยท ๐ด) = -(๐ต ยท ๐ด))
3 negcl 8152 . . 3 (๐ต โˆˆ โ„‚ โ†’ -๐ต โˆˆ โ„‚)
4 mulcom 7936 . . 3 ((๐ด โˆˆ โ„‚ โˆง -๐ต โˆˆ โ„‚) โ†’ (๐ด ยท -๐ต) = (-๐ต ยท ๐ด))
53, 4sylan2 286 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (๐ด ยท -๐ต) = (-๐ต ยท ๐ด))
6 mulcom 7936 . . 3 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (๐ด ยท ๐ต) = (๐ต ยท ๐ด))
76negeqd 8147 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ -(๐ด ยท ๐ต) = -(๐ต ยท ๐ด))
82, 5, 73eqtr4d 2220 1 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (๐ด ยท -๐ต) = -(๐ด ยท ๐ต))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   = wceq 1353   โˆˆ wcel 2148  (class class class)co 5871  โ„‚cc 7805   ยท cmul 7812  -cneg 8124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4120  ax-pow 4173  ax-pr 4208  ax-setind 4535  ax-resscn 7899  ax-1cn 7900  ax-icn 7902  ax-addcl 7903  ax-addrcl 7904  ax-mulcl 7905  ax-addcom 7907  ax-mulcom 7908  ax-addass 7909  ax-distr 7911  ax-i2m1 7912  ax-0id 7915  ax-rnegex 7916  ax-cnre 7918
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4003  df-opab 4064  df-id 4292  df-xp 4631  df-rel 4632  df-cnv 4633  df-co 4634  df-dm 4635  df-iota 5176  df-fun 5216  df-fv 5222  df-riota 5827  df-ov 5874  df-oprab 5875  df-mpo 5876  df-sub 8125  df-neg 8126
This theorem is referenced by:  mulneg12  8349  submul2  8351  mulsub  8353  mulneg2i  8357  mulneg2d  8364  zmulcl  9301  binom2sub  10627  cjreb  10867  recj  10868  reneg  10869  imcj  10876  imneg  10877  ipcnval  10887  cjneg  10891  efexp  11682  efmival  11733  sinsub  11740  cossub  11741  odd2np1  11869  sinperlem  14091  efimpi  14102
  Copyright terms: Public domain W3C validator