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

Axiom ax-distr 7917
Description: Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by Theorem axdistr 7875. Proofs should normally use adddi 7945 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
ax-distr ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))

Detailed syntax breakdown of Axiom ax-distr
StepHypRef Expression
1 cA . . . 4 class ๐ด
2 cc 7811 . . . 4 class โ„‚
31, 2wcel 2148 . . 3 wff ๐ด โˆˆ โ„‚
4 cB . . . 4 class ๐ต
54, 2wcel 2148 . . 3 wff ๐ต โˆˆ โ„‚
6 cC . . . 4 class ๐ถ
76, 2wcel 2148 . . 3 wff ๐ถ โˆˆ โ„‚
83, 5, 7w3a 978 . 2 wff (๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚)
9 caddc 7816 . . . . 5 class +
104, 6, 9co 5877 . . . 4 class (๐ต + ๐ถ)
11 cmul 7818 . . . 4 class ยท
121, 10, 11co 5877 . . 3 class (๐ด ยท (๐ต + ๐ถ))
131, 4, 11co 5877 . . . 4 class (๐ด ยท ๐ต)
141, 6, 11co 5877 . . . 4 class (๐ด ยท ๐ถ)
1513, 14, 9co 5877 . . 3 class ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ))
1612, 15wceq 1353 . 2 wff (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ))
178, 16wi 4 1 wff ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ)))
Colors of variables: wff set class
This axiom is referenced by:  adddi  7945
  Copyright terms: Public domain W3C validator