Theorem coseq0

Description: A complex number whose cosine is zero. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		picn	$$⊢\mathrm{\pi }\in ℂ$$
2	1	a1i	$$⊢A\in ℂ\to \mathrm{\pi }\in ℂ$$
3	2	halfcld	$$⊢A\in ℂ\to \frac{\mathrm{\pi }}{2}\in ℂ$$
4		id	$$⊢A\in ℂ\to A\in ℂ$$
5	3 4	addcld	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)+A\in ℂ$$
6		sineq0	$$⊢\left(\frac{\mathrm{\pi }}{2}\right)+A\in ℂ\to \left(\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)+A\right)=0\leftrightarrow \frac{\left(\frac{\mathrm{\pi }}{2}\right)+A}{\mathrm{\pi }}\in \mathbb{Z}\right)$$
7	5 6	syl	$$⊢A\in ℂ\to \left(\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)+A\right)=0\leftrightarrow \frac{\left(\frac{\mathrm{\pi }}{2}\right)+A}{\mathrm{\pi }}\in \mathbb{Z}\right)$$
8		sinhalfpip	$$⊢A\in ℂ\to \sin \left(\left(\frac{\mathrm{\pi }}{2}\right)+A\right)=\cos A$$
9	8	eqeq1d	$$⊢A\in ℂ\to \left(\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)+A\right)=0\leftrightarrow \cos A=0\right)$$
10		pire	$$⊢\mathrm{\pi }\in ℝ$$
11		pipos	$$⊢0<\mathrm{\pi }$$
12	10 11	gt0ne0ii	$$⊢\mathrm{\pi }\ne 0$$
13	12	a1i	$$⊢A\in ℂ\to \mathrm{\pi }\ne 0$$
14	3 4 2 13	divdird	$$⊢A\in ℂ\to \frac{\left(\frac{\mathrm{\pi }}{2}\right)+A}{\mathrm{\pi }}=\left(\frac{\frac{\mathrm{\pi }}{2}}{\mathrm{\pi }}\right)+\left(\frac{A}{\mathrm{\pi }}\right)$$
15		2cnd	$$⊢A\in ℂ\to 2\in ℂ$$
16		2ne0	$$⊢2\ne 0$$
17	16	a1i	$$⊢A\in ℂ\to 2\ne 0$$
18	2 15 2 17 13	divdiv32d	$$⊢A\in ℂ\to \frac{\frac{\mathrm{\pi }}{2}}{\mathrm{\pi }}=\frac{\frac{\mathrm{\pi }}{\mathrm{\pi }}}{2}$$
19	2 13	dividd	$$⊢A\in ℂ\to \frac{\mathrm{\pi }}{\mathrm{\pi }}=1$$
20	19	oveq1d	$$⊢A\in ℂ\to \frac{\frac{\mathrm{\pi }}{\mathrm{\pi }}}{2}=\frac{1}{2}$$
21	18 20	eqtrd	$$⊢A\in ℂ\to \frac{\frac{\mathrm{\pi }}{2}}{\mathrm{\pi }}=\frac{1}{2}$$
22	21	oveq1d	$$⊢A\in ℂ\to \left(\frac{\frac{\mathrm{\pi }}{2}}{\mathrm{\pi }}\right)+\left(\frac{A}{\mathrm{\pi }}\right)=\left(\frac{1}{2}\right)+\left(\frac{A}{\mathrm{\pi }}\right)$$
23		1cnd	$$⊢A\in ℂ\to 1\in ℂ$$
24	23	halfcld	$$⊢A\in ℂ\to \frac{1}{2}\in ℂ$$
25	4 2 13	divcld	$$⊢A\in ℂ\to \frac{A}{\mathrm{\pi }}\in ℂ$$
26	24 25	addcomd	$$⊢A\in ℂ\to \left(\frac{1}{2}\right)+\left(\frac{A}{\mathrm{\pi }}\right)=\left(\frac{A}{\mathrm{\pi }}\right)+\left(\frac{1}{2}\right)$$
27	14 22 26	3eqtrd	$$⊢A\in ℂ\to \frac{\left(\frac{\mathrm{\pi }}{2}\right)+A}{\mathrm{\pi }}=\left(\frac{A}{\mathrm{\pi }}\right)+\left(\frac{1}{2}\right)$$
28	27	eleq1d	$$⊢A\in ℂ\to \left(\frac{\left(\frac{\mathrm{\pi }}{2}\right)+A}{\mathrm{\pi }}\in \mathbb{Z}\leftrightarrow \left(\frac{A}{\mathrm{\pi }}\right)+\left(\frac{1}{2}\right)\in \mathbb{Z}\right)$$
29	7 9 28	3bitr3d	$$⊢A\in ℂ\to \left(\cos A=0\leftrightarrow \left(\frac{A}{\mathrm{\pi }}\right)+\left(\frac{1}{2}\right)\in \mathbb{Z}\right)$$