Step | Hyp | Ref
| Expression |
1 | | nn0uz 11193 |
. . . 4
     |
2 | | 0zd 10949 |
. . . 4
         |
3 | | eqeq1 2455 |
. . . . . . . 8
     |
4 | | oveq2 6298 |
. . . . . . . 8
       |
5 | 3, 4 | ifbieq2d 3906 |
. . . . . . 7
                 |
6 | | oveq2 6298 |
. . . . . . 7
           |
7 | 5, 6 | oveq12d 6308 |
. . . . . 6
                             |
8 | | eqid 2451 |
. . . . . 6

              
               |
9 | | ovex 6318 |
. . . . . 6
              |
10 | 7, 8, 9 | fvmpt 5948 |
. . . . 5

                                  |
11 | 10 | adantl 468 |
. . . 4
      
   
                                |
12 | | 0cnd 9636 |
. . . . . 6
        
    |
13 | | simpr 463 |
. . . . . . . . . . . 12
      
    |
14 | | elnn0 10871 |
. . . . . . . . . . . 12

    |
15 | 13, 14 | sylib 200 |
. . . . . . . . . . 11
      
      |
16 | 15 | ord 379 |
. . . . . . . . . 10
      
  
   |
17 | 16 | con1d 128 |
. . . . . . . . 9
      
      |
18 | 17 | imp 431 |
. . . . . . . 8
        
 
  |
19 | 18 | nnrecred 10655 |
. . . . . . 7
        
      |
20 | 19 | recnd 9669 |
. . . . . 6
        
      |
21 | 12, 20 | ifclda 3913 |
. . . . 5
      
           |
22 | | expcl 12290 |
. . . . . 6
 
       |
23 | 22 | adantlr 721 |
. . . . 5
      
        |
24 | 21, 23 | mulcld 9663 |
. . . 4
      
                 |
25 | | logtayllem 23604 |
. . . 4
                          |
26 | 1, 2, 11, 24, 25 | isumclim2 13819 |
. . 3
                                         |
27 | | simpl 459 |
. . . . . . . 8
      
  |
28 | | 0cn 9635 |
. . . . . . . 8
 |
29 | | eqid 2451 |
. . . . . . . . 9

  |
30 | 29 | cnmetdval 21791 |
. . . . . . . 8
 
   
          |
31 | 27, 28, 30 | sylancl 668 |
. . . . . . 7
         
          |
32 | | subid1 9894 |
. . . . . . . . 9
 
   |
33 | 32 | adantr 467 |
. . . . . . . 8
           |
34 | 33 | fveq2d 5869 |
. . . . . . 7
          
        |
35 | 31, 34 | eqtrd 2485 |
. . . . . 6
         
        |
36 | | simpr 463 |
. . . . . 6
          
  |
37 | 35, 36 | eqbrtrd 4423 |
. . . . 5
         
    |
38 | | cnxmet 21793 |
. . . . . . 7

      |
39 | | 1rp 11306 |
. . . . . . . 8
 |
40 | | rpxr 11309 |
. . . . . . . 8

  |
41 | 39, 40 | ax-mp 5 |
. . . . . . 7
 |
42 | | elbl3 21407 |
. . . . . . 7
   
                  
  
     |
43 | 38, 41, 42 | mpanl12 688 |
. . . . . 6
 
          
  
     |
44 | 28, 27, 43 | sylancr 669 |
. . . . 5
                
  
     |
45 | 37, 44 | mpbird 236 |
. . . 4
      
           |
46 | | tru 1448 |
. . . . . 6
 |
47 | | eqid 2451 |
. . . . . . . 8
                   |
48 | | 0cnd 9636 |
. . . . . . . 8
  |
49 | 41 | a1i 11 |
. . . . . . . 8
  |
50 | | ax-1cn 9597 |
. . . . . . . . . . . . 13
 |
51 | | blssm 21433 |
. . . . . . . . . . . . . . 15
  
    
            |
52 | 38, 28, 41, 51 | mp3an 1364 |
. . . . . . . . . . . . . 14
          |
53 | 52 | sseli 3428 |
. . . . . . . . . . . . 13
         
  |
54 | | subcl 9874 |
. . . . . . . . . . . . 13
 
     |
55 | 50, 53, 54 | sylancr 669 |
. . . . . . . . . . . 12
         
    |
56 | 53 | abscld 13498 |
. . . . . . . . . . . . . . 15
         
      |
57 | 29 | cnmetdval 21791 |
. . . . . . . . . . . . . . . . . 18
 
   
          |
58 | 53, 28, 57 | sylancl 668 |
. . . . . . . . . . . . . . . . 17
         
  
          |
59 | 53 | subid1d 9975 |
. . . . . . . . . . . . . . . . . 18
         
    |
60 | 59 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
         
            |
61 | 58, 60 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
         
  
        |
62 | | elbl3 21407 |
. . . . . . . . . . . . . . . . . . 19
   
                  
  
     |
63 | 38, 41, 62 | mpanl12 688 |
. . . . . . . . . . . . . . . . . 18
 
          
  
     |
64 | 28, 53, 63 | sylancr 669 |
. . . . . . . . . . . . . . . . 17
         
            
     |
65 | 64 | ibi 245 |
. . . . . . . . . . . . . . . 16
         
  
    |
66 | 61, 65 | eqbrtrrd 4425 |
. . . . . . . . . . . . . . 15
         
      |
67 | 56, 66 | gtned 9770 |
. . . . . . . . . . . . . 14
         
      |
68 | | abs1 13360 |
. . . . . . . . . . . . . . . 16
     |
69 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
           |
70 | 68, 69 | syl5eqr 2499 |
. . . . . . . . . . . . . . 15
       |
71 | 70 | necon3i 2656 |
. . . . . . . . . . . . . 14
    
  |
72 | 67, 71 | syl 17 |
. . . . . . . . . . . . 13
         
  |
73 | | subeq0 9900 |
. . . . . . . . . . . . . . 15
 
       |
74 | 73 | necon3bid 2668 |
. . . . . . . . . . . . . 14
 
       |
75 | 50, 53, 74 | sylancr 669 |
. . . . . . . . . . . . 13
         
  
   |
76 | 72, 75 | mpbird 236 |
. . . . . . . . . . . 12
         
    |
77 | 55, 76 | logcld 23520 |
. . . . . . . . . . 11
         
        |
78 | 77 | negcld 9973 |
. . . . . . . . . 10
         
         |
79 | 78 | adantl 468 |
. . . . . . . . 9
          
         |
80 | | eqid 2451 |
. . . . . . . . 9
                                     |
81 | 79, 80 | fmptd 6046 |
. . . . . . . 8
                                 |
82 | 53 | absge0d 13506 |
. . . . . . . . . . . 12
         
      |
83 | 56 | rexrd 9690 |
. . . . . . . . . . . . 13
         
      |
84 | | peano2re 9806 |
. . . . . . . . . . . . . . . 16
             |
85 | 56, 84 | syl 17 |
. . . . . . . . . . . . . . 15
         
        |
86 | 85 | rehalfcld 10859 |
. . . . . . . . . . . . . 14
         
          |
87 | 86 | rexrd 9690 |
. . . . . . . . . . . . 13
         
          |
88 | | iccssxr 11717 |
. . . . . . . . . . . . . . 15
    |
89 | | eqeq1 2455 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
90 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
91 | 89, 90 | ifbieq2d 3906 |
. . . . . . . . . . . . . . . . . . . . 21
  
              |
92 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . 21

        
         |
93 | | c0ex 9637 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
94 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
95 | 93, 94 | ifex 3949 |
. . . . . . . . . . . . . . . . . . . . 21
        |
96 | 91, 92, 95 | fvmpt 5948 |
. . . . . . . . . . . . . . . . . . . 20

                      |
97 | 96 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . 19

        
             |
98 | 97 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . 18

                                  |
99 | 98 | mpteq2ia 4485 |
. . . . . . . . . . . . . . . . 17

              
                     |
100 | 99 | mpteq2i 4486 |
. . . . . . . . . . . . . . . 16
 
                                       |
101 | | 0cnd 9636 |
. . . . . . . . . . . . . . . . . 18
      |
102 | | nn0cn 10879 |
. . . . . . . . . . . . . . . . . . . 20

  |
103 | 102 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
    |
104 | | df-ne 2624 |
. . . . . . . . . . . . . . . . . . . 20

  |
105 | 104 | biimpri 210 |
. . . . . . . . . . . . . . . . . . 19
   |
106 | | reccl 10277 |
. . . . . . . . . . . . . . . . . . 19
       |
107 | 103, 105,
106 | syl2an 480 |
. . . . . . . . . . . . . . . . . 18
  
     |
108 | 101, 107 | ifclda 3913 |
. . . . . . . . . . . . . . . . 17
   
       |
109 | 108, 92 | fmptd 6046 |
. . . . . . . . . . . . . . . 16
               |
110 | | recn 9629 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
111 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
112 | 111 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                             |
113 | 112 | mpteq2dv 4490 |
. . . . . . . . . . . . . . . . . . . . . . 23
                
                |
114 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                                 |
115 | | nn0ex 10875 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
116 | 115 | mptex 6136 |
. . . . . . . . . . . . . . . . . . . . . . 23

               |
117 | 113, 114,
116 | fvmpt 5948 |
. . . . . . . . . . . . . . . . . . . . . 22
                                       |
118 | 110, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
                                       |
119 | 118 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . 20
                                       |
120 | 119 | seqeq3d 12221 |
. . . . . . . . . . . . . . . . . . 19
                       
                     |
121 | 120 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . 18
                       
                     |
122 | 121 | rabbiia 3033 |
. . . . . . . . . . . . . . . . 17
                                             |
123 | 122 | supeq1i 7961 |
. . . . . . . . . . . . . . . 16
                                                     |
124 | 100, 109,
123 | radcnvcl 23372 |
. . . . . . . . . . . . . . 15
                            |
125 | 88, 124 | sseldi 3430 |
. . . . . . . . . . . . . 14
                         |
126 | 46, 125 | mp1i 13 |
. . . . . . . . . . . . 13
         
                         |
127 | | 1re 9642 |
. . . . . . . . . . . . . . 15
 |
128 | | avglt1 10850 |
. . . . . . . . . . . . . . 15
     
     
               |
129 | 56, 127, 128 | sylancl 668 |
. . . . . . . . . . . . . 14
         
        
           |
130 | 66, 129 | mpbid 214 |
. . . . . . . . . . . . 13
         
              |
131 | | 0red 9644 |
. . . . . . . . . . . . . . . 16
         
  |
132 | 131, 56, 86, 82, 130 | lelttrd 9793 |
. . . . . . . . . . . . . . . 16
         
          |
133 | 131, 86, 132 | ltled 9783 |
. . . . . . . . . . . . . . 15
         
          |
134 | 86, 133 | absidd 13484 |
. . . . . . . . . . . . . 14
         
                      |
135 | 46, 109 | mp1i 13 |
. . . . . . . . . . . . . . 15
         
               |
136 | 86 | recnd 9669 |
. . . . . . . . . . . . . . 15
         
          |
137 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
138 | 137 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . 20
                                             |
139 | 138 | mpteq2dv 4490 |
. . . . . . . . . . . . . . . . . . 19
                        
                        |
140 | 115 | mptex 6136 |
. . . . . . . . . . . . . . . . . . 19

                       |
141 | 139, 114,
140 | fvmpt 5948 |
. . . . . . . . . . . . . . . . . 18
        
                                                      |
142 | 136, 141 | syl 17 |
. . . . . . . . . . . . . . . . 17
         
                                                      |
143 | 142 | seqeq3d 12221 |
. . . . . . . . . . . . . . . 16
         
                                                            |
144 | | avglt2 10851 |
. . . . . . . . . . . . . . . . . . . 20
     
     
           |
145 | 56, 127, 144 | sylancl 668 |
. . . . . . . . . . . . . . . . . . 19
         
                |
146 | 66, 145 | mpbid 214 |
. . . . . . . . . . . . . . . . . 18
         
          |
147 | 134, 146 | eqbrtrd 4423 |
. . . . . . . . . . . . . . . . 17
         
              |
148 | | logtayllem 23604 |
. . . . . . . . . . . . . . . . 17
                                                  |
149 | 136, 147,
148 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
         
                           |
150 | 143, 149 | eqeltrd 2529 |
. . . . . . . . . . . . . . 15
         
                                 |
151 | 100, 135,
123, 136, 150 | radcnvle 23375 |
. . . . . . . . . . . . . 14
         
           
                         |
152 | 134, 151 | eqbrtrrd 4425 |
. . . . . . . . . . . . 13
         
                                 |
153 | 83, 87, 126, 130, 152 | xrltletrd 11458 |
. . . . . . . . . . . 12
         
                             |
154 | | 0re 9643 |
. . . . . . . . . . . . 13
 |
155 | | elico2 11698 |
. . . . . . . . . . . . 13
                                                              
                                   |
156 | 154, 126,
155 | sylancr 669 |
. . . . . . . . . . . 12
         
                                        
                               |
157 | 56, 82, 153, 156 | mpbir3and 1191 |
. . . . . . . . . . 11
         
                                 |
158 | | absf 13400 |
. . . . . . . . . . . 12
     |
159 | | ffn 5728 |
. . . . . . . . . . . 12
       |
160 | | elpreima 6002 |
. . . . . . . . . . . 12

                                                                     |
161 | 158, 159,
160 | mp2b 10 |
. . . . . . . . . . 11
                                                                    |
162 | 53, 157, 161 | sylanbrc 670 |
. . . . . . . . . 10
         
                                  |
163 | | cnvimass 5188 |
. . . . . . . . . . . . . . . . . 18
                                 |
164 | 158 | fdmi 5734 |
. . . . . . . . . . . . . . . . . 18
 |
165 | 163, 164 | sseqtri 3464 |
. . . . . . . . . . . . . . . . 17
                                 |
166 | 165 | sseli 3428 |
. . . . . . . . . . . . . . . 16
                                
  |
167 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
168 | 167 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . . 22
                             |
169 | 168 | mpteq2dv 4490 |
. . . . . . . . . . . . . . . . . . . . 21
                
                |
170 | 115 | mptex 6136 |
. . . . . . . . . . . . . . . . . . . . 21

               |
171 | 169, 114,
170 | fvmpt 5948 |
. . . . . . . . . . . . . . . . . . . 20
                                       |
172 | 171 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
                                       |
173 | 172 | fveq1d 5867 |
. . . . . . . . . . . . . . . . . 18
 
    
                      
                   |
174 | | eqeq1 2455 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
175 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
176 | 174, 175 | ifbieq2d 3906 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
177 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . . 21
           |
178 | 176, 177 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . 20
                             |
179 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . 20

              
               |
180 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . 20
              |
181 | 178, 179,
180 | fvmpt 5948 |
. . . . . . . . . . . . . . . . . . 19

                                  |
182 | 181 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
 
                                   |
183 | 173, 182 | eqtr2d 2486 |
. . . . . . . . . . . . . . . . 17
 
                                         |
184 | 183 | sumeq2dv 13769 |
. . . . . . . . . . . . . . . 16
               
   
                       |
185 | 166, 184 | syl 17 |
. . . . . . . . . . . . . . 15
                                
              
   
                       |
186 | 185 | mpteq2ia 4485 |
. . . . . . . . . . . . . 14
                                                                                                             |
187 | | eqid 2451 |
. . . . . . . . . . . . . 14
                                                                 |
188 | | eqid 2451 |
. . . . . . . . . . . . . 14
                                                                                                                                   |
189 | 100, 186,
109, 123, 187, 188 | psercn 23381 |
. . . . . . . . . . . . 13
                                                                                      |
190 | | cncff 21925 |
. . . . . . . . . . . . 13
                                                                                                                                                                           |
191 | 189, 190 | syl 17 |
. . . . . . . . . . . 12
                                                                                      |
192 | | eqid 2451 |
. . . . . . . . . . . . 13
                                                                                                 |
193 | 192 | fmpt 6043 |
. . . . . . . . . . . 12
 
                                                                                                                                     |
194 | 191, 193 | sylibr 216 |
. . . . . . . . . . 11
                                                  |
195 | 194 | r19.21bi 2757 |
. . . . . . . . . 10
                                                  |
196 | 162, 195 | sylan2 477 |
. . . . . . . . 9
          
                |
197 | | eqid 2451 |
. . . . . . . . 9
                                                   |
198 | 196, 197 | fmptd 6046 |
. . . . . . . 8
                                        |
199 | | cnelprrecn 9632 |
. . . . . . . . . . . . 13
    |
200 | 199 | a1i 11 |
. . . . . . . . . . . 12
     |
201 | 77 | adantl 468 |
. . . . . . . . . . . 12
          
        |
202 | | ovex 6318 |
. . . . . . . . . . . . 13
        |
203 | 202 | a1i 11 |
. . . . . . . . . . . 12
          
         |
204 | 29 | cnmetdval 21791 |
. . . . . . . . . . . . . . . . . 18
                      |
205 | 50, 55, 204 | sylancr 669 |
. . . . . . . . . . . . . . . . 17
         
                 |
206 | | nncan 9903 |
. . . . . . . . . . . . . . . . . . 19
 
       |
207 | 50, 53, 206 | sylancr 669 |
. . . . . . . . . . . . . . . . . 18
         
      |
208 | 207 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
         
              |
209 | 205, 208 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
         
             |
210 | 209, 66 | eqbrtrd 4423 |
. . . . . . . . . . . . . . 15
         
         |
211 | | elbl 21403 |
. . . . . . . . . . . . . . . 16
  
    
            
              |
212 | 38, 50, 41, 211 | mp3an 1364 |
. . . . . . . . . . . . . . 15
                         |
213 | 55, 210, 212 | sylanbrc 670 |
. . . . . . . . . . . . . 14
         
             |
214 | 213 | adantl 468 |
. . . . . . . . . . . . 13
          
             |
215 | | neg1cn 10713 |
. . . . . . . . . . . . . 14
  |
216 | 215 | a1i 11 |
. . . . . . . . . . . . 13
          
   |
217 | | eqid 2451 |
. . . . . . . . . . . . . . . . . 18
                   |
218 | 217 | dvlog2lem 23597 |
. . . . . . . . . . . . . . . . 17
           ![(,] (,]](_ioc.gif)    |
219 | 218 | sseli 3428 |
. . . . . . . . . . . . . . . 16
         

 ![(,] (,]](_ioc.gif)     |
220 | 219 | eldifad 3416 |
. . . . . . . . . . . . . . 15
         
  |
221 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
  ![(,] (,]](_ioc.gif)     ![(,] (,]](_ioc.gif)    |
222 | 221 | logdmn0 23585 |
. . . . . . . . . . . . . . . 16
   ![(,] (,]](_ioc.gif)  
  |
223 | 219, 222 | syl 17 |
. . . . . . . . . . . . . . 15
         
  |
224 | 220, 223 | logcld 23520 |
. . . . . . . . . . . . . 14
         
      |
225 | 224 | adantl 468 |
. . . . . . . . . . . . 13
          
      |
226 | | ovex 6318 |
. . . . . . . . . . . . . 14
   |
227 | 226 | a1i 11 |
. . . . . . . . . . . . 13
          
    |
228 | | simpr 463 |
. . . . . . . . . . . . . . 15
    |
229 | 50, 228, 54 | sylancr 669 |
. . . . . . . . . . . . . 14
      |
230 | 215 | a1i 11 |
. . . . . . . . . . . . . 14
     |
231 | | 1cnd 9659 |
. . . . . . . . . . . . . . . 16
    |
232 | | 0cnd 9636 |
. . . . . . . . . . . . . . . 16
    |
233 | | 1cnd 9659 |
. . . . . . . . . . . . . . . . 17
  |
234 | 200, 233 | dvmptc 22912 |
. . . . . . . . . . . . . . . 16
        |
235 | 200 | dvmptid 22911 |
. . . . . . . . . . . . . . . 16
        |
236 | 200, 231,
232, 234, 228, 231, 235 | dvmptsub 22921 |
. . . . . . . . . . . . . . 15
            |
237 | | df-neg 9863 |
. . . . . . . . . . . . . . . 16
    |
238 | 237 | mpteq2i 4486 |
. . . . . . . . . . . . . . 15
        |
239 | 236, 238 | syl6eqr 2503 |
. . . . . . . . . . . . . 14
           |
240 | 52 | a1i 11 |
. . . . . . . . . . . . . 14
           |
241 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
  ℂfld   ℂfld |
242 | 241 | cnfldtop 21804 |
. . . . . . . . . . . . . . . 16
  ℂfld  |
243 | 241 | cnfldtopon 21803 |
. . . . . . . . . . . . . . . . . 18
  ℂfld TopOn   |
244 | 243 | toponunii 19947 |
. . . . . . . . . . . . . . . . 17
   ℂfld |
245 | 244 | restid 15332 |
. . . . . . . . . . . . . . . 16
   ℂfld    ℂfld
↾t    ℂfld  |
246 | 242, 245 | ax-mp 5 |
. . . . . . . . . . . . . . 15
   ℂfld ↾t    ℂfld |
247 | 246 | eqcomi 2460 |
. . . . . . . . . . . . . 14
  ℂfld    ℂfld ↾t   |
248 | 241 | cnfldtopn 21802 |
. . . . . . . . . . . . . . . . 17
  ℂfld       |
249 | 248 | blopn 21515 |
. . . . . . . . . . . . . . . 16
  
    
            ℂfld  |
250 | 38, 28, 41, 249 | mp3an 1364 |
. . . . . . . . . . . . . . 15
           ℂfld |
251 | 250 | a1i 11 |
. . . . . . . . . . . . . 14
           ℂfld  |
252 | 200, 229,
230, 239, 240, 247, 241, 251 | dvmptres 22917 |
. . . . . . . . . . . . 13
                             |
253 | 217 | dvlog2 23598 |
. . . . . . . . . . . . . 14
                           |
254 | | logf1o 23514 |
. . . . . . . . . . . . . . . . . . . 20
         |
255 | | f1of 5814 |
. . . . . . . . . . . . . . . . . . . 20
                
  |
256 | 254, 255 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
         |
257 | 221 | logdmss 23587 |
. . . . . . . . . . . . . . . . . . . 20
  ![(,] (,]](_ioc.gif)   
    |
258 | 218, 257 | sstri 3441 |
. . . . . . . . . . . . . . . . . . 19
              |
259 | | fssres 5749 |
. . . . . . . . . . . . . . . . . . 19
         
                                        |
260 | 256, 258,
259 | mp2an 678 |
. . . . . . . . . . . . . . . . . 18
                         |
261 | 260 | a1i 11 |
. . . . . . . . . . . . . . . . 17
                          |
262 | 261 | feqmptd 5918 |
. . . . . . . . . . . . . . . 16
                      
                |
263 | | fvres 5879 |
. . . . . . . . . . . . . . . . 17
         
                     |
264 | 263 | mpteq2ia 4485 |
. . . . . . . . . . . . . . . 16
                                          |
265 | 262, 264 | syl6eq 2501 |
. . . . . . . . . . . . . . 15
                            |
266 | 265 | oveq2d 6306 |
. . . . . . . . . . . . . 14
                                |
267 | 253, 266 | syl5reqr 2500 |
. . . . . . . . . . . . 13
                                |
268 | | fveq2 5865 |
. . . . . . . . . . . . 13
               |
269 | | oveq2 6298 |
. . . . . . . . . . . . 13
           |
270 | 200, 200,
214, 216, 225, 227, 252, 267, 268, 269 | dvmptco 22926 |
. . . . . . . . . . . 12
                                       |
271 | 200, 201,
203, 270 | dvmptneg 22920 |
. . . . . . . . . . 11
                                         |
272 | 55, 76 | reccld 10376 |
. . . . . . . . . . . . . . . 16
         
      |
273 | | mulcom 9625 |
. . . . . . . . . . . . . . . 16
                        |
274 | 272, 215,
273 | sylancl 668 |
. . . . . . . . . . . . . . 15
         
                |
275 | 272 | mulm1d 10070 |
. . . . . . . . . . . . . . 15
         
              |
276 | 274, 275 | eqtrd 2485 |
. . . . . . . . . . . . . 14
         
              |
277 | 276 | negeqd 9869 |
. . . . . . . . . . . . 13
         
                |
278 | 272 | negnegd 9977 |
. . . . . . . . . . . . 13
         
            |
279 | 277, 278 | eqtrd 2485 |
. . . . . . . . . . . 12
         
              |
280 | 279 | mpteq2ia 4485 |
. . . . . . . . . . 11
                                   |
281 | 271, 280 | syl6eq 2501 |
. . . . . . . . . 10
                                     |
282 | 281 | dmeqd 5037 |
. . . . . . . . 9
                                     |
283 | | dmmptg 5332 |
. . . . . . . . . 10
 
             
                          |
284 | | ovex 6318 |
. . . . . . . . . . 11
     |
285 | 284 | a1i 11 |
. . . . . . . . . 10
         
      |
286 | 283, 285 | mprg 2751 |
. . . . . . . . 9
                         |
287 | 282, 286 | syl6eq 2501 |
. . . . . . . 8
                               |
288 | | sumex 13754 |
. . . . . . . . . . . 12
    
                    |
289 | 288 | a1i 11 |
. . . . . . . . . . 11
                                      
                     |
290 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
                             
                       |
291 | 290 | cbvsumv 13762 |
. . . . . . . . . . . . . 14
                              
                      |
292 | 185, 291 | syl6eq 2501 |
. . . . . . . . . . . . 13
                                
                  
                       |
293 | 292 | mpteq2ia 4485 |
. . . . . . . . . . . 12
                                                                                                             |
294 | | eqid 2451 |
. . . . . . . . . . . 12
                                                                                                                                                                     |
295 | 100, 293,
109, 123, 187, 188, 294 | pserdv2 23385 |
. . . . . . . . . . 11
                                                                                                              |
296 | 162 | ssriv 3436 |
. . . . . . . . . . . 12
                                          |
297 | 296 | a1i 11 |
. . . . . . . . . . 11
                                           |
298 | 200, 195,
289, 295, 297, 247, 241, 251 | dvmptres 22917 |
. . . . . . . . . 10
                                                                |
299 | | nnnn0 10876 |
. . . . . . . . . . . . . . . . . . . 20
   |
300 | 299 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
              |
301 | | eqeq1 2455 |
. . . . . . . . . . . . . . . . . . . . 21
     |
302 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . . 21
       |
303 | 301, 302 | ifbieq2d 3906 |
. . . . . . . . . . . . . . . . . . . 20
  
              |
304 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . . 21
   |
305 | 93, 304 | ifex 3949 |
. . . . . . . . . . . . . . . . . . . 20
        |
306 | 303, 92, 305 | fvmpt 5948 |
. . . . . . . . . . . . . . . . . . 19

                      |
307 | 300, 306 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                                  |
308 | | nnne0 10642 |
. . . . . . . . . . . . . . . . . . . . 21
   |
309 | 308 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
              |
310 | 309 | neneqd 2629 |
. . . . . . . . . . . . . . . . . . 19
           
  |
311 | 310 | iffalsed 3892 |
. . . . . . . . . . . . . . . . . 18
             
         |
312 | 307, 311 | eqtrd 2485 |
. . . . . . . . . . . . . . . . 17
                             |
313 | 312 | oveq2d 6306 |
. . . . . . . . . . . . . . . 16
                                 |
314 | | nncn 10617 |
. . . . . . . . . . . . . . . . . 18
   |
315 | 314 | adantl 468 |
. . . . . . . . . . . . . . . . 17
              |
316 | 315, 309 | recidd 10378 |
. . . . . . . . . . . . . . . 16
                  |
317 | 313, 316 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
                             |
318 | 317 | oveq1d 6305 |
. . . . . . . . . . . . . 14
                                             |
319 | | nnm1nn0 10911 |
. . . . . . . . . . . . . . . 16
     |
320 | | expcl 12290 |
. . . . . . . . . . . . . . . 16
  
          |
321 | 53, 319, 320 | syl2an 480 |
. . . . . . . . . . . . . . 15
                    |
322 | 321 | mulid2d 9661 |
. . . . . . . . . . . . . 14
                            |
323 | 318, 322 | eqtrd 2485 |
. . . . . . . . . . . . 13
                                           |
324 | 323 | sumeq2dv 13769 |
. . . . . . . . . . . 12
         
    
                            |
325 | | nnuz 11194 |
. . . . . . . . . . . . . . 15
     |
326 | | 1e0p1 11079 |
. . . . . . . . . . . . . . . 16
   |
327 | 326 | fveq2i 5868 |
. . . . . . . . . . . . . . 15
           |
328 | 325, 327 | eqtri 2473 |
. . . . . . . . . . . . . 14
       |
329 | | oveq1 6297 |
. . . . . . . . . . . . . . 15
           |
330 | 329 | oveq2d 6306 |
. . . . . . . . . . . . . 14
                   |
331 | | 1zzd 10968 |
. . . . . . . . . . . . . 14
         
  |
332 | | 0zd 10949 |
. . . . . . . . . . . . . 14
         
  |
333 | 1, 328, 330, 331, 332, 321 | isumshft 13897 |
. . . . . . . . . . . . 13
         
       
          |
334 | | pncan2 9882 |
. . . . . . . . . . . . . . . 16
 
       |
335 | 50, 102, 334 | sylancr 669 |
. . . . . . . . . . . . . . 15

      |
336 | 335 | oveq2d 6306 |
. . . . . . . . . . . . . 14

              |
337 | 336 | sumeq2i 13765 |
. . . . . . . . . . . . 13
         
     |
338 | 333, 337 | syl6eq 2501 |
. . . . . . . . . . . 12
         
       
      |
339 | | geoisum 13933 |
. . . . . . . . . . . . 13
                  |
340 | 53, 66, 339 | syl2anc 667 |
. . . . . . . . . . . 12
         
           |
341 | 324, 338,
340 | 3eqtrd 2489 |
. . . . . . . . . . 11
         
    
                         |
342 | 341 | mpteq2ia 4485 |
. . . . . . . . . 10
                                                   |
343 | 298, 342 | syl6eq 2501 |
. . . . . . . . 9
                                            |
344 | 281, 343 | eqtr4d 2488 |
. . . . . . . 8
                                                 |
345 | | blcntr 21428 |
. . . . . . . . . 10
  ![]() |