Metamath Proof Explorer

Theorem efeq1

Description: A complex number whose exponential is one is an integer multiple of 2pi i . (Contributed by NM, 17-Aug-2008) (Revised by Mario Carneiro, 10-May-2014)

Ref Expression
Assertion efeq1 
|- ( A e. CC -> ( ( exp ` A ) = 1 <-> ( A / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )

Proof

Step Hyp Ref Expression
1 halfcl 
 |-  ( A e. CC -> ( A / 2 ) e. CC )
2 ax-icn 
 |-  _i e. CC
3 ine0 
 |-  _i =/= 0
4 divcl 
 |-  ( ( ( A / 2 ) e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( ( A / 2 ) / _i ) e. CC )
5 2 3 4 mp3an23 
 |-  ( ( A / 2 ) e. CC -> ( ( A / 2 ) / _i ) e. CC )
6 1 5 syl 
 |-  ( A e. CC -> ( ( A / 2 ) / _i ) e. CC )
7 sineq0 
 |-  ( ( ( A / 2 ) / _i ) e. CC -> ( ( sin ` ( ( A / 2 ) / _i ) ) = 0 <-> ( ( ( A / 2 ) / _i ) / _pi ) e. ZZ ) )
8 6 7 syl 
 |-  ( A e. CC -> ( ( sin ` ( ( A / 2 ) / _i ) ) = 0 <-> ( ( ( A / 2 ) / _i ) / _pi ) e. ZZ ) )
9 sinval 
 |-  ( ( ( A / 2 ) / _i ) e. CC -> ( sin ` ( ( A / 2 ) / _i ) ) = ( ( ( exp ` ( _i x. ( ( A / 2 ) / _i ) ) ) - ( exp ` ( -u _i x. ( ( A / 2 ) / _i ) ) ) ) / ( 2 x. _i ) ) )
10 6 9 syl 
 |-  ( A e. CC -> ( sin ` ( ( A / 2 ) / _i ) ) = ( ( ( exp ` ( _i x. ( ( A / 2 ) / _i ) ) ) - ( exp ` ( -u _i x. ( ( A / 2 ) / _i ) ) ) ) / ( 2 x. _i ) ) )
11 divcan2 
 |-  ( ( ( A / 2 ) e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( _i x. ( ( A / 2 ) / _i ) ) = ( A / 2 ) )
12 2 3 11 mp3an23 
 |-  ( ( A / 2 ) e. CC -> ( _i x. ( ( A / 2 ) / _i ) ) = ( A / 2 ) )
13 1 12 syl 
 |-  ( A e. CC -> ( _i x. ( ( A / 2 ) / _i ) ) = ( A / 2 ) )
14 13 fveq2d 
 |-  ( A e. CC -> ( exp ` ( _i x. ( ( A / 2 ) / _i ) ) ) = ( exp ` ( A / 2 ) ) )
15 mulneg1 
 |-  ( ( _i e. CC /\ ( ( A / 2 ) / _i ) e. CC ) -> ( -u _i x. ( ( A / 2 ) / _i ) ) = -u ( _i x. ( ( A / 2 ) / _i ) ) )
16 2 6 15 sylancr 
 |-  ( A e. CC -> ( -u _i x. ( ( A / 2 ) / _i ) ) = -u ( _i x. ( ( A / 2 ) / _i ) ) )
17 13 negeqd 
 |-  ( A e. CC -> -u ( _i x. ( ( A / 2 ) / _i ) ) = -u ( A / 2 ) )
18 16 17 eqtrd 
 |-  ( A e. CC -> ( -u _i x. ( ( A / 2 ) / _i ) ) = -u ( A / 2 ) )
19 18 fveq2d 
 |-  ( A e. CC -> ( exp ` ( -u _i x. ( ( A / 2 ) / _i ) ) ) = ( exp ` -u ( A / 2 ) ) )
20 14 19 oveq12d 
 |-  ( A e. CC -> ( ( exp ` ( _i x. ( ( A / 2 ) / _i ) ) ) - ( exp ` ( -u _i x. ( ( A / 2 ) / _i ) ) ) ) = ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) )
21 20 oveq1d 
 |-  ( A e. CC -> ( ( ( exp ` ( _i x. ( ( A / 2 ) / _i ) ) ) - ( exp ` ( -u _i x. ( ( A / 2 ) / _i ) ) ) ) / ( 2 x. _i ) ) = ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( 2 x. _i ) ) )
22 10 21 eqtrd 
 |-  ( A e. CC -> ( sin ` ( ( A / 2 ) / _i ) ) = ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( 2 x. _i ) ) )
23 22 eqeq1d 
 |-  ( A e. CC -> ( ( sin ` ( ( A / 2 ) / _i ) ) = 0 <-> ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( 2 x. _i ) ) = 0 ) )
24 efcl 
 |-  ( ( A / 2 ) e. CC -> ( exp ` ( A / 2 ) ) e. CC )
25 1 24 syl 
 |-  ( A e. CC -> ( exp ` ( A / 2 ) ) e. CC )
26 1 negcld 
 |-  ( A e. CC -> -u ( A / 2 ) e. CC )
27 efcl 
 |-  ( -u ( A / 2 ) e. CC -> ( exp ` -u ( A / 2 ) ) e. CC )
28 26 27 syl 
 |-  ( A e. CC -> ( exp ` -u ( A / 2 ) ) e. CC )
29 25 28 subcld 
 |-  ( A e. CC -> ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) e. CC )
30 2cn 
 |-  2 e. CC
31 30 2 mulcli 
 |-  ( 2 x. _i ) e. CC
32 2ne0 
 |-  2 =/= 0
33 30 2 32 3 mulne0i 
 |-  ( 2 x. _i ) =/= 0
34 diveq0 
 |-  ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) e. CC /\ ( 2 x. _i ) e. CC /\ ( 2 x. _i ) =/= 0 ) -> ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( 2 x. _i ) ) = 0 <-> ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) = 0 ) )
35 31 33 34 mp3an23 
 |-  ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) e. CC -> ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( 2 x. _i ) ) = 0 <-> ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) = 0 ) )
36 29 35 syl 
 |-  ( A e. CC -> ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( 2 x. _i ) ) = 0 <-> ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) = 0 ) )
37 efne0 
 |-  ( -u ( A / 2 ) e. CC -> ( exp ` -u ( A / 2 ) ) =/= 0 )
38 26 37 syl 
 |-  ( A e. CC -> ( exp ` -u ( A / 2 ) ) =/= 0 )
39 25 28 28 38 divsubdird 
 |-  ( A e. CC -> ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( exp ` -u ( A / 2 ) ) ) = ( ( ( exp ` ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) - ( ( exp ` -u ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) ) )
40 efsub 
 |-  ( ( ( A / 2 ) e. CC /\ -u ( A / 2 ) e. CC ) -> ( exp ` ( ( A / 2 ) - -u ( A / 2 ) ) ) = ( ( exp ` ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) )
41 1 26 40 syl2anc 
 |-  ( A e. CC -> ( exp ` ( ( A / 2 ) - -u ( A / 2 ) ) ) = ( ( exp ` ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) )
42 1 1 subnegd 
 |-  ( A e. CC -> ( ( A / 2 ) - -u ( A / 2 ) ) = ( ( A / 2 ) + ( A / 2 ) ) )
43 2halves 
 |-  ( A e. CC -> ( ( A / 2 ) + ( A / 2 ) ) = A )
44 42 43 eqtrd 
 |-  ( A e. CC -> ( ( A / 2 ) - -u ( A / 2 ) ) = A )
45 44 fveq2d 
 |-  ( A e. CC -> ( exp ` ( ( A / 2 ) - -u ( A / 2 ) ) ) = ( exp ` A ) )
46 41 45 eqtr3d 
 |-  ( A e. CC -> ( ( exp ` ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) = ( exp ` A ) )
47 28 38 dividd 
 |-  ( A e. CC -> ( ( exp ` -u ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) = 1 )
48 46 47 oveq12d 
 |-  ( A e. CC -> ( ( ( exp ` ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) - ( ( exp ` -u ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) ) = ( ( exp ` A ) - 1 ) )
49 39 48 eqtrd 
 |-  ( A e. CC -> ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( exp ` -u ( A / 2 ) ) ) = ( ( exp ` A ) - 1 ) )
50 49 eqeq1d 
 |-  ( A e. CC -> ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( exp ` -u ( A / 2 ) ) ) = 0 <-> ( ( exp ` A ) - 1 ) = 0 ) )
51 29 28 38 diveq0ad 
 |-  ( A e. CC -> ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( exp ` -u ( A / 2 ) ) ) = 0 <-> ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) = 0 ) )
52 efcl 
 |-  ( A e. CC -> ( exp ` A ) e. CC )
53 ax-1cn 
 |-  1 e. CC
54 subeq0 
 |-  ( ( ( exp ` A ) e. CC /\ 1 e. CC ) -> ( ( ( exp ` A ) - 1 ) = 0 <-> ( exp ` A ) = 1 ) )
55 52 53 54 sylancl 
 |-  ( A e. CC -> ( ( ( exp ` A ) - 1 ) = 0 <-> ( exp ` A ) = 1 ) )
56 50 51 55 3bitr3d 
 |-  ( A e. CC -> ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) = 0 <-> ( exp ` A ) = 1 ) )
57 23 36 56 3bitrd 
 |-  ( A e. CC -> ( ( sin ` ( ( A / 2 ) / _i ) ) = 0 <-> ( exp ` A ) = 1 ) )
58 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
59 2 3 pm3.2i 
 |-  ( _i e. CC /\ _i =/= 0 )
60 divdiv32 
 |-  ( ( A e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( _i e. CC /\ _i =/= 0 ) ) -> ( ( A / 2 ) / _i ) = ( ( A / _i ) / 2 ) )
61 58 59 60 mp3an23 
 |-  ( A e. CC -> ( ( A / 2 ) / _i ) = ( ( A / _i ) / 2 ) )
62 61 oveq1d 
 |-  ( A e. CC -> ( ( ( A / 2 ) / _i ) / _pi ) = ( ( ( A / _i ) / 2 ) / _pi ) )
63 divcl 
 |-  ( ( A e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( A / _i ) e. CC )
64 2 3 63 mp3an23 
 |-  ( A e. CC -> ( A / _i ) e. CC )
65 picn 
 |-  _pi e. CC
66 pire 
 |-  _pi e. RR
67 pipos 
 |-  0 < _pi
68 66 67 gt0ne0ii 
 |-  _pi =/= 0
69 65 68 pm3.2i 
 |-  ( _pi e. CC /\ _pi =/= 0 )
70 divdiv1 
 |-  ( ( ( A / _i ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( _pi e. CC /\ _pi =/= 0 ) ) -> ( ( ( A / _i ) / 2 ) / _pi ) = ( ( A / _i ) / ( 2 x. _pi ) ) )
71 58 69 70 mp3an23 
 |-  ( ( A / _i ) e. CC -> ( ( ( A / _i ) / 2 ) / _pi ) = ( ( A / _i ) / ( 2 x. _pi ) ) )
72 64 71 syl 
 |-  ( A e. CC -> ( ( ( A / _i ) / 2 ) / _pi ) = ( ( A / _i ) / ( 2 x. _pi ) ) )
73 30 65 mulcli 
 |-  ( 2 x. _pi ) e. CC
74 30 65 32 68 mulne0i 
 |-  ( 2 x. _pi ) =/= 0
75 73 74 pm3.2i 
 |-  ( ( 2 x. _pi ) e. CC /\ ( 2 x. _pi ) =/= 0 )
76 divdiv1 
 |-  ( ( A e. CC /\ ( _i e. CC /\ _i =/= 0 ) /\ ( ( 2 x. _pi ) e. CC /\ ( 2 x. _pi ) =/= 0 ) ) -> ( ( A / _i ) / ( 2 x. _pi ) ) = ( A / ( _i x. ( 2 x. _pi ) ) ) )
77 59 75 76 mp3an23 
 |-  ( A e. CC -> ( ( A / _i ) / ( 2 x. _pi ) ) = ( A / ( _i x. ( 2 x. _pi ) ) ) )
78 72 77 eqtrd 
 |-  ( A e. CC -> ( ( ( A / _i ) / 2 ) / _pi ) = ( A / ( _i x. ( 2 x. _pi ) ) ) )
79 62 78 eqtrd 
 |-  ( A e. CC -> ( ( ( A / 2 ) / _i ) / _pi ) = ( A / ( _i x. ( 2 x. _pi ) ) ) )
80 79 eleq1d 
 |-  ( A e. CC -> ( ( ( ( A / 2 ) / _i ) / _pi ) e. ZZ <-> ( A / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
81 8 57 80 3bitr3d 
 |-  ( A e. CC -> ( ( exp ` A ) = 1 <-> ( A / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )