Step | Hyp | Ref
| Expression |
1 | | elioore 11700 |
. . . . . . . . . . . . . . . . . . . 20
   
  |
2 | 1 | adantl 472 |
. . . . . . . . . . . . . . . . . . 19
       |
3 | | 1rp 11340 |
. . . . . . . . . . . . . . . . . . . 20
 |
4 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
       |
5 | | 1red 9689 |
. . . . . . . . . . . . . . . . . . . 20
       |
6 | | eliooord 11728 |
. . . . . . . . . . . . . . . . . . . . . 22
   
    |
7 | 6 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . 21
     
   |
8 | 7 | simpld 465 |
. . . . . . . . . . . . . . . . . . . 20
       |
9 | 5, 2, 8 | ltled 9814 |
. . . . . . . . . . . . . . . . . . 19
       |
10 | 2, 4, 9 | rpgecld 11411 |
. . . . . . . . . . . . . . . . . 18
       |
11 | 10 | rprege0d 11382 |
. . . . . . . . . . . . . . . . . . . . 21
         |
12 | | flge0nn0 12092 |
. . . . . . . . . . . . . . . . . . . . 21
         |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
           |
14 | | nn0p1nn 10943 |
. . . . . . . . . . . . . . . . . . . 20
    
        |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
             |
16 | 15 | nnrpd 11373 |
. . . . . . . . . . . . . . . . . 18
             |
17 | 10, 16 | rpdivcld 11392 |
. . . . . . . . . . . . . . . . 17
               |
18 | | pntrlog2bnd.r |
. . . . . . . . . . . . . . . . . 18
  ψ     |
19 | 18 | pntrval 24456 |
. . . . . . . . . . . . . . . . 17
        
             ψ                     |
20 | 17, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
                  ψ 
                   |
21 | 2, 15 | nndivred 10691 |
. . . . . . . . . . . . . . . . . . 19
               |
22 | | 2re 10712 |
. . . . . . . . . . . . . . . . . . . 20
 |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
       |
24 | | flltp1 12074 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
25 | 2, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
             |
26 | 15 | nncnd 10658 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
27 | 26 | mulid1d 9691 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
28 | 25, 27 | breqtrrd 4445 |
. . . . . . . . . . . . . . . . . . . 20
               |
29 | 2, 5, 16 | ltdivmuld 11423 |
. . . . . . . . . . . . . . . . . . . 20
                         |
30 | 28, 29 | mpbird 240 |
. . . . . . . . . . . . . . . . . . 19
               |
31 | | 1lt2 10810 |
. . . . . . . . . . . . . . . . . . . 20
 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
       |
33 | 21, 5, 23, 30, 32 | lttrd 9827 |
. . . . . . . . . . . . . . . . . 18
               |
34 | | chpeq0 24192 |
. . . . . . . . . . . . . . . . . . 19
          ψ         
           |
35 | 21, 34 | syl 17 |
. . . . . . . . . . . . . . . . . 18
      ψ         
           |
36 | 33, 35 | mpbird 240 |
. . . . . . . . . . . . . . . . 17
     ψ            |
37 | 36 | oveq1d 6335 |
. . . . . . . . . . . . . . . 16
      ψ                               |
38 | 20, 37 | eqtrd 2496 |
. . . . . . . . . . . . . . 15
                             |
39 | 38 | fveq2d 5896 |
. . . . . . . . . . . . . 14
           
                         |
40 | | 0red 9675 |
. . . . . . . . . . . . . . 15
       |
41 | 17 | rpge0d 11379 |
. . . . . . . . . . . . . . 15
               |
42 | 40, 21, 41 | abssuble0d 13549 |
. . . . . . . . . . . . . 14
                               |
43 | 21 | recnd 9700 |
. . . . . . . . . . . . . . 15
               |
44 | 43 | subid1d 10006 |
. . . . . . . . . . . . . 14
                         |
45 | 39, 42, 44 | 3eqtrd 2500 |
. . . . . . . . . . . . 13
           
                   |
46 | 13 | nn0red 10960 |
. . . . . . . . . . . . . . . 16
           |
47 | | pntsval.1 |
. . . . . . . . . . . . . . . . 17
            Λ       ψ        |
48 | 47 | pntsval2 24470 |
. . . . . . . . . . . . . . . 16
             
               Λ         
 Λ  Λ        |
49 | 46, 48 | syl 17 |
. . . . . . . . . . . . . . 15
             
               Λ         
 Λ  Λ        |
50 | 13 | nn0cnd 10961 |
. . . . . . . . . . . . . . . . 17
           |
51 | | 1cnd 9690 |
. . . . . . . . . . . . . . . . 17
       |
52 | 50, 51 | pncand 10018 |
. . . . . . . . . . . . . . . 16
                   |
53 | 52 | fveq2d 5896 |
. . . . . . . . . . . . . . 15
                           |
54 | 47 | pntsval2 24470 |
. . . . . . . . . . . . . . . . 17
                 Λ       
   Λ  Λ        |
55 | 2, 54 | syl 17 |
. . . . . . . . . . . . . . . 16
                     Λ       
   Λ  Λ        |
56 | | flidm 12083 |
. . . . . . . . . . . . . . . . . . 19
               |
57 | 2, 56 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                   |
58 | 57 | oveq2d 6336 |
. . . . . . . . . . . . . . . . 17
                           |
59 | 58 | sumeq1d 13822 |
. . . . . . . . . . . . . . . 16
                     Λ       
   Λ  Λ                  Λ       
   Λ  Λ        |
60 | 55, 59 | eqtr4d 2499 |
. . . . . . . . . . . . . . 15
                         Λ       
   Λ  Λ        |
61 | 49, 53, 60 | 3eqtr4d 2506 |
. . . . . . . . . . . . . 14
                       |
62 | 52 | fveq2d 5896 |
. . . . . . . . . . . . . . 15
                           |
63 | 62 | oveq2d 6336 |
. . . . . . . . . . . . . 14
                               |
64 | 61, 63 | oveq12d 6338 |
. . . . . . . . . . . . 13
                                                   |
65 | 45, 64 | oveq12d 6338 |
. . . . . . . . . . . 12
                                                                               |
66 | 2 | recnd 9700 |
. . . . . . . . . . . . . . . . . . 19
       |
67 | 66 | div1d 10408 |
. . . . . . . . . . . . . . . . . 18
         |
68 | 67 | fveq2d 5896 |
. . . . . . . . . . . . . . . . 17
                 |
69 | 18 | pntrf 24457 |
. . . . . . . . . . . . . . . . . . 19
     |
70 | 69 | ffvelrni 6049 |
. . . . . . . . . . . . . . . . . 18

      |
71 | 10, 70 | syl 17 |
. . . . . . . . . . . . . . . . 17
           |
72 | 68, 71 | eqeltrd 2540 |
. . . . . . . . . . . . . . . 16
             |
73 | 72 | recnd 9700 |
. . . . . . . . . . . . . . 15
             |
74 | 73 | abscld 13553 |
. . . . . . . . . . . . . 14
           
     |
75 | 74 | recnd 9700 |
. . . . . . . . . . . . 13
           
     |
76 | 75 | mul01d 9863 |
. . . . . . . . . . . 12
                   |
77 | 65, 76 | oveq12d 6338 |
. . . . . . . . . . 11
                                                                                               |
78 | 47 | pntsf 24467 |
. . . . . . . . . . . . . . . . 17
     |
79 | 78 | ffvelrni 6049 |
. . . . . . . . . . . . . . . 16
       |
80 | 2, 79 | syl 17 |
. . . . . . . . . . . . . . 15
           |
81 | | pntrlog2bnd.t |
. . . . . . . . . . . . . . . . . . 19
              |
82 | | relogcl 23581 |
. . . . . . . . . . . . . . . . . . . . 21

      |
83 | | remulcl 9655 |
. . . . . . . . . . . . . . . . . . . . 21
               |
84 | 82, 83 | sylan2 481 |
. . . . . . . . . . . . . . . . . . . 20
 
         |
85 | | 0red 9675 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
86 | 84, 85 | ifclda 3925 |
. . . . . . . . . . . . . . . . . . 19
              |
87 | 81, 86 | fmpti 6073 |
. . . . . . . . . . . . . . . . . 18
     |
88 | 87 | ffvelrni 6049 |
. . . . . . . . . . . . . . . . 17
               |
89 | 46, 88 | syl 17 |
. . . . . . . . . . . . . . . 16
               |
90 | 23, 89 | remulcld 9702 |
. . . . . . . . . . . . . . 15
                 |
91 | 80, 90 | resubcld 10080 |
. . . . . . . . . . . . . 14
                       |
92 | 21, 91 | remulcld 9702 |
. . . . . . . . . . . . 13
                                 |
93 | 92 | recnd 9700 |
. . . . . . . . . . . 12
                                 |
94 | 93 | subid1d 10006 |
. . . . . . . . . . 11
                                                             |
95 | 77, 94 | eqtrd 2496 |
. . . . . . . . . 10
                                                                                             |
96 | 2 | flcld 12072 |
. . . . . . . . . . . . . 14
           |
97 | | fzval3 12020 |
. . . . . . . . . . . . . 14
              ..^         |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . 13
              ..^         |
99 | 98 | eqcomd 2468 |
. . . . . . . . . . . 12
      ..^                 |
100 | 10 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . 21
              
  |
101 | | elfznn 11863 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
102 | 101 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . 22
              
  |
103 | 102 | nnrpd 11373 |
. . . . . . . . . . . . . . . . . . . . 21
              
  |
104 | 100, 103 | rpdivcld 11392 |
. . . . . . . . . . . . . . . . . . . 20
              
    |
105 | 69 | ffvelrni 6049 |
. . . . . . . . . . . . . . . . . . . 20
  
        |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
              
        |
107 | 106 | recnd 9700 |
. . . . . . . . . . . . . . . . . 18
              
        |
108 | 107 | abscld 13553 |
. . . . . . . . . . . . . . . . 17
              
            |
109 | 108 | recnd 9700 |
. . . . . . . . . . . . . . . 16
              
            |
110 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
              
  |
111 | 103, 110 | rpaddcld 11390 |
. . . . . . . . . . . . . . . . . . . . 21
              
    |
112 | 100, 111 | rpdivcld 11392 |
. . . . . . . . . . . . . . . . . . . 20
              
      |
113 | 69 | ffvelrni 6049 |
. . . . . . . . . . . . . . . . . . . 20
    
          |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
              
          |
115 | 114 | recnd 9700 |
. . . . . . . . . . . . . . . . . 18
              
          |
116 | 115 | abscld 13553 |
. . . . . . . . . . . . . . . . 17
              
              |
117 | 116 | recnd 9700 |
. . . . . . . . . . . . . . . 16
              
              |
118 | 109, 117 | negsubdi2d 10033 |
. . . . . . . . . . . . . . 15
              
                                                   |
119 | 118 | eqcomd 2468 |
. . . . . . . . . . . . . 14
              
       
                                           |
120 | 102 | nncnd 10658 |
. . . . . . . . . . . . . . . . 17
              
  |
121 | | 1cnd 9690 |
. . . . . . . . . . . . . . . . 17
              
  |
122 | 120, 121 | pncand 10018 |
. . . . . . . . . . . . . . . 16
              
      |
123 | 122 | fveq2d 5896 |
. . . . . . . . . . . . . . 15
              
              |
124 | 122 | fveq2d 5896 |
. . . . . . . . . . . . . . . . 17
              
              |
125 | | rpre 11342 |
. . . . . . . . . . . . . . . . . . . 20

  |
126 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
127 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
128 | | fveq2 5892 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
129 | 127, 128 | oveq12d 6338 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
130 | 126, 129 | ifbieq1d 3916 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
131 | | ovex 6348 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
132 | | c0ex 9668 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
133 | 131, 132 | ifex 3961 |
. . . . . . . . . . . . . . . . . . . . 21
            |
134 | 130, 81, 133 | fvmpt 5976 |
. . . . . . . . . . . . . . . . . . . 20
                  |
135 | 125, 134 | syl 17 |
. . . . . . . . . . . . . . . . . . 19

                 |
136 | | iftrue 3899 |
. . . . . . . . . . . . . . . . . . 19

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

            |
138 | 103, 137 | syl 17 |
. . . . . . . . . . . . . . . . 17
              
            |
139 | 124, 138 | eqtrd 2496 |
. . . . . . . . . . . . . . . 16
              
                |
140 | 139 | oveq2d 6336 |
. . . . . . . . . . . . . . 15
              
                    |
141 | 123, 140 | oveq12d 6338 |
. . . . . . . . . . . . . 14
              
                                    |
142 | 119, 141 | oveq12d 6338 |
. . . . . . . . . . . . 13
              
                                                                 
                       |
143 | 108, 116 | resubcld 10080 |
. . . . . . . . . . . . . . 15
              
       
                  |
144 | 143 | recnd 9700 |
. . . . . . . . . . . . . 14
              
       
                  |
145 | 102 | nnred 10657 |
. . . . . . . . . . . . . . . . 17
              
  |
146 | 78 | ffvelrni 6049 |
. . . . . . . . . . . . . . . . 17
       |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . . 16
              
      |
148 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . 17
              
  |
149 | 103 | relogcld 23628 |
. . . . . . . . . . . . . . . . . 18
              
      |
150 | 145, 149 | remulcld 9702 |
. . . . . . . . . . . . . . . . 17
              
        |
151 | 148, 150 | remulcld 9702 |
. . . . . . . . . . . . . . . 16
              
          |
152 | 147, 151 | resubcld 10080 |
. . . . . . . . . . . . . . 15
              
                |
153 | 152 | recnd 9700 |
. . . . . . . . . . . . . 14
              
                |
154 | 144, 153 | mulneg1d 10104 |
. . . . . . . . . . . . 13
              
                                                                                    |
155 | 142, 154 | eqtrd 2496 |
. . . . . . . . . . . 12
              
                                                                 
                       |
156 | 99, 155 | sumeq12rdv 13828 |
. . . . . . . . . . 11
       ..^                            
                         
                            
                       |
157 | | fzfid 12224 |
. . . . . . . . . . . 12
               |
158 | 143, 152 | remulcld 9702 |
. . . . . . . . . . . . 13
              
                                          |
159 | 158 | recnd 9700 |
. . . . . . . . . . . 12
              
                                          |
160 | 157, 159 | fsumneg 13903 |
. . . . . . . . . . 11
                                                                                     
                       |
161 | 156, 160 | eqtrd 2496 |
. . . . . . . . . 10
       ..^                            
                                                      
                       |
162 | 95, 161 | oveq12d 6338 |
. . . . . . . . 9
                                                                    ..^                                                                                                               
                        |
163 | | oveq2 6328 |
. . . . . . . . . . . . . 14
       |
164 | 163 | fveq2d 5896 |
. . . . . . . . . . . . 13
               |
165 | 164 | fveq2d 5896 |
. . . . . . . . . . . 12
       
               |
166 | | oveq1 6327 |
. . . . . . . . . . . . . 14
       |
167 | 166 | fveq2d 5896 |
. . . . . . . . . . . . 13
          
    |
168 | 166 | fveq2d 5896 |
. . . . . . . . . . . . . 14
          
    |
169 | 168 | oveq2d 6336 |
. . . . . . . . . . . . 13
                   |
170 | 167, 169 | oveq12d 6338 |
. . . . . . . . . . . 12
            
                      |
171 | 165, 170 | jca 539 |
. . . . . . . . . . 11
                                                 
       |
172 | | oveq2 6328 |
. . . . . . . . . . . . . 14
           |
173 | 172 | fveq2d 5896 |
. . . . . . . . . . . . 13
                   |
174 | 173 | fveq2d 5896 |
. . . . . . . . . . . 12
         
                 |
175 | | oveq1 6327 |
. . . . . . . . . . . . . 14
           |
176 | 175 | fveq2d 5896 |
. . . . . . . . . . . . 13
                   |
177 | 175 | fveq2d 5896 |
. . . . . . . . . . . . . 14
                   |
178 | 177 | oveq2d 6336 |
. . . . . . . . . . . . 13
                       |
179 | 176, 178 | oveq12d 6338 |
. . . . . . . . . . . 12
              
                          |
180 | 174, 179 | jca 539 |
. . . . . . . . . . 11
                                                                 |
181 | | oveq2 6328 |
. . . . . . . . . . . . . 14
       |
182 | 181 | fveq2d 5896 |
. . . . . . . . . . . . 13
               |
183 | 182 | fveq2d 5896 |
. . . . . . . . . . . 12
       
               |
184 | | oveq1 6327 |
. . . . . . . . . . . . . . . . 17
       |
185 | | 1m1e0 10711 |
. . . . . . . . . . . . . . . . 17
   |
186 | 184, 185 | syl6eq 2512 |
. . . . . . . . . . . . . . . 16
     |
187 | 186 | fveq2d 5896 |
. . . . . . . . . . . . . . 15
             |
188 | | 0re 9674 |
. . . . . . . . . . . . . . . 16
 |
189 | | fveq2 5892 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
190 | | 0z 10982 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
191 | | flid 12082 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
192 | 190, 191 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
193 | 189, 192 | syl6eq 2512 |
. . . . . . . . . . . . . . . . . . . . 21
       |
194 | 193 | oveq2d 6336 |
. . . . . . . . . . . . . . . . . . . 20
               |
195 | | fz10 11855 |
. . . . . . . . . . . . . . . . . . . 20
     |
196 | 194, 195 | syl6eq 2512 |
. . . . . . . . . . . . . . . . . . 19
           |
197 | 196 | sumeq1d 13822 |
. . . . . . . . . . . . . . . . . 18
            Λ       ψ        Λ       ψ        |
198 | | sum0 13842 |
. . . . . . . . . . . . . . . . . 18
  Λ       ψ       |
199 | 197, 198 | syl6eq 2512 |
. . . . . . . . . . . . . . . . 17
            Λ       ψ        |
200 | 199, 47, 132 | fvmpt 5976 |
. . . . . . . . . . . . . . . 16
       |
201 | 188, 200 | ax-mp 5 |
. . . . . . . . . . . . . . 15
     |
202 | 187, 201 | syl6eq 2512 |
. . . . . . . . . . . . . 14
         |
203 | 186 | fveq2d 5896 |
. . . . . . . . . . . . . . . . 17
             |
204 | | rpne0 11351 |
. . . . . . . . . . . . . . . . . . . . 21

  |
205 | 204 | necon2bi 2666 |
. . . . . . . . . . . . . . . . . . . 20

  |
206 | 205 | iffalsed 3904 |
. . . . . . . . . . . . . . . . . . 19
              |
207 | 206, 81, 132 | fvmpt 5976 |
. . . . . . . . . . . . . . . . . 18
       |
208 | 188, 207 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
     |
209 | 203, 208 | syl6eq 2512 |
. . . . . . . . . . . . . . . 16
         |
210 | 209 | oveq2d 6336 |
. . . . . . . . . . . . . . 15
             |
211 | | 2t0e0 10799 |
. . . . . . . . . . . . . . 15
   |
212 | 210, 211 | syl6eq 2512 |
. . . . . . . . . . . . . 14
           |
213 | 202, 212 | oveq12d 6338 |
. . . . . . . . . . . . 13
            
        |
214 | | 0m0e0 10752 |
. . . . . . . . . . . . 13
   |
215 | 213, 214 | syl6eq 2512 |
. . . . . . . . . . . 12
            
      |
216 | 183, 215 | jca 539 |
. . . . . . . . . . 11
                                         |
217 | | oveq2 6328 |
. . . . . . . . . . . . . 14
                   |
218 | 217 | fveq2d 5896 |
. . . . . . . . . . . . 13
                           |
219 | 218 | fveq2d 5896 |
. . . . . . . . . . . 12
             
                     |
220 | | oveq1 6327 |
. . . . . . . . . . . . . 14
                   |
221 | 220 | fveq2d 5896 |
. . . . . . . . . . . . 13
                           |
222 | 220 | fveq2d 5896 |
. . . . . . . . . . . . . 14
                           |
223 | 222 | oveq2d 6336 |
. . . . . . . . . . . . 13
                               |
224 | 221, 223 | oveq12d 6338 |
. . . . . . . . . . . 12
                  
                                  |
225 | 219, 224 | jca 539 |
. . . . . . . . . . 11
                                                                                 |
226 | | nnuz 11228 |
. . . . . . . . . . . 12
     |
227 | 15, 226 | syl6eleq 2550 |
. . . . . . . . . . 11
                 |
228 | 10 | adantr 471 |
. . . . . . . . . . . . . . . 16
                   |
229 | | elfznn 11863 |
. . . . . . . . . . . . . . . . . 18
             |
230 | 229 | adantl 472 |
. . . . . . . . . . . . . . . . 17
                   |
231 | 230 | nnrpd 11373 |
. . . . . . . . . . . . . . . 16
                   |
232 | 228, 231 | rpdivcld 11392 |
. . . . . . . . . . . . . . 15
                     |
233 | 69 | ffvelrni 6049 |
. . . . . . . . . . . . . . 15
  
        |
234 | 232, 233 | syl 17 |
. . . . . . . . . . . . . 14
                         |
235 | 234 | recnd 9700 |
. . . . . . . . . . . . 13
                         |
236 | 235 | abscld 13553 |
. . . . . . . . . . . 12
                       
     |
237 | 236 | recnd 9700 |
. . . . . . . . . . 11
                       
     |
238 | 230 | nnred 10657 |
. . . . . . . . . . . . . . 15
                   |
239 | | 1red 9689 |
. . . . . . . . . . . . . . 15
                   |
240 | 238, 239 | resubcld 10080 |
. . . . . . . . . . . . . 14
                     |
241 | 78 | ffvelrni 6049 |
. . . . . . . . . . . . . 14
           |
242 | 240, 241 | syl 17 |
. . . . . . . . . . . . 13
                         |
243 | 22 | a1i 11 |
. . . . . . . . . . . . . 14
                   |
244 | 87 | ffvelrni 6049 |
. . . . . . . . . . . . . . 15
           |
245 | 240, 244 | syl 17 |
. . . . . . . . . . . . . 14
                         |
246 | 243, 245 | remulcld 9702 |
. . . . . . . . . . . . 13
                           |
247 | 242, 246 | resubcld 10080 |
. . . . . . . . . . . 12
                            
      |
248 | 247 | recnd 9700 |
. . . . . . . . . . 11
                            
      |
249 | 171, 180,
216, 225, 227, 237, 248 | fsumparts 13921 |
. . . . . . . . . 10
       ..^                                            
                                                                            ..^                            
                            |
250 | 147 | recnd 9700 |
. . . . . . . . . . . . . 14
              
      |
251 | 87 | ffvelrni 6049 |
. . . . . . . . . . . . . . . . 17
       |
252 | 145, 251 | syl 17 |
. . . . . . . . . . . . . . . 16
              
      |
253 | 148, 252 | remulcld 9702 |
. . . . . . . . . . . . . . 15
              
        |
254 | 253 | recnd 9700 |
. . . . . . . . . . . . . 14
              
        |
255 | | 1red 9689 |
. . . . . . . . . . . . . . . . 17
              
  |
256 | 145, 255 | resubcld 10080 |
. . . . . . . . . . . . . . . 16
              
    |
257 | 78 | ffvelrni 6049 |
. . . . . . . . . . . . . . . 16
           |
258 | 256, 257 | syl 17 |
. . . . . . . . . . . . . . 15
              
        |
259 | 258 | recnd 9700 |
. . . . . . . . . . . . . 14
              
        |
260 | 87 | ffvelrni 6049 |
. . . . . . . . . . . . . . . . 17
           |
261 | 256, 260 | syl 17 |
. . . . . . . . . . . . . . . 16
              
        |
262 | 148, 261 | remulcld 9702 |
. . . . . . . . . . . . . . 15
              
    
     |
263 | 262 | recnd 9700 |
. . . . . . . . . . . . . 14
              
    
     |
264 | 250, 254,
259, 263 | sub4d 10066 |
. . . . . . . . . . . . 13
              
                                                              |
265 | 124 | oveq2d 6336 |
. . . . . . . . . . . . . . 15
              
                  |
266 | 123, 265 | oveq12d 6338 |
. . . . . . . . . . . . . 14
              
                                  |
267 | 266 | oveq1d 6335 |
. . . . . . . . . . . . 13
              
                                                              
       |
268 | | 2cnd 10715 |
. . . . . . . . . . . . . . 15
              
  |
269 | 252 | recnd 9700 |
. . . . . . . . . . . . . . 15
              
      |
270 | 261 | recnd 9700 |
. . . . . . . . . . . . . . 15
              
        |
271 | 268, 269,
270 | subdid 10107 |
. . . . . . . . . . . . . 14
              
                         
      |
272 | 271 | oveq2d 6336 |
. . . . . . . . . . . . 13
              
                                                            |
273 | 264, 267,
272 | 3eqtr4d 2506 |
. . . . . . . . . . . 12
              
                                                                    |
274 | 273 | oveq2d 6336 |
. . . . . . . . . . 11
              
       
                                   
                          
                     |
275 | 99, 274 | sumeq12rdv 13828 |
. . . . . . . . . 10
       ..^                                            
             
                             
                     |
276 | 249, 275 | eqtr3d 2498 |
. . . . . . . . 9
                                                                    ..^                                                       
                             
                     |
277 | 157, 159 | fsumcl 13854 |
. . . . . . . . . 10
                                 
                       |
278 | 93, 277 | subnegd 10024 |
. . . . . . . . 9
                                                             
                                                                                                      |
279 | 162, 276,
278 | 3eqtr3rd 2505 |
. . . . . . . 8
                                                            
                      
                             
                     |
280 | 10 | relogcld 23628 |
. . . . . . . . . 10
           |
281 | 280 | recnd 9700 |
. . . . . . . . 9
           |
282 | 66, 281 | mulcomd 9695 |
. . . . . . . 8
                   |
283 | 279, 282 | oveq12d 6338 |
. . . . . . 7
                                                                                                                          
                            |
284 | 147, 258 | resubcld 10080 |
. . . . . . . . . . . 12
              
        
     |
285 | 252, 261 | resubcld 10080 |
. . . . . . . . . . . . 13
              
        
     |
286 | 148, 285 | remulcld 9702 |
. . . . . . . . . . . 12
              
                |
287 | 284, 286 | resubcld 10080 |
. . . . . . . . . . 11
              
                              |
288 | 108, 287 | remulcld 9702 |
. . . . . . . . . 10
              
       
                                  |
289 | 157, 288 | fsumrecl 13855 |
. . . . . . . . 9
                                   
                     |
290 | 289 | recnd 9700 |
. . . . . . . 8
                                   
                     |
291 | 2, 8 | rplogcld 23634 |
. . . . . . . . 9
           |
292 | 291 | rpne0d 11380 |
. . . . . . . 8
           |
293 | 10 | rpne0d 11380 |
. . . . . . . 8
       |
294 | 290, 281,
66, 292, 293 | divdiv1d 10447 |
. . . . . . 7
                                     
                                                        
                            |
295 | 283, 294 | eqtr4d 2499 |
. . . . . 6
                                                                                                                           
                           |
296 | 295 | oveq2d 6336 |
. . . . 5
                                                                                            
                                                                                                                                                     
                            |
297 | 71 | recnd 9700 |
. . . . . . . . . 10
           |
298 | 297 | abscld 13553 |
. . . . . . . . 9
               |
299 | 298, 280 | remulcld 9702 |
. . . . . . . 8
                     |
300 | 108, 284 | remulcld 9702 |
. . . . . . . . . 10
              
       
                  |
301 | 157, 300 | fsumrecl 13855 |
. . . . . . . . 9
                                         |
302 | 301, 291 | rerpdivcld 11403 |
. . . . . . . 8
                                               |
303 | 299, 302 | resubcld 10080 |
. . . . . . 7
                                                               |
304 | 303 | recnd 9700 |
. . . . . 6
                                                               |
305 | 290, 281,
292 | divcld 10416 |
. . . . . 6
                                    
                          |
306 | 304, 305,
66, 293 | divdird 10454 |
. . . . 5
                                                                                              
                                                                                                                     
                            |
307 | 299 | recnd 9700 |
. . . . . . . 8
                     |
308 | 302 | recnd 9700 |
. . . . . . . 8
                                               |
309 | 307, 308,
305 | subsubd 10045 |
. . . . . . 7
                                                                                            
                                                                                                                  
                           |
310 | | 2cnd 10715 |
. . . . . . . . . . . 12
       |
311 | 269, 270 | subcld 10017 |
. . . . . . . . . . . . 13
              
        
     |
312 | 109, 311 | mulcld 9694 |
. . . . . . . . . . . 12
              
       
                  |
313 | 157, 310,
312 | fsummulc2 13900 |
. . . . . . . . . . 11
                                         
                                     |
314 | 284 | recnd 9700 |
. . . . . . . . . . . . . . 15
              
        
     |
315 | 268, 311 | mulcld 9694 |
. . . . . . . . . . . . . . 15
              
                |
316 | 314, 315 | nncand 10022 |
. . . . . . . . . . . . . 14
              
                      
                                   |
317 | 316 | oveq2d 6336 |
. . . . . . . . . . . . 13
              
    |