This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ∈ ℤ ) )