Description: Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | cnfld0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 00id | |
|
2 | cnring | |
|
3 | ringgrp | |
|
4 | 2 3 | ax-mp | |
5 | 0cn | |
|
6 | cnfldbas | |
|
7 | cnfldadd | |
|
8 | eqid | |
|
9 | 6 7 8 | grpid | |
10 | 4 5 9 | mp2an | |
11 | 1 10 | mpbi | |
12 | 11 | eqcomi | |