Theorem angpieqvdlem2

Description: Equivalence used in angpieqvd . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	angpieqvd.angdef	|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
	angpieqvd.A	|- ( ph -> A e. CC )
	angpieqvd.B	|- ( ph -> B e. CC )
	angpieqvd.C	|- ( ph -> C e. CC )
	angpieqvd.AneB	|- ( ph -> A =/= B )
	angpieqvd.BneC	|- ( ph -> B =/= C )
Assertion	angpieqvdlem2	|- ( ph -> ( -u ( ( C - B ) / ( A - B ) ) e. RR+ <-> ( ( A - B ) F ( C - B ) ) = _pi ) )

Proof

Step	Hyp	Ref	Expression
1		angpieqvd.angdef	|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2		angpieqvd.A	|- ( ph -> A e. CC )
3		angpieqvd.B	|- ( ph -> B e. CC )
4		angpieqvd.C	|- ( ph -> C e. CC )
5		angpieqvd.AneB	|- ( ph -> A =/= B )
6		angpieqvd.BneC	|- ( ph -> B =/= C )
7	4 3	subcld	|- ( ph -> ( C - B ) e. CC )
8	2 3	subcld	|- ( ph -> ( A - B ) e. CC )
9	2 3 5	subne0d	|- ( ph -> ( A - B ) =/= 0 )
10	7 8 9	divcld	|- ( ph -> ( ( C - B ) / ( A - B ) ) e. CC )
11	6	necomd	|- ( ph -> C =/= B )
12	4 3 11	subne0d	|- ( ph -> ( C - B ) =/= 0 )
13	7 8 12 9	divne0d	|- ( ph -> ( ( C - B ) / ( A - B ) ) =/= 0 )
14		lognegb	|- ( ( ( ( C - B ) / ( A - B ) ) e. CC /\ ( ( C - B ) / ( A - B ) ) =/= 0 ) -> ( -u ( ( C - B ) / ( A - B ) ) e. RR+ <-> ( Im ` ( log ` ( ( C - B ) / ( A - B ) ) ) ) = _pi ) )
15	10 13 14	syl2anc	|- ( ph -> ( -u ( ( C - B ) / ( A - B ) ) e. RR+ <-> ( Im ` ( log ` ( ( C - B ) / ( A - B ) ) ) ) = _pi ) )
16	1 8 9 7 12	angvald	|- ( ph -> ( ( A - B ) F ( C - B ) ) = ( Im ` ( log ` ( ( C - B ) / ( A - B ) ) ) ) )
17	16	eqeq1d	|- ( ph -> ( ( ( A - B ) F ( C - B ) ) = _pi <-> ( Im ` ( log ` ( ( C - B ) / ( A - B ) ) ) ) = _pi ) )
18	15 17	bitr4d	|- ( ph -> ( -u ( ( C - B ) / ( A - B ) ) e. RR+ <-> ( ( A - B ) F ( C - B ) ) = _pi ) )