Metamath Proof Explorer

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 mulridd 
 |-  ( ( ( 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 } )