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 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cA ⊢ 𝐴
1
cc ⊢ ℂ
2
0 1
wcel ⊢ 𝐴 ∈ ℂ
3
cB ⊢ 𝐵
4
3 1
wcel ⊢ 𝐵 ∈ ℂ
5
cC ⊢ 𝐶
6
5 1
wcel ⊢ 𝐶 ∈ ℂ
7
2 4 6
w3a ⊢ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ )
8
cmul ⊢ ·
9
caddc ⊢ +
10
3 5 9
co ⊢ ( 𝐵 + 𝐶 )
11
0 10 8
co ⊢ ( 𝐴 · ( 𝐵 + 𝐶 ) )
12
0 3 8
co ⊢ ( 𝐴 · 𝐵 )
13
0 5 8
co ⊢ ( 𝐴 · 𝐶 )
14
12 13 9
co ⊢ ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) )
15
11 14
wceq ⊢ ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) )
16
7 15
wi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) )