Theorem eff1i 8744

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, one-to-one to 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
eff1i	|- (exp |` S):S-1-1->(CC \ {0})

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

Proof of Theorem eff1i

Step	Hyp	Ref	Expression
1		f1fv 3874	. 2 |- ((exp |` S):S-1-1->(CC \ {0}) <-> ((exp |` S):S-->(CC \ {0}) /\ A.x e. S A.y e. S (((exp |` S)` x) = ((exp |` S)` y) -> x = y)))
2		eff2 7370	. . 3 |- exp:CC-->(CC \ {0})
3		fveq2 3724	. . . . . . 7 |- (v = x -> (Im` v) = (Im` x))
4	3	eleq1d 1540	. . . . . 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 1907	. . . . 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 2069	. . 3 |- S (_ CC
9		fssres 3643	. . 3 |- ((exp:CC-->(CC \ {0}) /\ S (_ CC) -> (exp |` S):S-->(CC \ {0}))
10	2, 8, 9	mp2an 697	. 2 |- (exp |` S):S-->(CC \ {0})
11		fvres 3734	. . . . 5 |- (x e. S -> ((exp |` S)` x) = (exp` x))
12		fvres 3734	. . . . 5 |- (y e. S -> ((exp |` S)` y) = (exp` y))
13	11, 12	eqeqan12d 1490	. . . 4 |- ((x e. S /\ y e. S) -> (((exp |` S)` x) = ((exp |` S)` y) <-> (exp` x) = (exp` y)))
14		abseft 7483	. . . . . . . . . . 11 |- (x e. CC -> (abs` (exp` x)) = (exp` (Re` x)))
15		abseft 7483	. . . . . . . . . . 11 |- (y e. CC -> (abs` (exp` y)) = (exp` (Re` y)))
16	14, 15	eqeqan12d 1490	. . . . . . . . . 10 |- ((x e. CC /\ y e. CC) -> ((abs` (exp` x)) = (abs` (exp` y)) <-> (exp` (Re` x)) = (exp` (Re` y))))
17		fvres 3734	. . . . . . . . . . . . 13 |- ((Re` x) e. RR -> ((exp |` RR)` (Re` x)) = (exp` (Re` x)))
18		fvres 3734	. . . . . . . . . . . . 13 |- ((Re` y) e. RR -> ((exp |` RR)` (Re` y)) = (exp` (Re` y)))
19	17, 18	eqeqan12d 1490	. . . . . . . . . . . 12 |- (((Re` x) e. RR /\ (Re` y) e. RR) -> (((exp |` RR)` (Re` x)) = ((exp |` RR)` (Re` y)) <-> (exp` (Re` x)) = (exp` (Re` y))))
20		reeff1 7410	. . . . . . . . . . . . 13 |- (exp |` RR):RR-1-1->(0(,) +oo)
21		f1fveq 3876	. . . . . . . . . . . . 13 |- (((exp |` RR):RR-1-1->(0(,) +oo) /\ ((Re` x) e. RR /\ (Re` y) e. RR)) -> (((exp |` RR)` (Re` x)) = ((exp |` RR)` (Re` y)) <-> (Re` x) = (Re` y)))
22	20, 21	mpan 695	. . . . . . . . . . . 12 |- (((Re` x) e. RR /\ (Re` y) e. RR) -> (((exp |` RR)` (Re` x)) = ((exp |` RR)` (Re` y)) <-> (Re` x) = (Re` y)))
23	19, 22	bitr3d 530	. . . . . . . . . . 11 |- (((Re` x) e. RR /\ (Re` y) e. RR) -> ((exp` (Re` x)) = (exp` (Re` y)) <-> (Re` x) = (Re` y)))
24		reclt 6757	. . . . . . . . . . 11 |- (x e. CC -> (Re` x) e. RR)
25		reclt 6757	. . . . . . . . . . 11 |- (y e. CC -> (Re` y) e. RR)
26	23, 24, 25	syl2an 454	. . . . . . . . . 10 |- ((x e. CC /\ y e. CC) -> ((exp` (Re` x)) = (exp` (Re` y)) <-> (Re` x) = (Re` y)))
27	16, 26	bitrd 528	. . . . . . . . 9 |- ((x e. CC /\ y e. CC) -> ((abs` (exp` x)) = (abs` (exp` y)) <-> (Re` x) = (Re` y)))
28		fveq2 3724	. . . . . . . . 9 |- ((exp` x) = (exp` y) -> (abs` (exp` x)) = (abs` (exp` y)))
29	27, 28	syl5bi 208	. . . . . . . 8 |- ((x e. CC /\ y e. CC) -> ((exp` x) = (exp` y) -> (Re` x) = (Re` y)))
30		fveq2 3724	. . . . . . . . . . 11 |- (v = y -> (Im` v) = (Im` y))
31	30	eleq1d 1540	. . . . . . . . . 10 |- (v = y -> ((Im` v) e. D <-> (Im` y) e. D))
32	31, 5	elrab2 1907	. . . . . . . . 9 |- (y e. S <-> (y e. CC /\ (Im` y) e. D))
33	32	pm3.26bi 322	. . . . . . . 8 |- (y e. S -> y e. CC)
34	29, 7, 33	syl2an 454	. . . . . . 7 |- ((x e. S /\ y e. S) -> ((exp` x) = (exp` y) -> (Re` x) = (Re` y)))
35	34	imp 350	. . . . . 6 |- (((x e. S /\ y e. S) /\ (exp` x) = (exp` y)) -> (Re` x) = (Re` y))
36		eff1lem 8743	. . . . . . . . . . . . 13 |- (x e. CC -> (exp` x) = ((abs` (exp` x)) x. (exp` (i x. (Im` x)))))
37		eff1lem 8743	. . . . . . . . . . . . 13 |- (y e. CC -> (exp` y) = ((abs` (exp` y)) x. (exp` (i x. (Im` y)))))
38	36, 37	eqeqan12d 1490	. . . . . . . . . . . 12 |- ((x e. CC /\ y e. CC) -> ((exp` x) = (exp` y) <-> ((abs` (exp` x)) x. (exp` (i x. (Im` x)))) = ((abs` (exp` y)) x. (exp` (i x. (Im` y))))))
39	38	biimpa 416	. . . . . . . . . . 11 |- (((x e. CC /\ y e. CC) /\ (exp` x) = (exp` y)) -> ((abs` (exp` x)) x. (exp` (i x. (Im` x)))) = ((abs` (exp` y)) x. (exp` (i x. (Im` y)))))
40	28	opreq1d 3975	. . . . . . . . . . . . . 14 |- ((exp` x) = (exp` y) -> ((abs` (exp` x)) x. (exp` (i x. (Im` y)))) = ((abs` (exp` y)) x. (exp` (i x. (Im` y)))))
41	40	adantl 388	. . . . . . . . . . . . 13 |- (((x e. CC /\ y e. CC) /\ (exp` x) = (exp` y)) -> ((abs` (exp` x)) x. (exp` (i x. (Im` y)))) = ((abs` (exp` y)) x. (exp` (i x. (Im` y)))))
42	41	eqeq2d 1486	. . . . . . . . . . . 12 |- (((x e. CC /\ y e. CC) /\ (exp` x) = (exp` y)) -> (((abs` (exp` x)) x. (exp` (i x. (Im` x)))) = ((abs` (exp` x)) x. (exp` (i x. (Im` y)))) <-> ((abs` (exp` x)) x. (exp` (i x. (Im` x)))) = ((abs` (exp` y)) x. (exp` (i x. (Im` y))))))
43		mulcantOLD 5691	. . . . . . . . . . . . . 14 |- ((((abs` (exp` x)) e. CC /\ (exp` (i x. (Im` x))) e. CC /\ (exp` (i x. (Im` y))) e. CC) /\ (abs` (exp` x)) =/= 0) -> (((abs` (exp` x)) x. (exp` (i x. (Im` x)))) = ((abs` (exp` x)) x. (exp` (i x. (Im` y)))) <-> (exp` (i x. (Im` x))) = (exp` (i x. (Im` y)))))
44		efclt 7312	. . . . . . . . . . . . . . . . . 18 |- (x e. CC -> (exp` x) e. CC)
45		absclt 6833	. . . . . . . . . . . . . . . . . . 19 |- ((exp` x) e. CC -> (abs` (exp` x)) e. RR)
46	45	recnd 5315	. . . . . . . . . . . . . . . . . 18 |- ((exp` x) e. CC -> (abs` (exp` x)) e. CC)
47	44, 46	syl 10	. . . . . . . . . . . . . . . . 17 |- (x e. CC -> (abs` (exp` x)) e. CC)
48		imclt 6758	. . . . . . . . . . . . . . . . . . 19 |- (x e. CC -> (Im` x) e. RR)
49	48	recnd 5315	. . . . . . . . . . . . . . . . . 18 |- (x e. CC -> (Im` x) e. CC)
50		axicn 5270	. . . . . . . . . . . . . . . . . . 19 |- i e. CC
51		axmulcl 5273	. . . . . . . . . . . . . . . . . . 19 |- ((i e. CC /\ (Im` x) e. CC) -> (i x. (Im` x)) e. CC)
52	50, 51	mpan 695	. . . . . . . . . . . . . . . . . 18 |- ((Im` x) e. CC -> (i x. (Im` x)) e.