Step | Hyp | Ref
| Expression |
1 | | flid 12044 |
. . . . 5
       |
2 | 1 | oveq2d 6306 |
. . . 4
               |
3 | 2 | sumeq1d 13767 |
. . 3
             Λ             
       Λ               |
4 | | fveq2 5865 |
. . . . . 6
     Λ  Λ        |
5 | | eleq1 2517 |
. . . . . . 7
     
       |
6 | | fveq2 5865 |
. . . . . . 7
                   |
7 | 5, 6 | ifbieq1d 3904 |
. . . . . 6
      
                          |
8 | 4, 7 | oveq12d 6308 |
. . . . 5
      Λ             Λ                          |
9 | | id 22 |
. . . . 5
           |
10 | 8, 9 | oveq12d 6308 |
. . . 4
       Λ    
          Λ                               |
11 | | zre 10941 |
. . . 4
   |
12 | | elfznn 11828 |
. . . . . . . . 9
           |
13 | 12 | adantl 468 |
. . . . . . . 8
 
           |
14 | | vmacl 24045 |
. . . . . . . 8
 Λ    |
15 | 13, 14 | syl 17 |
. . . . . . 7
 
         Λ    |
16 | 13 | nnrpd 11339 |
. . . . . . . . 9
 
           |
17 | 16 | relogcld 23572 |
. . . . . . . 8
 
               |
18 | | 0re 9643 |
. . . . . . . 8
 |
19 | | ifcl 3923 |
. . . . . . . 8
     
   
        |
20 | 17, 18, 19 | sylancl 668 |
. . . . . . 7
 
                    |
21 | 15, 20 | resubcld 10047 |
. . . . . 6
 
          Λ              |
22 | 21, 13 | nndivred 10658 |
. . . . 5
 
           Λ   
           |
23 | 22 | recnd 9669 |
. . . 4
 
           Λ   
           |
24 | | simprr 766 |
. . . . . . . 8
  
        Λ    Λ    |
25 | | vmaprm 24044 |
. . . . . . . . . . . . 13

Λ        |
26 | | prmnn 14625 |
. . . . . . . . . . . . . . 15

  |
27 | 26 | nnred 10624 |
. . . . . . . . . . . . . 14

  |
28 | | prmgt1 14643 |
. . . . . . . . . . . . . 14

  |
29 | 27, 28 | rplogcld 23578 |
. . . . . . . . . . . . 13

      |
30 | 25, 29 | eqeltrd 2529 |
. . . . . . . . . . . 12

Λ    |
31 | 30 | rpne0d 11346 |
. . . . . . . . . . 11

Λ    |
32 | 31 | necon2bi 2654 |
. . . . . . . . . 10
 Λ 
  |
33 | 32 | ad2antll 735 |
. . . . . . . . 9
  
        Λ   
  |
34 | 33 | iffalsed 3892 |
. . . . . . . 8
  
        Λ               |
35 | 24, 34 | oveq12d 6308 |
. . . . . . 7
  
        Λ     Λ    
           |
36 | | 0m0e0 10719 |
. . . . . . 7
   |
37 | 35, 36 | syl6eq 2501 |
. . . . . 6
  
        Λ     Λ    
         |
38 | 37 | oveq1d 6305 |
. . . . 5
  
        Λ      Λ                 |
39 | 12 | ad2antrl 734 |
. . . . . . . 8
  
        Λ   
  |
40 | 39 | nnrpd 11339 |
. . . . . . 7
  
        Λ   
  |
41 | 40 | rpcnne0d 11350 |
. . . . . 6
  
        Λ        |
42 | | div0 10298 |
. . . . . 6
       |
43 | 41, 42 | syl 17 |
. . . . 5
  
        Λ        |
44 | 38, 43 | eqtrd 2485 |
. . . 4
  
        Λ      Λ               |
45 | 10, 11, 23, 44 | fsumvma2 24142 |
. . 3
             Λ             
   ![[,] [,]](_icc.gif) 
  
                     Λ                               |
46 | 3, 45 | eqtr3d 2487 |
. 2
         Λ   
             ![[,] [,]](_icc.gif) 
  
                     Λ                               |
47 | | fzfid 12186 |
. . . . 5
             |
48 | | inss2 3653 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)    |
49 | | simpr 463 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)   
   ![[,] [,]](_icc.gif)     |
50 | 48, 49 | sseldi 3430 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)   
  |
51 | | prmnn 14625 |
. . . . . . . . . . 11

  |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)   
  |
53 | 52 | nnred 10624 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)   
  |
54 | 11 | adantr 467 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)   
  |
55 | | zcn 10942 |
. . . . . . . . . . . 12
   |
56 | 55 | abscld 13498 |
. . . . . . . . . . 11
       |
57 | | peano2re 9806 |
. . . . . . . . . . 11
             |
58 | 56, 57 | syl 17 |
. . . . . . . . . 10
         |
59 | 58 | adantr 467 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)            |
60 | | inss1 3652 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   |
61 | 60 | sseli 3428 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)    |
62 | | elicc2 11699 |
. . . . . . . . . . . . 13
 
    ![[,] [,]](_icc.gif)  
    |
63 | 18, 11, 62 | sylancr 669 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif) 
     |
64 | 61, 63 | syl5ib 223 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)        |
65 | 64 | imp 431 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)    
   |
66 | 65 | simp3d 1022 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)      |
67 | 55 | adantr 467 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)   
  |
68 | 67 | abscld 13498 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)          |
69 | 54 | leabsd 13476 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)          |
70 | 68 | lep1d 10538 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)       
        |
71 | 54, 68, 59, 69, 70 | letrd 9792 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)            |
72 | 53, 54, 59, 66, 71 | letrd 9792 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)            |
73 | | prmuz2 14642 |
. . . . . . . . . 10

      |
74 | 50, 73 | syl 17 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)   
      |
75 | | nn0abscl 13375 |
. . . . . . . . . . . 12
       |
76 | | nn0p1nn 10909 |
. . . . . . . . . . . 12
    
        |
77 | 75, 76 | syl 17 |
. . . . . . . . . . 11
         |
78 | 77 | nnzd 11039 |
. . . . . . . . . 10
         |
79 | 78 | adantr 467 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)            |
80 | | elfz5 11792 |
. . . . . . . . 9
                       
         |
81 | 74, 79, 80 | syl2anc 667 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)              
         |
82 | 72, 81 | mpbird 236 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)   
            |
83 | 82 | ex 436 |
. . . . . 6
     ![[,] [,]](_icc.gif)                |
84 | 83 | ssrdv 3438 |
. . . . 5
    ![[,] [,]](_icc.gif) 
             |
85 | | ssfi 7792 |
. . . . 5
               ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif) 
   |
86 | 47, 84, 85 | syl2anc 667 |
. . . 4
    ![[,] [,]](_icc.gif) 
   |
87 | | fzfid 12186 |
. . . . 5
 
   ![[,] [,]](_icc.gif)                        |
88 | | simprl 764 |
. . . . . . . . . . 11
  
   ![[,] [,]](_icc.gif) 

                   
   ![[,] [,]](_icc.gif)     |
89 | 48, 88 | sseldi 3430 |
. . . . . . . . . 10
  
   ![[,] [,]](_icc.gif) 

                   
  |
90 | | elfznn 11828 |
. . . . . . . . . . 11
                  
  |
91 | 90 | ad2antll 735 |
. . . . . . . . . 10
  
   ![[,] [,]](_icc.gif) 

                      |
92 | | vmappw 24043 |
. . . . . . . . . 10
   Λ            |
93 | 89, 91, 92 | syl2anc 667 |
. . . . . . . . 9
  
   ![[,] [,]](_icc.gif) 

                    Λ            |
94 | 52 | adantrr 723 |
. . . . . . . . . . 11
  
   ![[,] [,]](_icc.gif) 

                   
  |
95 | 94 | nnrpd 11339 |
. . . . . . . . . 10
  
   ![[,] [,]](_icc.gif) 

                   
  |
96 | 95 | relogcld 23572 |
. . . . . . . . 9
  
   ![[,] [,]](_icc.gif) 

                          |
97 | 93, 96 | eqeltrd 2529 |
. . . . . . . 8
  
   ![[,] [,]](_icc.gif) 

                    Λ        |
98 | 91 | nnnn0d 10925 |
. . . . . . . . . . . 12
  
   ![[,] [,]](_icc.gif) 

                      |
99 | | nnexpcl 12285 |
. . . . . . . . . . . 12
 
       |
100 | 94, 98, 99 | syl2anc 667 |
. . . . . . . . . . 11
  
   ![[,] [,]](_icc.gif) 

                          |
101 | 100 | nnrpd 11339 |
. . . . . . . . . 10
  
   ![[,] [,]](_icc.gif) 

                          |
102 | 101 | relogcld 23572 |
. . . . . . . . 9
  
   ![[,] [,]](_icc.gif) 

                              |
103 | | ifcl 3923 |
. . . . . . . . 9
         
       
            |
104 | 102, 18, 103 | sylancl 668 |
. . . . . . . 8
  
   ![[,] [,]](_icc.gif) 

                                       |
105 | 97, 104 | resubcld 10047 |
. . . . . . 7
  
   ![[,] [,]](_icc.gif) 

                     Λ                          |
106 | 105, 100 | nndivred 10658 |
. . . . . 6
  
   ![[,] [,]](_icc.gif) 

                      Λ                               |
107 | 106 | anassrs 654 |
. . . . 5
      ![[,] [,]](_icc.gif)   
                     Λ                               |
108 | 87, 107 | fsumrecl 13800 |
. . . 4
 
   ![[,] [,]](_icc.gif)                          Λ                               |
109 | 86, 108 | fsumrecl 13800 |
. . 3
     ![[,] [,]](_icc.gif)                          Λ                               |
110 | 52 | nnrpd 11339 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)   
  |
111 | 110 | relogcld 23572 |
. . . . 5
 
   ![[,] [,]](_icc.gif)          |
112 | | uz2m1nn 11233 |
. . . . . . 7
    
    |
113 | 74, 112 | syl 17 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)        |
114 | 52, 113 | nnmulcld 10657 |
. . . . 5
 
   ![[,] [,]](_icc.gif)          |
115 | 111, 114 | nndivred 10658 |
. . . 4
 
   ![[,] [,]](_icc.gif)                |
116 | 86, 115 | fsumrecl 13800 |
. . 3
     ![[,] [,]](_icc.gif)                |
117 | | 2re 10679 |
. . . 4
 |
118 | 117 | a1i 11 |
. . 3
   |
119 | 18 | a1i 11 |
. . . . . . . . . . . . 13
 
   ![[,] [,]](_icc.gif)      |
120 | 52 | nngt0d 10653 |
. . . . . . . . . . . . 13
 
   ![[,] [,]](_icc.gif)   
  |
121 | 119, 53, 54, 120, 66 | ltletrd 9795 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)   
  |
122 | 54, 121 | elrpd 11338 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)   
  |
123 | 122 | relogcld 23572 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)          |
124 | | prmgt1 14643 |
. . . . . . . . . . . 12

  |
125 | 50, 124 | syl 17 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)   
  |
126 | 53, 125 | rplogcld 23578 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)          |
127 | 123, 126 | rerpdivcld 11369 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)                |
128 | 126 | rpcnd 11343 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)          |
129 | 128 | mulid2d 9661 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)                |
130 | 110, 122 | logled 23576 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)                |
131 | 66, 130 | mpbid 214 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)       
      |
132 | 129, 131 | eqbrtrd 4423 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)                |
133 | | 1re 9642 |
. . . . . . . . . . . 12
 |
134 | 133 | a1i 11 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)      |
135 | 134, 123,
126 | lemuldivd 11387 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)              
             |
136 | 132, 135 | mpbid 214 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)   
            |
137 | | flge1nn 12055 |
. . . . . . . . 9
                                       |
138 | 127, 136,
137 | syl2anc 667 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)                    |
139 | | nnuz 11194 |
. . . . . . . 8
     |
140 | 138, 139 | syl6eleq 2539 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)                        |
141 | 106 | recnd 9669 |
. . . . . . . 8
  
   ![[,] [,]](_icc.gif) 

                      Λ                               |
142 | 141 | anassrs 654 |
. . . . . . 7
      ![[,] [,]](_icc.gif)   
                     Λ                               |
143 | | oveq2 6298 |
. . . . . . . . . 10
           |
144 | 143 | fveq2d 5869 |
. . . . . . . . 9
 Λ      Λ        |
145 | 143 | eleq1d 2513 |
. . . . . . . . . 10
     
       |
146 | 143 | fveq2d 5869 |
. . . . . . . . . 10
                   |
147 | 145, 146 | ifbieq1d 3904 |
. . . . . . . . 9
                                     |
148 | 144, 147 | oveq12d 6308 |
. . . . . . . 8
  Λ                         Λ                          |
149 | 148, 143 | oveq12d 6308 |
. . . . . . 7
   Λ                               Λ                               |
150 | 140, 142,
149 | fsum1p 13814 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)                          Λ                                Λ                                                     Λ                                |
151 | 52 | nncnd 10625 |
. . . . . . . . . . . . . 14
 
   ![[,] [,]](_icc.gif)   
  |
152 | 151 | exp1d 12411 |
. . . . . . . . . . . . 13
 
   ![[,] [,]](_icc.gif)          |
153 | 152 | fveq2d 5869 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)    Λ      Λ    |
154 | | vmaprm 24044 |
. . . . . . . . . . . . 13

Λ        |
155 | 50, 154 | syl 17 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)    Λ        |
156 | 153, 155 | eqtrd 2485 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)    Λ            |
157 | 152, 50 | eqeltrd 2529 |
. . . . . . . . . . . . 13
 
   ![[,] [,]](_icc.gif)          |
158 | 157 | iftrued 3889 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)                               |
159 | 152 | fveq2d 5869 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)                  |
160 | 158, 159 | eqtrd 2485 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)                           |
161 | 156, 160 | oveq12d 6308 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)     Λ                                    |
162 | 128 | subidd 9974 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)                |
163 | 161, 162 | eqtrd 2485 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)     Λ                          |
164 | 163, 152 | oveq12d 6308 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)      Λ                                 |
165 | 110 | rpcnne0d 11350 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)        |
166 | | div0 10298 |
. . . . . . . . 9
       |
167 | 165, 166 | syl 17 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)        |
168 | 164, 167 | eqtrd 2485 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)      Λ                               |
169 | | 1p1e2 10723 |
. . . . . . . . . 10
   |
170 | 169 | oveq1i 6300 |
. . . . . . . . 9
                                       |
171 | 170 | a1i 11 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)                                            |
172 | | elfzuz 11796 |
. . . . . . . . . . . . . 14
                  
      |
173 | | eluz2nn 11197 |
. . . . . . . . . . . . . 14
    
  |
174 | 172, 173 | syl 17 |
. . . . . . . . . . . . 13
                  
  |
175 | 174, 170 | eleq2s 2547 |
. . . . . . . . . . . 12
                    
  |
176 | 50, 175, 92 | syl2an 480 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)   
                     Λ            |
177 | 52 | adantr 467 |
. . . . . . . . . . . . . 14
      ![[,] [,]](_icc.gif)   
                       |
178 | | nnq 11277 |
. . . . . . . . . . . . . 14
   |
179 | 177, 178 | syl 17 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif)   
                       |
180 | 172, 170 | eleq2s 2547 |
. . . . . . . . . . . . . 14
                    
      |
181 | 180 | adantl 468 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif)   
                           |
182 | | expnprm 14847 |
. . . . . . . . . . . . 13
 
           |
183 | 179, 181,
182 | syl2anc 667 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif)   
                           |
184 | 183 | iffalsed 3892 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)   
                                        |
185 | 176, 184 | oveq12d 6308 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)   
                      Λ                                |
186 | 128 | subid1d 9975 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)                |
187 | 186 | adantr 467 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)   
                                 |
188 | 185, 187 | eqtrd 2485 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)   
                      Λ                              |
189 | 188 | oveq1d 6305 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)   
                       Λ                                         |
190 | 171, 189 | sumeq12dv 13772 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)                            Λ                                                             |
191 | 168, 190 | oveq12d 6308 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)       Λ                                                     Λ                                                                |
192 | | fzfid 12186 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)                        |
193 | 111 | adantr 467 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)   
       |
194 | | nnnn0 10876 |
. . . . . . . . . . . 12
   |
195 | 52, 194, 99 | syl2an 480 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)   
       |
196 | 193, 195 | nndivred 10658 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)   
             |
197 | 174, 196 | sylan2 477 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)   
                               |
198 | 192, 197 | fsumrecl 13800 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)                                    |
199 | 198 | recnd 9669 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)                                    |
200 | 199 | addid2d 9834 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)     
                              
                               |
201 | 150, 191,
200 | 3eqtrd 2489 |
. . . . 5
 
   ![[,] [,]](_icc.gif)                          Λ                                                             |
202 | 110 | rpreccld 11351 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)        |
203 | 127 | flcld 12034 |
. . . . . . . . . . . . 13
 
   ![[,] [,]](_icc.gif)                    |
204 | 203 | peano2zd 11043 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)                      |
205 | 202, 204 | rpexpcld 12439 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)                            |
206 | 205 | rpge0d 11345 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)   
                        |
207 | 52 | nnrecred 10655 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)        |
208 | 207 | resqcld 12442 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)            |
209 | 138 | peano2nnd 10626 |
. . . . . . . . . . . . 13
 
   ![[,] [,]](_icc.gif)                      |
210 | 209 | nnnn0d 10925 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)                      |
211 | 207, 210 | reexpcld 12433 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)                            |
212 | 208, 211 | subge02d 10205 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)                          
                             
         |
213 | 206, 212 | mpbid 214 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)                                          |
214 | 113 | nnrpd 11339 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)        |
215 | 214 | rpcnne0d 11350 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)            |
216 | 202 | rpcnd 11343 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)        |
217 | | dmdcan 10317 |
. . . . . . . . . . 11
                               |
218 | 215, 165,
216, 217 | syl3anc 1268 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)                      |
219 | 134 | recnd 9669 |
. . . . . . . . . . . . 13
 
   ![[,] [,]](_icc.gif)      |
220 | | divsubdir 10303 |
. . . . . . . . . . . . 13
 
               |
221 | 151, 219,
165, 220 | syl3anc 1268 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)                |
222 | | divid 10297 |
. . . . . . . . . . . . . 14
       |
223 | 165, 222 | syl 17 |
. . . . . . . . . . . . 13
 
   ![[,] [,]](_icc.gif)        |
224 | 223 | oveq1d 6305 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)                |
225 | 221, 224 | eqtrd 2485 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)              |
226 | | divdiv1 10318 |
. . . . . . . . . . . 12
  
                      |
227 | 219, 165,
215, 226 | syl3anc 1268 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)                  |
228 | 225, 227 | oveq12d 6308 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)                              |
229 | 52 | nnne0d 10654 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)      |
230 | 216, 151,
229 | divrecd 10386 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)                |
231 | 216 | sqvald 12413 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)                  |
232 | 230, 231 | eqtr4d 2488 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)                |
233 | 218, 228,
232 | 3eqtr3d 2493 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)                        |
234 | 213, 233 | breqtrrd 4429 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)                                                |
235 | 208, 211 | resubcld 10047 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)                                    |
236 | 114 | nnrecred 10655 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)            |
237 | | resubcl 9938 |
. . . . . . . . . 10
           |
238 | 133, 207,
237 | sylancr 669 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)          |
239 | | recgt1 10502 |
. . . . . . . . . . . 12
         |
240 | 53, 120, 239 | syl2anc 667 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)          |
241 | 125, 240 | mpbid 214 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)     
  |
242 | | posdif 10107 |
. . . . . . . . . . 11
   
           |
243 | 207, 133,
242 | sylancl 668 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)              |
244 | 241, 243 | mpbid 214 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)   
      |
245 | | ledivmul 10481 |
. . . . . . . . 9
                                                                                     
     
                             
               |
246 | 235, 236,
238, 244, 245 | syl112anc 1272 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)                                              
                             
               |
247 | 234, 246 | mpbird 236 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)                                                |
248 | 238, 244 | elrpd 11338 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)          |
249 | 235, 248 | rerpdivcld 11369 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)                                          |
250 | 249, 236,
126 | lemul2d 11382 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)                                              
                                         
               |
251 | 247, 250 | mpbid 214 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)                                                            |
252 | 128 | adantr 467 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)   
       |
253 | 195 | nncnd 10625 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)   
       |
254 | 195 | nnne0d 10654 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)   
       |
255 | 252, 253,
254 | divrecd 10386 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)   
                         |
256 | 151 | adantr 467 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif)   
   |
257 | 52 | adantr 467 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif)   
   |
258 | 257 | nnne0d 10654 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif)   
   |
259 | | nnz 10959 |
. . . . . . . . . . . . 13
   |
260 | 259 | adantl 468 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif)   
   |
261 | 256, 258,
260 | exprecd 12424 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)   
               |
262 | 261 | oveq2d 6306 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)   
                           |
263 | 255, 262 | eqtr4d 2488 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)   
                         |
264 | 174, 263 | sylan2 477 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)   
                                           |
265 | 264 | sumeq2dv 13769 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)                                                                    |
266 | 174 | nnnn0d 10925 |
. . . . . . . . 9
                  
  |
267 | | expcl 12290 |
. . . . . . . . 9
   
         |
268 | 216, 266,
267 | syl2an 480 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)   
                           |
269 | 192, 128,
268 | fsummulc2 13845 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)                                                                      |
270 | | fzval3 11983 |
. . . . . . . . . . 11
              
                   ..^                   |
271 | 203, 270 | syl 17 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)                       ..^                   |
272 | 271 | sumeq1d 13767 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)                              
 ..^                          |
273 | 207, 241 | ltned 9771 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)        |
274 | | 2nn0 10886 |
. . . . . . . . . . 11
 |
275 | 274 | a1i 11 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)      |
276 | | eluzp1p1 11184 |
. . . . . . . . . . . 12
                                           |
277 | 140, 276 | syl 17 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif)                            |
278 | | df-2 10668 |
. . . . . . . . . . . 12
   |
279 | 278 | fveq2i 5868 |
. . . . . . . . . . 11
           |
280 | 277, 279 | syl6eleqr 2540 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)                          |
281 | 216, 273,
275, 280 | geoserg 13924 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)      ..^                                                              |
282 | 272, 281 | eqtrd 2485 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)                                                                    |
283 | 282 | oveq2d 6306 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)                                                                                |
284 | 265, 269,
283 | 3eqtr2d 2491 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)                                                                              |
285 | 114 | nncnd 10625 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)          |
286 | 114 | nnne0d 10654 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)          |
287 | 128, 285,
286 | divrecd 10386 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)                            |
288 | 251, 284,
287 | 3brtr4d 4433 |
. . . . 5
 
   ![[,] [,]](_icc.gif)                                 
            |
289 | 201, 288 | eqbrtrd 4423 |
. . . 4
 
   ![[,] [,]](_icc.gif)                          Λ                                         |
290 | 86, 108, 115, 289 | fsumle 13859 |
. . 3
     ![[,] [,]](_icc.gif)                          Λ                            
    ![[,] [,]](_icc.gif)                |
291 | | elfzuz 11796 |
. . . . . . . . . . 11
          
      |
292 | | eluz2nn 11197 |
. . . . . . . . . . 11
    
  |
293 | 291, 292 | syl 17 |
. . . . . . . . . 10
          
  |
294 | 293 | adantl 468 |
. . . . . . . . 9
 
          
  |
295 | 294 | nnred 10624 |
. . . . . . . 8
 
          
  |
296 | 291 | adantl 468 |
. . . . . . . . 9
 
          
      |
297 | | eluz2b2 11231 |
. . . . . . . . . 10
         |
298 | 297 | simprbi 466 |
. . . . . . . . 9
    
  |
299 | 296, 298 | syl 17 |
. . . . . . . 8
 
          
  |
300 | 295, 299 | rplogcld 23578 |
. . . . . . 7
 
                 |
301 | 296, 112 | syl 17 |
. . . . . . . . 9
 
               |
302 | 294, 301 | nnmulcld 10657 |
. . . . . . . 8
 
                 |
303 | 302 | nnrpd 11339 |
. . . . . . 7
 
                 |
304 | 300, 303 | rpdivcld 11358 |
. . . . . 6
 
                       |
305 | 304 | rpred 11341 |
. . . . 5
 
                       |
306 | 47, 305 | fsumrecl 13800 |
. . . 4
                         |
307 | 304 | rpge0d 11345 |
. . . . 5
 
          
            |
308 | 47, 305, 307, 84 | fsumless 13856 |
. . . 4
     ![[,] [,]](_icc.gif)                                      |
309 | | rplogsumlem1 24322 |
. . . . 5
                            
  |
310 | 77, 309 | syl 17 |
. . . 4
                      
  |
311 | 116, 306,
118, 308, 310 | letrd 9792 |
. . 3
     ![[,] [,]](_icc.gif)                |
312 | 109, 116,
118, 290, 311 | letrd 9792 |
. 2
     ![[,] [,]](_icc.gif)                          Λ                            
  |
313 | 46, 312 | eqbrtrd 4423 |
1
         Λ   
           |