Metamath Proof Explorer

Theorem coseq0

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

Ref Expression
Assertion coseq0 ⊢ A ∈ ℂ → cos ⁡ A = 0 ↔ A π + 1 2 ∈ ℤ

Proof

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