angrteqvd

Description: Two vectors are at a right angle iff their quotient is purely imaginary. (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	ang.1	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
	angrteqvd.1	$⊢ φ \to X \in ℂ$
	angrteqvd.2	$⊢ φ \to X \neq 0$
	angrteqvd.3	$⊢ φ \to Y \in ℂ$
	angrteqvd.4	$⊢ φ \to Y \neq 0$
Assertion	angrteqvd	$⊢ φ \to (X F Y \in \{\frac{π}{2}, - \frac{π}{2}\} \leftrightarrow ℜ (\frac{Y}{X}) = 0)$

Step	Hyp	Ref	Expression
1		ang.1	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
2		angrteqvd.1	$⊢ φ \to X \in ℂ$
3		angrteqvd.2	$⊢ φ \to X \neq 0$
4		angrteqvd.3	$⊢ φ \to Y \in ℂ$
5		angrteqvd.4	$⊢ φ \to Y \neq 0$
6	1 2 3 4 5	angvald	$⊢ φ \to X F Y = ℑ (\log (\frac{Y}{X}))$
7	6	eleq1d	$⊢ φ \to (X F Y \in \{\frac{π}{2}, - \frac{π}{2}\} \leftrightarrow ℑ (\log (\frac{Y}{X})) \in \{\frac{π}{2}, - \frac{π}{2}\})$
8	4 2 3	divcld	$⊢ φ \to \frac{Y}{X} \in ℂ$
9	4 2 5 3	divne0d	$⊢ φ \to \frac{Y}{X} \neq 0$
10	8 9	logimclad	$⊢ φ \to ℑ (\log (\frac{Y}{X})) \in (- π, π]$
11		coseq0negpitopi	$⊢ ℑ (\log (\frac{Y}{X})) \in (- π, π] \to (\cos ℑ (\log (\frac{Y}{X})) = 0 \leftrightarrow ℑ (\log (\frac{Y}{X})) \in \{\frac{π}{2}, - \frac{π}{2}\})$
12	10 11	syl	$⊢ φ \to (\cos ℑ (\log (\frac{Y}{X})) = 0 \leftrightarrow ℑ (\log (\frac{Y}{X})) \in \{\frac{π}{2}, - \frac{π}{2}\})$
13	8 9	cosarg0d	$⊢ φ \to (\cos ℑ (\log (\frac{Y}{X})) = 0 \leftrightarrow ℜ (\frac{Y}{X}) = 0)$
14	7 12 13	3bitr2d	$⊢ φ \to (X F Y \in \{\frac{π}{2}, - \frac{π}{2}\} \leftrightarrow ℜ (\frac{Y}{X}) = 0)$

Metamath Proof Explorer