Step | Hyp | Ref
| Expression |
1 | | oveq2 6323 |
. . . . 5
       |
2 | 1 | oveq2d 6331 |
. . . 4
               |
3 | 2 | sumeq1d 13816 |
. . 3
                               |
4 | 3 | eqeq1d 2464 |
. 2
               
                 |
5 | | oveq2 6323 |
. . . . 5
       |
6 | 5 | oveq2d 6331 |
. . . 4
               |
7 | 6 | sumeq1d 13816 |
. . 3
                               |
8 | 7 | eqeq1d 2464 |
. 2
               
                 |
9 | | oveq2 6323 |
. . . . 5
           |
10 | 9 | oveq2d 6331 |
. . . 4
                   |
11 | 10 | sumeq1d 13816 |
. . 3
                                   |
12 | 11 | eqeq1d 2464 |
. 2
                 
                   |
13 | | oveq2 6323 |
. . . . 5
       |
14 | 13 | oveq2d 6331 |
. . . 4
               |
15 | 14 | sumeq1d 13816 |
. . 3
                               |
16 | 15 | eqeq1d 2464 |
. 2
               
                 |
17 | | ax-1cn 9623 |
. . . . . 6
 |
18 | 17 | 2timesi 10759 |
. . . . 5
     |
19 | 18 | oveq2i 6326 |
. . . 4
             |
20 | 19 | sumeq1i 13813 |
. . 3
                             |
21 | | 1z 10996 |
. . . . . . . 8
 |
22 | | uzid 11202 |
. . . . . . . 8
       |
23 | 21, 22 | ax-mp 5 |
. . . . . . 7
     |
24 | 23 | a1i 11 |
. . . . . 6
      |
25 | | elfzelz 11829 |
. . . . . . . . . 10
         |
26 | 25 | zcnd 11070 |
. . . . . . . . 9
         |
27 | 26 | adantl 472 |
. . . . . . . 8
          |
28 | | picn 23463 |
. . . . . . . . 9
 |
29 | 28 | a1i 11 |
. . . . . . . 8
          |
30 | 27, 29 | mulcld 9689 |
. . . . . . 7
            |
31 | 30 | coscld 14234 |
. . . . . 6
                |
32 | | id 22 |
. . . . . . . . 9
       |
33 | | 1p1e2 10751 |
. . . . . . . . 9
   |
34 | 32, 33 | syl6eq 2512 |
. . . . . . . 8
     |
35 | 34 | oveq1d 6330 |
. . . . . . 7
         |
36 | 35 | fveq2d 5892 |
. . . . . 6
                 |
37 | 24, 31, 36 | fsump1 13866 |
. . . . 5
                                    |
38 | 37 | trud 1464 |
. . . 4
                                   |
39 | | coscl 14230 |
. . . . . . . 8
       |
40 | 28, 39 | ax-mp 5 |
. . . . . . 7
     |
41 | | oveq1 6322 |
. . . . . . . . . 10
       |
42 | 28 | mulid2i 9672 |
. . . . . . . . . 10
   |
43 | 41, 42 | syl6eq 2512 |
. . . . . . . . 9
     |
44 | 43 | fveq2d 5892 |
. . . . . . . 8
             |
45 | 44 | fsum1 13857 |
. . . . . . 7
                         |
46 | 21, 40, 45 | mp2an 683 |
. . . . . 6
                 |
47 | | cospi 23476 |
. . . . . 6
      |
48 | 46, 47 | eqtri 2484 |
. . . . 5
              |
49 | | cos2pi 23480 |
. . . . 5
       |
50 | 48, 49 | oveq12i 6327 |
. . . 4
                        |
51 | | neg1cn 10741 |
. . . . 5
  |
52 | | 1pneg1e0 10746 |
. . . . 5
    |
53 | 17, 51, 52 | addcomli 9851 |
. . . 4
    |
54 | 38, 50, 53 | 3eqtri 2488 |
. . 3
               |
55 | 20, 54 | eqtri 2484 |
. 2
               |
56 | 18 | oveq2i 6326 |
. . . . . . . 8
             |
57 | | 2cnd 10710 |
. . . . . . . . 9
   |
58 | | nncn 10645 |
. . . . . . . . 9
   |
59 | 17 | a1i 11 |
. . . . . . . . 9
   |
60 | 57, 58, 59 | adddid 9693 |
. . . . . . . 8
             |
61 | 57, 58 | mulcld 9689 |
. . . . . . . . 9
     |
62 | 61, 59, 59 | addassd 9691 |
. . . . . . . 8
               |
63 | 56, 60, 62 | 3eqtr4a 2522 |
. . . . . . 7
             |
64 | 63 | oveq2d 6331 |
. . . . . 6
                     |
65 | 64 | sumeq1d 13816 |
. . . . 5
                                     |
66 | 65 | adantr 471 |
. . . 4
                                                     |
67 | | 1red 9684 |
. . . . . . . 8
   |
68 | | 2re 10707 |
. . . . . . . . . . 11
 |
69 | 68 | a1i 11 |
. . . . . . . . . 10
   |
70 | | nnre 10644 |
. . . . . . . . . 10
   |
71 | 69, 70 | remulcld 9697 |
. . . . . . . . 9
     |
72 | 71, 67 | readdcld 9696 |
. . . . . . . 8
       |
73 | | 2rp 11336 |
. . . . . . . . . . 11
 |
74 | 73 | a1i 11 |
. . . . . . . . . 10
   |
75 | | nnrp 11340 |
. . . . . . . . . 10
   |
76 | 74, 75 | rpmulcld 11386 |
. . . . . . . . 9
     |
77 | 67, 76 | ltaddrp2d 11401 |
. . . . . . . 8
       |
78 | 67, 72, 77 | ltled 9809 |
. . . . . . 7
       |
79 | | 2z 10998 |
. . . . . . . . . . 11
 |
80 | 79 | a1i 11 |
. . . . . . . . . 10
   |
81 | | nnz 10988 |
. . . . . . . . . 10
   |
82 | 80, 81 | zmulcld 11075 |
. . . . . . . . 9
     |
83 | 82 | peano2zd 11072 |
. . . . . . . 8
       |
84 | | eluz 11201 |
. . . . . . . 8
                       |
85 | 21, 83, 84 | sylancr 674 |
. . . . . . 7
         
       |
86 | 78, 85 | mpbird 240 |
. . . . . 6
           |
87 | | elfzelz 11829 |
. . . . . . . . . 10
             |
88 | 87 | zcnd 11070 |
. . . . . . . . 9
             |
89 | 28 | a1i 11 |
. . . . . . . . 9
             |
90 | 88, 89 | mulcld 9689 |
. . . . . . . 8
               |
91 | 90 | coscld 14234 |
. . . . . . 7
                   |
92 | 91 | adantl 472 |
. . . . . 6
 
                   |
93 | | oveq1 6322 |
. . . . . . 7
                   |
94 | 93 | fveq2d 5892 |
. . . . . 6
                           |
95 | 86, 92, 94 | fsump1 13866 |
. . . . 5
                                                   |
96 | 95 | adantr 471 |
. . . 4
                                                                   |
97 | | 1lt2 10805 |
. . . . . . . . . . . 12
 |
98 | 97 | a1i 11 |
. . . . . . . . . . 11
   |
99 | | 2t1e2 10787 |
. . . . . . . . . . . 12
   |
100 | | nnge1 10663 |
. . . . . . . . . . . . 13
   |
101 | 67, 70, 74 | lemul2d 11411 |
. . . . . . . . . . . . 13
 
       |
102 | 100, 101 | mpbid 215 |
. . . . . . . . . . . 12
       |
103 | 99, 102 | syl5eqbrr 4451 |
. . . . . . . . . . 11
     |
104 | 67, 69, 71, 98, 103 | ltletrd 9821 |
. . . . . . . . . 10
     |
105 | 67, 71, 104 | ltled 9809 |
. . . . . . . . 9
     |
106 | | eluz 11201 |
. . . . . . . . . 10
                 |
107 | 21, 82, 106 | sylancr 674 |
. . . . . . . . 9
       
     |
108 | 105, 107 | mpbird 240 |
. . . . . . . 8
         |
109 | | elfzelz 11829 |
. . . . . . . . . . . 12
           |
110 | 109 | zcnd 11070 |
. . . . . . . . . . 11
           |
111 | 28 | a1i 11 |
. . . . . . . . . . 11
           |
112 | 110, 111 | mulcld 9689 |
. . . . . . . . . 10
             |
113 | 112 | coscld 14234 |
. . . . . . . . 9
                 |
114 | 113 | adantl 472 |
. . . . . . . 8
 
                 |
115 | | oveq1 6322 |
. . . . . . . . 9
               |
116 | 115 | fveq2d 5892 |
. . . . . . . 8
                       |
117 | 108, 114,
116 | fsump1 13866 |
. . . . . . 7
                                             |
118 | 33, 99 | eqtr4i 2487 |
. . . . . . . . . . . . 13
     |
119 | 118 | a1i 11 |
. . . . . . . . . . . 12
       |
120 | 119 | oveq2d 6331 |
. . . . . . . . . . 11
               |
121 | 120, 62, 60 | 3eqtr4d 2506 |
. . . . . . . . . 10
             |
122 | 121 | oveq1d 6330 |
. . . . . . . . 9
                 |
123 | 122 | fveq2d 5892 |
. . . . . . . 8
                         |
124 | 58, 59 | addcld 9688 |
. . . . . . . . . . . . 13
     |
125 | 28 | a1i 11 |
. . . . . . . . . . . . 13
   |
126 | 57, 124, 125 | mulassd 9692 |
. . . . . . . . . . . 12
               |
127 | 126 | oveq1d 6330 |
. . . . . . . . . . 11
                       |
128 | 124, 125 | mulcld 9689 |
. . . . . . . . . . . 12
       |
129 | | 0re 9669 |
. . . . . . . . . . . . . 14
 |
130 | | pipos 23464 |
. . . . . . . . . . . . . 14
 |
131 | 129, 130 | gtneii 9772 |
. . . . . . . . . . . . 13
 |
132 | 131 | a1i 11 |
. . . . . . . . . . . 12
   |
133 | 74 | rpne0d 11375 |
. . . . . . . . . . . 12
   |
134 | 128, 125,
57, 132, 133 | divcan5d 10437 |
. . . . . . . . . . 11
                   |
135 | 124, 125,
132 | divcan4d 10417 |
. . . . . . . . . . 11
           |
136 | 127, 134,
135 | 3eqtrd 2500 |
. . . . . . . . . 10
               |
137 | 81 | peano2zd 11072 |
. . . . . . . . . 10
     |
138 | 136, 137 | eqeltrd 2540 |
. . . . . . . . 9
             |
139 | | peano2cn 9831 |
. . . . . . . . . . . . 13
     |
140 | 58, 139 | syl 17 |
. . . . . . . . . . . 12
     |
141 | 57, 140 | mulcld 9689 |
. . . . . . . . . . 11
       |
142 | 141, 125 | mulcld 9689 |
. . . . . . . . . 10
         |
143 | | coseq1 23526 |
. . . . . . . . . 10
                               |
144 | 142, 143 | syl 17 |
. . . . . . . . 9
                         |
145 | 138, 144 | mpbird 240 |
. . . . . . . 8
             |
146 | 123, 145 | eqtrd 2496 |
. . . . . . 7
               |
147 | 117, 146 | oveq12d 6333 |
. . . . . 6
                                                             |
148 | 147 | adantr 471 |
. . . . 5
                                                                             |
149 | | simpr 467 |
. . . . . . . 8
                                 |
150 | 61, 59, 125 | adddird 9694 |
. . . . . . . . . . . 12
                 |
151 | 61, 125 | mulcld 9689 |
. . . . . . . . . . . . 13
       |
152 | 42, 125 | syl5eqel 2544 |
. . . . . . . . . . . . 13
     |
153 | 151, 152 | addcomd 9861 |
. . . . . . . . . . . 12
     
             |
154 | 42 | a1i 11 |
. . . . . . . . . . . . 13
     |
155 | 57, 58 | mulcomd 9690 |
. . . . . . . . . . . . . . 15
       |
156 | 155 | oveq1d 6330 |
. . . . . . . . . . . . . 14
           |
157 | 58, 57, 125 | mulassd 9692 |
. . . . . . . . . . . . . 14
           |
158 | 156, 157 | eqtrd 2496 |
. . . . . . . . . . . . 13
           |
159 | 154, 158 | oveq12d 6333 |
. . . . . . . . . . . 12
   
             |
160 | 150, 153,
159 | 3eqtrd 2500 |
. . . . . . . . . . 11
               |
161 | 160 | fveq2d 5892 |
. . . . . . . . . 10
                       |
162 | | cosper 23486 |
. . . . . . . . . . 11
 
                 |
163 | 28, 81, 162 | sylancr 674 |
. . . . . . . . . 10
                 |
164 | 47 | a1i 11 |
. . . . . . . . . 10
        |
165 | 161, 163,
164 | 3eqtrd 2500 |
. . . . . . . . 9
              |
166 | 165 | adantr 471 |
. . . . . . . 8
                              |
167 | 149, 166 | oveq12d 6333 |
. . . . . . 7
                                                |
168 | 167 | oveq1d 6330 |
. . . . . 6
                                                    |
169 | 51 | addid2i 9847 |
. . . . . . . 8
     |
170 | 169 | oveq1i 6325 |
. . . . . . 7
         |
171 | 170, 53 | eqtri 2484 |
. . . . . 6
      |
172 | 168, 171 | syl6eq 2512 |
. . . . 5
                                               |
173 | 148, 172 | eqtrd 2496 |
. . . 4
                                                 |
174 | 66, 96, 173 | 3eqtrd 2500 |
. . 3
                                   |
175 | 174 | ex 440 |
. 2
                                   |
176 | 4, 8, 12, 16, 55, 175 | nnind 10655 |
1
                 |