Proof of Theorem ang180lem2
Step | Hyp | Ref
| Expression |
1 | | 2cn 10680 |
. . . . . . 7
 |
2 | | 1re 9642 |
. . . . . . . . 9
 |
3 | 2 | rehalfcli 10861 |
. . . . . . . 8
   |
4 | 3 | recni 9655 |
. . . . . . 7
   |
5 | 1, 4 | negsubdii 9960 |
. . . . . 6
           |
6 | | 4d2e2 10766 |
. . . . . . . . 9
   |
7 | 6 | oveq1i 6300 |
. . . . . . . 8
           |
8 | | 4cn 10687 |
. . . . . . . . . 10
 |
9 | | ax-1cn 9597 |
. . . . . . . . . 10
 |
10 | | 2cnne0 10824 |
. . . . . . . . . 10
   |
11 | | divsubdir 10303 |
. . . . . . . . . 10
 
               |
12 | 8, 9, 10, 11 | mp3an 1364 |
. . . . . . . . 9
           |
13 | | 3cn 10684 |
. . . . . . . . . . 11
 |
14 | 9, 13 | addcomi 9824 |
. . . . . . . . . . . 12
     |
15 | | df-4 10670 |
. . . . . . . . . . . 12
   |
16 | 14, 15 | eqtr4i 2476 |
. . . . . . . . . . 11
   |
17 | 8, 9, 13, 16 | subaddrii 9964 |
. . . . . . . . . 10
   |
18 | 17 | oveq1i 6300 |
. . . . . . . . 9
       |
19 | 12, 18 | eqtr3i 2475 |
. . . . . . . 8
         |
20 | 7, 19 | eqtr3i 2475 |
. . . . . . 7
       |
21 | 20 | negeqi 9868 |
. . . . . 6
         |
22 | 5, 21 | eqtr3i 2475 |
. . . . 5
         |
23 | | 3re 10683 |
. . . . . . . . . . . . 13
 |
24 | 23 | rehalfcli 10861 |
. . . . . . . . . . . 12
   |
25 | 24 | recni 9655 |
. . . . . . . . . . 11
   |
26 | | picn 23414 |
. . . . . . . . . . 11
 |
27 | 25, 1, 26 | mulassi 9652 |
. . . . . . . . . 10
             |
28 | | 2ne0 10702 |
. . . . . . . . . . . 12
 |
29 | 13, 1, 28 | divcan1i 10351 |
. . . . . . . . . . 11
     |
30 | 29 | oveq1i 6300 |
. . . . . . . . . 10
         |
31 | 27, 30 | eqtr3i 2475 |
. . . . . . . . 9
         |
32 | 31 | negeqi 9868 |
. . . . . . . 8
           |
33 | | 2re 10679 |
. . . . . . . . . . 11
 |
34 | | pire 23413 |
. . . . . . . . . . 11
 |
35 | 33, 34 | remulcli 9657 |
. . . . . . . . . 10
   |
36 | 35 | recni 9655 |
. . . . . . . . 9
   |
37 | 25, 36 | mulneg1i 10064 |
. . . . . . . 8
               |
38 | 13, 26 | mulneg2i 10065 |
. . . . . . . 8
       |
39 | 32, 37, 38 | 3eqtr4i 2483 |
. . . . . . 7
           |
40 | 34 | renegcli 9935 |
. . . . . . . . . . . 12
  |
41 | 33, 40 | remulcli 9657 |
. . . . . . . . . . 11
    |
42 | 41 | a1i 11 |
. . . . . . . . . 10
     
  |
43 | 40 | a1i 11 |
. . . . . . . . . 10
      |
44 | | simp1 1008 |
. . . . . . . . . . . . . . 15
     |
45 | | subcl 9874 |
. . . . . . . . . . . . . . 15
 
     |
46 | 9, 44, 45 | sylancr 669 |
. . . . . . . . . . . . . 14
       |
47 | | simp3 1010 |
. . . . . . . . . . . . . . . 16
     |
48 | 47 | necomd 2679 |
. . . . . . . . . . . . . . 15
     |
49 | | subeq0 9900 |
. . . . . . . . . . . . . . . . 17
 
       |
50 | 9, 44, 49 | sylancr 669 |
. . . . . . . . . . . . . . . 16
         |
51 | 50 | necon3bid 2668 |
. . . . . . . . . . . . . . 15
         |
52 | 48, 51 | mpbird 236 |
. . . . . . . . . . . . . 14
       |
53 | 46, 52 | reccld 10376 |
. . . . . . . . . . . . 13
         |
54 | 46, 52 | recne0d 10377 |
. . . . . . . . . . . . 13
         |
55 | 53, 54 | logcld 23520 |
. . . . . . . . . . . 12
             |
56 | | subcl 9874 |
. . . . . . . . . . . . . . 15
 
     |
57 | 44, 9, 56 | sylancl 668 |
. . . . . . . . . . . . . 14
   
   |
58 | | simp2 1009 |
. . . . . . . . . . . . . 14
     |
59 | 57, 44, 58 | divcld 10383 |
. . . . . . . . . . . . 13
         |
60 | | subeq0 9900 |
. . . . . . . . . . . . . . . . 17
 
       |
61 | 44, 9, 60 | sylancl 668 |
. . . . . . . . . . . . . . . 16
         |
62 | 61 | necon3bid 2668 |
. . . . . . . . . . . . . . 15
         |
63 | 47, 62 | mpbird 236 |
. . . . . . . . . . . . . 14
   
   |
64 | 57, 44, 63, 58 | divne0d 10399 |
. . . . . . . . . . . . 13
         |
65 | 59, 64 | logcld 23520 |
. . . . . . . . . . . 12
             |
66 | 55, 65 | addcld 9662 |
. . . . . . . . . . 11
                       |
67 | 66 | imcld 13258 |
. . . . . . . . . 10
                           |
68 | | logcl 23518 |
. . . . . . . . . . . 12
         |
69 | 68 | 3adant3 1028 |
. . . . . . . . . . 11
         |
70 | 69 | imcld 13258 |
. . . . . . . . . 10
             |
71 | 55 | imcld 13258 |
. . . . . . . . . . . 12
                 |
72 | 65 | imcld 13258 |
. . . . . . . . . . . 12
                 |
73 | 53, 54 | logimcld 23521 |
. . . . . . . . . . . . 13
                                |
74 | 73 | simpld 461 |
. . . . . . . . . . . 12
                  |
75 | 59, 64 | logimcld 23521 |
. . . . . . . . . . . . 13
                                |
76 | 75 | simpld 461 |
. . . . . . . . . . . 12
                  |
77 | 43, 43, 71, 72, 74, 76 | lt2addd 10236 |
. . . . . . . . . . 11
                                   |
78 | | negpicn 23417 |
. . . . . . . . . . . . 13
  |
79 | 78 | 2timesi 10730 |
. . . . . . . . . . . 12
        |
80 | 79 | a1i 11 |
. . . . . . . . . . 11
     
      |
81 | 55, 65 | imaddd 13278 |
. . . . . . . . . . 11
                                                     |
82 | 77, 80, 81 | 3brtr4d 4433 |
. . . . . . . . . 10
                              |
83 | | logimcl 23519 |
. . . . . . . . . . . 12
                        |
84 | 83 | 3adant3 1028 |
. . . . . . . . . . 11
                        |
85 | 84 | simpld 461 |
. . . . . . . . . 10
              |
86 | 42, 43, 67, 70, 82, 85 | lt2addd 10236 |
. . . . . . . . 9
      
                                    |
87 | | df-3 10669 |
. . . . . . . . . . . 12
   |
88 | 87 | oveq1i 6300 |
. . . . . . . . . . 11
         |
89 | 1, 9, 78 | adddiri 9654 |
. . . . . . . . . . 11
              |
90 | 78 | mulid2i 9646 |
. . . . . . . . . . . 12
     |
91 | 90 | oveq2i 6301 |
. . . . . . . . . . 11
   
           |
92 | 88, 89, 91 | 3eqtri 2477 |
. . . . . . . . . 10
          |
93 | 92 | a1i 11 |
. . . . . . . . 9
     
   
    |
94 | | ang180lem1.2 |
. . . . . . . . . . 11
                         |
95 | 94 | fveq2i 5868 |
. . . . . . . . . 10
                                 |
96 | 66, 69 | imaddd 13278 |
. . . . . . . . . 10
                                                                 |
97 | 95, 96 | syl5eq 2497 |
. . . . . . . . 9
                                         |
98 | 86, 93, 97 | 3brtr4d 4433 |
. . . . . . . 8
            |
99 | 66, 69 | addcld 9662 |
. . . . . . . . . . 11
                             |
100 | 94, 99 | syl5eqel 2533 |
. . . . . . . . . 10
     |
101 | | imval 13170 |
. . . . . . . . . 10
        
    |
102 | 100, 101 | syl 17 |
. . . . . . . . 9
          
    |
103 | | ang.1 |
. . . . . . . . . . . 12
                      |
104 | | ang180lem1.3 |
. . . . . . . . . . . 12
           |
105 | 103, 94, 104 | ang180lem1 23738 |
. . . . . . . . . . 11
   
     |
106 | 105 | simprd 465 |
. . . . . . . . . 10
       |
107 | 106 | rered 13287 |
. . . . . . . . 9
             |
108 | 102, 107 | eqtrd 2485 |
. . . . . . . 8
           |
109 | 98, 108 | breqtrd 4427 |
. . . . . . 7
          |
110 | 39, 109 | syl5eqbr 4436 |
. . . . . 6
              |
111 | 24 | renegcli 9935 |
. . . . . . . 8
    |
112 | 111 | a1i 11 |
. . . . . . 7
        |
113 | 35 | a1i 11 |
. . . . . . 7
       |
114 | | 2pos 10701 |
. . . . . . . . 9
 |
115 | | pipos 23415 |
. . . . . . . . 9
 |
116 | 33, 34, 114, 115 | mulgt0ii 9768 |
. . . . . . . 8
   |
117 | 116 | a1i 11 |
. . . . . . 7
       |
118 | | ltmuldiv 10478 |
. . . . . . 7
      
  
                          |
119 | 112, 106,
113, 117, 118 | syl112anc 1272 |
. . . . . 6
            
     
      |
120 | 110, 119 | mpbid 214 |
. . . . 5
              |
121 | 22, 120 | syl5eqbr 4436 |
. . . 4
                |
122 | 33 | renegcli 9935 |
. . . . . 6
  |
123 | 122 | a1i 11 |
. . . . 5
      |
124 | 3 | a1i 11 |
. . . . 5
       |
125 | 35, 116 | gt0ne0ii 10150 |
. . . . . . 7
   |
126 | 125 | a1i 11 |
. . . . . 6
       |
127 | 106, 113,
126 | redivcld 10435 |
. . . . 5
           |
128 | 123, 124,
127 | ltaddsubd 10213 |
. . . 4
              
              |
129 | 121, 128 | mpbid 214 |
. . 3
                |
130 | 129, 104 | syl6breqr 4443 |
. 2
      |
131 | 34 | a1i 11 |
. . . . . . . . . 10
     |
132 | 73 | simprd 465 |
. . . . . . . . . . . 12
                 |
133 | 75 | simprd 465 |
. . . . . . . . . . . 12
                 |
134 | 71, 72, 131, 131, 132, 133 | le2addd 10232 |
. . . . . . . . . . 11
                                 |
135 | 26 | 2timesi 10730 |
. . . . . . . . . . . 12
     |
136 | 135 | a1i 11 |
. . . . . . . . . . 11
         |
137 | 134, 81, 136 | 3brtr4d 4433 |
. . . . . . . . . 10
                             |
138 | 84 | simprd 465 |
. . . . . . . . . 10
             |
139 | 67, 70, 113, 131, 137, 138 | le2addd 10232 |
. . . . . . . . 9
                                     
   |
140 | 108, 97 | eqtr3d 2487 |
. . . . . . . . 9
                                       |
141 | 87 | oveq1i 6300 |
. . . . . . . . . . 11
       |
142 | 1, 9, 26 | adddiri 9654 |
. . . . . . . . . . 11
           |
143 | 26 | mulid2i 9646 |
. . . . . . . . . . . 12
   |
144 | 143 | oveq2i 6301 |
. . . . . . . . . . 11
           |
145 | 141, 142,
144 | 3eqtri 2477 |
. . . . . . . . . 10
       |
146 | 145 | a1i 11 |
. . . . . . . . 9
           |
147 | 139, 140,
146 | 3brtr4d 4433 |
. . . . . . . 8
         |
148 | 36 | subid1i 9946 |
. . . . . . . . . 10
       |
149 | 148, 125 | eqnetri 2694 |
. . . . . . . . 9
     |
150 | | negsub 9922 |
. . . . . . . . . . . . . . . . . . . 20
 
        |
151 | 9, 44, 150 | sylancr 669 |
. . . . . . . . . . . . . . . . . . 19
          |
152 | 151 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
        
       |
153 | | 1rp 11306 |
. . . . . . . . . . . . . . . . . . 19
 |
154 | 146, 140 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                                           |
155 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
156 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
157 | 67 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                           |
158 | 70 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             |
159 | 155, 156,
157, 158 | addsub4d 10033 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
                                                                         |
160 | 154, 159 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
                                           |
161 | 160 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
                                              |
162 | 23, 34 | remulcli 9657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
163 | 162 | recni 9655 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
164 | | ax-icn 9598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
165 | 164 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
166 | | ine0 10054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
167 | 166 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
168 | 100, 165,
167 | divcld 10383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
169 | | subeq0 9900 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
         
       |
170 | 163, 168,
169 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         
       |
171 | 170 | biimpar 488 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
        |
172 | 161, 171 | eqtr3d 2487 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
   
                                    |
173 | | resubcl 9938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                         
                         |
174 | 35, 67, 173 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
                         |
175 | | subge0 10127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
                       
                                                     |
176 | 35, 67, 175 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                                                     |
177 | 137, 176 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                               |
178 | | resubcl 9938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           
           |
179 | 34, 70, 178 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
           |
180 | | subge0 10127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           
                 
   |
181 | 34, 70, 180 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                 
   |
182 | 138, 181 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               |
183 | | add20 10126 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                                                                                                                                 
             |
184 | 174, 177,
179, 182, 183 | syl22anc 1269 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                                                     
             |
185 | 184 | biimpa 487 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                                      
            |
186 | 172, 185 | syldan 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
   
                                    |
187 | 186 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . 22
        
            |
188 | 158 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
          |
189 | | subeq0 9900 |
. . . . . . . . . . . . . . . . . . . . . . 23
                     
           |
190 | 26, 188, 189 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . 22
        
 
        
           |
191 | 187, 190 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . 21
        
          |
192 | 191 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . 20
        
          |
193 | | lognegb 23539 |
. . . . . . . . . . . . . . . . . . . . . 22
                |
194 | 193 | 3adant3 1028 |
. . . . . . . . . . . . . . . . . . . . 21
    
           |
195 | 194 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
        
             |
196 | 192, 195 | mpbird 236 |
. . . . . . . . . . . . . . . . . . 19
        
   |
197 | | rpaddcl 11323 |
. . . . . . . . . . . . . . . . . . 19
         |
198 | 153, 196,
197 | sylancr 669 |
. . . . . . . . . . . . . . . . . 18
        
     |
199 | 152, 198 | eqeltrrd 2530 |
. . . . . . . . . . . . . . . . 17
        
    |
200 | 199 | rpreccld 11351 |
. . . . . . . . . . . . . . . 16
        
      |
201 | 200 | relogcld 23572 |
. . . . . . . . . . . . . . 15
        
          |
202 | | negsubdi2 9933 |
. . . . . . . . . . . . . . . . . . . . 21
 
        |
203 | 44, 9, 202 | sylancl 668 |
. . . . . . . . . . . . . . . . . . . 20
    
     |
204 | 203 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . 19
                |
205 | 57, 44, 58 | div2negd 10398 |
. . . . . . . . . . . . . . . . . . 19
               |
206 | 204, 205 | eqtr3d 2487 |
. . . . . . . . . . . . . . . . . 18
              |
207 | 206 | adantr 467 |
. . . . . . . . . . . . . . . . 17
        
           |
208 | 199, 196 | rpdivcld 11358 |
. . . . . . . . . . . . . . . . 17
        
       |
209 | 207, 208 | eqeltrrd 2530 |
. . . . . . . . . . . . . . . 16
        
 
    |
210 | 209 | relogcld 23572 |
. . . . . . . . . . . . . . 15
        
          |
211 | 201, 210 | readdcld 9670 |
. . . . . . . . . . . . . 14
        
                    |
212 | 211 | reim0d 13288 |
. . . . . . . . . . . . 13
        
                        |
213 | 212 | oveq2d 6306 |
. . . . . . . . . . . 12
        
                                |
214 | 186 | simpld 461 |
. . . . . . . . . . . 12
        
                            |
215 | 213, 214 | eqtr3d 2487 |
. . . . . . . . . . 11
        
      |
216 | 215 | ex 436 |
. . . . . . . . . 10
     
    
    |
217 | 216 | necon3d 2645 |
. . . . . . . . 9
               |
218 | 149, 217 | mpi 20 |
. . . . . . . 8
         |
219 | | ltlen 9735 |
. . . . . . . . 9
   
     
 
             |
220 | 106, 162,
219 | sylancl 668 |
. . . . . . . 8
       
             |
221 | 147, 218,
220 | mpbir2and 933 |
. . . . . . 7
         |
222 | 221, 31 | syl6breqr 4443 |
. . . . . 6
             |
223 | 24 | a1i 11 |
. . . . . . 7
       |
224 | | ltdivmul2 10482 |
. . . . . . 7
   
    
                        |
225 | 106, 223,
113, 117, 224 | syl112anc 1272 |
. . . . . 6
      
    
           |
226 | 222, 225 | mpbird 236 |
. . . . 5
             |
227 | 87 | oveq1i 6300 |
. . . . . 6
       |
228 | 1, 9, 1, 28 | divdiri 10364 |
. . . . . 6
           |
229 | | 2div2e1 10732 |
. . . . . . 7
   |
230 | 229 | oveq1i 6300 |
. . . . . 6
           |
231 | 227, 228,
230 | 3eqtri 2477 |
. . . . 5
       |
232 | 226, 231 | syl6breq 4442 |
. . . 4
               |
233 | 2 | a1i 11 |
. . . . 5
     |
234 | 127, 124,
233 | ltsubaddd 10209 |
. . . 4
                           |
235 | 232, 234 | mpbird 236 |
. . 3
      
        |
236 | 104, 235 | syl5eqbr 4436 |
. 2
     |
237 | 130, 236 | jca 535 |
1
        |