Theorem coseq1

Description: A complex number whose cosine is one is an integer multiple of 2 _pi . (Contributed by Mario Carneiro, 12-May-2014)

	Ref	Expression
Assertion	coseq1	$$⊢A\in ℂ\to \left(\cos A=1\leftrightarrow \frac{A}{2\mathrm{\pi }}\in \mathbb{Z}\right)$$

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2		2ne0	$$⊢2\ne 0$$
3		divcan2	$$⊢\left(A\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to 2\left(\frac{A}{2}\right)=A$$
4	1 2 3	mp3an23	$$⊢A\in ℂ\to 2\left(\frac{A}{2}\right)=A$$
5	4	fveq2d	$$⊢A\in ℂ\to \cos 2\left(\frac{A}{2}\right)=\cos A$$
6		halfcl	$$⊢A\in ℂ\to \frac{A}{2}\in ℂ$$
7		cos2tsin	$$⊢\frac{A}{2}\in ℂ\to \cos 2\left(\frac{A}{2}\right)=1-2{\sin \left(\frac{A}{2}\right)}^2$$
8	6 7	syl	$$⊢A\in ℂ\to \cos 2\left(\frac{A}{2}\right)=1-2{\sin \left(\frac{A}{2}\right)}^2$$
9	5 8	eqtr3d	$$⊢A\in ℂ\to \cos A=1-2{\sin \left(\frac{A}{2}\right)}^2$$
10	9	eqeq1d	$$⊢A\in ℂ\to \left(\cos A=1\leftrightarrow 1-2{\sin \left(\frac{A}{2}\right)}^2=1\right)$$
11	6	sincld	$$⊢A\in ℂ\to \sin \left(\frac{A}{2}\right)\in ℂ$$
12	11	sqcld	$$⊢A\in ℂ\to {\sin \left(\frac{A}{2}\right)}^2\in ℂ$$
13		mulcl	$$⊢\left(2\in ℂ\wedge {\sin \left(\frac{A}{2}\right)}^2\in ℂ\right)\to 2{\sin \left(\frac{A}{2}\right)}^2\in ℂ$$
14	1 12 13	sylancr	$$⊢A\in ℂ\to 2{\sin \left(\frac{A}{2}\right)}^2\in ℂ$$
15		ax-1cn	$$⊢1\in ℂ$$
16		subsub23	$$⊢\left(1\in ℂ\wedge 2{\sin \left(\frac{A}{2}\right)}^2\in ℂ\wedge 1\in ℂ\right)\to \left(1-2{\sin \left(\frac{A}{2}\right)}^2=1\leftrightarrow 1-1=2{\sin \left(\frac{A}{2}\right)}^2\right)$$
17	15 15 16	mp3an13	$$⊢2{\sin \left(\frac{A}{2}\right)}^2\in ℂ\to \left(1-2{\sin \left(\frac{A}{2}\right)}^2=1\leftrightarrow 1-1=2{\sin \left(\frac{A}{2}\right)}^2\right)$$
18	14 17	syl	$$⊢A\in ℂ\to \left(1-2{\sin \left(\frac{A}{2}\right)}^2=1\leftrightarrow 1-1=2{\sin \left(\frac{A}{2}\right)}^2\right)$$
19		eqcom	$$⊢1-1=2{\sin \left(\frac{A}{2}\right)}^2\leftrightarrow 2{\sin \left(\frac{A}{2}\right)}^2=1-1$$
20		1m1e0	$$⊢1-1=0$$
21	20	eqeq2i	$$⊢2{\sin \left(\frac{A}{2}\right)}^2=1-1\leftrightarrow 2{\sin \left(\frac{A}{2}\right)}^2=0$$
22	19 21	bitri	$$⊢1-1=2{\sin \left(\frac{A}{2}\right)}^2\leftrightarrow 2{\sin \left(\frac{A}{2}\right)}^2=0$$
23	18 22	bitrdi	$$⊢A\in ℂ\to \left(1-2{\sin \left(\frac{A}{2}\right)}^2=1\leftrightarrow 2{\sin \left(\frac{A}{2}\right)}^2=0\right)$$
24	10 23	bitrd	$$⊢A\in ℂ\to \left(\cos A=1\leftrightarrow 2{\sin \left(\frac{A}{2}\right)}^2=0\right)$$
25		mul0or	$$⊢\left(2\in ℂ\wedge {\sin \left(\frac{A}{2}\right)}^2\in ℂ\right)\to \left(2{\sin \left(\frac{A}{2}\right)}^2=0\leftrightarrow \left(2=0\vee {\sin \left(\frac{A}{2}\right)}^2=0\right)\right)$$
26	1 12 25	sylancr	$$⊢A\in ℂ\to \left(2{\sin \left(\frac{A}{2}\right)}^2=0\leftrightarrow \left(2=0\vee {\sin \left(\frac{A}{2}\right)}^2=0\right)\right)$$
27	2	neii	$$⊢\neg 2=0$$
28		biorf	$$⊢\neg 2=0\to \left({\sin \left(\frac{A}{2}\right)}^2=0\leftrightarrow \left(2=0\vee {\sin \left(\frac{A}{2}\right)}^2=0\right)\right)$$
29	27 28	ax-mp	$$⊢{\sin \left(\frac{A}{2}\right)}^2=0\leftrightarrow \left(2=0\vee {\sin \left(\frac{A}{2}\right)}^2=0\right)$$
30	26 29	bitr4di	$$⊢A\in ℂ\to \left(2{\sin \left(\frac{A}{2}\right)}^2=0\leftrightarrow {\sin \left(\frac{A}{2}\right)}^2=0\right)$$
31		sqeq0	$$⊢\sin \left(\frac{A}{2}\right)\in ℂ\to \left({\sin \left(\frac{A}{2}\right)}^2=0\leftrightarrow \sin \left(\frac{A}{2}\right)=0\right)$$
32	11 31	syl	$$⊢A\in ℂ\to \left({\sin \left(\frac{A}{2}\right)}^2=0\leftrightarrow \sin \left(\frac{A}{2}\right)=0\right)$$
33	24 30 32	3bitrd	$$⊢A\in ℂ\to \left(\cos A=1\leftrightarrow \sin \left(\frac{A}{2}\right)=0\right)$$
34		sineq0	$$⊢\frac{A}{2}\in ℂ\to \left(\sin \left(\frac{A}{2}\right)=0\leftrightarrow \frac{\frac{A}{2}}{\mathrm{\pi }}\in \mathbb{Z}\right)$$
35	6 34	syl	$$⊢A\in ℂ\to \left(\sin \left(\frac{A}{2}\right)=0\leftrightarrow \frac{\frac{A}{2}}{\mathrm{\pi }}\in \mathbb{Z}\right)$$
36	1 2	pm3.2i	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
37		picn	$$⊢\mathrm{\pi }\in ℂ$$
38		pire	$$⊢\mathrm{\pi }\in ℝ$$
39		pipos	$$⊢0<\mathrm{\pi }$$
40	38 39	gt0ne0ii	$$⊢\mathrm{\pi }\ne 0$$
41	37 40	pm3.2i	$$⊢\left(\mathrm{\pi }\in ℂ\wedge \mathrm{\pi }\ne 0\right)$$
42		divdiv1	$$⊢\left(A\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{A}{2}}{\mathrm{\pi }}=\frac{A}{2\mathrm{\pi }}$$
43	36 41 42	mp3an23	$$⊢A\in ℂ\to \frac{\frac{A}{2}}{\mathrm{\pi }}=\frac{A}{2\mathrm{\pi }}$$
44	43	eleq1d	$$⊢A\in ℂ\to \left(\frac{\frac{A}{2}}{\mathrm{\pi }}\in \mathbb{Z}\leftrightarrow \frac{A}{2\mathrm{\pi }}\in \mathbb{Z}\right)$$
45	33 35 44	3bitrd	$$⊢A\in ℂ\to \left(\cos A=1\leftrightarrow \frac{A}{2\mathrm{\pi }}\in \mathbb{Z}\right)$$