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	$⊢ φ \to X \in ℂ$
	cosargd.2	$⊢ φ \to X \neq 0$
Assertion	cosarg0d	$⊢ φ \to (\cos ℑ (\log X) = 0 \leftrightarrow ℜ (X) = 0)$

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

Metamath Proof Explorer