Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnaddabl Structured version   Visualization version   Unicode version

 Description: The complex numbers are an Abelian group under addition. This version of cnaddablx 17506 hides the explicit structure indices i.e. is "scaffold-independent". Note that the proof also does not reference explicit structure indices. The actual structure is dependent on how and is defined. This theorem should not be referenced in any proof. For the group/ring properties of the complex numbers, see cnring 18990. (Contributed by NM, 20-Oct-2012.) (New usage is discouraged.)
Hypothesis
Ref Expression
Assertion
Ref Expression

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnex 9620 . . . 4
2 cnaddabl.g . . . . 5
32grpbase 15237 . . . 4
41, 3ax-mp 5 . . 3
5 addex 11300 . . . 4
62grpplusg 15238 . . . 4
75, 6ax-mp 5 . . 3
8 addcl 9621 . . 3
9 addass 9626 . . 3
10 0cn 9635 . . 3
11 addid2 9816 . . 3
12 negcl 9875 . . 3
13 addcom 9819 . . . . 5
1412, 13mpdan 674 . . . 4
15 negid 9921 . . . 4
1614, 15eqtr3d 2487 . . 3
174, 7, 8, 9, 10, 11, 12, 16isgrpi 16692 . 2