Description: Multiplication maps nonzero complex numbers to nonzero complex numbers. (Contributed by Steve Rodriguez, 23-Feb-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | mulnzcnopr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulf | |
|
2 | ffnov | |
|
3 | 1 2 | mpbi | |
4 | 3 | simpli | |
5 | difss | |
|
6 | xpss12 | |
|
7 | 5 5 6 | mp2an | |
8 | fnssres | |
|
9 | 4 7 8 | mp2an | |
10 | ovres | |
|
11 | eldifsn | |
|
12 | eldifsn | |
|
13 | mulcl | |
|
14 | 13 | ad2ant2r | |
15 | mulne0 | |
|
16 | 14 15 | jca | |
17 | 11 12 16 | syl2anb | |
18 | eldifsn | |
|
19 | 17 18 | sylibr | |
20 | 10 19 | eqeltrd | |
21 | 20 | rgen2 | |
22 | ffnov | |
|
23 | 9 21 22 | mpbir2an | |