Description: Addition of complex numbers is associative. Axiom 9 of 22 for real and complex numbers, justified by Theorem axaddass . Proofs should normally use addass instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | ax-addass | |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cA | |- A |
|
1 | cc | |- CC |
|
2 | 0 1 | wcel | |- A e. CC |
3 | cB | |- B |
|
4 | 3 1 | wcel | |- B e. CC |
5 | cC | |- C |
|
6 | 5 1 | wcel | |- C e. CC |
7 | 2 4 6 | w3a | |- ( A e. CC /\ B e. CC /\ C e. CC ) |
8 | caddc | |- + |
|
9 | 0 3 8 | co | |- ( A + B ) |
10 | 9 5 8 | co | |- ( ( A + B ) + C ) |
11 | 3 5 8 | co | |- ( B + C ) |
12 | 0 11 8 | co | |- ( A + ( B + C ) ) |
13 | 10 12 | wceq | |- ( ( A + B ) + C ) = ( A + ( B + C ) ) |
14 | 7 13 | wi | |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) ) |