Description: Existence of reciprocal of nonzero complex number. (Contributed by Eric Schmidt, 22-May-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | recex | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnre | |
|
2 | recextlem2 | |
|
3 | 2 | 3expia | |
4 | remulcl | |
|
5 | 4 | anidms | |
6 | remulcl | |
|
7 | 6 | anidms | |
8 | readdcl | |
|
9 | 5 7 8 | syl2an | |
10 | ax-rrecex | |
|
11 | 9 10 | sylan | |
12 | recn | |
|
13 | recn | |
|
14 | recn | |
|
15 | ax-icn | |
|
16 | mulcl | |
|
17 | 15 16 | mpan | |
18 | subcl | |
|
19 | 17 18 | sylan2 | |
20 | mulcl | |
|
21 | 19 20 | sylan | |
22 | addcl | |
|
23 | 17 22 | sylan2 | |
24 | 23 | adantr | |
25 | 19 | adantr | |
26 | simpr | |
|
27 | 24 25 26 | mulassd | |
28 | recextlem1 | |
|
29 | 28 | adantr | |
30 | 29 | oveq1d | |
31 | 27 30 | eqtr3d | |
32 | id | |
|
33 | 31 32 | sylan9eq | |
34 | oveq2 | |
|
35 | 34 | eqeq1d | |
36 | 35 | rspcev | |
37 | 21 33 36 | syl2an2r | |
38 | 37 | exp31 | |
39 | 14 38 | syl5 | |
40 | 39 | rexlimdv | |
41 | 12 13 40 | syl2an | |
42 | 41 | adantr | |
43 | 11 42 | mpd | |
44 | 43 | ex | |
45 | 3 44 | syld | |
46 | 45 | adantr | |
47 | neeq1 | |
|
48 | 47 | adantl | |
49 | oveq1 | |
|
50 | 49 | eqeq1d | |
51 | 50 | rexbidv | |
52 | 51 | adantl | |
53 | 46 48 52 | 3imtr4d | |
54 | 53 | ex | |
55 | 54 | rexlimivv | |
56 | 1 55 | syl | |
57 | 56 | imp | |