Theorem cosarg0d

Description: The cosine of the argument is zero precisely on the imaginary axis. (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	cosargd.1	$$⊢\phi \to X\in ℂ$$
	cosargd.2	$$⊢\phi \to X\ne 0$$
Assertion	cosarg0d	$$⊢\phi \to \left(\cos \Im \left(\log X\right)=0\leftrightarrow \Re \left(X\right)=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		cosargd.1	$$⊢\phi \to X\in ℂ$$
2		cosargd.2	$$⊢\phi \to X\ne 0$$
3	1 2	cosargd	$$⊢\phi \to \cos \Im \left(\log X\right)=\frac{\Re \left(X\right)}{\left|X\right|}$$
4	3	eqeq1d	$$⊢\phi \to \left(\cos \Im \left(\log X\right)=0\leftrightarrow \frac{\Re \left(X\right)}{\left|X\right|}=0\right)$$
5	1	recld	$$⊢\phi \to \Re \left(X\right)\in ℝ$$
6	5	recnd	$$⊢\phi \to \Re \left(X\right)\in ℂ$$
7	1	abscld	$$⊢\phi \to \left|X\right|\in ℝ$$
8	7	recnd	$$⊢\phi \to \left|X\right|\in ℂ$$
9	1 2	absne0d	$$⊢\phi \to \left|X\right|\ne 0$$
10	6 8 9	diveq0ad	$$⊢\phi \to \left(\frac{\Re \left(X\right)}{\left|X\right|}=0\leftrightarrow \Re \left(X\right)=0\right)$$
11	4 10	bitrd	$$⊢\phi \to \left(\cos \Im \left(\log X\right)=0\leftrightarrow \Re \left(X\right)=0\right)$$