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 
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
ang180lem1.2 
|- T = ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) )
ang180lem1.3 
|- N = ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) )
Assertion ang180lem2 
|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( -u 2 < N /\ N < 1 ) )

Proof

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