Theorem angval

Description: Define the angle function, which takes two complex numbers, treated as vectors from the origin, and returns the angle between them, in the range ( -pi , pi ] . To convert from the geometry notation, m A B C , the measure of the angle with legs A B , C B where C is more counterclockwise for positive angles, is represented by ( ( C - B ) F ( A - B ) ) . (Contributed by Mario Carneiro, 23-Sep-2014)

	Ref	Expression
Hypothesis	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)$$
Assertion	angval	$$⊢\left(\left(A\in ℂ\wedge A\ne 0\right)\wedge \left(B\in ℂ\wedge B\ne 0\right)\right)\to AFB=\Im \left(\log \left(\frac{B}{A}\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		eldifsn	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(A\in ℂ\wedge A\ne 0\right)$$
3		eldifsn	$$⊢B\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(B\in ℂ\wedge B\ne 0\right)$$
4		oveq12	$$⊢\left(y=B\wedge x=A\right)\to \frac{y}{x}=\frac{B}{A}$$
5	4	ancoms	$$⊢\left(x=A\wedge y=B\right)\to \frac{y}{x}=\frac{B}{A}$$
6	5	fveq2d	$$⊢\left(x=A\wedge y=B\right)\to \log \left(\frac{y}{x}\right)=\log \left(\frac{B}{A}\right)$$
7	6	fveq2d	$$⊢\left(x=A\wedge y=B\right)\to \Im \left(\log \left(\frac{y}{x}\right)\right)=\Im \left(\log \left(\frac{B}{A}\right)\right)$$
8		fvex	$$⊢\Im \left(\log \left(\frac{B}{A}\right)\right)\in \mathrm{V}$$
9	7 1 8	ovmpoa	$$⊢\left(A\in \left(ℂ\setminus \left\{0\right\}\right)\wedge B\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to AFB=\Im \left(\log \left(\frac{B}{A}\right)\right)$$
10	2 3 9	syl2anbr	$$⊢\left(\left(A\in ℂ\wedge A\ne 0\right)\wedge \left(B\in ℂ\wedge B\ne 0\right)\right)\to AFB=\Im \left(\log \left(\frac{B}{A}\right)\right)$$