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 ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) = 1 ↔ ( 𝐴 / ( i · ( 2 · π ) ) ) ∈ ℤ ) )

Proof

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