Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem effoiOLD 8667

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

Hypotheses

Ref	Expression
eff1i.1
eff1i.2	[,)
eff1i.3
eff1i.4
eff1i.5

Assertion

Ref	Expression
effoiOLD

Distinct variable groups:   ,,,   ,,,   ,,   ,

---

Proof of Theorem effoiOLD

Step	Hyp	Ref	Expression
1		dffo3 3804	. 2
2		eff2 7312	. . 3
3		fveq2 3709	. . . . . . 7
4	3	eleq1d 1532	. . . . . 6
5		eff1i.3	. . . . . 6
6	4, 5	elrab2 1898	. . . . 5
7	6	pm3.26bi 322	. . . 4
8	7	ssriv 2059	. . 3
9		fssres 3628	. . 3
10	2, 8, 9	mp2an 695	. 2
11		fveq2 3709	. . . . . 6
12	11	eqeq2d 1478	. . . . 5
13	12	rcla4ev 1868	. . . 4
14		fveq2 3709	. . . . . . . 8
15	14	eleq1d 1532	. . . . . . 7
16	15, 5	elrab2 1898	. . . . . 6
17	16	biimpr 152	. . . . 5
18		axaddcl 5243	. . . . . 6
19		elrp 6220	. . . . . . . . . 10
20	19	biimpr 152	. . . . . . . . 9
21		eldifi 2152	. . . . . . . . . 10
22		absclt 6768	. . . . . . . . . 10
23	21, 22	syl 10	. . . . . . . . 9
24		absgt0t 6831	. . . . . . . . . . 11
25	24	biimpa 416	. . . . . . . . . 10
26		eldifn 2153	. . . . . . . . . . 11
27		elsn 2411	. . . . . . . . . . . 12
28	27	necon3bbii 1589	. . . . . . . . . . 11
29	26, 28	sylib 198	. . . . . . . . . 10
30	25, 21, 29	sylanc 471	. . . . . . . . 9
31	20, 23, 30	sylanc 471	. . . . . . . 8
32		reeff1o2 7369	. . . . . . . . . . 11
33		f1ocnv 3686	. . . . . . . . . . 11
34	32, 33	ax-mp 7	. . . . . . . . . 10
35		f1of 3674	. . . . . . . . . 10
36	34, 35	ax-mp 7	. . . . . . . . 9
37	36	ffvelrni 3800	. . . . . . . 8
38	31, 37	syl 10	. . . . . . 7
39	38	recnd 5287	. . . . . 6
40		eff1i.5	. . . . . . . . . . . 12
41	40	elcircOLD 8654	. . . . . . . . . . 11
42	41	biimpr 152	. . . . . . . . . 10
43		divclt 5681	. . . . . . . . . . 11
44	23	recnd 5287	. . . . . . . . . . 11
45		gt0ne0t 5592	. . . . . . . . . . . 12
46	45, 23, 30	sylanc 471	. . . . . . . . . . 11
47	43, 21, 44, 46	syl3anc 856	. . . . . . . . . 10
48		absdivt 6795	. . . . . . . . . . . 12
49	48, 21, 44, 46	syl3anc 856	. . . . . . . . . . 11
50		absidmt 6830	. . . . . . . . . . . . 13
51	50	opreq2d 3961	. . . . . . . . . . . 12
52	21, 51	syl 10	. . . . . . . . . . 11
53		dividt 5722	. . . . . . . . . . . 12
54	53, 44, 46	sylanc 471	. . . . . . . . . . 11