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 = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
Assertion	angval	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A F B ) = ( Im ` ( log ` ( B / A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ang.1	|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2		eldifsn	|- ( A e. ( CC \ { 0 } ) <-> ( A e. CC /\ A =/= 0 ) )
3		eldifsn	|- ( B e. ( CC \ { 0 } ) <-> ( B e. CC /\ B =/= 0 ) )
4		oveq12	|- ( ( y = B /\ x = A ) -> ( y / x ) = ( B / A ) )
5	4	ancoms	|- ( ( x = A /\ y = B ) -> ( y / x ) = ( B / A ) )
6	5	fveq2d	|- ( ( x = A /\ y = B ) -> ( log ` ( y / x ) ) = ( log ` ( B / A ) ) )
7	6	fveq2d	|- ( ( x = A /\ y = B ) -> ( Im ` ( log ` ( y / x ) ) ) = ( Im ` ( log ` ( B / A ) ) ) )
8		fvex	|- ( Im ` ( log ` ( B / A ) ) ) e. _V
9	7 1 8	ovmpoa	|- ( ( A e. ( CC \ { 0 } ) /\ B e. ( CC \ { 0 } ) ) -> ( A F B ) = ( Im ` ( log ` ( B / A ) ) ) )
10	2 3 9	syl2anbr	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A F B ) = ( Im ` ( log ` ( B / A ) ) ) )