Description: Derive the absolute value of a negative complex number absneg to demonstrate the use of the properties of a normed subcomplex vector space for the complex numbers. (Contributed by AV, 9-Oct-2021) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | cnncvsabsnegdemo | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnfldnm | |
|
2 | 1 | a1i | |
3 | cnfldneg | |
|
4 | 3 | eqcomd | |
5 | 2 4 | fveq12d | |
6 | cnngp | |
|
7 | cnfldbas | |
|
8 | eqid | |
|
9 | eqid | |
|
10 | 7 8 9 | nminv | |
11 | 6 10 | mpan | |
12 | 1 | eqcomi | |
13 | 12 | fveq1i | |
14 | 13 | a1i | |
15 | 5 11 14 | 3eqtrd | |