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 ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
Assertion ang180lem5 ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( ( 𝐴 − 𝐵 ) 𝐹 𝐴 ) + ( 𝐵 𝐹 ( 𝐵 − 𝐴 ) ) ) + ( 𝐴 𝐹 𝐵 ) ) ∈ { - π , π } )

Proof

Step Hyp Ref Expression
1 ang.1 ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2 simp1l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ ℂ )
3 1cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → 1 ∈ ℂ )
4 simp2l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ ℂ )
5 simp1r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 0 )
6 4 2 5 divcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 / 𝐴 ) ∈ ℂ )
7 2 3 6 subdid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 · ( 1 − ( 𝐵 / 𝐴 ) ) ) = ( ( 𝐴 · 1 ) − ( 𝐴 · ( 𝐵 / 𝐴 ) ) ) )
8 2 mulridd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 · 1 ) = 𝐴 )
9 4 2 5 divcan2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 · ( 𝐵 / 𝐴 ) ) = 𝐵 )
10 8 9 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 · 1 ) − ( 𝐴 · ( 𝐵 / 𝐴 ) ) ) = ( 𝐴 − 𝐵 ) )
11 7 10 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 · ( 1 − ( 𝐵 / 𝐴 ) ) ) = ( 𝐴 − 𝐵 ) )
12 11 8 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 · ( 1 − ( 𝐵 / 𝐴 ) ) ) 𝐹 ( 𝐴 · 1 ) ) = ( ( 𝐴 − 𝐵 ) 𝐹 𝐴 ) )
13 3 6 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( 1 − ( 𝐵 / 𝐴 ) ) ∈ ℂ )
14 simp3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
15 14 necomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ≠ 𝐴 )
16 4 2 5 15 divne1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 / 𝐴 ) ≠ 1 )
17 16 necomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → 1 ≠ ( 𝐵 / 𝐴 ) )
18 3 6 17 subne0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( 1 − ( 𝐵 / 𝐴 ) ) ≠ 0 )
19 ax-1ne0 ⊢ 1 ≠ 0
20 19 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → 1 ≠ 0 )
21 1 angcan ⊢ ( ( ( ( 1 − ( 𝐵 / 𝐴 ) ) ∈ ℂ ∧ ( 1 − ( 𝐵 / 𝐴 ) ) ≠ 0 ) ∧ ( 1 ∈ ℂ ∧ 1 ≠ 0 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( 𝐴 · ( 1 − ( 𝐵 / 𝐴 ) ) ) 𝐹 ( 𝐴 · 1 ) ) = ( ( 1 − ( 𝐵 / 𝐴 ) ) 𝐹 1 ) )
22 13 18 3 20 2 5 21 syl222anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 · ( 1 − ( 𝐵 / 𝐴 ) ) ) 𝐹 ( 𝐴 · 1 ) ) = ( ( 1 − ( 𝐵 / 𝐴 ) ) 𝐹 1 ) )
23 12 22 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 − 𝐵 ) 𝐹 𝐴 ) = ( ( 1 − ( 𝐵 / 𝐴 ) ) 𝐹 1 ) )
24 2 6 3 subdid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 · ( ( 𝐵 / 𝐴 ) − 1 ) ) = ( ( 𝐴 · ( 𝐵 / 𝐴 ) ) − ( 𝐴 · 1 ) ) )
25 9 8 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 · ( 𝐵 / 𝐴 ) ) − ( 𝐴 · 1 ) ) = ( 𝐵 − 𝐴 ) )
26 24 25 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 · ( ( 𝐵 / 𝐴 ) − 1 ) ) = ( 𝐵 − 𝐴 ) )
27 9 26 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 · ( 𝐵 / 𝐴 ) ) 𝐹 ( 𝐴 · ( ( 𝐵 / 𝐴 ) − 1 ) ) ) = ( 𝐵 𝐹 ( 𝐵 − 𝐴 ) ) )
28 simp2r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ≠ 0 )
29 4 2 28 5 divne0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 / 𝐴 ) ≠ 0 )
30 6 3 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐵 / 𝐴 ) − 1 ) ∈ ℂ )
31 6 3 16 subne0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐵 / 𝐴 ) − 1 ) ≠ 0 )
32 1 angcan ⊢ ( ( ( ( 𝐵 / 𝐴 ) ∈ ℂ ∧ ( 𝐵 / 𝐴 ) ≠ 0 ) ∧ ( ( ( 𝐵 / 𝐴 ) − 1 ) ∈ ℂ ∧ ( ( 𝐵 / 𝐴 ) − 1 ) ≠ 0 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( 𝐴 · ( 𝐵 / 𝐴 ) ) 𝐹 ( 𝐴 · ( ( 𝐵 / 𝐴 ) − 1 ) ) ) = ( ( 𝐵 / 𝐴 ) 𝐹 ( ( 𝐵 / 𝐴 ) − 1 ) ) )
33 6 29 30 31 2 5 32 syl222anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 · ( 𝐵 / 𝐴 ) ) 𝐹 ( 𝐴 · ( ( 𝐵 / 𝐴 ) − 1 ) ) ) = ( ( 𝐵 / 𝐴 ) 𝐹 ( ( 𝐵 / 𝐴 ) − 1 ) ) )
34 27 33 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐵 𝐹 ( 𝐵 − 𝐴 ) ) = ( ( 𝐵 / 𝐴 ) 𝐹 ( ( 𝐵 / 𝐴 ) − 1 ) ) )
35 23 34 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐴 − 𝐵 ) 𝐹 𝐴 ) + ( 𝐵 𝐹 ( 𝐵 − 𝐴 ) ) ) = ( ( ( 1 − ( 𝐵 / 𝐴 ) ) 𝐹 1 ) + ( ( 𝐵 / 𝐴 ) 𝐹 ( ( 𝐵 / 𝐴 ) − 1 ) ) ) )
36 8 9 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 · 1 ) 𝐹 ( 𝐴 · ( 𝐵 / 𝐴 ) ) ) = ( 𝐴 𝐹 𝐵 ) )
37 1 angcan ⊢ ( ( ( 1 ∈ ℂ ∧ 1 ≠ 0 ) ∧ ( ( 𝐵 / 𝐴 ) ∈ ℂ ∧ ( 𝐵 / 𝐴 ) ≠ 0 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( 𝐴 · 1 ) 𝐹 ( 𝐴 · ( 𝐵 / 𝐴 ) ) ) = ( 1 𝐹 ( 𝐵 / 𝐴 ) ) )
38 3 20 6 29 2 5 37 syl222anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝐴 · 1 ) 𝐹 ( 𝐴 · ( 𝐵 / 𝐴 ) ) ) = ( 1 𝐹 ( 𝐵 / 𝐴 ) ) )
39 36 38 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 𝐹 𝐵 ) = ( 1 𝐹 ( 𝐵 / 𝐴 ) ) )
40 35 39 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( ( 𝐴 − 𝐵 ) 𝐹 𝐴 ) + ( 𝐵 𝐹 ( 𝐵 − 𝐴 ) ) ) + ( 𝐴 𝐹 𝐵 ) ) = ( ( ( ( 1 − ( 𝐵 / 𝐴 ) ) 𝐹 1 ) + ( ( 𝐵 / 𝐴 ) 𝐹 ( ( 𝐵 / 𝐴 ) − 1 ) ) ) + ( 1 𝐹 ( 𝐵 / 𝐴 ) ) ) )
41 1 ang180lem4 ⊢ ( ( ( 𝐵 / 𝐴 ) ∈ ℂ ∧ ( 𝐵 / 𝐴 ) ≠ 0 ∧ ( 𝐵 / 𝐴 ) ≠ 1 ) → ( ( ( ( 1 − ( 𝐵 / 𝐴 ) ) 𝐹 1 ) + ( ( 𝐵 / 𝐴 ) 𝐹 ( ( 𝐵 / 𝐴 ) − 1 ) ) ) + ( 1 𝐹 ( 𝐵 / 𝐴 ) ) ) ∈ { - π , π } )
42 6 29 16 41 syl3anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( ( 1 − ( 𝐵 / 𝐴 ) ) 𝐹 1 ) + ( ( 𝐵 / 𝐴 ) 𝐹 ( ( 𝐵 / 𝐴 ) − 1 ) ) ) + ( 1 𝐹 ( 𝐵 / 𝐴 ) ) ) ∈ { - π , π } )
43 40 42 eqeltrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( ( 𝐴 − 𝐵 ) 𝐹 𝐴 ) + ( 𝐵 𝐹 ( 𝐵 − 𝐴 ) ) ) + ( 𝐴 𝐹 𝐵 ) ) ∈ { - π , π } )