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 2cn 
 |-  2 e. CC
62 picn 
 |-  _pi e. CC
63 61 62 mulcli 
 |-  ( 2 x. _pi ) e. CC
64 63 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 2 x. _pi ) e. CC )
65 2ne0 
 |-  2 =/= 0
66 pire 
 |-  _pi e. RR
67 pipos 
 |-  0 < _pi
68 66 67 gt0ne0ii 
 |-  _pi =/= 0
69 61 62 65 68 mulne0i 
 |-  ( 2 x. _pi ) =/= 0
70 69 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 2 x. _pi ) =/= 0 )
71 60 64 70 divcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( T / _i ) / ( 2 x. _pi ) ) e. CC )
72 71 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( T / _i ) / ( 2 x. _pi ) ) e. CC )
73 halfcn 
 |-  ( 1 / 2 ) e. CC
74 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 ) ) )
75 72 73 74 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 ) ) )
76 27 75 mpbid 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( T / _i ) / ( 2 x. _pi ) ) = ( 1 / 2 ) )
77 60 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( T / _i ) e. CC )
78 63 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( 2 x. _pi ) e. CC )
79 73 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( 1 / 2 ) e. CC )
80 69 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( 2 x. _pi ) =/= 0 )
81 77 78 79 80 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 ) ) )
82 76 81 mpbid 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( 2 x. _pi ) x. ( 1 / 2 ) ) = ( T / _i ) )
83 63 61 65 divreci 
 |-  ( ( 2 x. _pi ) / 2 ) = ( ( 2 x. _pi ) x. ( 1 / 2 ) )
84 62 61 65 divcan3i 
 |-  ( ( 2 x. _pi ) / 2 ) = _pi
85 83 84 eqtr3i 
 |-  ( ( 2 x. _pi ) x. ( 1 / 2 ) ) = _pi
86 82 85 eqtr3di 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( T / _i ) = _pi )
87 55 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> T e. CC )
88 56 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> _i e. CC )
89 62 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> _pi e. CC )
90 58 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> _i =/= 0 )
91 87 88 89 90 divmuld 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( T / _i ) = _pi <-> ( _i x. _pi ) = T ) )
92 86 91 mpbid 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( _i x. _pi ) = T )
93 92 eqcomd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> T = ( _i x. _pi ) )
94 93 olcd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( T = -u ( _i x. _pi ) \/ T = ( _i x. _pi ) ) )
95 62 56 mulneg1i 
 |-  ( -u _pi x. _i ) = -u ( _pi x. _i )
96 62 56 mulcomi 
 |-  ( _pi x. _i ) = ( _i x. _pi )
97 96 negeqi 
 |-  -u ( _pi x. _i ) = -u ( _i x. _pi )
98 95 97 eqtri 
 |-  ( -u _pi x. _i ) = -u ( _i x. _pi )
99 73 63 mulneg1i 
 |-  ( -u ( 1 / 2 ) x. ( 2 x. _pi ) ) = -u ( ( 1 / 2 ) x. ( 2 x. _pi ) )
100 28 61 65 divcan1i 
 |-  ( ( 1 / 2 ) x. 2 ) = 1
101 100 oveq1i 
 |-  ( ( ( 1 / 2 ) x. 2 ) x. _pi ) = ( 1 x. _pi )
102 73 61 62 mulassi 
 |-  ( ( ( 1 / 2 ) x. 2 ) x. _pi ) = ( ( 1 / 2 ) x. ( 2 x. _pi ) )
103 62 mullidi 
 |-  ( 1 x. _pi ) = _pi
104 101 102 103 3eqtr3i 
 |-  ( ( 1 / 2 ) x. ( 2 x. _pi ) ) = _pi
105 104 negeqi 
 |-  -u ( ( 1 / 2 ) x. ( 2 x. _pi ) ) = -u _pi
106 99 105 eqtri 
 |-  ( -u ( 1 / 2 ) x. ( 2 x. _pi ) ) = -u _pi
107 28 73 negsubdii 
 |-  -u ( 1 - ( 1 / 2 ) ) = ( -u 1 + ( 1 / 2 ) )
108 1mhlfehlf 
 |-  ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )
109 108 negeqi 
 |-  -u ( 1 - ( 1 / 2 ) ) = -u ( 1 / 2 )
110 107 109 eqtr3i 
 |-  ( -u 1 + ( 1 / 2 ) ) = -u ( 1 / 2 )
111 simpr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> -u 1 = N )
112 111 3 eqtrdi 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> -u 1 = ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) )
113 112 oveq1d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> ( -u 1 + ( 1 / 2 ) ) = ( ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) + ( 1 / 2 ) ) )
114 110 113 eqtr3id 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> -u ( 1 / 2 ) = ( ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) + ( 1 / 2 ) ) )
115 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 ) ) )
116 71 73 115 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( T / _i ) / ( 2 x. _pi ) ) )
117 116 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 ) ) )
118 114 117 eqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> -u ( 1 / 2 ) = ( ( T / _i ) / ( 2 x. _pi ) ) )
119 118 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 ) ) )
120 106 119 eqtr3id 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> -u _pi = ( ( ( T / _i ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) )
121 60 64 70 divcan1d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( ( T / _i ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) = ( T / _i ) )
122 121 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> ( ( ( T / _i ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) = ( T / _i ) )
123 120 122 eqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> -u _pi = ( T / _i ) )
124 123 oveq1d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> ( -u _pi x. _i ) = ( ( T / _i ) x. _i ) )
125 98 124 eqtr3id 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> -u ( _i x. _pi ) = ( ( T / _i ) x. _i ) )
126 55 57 59 divcan1d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( T / _i ) x. _i ) = T )
127 126 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> ( ( T / _i ) x. _i ) = T )
128 125 127 eqtr2d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> T = -u ( _i x. _pi ) )
129 128 orcd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 = N ) -> ( T = -u ( _i x. _pi ) \/ T = ( _i x. _pi ) ) )
130 df-2 
 |-  2 = ( 1 + 1 )
131 130 negeqi 
 |-  -u 2 = -u ( 1 + 1 )
132 negdi2 
 |-  ( ( 1 e. CC /\ 1 e. CC ) -> -u ( 1 + 1 ) = ( -u 1 - 1 ) )
133 28 28 132 mp2an 
 |-  -u ( 1 + 1 ) = ( -u 1 - 1 )
134 131 133 eqtri 
 |-  -u 2 = ( -u 1 - 1 )
135 4 simpld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> -u 2 < N )
136 134 135 eqbrtrrid 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( -u 1 - 1 ) < N )
137 neg1z 
 |-  -u 1 e. ZZ
138 zlem1lt 
 |-  ( ( -u 1 e. ZZ /\ N e. ZZ ) -> ( -u 1 <_ N <-> ( -u 1 - 1 ) < N ) )
139 137 9 138 sylancr 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( -u 1 <_ N <-> ( -u 1 - 1 ) < N ) )
140 136 139 mpbird 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> -u 1 <_ N )
141 neg1rr 
 |-  -u 1 e. RR
142 leloe 
 |-  ( ( -u 1 e. RR /\ N e. RR ) -> ( -u 1 <_ N <-> ( -u 1 < N \/ -u 1 = N ) ) )
143 141 21 142 sylancr 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( -u 1 <_ N <-> ( -u 1 < N \/ -u 1 = N ) ) )
144 140 143 mpbid 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( -u 1 < N \/ -u 1 = N ) )
145 94 129 144 mpjaodan 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( T = -u ( _i x. _pi ) \/ T = ( _i x. _pi ) ) )
146 2 ovexi 
 |-  T e. _V
147 146 elpr 
 |-  ( T e. { -u ( _i x. _pi ) , ( _i x. _pi ) } <-> ( T = -u ( _i x. _pi ) \/ T = ( _i x. _pi ) ) )
148 145 147 sylibr 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> T e. { -u ( _i x. _pi ) , ( _i x. _pi ) } )