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 = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
	angcld.1	|- ( ph -> X e. CC )
	angcld.2	|- ( ph -> X =/= 0 )
	angcld.3	|- ( ph -> Y e. CC )
	angcld.4	|- ( ph -> Y =/= 0 )
Assertion	angcld	|- ( ph -> ( X F Y ) e. ( -u _pi (,] _pi ) )

Proof

Step	Hyp	Ref	Expression
1		ang.1	|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2		angcld.1	|- ( ph -> X e. CC )
3		angcld.2	|- ( ph -> X =/= 0 )
4		angcld.3	|- ( ph -> Y e. CC )
5		angcld.4	|- ( ph -> Y =/= 0 )
6	1 2 3 4 5	angvald	|- ( ph -> ( X F Y ) = ( Im ` ( log ` ( Y / X ) ) ) )
7	4 2 3	divcld	|- ( ph -> ( Y / X ) e. CC )
8	4 2 5 3	divne0d	|- ( ph -> ( Y / X ) =/= 0 )
9	7 8	logimclad	|- ( ph -> ( Im ` ( log ` ( Y / X ) ) ) e. ( -u _pi (,] _pi ) )
10	6 9	eqeltrd	|- ( ph -> ( X F Y ) e. ( -u _pi (,] _pi ) )