Metamath Proof Explorer

Theorem ang180lem4

Description: Lemma for ang180 . Reduce the statement to one variable. (Contributed by Mario Carneiro, 23-Sep-2014)

Ref Expression
Hypothesis ang.1 ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
Assertion ang180lem4 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( ( 1 − 𝐴 ) 𝐹 1 ) + ( 𝐴 𝐹 ( 𝐴 − 1 ) ) ) + ( 1 𝐹 𝐴 ) ) ∈ { - π , π } )

Proof

Step Hyp Ref Expression
1 ang.1 ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2 1cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 1 ∈ ℂ )
3 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ∈ ℂ )
4 2 3 subcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 − 𝐴 ) ∈ ℂ )
5 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ≠ 1 )
6 5 necomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 1 ≠ 𝐴 )
7 2 3 6 subne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 − 𝐴 ) ≠ 0 )
8 ax-1ne0 ⊢ 1 ≠ 0
9 8 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 1 ≠ 0 )
10 1 4 7 2 9 angvald ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 1 − 𝐴 ) 𝐹 1 ) = ( ℑ ‘ ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ) )
11 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ≠ 0 )
12 3 2 subcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝐴 − 1 ) ∈ ℂ )
13 3 2 5 subne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝐴 − 1 ) ≠ 0 )
14 1 3 11 12 13 angvald ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝐴 𝐹 ( 𝐴 − 1 ) ) = ( ℑ ‘ ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) )
15 10 14 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( 1 − 𝐴 ) 𝐹 1 ) + ( 𝐴 𝐹 ( 𝐴 − 1 ) ) ) = ( ( ℑ ‘ ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ) + ( ℑ ‘ ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) )
16 2 4 7 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 / ( 1 − 𝐴 ) ) ∈ ℂ )
17 4 7 recne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 / ( 1 − 𝐴 ) ) ≠ 0 )
18 16 17 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ∈ ℂ )
19 12 3 11 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝐴 − 1 ) / 𝐴 ) ∈ ℂ )
20 12 3 13 11 divne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝐴 − 1 ) / 𝐴 ) ≠ 0 )
21 19 20 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ∈ ℂ )
22 18 21 imaddd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) = ( ( ℑ ‘ ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ) + ( ℑ ‘ ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) )
23 15 22 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( 1 − 𝐴 ) 𝐹 1 ) + ( 𝐴 𝐹 ( 𝐴 − 1 ) ) ) = ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) )
24 1 2 9 3 11 angvald ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 𝐹 𝐴 ) = ( ℑ ‘ ( log ‘ ( 𝐴 / 1 ) ) ) )
25 3 div1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝐴 / 1 ) = 𝐴 )
26 25 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ ( 𝐴 / 1 ) ) = ( log ‘ 𝐴 ) )
27 26 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( log ‘ ( 𝐴 / 1 ) ) ) = ( ℑ ‘ ( log ‘ 𝐴 ) ) )
28 24 27 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 𝐹 𝐴 ) = ( ℑ ‘ ( log ‘ 𝐴 ) ) )
29 23 28 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( ( 1 − 𝐴 ) 𝐹 1 ) + ( 𝐴 𝐹 ( 𝐴 − 1 ) ) ) + ( 1 𝐹 𝐴 ) ) = ( ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) + ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
30 18 21 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ∈ ℂ )
31 3 11 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ 𝐴 ) ∈ ℂ )
32 30 31 imaddd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) = ( ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) + ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
33 29 32 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( ( 1 − 𝐴 ) 𝐹 1 ) + ( 𝐴 𝐹 ( 𝐴 − 1 ) ) ) + ( 1 𝐹 𝐴 ) ) = ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) )
34 eqid ⊢ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) = ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) )
35 eqid ⊢ ( ( ( ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) = ( ( ( ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) / i ) / ( 2 · π ) ) − ( 1 / 2 ) )
36 1 34 35 ang180lem3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ∈ { - ( i · π ) , ( i · π ) } )
37 fveq2 ⊢ ( ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) = - ( i · π ) → ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) = ( ℑ ‘ - ( i · π ) ) )
38 ax-icn ⊢ i ∈ ℂ
39 picn ⊢ π ∈ ℂ
40 38 39 mulcli ⊢ ( i · π ) ∈ ℂ
41 40 imnegi ⊢ ( ℑ ‘ - ( i · π ) ) = - ( ℑ ‘ ( i · π ) )
42 40 addlidi ⊢ ( 0 + ( i · π ) ) = ( i · π )
43 42 fveq2i ⊢ ( ℑ ‘ ( 0 + ( i · π ) ) ) = ( ℑ ‘ ( i · π ) )
44 0re ⊢ 0 ∈ ℝ
45 pire ⊢ π ∈ ℝ
46 44 45 crimi ⊢ ( ℑ ‘ ( 0 + ( i · π ) ) ) = π
47 43 46 eqtr3i ⊢ ( ℑ ‘ ( i · π ) ) = π
48 47 negeqi ⊢ - ( ℑ ‘ ( i · π ) ) = - π
49 41 48 eqtri ⊢ ( ℑ ‘ - ( i · π ) ) = - π
50 37 49 eqtrdi ⊢ ( ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) = - ( i · π ) → ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) = - π )
51 fveq2 ⊢ ( ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) = ( i · π ) → ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) = ( ℑ ‘ ( i · π ) ) )
52 51 47 eqtrdi ⊢ ( ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) = ( i · π ) → ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) = π )
53 50 52 orim12i ⊢ ( ( ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) = - ( i · π ) ∨ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) = ( i · π ) ) → ( ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) = - π ∨ ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) = π ) )
54 ovex ⊢ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ∈ V
55 54 elpr ⊢ ( ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ∈ { - ( i · π ) , ( i · π ) } ↔ ( ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) = - ( i · π ) ∨ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) = ( i · π ) ) )
56 fvex ⊢ ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) ∈ V
57 56 elpr ⊢ ( ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) ∈ { - π , π } ↔ ( ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) = - π ∨ ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) = π ) )
58 53 55 57 3imtr4i ⊢ ( ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ∈ { - ( i · π ) , ( i · π ) } → ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) ∈ { - π , π } )
59 36 58 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) ∈ { - π , π } )
60 33 59 eqeltrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( ( 1 − 𝐴 ) 𝐹 1 ) + ( 𝐴 𝐹 ( 𝐴 − 1 ) ) ) + ( 1 𝐹 𝐴 ) ) ∈ { - π , π } )