Metamath Proof Explorer

Theorem ang180lem3

Description: Lemma for ang180 . Since ang180lem1 shows that N is an integer and ang180lem2 shows that N is strictly between -u 2 and 1 , it follows that N e. { -u 1 , 0 } , and these two cases correspond to the two possible values for T . (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 ang180lem3 
|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> T e. { -u ( _i x. _pi ) , ( _i x. _pi ) } )

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 1 2 3 ang180lem2 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( -u 2 < N /\ N < 1 ) )
5 4 simprd 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> N < 1 )
6 1e0p1 
 |-  1 = ( 0 + 1 )
7 5 6 breqtrdi 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> N < ( 0 + 1 ) )
8 1 2 3 ang180lem1 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( N e. ZZ /\ ( T / _i ) e. RR ) )
9 8 simpld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> N e. ZZ )
10 0z 
 |-  0 e. ZZ
11 zleltp1 
 |-  ( ( N e. ZZ /\ 0 e. ZZ ) -> ( N <_ 0 <-> N < ( 0 + 1 ) ) )
12 9 10 11 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( N <_ 0 <-> N < ( 0 + 1 ) ) )
13 7 12 mpbird 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> N <_ 0 )
14 13 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> N <_ 0 )
15 zlem1lt 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( 0 <_ N <-> ( 0 - 1 ) < N ) )
16 10 9 15 sylancr 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 0 <_ N <-> ( 0 - 1 ) < N ) )
17 df-neg 
 |-  -u 1 = ( 0 - 1 )
18 17 breq1i 
 |-  ( -u 1 < N <-> ( 0 - 1 ) < N )
19 16 18 bitr4di 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 0 <_ N <-> -u 1 < N ) )
20 19 biimpar 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> 0 <_ N )
21 9 zred 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> N e. RR )
22 21 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> N e. RR )
23 0re 
 |-  0 e. RR
24 letri3 
 |-  ( ( N e. RR /\ 0 e. RR ) -> ( N = 0 <-> ( N <_ 0 /\ 0 <_ N ) ) )
25 22 23 24 sylancl 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( N = 0 <-> ( N <_ 0 /\ 0 <_ N ) ) )
26 14 20 25 mpbir2and 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> N = 0 )
27 3 26 eqtr3id 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) = 0 )
28 ax-1cn 
 |-  1 e. CC
29 simp1 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> A e. CC )
30 subcl 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( 1 - A ) e. CC )
31 28 29 30 sylancr 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 1 - A ) e. CC )
32 simp3 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> A =/= 1 )
33 32 necomd 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> 1 =/= A )
34 subeq0 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( ( 1 - A ) = 0 <-> 1 = A ) )
35 28 29 34 sylancr 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( 1 - A ) = 0 <-> 1 = A ) )
36 35 necon3bid 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( 1 - A ) =/= 0 <-> 1 =/= A ) )
37 33 36 mpbird 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 1 - A ) =/= 0 )
38 31 37 reccld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 1 / ( 1 - A ) ) e. CC )
39 31 37 recne0d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 1 / ( 1 - A ) ) =/= 0 )
40 38 39 logcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` ( 1 / ( 1 - A ) ) ) e. CC )
41 subcl 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( A - 1 ) e. CC )
42 29 28 41 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( A - 1 ) e. CC )
43 simp2 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> A =/= 0 )
44 42 29 43 divcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( A - 1 ) / A ) e. CC )
45 subeq0 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A - 1 ) = 0 <-> A = 1 ) )
46 29 28 45 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( A - 1 ) = 0 <-> A = 1 ) )
47 46 necon3bid 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( A - 1 ) =/= 0 <-> A =/= 1 ) )
48 32 47 mpbird 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( A - 1 ) =/= 0 )
49 42 29 48 43 divne0d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( A - 1 ) / A ) =/= 0 )
50 44 49 logcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` ( ( A - 1 ) / A ) ) e. CC )
51 40 50 addcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) e. CC )
52 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
53 52 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` A ) e. CC )
54 51 53 addcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) e. CC )
55 2 54 eqeltrid 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> T e. CC )
56 ax-icn 
 |-  _i e. CC
57 56 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> _i e. CC )
58 ine0 
 |-  _i =/= 0
59 58 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> _i =/= 0 )
60 55 57 59 divcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( T / _i ) e. CC )
61 2picn 
 |-  ( 2 x. _pi ) e. CC
62 61 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 2 x. _pi ) e. CC )
63 2cn 
 |-  2 e. CC
64 picn 
 |-  _pi e. CC
65 2ne0 
 |-  2 =/= 0
66 pine0 
 |-  _pi =/= 0
67 63 64 65 66 mulne0i 
 |-  ( 2 x. _pi ) =/= 0
68 67 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 2 x. _pi ) =/= 0 )
69 60 62 68 divcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( T / _i ) / ( 2 x. _pi ) ) e. CC )
70 69 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( T / _i ) / ( 2 x. _pi ) ) e. CC )
71 halfcn 
 |-  ( 1 / 2 ) e. CC
72 subeq0 
 |-  ( ( ( ( T / _i ) / ( 2 x. _pi ) ) e. CC /\ ( 1 / 2 ) e. CC ) -> ( ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) = 0 <-> ( ( T / _i ) / ( 2 x. _pi ) ) = ( 1 / 2 ) ) )
73 70 71 72 sylancl 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) = 0 <-> ( ( T / _i ) / ( 2 x. _pi ) ) = ( 1 / 2 ) ) )
74 27 73 mpbid 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( T / _i ) / ( 2 x. _pi ) ) = ( 1 / 2 ) )
75 60 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( T / _i ) e. CC )
76 61 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( 2 x. _pi ) e. CC )
77 71 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( 1 / 2 ) e. CC )
78 67 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( 2 x. _pi ) =/= 0 )
79 75 76 77 78 divmuld 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( ( T / _i ) / ( 2 x. _pi ) ) = ( 1 / 2 ) <-> ( ( 2 x. _pi ) x. ( 1 / 2 ) ) = ( T / _i ) ) )
80 74 79 mpbid 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( 2 x. _pi ) x. ( 1 / 2 ) ) = ( T / _i ) )
81 61 63 65 divreci 
 |-  ( ( 2 x. _pi ) / 2 ) = ( ( 2 x. _pi ) x. ( 1 / 2 ) )
82 64 63 65 divcan3i 
 |-  ( ( 2 x. _pi ) / 2 ) = _pi
83 81 82 eqtr3i 
 |-  ( ( 2 x. _pi ) x. ( 1 / 2 ) ) = _pi
84 80 83 eqtr3di 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( T / _i ) = _pi )
85 55 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> T e. CC )
86 56 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> _i e. CC )
87 64 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> _pi e. CC )
88 58 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> _i =/= 0 )
89 85 86 87 88 divmuld 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( T / _i ) = _pi <-> ( _i x. _pi ) = T ) )
90 84 89 mpbid 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( _i x. _pi ) = T )
91 90 eqcomd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> T = ( _i x. _pi ) )
92 91 olcd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( T = -u ( _i x. _pi ) \/ T = ( _i x. _pi ) ) )
93 64 56 mulneg1i 
 |-  ( -u _pi x. _i ) = -u ( _pi x. _i )
94 64 56 mulcomi 
 |-  ( _pi x. _i ) = ( _i x. _pi )
95 94 negeqi 
 |-  -u ( _pi x. _i ) = -u ( _i x. _pi )
96 93 95 eqtri 
 |-  ( -u _pi x. _i ) = -u ( _i x. _pi )
97 71 61 mulneg1i 
 |-  ( -u ( 1 / 2 ) x. ( 2 x. _pi ) ) = -u ( ( 1 / 2 ) x. ( 2 x. _pi ) )
98 28 63 65 divcan1i 
 |-  ( ( 1 / 2 ) x. 2 ) = 1
99 98 oveq1i 
 |-  ( ( ( 1 / 2 ) x. 2 ) x. _pi ) = ( 1 x. _pi )
100 71 63 64 mulassi 
 |-  ( ( ( 1 / 2 ) x. 2 ) x. _pi ) = ( ( 1 / 2 ) x. ( 2 x. _pi ) )
101 64 mullidi 
 |-  ( 1 x. _pi ) = _pi
102 99 100 101 3eqtr3i 
 |-  ( ( 1 / 2 ) x. ( 2 x. _pi ) ) = _pi
103 102 negeqi 
 |-  -u ( ( 1 / 2 ) x. ( 2 x. _pi ) ) = -u _pi
104 97 103 eqtri 
 |-  ( -u ( 1 / 2 ) x. ( 2 x. _pi ) ) = -u _pi
105 28 71 negsubdii 
 |-  -u ( 1 - ( 1 / 2 ) ) = ( -u 1 + ( 1 / 2 ) )
106 1mhlfehlf 
 |-  ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )
107 106 negeqi 
 |-  -u ( 1 - ( 1 / 2 ) ) = -u ( 1 / 2 )
108 105 107 eqtr3i 
 |-  ( -u 1 + ( 1 / 2 ) ) = -u ( 1 / 2 )
109 simpr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> -u 1 = N )
110 109 3 eqtrdi 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> -u 1 = ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) )
111 110 oveq1d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> ( -u 1 + ( 1 / 2 ) ) = ( ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) + ( 1 / 2 ) ) )
112 108 111 eqtr3id 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> -u ( 1 / 2 ) = ( ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) + ( 1 / 2 ) ) )
113 npcan 
 |-  ( ( ( ( T / _i ) / ( 2 x. _pi ) ) e. CC /\ ( 1 / 2 ) e. CC ) -> ( ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( T / _i ) / ( 2 x. _pi ) ) )
114 69 71 113 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( T / _i ) / ( 2 x. _pi ) ) )
115 114 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> ( ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( T / _i ) / ( 2 x. _pi ) ) )
116 112 115 eqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> -u ( 1 / 2 ) = ( ( T / _i ) / ( 2 x. _pi ) ) )
117 116 oveq1d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> ( -u ( 1 / 2 ) x. ( 2 x. _pi ) ) = ( ( ( T / _i ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) )
118 104 117 eqtr3id 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> -u _pi = ( ( ( T / _i ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) )
119 60 62 68 divcan1d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( ( T / _i ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) = ( T / _i ) )
120 119 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> ( ( ( T / _i ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) = ( T / _i ) )
121 118 120 eqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> -u _pi = ( T / _i ) )
122 121 oveq1d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> ( -u _pi x. _i ) = ( ( T / _i ) x. _i ) )
123 96 122 eqtr3id 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> -u ( _i x. _pi ) = ( ( T / _i ) x. _i ) )
124 55 57 59 divcan1d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( T / _i ) x. _i ) = T )
125 124 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> ( ( T / _i ) x. _i ) = T )
126 123 125 eqtr2d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> T = -u ( _i x. _pi ) )
127 126 orcd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> ( T = -u ( _i x. _pi ) \/ T = ( _i x. _pi ) ) )
128 df-2 
 |-  2 = ( 1 + 1 )
129 128 negeqi 
 |-  -u 2 = -u ( 1 + 1 )
130 negdi2 
 |-  ( ( 1 e. CC /\ 1 e. CC ) -> -u ( 1 + 1 ) = ( -u 1 - 1 ) )
131 28 28 130 mp2an 
 |-  -u ( 1 + 1 ) = ( -u 1 - 1 )
132 129 131 eqtri 
 |-  -u 2 = ( -u 1 - 1 )
133 4 simpld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> -u 2 < N )
134 132 133 eqbrtrrid 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( -u 1 - 1 ) < N )
135 neg1z 
 |-  -u 1 e. ZZ
136 zlem1lt 
 |-  ( ( -u 1 e. ZZ /\ N e. ZZ ) -> ( -u 1 <_ N <-> ( -u 1 - 1 ) < N ) )
137 135 9 136 sylancr 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( -u 1 <_ N <-> ( -u 1 - 1 ) < N ) )
138 134 137 mpbird 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> -u 1 <_ N )
139 neg1rr 
 |-  -u 1 e. RR
140 leloe 
 |-  ( ( -u 1 e. RR /\ N e. RR ) -> ( -u 1 <_ N <-> ( -u 1 < N \/ -u 1 = N ) ) )
141 139 21 140 sylancr 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( -u 1 <_ N <-> ( -u 1 < N \/ -u 1 = N ) ) )
142 138 141 mpbid 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( -u 1 < N \/ -u 1 = N ) )
143 92 127 142 mpjaodan 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( T = -u ( _i x. _pi ) \/ T = ( _i x. _pi ) ) )
144 2 ovexi 
 |-  T e. _V
145 144 elpr 
 |-  ( T e. { -u ( _i x. _pi ) , ( _i x. _pi ) } <-> ( T = -u ( _i x. _pi ) \/ T = ( _i x. _pi ) ) )
146 143 145 sylibr 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> T e. { -u ( _i x. _pi ) , ( _i x. _pi ) } )