Theorem angvald

Description: The (signed) angle between two vectors is the argument of their quotient. Deduction form of angval . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	ang.1	$$⊢F=\left(x\in \left(ℂ\setminus \left\{0\right\}\right),y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\Im \left(\log \left(\frac{y}{x}\right)\right)\right)$$
	angvald.1	$$⊢\phi \to X\in ℂ$$
	angvald.2	$$⊢\phi \to X\ne 0$$
	angvald.3	$$⊢\phi \to Y\in ℂ$$
	angvald.4	$$⊢\phi \to Y\ne 0$$
Assertion	angvald	$$⊢\phi \to XFY=\Im \left(\log \left(\frac{Y}{X}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ang.1	$$⊢F=\left(x\in \left(ℂ\setminus \left\{0\right\}\right),y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\Im \left(\log \left(\frac{y}{x}\right)\right)\right)$$
2		angvald.1	$$⊢\phi \to X\in ℂ$$
3		angvald.2	$$⊢\phi \to X\ne 0$$
4		angvald.3	$$⊢\phi \to Y\in ℂ$$
5		angvald.4	$$⊢\phi \to Y\ne 0$$
6	1	angval	$$⊢\left(\left(X\in ℂ\wedge X\ne 0\right)\wedge \left(Y\in ℂ\wedge Y\ne 0\right)\right)\to XFY=\Im \left(\log \left(\frac{Y}{X}\right)\right)$$
7	2 3 4 5 6	syl22anc	$$⊢\phi \to XFY=\Im \left(\log \left(\frac{Y}{X}\right)\right)$$