Theorem coseq0

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

	Ref	Expression
Assertion	coseq0	⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) = 0 ↔ ( ( 𝐴 / π ) + ( 1 / 2 ) ) ∈ ℤ ) )

Proof

Step	Hyp	Ref	Expression
1		picn	⊢ π ∈ ℂ
2	1	a1i	⊢ ( 𝐴 ∈ ℂ → π ∈ ℂ )
3	2	halfcld	⊢ ( 𝐴 ∈ ℂ → ( π / 2 ) ∈ ℂ )
4		id	⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
5	3 4	addcld	⊢ ( 𝐴 ∈ ℂ → ( ( π / 2 ) + 𝐴 ) ∈ ℂ )
6		sineq0	⊢ ( ( ( π / 2 ) + 𝐴 ) ∈ ℂ → ( ( sin ‘ ( ( π / 2 ) + 𝐴 ) ) = 0 ↔ ( ( ( π / 2 ) + 𝐴 ) / π ) ∈ ℤ ) )
7	5 6	syl	⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ ( ( π / 2 ) + 𝐴 ) ) = 0 ↔ ( ( ( π / 2 ) + 𝐴 ) / π ) ∈ ℤ ) )
8		sinhalfpip	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( ( π / 2 ) + 𝐴 ) ) = ( cos ‘ 𝐴 ) )
9	8	eqeq1d	⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ ( ( π / 2 ) + 𝐴 ) ) = 0 ↔ ( cos ‘ 𝐴 ) = 0 ) )
10		pire	⊢ π ∈ ℝ
11		pipos	⊢ 0 < π
12	10 11	gt0ne0ii	⊢ π ≠ 0
13	12	a1i	⊢ ( 𝐴 ∈ ℂ → π ≠ 0 )
14	3 4 2 13	divdird	⊢ ( 𝐴 ∈ ℂ → ( ( ( π / 2 ) + 𝐴 ) / π ) = ( ( ( π / 2 ) / π ) + ( 𝐴 / π ) ) )
15		2cnd	⊢ ( 𝐴 ∈ ℂ → 2 ∈ ℂ )
16		2ne0	⊢ 2 ≠ 0
17	16	a1i	⊢ ( 𝐴 ∈ ℂ → 2 ≠ 0 )
18	2 15 2 17 13	divdiv32d	⊢ ( 𝐴 ∈ ℂ → ( ( π / 2 ) / π ) = ( ( π / π ) / 2 ) )
19	2 13	dividd	⊢ ( 𝐴 ∈ ℂ → ( π / π ) = 1 )
20	19	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( π / π ) / 2 ) = ( 1 / 2 ) )
21	18 20	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ( π / 2 ) / π ) = ( 1 / 2 ) )
22	21	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( ( π / 2 ) / π ) + ( 𝐴 / π ) ) = ( ( 1 / 2 ) + ( 𝐴 / π ) ) )
23		1cnd	⊢ ( 𝐴 ∈ ℂ → 1 ∈ ℂ )
24	23	halfcld	⊢ ( 𝐴 ∈ ℂ → ( 1 / 2 ) ∈ ℂ )
25	4 2 13	divcld	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 / π ) ∈ ℂ )
26	24 25	addcomd	⊢ ( 𝐴 ∈ ℂ → ( ( 1 / 2 ) + ( 𝐴 / π ) ) = ( ( 𝐴 / π ) + ( 1 / 2 ) ) )
27	14 22 26	3eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ( ( π / 2 ) + 𝐴 ) / π ) = ( ( 𝐴 / π ) + ( 1 / 2 ) ) )
28	27	eleq1d	⊢ ( 𝐴 ∈ ℂ → ( ( ( ( π / 2 ) + 𝐴 ) / π ) ∈ ℤ ↔ ( ( 𝐴 / π ) + ( 1 / 2 ) ) ∈ ℤ ) )
29	7 9 28	3bitr3d	⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) = 0 ↔ ( ( 𝐴 / π ) + ( 1 / 2 ) ) ∈ ℤ ) )