Theorem angrteqvd

Description: Two vectors are at a right angle iff their quotient is purely imaginary. (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 ) ) ) )
	angrteqvd.1	|- ( ph -> X e. CC )
	angrteqvd.2	|- ( ph -> X =/= 0 )
	angrteqvd.3	|- ( ph -> Y e. CC )
	angrteqvd.4	|- ( ph -> Y =/= 0 )
Assertion	angrteqvd	|- ( ph -> ( ( X F Y ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } <-> ( Re ` ( Y / X ) ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		ang.1	|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2		angrteqvd.1	|- ( ph -> X e. CC )
3		angrteqvd.2	|- ( ph -> X =/= 0 )
4		angrteqvd.3	|- ( ph -> Y e. CC )
5		angrteqvd.4	|- ( ph -> Y =/= 0 )
6	1 2 3 4 5	angvald	|- ( ph -> ( X F Y ) = ( Im ` ( log ` ( Y / X ) ) ) )
7	6	eleq1d	|- ( ph -> ( ( X F Y ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } <-> ( Im ` ( log ` ( Y / X ) ) ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) )
8	4 2 3	divcld	|- ( ph -> ( Y / X ) e. CC )
9	4 2 5 3	divne0d	|- ( ph -> ( Y / X ) =/= 0 )
10	8 9	logimclad	|- ( ph -> ( Im ` ( log ` ( Y / X ) ) ) e. ( -u _pi (,] _pi ) )
11		coseq0negpitopi	|- ( ( Im ` ( log ` ( Y / X ) ) ) e. ( -u _pi (,] _pi ) -> ( ( cos ` ( Im ` ( log ` ( Y / X ) ) ) ) = 0 <-> ( Im ` ( log ` ( Y / X ) ) ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) )
12	10 11	syl	|- ( ph -> ( ( cos ` ( Im ` ( log ` ( Y / X ) ) ) ) = 0 <-> ( Im ` ( log ` ( Y / X ) ) ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) )
13	8 9	cosarg0d	|- ( ph -> ( ( cos ` ( Im ` ( log ` ( Y / X ) ) ) ) = 0 <-> ( Re ` ( Y / X ) ) = 0 ) )
14	7 12 13	3bitr2d	|- ( ph -> ( ( X F Y ) e. { ( _pi / 2 ) , -u ( _pi / 2 ) } <-> ( Re ` ( Y / X ) ) = 0 ) )