Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eff1olem Unicode version

Theorem eff1olem 19910
 Description: The exponential function maps the set , of complex numbers with imaginary part in a real interval of length , one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.) (Proof shortened by Mario Carneiro, 13-May-2014.)
Hypotheses
Ref Expression
eff1olem.1
eff1olem.2
eff1olem.3
eff1olem.4
eff1olem.5
Assertion
Ref Expression
eff1olem
Distinct variable groups:   ,,,,   ,,,   ,,,,   ,,
Allowed substitution hints:   (,)   ()

Proof of Theorem eff1olem
StepHypRef Expression
1 cnvimass 5033 . . . 4
2 eff1olem.2 . . . 4
3 imf 11598 . . . . . 6
43fdmi 5394 . . . . 5
54eqcomi 2287 . . . 4
61, 2, 53sstr4i 3217 . . 3
7 eff2 12379 . . . . . . 7
87a1i 10 . . . . . 6
98feqmptd 5575 . . . . 5
109reseq1d 4954 . . . 4
11 resmpt 5000 . . . 4
1210, 11eqtrd 2315 . . 3
136, 12ax-mp 8 . 2
146sseli 3176 . . . 4
157ffvelrni 5664 . . . 4
1614, 15syl 15 . . 3
18 simpr 447 . . . . . . . . . 10
19 eldifsn 3749 . . . . . . . . . 10
2018, 19sylib 188 . . . . . . . . 9
2120simpld 445 . . . . . . . 8
2220simprd 449 . . . . . . . 8
2321, 22absrpcld 11930 . . . . . . 7
24 reeff1o 19823 . . . . . . . . 9
25 f1ocnv 5485 . . . . . . . . 9
26 f1of 5472 . . . . . . . . 9
2724, 25, 26mp2b 9 . . . . . . . 8
2827ffvelrni 5664 . . . . . . 7
2923, 28syl 15 . . . . . 6
3029recnd 8861 . . . . 5
31 ax-icn 8796 . . . . . 6
32 eff1olem.3 . . . . . . . . 9
3332adantr 451 . . . . . . . 8
34 eff1olem.1 . . . . . . . . . . . 12
35 eqid 2283 . . . . . . . . . . . 12
36 eff1olem.4 . . . . . . . . . . . 12
37 eff1olem.5 . . . . . . . . . . . 12
38 eqid 2283 . . . . . . . . . . . 12
3934, 35, 32, 36, 37, 38efif1olem4 19907 . . . . . . . . . . 11
40 f1ocnv 5485 . . . . . . . . . . 11
41 f1of 5472 . . . . . . . . . . 11
4239, 40, 413syl 18 . . . . . . . . . 10
4342adantr 451 . . . . . . . . 9
4421abscld 11918 . . . . . . . . . . . 12
4544recnd 8861 . . . . . . . . . . 11
4621, 22absne0d 11929 . . . . . . . . . . 11
4721, 45, 46divcld 9536 . . . . . . . . . 10
4821, 45, 46absdivd 11937 . . . . . . . . . . 11
49 absidm 11807 . . . . . . . . . . . . 13
5021, 49syl 15 . . . . . . . . . . . 12
5150oveq2d 5874 . . . . . . . . . . 11
5245, 46dividd 9534 . . . . . . . . . . 11
5348, 51, 523eqtrd 2319 . . . . . . . . . 10
54 absf 11821 . . . . . . . . . . 11
55 ffn 5389 . . . . . . . . . . 11
56 fniniseg 5646 . . . . . . . . . . 11
5754, 55, 56mp2b 9 . . . . . . . . . 10
5847, 53, 57sylanbrc 645 . . . . . . . . 9
59 ffvelrn 5663 . . . . . . . . 9
6043, 58, 59syl2anc 642 . . . . . . . 8
6133, 60sseldd 3181 . . . . . . 7
6261recnd 8861 . . . . . 6
63 mulcl 8821 . . . . . 6
6431, 62, 63sylancr 644 . . . . 5
6530, 64addcld 8854 . . . 4
6629, 61crimd 11717 . . . . 5
6766, 60eqeltrd 2357 . . . 4
68 ffn 5389 . . . . 5
69 elpreima 5645 . . . . 5
703, 68, 69mp2b 9 . . . 4
7165, 67, 70sylanbrc 645 . . 3
7271, 2syl6eleqr 2374 . 2
73 efadd 12375 . . . . . . 7
7430, 64, 73syl2anc 642 . . . . . 6
75 fvres 5542 . . . . . . . . 9
7629, 75syl 15 . . . . . . . 8
77 f1ocnvfv2 5793 . . . . . . . . 9
7824, 23, 77sylancr 644 . . . . . . . 8
7976, 78eqtr3d 2317 . . . . . . 7
80 oveq2 5866 . . . . . . . . . . 11
8180fveq2d 5529 . . . . . . . . . 10
82 oveq2 5866 . . . . . . . . . . . . 13
8382fveq2d 5529 . . . . . . . . . . . 12
8483cbvmptv 4111 . . . . . . . . . . 11
8534, 84eqtri 2303 . . . . . . . . . 10
86 fvex 5539 . . . . . . . . . 10
8781, 85, 86fvmpt 5602 . . . . . . . . 9
8860, 87syl 15 . . . . . . . 8
8939adantr 451 . . . . . . . . 9
90 f1ocnvfv2 5793 . . . . . . . . 9
9189, 58, 90syl2anc 642 . . . . . . . 8
9288, 91eqtr3d 2317 . . . . . . 7
9379, 92oveq12d 5876 . . . . . 6
9421, 45, 46divcan2d 9538 . . . . . 6
9574, 93, 943eqtrrd 2320 . . . . 5
9695adantrl 696 . . . 4
97 fveq2 5525 . . . . 5
9897eqeq2d 2294 . . . 4
9996, 98syl5ibrcom 213 . . 3
10014adantl 452 . . . . . . 7
101100replimd 11682 . . . . . 6
102 absef 12477 . . . . . . . . . . 11
103100, 102syl 15 . . . . . . . . . 10
104100recld 11679 . . . . . . . . . . 11
105 fvres 5542 . . . . . . . . . . 11
106104, 105syl 15 . . . . . . . . . 10
107103, 106eqtr4d 2318 . . . . . . . . 9
108107fveq2d 5529 . . . . . . . 8
109 f1ocnvfv1 5792 . . . . . . . . 9
11024, 104, 109sylancr 644 . . . . . . . 8
111108, 110eqtrd 2315 . . . . . . 7
112100imcld 11680 . . . . . . . . . . . . . . 15
113112recnd 8861 . . . . . . . . . . . . . 14
114 mulcl 8821 . . . . . . . . . . . . . 14
11531, 113, 114sylancr 644 . . . . . . . . . . . . 13
116 efcl 12364 . . . . . . . . . . . . 13
117115, 116syl 15 . . . . . . . . . . . 12
118104recnd 8861 . . . . . . . . . . . . 13
119 efcl 12364 . . . . . . . . . . . . 13
120118, 119syl 15 . . . . . . . . . . . 12
121 efne0 12377 . . . . . . . . . . . . 13
122118, 121syl 15 . . . . . . . . . . . 12
123117, 120, 122divcan3d 9541 . . . . . . . . . . 11
124101fveq2d 5529 . . . . . . . . . . . . 13
125 efadd 12375 . . . . . . . . . . . . . 14
126118, 115, 125syl2anc 642 . . . . . . . . . . . . 13
127124, 126eqtrd 2315 . . . . . . . . . . . 12
128127, 103oveq12d 5876 . . . . . . . . . . 11
129 elpreima 5645 . . . . . . . . . . . . . . . 16
1303, 68, 129mp2b 9 . . . . . . . . . . . . . . 15
131130simprbi 450 . . . . . . . . . . . . . 14
132131, 2eleq2s 2375 . . . . . . . . . . . . 13
133132adantl 452 . . . . . . . . . . . 12
134 oveq2 5866 . . . . . . . . . . . . . 14
135134fveq2d 5529 . . . . . . . . . . . . 13
136 fvex 5539 . . . . . . . . . . . . 13
137135, 34, 136fvmpt 5602 . . . . . . . . . . . 12
138133, 137syl 15 . . . . . . . . . . 11
139123, 128, 1383eqtr4d 2325 . . . . . . . . . 10
140139fveq2d 5529 . . . . . . . . 9
141 f1ocnvfv1 5792 . . . . . . . . . 10
14239, 132, 141syl2an 463 . . . . . . . . 9
143140, 142eqtrd 2315 . . . . . . . 8
144143oveq2d 5874 . . . . . . 7
145111, 144oveq12d 5876 . . . . . 6
146101, 145eqtr4d 2318 . . . . 5
147 fveq2 5525 . . . . . . . 8
148147fveq2d 5529 . . . . . . 7
149 id 19 . . . . . . . . . 10
150149, 147oveq12d 5876 . . . . . . . . 9
151150fveq2d 5529 . . . . . . . 8
152151oveq2d 5874 . . . . . . 7
153148, 152oveq12d 5876 . . . . . 6
154153eqeq2d 2294 . . . . 5
155146, 154syl5ibrcom 213 . . . 4