Description: The base set of the normed complex vector space of complex numbers. (Contributed by NM, 7-Nov-2007) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cnnvba.6 | |
|
Assertion | cnnvba | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnnvba.6 | |
|
2 | 1 | cnnvg | |
3 | 2 | rneqi | |
4 | cnaddabloOLD | |
|
5 | ablogrpo | |
|
6 | 4 5 | ax-mp | |
7 | ax-addf | |
|
8 | 7 | fdmi | |
9 | 6 8 | grporn | |
10 | eqid | |
|
11 | eqid | |
|
12 | 10 11 | bafval | |
13 | 3 9 12 | 3eqtr4i | |