Theorem effoi 8700

Description: The exponential function maps the set S, of complex numbers with imaginary part in a closed-below, open-above real interval of length 2 x. pi starting at A, onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.)

Hypotheses

Ref	Expression
eff1i.1	|- A e. RR
eff1i.2	|- D = (A[,)(A + (2 x. pi)))
eff1i.3	|- S = {v e. CC | (Im` v) e. D}
eff1i.4	|- F = {<.z, w>. | (z e. D /\ w = (exp` (i x. z)))}
eff1i.5	|- C = {v e. CC | (abs` v) = 1}

Assertion

Ref	Expression
effoi	|- (exp |` S):S-onto->(CC \ {0})

Distinct variable groups:   v,A,w,z   v,D,w,z   w,C,z   v,F

Proof of Theorem effoi

Step	Hyp	Ref	Expression
1		dffo3 3814	. 2 |- ((exp |` S):S-onto->(CC \ {0}) <-> ((exp |` S):S-->(CC \ {0}) /\ A.y e. (CC \ {0})E.x e. S y = ((exp |` S)` x)))
2		eff2 7329	. . 3 |- exp:CC-->(CC \ {0})
3		fveq2 3719	. . . . . . 7 |- (v = x -> (Im` v) = (Im` x))
4	3	eleq1d 1538	. . . . . 6 |- (v = x -> ((Im` v) e. D <-> (Im` x) e. D))
5		eff1i.3	. . . . . 6 |- S = {v e. CC | (Im` v) e. D}
6	4, 5	elrab2 1904	. . . . 5 |- (x e. S <-> (x e. CC /\ (Im` x) e. D))
7	6	pm3.26bi 322	. . . 4 |- (x e. S -> x e. CC)
8	7	ssriv 2066	. . 3 |- S (_ CC
9		fssres 3638	. . 3 |- ((exp:CC-->(CC \ {0}) /\ S (_ CC) -> (exp |` S):S-->(CC \ {0}))
10	2, 8, 9	mp2an 696	. 2 |- (exp |` S):S-->(CC \ {0})
11		fveq2 3719	. . . . . 6 |- (x = ((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y))))) -> ((exp |` S)` x) = ((exp |` S)` ((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y)))))))
12	11	eqeq2d 1484	. . . . 5 |- (x = ((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y))))) -> (y = ((exp |` S)` x) <-> y = ((exp |` S)` ((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y))))))))
13	12	rcla4ev 1874	. . . 4 |- ((((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y))))) e. S /\ y = ((exp |` S)` ((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y))))))) -> E.x e. S y = ((exp |` S)` x))
14		fveq2 3719	. . . . . . . 8 |- (v = ((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y))))) -> (Im` v) = (Im` ((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y)))))))
15	14	eleq1d 1538	. . . . . . 7 |- (v = ((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y))))) -> ((Im` v) e. D <-> (Im` ((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y)))))) e. D))
16	15, 5	elrab2 1904	. . . . . 6 |- (((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y))))) e. S <-> (((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y))))) e. CC /\ (Im` ((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y)))))) e. D))
17	16	biimpr 152	. . . . 5 |- ((((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y))))) e. CC /\ (Im` ((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y)))))) e. D) -> ((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y))))) e. S)
18		axaddcl 5254	. . . . . 6 |- (((`'(exp |` RR)` (abs` y)) e. CC /\ (i x. (`'F` (y / (abs` y)))) e. CC) -> ((`'(exp |` RR)` (abs` y)) + (i x. (`'F` (y / (abs` y))))) e. CC)
19		elrp 6232	. . . . . . . . . 10 |- ((abs` y) e. RR+ <-> ((abs` y) e. RR /\ 0 < (abs` y)))
20	19	biimpr 152	. . . . . . . . 9 |- (((abs` y) e. RR /\ 0 < (abs` y)) -> (abs` y) e. RR+)
21		eldifi 2159	. . . . . . . . . 10 |- (y e. (CC \ {0}) -> y e. CC)
22		absclt 6783	. . . . . . . . . 10 |- (y e. CC -> (abs` y) e. RR)
23	21, 22	syl 10	. . . . . . . . 9 |- (y e. (CC \ {0}) -> (abs` y) e. RR)
24		eldifsn 2459	. . . . . . . . . 10 |- (y e. (CC \ {0}) <-> (y e. CC /\ y =/= 0))
25		absgt0t 6846	. . . . . . . . . . 11 |- (y e. CC -> (y =/= 0 <-> 0 < (abs` y)))
26	25	biimpa 416	. . . . . . . . . 10 |- ((y e. CC /\ y =/= 0) -> 0 < (abs` y))
27	24, 26	sylbi 199	. . . . . . . . 9 |- (y e. (CC \ {0}) -> 0 < (abs` y))
28	20, 23, 27	sylanc 471	. . . . . . . 8 |- (y e. (CC \ {0}) -> (abs` y) e. RR+)
29		reeff1o2 7386	. . . . . . . . . . 11 |- (exp |` RR):RR-1-1-onto->RR+
30		f1ocnv 3696	. . . . . . . . . . 11 |- ((exp |` RR):RR-1-1-onto->RR+ -> `'(exp |` RR):RR+-1-1-onto->RR)
31	29, 30	ax-mp 7	. . . . . . . . . 10 |- `'(exp |` RR):RR+-1-1-onto->RR
32		f1of 3684	. . . . . . . . . 10 |- (`'(exp |` RR):RR+-1-1-onto->RR -> `'(exp |` RR):RR+-->RR)
33	31, 32	ax-mp 7	. . . . . . . . 9 |- `'(exp |` RR):RR+-->RR
34	33	ffvelrni 3810	. . . . . . . 8 |- ((abs` y) e. RR+ -> (`'(exp |` RR)` (abs` y)) e. RR)
35	28, 34	syl 10	. . . . . . 7 |- (y e. (CC \ {0}) -> (`'(exp |` RR)` (abs` y)) e. RR)
36	35	recnd 5298	. . . . . 6 |- (y e. (CC \ {0}) -> (`'(exp |` RR)` (abs` y)) e. CC)
37		fveq2 3719	. . . . . . . . . . . . 13 |- (v = (y / (abs` y)) -> (abs` v) = (abs` (y / (abs` y))))
38	37	eqeq1d 1481	. . . . . . . . . . . 12 |- (v = (y / (abs` y)) -> ((abs` v) = 1 <-> (abs` (y / (abs` y))) = 1))
39		eff1i.5	. . . . . . . . . . . 12 |- C = {v e. CC | (abs` v) = 1}
40	38, 39	elrab2 1904	. . . . . . . . . . 11 |- ((y / (abs` y)) e. C <-> ((y / (abs` y)) e. CC /\ (abs` (y / (abs` y))) = 1))
41	40	biimpr 152	. . . . . . . . . 10 |- (((y / (abs` y)) e. CC /\ (abs` (y / (abs` y))) = 1) -> (y / (abs` y)) e. C)
42		divclt 5691	. . . . . . . . . . 11 |- ((y e. CC /\ (abs` y) e. CC /\ (abs` y) =/= 0) -> (y / (abs` y)) e. CC)
43	23	recnd 5298	. . . . . . . . . . 11 |- (y e. (CC \ {0}) -> (abs` y) e. CC)
44		gt0ne0t 5602	. . . . . . . . . . . 12 |- (((abs` y) e. RR /\ 0 < (abs` y)) -> (abs` y) =/= 0)
45	44, 23, 27	sylanc 471	. . . . . . . . . . 11 |- (y e. (CC \ {0}) -> (abs` y) =/= 0)
46	42, 21, 43, 45	syl3anc 857	. . . . . . . . . 10 |- (y e. (CC \ {0}) -> (y / (abs` y)) e. CC)
47		absdivt 6810	. . . . . . . . . . . 12 |- ((y e. CC /\ (abs` y) e. CC /\ (abs` y) =/= 0) -> (abs` (y / (abs` y))) = ((abs` y) / (abs` (abs` y))))
48	47, 21, 43, 45	syl3anc 857	. . . . . . . . . . 11 |- (y e. (CC \ {0}) -> (abs` (y / (abs` y))) = ((abs` y) / (abs` (abs` y))))
49		absidmt 6845	. . . . . . . . . . . . 13 |- (y e. CC -> (abs` (abs` y)) = (abs` y))
50	49	opreq2d 3971	. . . . . . . . . . . 12 |- (y e. CC -> ((abs` y) / (abs` (abs` y))) = ((abs` y) / (abs` y)))
51	21, 50	syl 10	. . . . . . . . . . 11 |- (y e. (CC \ {0}) -> ((abs` y) / (abs` (abs` y))) = ((abs` y) / (abs` y)))
52		dividt 5732	. . . . . . . . . . . 12 |- (((abs` y) e. CC /\ (abs` y