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

Theorem efif1olem4 20498
Description: The exponential function of an imaginary number maps any interval of length 2 one-to-one onto the unit circle. (Contributed by Paul Chapman, 16-Mar-2008.) (Proof shortened by Mario Carneiro, 13-May-2014.)
Hypotheses
Ref Expression
efif1o.1
efif1o.2
efif1olem4.3
efif1olem4.4
efif1olem4.5
efif1olem4.6
Assertion
Ref Expression
efif1olem4
Distinct variable groups:   , , ,   , , ,   , ,   , , , ,   ,S,   , , , ,
Allowed substitution hints:   ( )   S( , )   ( , )

Proof of Theorem efif1olem4
StepHypRef Expression
1 efif1olem4.3 . . . . . 6
21sselda 3337 . . . . 5
3 ax-icn 9100 . . . . . . . . 9
4 recn 9131 . . . . . . . . 9
5 mulcl 9125 . . . . . . . . 9
63, 4, 5sylancr 646 . . . . . . . 8
7 efcl 12736 . . . . . . . 8
86, 7syl 16 . . . . . . 7
9 absefi 12848 . . . . . . 7
10 absf 12192 . . . . . . . . 9
11 ffn 5638 . . . . . . . . 9
1210, 11ax-mp 5 . . . . . . . 8
13 fniniseg 5899 . . . . . . . 8
1412, 13ax-mp 5 . . . . . . 7
158, 9, 14sylanbrc 647 . . . . . 6
16 efif1o.2 . . . . . 6
1715, 16syl6eleqr 2534 . . . . 5
182, 17syl 16 . . . 4
19 efif1o.1 . . . 4
2018, 19fmptd 5941 . . 3
211ad2antrr 708 . . . . . . . 8
22 simplrl 738 . . . . . . . 8
2321, 22sseldd 3338 . . . . . . 7
2423recnd 9165 . . . . . 6
25 simplrr 739 . . . . . . . 8
2621, 25sseldd 3338 . . . . . . 7
2726recnd 9165 . . . . . 6
2824, 27subcld 9462 . . . . . . . . 9
29 2re 10120 . . . . . . . . . . . 12
30 pire 20423 . . . . . . . . . . . 12
3129, 30remulcli 9155 . . . . . . . . . . 11
3231recni 9153 . . . . . . . . . 10
33 2pos 10133 . . . . . . . . . . . 12
34 pipos 20424 . . . . . . . . . . . 12
3529, 30, 33, 34mulgt0ii 9257 . . . . . . . . . . 11
3631, 35gt0ne0ii 9614 . . . . . . . . . 10
37 divcl 9735 . . . . . . . . . 10
3832, 36, 37mp3an23 1272 . . . . . . . . 9
3928, 38syl 16 . . . . . . . 8
40 absdiv 12151 . . . . . . . . . . . . 13
4132, 36, 40mp3an23 1272 . . . . . . . . . . . 12
4228, 41syl 16 . . . . . . . . . . 11
43 0re 9142 . . . . . . . . . . . . . 14
4443, 31, 35ltleii 9247 . . . . . . . . . . . . 13
45 absid 12152 . . . . . . . . . . . . 13
4631, 44, 45mp2an 655 . . . . . . . . . . . 12
4746oveq2i 6140 . . . . . . . . . . 11
4842, 47syl6eq 2491 . . . . . . . . . 10
49 efif1olem4.4 . . . . . . . . . . . . 13
5049adantr 453 . . . . . . . . . . . 12
5132mulid1i 9143 . . . . . . . . . . . 12
5250, 51syl6breqr 4283 . . . . . . . . . . 11
5328abscld 12289 . . . . . . . . . . . 12
54 1re 9141 . . . . . . . . . . . . 13
5531, 35pm3.2i 443 . . . . . . . . . . . . 13
56 ltdivmul 9933 . . . . . . . . . . . . 13
5754, 55, 56mp3an23 1272 . . . . . . . . . . . 12
5853, 57syl 16 . . . . . . . . . . 11
5952, 58mpbird 225 . . . . . . . . . 10
6048, 59eqbrtrd 4263 . . . . . . . . 9
6132, 36pm3.2i 443 . . . . . . . . . . . . . 14
62 ine0 9520 . . . . . . . . . . . . . . 15
633, 62pm3.2i 443 . . . . . . . . . . . . . 14
64 divcan5 9767 . . . . . . . . . . . . . 14
6561, 63, 64mp3an23 1272 . . . . . . . . . . . . 13
6628, 65syl 16 . . . . . . . . . . . 12
673a1i 11 . . . . . . . . . . . . . . . 16
6867, 24, 27subdid 9540 . . . . . . . . . . . . . . 15
6968fveq2d 5779 . . . . . . . . . . . . . 14
70 mulcl 9125 . . . . . . . . . . . . . . . 16
713, 24, 70sylancr 646 . . . . . . . . . . . . . . 15
72 mulcl 9125 . . . . . . . . . . . . . . . 16
733, 27, 72sylancr 646 . . . . . . . . . . . . . . 15
74 efsub 12752 . . . . . . . . . . . . . . 15
7571, 73, 74syl2anc 644 . . . . . . . . . . . . . 14
76 efcl 12736 . . . . . . . . . . . . . . . 16
7773, 76syl 16 . . . . . . . . . . . . . . 15
78 efne0 12749 . . . . . . . . . . . . . . . 16
7973, 78syl 16 . . . . . . . . . . . . . . 15
80 simpr 449 . . . . . . . . . . . . . . . 16
81 oveq2 6137 . . . . . . . . . . . . . . . . . . 19
8281fveq2d 5779 . . . . . . . . . . . . . . . . . 18
83 fvex 5785 . . . . . . . . . . . . . . . . . 18
8482, 19, 83fvmpt 5854 . . . . . . . . . . . . . . . . 17
8522, 84syl 16 . . . . . . . . . . . . . . . 16
86 oveq2 6137 . . . . . . . . . . . . . . . . . . 19
8786fveq2d 5779 . . . . . . . . . . . . . . . . . 18
88 fvex 5785 . . . . . . . . . . . . . . . . . 18
8987, 19, 88fvmpt 5854 . . . . . . . . . . . . . . . . 17
9025, 89syl 16 . . . . . . . . . . . . . . . 16
9180, 85, 903eqtr3d 2483 . . . . . . . . . . . . . . 15
9277, 79, 91diveq1bd 9889 . . . . . . . . . . . . . 14
9369, 75, 923eqtrd 2479 . . . . . . . . . . . . 13
94 mulcl 9125 . . . . . . . . . . . . . . 15
953, 28, 94sylancr 646 . . . . . . . . . . . . . 14
96 efeq1 20482 . . . . . . . . . . . . . 14
9795, 96syl 16 . . . . . . . . . . . . 13
9893, 97mpbid 203 . . . . . . . . . . . 12
9966, 98eqeltrrd 2518 . . . . . . . . . . 11
100 nn0abscl 12168 . . . . . . . . . . 11
10199, 100syl 16 . . . . . . . . . 10
102 nn0lt10b 10387 . . . . . . . . . 10
103101, 102syl 16 . . . . . . . . 9
10460, 103mpbid 203 . . . . . . . 8
10539, 104abs00d 12299 . . . . . . 7
106 diveq0 9739 . . . . . . . . 9
10732, 36, 106mp3an23 1272 . . . . . . . 8
10828, 107syl 16 . . . . . . 7
109105, 108mpbid 203 . . . . . 6
11024, 27, 109subeq0d 9470 . . . . 5
111110ex 425 . . . 4
112111ralrimivva 2805 . . 3
113 dff13 6052 . . 3
11420, 112, 113sylanbrc 647 . 2
115 halfpire 20426 . . . . . . . . . 10
116115renegcli 9413 . . . . . . . . 9
117 iccssre 11043 . . . . . . . . 9
118116, 115, 117mp2an 655 . . . . . . . 8
11919, 16efif1olem3 20497 . . . . . . . . 9
120 resinf1o 20489 . . . . . . . . . . . 12
121 efif1olem4.6 . . . . . . . . . . . . 13
122 f1oeq1 5712 . . . . . . . . . . . . 13
123121, 122ax-mp 5 . . . . . . . . . . . 12
124120, 123mpbir 202 . . . . . . . . . . 11
125 f1ocnv 5734 . . . . . . . . . . 11
126 f1of 5721 . . . . . . . . . . 11
127124, 125, 126mp2b 10 . . . . . . . . . 10
128127ffvelrni 5917 . . . . . . . . 9
129119, 128syl 16 . . . . . . . 8
130118, 129sseldi 3335 . . . . . . 7
131 remulcl 9126 . . . . . . 7
13229, 130, 131sylancr 646 . . . . . 6
133 efif1olem4.5 . . . . . . . 8
134133ralrimiva 2796 . . . . . . 7
135134adantr 453 . . . . . 6
136 oveq1 6136 . . . . . . . . . 10
137136oveq1d 6144 . . . . . . . . 9
138137eleq1d 2509 . . . . . . . 8
139138rexbidv 2733 . . . . . . 7
140139rspcv 3057 . . . . . 6
141132, 135, 140sylc 59 . . . . 5
142 oveq1 6136 . . . . . . . 8
1433a1i 11 . . . . . . . . . . . . . 14
144132adantr 453 . . . . . . . . . . . . . . 15
145144recnd 9165 . . . . . . . . . . . . . 14
1461ad2antrr 708 . . . . . . . . . . . . . . . 16
147 simpr 449 . . . . . . . . . . . . . . . 16
148146, 147sseldd 3338 . . . . . . . . . . . . . . 15
149148recnd 9165 . . . . . . . . . . . . . 14
150143, 145, 149subdid 9540 . . . . . . . . . . . . 13
151150oveq1d 6144 . . . . . . . . . . . 12
152 mulcl 9125 . . . . . . . . . . . . . 14
1533, 145, 152sylancr 646 . . . . . . . . . . . . 13
1543, 149, 72sylancr 646 . . . . . . . . . . . . 13
155153, 154npcand 9466 . . . . . . . . . . . 12
156151, 155eqtrd 2475 . . . . . . . . . . 11
157156fveq2d 5779 . . . . . . . . . 10
158145, 149subcld 9462 . . . . . . . . . . . 12
159 mulcl 9125 . . . . . . . . . . . 12
1603, 158, 159sylancr 646 . . . . . . . . . . 11
161 efadd 12747 . . . . . . . . . . 11
162160, 154, 161syl2anc 644 . . . . . . . . . 10
163130recnd 9165 . . . . . . . . . . . . . . 15
164 2cn 10121 . . . . . . . . . . . . . . . 16
165 mul12 9283 . . . . . . . . . . . . . . . 16
1663, 164, 165mp3an12 1270 . . . . . . . . . . . . . . 15
167163, 166syl 16 . . . . . . . . . . . . . 14
168167fveq2d 5779 . . . . . . . . . . . . 13
169 mulcl 9125 . . . . . . . . . . . . . . 15
1703, 163, 169sylancr 646 . . . . . . . . . . . . . 14
171 2z 10363 . . . . . . . . . . . . . 14
172 efexp 12753 . . . . . . . . . . . . . 14
173170, 171, 172sylancl 645 . . . . . . . . . . . . 13
174168, 173eqtrd 2475 . . . . . . . . . . . 12
175130recoscld 12796 . . . . . . . . . . . . . . . 16
176 simpr 449 . . . . . . . . . . . . . . . . . . . . 21
177176, 16syl6eleq 2533 . . . . . . . . . . . . . . . . . . . 20
178 fniniseg 5899 . . . . . . . . . . . . . . . . . . . . 21
17912, 178ax-mp 5 . . . . . . . . . . . . . . . . . . . 20
180177, 179sylib 190 . . . . . . . . . . . . . . . . . . 19
181180simpld 447 . . . . . . . . . . . . . . . . . 18
182181sqrcld 12290 . . . . . . . . . . . . . . . . 17
183182recld 12050 . . . . . . . . . . . . . . . 16
184 cosq14ge0 20470 . . . . . . . . . . . . . . . . 17
185129, 184syl 16 . . . . . . . . . . . . . . . 16
186181sqrrege0d 12291 . . . . . . . . . . . . . . . 16
187 sincossq 12828 . . . . . . . . . . . . . . . . . . . 20
188163, 187syl 16 . . . . . . . . . . . . . . . . . . 19
189181sqsqrd 12292 . . . . . . . . . . . . . . . . . . . . 21
190189fveq2d 5779 . . . . . . . . . . . . . . . . . . . 20
191 2nn0 10289 . . . . . . . . . . . . . . . . . . . . 21
192 absexp 12160 . . . . . . . . . . . . . . . . . . . . 21
193182, 191, 192sylancl 645 . . . . . . . . . . . . . . . . . . . 20
194180simprd 451 . . . . . . . . . . . . . . . . . . . 20
195190, 193, 1943eqtr3d 2483 . . . . . . . . . . . . . . . . . . 19
196182absvalsq2d 12296 . . . . . . . . . . . . . . . . . . 19
197188, 195, 1963eqtr2d 2481 . . . . . . . . . . . . . . . . . 18
198121fveq1i 5776 . . . . . . . . . . . . . . . . . . . . 21
199 fvres 5788 . . . . . . . . . . . . . . . . . . . . . 22
200129, 199syl 16 . . . . . . . . . . . . . . . . . . . . 21
201198, 200syl5eq 2487 . . . . . . . . . . . . . . . . . . . 20
202 f1ocnvfv2 6063 . . . . . . . . . . . . . . . . . . . . 21
203124, 119, 202sylancr 646 . . . . . . . . . . . . . . . . . . . 20
204201, 203eqtr3d 2477 . . . . . . . . . . . . . . . . . . 19
205204oveq1d 6144 . . . . . . . . . . . . . . . . . 18
206197, 205oveq12d 6147 . . . . . . . . . . . . . . . . 17
207163sincld 12782 . . . . . . . . . . . . . . . . . . 19
208207sqcld 11572 . . . . . . . . . . . . . . . . . 18
209163coscld 12783 . . . . . . . . . . . . . . . . . . 19
210209sqcld 11572 . . . . . . . . . . . . . . . . . 18
211208, 210pncan2d 9464 . . . . . . . . . . . . . . . . 17
212183recnd 9165 . . . . . . . . . . . . . . . . . . 19
213212sqcld 11572 . . . . . . . . . . . . . . . . . 18
214205, 208eqeltrrd 2518 . . . . . . . . . . . . . . . . . 18
215213, 214pncand 9463 . . . . . . . . . . . . . . . . 17
216206, 211, 2153eqtr3d 2483 . . . . . . . . . . . . . . . 16
217175, 183, 185, 186, 216sq11d 11610 . . . . . . . . . . . . . . 15
218204oveq2d 6145 . . . . . . . . . . . . . . 15
219217, 218oveq12d 6147 . . . . . . . . . . . . . 14
220 efival 12804 . . . . . . . . . . . . . . 15