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