Metamath Proof Explorer

Theorem ang180lem2

Description: Lemma for ang180 . Show that the revolution number N is strictly between -u 2 and 1 . Both bounds are established by iterating using the bounds on the imaginary part of the logarithm, logimcl , but the resulting bound gives only N <_ 1 for the upper bound. The case N = 1 is not ruled out here, but it is in some sense an "edge case" that can only happen under very specific conditions; in particular we show that all the angle arguments A , 1 / ( 1 - A ) , ( A - 1 ) / A must lie on the negative real axis, which is a contradiction because clearly if A is negative then the other two are positive real. (Contributed by Mario Carneiro, 23-Sep-2014)

Ref Expression
Hypotheses ang.1 ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
ang180lem1.2 ⊢ 𝑇 = ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) )
ang180lem1.3 ⊢ 𝑁 = ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) )
Assertion ang180lem2 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 2 < 𝑁 ∧ 𝑁 < 1 ) )

Proof

Step Hyp Ref Expression
1 ang.1 ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2 ang180lem1.2 ⊢ 𝑇 = ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) )
3 ang180lem1.3 ⊢ 𝑁 = ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) )
4 2cn ⊢ 2 ∈ ℂ
5 1re ⊢ 1 ∈ ℝ
6 5 rehalfcli ⊢ ( 1 / 2 ) ∈ ℝ
7 6 recni ⊢ ( 1 / 2 ) ∈ ℂ
8 4 7 negsubdii ⊢ - ( 2 − ( 1 / 2 ) ) = ( - 2 + ( 1 / 2 ) )
9 4d2e2 ⊢ ( 4 / 2 ) = 2
10 9 oveq1i ⊢ ( ( 4 / 2 ) − ( 1 / 2 ) ) = ( 2 − ( 1 / 2 ) )
11 4cn ⊢ 4 ∈ ℂ
12 ax-1cn ⊢ 1 ∈ ℂ
13 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
14 divsubdir ⊢ ( ( 4 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 4 − 1 ) / 2 ) = ( ( 4 / 2 ) − ( 1 / 2 ) ) )
15 11 12 13 14 mp3an ⊢ ( ( 4 − 1 ) / 2 ) = ( ( 4 / 2 ) − ( 1 / 2 ) )
16 4m1e3 ⊢ ( 4 − 1 ) = 3
17 16 oveq1i ⊢ ( ( 4 − 1 ) / 2 ) = ( 3 / 2 )
18 15 17 eqtr3i ⊢ ( ( 4 / 2 ) − ( 1 / 2 ) ) = ( 3 / 2 )
19 10 18 eqtr3i ⊢ ( 2 − ( 1 / 2 ) ) = ( 3 / 2 )
20 19 negeqi ⊢ - ( 2 − ( 1 / 2 ) ) = - ( 3 / 2 )
21 8 20 eqtr3i ⊢ ( - 2 + ( 1 / 2 ) ) = - ( 3 / 2 )
22 3re ⊢ 3 ∈ ℝ
23 22 rehalfcli ⊢ ( 3 / 2 ) ∈ ℝ
24 23 recni ⊢ ( 3 / 2 ) ∈ ℂ
25 picn ⊢ π ∈ ℂ
26 24 4 25 mulassi ⊢ ( ( ( 3 / 2 ) · 2 ) · π ) = ( ( 3 / 2 ) · ( 2 · π ) )
27 3cn ⊢ 3 ∈ ℂ
28 2ne0 ⊢ 2 ≠ 0
29 27 4 28 divcan1i ⊢ ( ( 3 / 2 ) · 2 ) = 3
30 29 oveq1i ⊢ ( ( ( 3 / 2 ) · 2 ) · π ) = ( 3 · π )
31 26 30 eqtr3i ⊢ ( ( 3 / 2 ) · ( 2 · π ) ) = ( 3 · π )
32 31 negeqi ⊢ - ( ( 3 / 2 ) · ( 2 · π ) ) = - ( 3 · π )
33 2re ⊢ 2 ∈ ℝ
34 pire ⊢ π ∈ ℝ
35 33 34 remulcli ⊢ ( 2 · π ) ∈ ℝ
36 35 recni ⊢ ( 2 · π ) ∈ ℂ
37 24 36 mulneg1i ⊢ ( - ( 3 / 2 ) · ( 2 · π ) ) = - ( ( 3 / 2 ) · ( 2 · π ) )
38 27 25 mulneg2i ⊢ ( 3 · - π ) = - ( 3 · π )
39 32 37 38 3eqtr4i ⊢ ( - ( 3 / 2 ) · ( 2 · π ) ) = ( 3 · - π )
40 34 renegcli ⊢ - π ∈ ℝ
41 33 40 remulcli ⊢ ( 2 · - π ) ∈ ℝ
42 41 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 2 · - π ) ∈ ℝ )
43 40 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - π ∈ ℝ )
44 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ∈ ℂ )
45 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 − 𝐴 ) ∈ ℂ )
46 12 44 45 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 − 𝐴 ) ∈ ℂ )
47 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ≠ 1 )
48 47 necomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 1 ≠ 𝐴 )
49 subeq0 ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
50 12 44 49 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
51 50 necon3bid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 1 − 𝐴 ) ≠ 0 ↔ 1 ≠ 𝐴 ) )
52 48 51 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 − 𝐴 ) ≠ 0 )
53 46 52 reccld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 / ( 1 − 𝐴 ) ) ∈ ℂ )
54 46 52 recne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 / ( 1 − 𝐴 ) ) ≠ 0 )
55 53 54 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ∈ ℂ )
56 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 − 1 ) ∈ ℂ )
57 44 12 56 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝐴 − 1 ) ∈ ℂ )
58 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝐴 ≠ 0 )
59 57 44 58 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝐴 − 1 ) / 𝐴 ) ∈ ℂ )
60 subeq0 ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 − 1 ) = 0 ↔ 𝐴 = 1 ) )
61 44 12 60 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝐴 − 1 ) = 0 ↔ 𝐴 = 1 ) )
62 61 necon3bid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝐴 − 1 ) ≠ 0 ↔ 𝐴 ≠ 1 ) )
63 47 62 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝐴 − 1 ) ≠ 0 )
64 57 44 63 58 divne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝐴 − 1 ) / 𝐴 ) ≠ 0 )
65 59 64 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ∈ ℂ )
66 55 65 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ∈ ℂ )
67 66 imcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ∈ ℝ )
68 logcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
69 68 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ 𝐴 ) ∈ ℂ )
70 69 imcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
71 55 imcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ) ∈ ℝ )
72 65 imcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ∈ ℝ )
73 53 54 logimcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - π < ( ℑ ‘ ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ) ∧ ( ℑ ‘ ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ) ≤ π ) )
74 73 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - π < ( ℑ ‘ ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ) )
75 59 64 logimcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - π < ( ℑ ‘ ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ∧ ( ℑ ‘ ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ≤ π ) )
76 75 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - π < ( ℑ ‘ ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) )
77 43 43 71 72 74 76 lt2addd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - π + - π ) < ( ( ℑ ‘ ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ) + ( ℑ ‘ ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) )
78 negpicn ⊢ - π ∈ ℂ
79 78 2timesi ⊢ ( 2 · - π ) = ( - π + - π )
80 79 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 2 · - π ) = ( - π + - π ) )
81 55 65 imaddd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) = ( ( ℑ ‘ ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ) + ( ℑ ‘ ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) )
82 77 80 81 3brtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 2 · - π ) < ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) )
83 logimcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
84 83 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
85 84 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) )
86 42 43 67 70 82 85 lt2addd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 2 · - π ) + - π ) < ( ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) + ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
87 df-3 ⊢ 3 = ( 2 + 1 )
88 87 oveq1i ⊢ ( 3 · - π ) = ( ( 2 + 1 ) · - π )
89 4 12 78 adddiri ⊢ ( ( 2 + 1 ) · - π ) = ( ( 2 · - π ) + ( 1 · - π ) )
90 78 mulid2i ⊢ ( 1 · - π ) = - π
91 90 oveq2i ⊢ ( ( 2 · - π ) + ( 1 · - π ) ) = ( ( 2 · - π ) + - π )
92 88 89 91 3eqtri ⊢ ( 3 · - π ) = ( ( 2 · - π ) + - π )
93 92 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 3 · - π ) = ( ( 2 · - π ) + - π ) )
94 2 fveq2i ⊢ ( ℑ ‘ 𝑇 ) = ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) )
95 66 69 imaddd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ) = ( ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) + ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
96 94 95 syl5eq ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ 𝑇 ) = ( ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) + ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
97 86 93 96 3brtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 3 · - π ) < ( ℑ ‘ 𝑇 ) )
98 66 69 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) + ( log ‘ 𝐴 ) ) ∈ ℂ )
99 2 98 eqeltrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑇 ∈ ℂ )
100 imval ⊢ ( 𝑇 ∈ ℂ → ( ℑ ‘ 𝑇 ) = ( ℜ ‘ ( 𝑇 / i ) ) )
101 99 100 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ 𝑇 ) = ( ℜ ‘ ( 𝑇 / i ) ) )
102 1 2 3 ang180lem1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑁 ∈ ℤ ∧ ( 𝑇 / i ) ∈ ℝ ) )
103 102 simprd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑇 / i ) ∈ ℝ )
104 103 rered ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℜ ‘ ( 𝑇 / i ) ) = ( 𝑇 / i ) )
105 101 104 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ 𝑇 ) = ( 𝑇 / i ) )
106 97 105 breqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 3 · - π ) < ( 𝑇 / i ) )
107 39 106 eqbrtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - ( 3 / 2 ) · ( 2 · π ) ) < ( 𝑇 / i ) )
108 23 renegcli ⊢ - ( 3 / 2 ) ∈ ℝ
109 108 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - ( 3 / 2 ) ∈ ℝ )
110 35 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 2 · π ) ∈ ℝ )
111 2pos ⊢ 0 < 2
112 pipos ⊢ 0 < π
113 33 34 111 112 mulgt0ii ⊢ 0 < ( 2 · π )
114 113 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 0 < ( 2 · π ) )
115 ltmuldiv ⊢ ( ( - ( 3 / 2 ) ∈ ℝ ∧ ( 𝑇 / i ) ∈ ℝ ∧ ( ( 2 · π ) ∈ ℝ ∧ 0 < ( 2 · π ) ) ) → ( ( - ( 3 / 2 ) · ( 2 · π ) ) < ( 𝑇 / i ) ↔ - ( 3 / 2 ) < ( ( 𝑇 / i ) / ( 2 · π ) ) ) )
116 109 103 110 114 115 syl112anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( - ( 3 / 2 ) · ( 2 · π ) ) < ( 𝑇 / i ) ↔ - ( 3 / 2 ) < ( ( 𝑇 / i ) / ( 2 · π ) ) ) )
117 107 116 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - ( 3 / 2 ) < ( ( 𝑇 / i ) / ( 2 · π ) ) )
118 21 117 eqbrtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 2 + ( 1 / 2 ) ) < ( ( 𝑇 / i ) / ( 2 · π ) ) )
119 33 renegcli ⊢ - 2 ∈ ℝ
120 119 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - 2 ∈ ℝ )
121 6 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 / 2 ) ∈ ℝ )
122 35 113 gt0ne0ii ⊢ ( 2 · π ) ≠ 0
123 122 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 2 · π ) ≠ 0 )
124 103 110 123 redivcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝑇 / i ) / ( 2 · π ) ) ∈ ℝ )
125 120 121 124 ltaddsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( - 2 + ( 1 / 2 ) ) < ( ( 𝑇 / i ) / ( 2 · π ) ) ↔ - 2 < ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) ) )
126 118 125 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - 2 < ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) )
127 126 3 breqtrrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - 2 < 𝑁 )
128 34 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → π ∈ ℝ )
129 73 simprd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ) ≤ π )
130 75 simprd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ≤ π )
131 71 72 128 128 129 130 le2addd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ℑ ‘ ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ) + ( ℑ ‘ ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ≤ ( π + π ) )
132 25 2timesi ⊢ ( 2 · π ) = ( π + π )
133 132 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 2 · π ) = ( π + π ) )
134 131 81 133 3brtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ≤ ( 2 · π ) )
135 84 simprd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π )
136 67 70 110 128 134 135 le2addd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) + ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( ( 2 · π ) + π ) )
137 105 96 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑇 / i ) = ( ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) + ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
138 87 oveq1i ⊢ ( 3 · π ) = ( ( 2 + 1 ) · π )
139 4 12 25 adddiri ⊢ ( ( 2 + 1 ) · π ) = ( ( 2 · π ) + ( 1 · π ) )
140 25 mulid2i ⊢ ( 1 · π ) = π
141 140 oveq2i ⊢ ( ( 2 · π ) + ( 1 · π ) ) = ( ( 2 · π ) + π )
142 138 139 141 3eqtri ⊢ ( 3 · π ) = ( ( 2 · π ) + π )
143 142 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 3 · π ) = ( ( 2 · π ) + π ) )
144 136 137 143 3brtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑇 / i ) ≤ ( 3 · π ) )
145 36 subid1i ⊢ ( ( 2 · π ) − 0 ) = ( 2 · π )
146 145 122 eqnetri ⊢ ( ( 2 · π ) − 0 ) ≠ 0
147 negsub ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 + - 𝐴 ) = ( 1 − 𝐴 ) )
148 12 44 147 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 1 + - 𝐴 ) = ( 1 − 𝐴 ) )
149 148 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( 1 + - 𝐴 ) = ( 1 − 𝐴 ) )
150 1rp ⊢ 1 ∈ ℝ+
151 143 137 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 3 · π ) − ( 𝑇 / i ) ) = ( ( ( 2 · π ) + π ) − ( ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) + ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
152 36 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 2 · π ) ∈ ℂ )
153 25 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → π ∈ ℂ )
154 67 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ∈ ℂ )
155 70 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
156 152 153 154 155 addsub4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( 2 · π ) + π ) − ( ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) + ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) + ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
157 151 156 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 3 · π ) − ( 𝑇 / i ) ) = ( ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) + ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
158 157 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ( 3 · π ) − ( 𝑇 / i ) ) = ( ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) + ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
159 22 34 remulcli ⊢ ( 3 · π ) ∈ ℝ
160 159 recni ⊢ ( 3 · π ) ∈ ℂ
161 ax-icn ⊢ i ∈ ℂ
162 161 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → i ∈ ℂ )
163 ine0 ⊢ i ≠ 0
164 163 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → i ≠ 0 )
165 99 162 164 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑇 / i ) ∈ ℂ )
166 subeq0 ⊢ ( ( ( 3 · π ) ∈ ℂ ∧ ( 𝑇 / i ) ∈ ℂ ) → ( ( ( 3 · π ) − ( 𝑇 / i ) ) = 0 ↔ ( 3 · π ) = ( 𝑇 / i ) ) )
167 160 165 166 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( 3 · π ) − ( 𝑇 / i ) ) = 0 ↔ ( 3 · π ) = ( 𝑇 / i ) ) )
168 167 biimpar ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ( 3 · π ) − ( 𝑇 / i ) ) = 0 )
169 158 168 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) + ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = 0 )
170 resubcl ⊢ ( ( ( 2 · π ) ∈ ℝ ∧ ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ∈ ℝ ) → ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) ∈ ℝ )
171 35 67 170 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) ∈ ℝ )
172 subge0 ⊢ ( ( ( 2 · π ) ∈ ℝ ∧ ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ∈ ℝ ) → ( 0 ≤ ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) ↔ ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ≤ ( 2 · π ) ) )
173 35 67 172 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 0 ≤ ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) ↔ ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ≤ ( 2 · π ) ) )
174 134 173 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 0 ≤ ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) )
175 resubcl ⊢ ( ( π ∈ ℝ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ) → ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ )
176 34 70 175 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ )
177 subge0 ⊢ ( ( π ∈ ℝ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ) → ( 0 ≤ ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
178 34 70 177 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 0 ≤ ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
179 135 178 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 0 ≤ ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
180 add20 ⊢ ( ( ( ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) ∈ ℝ ∧ 0 ≤ ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) ) ∧ ( ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ ∧ 0 ≤ ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) → ( ( ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) + ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = 0 ↔ ( ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) = 0 ∧ ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = 0 ) ) )
181 171 174 176 179 180 syl22anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) + ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = 0 ↔ ( ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) = 0 ∧ ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = 0 ) ) )
182 181 biimpa ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) + ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = 0 ) → ( ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) = 0 ∧ ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = 0 ) )
183 169 182 syldan ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) = 0 ∧ ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = 0 ) )
184 183 simprd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = 0 )
185 155 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
186 subeq0 ⊢ ( ( π ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ ) → ( ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = 0 ↔ π = ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
187 25 185 186 sylancr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ( π − ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = 0 ↔ π = ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
188 184 187 mpbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → π = ( ℑ ‘ ( log ‘ 𝐴 ) ) )
189 188 eqcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) = π )
190 lognegb ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - 𝐴 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) = π ) )
191 190 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 𝐴 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) = π ) )
192 191 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( - 𝐴 ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ 𝐴 ) ) = π ) )
193 189 192 mpbird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → - 𝐴 ∈ ℝ+ )
194 rpaddcl ⊢ ( ( 1 ∈ ℝ+ ∧ - 𝐴 ∈ ℝ+ ) → ( 1 + - 𝐴 ) ∈ ℝ+ )
195 150 193 194 sylancr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( 1 + - 𝐴 ) ∈ ℝ+ )
196 149 195 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( 1 − 𝐴 ) ∈ ℝ+ )
197 196 rpreccld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( 1 / ( 1 − 𝐴 ) ) ∈ ℝ+ )
198 197 relogcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ∈ ℝ )
199 negsubdi2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → - ( 𝐴 − 1 ) = ( 1 − 𝐴 ) )
200 44 12 199 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → - ( 𝐴 − 1 ) = ( 1 − 𝐴 ) )
201 200 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - ( 𝐴 − 1 ) / - 𝐴 ) = ( ( 1 − 𝐴 ) / - 𝐴 ) )
202 57 44 58 div2negd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - ( 𝐴 − 1 ) / - 𝐴 ) = ( ( 𝐴 − 1 ) / 𝐴 ) )
203 201 202 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 1 − 𝐴 ) / - 𝐴 ) = ( ( 𝐴 − 1 ) / 𝐴 ) )
204 203 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ( 1 − 𝐴 ) / - 𝐴 ) = ( ( 𝐴 − 1 ) / 𝐴 ) )
205 196 193 rpdivcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ( 1 − 𝐴 ) / - 𝐴 ) ∈ ℝ+ )
206 204 205 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ( 𝐴 − 1 ) / 𝐴 ) ∈ ℝ+ )
207 206 relogcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ∈ ℝ )
208 198 207 readdcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ∈ ℝ )
209 208 reim0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) = 0 )
210 209 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) = ( ( 2 · π ) − 0 ) )
211 183 simpld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ( 2 · π ) − ( ℑ ‘ ( ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) + ( log ‘ ( ( 𝐴 − 1 ) / 𝐴 ) ) ) ) ) = 0 )
212 210 211 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) ∧ ( 3 · π ) = ( 𝑇 / i ) ) → ( ( 2 · π ) − 0 ) = 0 )
213 212 ex ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 3 · π ) = ( 𝑇 / i ) → ( ( 2 · π ) − 0 ) = 0 ) )
214 213 necon3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( 2 · π ) − 0 ) ≠ 0 → ( 3 · π ) ≠ ( 𝑇 / i ) ) )
215 146 214 mpi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 3 · π ) ≠ ( 𝑇 / i ) )
216 ltlen ⊢ ( ( ( 𝑇 / i ) ∈ ℝ ∧ ( 3 · π ) ∈ ℝ ) → ( ( 𝑇 / i ) < ( 3 · π ) ↔ ( ( 𝑇 / i ) ≤ ( 3 · π ) ∧ ( 3 · π ) ≠ ( 𝑇 / i ) ) ) )
217 103 159 216 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝑇 / i ) < ( 3 · π ) ↔ ( ( 𝑇 / i ) ≤ ( 3 · π ) ∧ ( 3 · π ) ≠ ( 𝑇 / i ) ) ) )
218 144 215 217 mpbir2and ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑇 / i ) < ( 3 · π ) )
219 218 31 breqtrrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 𝑇 / i ) < ( ( 3 / 2 ) · ( 2 · π ) ) )
220 23 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( 3 / 2 ) ∈ ℝ )
221 ltdivmul2 ⊢ ( ( ( 𝑇 / i ) ∈ ℝ ∧ ( 3 / 2 ) ∈ ℝ ∧ ( ( 2 · π ) ∈ ℝ ∧ 0 < ( 2 · π ) ) ) → ( ( ( 𝑇 / i ) / ( 2 · π ) ) < ( 3 / 2 ) ↔ ( 𝑇 / i ) < ( ( 3 / 2 ) · ( 2 · π ) ) ) )
222 103 220 110 114 221 syl112anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( 𝑇 / i ) / ( 2 · π ) ) < ( 3 / 2 ) ↔ ( 𝑇 / i ) < ( ( 3 / 2 ) · ( 2 · π ) ) ) )
223 219 222 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝑇 / i ) / ( 2 · π ) ) < ( 3 / 2 ) )
224 87 oveq1i ⊢ ( 3 / 2 ) = ( ( 2 + 1 ) / 2 )
225 4 12 4 28 divdiri ⊢ ( ( 2 + 1 ) / 2 ) = ( ( 2 / 2 ) + ( 1 / 2 ) )
226 2div2e1 ⊢ ( 2 / 2 ) = 1
227 226 oveq1i ⊢ ( ( 2 / 2 ) + ( 1 / 2 ) ) = ( 1 + ( 1 / 2 ) )
228 224 225 227 3eqtri ⊢ ( 3 / 2 ) = ( 1 + ( 1 / 2 ) )
229 223 228 breqtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( 𝑇 / i ) / ( 2 · π ) ) < ( 1 + ( 1 / 2 ) ) )
230 5 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 1 ∈ ℝ )
231 124 121 230 ltsubaddd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) < 1 ↔ ( ( 𝑇 / i ) / ( 2 · π ) ) < ( 1 + ( 1 / 2 ) ) ) )
232 229 231 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( ( ( 𝑇 / i ) / ( 2 · π ) ) − ( 1 / 2 ) ) < 1 )
233 3 232 eqbrtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → 𝑁 < 1 )
234 127 233 jca ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( - 2 < 𝑁 ∧ 𝑁 < 1 ) )