Step | Hyp | Ref
| Expression |
1 | | elioore 11440 |
. . . . . . . . . . . . . . . . . . . 20
   
  |
2 | 1 | adantl 466 |
. . . . . . . . . . . . . . . . . . 19
       |
3 | | 1rp 11105 |
. . . . . . . . . . . . . . . . . . . 20
 |
4 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
       |
5 | | 1red 9511 |
. . . . . . . . . . . . . . . . . . . 20
       |
6 | | eliooord 11465 |
. . . . . . . . . . . . . . . . . . . . . 22
   
    |
7 | 6 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . 21
     
   |
8 | 7 | simpld 459 |
. . . . . . . . . . . . . . . . . . . 20
       |
9 | 5, 2, 8 | ltled 9632 |
. . . . . . . . . . . . . . . . . . 19
       |
10 | 2, 4, 9 | rpgecld 11172 |
. . . . . . . . . . . . . . . . . 18
       |
11 | 10 | rprege0d 11144 |
. . . . . . . . . . . . . . . . . . . . 21
         |
12 | | flge0nn0 11782 |
. . . . . . . . . . . . . . . . . . . . 21
         |
13 | 11, 12 | syl 16 |
. . . . . . . . . . . . . . . . . . . 20
           |
14 | | nn0p1nn 10729 |
. . . . . . . . . . . . . . . . . . . 20
    
        |
15 | 13, 14 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
             |
16 | 15 | nnrpd 11136 |
. . . . . . . . . . . . . . . . . 18
             |
17 | 10, 16 | rpdivcld 11154 |
. . . . . . . . . . . . . . . . 17
               |
18 | | pntrlog2bnd.r |
. . . . . . . . . . . . . . . . . 18
  ψ     |
19 | 18 | pntrval 22943 |
. . . . . . . . . . . . . . . . 17
        
             ψ                     |
20 | 17, 19 | syl 16 |
. . . . . . . . . . . . . . . 16
                  ψ 
                   |
21 | 2, 15 | nndivred 10480 |
. . . . . . . . . . . . . . . . . . 19
               |
22 | | 2re 10501 |
. . . . . . . . . . . . . . . . . . . 20
 |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
       |
24 | | flltp1 11766 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
25 | 2, 24 | syl 16 |
. . . . . . . . . . . . . . . . . . . . 21
             |
26 | 15 | nncnd 10448 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
27 | 26 | mulid1d 9513 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
28 | 25, 27 | breqtrrd 4425 |
. . . . . . . . . . . . . . . . . . . 20
               |
29 | 2, 5, 16 | ltdivmuld 11184 |
. . . . . . . . . . . . . . . . . . . 20
                         |
30 | 28, 29 | mpbird 232 |
. . . . . . . . . . . . . . . . . . 19
               |
31 | | 1lt2 10598 |
. . . . . . . . . . . . . . . . . . . 20
 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
       |
33 | 21, 5, 23, 30, 32 | lttrd 9642 |
. . . . . . . . . . . . . . . . . 18
               |
34 | | chpeq0 22679 |
. . . . . . . . . . . . . . . . . . 19
          ψ         
           |
35 | 21, 34 | syl 16 |
. . . . . . . . . . . . . . . . . 18
      ψ         
           |
36 | 33, 35 | mpbird 232 |
. . . . . . . . . . . . . . . . 17
     ψ            |
37 | 36 | oveq1d 6214 |
. . . . . . . . . . . . . . . 16
      ψ                               |
38 | 20, 37 | eqtrd 2495 |
. . . . . . . . . . . . . . 15
                             |
39 | 38 | fveq2d 5802 |
. . . . . . . . . . . . . 14
           
                         |
40 | | 0red 9497 |
. . . . . . . . . . . . . . 15
       |
41 | 17 | rpge0d 11141 |
. . . . . . . . . . . . . . 15
               |
42 | 40, 21, 41 | abssuble0d 13036 |
. . . . . . . . . . . . . 14
                               |
43 | 21 | recnd 9522 |
. . . . . . . . . . . . . . 15
               |
44 | 43 | subid1d 9818 |
. . . . . . . . . . . . . 14
                         |
45 | 39, 42, 44 | 3eqtrd 2499 |
. . . . . . . . . . . . 13
           
                   |
46 | 13 | nn0red 10747 |
. . . . . . . . . . . . . . . 16
           |
47 | | pntsval.1 |
. . . . . . . . . . . . . . . . 17
            Λ       ψ        |
48 | 47 | pntsval2 22957 |
. . . . . . . . . . . . . . . 16
             
               Λ         
 Λ  Λ        |
49 | 46, 48 | syl 16 |
. . . . . . . . . . . . . . 15
             
               Λ         
 Λ  Λ        |
50 | 13 | nn0cnd 10748 |
. . . . . . . . . . . . . . . . 17
           |
51 | | 1cnd 9512 |
. . . . . . . . . . . . . . . . 17
       |
52 | 50, 51 | pncand 9830 |
. . . . . . . . . . . . . . . 16
                   |
53 | 52 | fveq2d 5802 |
. . . . . . . . . . . . . . 15
                           |
54 | 47 | pntsval2 22957 |
. . . . . . . . . . . . . . . . 17
                 Λ       
   Λ  Λ        |
55 | 2, 54 | syl 16 |
. . . . . . . . . . . . . . . 16
                     Λ       
   Λ  Λ        |
56 | | flidm 11774 |
. . . . . . . . . . . . . . . . . . 19
               |
57 | 2, 56 | syl 16 |
. . . . . . . . . . . . . . . . . 18
                   |
58 | 57 | oveq2d 6215 |
. . . . . . . . . . . . . . . . 17
                           |
59 | 58 | sumeq1d 13295 |
. . . . . . . . . . . . . . . 16
                     Λ       
   Λ  Λ                  Λ       
   Λ  Λ        |
60 | 55, 59 | eqtr4d 2498 |
. . . . . . . . . . . . . . 15
                         Λ       
   Λ  Λ        |
61 | 49, 53, 60 | 3eqtr4d 2505 |
. . . . . . . . . . . . . 14
                       |
62 | 52 | fveq2d 5802 |
. . . . . . . . . . . . . . 15
                           |
63 | 62 | oveq2d 6215 |
. . . . . . . . . . . . . 14
                               |
64 | 61, 63 | oveq12d 6217 |
. . . . . . . . . . . . 13
                                                   |
65 | 45, 64 | oveq12d 6217 |
. . . . . . . . . . . 12
                                                                               |
66 | 2 | recnd 9522 |
. . . . . . . . . . . . . . . . . . 19
       |
67 | 66 | div1d 10209 |
. . . . . . . . . . . . . . . . . 18
         |
68 | 67 | fveq2d 5802 |
. . . . . . . . . . . . . . . . 17
                 |
69 | 18 | pntrf 22944 |
. . . . . . . . . . . . . . . . . . 19
     |
70 | 69 | ffvelrni 5950 |
. . . . . . . . . . . . . . . . . 18

      |
71 | 10, 70 | syl 16 |
. . . . . . . . . . . . . . . . 17
           |
72 | 68, 71 | eqeltrd 2542 |
. . . . . . . . . . . . . . . 16
             |
73 | 72 | recnd 9522 |
. . . . . . . . . . . . . . 15
             |
74 | 73 | abscld 13039 |
. . . . . . . . . . . . . 14
           
     |
75 | 74 | recnd 9522 |
. . . . . . . . . . . . 13
           
     |
76 | 75 | mul01d 9678 |
. . . . . . . . . . . 12
                   |
77 | 65, 76 | oveq12d 6217 |
. . . . . . . . . . 11
                                                                                               |
78 | 47 | pntsf 22954 |
. . . . . . . . . . . . . . . . 17
     |
79 | 78 | ffvelrni 5950 |
. . . . . . . . . . . . . . . 16
       |
80 | 2, 79 | syl 16 |
. . . . . . . . . . . . . . 15
           |
81 | | pntrlog2bnd.t |
. . . . . . . . . . . . . . . . . . 19
              |
82 | | relogcl 22159 |
. . . . . . . . . . . . . . . . . . . . 21

      |
83 | | remulcl 9477 |
. . . . . . . . . . . . . . . . . . . . 21
               |
84 | 82, 83 | sylan2 474 |
. . . . . . . . . . . . . . . . . . . 20
 
         |
85 | | 0red 9497 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
86 | 84, 85 | ifclda 3928 |
. . . . . . . . . . . . . . . . . . 19
              |
87 | 81, 86 | fmpti 5974 |
. . . . . . . . . . . . . . . . . 18
     |
88 | 87 | ffvelrni 5950 |
. . . . . . . . . . . . . . . . 17
               |
89 | 46, 88 | syl 16 |
. . . . . . . . . . . . . . . 16
               |
90 | 23, 89 | remulcld 9524 |
. . . . . . . . . . . . . . 15
                 |
91 | 80, 90 | resubcld 9886 |
. . . . . . . . . . . . . 14
                       |
92 | 21, 91 | remulcld 9524 |
. . . . . . . . . . . . 13
                                 |
93 | 92 | recnd 9522 |
. . . . . . . . . . . 12
                                 |
94 | 93 | subid1d 9818 |
. . . . . . . . . . 11
                                                             |
95 | 77, 94 | eqtrd 2495 |
. . . . . . . . . 10
                                                                                             |
96 | 2 | flcld 11764 |
. . . . . . . . . . . . . 14
           |
97 | | fzval3 11721 |
. . . . . . . . . . . . . 14
              ..^         |
98 | 96, 97 | syl 16 |
. . . . . . . . . . . . 13
              ..^         |
99 | 98 | eqcomd 2462 |
. . . . . . . . . . . 12
      ..^                 |
100 | 10 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . 21
              
  |
101 | | elfznn 11594 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
102 | 101 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . 22
              
  |
103 | 102 | nnrpd 11136 |
. . . . . . . . . . . . . . . . . . . . 21
              
  |
104 | 100, 103 | rpdivcld 11154 |
. . . . . . . . . . . . . . . . . . . 20
              
    |
105 | 69 | ffvelrni 5950 |
. . . . . . . . . . . . . . . . . . . 20
  
        |
106 | 104, 105 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
              
        |
107 | 106 | recnd 9522 |
. . . . . . . . . . . . . . . . . 18
              
        |
108 | 107 | abscld 13039 |
. . . . . . . . . . . . . . . . 17
              
            |
109 | 108 | recnd 9522 |
. . . . . . . . . . . . . . . 16
              
            |
110 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
              
  |
111 | 103, 110 | rpaddcld 11152 |
. . . . . . . . . . . . . . . . . . . . 21
              
    |
112 | 100, 111 | rpdivcld 11154 |
. . . . . . . . . . . . . . . . . . . 20
              
      |
113 | 69 | ffvelrni 5950 |
. . . . . . . . . . . . . . . . . . . 20
    
          |
114 | 112, 113 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
              
          |
115 | 114 | recnd 9522 |
. . . . . . . . . . . . . . . . . 18
              
          |
116 | 115 | abscld 13039 |
. . . . . . . . . . . . . . . . 17
              
              |
117 | 116 | recnd 9522 |
. . . . . . . . . . . . . . . 16
              
              |
118 | 109, 117 | negsubdi2d 9845 |
. . . . . . . . . . . . . . 15
              
                                                   |
119 | 118 | eqcomd 2462 |
. . . . . . . . . . . . . 14
              
       
                                           |
120 | 102 | nncnd 10448 |
. . . . . . . . . . . . . . . . 17
              
  |
121 | | 1cnd 9512 |
. . . . . . . . . . . . . . . . 17
              
  |
122 | 120, 121 | pncand 9830 |
. . . . . . . . . . . . . . . 16
              
      |
123 | 122 | fveq2d 5802 |
. . . . . . . . . . . . . . 15
              
              |
124 | 122 | fveq2d 5802 |
. . . . . . . . . . . . . . . . 17
              
              |
125 | | rpre 11107 |
. . . . . . . . . . . . . . . . . . . 20

  |
126 | | eleq1 2526 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
127 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
128 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
129 | 127, 128 | oveq12d 6217 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
130 | 126, 129 | ifbieq1d 3919 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
131 | | ovex 6224 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
132 | | c0ex 9490 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
133 | 131, 132 | ifex 3965 |
. . . . . . . . . . . . . . . . . . . . 21
            |
134 | 130, 81, 133 | fvmpt 5882 |
. . . . . . . . . . . . . . . . . . . 20
                  |
135 | 125, 134 | syl 16 |
. . . . . . . . . . . . . . . . . . 19

                 |
136 | | iftrue 3904 |
. . . . . . . . . . . . . . . . . . 19

                   |
137 | 135, 136 | eqtrd 2495 |
. . . . . . . . . . . . . . . . . 18

            |
138 | 103, 137 | syl 16 |
. . . . . . . . . . . . . . . . 17
              
            |
139 | 124, 138 | eqtrd 2495 |
. . . . . . . . . . . . . . . 16
              
                |
140 | 139 | oveq2d 6215 |
. . . . . . . . . . . . . . 15
              
                    |
141 | 123, 140 | oveq12d 6217 |
. . . . . . . . . . . . . 14
              
                                    |
142 | 119, 141 | oveq12d 6217 |
. . . . . . . . . . . . 13
              
                                                                 
                       |
143 | 108, 116 | resubcld 9886 |
. . . . . . . . . . . . . . 15
              
       
                  |
144 | 143 | recnd 9522 |
. . . . . . . . . . . . . 14
              
       
                  |
145 | 102 | nnred 10447 |
. . . . . . . . . . . . . . . . 17
              
  |
146 | 78 | ffvelrni 5950 |
. . . . . . . . . . . . . . . . 17
       |
147 | 145, 146 | syl 16 |
. . . . . . . . . . . . . . . 16
              
      |
148 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . 17
              
  |
149 | 103 | relogcld 22204 |
. . . . . . . . . . . . . . . . . 18
              
      |
150 | 145, 149 | remulcld 9524 |
. . . . . . . . . . . . . . . . 17
              
        |
151 | 148, 150 | remulcld 9524 |
. . . . . . . . . . . . . . . 16
              
          |
152 | 147, 151 | resubcld 9886 |
. . . . . . . . . . . . . . 15
              
                |
153 | 152 | recnd 9522 |
. . . . . . . . . . . . . 14
              
                |
154 | 144, 153 | mulneg1d 9907 |
. . . . . . . . . . . . 13
              
                                                                                    |
155 | 142, 154 | eqtrd 2495 |
. . . . . . . . . . . 12
              
                                                                 
                       |
156 | 99, 155 | sumeq12rdv 13301 |
. . . . . . . . . . 11
       ..^                            
                         
                            
                       |
157 | | fzfid 11911 |
. . . . . . . . . . . 12
               |
158 | 143, 152 | remulcld 9524 |
. . . . . . . . . . . . 13
              
                                          |
159 | 158 | recnd 9522 |
. . . . . . . . . . . 12
              
                                          |
160 | 157, 159 | fsumneg 13371 |
. . . . . . . . . . 11
                                                                                     
                       |
161 | 156, 160 | eqtrd 2495 |
. . . . . . . . . 10
       ..^                            
                                                      
                       |
162 | 95, 161 | oveq12d 6217 |
. . . . . . . . 9
                                                                    ..^                                                                                                               
                        |
163 | | oveq2 6207 |
. . . . . . . . . . . . . 14
       |
164 | 163 | fveq2d 5802 |
. . . . . . . . . . . . 13
               |
165 | 164 | fveq2d 5802 |
. . . . . . . . . . . 12
       
               |
166 | | oveq1 6206 |
. . . . . . . . . . . . . 14
       |
167 | 166 | fveq2d 5802 |
. . . . . . . . . . . . 13
          
    |
168 | 166 | fveq2d 5802 |
. . . . . . . . . . . . . 14
          
    |
169 | 168 | oveq2d 6215 |
. . . . . . . . . . . . 13
                   |
170 | 167, 169 | oveq12d 6217 |
. . . . . . . . . . . 12
            
                      |
171 | 165, 170 | jca 532 |
. . . . . . . . . . 11
                                                 
       |
172 | | oveq2 6207 |
. . . . . . . . . . . . . 14
           |
173 | 172 | fveq2d 5802 |
. . . . . . . . . . . . 13
                   |
174 | 173 | fveq2d 5802 |
. . . . . . . . . . . 12
         
                 |
175 | | oveq1 6206 |
. . . . . . . . . . . . . 14
           |
176 | 175 | fveq2d 5802 |
. . . . . . . . . . . . 13
                   |
177 | 175 | fveq2d 5802 |
. . . . . . . . . . . . . 14
                   |
178 | 177 | oveq2d 6215 |
. . . . . . . . . . . . 13
                       |
179 | 176, 178 | oveq12d 6217 |
. . . . . . . . . . . 12
              
                          |
180 | 174, 179 | jca 532 |
. . . . . . . . . . 11
                                                                 |
181 | | oveq2 6207 |
. . . . . . . . . . . . . 14
       |
182 | 181 | fveq2d 5802 |
. . . . . . . . . . . . 13
               |
183 | 182 | fveq2d 5802 |
. . . . . . . . . . . 12
       
               |
184 | | oveq1 6206 |
. . . . . . . . . . . . . . . . 17
       |
185 | | 1m1e0 10500 |
. . . . . . . . . . . . . . . . 17
   |
186 | 184, 185 | syl6eq 2511 |
. . . . . . . . . . . . . . . 16
     |
187 | 186 | fveq2d 5802 |
. . . . . . . . . . . . . . 15
             |
188 | | 0re 9496 |
. . . . . . . . . . . . . . . 16
 |
189 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
190 | | 0z 10767 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
191 | | flid 11773 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
192 | 190, 191 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
193 | 189, 192 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . . . . 21
       |
194 | 193 | oveq2d 6215 |
. . . . . . . . . . . . . . . . . . . 20
               |
195 | | fz10 11586 |
. . . . . . . . . . . . . . . . . . . 20
     |
196 | 194, 195 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . . 19
           |
197 | 196 | sumeq1d 13295 |
. . . . . . . . . . . . . . . . . 18
            Λ       ψ        Λ       ψ        |
198 | | sum0 13315 |
. . . . . . . . . . . . . . . . . 18
  Λ       ψ       |
199 | 197, 198 | syl6eq 2511 |
. . . . . . . . . . . . . . . . 17
            Λ       ψ        |
200 | 199, 47, 132 | fvmpt 5882 |
. . . . . . . . . . . . . . . 16
       |
201 | 188, 200 | ax-mp 5 |
. . . . . . . . . . . . . . 15
     |
202 | 187, 201 | syl6eq 2511 |
. . . . . . . . . . . . . 14
         |
203 | 186 | fveq2d 5802 |
. . . . . . . . . . . . . . . . 17
             |
204 | | rpne0 11116 |
. . . . . . . . . . . . . . . . . . . . 21

  |
205 | 204 | necon2bi 2688 |
. . . . . . . . . . . . . . . . . . . 20

  |
206 | | iffalse 3906 |
. . . . . . . . . . . . . . . . . . . 20
              |
207 | 205, 206 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
              |
208 | 207, 81, 132 | fvmpt 5882 |
. . . . . . . . . . . . . . . . . 18
       |
209 | 188, 208 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
     |
210 | 203, 209 | syl6eq 2511 |
. . . . . . . . . . . . . . . 16
         |
211 | 210 | oveq2d 6215 |
. . . . . . . . . . . . . . 15
             |
212 | | 2t0e0 10587 |
. . . . . . . . . . . . . . 15
   |
213 | 211, 212 | syl6eq 2511 |
. . . . . . . . . . . . . 14
           |
214 | 202, 213 | oveq12d 6217 |
. . . . . . . . . . . . 13
            
        |
215 | | 0m0e0 10541 |
. . . . . . . . . . . . 13
   |
216 | 214, 215 | syl6eq 2511 |
. . . . . . . . . . . 12
            
      |
217 | 183, 216 | jca 532 |
. . . . . . . . . . 11
                                         |
218 | | oveq2 6207 |
. . . . . . . . . . . . . 14
                   |
219 | 218 | fveq2d 5802 |
. . . . . . . . . . . . 13
                           |
220 | 219 | fveq2d 5802 |
. . . . . . . . . . . 12
             
                     |
221 | | oveq1 6206 |
. . . . . . . . . . . . . 14
                   |
222 | 221 | fveq2d 5802 |
. . . . . . . . . . . . 13
                           |
223 | 221 | fveq2d 5802 |
. . . . . . . . . . . . . 14
                           |
224 | 223 | oveq2d 6215 |
. . . . . . . . . . . . 13
                               |
225 | 222, 224 | oveq12d 6217 |
. . . . . . . . . . . 12
                  
                                  |
226 | 220, 225 | jca 532 |
. . . . . . . . . . 11
                                                                                 |
227 | | nnuz 11006 |
. . . . . . . . . . . 12
     |
228 | 15, 227 | syl6eleq 2552 |
. . . . . . . . . . 11
                 |
229 | 10 | adantr 465 |
. . . . . . . . . . . . . . . 16
                   |
230 | | elfznn 11594 |
. . . . . . . . . . . . . . . . . 18
             |
231 | 230 | adantl 466 |
. . . . . . . . . . . . . . . . 17
                   |
232 | 231 | nnrpd 11136 |
. . . . . . . . . . . . . . . 16
                   |
233 | 229, 232 | rpdivcld 11154 |
. . . . . . . . . . . . . . 15
                     |
234 | 69 | ffvelrni 5950 |
. . . . . . . . . . . . . . 15
  
        |
235 | 233, 234 | syl 16 |
. . . . . . . . . . . . . 14
                         |
236 | 235 | recnd 9522 |
. . . . . . . . . . . . 13
                         |
237 | 236 | abscld 13039 |
. . . . . . . . . . . 12
                       
     |
238 | 237 | recnd 9522 |
. . . . . . . . . . 11
                       
     |
239 | 231 | nnred 10447 |
. . . . . . . . . . . . . . 15
                   |
240 | | 1red 9511 |
. . . . . . . . . . . . . . 15
                   |
241 | 239, 240 | resubcld 9886 |
. . . . . . . . . . . . . 14
                     |
242 | 78 | ffvelrni 5950 |
. . . . . . . . . . . . . 14
           |
243 | 241, 242 | syl 16 |
. . . . . . . . . . . . 13
                         |
244 | 22 | a1i 11 |
. . . . . . . . . . . . . 14
                   |
245 | 87 | ffvelrni 5950 |
. . . . . . . . . . . . . . 15
           |
246 | 241, 245 | syl 16 |
. . . . . . . . . . . . . 14
                         |
247 | 244, 246 | remulcld 9524 |
. . . . . . . . . . . . 13
                           |
248 | 243, 247 | resubcld 9886 |
. . . . . . . . . . . 12
                            
      |
249 | 248 | recnd 9522 |
. . . . . . . . . . 11
                            
      |
250 | 171, 180,
217, 226, 228, 238, 249 | fsumparts 13386 |
. . . . . . . . . 10
       ..^                                            
                                                                            ..^                            
                            |
251 | 147 | recnd 9522 |
. . . . . . . . . . . . . 14
              
      |
252 | 87 | ffvelrni 5950 |
. . . . . . . . . . . . . . . . 17
       |
253 | 145, 252 | syl 16 |
. . . . . . . . . . . . . . . 16
              
      |
254 | 148, 253 | remulcld 9524 |
. . . . . . . . . . . . . . 15
              
        |
255 | 254 | recnd 9522 |
. . . . . . . . . . . . . 14
              
        |
256 | | 1red 9511 |
. . . . . . . . . . . . . . . . 17
              
  |
257 | 145, 256 | resubcld 9886 |
. . . . . . . . . . . . . . . 16
              
    |
258 | 78 | ffvelrni 5950 |
. . . . . . . . . . . . . . . 16
           |
259 | 257, 258 | syl 16 |
. . . . . . . . . . . . . . 15
              
        |
260 | 259 | recnd 9522 |
. . . . . . . . . . . . . 14
              
        |
261 | 87 | ffvelrni 5950 |
. . . . . . . . . . . . . . . . 17
           |
262 | 257, 261 | syl 16 |
. . . . . . . . . . . . . . . 16
              
        |
263 | 148, 262 | remulcld 9524 |
. . . . . . . . . . . . . . 15
              
    
     |
264 | 263 | recnd 9522 |
. . . . . . . . . . . . . 14
              
    
     |
265 | 251, 255,
260, 264 | sub4d 9878 |
. . . . . . . . . . . . 13
              
                                                              |
266 | 124 | oveq2d 6215 |
. . . . . . . . . . . . . . 15
              
                  |
267 | 123, 266 | oveq12d 6217 |
. . . . . . . . . . . . . 14
              
                                  |
268 | 267 | oveq1d 6214 |
. . . . . . . . . . . . 13
              
                                                              
       |
269 | | 2cnd 10504 |
. . . . . . . . . . . . . . 15
              
  |
270 | 253 | recnd 9522 |
. . . . . . . . . . . . . . 15
              
      |
271 | 262 | recnd 9522 |
. . . . . . . . . . . . . . 15
              
        |
272 | 269, 270,
271 | subdid 9910 |
. . . . . . . . . . . . . 14
              
                         
      |
273 | 272 | oveq2d 6215 |
. . . . . . . . . . . . 13
              
                                                            |
274 | 265, 268,
273 | 3eqtr4d 2505 |
. . . . . . . . . . . 12
              
                                                                    |
275 | 274 | oveq2d 6215 |
. . . . . . . . . . 11
              
       
                                   
                          
                     |
276 | 99, 275 | sumeq12rdv 13301 |
. . . . . . . . . 10
       ..^                                            
             
                             
                     |
277 | 250, 276 | eqtr3d 2497 |
. . . . . . . . 9
                                                                    ..^                                                       
                             
                     |
278 | 157, 159 | fsumcl 13327 |
. . . . . . . . . 10
                                 
                       |
279 | 93, 278 | subnegd 9836 |
. . . . . . . . 9
                                                             
                                                                                                      |
280 | 162, 277,
279 | 3eqtr3rd 2504 |
. . . . . . . 8
                                                            
                      
                             
                     |
281 | 10 | relogcld 22204 |
. . . . . . . . . 10
           |
282 | 281 | recnd 9522 |
. . . . . . . . 9
           |
283 | 66, 282 | mulcomd 9517 |
. . . . . . . 8
                   |
284 | 280, 283 | oveq12d 6217 |
. . . . . . 7
                                                                                                                          
                            |
285 | 147, 259 | resubcld 9886 |
. . . . . . . . . . . 12
              
        
     |
286 | 253, 262 | resubcld 9886 |
. . . . . . . . . . . . 13
              
        
     |
287 | 148, 286 | remulcld 9524 |
. . . . . . . . . . . 12
              
                |
288 | 285, 287 | resubcld 9886 |
. . . . . . . . . . 11
              
                              |
289 | 108, 288 | remulcld 9524 |
. . . . . . . . . 10
              
       
                                  |
290 | 157, 289 | fsumrecl 13328 |
. . . . . . . . 9
                                   
                     |
291 | 290 | recnd 9522 |
. . . . . . . 8
                                   
                     |
292 | 2, 8 | rplogcld 22210 |
. . . . . . . . 9
           |
293 | 292 | rpne0d 11142 |
. . . . . . . 8
           |
294 | 10 | rpne0d 11142 |
. . . . . . . 8
       |
295 | 291, 282,
66, 293, 294 | divdiv1d 10248 |
. . . . . . 7
                                     
                                                        
                            |
296 | 284, 295 | eqtr4d 2498 |
. . . . . 6
                                                                                                                           
                           |
297 | 296 | oveq2d 6215 |
. . . . 5
                                                                                            
                                                                                                                                                     
                            |
298 | 71 | recnd 9522 |
. . . . . . . . . 10
           |
299 | 298 | abscld 13039 |
. . . . . . . . 9
               |
300 | 299, 281 | remulcld 9524 |
. . . . . . . 8
                     |
301 | 108, 285 | remulcld 9524 |
. . . . . . . . . 10
              
       
                  |
302 | 157, 301 | fsumrecl 13328 |
. . . . . . . . 9
                                         |
303 | 302, 292 | rerpdivcld 11164 |
. . . . . . . 8
                                               |
304 | 300, 303 | resubcld 9886 |
. . . . . . 7
                                                               |
305 | 304 | recnd 9522 |
. . . . . 6
                                                               |
306 | 291, 282,
293 | divcld 10217 |
. . . . . 6
                                    
                          |
307 | 305, 306,
66, 294 | divdird 10255 |
. . . . 5
                                                                                              
                                                                                                                     
                            |
308 | 300 | recnd 9522 |
. . . . . . . 8
                     |
309 | 303 | recnd 9522 |
. . . . . . . 8
                                               |
310 | 308, 309,
306 | subsubd 9857 |
. . . . . . 7
                                                                                            
                                                                                                                  
                           |
311 | | 2cnd 10504 |
. . . . . . . . . . . 12
       |
312 | 270, 271 | subcld 9829 |
. . . . . . . . . . . . 13
              
        
     |
313 | 109, 312 | mulcld 9516 |
. . . . . . . . . . . 12
              
       
                  |
314 | 157, 311,
313 | fsummulc2 13368 |
. . . . . . . . . . 11
                                         
                                     |
315 | 285 | recnd 9522 |
. . . . . . . . . . . . . . 15
              
        
     |
316 | 269, 312 | mulcld 9516 |
. . . . . . . . . . . . . . 15
              
                |
317 | 315, 316 | nncand 9834 |
. . . . . . . . . . . . . 14
              
                      
                                   |
318 | 317 | oveq2d 6215 |
. . . . . . . . . . . . 13
 |