Step | Hyp | Ref
| Expression |
1 | | basel.n |
. . . . . . . . 9
     |
2 | 1 | basellem1 24000 |
. . . . . . . 8
 
                 |
3 | | tanrpcl 23452 |
. . . . . . . 8
        
 
          |
4 | 2, 3 | syl 17 |
. . . . . . 7
 
               |
5 | | 2z 10966 |
. . . . . . . 8
 |
6 | | znegcl 10969 |
. . . . . . . 8
    |
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
  |
8 | | rpexpcl 12288 |
. . . . . . 7
         
                 |
9 | 4, 7, 8 | sylancl 667 |
. . . . . 6
 
                    |
10 | 9 | rpcnd 11340 |
. . . . 5
 
                    |
11 | | basel.p |
. . . . . . . 8
                            |
12 | 1, 11 | basellem3 24002 |
. . . . . . 7
                                                        |
13 | 2, 12 | syldan 473 |
. . . . . 6
 
                                                |
14 | | elfzelz 11797 |
. . . . . . . . . . . . . 14
       |
15 | 14 | adantl 468 |
. . . . . . . . . . . . 13
 
       |
16 | 15 | zred 11037 |
. . . . . . . . . . . 12
 
       |
17 | | pire 23406 |
. . . . . . . . . . . 12
 |
18 | | remulcl 9621 |
. . . . . . . . . . . 12
    
  |
19 | 16, 17, 18 | sylancl 667 |
. . . . . . . . . . 11
 
         |
20 | 19 | recnd 9666 |
. . . . . . . . . 10
 
         |
21 | | 2nn 10764 |
. . . . . . . . . . . . . . 15
 |
22 | | nnmulcl 10629 |
. . . . . . . . . . . . . . 15
 
     |
23 | 21, 22 | mpan 675 |
. . . . . . . . . . . . . 14
     |
24 | 23 | peano2nnd 10623 |
. . . . . . . . . . . . 13
       |
25 | 1, 24 | syl5eqel 2532 |
. . . . . . . . . . . 12
   |
26 | 25 | adantr 467 |
. . . . . . . . . . 11
 
       |
27 | 26 | nncnd 10622 |
. . . . . . . . . 10
 
       |
28 | 26 | nnne0d 10651 |
. . . . . . . . . 10
 
       |
29 | 20, 27, 28 | divcan2d 10382 |
. . . . . . . . 9
 
               |
30 | 29 | fveq2d 5867 |
. . . . . . . 8
 
        
              |
31 | | sinkpi 23467 |
. . . . . . . . 9
         |
32 | 15, 31 | syl 17 |
. . . . . . . 8
 
             |
33 | 30, 32 | eqtrd 2484 |
. . . . . . 7
 
        
        |
34 | 33 | oveq1d 6303 |
. . . . . 6
 
                                             |
35 | 19, 26 | nndivred 10655 |
. . . . . . . . . 10
 
           |
36 | 35 | resincld 14190 |
. . . . . . . . 9
 
               |
37 | 36 | recnd 9666 |
. . . . . . . 8
 
               |
38 | 26 | nnnn0d 10922 |
. . . . . . . 8
 
       |
39 | 37, 38 | expcld 12413 |
. . . . . . 7
 
                   |
40 | | sincosq1sgn 23446 |
. . . . . . . . . . 11
        
 
                    |
41 | 2, 40 | syl 17 |
. . . . . . . . . 10
 
                         |
42 | 41 | simpld 461 |
. . . . . . . . 9
 
               |
43 | 42 | gt0ne0d 10175 |
. . . . . . . 8
 
               |
44 | 26 | nnzd 11036 |
. . . . . . . 8
 
       |
45 | 37, 43, 44 | expne0d 12419 |
. . . . . . 7
 
                   |
46 | 39, 45 | div0d 10379 |
. . . . . 6
 
                     |
47 | 13, 34, 46 | 3eqtrd 2488 |
. . . . 5
 
                        |
48 | 1, 11 | basellem2 24001 |
. . . . . . . . 9
 
Poly  deg  coeff                    |
49 | 48 | simp1d 1019 |
. . . . . . . 8
 Poly    |
50 | | plyf 23145 |
. . . . . . . 8
 Poly        |
51 | | ffn 5726 |
. . . . . . . 8
       |
52 | 49, 50, 51 | 3syl 18 |
. . . . . . 7
   |
53 | 52 | adantr 467 |
. . . . . 6
 
       |
54 | | fniniseg 6001 |
. . . . . 6
                                                         |
55 | 53, 54 | syl 17 |
. . . . 5
 
                                                             |
56 | 10, 47, 55 | mpbir2and 932 |
. . . 4
 
                           |
57 | | basel.t |
. . . 4
                    |
58 | 56, 57 | fmptd 6044 |
. . 3
                  |
59 | | fveq2 5863 |
. . . . . 6
           |
60 | | fveq2 5863 |
. . . . . 6
           |
61 | | fveq2 5863 |
. . . . . 6
           |
62 | 14 | zred 11037 |
. . . . . . 7
       |
63 | 62 | ssriv 3435 |
. . . . . 6
     |
64 | 9 | rpred 11338 |
. . . . . . . 8
 
                    |
65 | 64, 57 | fmptd 6044 |
. . . . . . 7
           |
66 | 65 | ffvelrnda 6020 |
. . . . . 6
 
           |
67 | | simplr 761 |
. . . . . . . . . . . . . 14
        
     
  |
68 | 63 | sseli 3427 |
. . . . . . . . . . . . . . . 16
       |
69 | 68 | ad2antrl 733 |
. . . . . . . . . . . . . . 15
        
        |
70 | 63 | sseli 3427 |
. . . . . . . . . . . . . . . 16
       |
71 | 70 | ad2antll 734 |
. . . . . . . . . . . . . . 15
        
     
  |
72 | 17 | a1i 11 |
. . . . . . . . . . . . . . 15
        
        |
73 | | pipos 23408 |
. . . . . . . . . . . . . . . 16
 |
74 | 73 | a1i 11 |
. . . . . . . . . . . . . . 15
        
     
  |
75 | | ltmul1 10452 |
. . . . . . . . . . . . . . 15
 
           |
76 | 69, 71, 72, 74, 75 | syl112anc 1271 |
. . . . . . . . . . . . . 14
        
              |
77 | 67, 76 | mpbid 214 |
. . . . . . . . . . . . 13
        
            |
78 | | remulcl 9621 |
. . . . . . . . . . . . . . 15
    
  |
79 | 69, 17, 78 | sylancl 667 |
. . . . . . . . . . . . . 14
        
       
  |
80 | | remulcl 9621 |
. . . . . . . . . . . . . . 15
    
  |
81 | 71, 17, 80 | sylancl 667 |
. . . . . . . . . . . . . 14
        
       
  |
82 | 25 | ad2antrr 731 |
. . . . . . . . . . . . . . 15
        
     
  |
83 | 82 | nnred 10621 |
. . . . . . . . . . . . . 14
        
     
  |
84 | 82 | nngt0d 10650 |
. . . . . . . . . . . . . 14
        
     
  |
85 | | ltdiv1 10466 |
. . . . . . . . . . . . . 14
   
  
          
       |
86 | 79, 81, 83, 84, 85 | syl112anc 1271 |
. . . . . . . . . . . . 13
        
              
       |
87 | 77, 86 | mpbid 214 |
. . . . . . . . . . . 12
        
         
      |
88 | | neghalfpirx 23414 |
. . . . . . . . . . . . . . 15
 
  |
89 | | pirp 23409 |
. . . . . . . . . . . . . . . . 17
 |
90 | | rphalfcl 11324 |
. . . . . . . . . . . . . . . . 17

    |
91 | | rpge0 11311 |
. . . . . . . . . . . . . . . . 17
  
    |
92 | 89, 90, 91 | mp2b 10 |
. . . . . . . . . . . . . . . 16
   |
93 | | halfpire 23412 |
. . . . . . . . . . . . . . . . 17
   |
94 | | le0neg2 10120 |
. . . . . . . . . . . . . . . . 17
   
 
      |
95 | 93, 94 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
  
     |
96 | 92, 95 | mpbi 212 |
. . . . . . . . . . . . . . 15
 
  |
97 | | iooss1 11668 |
. . . . . . . . . . . . . . 15
       
                  |
98 | 88, 96, 97 | mp2an 677 |
. . . . . . . . . . . . . 14
            
   |
99 | 1 | basellem1 24000 |
. . . . . . . . . . . . . . 15
 
                 |
100 | 99 | ad2ant2r 752 |
. . . . . . . . . . . . . 14
        
                  |
101 | 98, 100 | sseldi 3429 |
. . . . . . . . . . . . 13
        
            
        |
102 | 1 | basellem1 24000 |
. . . . . . . . . . . . . . 15
 
                 |
103 | 102 | ad2ant2rl 754 |
. . . . . . . . . . . . . 14
        
                  |
104 | 98, 103 | sseldi 3429 |
. . . . . . . . . . . . 13
        
            
        |
105 | | tanord 23480 |
. . . . . . . . . . . . 13
        
                
       
   
                   |
106 | 101, 104,
105 | syl2anc 666 |
. . . . . . . . . . . 12
        
              
                   |
107 | 87, 106 | mpbid 214 |
. . . . . . . . . . 11
        
                        |
108 | | tanrpcl 23452 |
. . . . . . . . . . . . 13
        
 
          |
109 | 100, 108 | syl 17 |
. . . . . . . . . . . 12
        
                |
110 | | tanrpcl 23452 |
. . . . . . . . . . . . 13
        
 
          |
111 | 103, 110 | syl 17 |
. . . . . . . . . . . 12
        
                |
112 | | rprege0 11313 |
. . . . . . . . . . . . 13
        
                    |
113 | | rprege0 11313 |
. . . . . . . . . . . . 13
        
                    |
114 | | lt2sq 12345 |
. . . . . . . . . . . . 13
                                                                                   |
115 | 112, 113,
114 | syl2an 480 |
. . . . . . . . . . . 12
         
        
                                            |
116 | 109, 111,
115 | syl2anc 666 |
. . . . . . . . . . 11
        
                                                  |
117 | 107, 116 | mpbid 214 |
. . . . . . . . . 10
        
                                |
118 | | rpexpcl 12288 |
. . . . . . . . . . . 12
         
               |
119 | 109, 5, 118 | sylancl 667 |
. . . . . . . . . . 11
        
                    |
120 | | rpexpcl 12288 |
. . . . . . . . . . . 12
         
               |
121 | 111, 5, 120 | sylancl 667 |
. . . . . . . . . . 11
        
                    |
122 | 119, 121 | ltrecd 11356 |
. . . . . . . . . 10
        
                              
                               |
123 | 117, 122 | mpbid 214 |
. . . . . . . . 9
        
                                    |
124 | | oveq1 6295 |
. . . . . . . . . . . . . . 15
       |
125 | 124 | oveq1d 6303 |
. . . . . . . . . . . . . 14
           |
126 | 125 | fveq2d 5867 |
. . . . . . . . . . . . 13
                   |
127 | 126 | oveq1d 6303 |
. . . . . . . . . . . 12
                             |
128 | | ovex 6316 |
. . . . . . . . . . . 12
              |
129 | 127, 57, 128 | fvmpt 5946 |
. . . . . . . . . . 11
                        |
130 | 129 | ad2antll 734 |
. . . . . . . . . 10
        
                         |
131 | 111 | rpcnd 11340 |
. . . . . . . . . . 11
        
                |
132 | | 2nn0 10883 |
. . . . . . . . . . 11
 |
133 | | expneg 12277 |
. . . . . . . . . . 11
                                        |
134 | 131, 132,
133 | sylancl 667 |
. . . . . . . . . 10
        
                                   |
135 | 130, 134 | eqtrd 2484 |
. . . . . . . . 9
        
                          |
136 | | oveq1 6295 |
. . . . . . . . . . . . . . 15
       |
137 | 136 | oveq1d 6303 |
. . . . . . . . . . . . . 14
           |
138 | 137 | fveq2d 5867 |
. . . . . . . . . . . . 13
                   |
139 | 138 | oveq1d 6303 |
. . . . . . . . . . . 12
                             |
140 | | ovex 6316 |
. . . . . . . . . . . 12
              |
141 | 139, 57, 140 | fvmpt 5946 |
. . . . . . . . . . 11
                        |
142 | 141 | ad2antrl 733 |
. . . . . . . . . 10
        
                         |
143 | 109 | rpcnd 11340 |
. . . . . . . . . . 11
        
                |
144 | | expneg 12277 |
. . . . . . . . . . 11
                                        |
145 | 143, 132,
144 | sylancl 667 |
. . . . . . . . . 10
        
                                   |
146 | 142, 145 | eqtrd 2484 |
. . . . . . . . 9
        
                          |
147 | 123, 135,
146 | 3brtr4d 4432 |
. . . . . . . 8
        
         
      |
148 | 147 | an32s 812 |
. . . . . . 7
                         |
149 | 148 | ex 436 |
. . . . . 6
             
           |
150 | 59, 60, 61, 63, 66, 149 | eqord2 10142 |
. . . . 5
  
   
     

           |
151 | 150 | biimprd 227 |
. . . 4
  
   
     
            |
152 | 151 | ralrimivva 2808 |
. . 3
                     
   |
153 | | dff13 6157 |
. . 3
               
                
     
             
    |
154 | 58, 152, 153 | sylanbrc 669 |
. 2
                  |
155 | 48 | simp2d 1020 |
. . . . . . . . 9
 deg    |
156 | | nnne0 10639 |
. . . . . . . . 9
   |
157 | 155, 156 | eqnetrd 2690 |
. . . . . . . 8
 deg    |
158 | | fveq2 5863 |
. . . . . . . . . 10
  deg  deg     |
159 | | dgr0 23209 |
. . . . . . . . . 10
deg    |
160 | 158, 159 | syl6eq 2500 |
. . . . . . . . 9
  deg    |
161 | 160 | necon3i 2655 |
. . . . . . . 8
 deg 
   |
162 | 157, 161 | syl 17 |
. . . . . . 7
    |
163 | | eqid 2450 |
. . . . . . . 8
               |
164 | 163 | fta1 23254 |
. . . . . . 7
  Poly 
                    
deg     |
165 | 49, 162, 164 | syl2anc 666 |
. . . . . 6
                   
deg     |
166 | 165 | simpld 461 |
. . . . 5
          |
167 | | f1domg 7586 |
. . . . 5
                                      |
168 | 166, 154,
167 | sylc 62 |
. . . 4
              |
169 | 165 | simprd 465 |
. . . . . 6
           
deg    |
170 | | nnnn0 10873 |
. . . . . . . 8
   |
171 | | hashfz1 12526 |
. . . . . . . 8

          |
172 | 170, 171 | syl 17 |
. . . . . . 7
           |
173 | 155, 172 | eqtr4d 2487 |
. . . . . 6
 deg            |
174 | 169, 173 | breqtrd 4426 |
. . . . 5
           
          |
175 | | fzfid 12183 |
. . . . . 6
       |
176 | | hashdom 12555 |
. . . . . 6
                                                |
177 | 166, 175,
176 | syl2anc 666 |
. . . . 5
                                   |
178 | 174, 177 | mpbid 214 |
. . . 4
              |
179 | | sbth 7689 |
. . . 4
                                      |
180 | 168, 178,
179 | syl2anc 666 |
. . 3
              |
181 | | f1finf1o 7795 |
. . 3
     
                                                 |
182 | 180, 166,
181 | syl2anc 666 |
. 2
                
                  |
183 | 154, 182 | mpbid 214 |
1
                  |