Theorem ang180lem5

Description: Lemma for ang180 : Reduce the statement to two variables. (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	ang180lem5	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( ( ( A - B ) F A ) + ( B F ( B - A ) ) ) + ( A F B ) ) 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		simp1l	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> A e. CC )
3		1cnd	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> 1 e. CC )
4		simp2l	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> B e. CC )
5		simp1r	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> A =/= 0 )
6	4 2 5	divcld	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( B / A ) e. CC )
7	2 3 6	subdid	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( A x. ( 1 - ( B / A ) ) ) = ( ( A x. 1 ) - ( A x. ( B / A ) ) ) )
8	2	mulid1d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( A x. 1 ) = A )
9	4 2 5	divcan2d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( A x. ( B / A ) ) = B )
10	8 9	oveq12d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( A x. 1 ) - ( A x. ( B / A ) ) ) = ( A - B ) )
11	7 10	eqtrd	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( A x. ( 1 - ( B / A ) ) ) = ( A - B ) )
12	11 8	oveq12d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( A x. ( 1 - ( B / A ) ) ) F ( A x. 1 ) ) = ( ( A - B ) F A ) )
13	3 6	subcld	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( 1 - ( B / A ) ) e. CC )
14		simp3	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> A =/= B )
15	14	necomd	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> B =/= A )
16	4 2 5 15	divne1d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( B / A ) =/= 1 )
17	16	necomd	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> 1 =/= ( B / A ) )
18	3 6 17	subne0d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( 1 - ( B / A ) ) =/= 0 )
19		ax-1ne0	|- 1 =/= 0
20	19	a1i	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> 1 =/= 0 )
21	1	angcan	|- ( ( ( ( 1 - ( B / A ) ) e. CC /\ ( 1 - ( B / A ) ) =/= 0 ) /\ ( 1 e. CC /\ 1 =/= 0 ) /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( A x. ( 1 - ( B / A ) ) ) F ( A x. 1 ) ) = ( ( 1 - ( B / A ) ) F 1 ) )
22	13 18 3 20 2 5 21	syl222anc	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( A x. ( 1 - ( B / A ) ) ) F ( A x. 1 ) ) = ( ( 1 - ( B / A ) ) F 1 ) )
23	12 22	eqtr3d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( A - B ) F A ) = ( ( 1 - ( B / A ) ) F 1 ) )
24	2 6 3	subdid	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( A x. ( ( B / A ) - 1 ) ) = ( ( A x. ( B / A ) ) - ( A x. 1 ) ) )
25	9 8	oveq12d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( A x. ( B / A ) ) - ( A x. 1 ) ) = ( B - A ) )
26	24 25	eqtrd	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( A x. ( ( B / A ) - 1 ) ) = ( B - A ) )
27	9 26	oveq12d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( A x. ( B / A ) ) F ( A x. ( ( B / A ) - 1 ) ) ) = ( B F ( B - A ) ) )
28		simp2r	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> B =/= 0 )
29	4 2 28 5	divne0d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( B / A ) =/= 0 )
30	6 3	subcld	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( B / A ) - 1 ) e. CC )
31	6 3 16	subne0d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( B / A ) - 1 ) =/= 0 )
32	1	angcan	|- ( ( ( ( B / A ) e. CC /\ ( B / A ) =/= 0 ) /\ ( ( ( B / A ) - 1 ) e. CC /\ ( ( B / A ) - 1 ) =/= 0 ) /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( A x. ( B / A ) ) F ( A x. ( ( B / A ) - 1 ) ) ) = ( ( B / A ) F ( ( B / A ) - 1 ) ) )
33	6 29 30 31 2 5 32	syl222anc	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( A x. ( B / A ) ) F ( A x. ( ( B / A ) - 1 ) ) ) = ( ( B / A ) F ( ( B / A ) - 1 ) ) )
34	27 33	eqtr3d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( B F ( B - A ) ) = ( ( B / A ) F ( ( B / A ) - 1 ) ) )
35	23 34	oveq12d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( ( A - B ) F A ) + ( B F ( B - A ) ) ) = ( ( ( 1 - ( B / A ) ) F 1 ) + ( ( B / A ) F ( ( B / A ) - 1 ) ) ) )
36	8 9	oveq12d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( A x. 1 ) F ( A x. ( B / A ) ) ) = ( A F B ) )
37	1	angcan	|- ( ( ( 1 e. CC /\ 1 =/= 0 ) /\ ( ( B / A ) e. CC /\ ( B / A ) =/= 0 ) /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( A x. 1 ) F ( A x. ( B / A ) ) ) = ( 1 F ( B / A ) ) )
38	3 20 6 29 2 5 37	syl222anc	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( A x. 1 ) F ( A x. ( B / A ) ) ) = ( 1 F ( B / A ) ) )
39	36 38	eqtr3d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( A F B ) = ( 1 F ( B / A ) ) )
40	35 39	oveq12d	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( ( ( A - B ) F A ) + ( B F ( B - A ) ) ) + ( A F B ) ) = ( ( ( ( 1 - ( B / A ) ) F 1 ) + ( ( B / A ) F ( ( B / A ) - 1 ) ) ) + ( 1 F ( B / A ) ) ) )
41	1	ang180lem4	|- ( ( ( B / A ) e. CC /\ ( B / A ) =/= 0 /\ ( B / A ) =/= 1 ) -> ( ( ( ( 1 - ( B / A ) ) F 1 ) + ( ( B / A ) F ( ( B / A ) - 1 ) ) ) + ( 1 F ( B / A ) ) ) e. { -u _pi , _pi } )
42	6 29 16 41	syl3anc	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( ( ( 1 - ( B / A ) ) F 1 ) + ( ( B / A ) F ( ( B / A ) - 1 ) ) ) + ( 1 F ( B / A ) ) ) e. { -u _pi , _pi } )
43	40 42	eqeltrd	|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ A =/= B ) -> ( ( ( ( A - B ) F A ) + ( B F ( B - A ) ) ) + ( A F B ) ) e. { -u _pi , _pi } )