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∈ℂ→eA=1↔Ai⁢2⁢π∈ℤ

Proof

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