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\in ℂ\to \left({\mathrm{e}}^A=1\leftrightarrow \frac{A}{\mathrm{i}2\mathrm{\pi }}\in \mathbb{Z}\right)$$

Proof

Step	Hyp	Ref	Expression
1		halfcl	$$⊢A\in ℂ\to \frac{A}{2}\in ℂ$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3		ine0	$$⊢\mathrm{i}\ne 0$$
4		divcl	$$⊢\left(\frac{A}{2}\in ℂ\wedge \mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\right)\to \frac{\frac{A}{2}}{\mathrm{i}}\in ℂ$$
5	2 3 4	mp3an23	$$⊢\frac{A}{2}\in ℂ\to \frac{\frac{A}{2}}{\mathrm{i}}\in ℂ$$
6	1 5	syl	$$⊢A\in ℂ\to \frac{\frac{A}{2}}{\mathrm{i}}\in ℂ$$
7		sineq0	$$⊢\frac{\frac{A}{2}}{\mathrm{i}}\in ℂ\to \left(\sin \left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=0\leftrightarrow \frac{\frac{\frac{A}{2}}{\mathrm{i}}}{\mathrm{\pi }}\in \mathbb{Z}\right)$$
8	6 7	syl	$$⊢A\in ℂ\to \left(\sin \left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=0\leftrightarrow \frac{\frac{\frac{A}{2}}{\mathrm{i}}}{\mathrm{\pi }}\in \mathbb{Z}\right)$$
9		sinval	$$⊢\frac{\frac{A}{2}}{\mathrm{i}}\in ℂ\to \sin \left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=\frac{{\mathrm{e}}^{\mathrm{i}\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)}-{\mathrm{e}}^{\left(-\mathrm{i}\right)\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)}}{2\mathrm{i}}$$
10	6 9	syl	$$⊢A\in ℂ\to \sin \left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=\frac{{\mathrm{e}}^{\mathrm{i}\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)}-{\mathrm{e}}^{\left(-\mathrm{i}\right)\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)}}{2\mathrm{i}}$$
11		divcan2	$$⊢\left(\frac{A}{2}\in ℂ\wedge \mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\right)\to \mathrm{i}\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=\frac{A}{2}$$
12	2 3 11	mp3an23	$$⊢\frac{A}{2}\in ℂ\to \mathrm{i}\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=\frac{A}{2}$$
13	1 12	syl	$$⊢A\in ℂ\to \mathrm{i}\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=\frac{A}{2}$$
14	13	fveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)}={\mathrm{e}}^{\frac{A}{2}}$$
15		mulneg1	$$⊢\left(\mathrm{i}\in ℂ\wedge \frac{\frac{A}{2}}{\mathrm{i}}\in ℂ\right)\to \left(-\mathrm{i}\right)\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=-\mathrm{i}\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)$$
16	2 6 15	sylancr	$$⊢A\in ℂ\to \left(-\mathrm{i}\right)\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=-\mathrm{i}\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)$$
17	13	negeqd	$$⊢A\in ℂ\to -\mathrm{i}\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=-\frac{A}{2}$$
18	16 17	eqtrd	$$⊢A\in ℂ\to \left(-\mathrm{i}\right)\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=-\frac{A}{2}$$
19	18	fveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{\left(-\mathrm{i}\right)\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)}={\mathrm{e}}^{-\frac{A}{2}}$$
20	14 19	oveq12d	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)}-{\mathrm{e}}^{\left(-\mathrm{i}\right)\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)}={\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}$$
21	20	oveq1d	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^{\mathrm{i}\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)}-{\mathrm{e}}^{\left(-\mathrm{i}\right)\left(\frac{\frac{A}{2}}{\mathrm{i}}\right)}}{2\mathrm{i}}=\frac{{\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}}{2\mathrm{i}}$$
22	10 21	eqtrd	$$⊢A\in ℂ\to \sin \left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=\frac{{\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}}{2\mathrm{i}}$$
23	22	eqeq1d	$$⊢A\in ℂ\to \left(\sin \left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=0\leftrightarrow \frac{{\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}}{2\mathrm{i}}=0\right)$$
24	1	efcld	$$⊢A\in ℂ\to {\mathrm{e}}^{\frac{A}{2}}\in ℂ$$
25	1	negcld	$$⊢A\in ℂ\to -\frac{A}{2}\in ℂ$$
26	25	efcld	$$⊢A\in ℂ\to {\mathrm{e}}^{-\frac{A}{2}}\in ℂ$$
27	24 26	subcld	$$⊢A\in ℂ\to {\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}\in ℂ$$
28		2mulicn	$$⊢2\mathrm{i}\in ℂ$$
29		2muline0	$$⊢2\mathrm{i}\ne 0$$
30		diveq0	$$⊢\left({\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}\in ℂ\wedge 2\mathrm{i}\in ℂ\wedge 2\mathrm{i}\ne 0\right)\to \left(\frac{{\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}}{2\mathrm{i}}=0\leftrightarrow {\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}=0\right)$$
31	28 29 30	mp3an23	$$⊢{\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}\in ℂ\to \left(\frac{{\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}}{2\mathrm{i}}=0\leftrightarrow {\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}=0\right)$$
32	27 31	syl	$$⊢A\in ℂ\to \left(\frac{{\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}}{2\mathrm{i}}=0\leftrightarrow {\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}=0\right)$$
33	25	efne0d	$$⊢A\in ℂ\to {\mathrm{e}}^{-\frac{A}{2}}\ne 0$$
34	24 26 26 33	divsubdird	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}=\left(\frac{{\mathrm{e}}^{\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}\right)-\left(\frac{{\mathrm{e}}^{-\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}\right)$$
35		efsub	$$⊢\left(\frac{A}{2}\in ℂ\wedge -\frac{A}{2}\in ℂ\right)\to {\mathrm{e}}^{\left(\frac{A}{2}\right)-\left(-\frac{A}{2}\right)}=\frac{{\mathrm{e}}^{\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}$$
36	1 25 35	syl2anc	$$⊢A\in ℂ\to {\mathrm{e}}^{\left(\frac{A}{2}\right)-\left(-\frac{A}{2}\right)}=\frac{{\mathrm{e}}^{\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}$$
37	1 1	subnegd	$$⊢A\in ℂ\to \left(\frac{A}{2}\right)-\left(-\frac{A}{2}\right)=\left(\frac{A}{2}\right)+\left(\frac{A}{2}\right)$$
38		2halves	$$⊢A\in ℂ\to \left(\frac{A}{2}\right)+\left(\frac{A}{2}\right)=A$$
39	37 38	eqtrd	$$⊢A\in ℂ\to \left(\frac{A}{2}\right)-\left(-\frac{A}{2}\right)=A$$
40	39	fveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{\left(\frac{A}{2}\right)-\left(-\frac{A}{2}\right)}={\mathrm{e}}^A$$
41	36 40	eqtr3d	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^{\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}={\mathrm{e}}^A$$
42	26 33	dividd	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^{-\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}=1$$
43	41 42	oveq12d	$$⊢A\in ℂ\to \left(\frac{{\mathrm{e}}^{\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}\right)-\left(\frac{{\mathrm{e}}^{-\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}\right)={\mathrm{e}}^A-1$$
44	34 43	eqtrd	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}={\mathrm{e}}^A-1$$
45	44	eqeq1d	$$⊢A\in ℂ\to \left(\frac{{\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}=0\leftrightarrow {\mathrm{e}}^A-1=0\right)$$
46	27 26 33	diveq0ad	$$⊢A\in ℂ\to \left(\frac{{\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}=0\leftrightarrow {\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}=0\right)$$
47		efcl	$$⊢A\in ℂ\to {\mathrm{e}}^A\in ℂ$$
48		ax-1cn	$$⊢1\in ℂ$$
49		subeq0	$$⊢\left({\mathrm{e}}^A\in ℂ\wedge 1\in ℂ\right)\to \left({\mathrm{e}}^A-1=0\leftrightarrow {\mathrm{e}}^A=1\right)$$
50	47 48 49	sylancl	$$⊢A\in ℂ\to \left({\mathrm{e}}^A-1=0\leftrightarrow {\mathrm{e}}^A=1\right)$$
51	45 46 50	3bitr3d	$$⊢A\in ℂ\to \left({\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}=0\leftrightarrow {\mathrm{e}}^A=1\right)$$
52	23 32 51	3bitrd	$$⊢A\in ℂ\to \left(\sin \left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=0\leftrightarrow {\mathrm{e}}^A=1\right)$$
53		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
54	2 3	pm3.2i	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\right)$$
55		divdiv32	$$⊢\left(A\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\right)\right)\to \frac{\frac{A}{2}}{\mathrm{i}}=\frac{\frac{A}{\mathrm{i}}}{2}$$
56	53 54 55	mp3an23	$$⊢A\in ℂ\to \frac{\frac{A}{2}}{\mathrm{i}}=\frac{\frac{A}{\mathrm{i}}}{2}$$
57	56	oveq1d	$$⊢A\in ℂ\to \frac{\frac{\frac{A}{2}}{\mathrm{i}}}{\mathrm{\pi }}=\frac{\frac{\frac{A}{\mathrm{i}}}{2}}{\mathrm{\pi }}$$
58		divcl	$$⊢\left(A\in ℂ\wedge \mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\right)\to \frac{A}{\mathrm{i}}\in ℂ$$
59	2 3 58	mp3an23	$$⊢A\in ℂ\to \frac{A}{\mathrm{i}}\in ℂ$$
60		picn	$$⊢\mathrm{\pi }\in ℂ$$
61		pine0	$$⊢\mathrm{\pi }\ne 0$$
62	60 61	pm3.2i	$$⊢\left(\mathrm{\pi }\in ℂ\wedge \mathrm{\pi }\ne 0\right)$$
63		divdiv1	$$⊢\left(\frac{A}{\mathrm{i}}\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(\mathrm{\pi }\in ℂ\wedge \mathrm{\pi }\ne 0\right)\right)\to \frac{\frac{\frac{A}{\mathrm{i}}}{2}}{\mathrm{\pi }}=\frac{\frac{A}{\mathrm{i}}}{2\mathrm{\pi }}$$
64	53 62 63	mp3an23	$$⊢\frac{A}{\mathrm{i}}\in ℂ\to \frac{\frac{\frac{A}{\mathrm{i}}}{2}}{\mathrm{\pi }}=\frac{\frac{A}{\mathrm{i}}}{2\mathrm{\pi }}$$
65	59 64	syl	$$⊢A\in ℂ\to \frac{\frac{\frac{A}{\mathrm{i}}}{2}}{\mathrm{\pi }}=\frac{\frac{A}{\mathrm{i}}}{2\mathrm{\pi }}$$
66		2picn	$$⊢2\mathrm{\pi }\in ℂ$$
67		2cn	$$⊢2\in ℂ$$
68		2ne0	$$⊢2\ne 0$$
69	67 60 68 61	mulne0i	$$⊢2\mathrm{\pi }\ne 0$$
70	66 69	pm3.2i	$$⊢\left(2\mathrm{\pi }\in ℂ\wedge 2\mathrm{\pi }\ne 0\right)$$
71		divdiv1	$$⊢\left(A\in ℂ\wedge \left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\right)\wedge \left(2\mathrm{\pi }\in ℂ\wedge 2\mathrm{\pi }\ne 0\right)\right)\to \frac{\frac{A}{\mathrm{i}}}{2\mathrm{\pi }}=\frac{A}{\mathrm{i}2\mathrm{\pi }}$$
72	54 70 71	mp3an23	$$⊢A\in ℂ\to \frac{\frac{A}{\mathrm{i}}}{2\mathrm{\pi }}=\frac{A}{\mathrm{i}2\mathrm{\pi }}$$
73	65 72	eqtrd	$$⊢A\in ℂ\to \frac{\frac{\frac{A}{\mathrm{i}}}{2}}{\mathrm{\pi }}=\frac{A}{\mathrm{i}2\mathrm{\pi }}$$
74	57 73	eqtrd	$$⊢A\in ℂ\to \frac{\frac{\frac{A}{2}}{\mathrm{i}}}{\mathrm{\pi }}=\frac{A}{\mathrm{i}2\mathrm{\pi }}$$
75	74	eleq1d	$$⊢A\in ℂ\to \left(\frac{\frac{\frac{A}{2}}{\mathrm{i}}}{\mathrm{\pi }}\in \mathbb{Z}\leftrightarrow \frac{A}{\mathrm{i}2\mathrm{\pi }}\in \mathbb{Z}\right)$$
76	8 52 75	3bitr3d	$$⊢A\in ℂ\to \left({\mathrm{e}}^A=1\leftrightarrow \frac{A}{\mathrm{i}2\mathrm{\pi }}\in \mathbb{Z}\right)$$