Theorem angcld

Description: The (signed) angle between two vectors is in ( -upi (,] pi ) . Deduction form. (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)$$
	angcld.1	$$⊢\phi \to X\in ℂ$$
	angcld.2	$$⊢\phi \to X\ne 0$$
	angcld.3	$$⊢\phi \to Y\in ℂ$$
	angcld.4	$$⊢\phi \to Y\ne 0$$
Assertion	angcld	$$⊢\phi \to XFY\in \left(-\mathrm{\pi },\mathrm{\pi }\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		angcld.1	$$⊢\phi \to X\in ℂ$$
3		angcld.2	$$⊢\phi \to X\ne 0$$
4		angcld.3	$$⊢\phi \to Y\in ℂ$$
5		angcld.4	$$⊢\phi \to Y\ne 0$$
6	1 2 3 4 5	angvald	$$⊢\phi \to XFY=\Im \left(\log \left(\frac{Y}{X}\right)\right)$$
7	4 2 3	divcld	$$⊢\phi \to \frac{Y}{X}\in ℂ$$
8	4 2 5 3	divne0d	$$⊢\phi \to \frac{Y}{X}\ne 0$$
9	7 8	logimclad	$$⊢\phi \to \Im \left(\log \left(\frac{Y}{X}\right)\right)\in \left(-\mathrm{\pi },\mathrm{\pi }\right]$$
10	6 9	eqeltrd	$$⊢\phi \to XFY\in \left(-\mathrm{\pi },\mathrm{\pi }\right]$$