Metamath Proof Explorer


Theorem recex

Description: Existence of reciprocal of nonzero complex number. (Contributed by Eric Schmidt, 22-May-2007)

Ref Expression
Assertion recex AA0xAx=1

Proof

Step Hyp Ref Expression
1 cnre AabA=a+ib
2 recextlem2 aba+ib0aa+bb0
3 2 3expia aba+ib0aa+bb0
4 remulcl aaaa
5 4 anidms aaa
6 remulcl bbbb
7 6 anidms bbb
8 readdcl aabbaa+bb
9 5 7 8 syl2an abaa+bb
10 ax-rrecex aa+bbaa+bb0yaa+bby=1
11 9 10 sylan abaa+bb0yaa+bby=1
12 recn aa
13 recn bb
14 recn yy
15 ax-icn i
16 mulcl ibib
17 15 16 mpan bib
18 subcl aibaib
19 17 18 sylan2 abaib
20 mulcl aibyaiby
21 19 20 sylan abyaiby
22 addcl aiba+ib
23 17 22 sylan2 aba+ib
24 23 adantr abya+ib
25 19 adantr abyaib
26 simpr abyy
27 24 25 26 mulassd abya+ibaiby=a+ibaiby
28 recextlem1 aba+ibaib=aa+bb
29 28 adantr abya+ibaib=aa+bb
30 29 oveq1d abya+ibaiby=aa+bby
31 27 30 eqtr3d abya+ibaiby=aa+bby
32 id aa+bby=1aa+bby=1
33 31 32 sylan9eq abyaa+bby=1a+ibaiby=1
34 oveq2 x=aibya+ibx=a+ibaiby
35 34 eqeq1d x=aibya+ibx=1a+ibaiby=1
36 35 rspcev aibya+ibaiby=1xa+ibx=1
37 21 33 36 syl2an2r abyaa+bby=1xa+ibx=1
38 37 exp31 abyaa+bby=1xa+ibx=1
39 14 38 syl5 abyaa+bby=1xa+ibx=1
40 39 rexlimdv abyaa+bby=1xa+ibx=1
41 12 13 40 syl2an abyaa+bby=1xa+ibx=1
42 41 adantr abaa+bb0yaa+bby=1xa+ibx=1
43 11 42 mpd abaa+bb0xa+ibx=1
44 43 ex abaa+bb0xa+ibx=1
45 3 44 syld aba+ib0xa+ibx=1
46 45 adantr abA=a+iba+ib0xa+ibx=1
47 neeq1 A=a+ibA0a+ib0
48 47 adantl abA=a+ibA0a+ib0
49 oveq1 A=a+ibAx=a+ibx
50 49 eqeq1d A=a+ibAx=1a+ibx=1
51 50 rexbidv A=a+ibxAx=1xa+ibx=1
52 51 adantl abA=a+ibxAx=1xa+ibx=1
53 46 48 52 3imtr4d abA=a+ibA0xAx=1
54 53 ex abA=a+ibA0xAx=1
55 54 rexlimivv abA=a+ibA0xAx=1
56 1 55 syl AA0xAx=1
57 56 imp AA0xAx=1