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 1 efcld 
 |-  ( A e. CC -> ( exp ` ( A / 2 ) ) e. CC )
25 1 negcld 
 |-  ( A e. CC -> -u ( A / 2 ) e. CC )
26 25 efcld 
 |-  ( A e. CC -> ( exp ` -u ( A / 2 ) ) e. CC )
27 24 26 subcld 
 |-  ( A e. CC -> ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) e. CC )
28 2mulicn 
 |-  ( 2 x. _i ) e. CC
29 2muline0 
 |-  ( 2 x. _i ) =/= 0
30 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 ) )
31 28 29 30 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 ) )
32 27 31 syl 
 |-  ( A e. CC -> ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( 2 x. _i ) ) = 0 <-> ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) = 0 ) )
33 25 efne0d 
 |-  ( A e. CC -> ( exp ` -u ( A / 2 ) ) =/= 0 )
34 24 26 26 33 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 ) ) ) ) )
35 efsub 
 |-  ( ( ( A / 2 ) e. CC /\ -u ( A / 2 ) e. CC ) -> ( exp ` ( ( A / 2 ) - -u ( A / 2 ) ) ) = ( ( exp ` ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) )
36 1 25 35 syl2anc 
 |-  ( A e. CC -> ( exp ` ( ( A / 2 ) - -u ( A / 2 ) ) ) = ( ( exp ` ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) )
37 1 1 subnegd 
 |-  ( A e. CC -> ( ( A / 2 ) - -u ( A / 2 ) ) = ( ( A / 2 ) + ( A / 2 ) ) )
38 2halves 
 |-  ( A e. CC -> ( ( A / 2 ) + ( A / 2 ) ) = A )
39 37 38 eqtrd 
 |-  ( A e. CC -> ( ( A / 2 ) - -u ( A / 2 ) ) = A )
40 39 fveq2d 
 |-  ( A e. CC -> ( exp ` ( ( A / 2 ) - -u ( A / 2 ) ) ) = ( exp ` A ) )
41 36 40 eqtr3d 
 |-  ( A e. CC -> ( ( exp ` ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) = ( exp ` A ) )
42 26 33 dividd 
 |-  ( A e. CC -> ( ( exp ` -u ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) = 1 )
43 41 42 oveq12d 
 |-  ( A e. CC -> ( ( ( exp ` ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) - ( ( exp ` -u ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) ) = ( ( exp ` A ) - 1 ) )
44 34 43 eqtrd 
 |-  ( A e. CC -> ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( exp ` -u ( A / 2 ) ) ) = ( ( exp ` A ) - 1 ) )
45 44 eqeq1d 
 |-  ( A e. CC -> ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( exp ` -u ( A / 2 ) ) ) = 0 <-> ( ( exp ` A ) - 1 ) = 0 ) )
46 27 26 33 diveq0ad 
 |-  ( A e. CC -> ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( exp ` -u ( A / 2 ) ) ) = 0 <-> ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) = 0 ) )
47 efcl 
 |-  ( A e. CC -> ( exp ` A ) e. CC )
48 ax-1cn 
 |-  1 e. CC
49 subeq0 
 |-  ( ( ( exp ` A ) e. CC /\ 1 e. CC ) -> ( ( ( exp ` A ) - 1 ) = 0 <-> ( exp ` A ) = 1 ) )
50 47 48 49 sylancl 
 |-  ( A e. CC -> ( ( ( exp ` A ) - 1 ) = 0 <-> ( exp ` A ) = 1 ) )
51 45 46 50 3bitr3d 
 |-  ( A e. CC -> ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) = 0 <-> ( exp ` A ) = 1 ) )
52 23 32 51 3bitrd 
 |-  ( A e. CC -> ( ( sin ` ( ( A / 2 ) / _i ) ) = 0 <-> ( exp ` A ) = 1 ) )
53 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
54 2 3 pm3.2i 
 |-  ( _i e. CC /\ _i =/= 0 )
55 divdiv32 
 |-  ( ( A e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( _i e. CC /\ _i =/= 0 ) ) -> ( ( A / 2 ) / _i ) = ( ( A / _i ) / 2 ) )
56 53 54 55 mp3an23 
 |-  ( A e. CC -> ( ( A / 2 ) / _i ) = ( ( A / _i ) / 2 ) )
57 56 oveq1d 
 |-  ( A e. CC -> ( ( ( A / 2 ) / _i ) / _pi ) = ( ( ( A / _i ) / 2 ) / _pi ) )
58 divcl 
 |-  ( ( A e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( A / _i ) e. CC )
59 2 3 58 mp3an23 
 |-  ( A e. CC -> ( A / _i ) e. CC )
60 picn 
 |-  _pi e. CC
61 pine0 
 |-  _pi =/= 0
62 60 61 pm3.2i 
 |-  ( _pi e. CC /\ _pi =/= 0 )
63 divdiv1 
 |-  ( ( ( A / _i ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( _pi e. CC /\ _pi =/= 0 ) ) -> ( ( ( A / _i ) / 2 ) / _pi ) = ( ( A / _i ) / ( 2 x. _pi ) ) )
64 53 62 63 mp3an23 
 |-  ( ( A / _i ) e. CC -> ( ( ( A / _i ) / 2 ) / _pi ) = ( ( A / _i ) / ( 2 x. _pi ) ) )
65 59 64 syl 
 |-  ( A e. CC -> ( ( ( A / _i ) / 2 ) / _pi ) = ( ( A / _i ) / ( 2 x. _pi ) ) )
66 2picn 
 |-  ( 2 x. _pi ) e. CC
67 2cn 
 |-  2 e. CC
68 2ne0 
 |-  2 =/= 0
69 67 60 68 61 mulne0i 
 |-  ( 2 x. _pi ) =/= 0
70 66 69 pm3.2i 
 |-  ( ( 2 x. _pi ) e. CC /\ ( 2 x. _pi ) =/= 0 )
71 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 ) ) ) )
72 54 70 71 mp3an23 
 |-  ( A e. CC -> ( ( A / _i ) / ( 2 x. _pi ) ) = ( A / ( _i x. ( 2 x. _pi ) ) ) )
73 65 72 eqtrd 
 |-  ( A e. CC -> ( ( ( A / _i ) / 2 ) / _pi ) = ( A / ( _i x. ( 2 x. _pi ) ) ) )
74 57 73 eqtrd 
 |-  ( A e. CC -> ( ( ( A / 2 ) / _i ) / _pi ) = ( A / ( _i x. ( 2 x. _pi ) ) ) )
75 74 eleq1d 
 |-  ( A e. CC -> ( ( ( ( A / 2 ) / _i ) / _pi ) e. ZZ <-> ( A / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
76 8 52 75 3bitr3d 
 |-  ( A e. CC -> ( ( exp ` A ) = 1 <-> ( A / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )