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		efcl	$$⊢\frac{A}{2}\in ℂ\to {\mathrm{e}}^{\frac{A}{2}}\in ℂ$$
25	1 24	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{\frac{A}{2}}\in ℂ$$
26	1	negcld	$$⊢A\in ℂ\to -\frac{A}{2}\in ℂ$$
27		efcl	$$⊢-\frac{A}{2}\in ℂ\to {\mathrm{e}}^{-\frac{A}{2}}\in ℂ$$
28	26 27	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{-\frac{A}{2}}\in ℂ$$
29	25 28	subcld	$$⊢A\in ℂ\to {\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}\in ℂ$$
30		2cn	$$⊢2\in ℂ$$
31	30 2	mulcli	$$⊢2\mathrm{i}\in ℂ$$
32		2ne0	$$⊢2\ne 0$$
33	30 2 32 3	mulne0i	$$⊢2\mathrm{i}\ne 0$$
34		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)$$
35	31 33 34	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)$$
36	29 35	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)$$
37		efne0	$$⊢-\frac{A}{2}\in ℂ\to {\mathrm{e}}^{-\frac{A}{2}}\ne 0$$
38	26 37	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{-\frac{A}{2}}\ne 0$$
39	25 28 28 38	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)$$
40		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}}}$$
41	1 26 40	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}}}$$
42	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)$$
43		2halves	$$⊢A\in ℂ\to \left(\frac{A}{2}\right)+\left(\frac{A}{2}\right)=A$$
44	42 43	eqtrd	$$⊢A\in ℂ\to \left(\frac{A}{2}\right)-\left(-\frac{A}{2}\right)=A$$
45	44	fveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{\left(\frac{A}{2}\right)-\left(-\frac{A}{2}\right)}={\mathrm{e}}^A$$
46	41 45	eqtr3d	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^{\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}={\mathrm{e}}^A$$
47	28 38	dividd	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^{-\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}=1$$
48	46 47	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$$
49	39 48	eqtrd	$$⊢A\in ℂ\to \frac{{\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}}{{\mathrm{e}}^{-\frac{A}{2}}}={\mathrm{e}}^A-1$$
50	49	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)$$
51	29 28 38	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)$$
52		efcl	$$⊢A\in ℂ\to {\mathrm{e}}^A\in ℂ$$
53		ax-1cn	$$⊢1\in ℂ$$
54		subeq0	$$⊢\left({\mathrm{e}}^A\in ℂ\wedge 1\in ℂ\right)\to \left({\mathrm{e}}^A-1=0\leftrightarrow {\mathrm{e}}^A=1\right)$$
55	52 53 54	sylancl	$$⊢A\in ℂ\to \left({\mathrm{e}}^A-1=0\leftrightarrow {\mathrm{e}}^A=1\right)$$
56	50 51 55	3bitr3d	$$⊢A\in ℂ\to \left({\mathrm{e}}^{\frac{A}{2}}-{\mathrm{e}}^{-\frac{A}{2}}=0\leftrightarrow {\mathrm{e}}^A=1\right)$$
57	23 36 56	3bitrd	$$⊢A\in ℂ\to \left(\sin \left(\frac{\frac{A}{2}}{\mathrm{i}}\right)=0\leftrightarrow {\mathrm{e}}^A=1\right)$$
58		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
59	2 3	pm3.2i	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\right)$$
60		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}$$
61	58 59 60	mp3an23	$$⊢A\in ℂ\to \frac{\frac{A}{2}}{\mathrm{i}}=\frac{\frac{A}{\mathrm{i}}}{2}$$
62	61	oveq1d	$$⊢A\in ℂ\to \frac{\frac{\frac{A}{2}}{\mathrm{i}}}{\mathrm{\pi }}=\frac{\frac{\frac{A}{\mathrm{i}}}{2}}{\mathrm{\pi }}$$
63		divcl	$$⊢\left(A\in ℂ\wedge \mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\right)\to \frac{A}{\mathrm{i}}\in ℂ$$
64	2 3 63	mp3an23	$$⊢A\in ℂ\to \frac{A}{\mathrm{i}}\in ℂ$$
65		picn	$$⊢\mathrm{\pi }\in ℂ$$
66		pire	$$⊢\mathrm{\pi }\in ℝ$$
67		pipos	$$⊢0<\mathrm{\pi }$$
68	66 67	gt0ne0ii	$$⊢\mathrm{\pi }\ne 0$$
69	65 68	pm3.2i	$$⊢\left(\mathrm{\pi }\in ℂ\wedge \mathrm{\pi }\ne 0\right)$$
70		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 }}$$
71	58 69 70	mp3an23	$$⊢\frac{A}{\mathrm{i}}\in ℂ\to \frac{\frac{\frac{A}{\mathrm{i}}}{2}}{\mathrm{\pi }}=\frac{\frac{A}{\mathrm{i}}}{2\mathrm{\pi }}$$
72	64 71	syl	$$⊢A\in ℂ\to \frac{\frac{\frac{A}{\mathrm{i}}}{2}}{\mathrm{\pi }}=\frac{\frac{A}{\mathrm{i}}}{2\mathrm{\pi }}$$
73	30 65	mulcli	$$⊢2\mathrm{\pi }\in ℂ$$
74	30 65 32 68	mulne0i	$$⊢2\mathrm{\pi }\ne 0$$
75	73 74	pm3.2i	$$⊢\left(2\mathrm{\pi }\in ℂ\wedge 2\mathrm{\pi }\ne 0\right)$$
76		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 }}$$
77	59 75 76	mp3an23	$$⊢A\in ℂ\to \frac{\frac{A}{\mathrm{i}}}{2\mathrm{\pi }}=\frac{A}{\mathrm{i}2\mathrm{\pi }}$$
78	72 77	eqtrd	$$⊢A\in ℂ\to \frac{\frac{\frac{A}{\mathrm{i}}}{2}}{\mathrm{\pi }}=\frac{A}{\mathrm{i}2\mathrm{\pi }}$$
79	62 78	eqtrd	$$⊢A\in ℂ\to \frac{\frac{\frac{A}{2}}{\mathrm{i}}}{\mathrm{\pi }}=\frac{A}{\mathrm{i}2\mathrm{\pi }}$$
80	79	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)$$
81	8 57 80	3bitr3d	$$⊢A\in ℂ\to \left({\mathrm{e}}^A=1\leftrightarrow \frac{A}{\mathrm{i}2\mathrm{\pi }}\in \mathbb{Z}\right)$$