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 2cn 
 |-  2 e. CC
5 picn 
 |-  _pi e. CC
6 4 5 mulcli 
 |-  ( 2 x. _pi ) e. CC
7 2ne0 
 |-  2 =/= 0
8 6 4 7 divreci 
 |-  ( ( 2 x. _pi ) / 2 ) = ( ( 2 x. _pi ) x. ( 1 / 2 ) )
9 5 4 7 divcan3i 
 |-  ( ( 2 x. _pi ) / 2 ) = _pi
10 8 9 eqtr3i 
 |-  ( ( 2 x. _pi ) x. ( 1 / 2 ) ) = _pi
11 1 2 3 ang180lem2 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( -u 2 < N /\ N < 1 ) )
12 11 simprd 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> N < 1 )
13 1e0p1 
 |-  1 = ( 0 + 1 )
14 12 13 breqtrdi 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> N < ( 0 + 1 ) )
15 1 2 3 ang180lem1 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( N e. ZZ /\ ( T / _i ) e. RR ) )
16 15 simpld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> N e. ZZ )
17 0z 
 |-  0 e. ZZ
18 zleltp1 
 |-  ( ( N e. ZZ /\ 0 e. ZZ ) -> ( N <_ 0 <-> N < ( 0 + 1 ) ) )
19 16 17 18 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( N <_ 0 <-> N < ( 0 + 1 ) ) )
20 14 19 mpbird 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> N <_ 0 )
21 20 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> N <_ 0 )
22 zlem1lt 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( 0 <_ N <-> ( 0 - 1 ) < N ) )
23 17 16 22 sylancr 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 0 <_ N <-> ( 0 - 1 ) < N ) )
24 df-neg 
 |-  -u 1 = ( 0 - 1 )
25 24 breq1i 
 |-  ( -u 1 < N <-> ( 0 - 1 ) < N )
26 23 25 bitr4di 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 0 <_ N <-> -u 1 < N ) )
27 26 biimpar 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> 0 <_ N )
28 16 zred 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> N e. RR )
29 28 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> N e. RR )
30 0re 
 |-  0 e. RR
31 letri3 
 |-  ( ( N e. RR /\ 0 e. RR ) -> ( N = 0 <-> ( N <_ 0 /\ 0 <_ N ) ) )
32 29 30 31 sylancl 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( N = 0 <-> ( N <_ 0 /\ 0 <_ N ) ) )
33 21 27 32 mpbir2and 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> N = 0 )
34 3 33 eqtr3id 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( ( T / _i ) / ( 2 x. _pi ) ) - ( 1 / 2 ) ) = 0 )
35 ax-1cn 
 |-  1 e. CC
36 simp1 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> A e. CC )
37 subcl 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( 1 - A ) e. CC )
38 35 36 37 sylancr 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 1 - A ) e. CC )
39 simp3 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> A =/= 1 )
40 39 necomd 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> 1 =/= A )
41 subeq0 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( ( 1 - A ) = 0 <-> 1 = A ) )
42 35 36 41 sylancr 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( 1 - A ) = 0 <-> 1 = A ) )
43 42 necon3bid 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( 1 - A ) =/= 0 <-> 1 =/= A ) )
44 40 43 mpbird 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 1 - A ) =/= 0 )
45 38 44 reccld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 1 / ( 1 - A ) ) e. CC )
46 38 44 recne0d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 1 / ( 1 - A ) ) =/= 0 )
47 45 46 logcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` ( 1 / ( 1 - A ) ) ) e. CC )
48 subcl 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( A - 1 ) e. CC )
49 36 35 48 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( A - 1 ) e. CC )
50 simp2 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> A =/= 0 )
51 49 36 50 divcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( A - 1 ) / A ) e. CC )
52 subeq0 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A - 1 ) = 0 <-> A = 1 ) )
53 36 35 52 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( A - 1 ) = 0 <-> A = 1 ) )
54 53 necon3bid 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( A - 1 ) =/= 0 <-> A =/= 1 ) )
55 39 54 mpbird 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( A - 1 ) =/= 0 )
56 49 36 55 50 divne0d 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( A - 1 ) / A ) =/= 0 )
57 51 56 logcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` ( ( A - 1 ) / A ) ) e. CC )
58 47 57 addcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) e. CC )
59 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
60 59 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` A ) e. CC )
61 58 60 addcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( ( log ` ( 1 / ( 1 - A ) ) ) + ( log ` ( ( A - 1 ) / A ) ) ) + ( log ` A ) ) e. CC )
62 2 61 eqeltrid 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> T e. CC )
63 ax-icn 
 |-  _i e. CC
64 63 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> _i e. CC )
65 ine0 
 |-  _i =/= 0
66 65 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> _i =/= 0 )
67 62 64 66 divcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( T / _i ) e. CC )
68 6 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 2 x. _pi ) e. CC )
69 pire 
 |-  _pi e. RR
70 pipos 
 |-  0 < _pi
71 69 70 gt0ne0ii 
 |-  _pi =/= 0
72 4 5 7 71 mulne0i 
 |-  ( 2 x. _pi ) =/= 0
73 72 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( 2 x. _pi ) =/= 0 )
74 67 68 73 divcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( T / _i ) / ( 2 x. _pi ) ) e. CC )
75 74 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( T / _i ) / ( 2 x. _pi ) ) e. CC )
76 halfcn 
 |-  ( 1 / 2 ) e. CC
77 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 ) ) )
78 75 76 77 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 ) ) )
79 34 78 mpbid 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( T / _i ) / ( 2 x. _pi ) ) = ( 1 / 2 ) )
80 67 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( T / _i ) e. CC )
81 6 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( 2 x. _pi ) e. CC )
82 76 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( 1 / 2 ) e. CC )
83 72 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( 2 x. _pi ) =/= 0 )
84 80 81 82 83 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 ) ) )
85 79 84 mpbid 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( ( 2 x. _pi ) x. ( 1 / 2 ) ) = ( T / _i ) )
86 10 85 syl5reqr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> ( T / _i ) = _pi )
87 62 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> T e. CC )
88 63 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> _i e. CC )
89 5 a1i 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ -u 1 < N ) -> _pi e. CC )
90 65 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 5 63 mulneg1i 
 |-  ( -u _pi x. _i ) = -u ( _pi x. _i )
96 5 63 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 76 6 mulneg1i 
 |-  ( -u ( 1 / 2 ) x. ( 2 x. _pi ) ) = -u ( ( 1 / 2 ) x. ( 2 x. _pi ) )
100 35 4 7 divcan1i 
 |-  ( ( 1 / 2 ) x. 2 ) = 1
101 100 oveq1i 
 |-  ( ( ( 1 / 2 ) x. 2 ) x. _pi ) = ( 1 x. _pi )
102 76 4 5 mulassi 
 |-  ( ( ( 1 / 2 ) x. 2 ) x. _pi ) = ( ( 1 / 2 ) x. ( 2 x. _pi ) )
103 5 mulid2i 
 |-  ( 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 35 76 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 74 76 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 67 68 73 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 62 64 66 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 35 35 132 mp2an 
 |-  -u ( 1 + 1 ) = ( -u 1 - 1 )
134 131 133 eqtri 
 |-  -u 2 = ( -u 1 - 1 )
135 11 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 16 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 28 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 ) } )