This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Construction and axiomatization of real and complex numbers Real and complex number postulates restated as axioms ax-distr
Description: Distributive law for complex numbers (left-distributivity). Axiom 11 of
22 for real and complex numbers, justified by Theorem axdistr . Proofs
should normally use adddi instead. (New usage is discouraged.)
(Contributed by NM , 22-Nov-1994)
Ref
Expression
Assertion
ax-distr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A B + C = A B + A C
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cA class A
1
cc class ℂ
2
0 1
wcel wff A ∈ ℂ
3
cB class B
4
3 1
wcel wff B ∈ ℂ
5
cC class C
6
5 1
wcel wff C ∈ ℂ
7
2 4 6
w3a wff A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ
8
cmul class ×
9
caddc class +
10
3 5 9
co class B + C
11
0 10 8
co class A B + C
12
0 3 8
co class A B
13
0 5 8
co class A C
14
12 13 9
co class A B + A C
15
11 14
wceq wff A B + C = A B + A C
16
7 15
wi wff A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A B + C = A B + A C