Description: The group identity element of nonzero complex number multiplication is one. (Contributed by Steve Rodriguez, 23-Feb-2007) (Revised by AV, 26-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cnmgpabl.m | |
|
Assertion | cnmgpid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnmgpabl.m | |
|
2 | cnring | |
|
3 | difss | |
|
4 | ax-1cn | |
|
5 | ax-1ne0 | |
|
6 | eldifsn | |
|
7 | 4 5 6 | mpbir2an | |
8 | cnfldbas | |
|
9 | cnfld1 | |
|
10 | 1 8 9 | ringidss | |
11 | 10 | eqcomd | |
12 | 2 3 7 11 | mp3an | |