Proof of Theorem dirkertrigeqlem3
Step | Hyp | Ref
| Expression |
1 | | dirkertrigeqlem3.a |
. . . . . . . . . . . . 13
       |
2 | 1 | a1i 11 |
. . . . . . . . . . . 12
 
             |
3 | 2 | oveq2d 6306 |
. . . . . . . . . . 11
 
                 |
4 | | elfzelz 11800 |
. . . . . . . . . . . . . 14
       |
5 | 4 | zcnd 11041 |
. . . . . . . . . . . . 13
       |
6 | 5 | adantl 468 |
. . . . . . . . . . . 12
 
       |
7 | | 2cnd 10682 |
. . . . . . . . . . . . . . 15
 
       |
8 | | dirkertrigeqlem3.k |
. . . . . . . . . . . . . . . . 17
   |
9 | 8 | zcnd 11041 |
. . . . . . . . . . . . . . . 16
   |
10 | 9 | adantr 467 |
. . . . . . . . . . . . . . 15
 
       |
11 | 7, 10 | mulcld 9663 |
. . . . . . . . . . . . . 14
 
         |
12 | | 1cnd 9659 |
. . . . . . . . . . . . . 14
 
       |
13 | 11, 12 | addcld 9662 |
. . . . . . . . . . . . 13
 
           |
14 | | picn 23414 |
. . . . . . . . . . . . . 14
 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . 13
 
       |
16 | 13, 15 | mulcld 9663 |
. . . . . . . . . . . 12
 
             |
17 | 6, 16 | mulcomd 9664 |
. . . . . . . . . . 11
 
                       |
18 | 13, 15, 6 | mulassd 9666 |
. . . . . . . . . . . 12
 
           
           |
19 | 15, 6 | mulcld 9663 |
. . . . . . . . . . . . 13
 
     
   |
20 | 11, 12, 19 | adddird 9668 |
. . . . . . . . . . . 12
 
                     
     |
21 | 11, 19 | mulcld 9663 |
. . . . . . . . . . . . . 14
 
             |
22 | 12, 19 | mulcld 9663 |
. . . . . . . . . . . . . 14
 
           |
23 | 21, 22 | addcomd 9835 |
. . . . . . . . . . . . 13
 
         
               
     |
24 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . 17
       |
25 | 24, 5 | mulcld 9663 |
. . . . . . . . . . . . . . . 16
     
   |
26 | 25 | mulid2d 9661 |
. . . . . . . . . . . . . . 15
             |
27 | 26 | adantl 468 |
. . . . . . . . . . . . . 14
 
             |
28 | 7, 10, 15, 6 | mul4d 9845 |
. . . . . . . . . . . . . . 15
 
                   |
29 | 7, 15 | mulcld 9663 |
. . . . . . . . . . . . . . . 16
 
         |
30 | 10, 6 | mulcld 9663 |
. . . . . . . . . . . . . . . 16
 
     
   |
31 | 29, 30 | mulcomd 9664 |
. . . . . . . . . . . . . . 15
 
       
           |
32 | 28, 31 | eqtrd 2485 |
. . . . . . . . . . . . . 14
 
                   |
33 | 27, 32 | oveq12d 6308 |
. . . . . . . . . . . . 13
 
       
                     |
34 | 23, 33 | eqtrd 2485 |
. . . . . . . . . . . 12
 
         
                   |
35 | 18, 20, 34 | 3eqtrd 2489 |
. . . . . . . . . . 11
 
           
             |
36 | 3, 17, 35 | 3eqtrd 2489 |
. . . . . . . . . 10
 
                   |
37 | 36 | fveq2d 5869 |
. . . . . . . . 9
 
                           |
38 | 8 | adantr 467 |
. . . . . . . . . . 11
 
       |
39 | 4 | adantl 468 |
. . . . . . . . . . 11
 
       |
40 | 38, 39 | zmulcld 11046 |
. . . . . . . . . 10
 
     
   |
41 | | cosper 23437 |
. . . . . . . . . 10
    
                        |
42 | 19, 40, 41 | syl2anc 667 |
. . . . . . . . 9
 
                      
    |
43 | 37, 42 | eqtrd 2485 |
. . . . . . . 8
 
              
    |
44 | 43 | sumeq2dv 13769 |
. . . . . . 7
 
                    
    |
45 | 44 | oveq2d 6306 |
. . . . . 6
                                   |
46 | 45 | oveq1d 6305 |
. . . . 5
     
                          
      |
47 | 46 | adantr 467 |
. . . 4
 
  
                 
             
      |
48 | | dirkertrigeqlem3.n |
. . . . . . . . . . . . . 14
   |
49 | 48 | nncnd 10625 |
. . . . . . . . . . . . 13
   |
50 | | 2cnd 10682 |
. . . . . . . . . . . . 13
   |
51 | | 2ne0 10702 |
. . . . . . . . . . . . . 14
 |
52 | 51 | a1i 11 |
. . . . . . . . . . . . 13
   |
53 | 49, 50, 52 | divcan2d 10385 |
. . . . . . . . . . . 12
       |
54 | 53 | eqcomd 2457 |
. . . . . . . . . . 11
       |
55 | 54 | oveq2d 6306 |
. . . . . . . . . 10
               |
56 | 55 | sumeq1d 13767 |
. . . . . . . . 9
 
                        
    |
57 | 56 | adantr 467 |
. . . . . . . 8
 
  
         
               
    |
58 | 14 | a1i 11 |
. . . . . . . . . . . . 13
        
  |
59 | | elfzelz 11800 |
. . . . . . . . . . . . . 14
        
  |
60 | 59 | zcnd 11041 |
. . . . . . . . . . . . 13
        
  |
61 | 58, 60 | mulcomd 9664 |
. . . . . . . . . . . 12
        
      |
62 | 61 | fveq2d 5869 |
. . . . . . . . . . 11
        
              |
63 | 62 | rgen 2747 |
. . . . . . . . . 10
             
         |
64 | 63 | a1i 11 |
. . . . . . . . 9
 
  
             
          |
65 | 64 | sumeq2d 13768 |
. . . . . . . 8
 
  
             
                    |
66 | | simpr 463 |
. . . . . . . . . . 11
 
  
    |
67 | 48 | nnred 10624 |
. . . . . . . . . . . . 13
   |
68 | 67 | adantr 467 |
. . . . . . . . . . . 12
 
  
  |
69 | | 2rp 11307 |
. . . . . . . . . . . 12
 |
70 | | mod0 12103 |
. . . . . . . . . . . 12
 
         |
71 | 68, 69, 70 | sylancl 668 |
. . . . . . . . . . 11
 
  
        |
72 | 66, 71 | mpbid 214 |
. . . . . . . . . 10
 
  
    |
73 | | 2re 10679 |
. . . . . . . . . . . . 13
 |
74 | 73 | a1i 11 |
. . . . . . . . . . . 12
   |
75 | 48 | nngt0d 10653 |
. . . . . . . . . . . 12
   |
76 | | 2pos 10701 |
. . . . . . . . . . . . 13
 |
77 | 76 | a1i 11 |
. . . . . . . . . . . 12
   |
78 | 67, 74, 75, 77 | divgt0d 10542 |
. . . . . . . . . . 11
     |
79 | 78 | adantr 467 |
. . . . . . . . . 10
 
  
    |
80 | | elnnz 10947 |
. . . . . . . . . 10
  
        |
81 | 72, 79, 80 | sylanbrc 670 |
. . . . . . . . 9
 
  
    |
82 | | dirkertrigeqlem1 37960 |
. . . . . . . . 9
                     |
83 | 81, 82 | syl 17 |
. . . . . . . 8
 
  
                  |
84 | 57, 65, 83 | 3eqtrd 2489 |
. . . . . . 7
 
  
         
    |
85 | 84 | oveq2d 6306 |
. . . . . 6
 
  
            
         |
86 | | halfcn 10829 |
. . . . . . 7
   |
87 | 86 | addid1i 9820 |
. . . . . 6
       |
88 | 85, 87 | syl6eq 2501 |
. . . . 5
 
  
            
       |
89 | 88 | oveq1d 6305 |
. . . 4
 
  
             
   
      |
90 | | ax-1cn 9597 |
. . . . . 6
 |
91 | | 2cnne0 10824 |
. . . . . 6
   |
92 | | pire 23413 |
. . . . . . . 8
 |
93 | | pipos 23415 |
. . . . . . . 8
 |
94 | 92, 93 | gt0ne0ii 10150 |
. . . . . . 7
 |
95 | 14, 94 | pm3.2i 457 |
. . . . . 6
   |
96 | | divdiv1 10318 |
. . . . . 6
                 |
97 | 90, 91, 95, 96 | mp3an 1364 |
. . . . 5
         |
98 | 97 | a1i 11 |
. . . 4
 
  
          |
99 | 47, 89, 98 | 3eqtrd 2489 |
. . 3
 
  
                 
      |
100 | 1 | oveq2i 6301 |
. . . . . . . . . 10
                   |
101 | 100 | a1i 11 |
. . . . . . . . 9
                     |
102 | 86 | a1i 11 |
. . . . . . . . . . 11
     |
103 | 49, 102 | addcld 9662 |
. . . . . . . . . 10
       |
104 | 50, 9 | mulcld 9663 |
. . . . . . . . . . 11
     |
105 | | peano2cn 9805 |
. . . . . . . . . . 11
         |
106 | 104, 105 | syl 17 |
. . . . . . . . . 10
       |
107 | 14 | a1i 11 |
. . . . . . . . . 10
   |
108 | 103, 106,
107 | mulassd 9666 |
. . . . . . . . 9
            
 
            |
109 | | 1cnd 9659 |
. . . . . . . . . . . . . 14
   |
110 | 49, 102, 104, 109 | muladdd 10076 |
. . . . . . . . . . . . 13
                                   |
111 | 49, 50, 9 | mul12d 9842 |
. . . . . . . . . . . . . . 15
           |
112 | 102 | mulid2d 9661 |
. . . . . . . . . . . . . . 15
         |
113 | 111, 112 | oveq12d 6308 |
. . . . . . . . . . . . . 14
                     |
114 | 49 | mulid1d 9660 |
. . . . . . . . . . . . . . 15
     |
115 | 50, 9 | mulcomd 9664 |
. . . . . . . . . . . . . . . . 17
       |
116 | 115 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
               |
117 | 9, 50, 102 | mulassd 9666 |
. . . . . . . . . . . . . . . 16
               |
118 | | 2cn 10680 |
. . . . . . . . . . . . . . . . . . 19
 |
119 | 118, 51 | recidi 10338 |
. . . . . . . . . . . . . . . . . 18
     |
120 | 119 | oveq2i 6301 |
. . . . . . . . . . . . . . . . 17
         |
121 | 9 | mulid1d 9660 |
. . . . . . . . . . . . . . . . 17
     |
122 | 120, 121 | syl5eq 2497 |
. . . . . . . . . . . . . . . 16
         |
123 | 116, 117,
122 | 3eqtrd 2489 |
. . . . . . . . . . . . . . 15
         |
124 | 114, 123 | oveq12d 6308 |
. . . . . . . . . . . . . 14
               |
125 | 113, 124 | oveq12d 6308 |
. . . . . . . . . . . . 13
                          
          |
126 | 49, 9 | mulcld 9663 |
. . . . . . . . . . . . . . 15
     |
127 | 50, 126 | mulcld 9663 |
. . . . . . . . . . . . . 14
  
    |
128 | 49, 9 | addcld 9662 |
. . . . . . . . . . . . . 14
     |
129 | 127, 102,
128 | addassd 9665 |
. . . . . . . . . . . . 13
                           |
130 | 110, 125,
129 | 3eqtrd 2489 |
. . . . . . . . . . . 12
                         |
131 | 102, 128 | addcld 9662 |
. . . . . . . . . . . . 13
         |
132 | 127, 131 | addcomd 9835 |
. . . . . . . . . . . 12
                           |
133 | 50, 126 | mulcomd 9664 |
. . . . . . . . . . . . 13
  
        |
134 | 133 | oveq2d 6306 |
. . . . . . . . . . . 12
                           |
135 | 130, 132,
134 | 3eqtrd 2489 |
. . . . . . . . . . 11
                         |
136 | 135 | oveq1d 6305 |
. . . . . . . . . 10
            
                |
137 | 126, 50 | mulcld 9663 |
. . . . . . . . . . 11
       |
138 | 131, 137,
107 | adddird 9668 |
. . . . . . . . . 10
              
                  |
139 | 126, 50, 107 | mulassd 9666 |
. . . . . . . . . . 11
      
 
      |
140 | 139 | oveq2d 6306 |
. . . . . . . . . 10
                                   |
141 | 136, 138,
140 | 3eqtrd 2489 |
. . . . . . . . 9
            
                  |
142 | 101, 108,
141 | 3eqtr2d 2491 |
. . . . . . . 8
                         |
143 | 142 | fveq2d 5869 |
. . . . . . 7
                                 |
144 | 131, 107 | mulcld 9663 |
. . . . . . . 8
        
  |
145 | 48 | nnzd 11039 |
. . . . . . . . 9
   |
146 | 145, 8 | zmulcld 11046 |
. . . . . . . 8
     |
147 | | sinper 23436 |
. . . . . . . 8
         

                                    |
148 | 144, 146,
147 | syl2anc 667 |
. . . . . . 7
            
 
                    |
149 | 102, 128 | addcomd 9835 |
. . . . . . . . . 10
               |
150 | 49, 9, 102 | addassd 9665 |
. . . . . . . . . 10
               |
151 | 9, 102 | addcld 9662 |
. . . . . . . . . . 11
       |
152 | 49, 151 | addcomd 9835 |
. . . . . . . . . 10
               |
153 | 149, 150,
152 | 3eqtrd 2489 |
. . . . . . . . 9
               |
154 | 153 | oveq1d 6305 |
. . . . . . . 8
        
          |
155 | 154 | fveq2d 5869 |
. . . . . . 7
                           |
156 | 143, 148,
155 | 3eqtrd 2489 |
. . . . . 6
                         |
157 | 1 | a1i 11 |
. . . . . . . . . 10
         |
158 | 157 | oveq1d 6305 |
. . . . . . . . 9
             |
159 | 106, 107,
50, 52 | div23d 10420 |
. . . . . . . . 9
                   |
160 | 104, 109,
50, 52 | divdird 10421 |
. . . . . . . . . . 11
                 |
161 | 9, 50, 52 | divcan3d 10388 |
. . . . . . . . . . . 12
       |
162 | 161 | oveq1d 6305 |
. . . . . . . . . . 11
               |
163 | 160, 162 | eqtrd 2485 |
. . . . . . . . . 10
             |
164 | 163 | oveq1d 6305 |
. . . . . . . . 9
        
 
      |
165 | 158, 159,
164 | 3eqtrd 2489 |
. . . . . . . 8
           |
166 | 165 | fveq2d 5869 |
. . . . . . 7
                   |
167 | 166 | oveq2d 6306 |
. . . . . 6
                           |
168 | 156, 167 | oveq12d 6308 |
. . . . 5
                                                     |
169 | 168 | adantr 467 |
. . . 4
 
  
                                                    |
170 | 151, 49, 107 | adddird 9668 |
. . . . . . 7
        
            |
171 | 170 | fveq2d 5869 |
. . . . . 6
                             |
172 | 171 | oveq1d 6305 |
. . . . 5
                                       
                     |
173 | 172 | adantr 467 |
. . . 4
 
  
                                                            |
174 | 49 | halfcld 10857 |
. . . . . . . . . . . . . 14
     |
175 | 50, 174 | mulcomd 9664 |
. . . . . . . . . . . . 13
           |
176 | 53, 175 | eqtr3d 2487 |
. . . . . . . . . . . 12
       |
177 | 176 | oveq1d 6305 |
. . . . . . . . . . 11
  
        |
178 | 174, 50, 107 | mulassd 9666 |
. . . . . . . . . . 11
      
        |
179 | 177, 178 | eqtrd 2485 |
. . . . . . . . . 10
  
        |
180 | 179 | oveq2d 6306 |
. . . . . . . . 9
                           |
181 | 180 | fveq2d 5869 |
. . . . . . . 8
          
             
          |
182 | 181 | adantr 467 |
. . . . . . 7
 
  
                                  |
183 | 9 | adantr 467 |
. . . . . . . . . 10
 
  
  |
184 | | 1cnd 9659 |
. . . . . . . . . . 11
 
  
  |
185 | 184 | halfcld 10857 |
. . . . . . . . . 10
 
  
    |
186 | 183, 185 | addcld 9662 |
. . . . . . . . 9
 
  
      |
187 | 14 | a1i 11 |
. . . . . . . . 9
 
  
  |
188 | 186, 187 | mulcld 9663 |
. . . . . . . 8
 
  
 
      |
189 | | sinper 23436 |
. . . . . . . 8
       
                                 |
190 | 188, 72, 189 | syl2anc 667 |
. . . . . . 7
 
  
                              |
191 | 182, 190 | eqtrd 2485 |
. . . . . 6
 
  
                          |
192 | 50, 107 | mulcld 9663 |
. . . . . . . 8
  
  |
193 | 151, 107 | mulcld 9663 |
. . . . . . . . 9
      
  |
194 | 193 | sincld 14184 |
. . . . . . . 8
             |
195 | 192, 194 | mulcomd 9664 |
. . . . . . 7
                               |
196 | 195 | adantr 467 |
. . . . . 6
 
  
                              |
197 | 191, 196 | oveq12d 6308 |
. . . . 5
 
  
                                                          |
198 | 94 | a1i 11 |
. . . . . . . . . . . 12
   |
199 | 151, 107,
198 | divcan4d 10389 |
. . . . . . . . . . 11
        
      |
200 | 8 | zred 11040 |
. . . . . . . . . . . . 13
   |
201 | 69 | a1i 11 |
. . . . . . . . . . . . . 14
   |
202 | 201 | rpreccld 11351 |
. . . . . . . . . . . . 13
     |
203 | 200, 202 | ltaddrpd 11371 |
. . . . . . . . . . . 12
       |
204 | | 1red 9658 |
. . . . . . . . . . . . . 14
   |
205 | 204 | rehalfcld 10859 |
. . . . . . . . . . . . 13
     |
206 | | halflt1 10831 |
. . . . . . . . . . . . . 14
   |
207 | 206 | a1i 11 |
. . . . . . . . . . . . 13
  
  |
208 | 205, 204,
200, 207 | ltadd2dd 9794 |
. . . . . . . . . . . 12
         |
209 | | btwnnz 11012 |
. . . . . . . . . . . 12
      
            |
210 | 8, 203, 208, 209 | syl3anc 1268 |
. . . . . . . . . . 11
       |
211 | 199, 210 | eqneltrd 2548 |
. . . . . . . . . 10
        
  |
212 | | sineq0 23476 |
. . . . . . . . . . 11
                             |
213 | 193, 212 | syl 17 |
. . . . . . . . . 10
                       |
214 | 211, 213 | mtbird 303 |
. . . . . . . . 9
             |
215 | 214 | neqned 2631 |
. . . . . . . 8
             |
216 | 50, 107, 52, 198 | mulne0d 10264 |
. . . . . . . 8
     |
217 | 194, 194,
192, 215, 216 | divdiv1d 10414 |
. . . . . . 7
                                                       |
218 | 194, 215 | dividd 10381 |
. . . . . . . 8
                         |
219 | 218 | oveq1d 6305 |
. . . . . . 7
                                 |
220 | 217, 219 | eqtr3d 2487 |
. . . . . 6
                                 |
221 | 220 | adantr 467 |
. . . . 5
 
  
                                |
222 | 197, 221 | eqtrd 2485 |
. . . 4
 
  
                                    |
223 | 169, 173,
222 | 3eqtrrd 2490 |
. . 3
 
  
                            |
224 | 99, 223 | eqtrd 2485 |
. 2
 
  
                 
                        |
225 | 46 | adantr 467 |
. . 3
 
                    
                    |
226 | 145 | adantr 467 |
. . . . . . . . 9
 
     |
227 | | simpr 463 |
. . . . . . . . . 10
 
   
   |
228 | 227 | neqned 2631 |
. . . . . . . . 9
 
       |
229 | | oddfl 37487 |
. . . . . . . . 9
  
              |
230 | 226, 228,
229 | syl2anc 667 |
. . . . . . . 8
 
        
      |
231 | 230 | oveq2d 6306 |
. . . . . . 7
 
                       |
232 | 231 | sumeq1d 13767 |
. . . . . 6
 
            
                     
    |
233 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . 18
       |
234 | 233 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
               |
235 | | halffl 37513 |
. . . . . . . . . . . . . . . . 17
       |
236 | 234, 235 | syl6eq 2501 |
. . . . . . . . . . . . . . . 16
         |
237 | 236 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
             |
238 | | 2t0e0 10765 |
. . . . . . . . . . . . . . 15
   |
239 | 237, 238 | syl6eq 2501 |
. . . . . . . . . . . . . 14
           |
240 | 239 | oveq1d 6305 |
. . . . . . . . . . . . 13
               |
241 | 90 | addid2i 9821 |
. . . . . . . . . . . . 13
   |
242 | 240, 241 | syl6eq 2501 |
. . . . . . . . . . . 12
             |
243 | 242 | oveq2d 6306 |
. . . . . . . . . . 11
         
           |
244 | 243 | sumeq1d 13767 |
. . . . . . . . . 10
                    
           
    |
245 | | 1z 10967 |
. . . . . . . . . . . 12
 |
246 | | coscl 14181 |
. . . . . . . . . . . . 13
       |
247 | 14, 246 | ax-mp 5 |
. . . . . . . . . . . 12
     |
248 | | oveq2 6298 |
. . . . . . . . . . . . . . 15
 
     |
249 | 14 | mulid1i 9645 |
. . . . . . . . . . . . . . 15
   |
250 | 248, 249 | syl6eq 2501 |
. . . . . . . . . . . . . 14
 
   |
251 | 250 | fveq2d 5869 |
. . . . . . . . . . . . 13
             |
252 | 251 | fsum1 13808 |
. . . . . . . . . . . 12
                         |
253 | 245, 247,
252 | mp2an 678 |
. . . . . . . . . . 11
         
       |
254 | 253 | a1i 11 |
. . . . . . . . . 10
          
        |
255 | | cospi 23427 |
. . . . . . . . . . 11
      |
256 | 255 | a1i 11 |
. . . . . . . . . 10
        |
257 | 244, 254,
256 | 3eqtrd 2489 |
. . . . . . . . 9
                    
     |
258 | 257 | adantl 468 |
. . . . . . . 8
 
                    
     |
259 | | 2nn 10767 |
. . . . . . . . . . . . 13
 |
260 | 259 | a1i 11 |
. . . . . . . . . . . 12
 
   |
261 | 67 | rehalfcld 10859 |
. . . . . . . . . . . . . . 15
     |
262 | 261 | flcld 12034 |
. . . . . . . . . . . . . 14
         |
263 | 262 | adantr 467 |
. . . . . . . . . . . . 13
 
         |
264 | | 2div2e1 10732 |
. . . . . . . . . . . . . . 15
   |
265 | 73 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
   |
266 | 67 | adantr 467 |
. . . . . . . . . . . . . . . 16
 

  |
267 | 69 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
   |
268 | | neqne 37374 |
. . . . . . . . . . . . . . . . 17
   |
269 | | nnne1ge2 37505 |
. . . . . . . . . . . . . . . . 17
  
  |
270 | 48, 268, 269 | syl2an 480 |
. . . . . . . . . . . . . . . 16
 

  |
271 | 265, 266,
267, 270 | lediv1dd 11396 |
. . . . . . . . . . . . . . 15
 
  
    |
272 | 264, 271 | syl5eqbrr 4437 |
. . . . . . . . . . . . . 14
 

    |
273 | 261 | adantr 467 |
. . . . . . . . . . . . . . 15
 
     |
274 | | flge 12041 |
. . . . . . . . . . . . . . 15
   
   
         |
275 | 273, 245,
274 | sylancl 668 |
. . . . . . . . . . . . . 14
 
   
         |
276 | 272, 275 | mpbid 214 |
. . . . . . . . . . . . 13
 

        |
277 | | elnnz1 10963 |
. . . . . . . . . . . . 13
      
                |
278 | 263, 276,
277 | sylanbrc 670 |
. . . . . . . . . . . 12
 
         |
279 | 260, 278 | nnmulcld 10657 |
. . . . . . . . . . 11
 
           |
280 | | nnuz 11194 |
. . . . . . . . . . 11
     |
281 | 279, 280 | syl6eleq 2539 |
. . . . . . . . . 10
 
               |
282 | 14 | a1i 11 |
. . . . . . . . . . . 12
  
               
  |
283 | | elfzelz 11800 |
. . . . . . . . . . . . . 14
              
  |
284 | 283 | zcnd 11041 |
. . . . . . . . . . . . 13
              
  |
285 | 284 | adantl 468 |
. . . . . . . . . . . 12
  
               
  |
286 | 282, 285 | mulcld 9663 |
. . . . . . . . . . 11
  
               
    |
287 | 286 | coscld 14185 |
. . . . . . . . . 10
  
               
        |
288 | | oveq2 6298 |
. . . . . . . . . . 11
      
    
               |
289 | 288 | fveq2d 5869 |
. . . . . . . . . 10
      
             
              |
290 | 281, 287,
289 | fsump1 13817 |
. . . . . . . . 9
 
          
                              
                     |
291 | 14 | a1i 11 |
. . . . . . . . . . . . . 14
            
  |
292 | | elfzelz 11800 |
. . . . . . . . . . . . . . 15
            
  |
293 | 292 | zcnd 11041 |
. . . . . . . . . . . . . 14
            
  |
294 | 291, 293 | mulcomd 9664 |
. . . . . . . . . . . . 13
            
      |
295 | 294 | fveq2d 5869 |
. . . . . . . . . . . 12
            
              |
296 | 295 | sumeq2i 13765 |
. . . . . . . . . . 11
                 
                       |
297 | | dirkertrigeqlem1 37960 |
. . . . . . . . . . . 12
                             |
298 | 278, 297 | syl 17 |
. . . . . . . . . . 11
 
                       |
299 | 296, 298 | syl5eq 2497 |
. . . . . . . . . 10
 
                       |
300 | 262 | zcnd 11041 |
. . . . . . . . . . . . . . . 16
         |
301 | 50, 300 | mulcld 9663 |
. . . . . . . . . . . . . . 15
           |
302 | 107, 301,
109 | adddid 9667 |
. . . . . . . . . . . . . 14
                             |
303 | 107, 50, 300 | mul13d 37489 |
. . . . . . . . . . . . . . 15
                       |
304 | 249 | a1i 11 |
. . . . . . . . . . . . . . 15
     |
305 | 303, 304 | oveq12d 6308 |
. . . . . . . . . . . . . 14
                             |
306 | 300, 192 | mulcld 9663 |
. . . . . . . . . . . . . . 15
     
       |
307 | 306, 107 | addcomd 9835 |
. . . . . . . . . . . . . 14
            
              |
308 | 302, 305,
307 | 3eqtrd 2489 |
. . . . . . . . . . . . 13
                  
        |
309 | 308 | fveq2d 5869 |
. . . . . . . . . . . 12
    
                              |
310 | | cosper 23437 |
. . . . . . . . . . . . 13
                               |
311 | 107, 262,
310 | syl2anc 667 |
. . . . . . . . . . . 12
                       |
312 | 255 | a1i 11 |
. . . . . . . . . . . 12
    
   |
313 | 309, 311,
312 | 3eqtrd 2489 |
. . . . . . . . . . 11
    
               |
314 | 313 | adantr 467 |
. . . . . . . . . 10
 
    
               |
315 | 299, 314 | oveq12d 6308 |
. . . . . . . . 9
 
          
        
                        |
316 | | neg1cn 10713 |
. . . . . . . . . . 11
  |
317 | 316 | addid2i 9821 |
. . . . . . . . . 10
     |
318 | 317 | a1i 11 |
. . . . . . . . 9
 
       |
319 | 290, 315,
318 | 3eqtrd 2489 |
. . . . . . . 8
 
          
               |
320 | 258, 319 | pm2.61dan 800 |
. . . . . . 7
 
        
               |
321 | 320 | adantr 467 |
. . . . . 6
 
                      
     |
322 | 232, 321 | eqtrd 2485 |
. . . . 5
 
            
     |
323 | 322 | oveq2d 6306 |
. . . 4
 
               
          |
324 | 323 | oveq1d 6305 |
. . 3
 
                    
         |
325 | 168, 172 | eqtrd 2485 |
. . . . 5
                                 
                     |
326 | 325 | adantr 467 |
. . . 4
 
                                   
                     |
327 | 230 | oveq1d 6305 |
. . . . . . . . 9
 
   
               |
328 | 301, 109,
107 | adddird 9668 |
. . . . . . . . . . 11
       
    
                |
329 | 107 | mulid2d 9661 |
. . . . . . . . . . . 12
  
  |
330 | 329 | oveq2d 6306 |
. . . . . . . . . . 11
       
                     |
331 | 301, 107 | mulcld 9663 |
. . . . . . . . . . . 12
             |
332 | 331, 107 | addcomd 9835 |
. . . . . . . . . . 11
       
    
      
       |
333 | 328, 330,
332 | 3eqtrd 2489 |
. . . . . . . . . 10
       
    
      
       |
334 | 333 | adantr 467 |
. . . . . . . . 9
 
                             |
335 | 50, 300 | mulcomd 9664 |
. . . . . . . . . . . . 13
                   |
336 | 335 | oveq1d 6305 |
. . . . . . . . . . . 12
                       |
337 | 300, 50, 107 | mulassd 9666 |
. . . . . . . . . . . 12
          
            |
338 | 336, 337 | eqtrd 2485 |
. . . . . . . . . . 11
                       |
339 | 338 | oveq2d 6306 |
. . . . . . . . . 10
                  
        |
340 | 339 | adantr 467 |
. . . . . . . . 9
 
                    
        |
341 | 327, 334,
340 | 3eqtrd 2489 |
. . . . . . . 8
 
   
      
        |
342 | 341 | oveq2d 6306 |
. . . . . . 7
 
         
                         |
343 | 193 | adantr 467 |
. . . . . . . 8
 
           |
344 | 14 | a1i 11 |
. . . . . . . 8
 
     |
345 | 306 | adantr 467 |
. . . . . . . 8
 
               |
346 | 343, 344,
345 | addassd 9665 |
. . . . . . 7
 
           
                                 |
347 | 342, 346 | eqtr4d 2488 |
. . . . . 6
 
         
                         |
348 | 347 | fveq2d 5869 |
. . . . 5
 
                            
              |
349 | 348 | oveq1d 6305 |
. . . 4
 
             
                               
                             |
350 | 193, 107 | addcld 9662 |
. . . . . . . . 9
        
  |
351 | | sinper 23436 |
. . . . . . . . 9
         
                       
                
    |
352 | 350, 262,
351 | syl2anc 667 |
. . . . . . . 8
            
                     
    |
353 | | sinppi 23444 |
. . . . . . . . 9
                                |
354 | 193, 353 | syl 17 |
. . . . . . . 8
          
               |
355 | 352, 354 | eqtrd 2485 |
. . . . . . 7
            
                         |
356 | 355 | oveq1d 6305 |
. . . . . 6
             
                                         
              |
357 | 195 | oveq2d 6306 |
. . . . . 6
               
                                         |
358 | 194, 194,
215 | divnegd 10396 |
. . . . . . . . 9
                                                 |
359 | 218 | negeqd 9869 |
. . . . . . . . 9
                           |
360 | 358, 359 | eqtr3d 2487 |
. . . . . . . 8
                           |
361 | 360 | oveq1d 6305 |
. . . . . . 7
                                   |
362 | 194 | negcld 9973 |
. . . . . . . 8
              |
363 | 362, 194,
192, 215, 216 | divdiv1d 10414 |
. . . . . . 7
                                                         |
364 | 86, 90 | negsubi 9952 |
. . . . . . . . . . 11
          |
365 | 90, 86 | negsubdi2i 9961 |
. . . . . . . . . . 11
          |
366 | | 1mhlfehlf 10832 |
. . . . . . . . . . . . 13
       |
367 | 366 | negeqi 9868 |
. . . . . . . . . . . 12
         |
368 | | divneg 10302 |
. . . . . . . . . . . . 13
 
         |
369 | 90, 118, 51, 368 | mp3an 1364 |
. . . . . . . . . . . 12
       |
370 | 367, 369 | eqtri 2473 |
. . . . . . . . . . 11
         |
371 | 364, 365,
370 | 3eqtr2i 2479 |
. . . . . . . . . 10
         |
372 | 371 | oveq1i 6300 |
. . . . . . . . 9
             |
373 | | divdiv1 10318 |
. . . . . . . . . 10
                    |
374 | 316, 91, 95, 373 | mp3an 1364 |
. . . . . . . . 9
           |
375 | 372, 374 | eqtr2i 2474 |
. . . . . . . 8
             |
376 | 375 | a1i 11 |
. . . . . . 7
               |
377 | 361, 363,
376 | 3eqtr3d 2493 |
. . . . . 6
                                     |
378 | 356, 357,
377 | 3eqtrd 2489 |
. . . . 5
             
                                    |
379 | 378 | adantr 467 |
. . . 4
 
               
                                    |
380 | 326, 349,
379 | 3eqtrrd 2490 |
. . 3
 
         
                        |
381 | 225, 324,
380 | 3eqtrd 2489 |
. 2
 
                    
                        |
382 | 224, 381 | pm2.61dan 800 |
1
     
                          
          |