Step | Hyp | Ref
| Expression |
1 | | pntlem1.r |
. . . . . . . . . 10
  ψ     |
2 | | pntlem1.a |
. . . . . . . . . 10
   |
3 | | pntlem1.b |
. . . . . . . . . 10
   |
4 | | pntlem1.l |
. . . . . . . . . 10
       |
5 | | pntlem1.d |
. . . . . . . . . 10
   |
6 | | pntlem1.f |
. . . . . . . . . 10
       ;          |
7 | | pntlem1.u |
. . . . . . . . . 10
   |
8 | | pntlem1.u2 |
. . . . . . . . . 10

  |
9 | | pntlem1.e |
. . . . . . . . . 10
   |
10 | | pntlem1.k |
. . . . . . . . . 10
       |
11 | | pntlem1.y |
. . . . . . . . . 10
 
   |
12 | | pntlem1.x |
. . . . . . . . . 10
     |
13 | | pntlem1.c |
. . . . . . . . . 10
   |
14 | | pntlem1.w |
. . . . . . . . . 10
                           ;                      |
15 | | pntlem1.z |
. . . . . . . . . 10
      |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | pntlemb 24514 |
. . . . . . . . 9
  
             
 
                                           ;             |
17 | 16 | simp1d 1042 |
. . . . . . . 8
   |
18 | 1 | pntrf 24480 |
. . . . . . . . 9
     |
19 | 18 | ffvelrni 6036 |
. . . . . . . 8

      |
20 | 17, 19 | syl 17 |
. . . . . . 7
       |
21 | 20, 17 | rerpdivcld 11392 |
. . . . . 6
         |
22 | 21 | recnd 9687 |
. . . . 5
         |
23 | 22 | abscld 13575 |
. . . 4
             |
24 | 17 | relogcld 23651 |
. . . 4
       |
25 | 23, 24 | remulcld 9689 |
. . 3
                   |
26 | 7 | rpred 11364 |
. . . . . 6
   |
27 | | 3re 10705 |
. . . . . . . 8
 |
28 | 27 | a1i 11 |
. . . . . . 7
   |
29 | 24, 28 | readdcld 9688 |
. . . . . 6
         |
30 | 26, 29 | remulcld 9689 |
. . . . 5
           |
31 | | 2re 10701 |
. . . . . . 7
 |
32 | 31 | a1i 11 |
. . . . . 6
   |
33 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pntlemc 24512 |
. . . . . . . . . . 11
  
    
     |
34 | 33 | simp3d 1044 |
. . . . . . . . . 10
           |
35 | 34 | simp3d 1044 |
. . . . . . . . 9
     |
36 | 35 | rpred 11364 |
. . . . . . . 8
     |
37 | 1, 2, 3, 4, 5, 6 | pntlemd 24511 |
. . . . . . . . . . . 12
     |
38 | 37 | simp1d 1042 |
. . . . . . . . . . 11
   |
39 | 33 | simp1d 1042 |
. . . . . . . . . . . 12
   |
40 | | 2z 10993 |
. . . . . . . . . . . 12
 |
41 | | rpexpcl 12329 |
. . . . . . . . . . . 12
         |
42 | 39, 40, 41 | sylancl 675 |
. . . . . . . . . . 11
       |
43 | 38, 42 | rpmulcld 11380 |
. . . . . . . . . 10
         |
44 | | 3nn0 10911 |
. . . . . . . . . . . . 13
 |
45 | | 2nn 10790 |
. . . . . . . . . . . . 13
 |
46 | 44, 45 | decnncl 11087 |
. . . . . . . . . . . 12
;  |
47 | | nnrp 11334 |
. . . . . . . . . . . 12
; ;   |
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . . 11
;  |
49 | | rpmulcl 11347 |
. . . . . . . . . . 11
 ;  ;    |
50 | 48, 3, 49 | sylancr 676 |
. . . . . . . . . 10
 ;    |
51 | 43, 50 | rpdivcld 11381 |
. . . . . . . . 9
        ;     |
52 | 51 | rpred 11364 |
. . . . . . . 8
        ;     |
53 | 36, 52 | remulcld 9689 |
. . . . . . 7
           ;      |
54 | 53, 24 | remulcld 9689 |
. . . . . 6
            ;           |
55 | 32, 54 | remulcld 9689 |
. . . . 5
             ;            |
56 | 30, 55 | resubcld 10068 |
. . . 4
                      ;             |
57 | 13 | rpred 11364 |
. . . 4
   |
58 | 56, 57 | readdcld 9688 |
. . 3
                       ;              |
59 | 7 | rpcnd 11366 |
. . . . . 6
   |
60 | 53 | recnd 9687 |
. . . . . 6
           ;      |
61 | 24 | recnd 9687 |
. . . . . 6
       |
62 | 59, 60, 61 | subdird 10096 |
. . . . 5
             ;                            ;            |
63 | 38 | rpcnd 11366 |
. . . . . . . . . . 11
   |
64 | 42 | rpcnd 11366 |
. . . . . . . . . . 11
       |
65 | 50 | rpcnne0d 11373 |
. . . . . . . . . . 11
  ;  ;     |
66 | | div23 10311 |
. . . . . . . . . . 11
       ;  ;           ;     ;          |
67 | 63, 64, 65, 66 | syl3anc 1292 |
. . . . . . . . . 10
        ;     ;          |
68 | 9 | oveq1i 6318 |
. . . . . . . . . . . 12
           |
69 | 37 | simp2d 1043 |
. . . . . . . . . . . . . 14
   |
70 | 69 | rpcnd 11366 |
. . . . . . . . . . . . 13
   |
71 | 69 | rpne0d 11369 |
. . . . . . . . . . . . 13
   |
72 | 59, 70, 71 | sqdivd 12467 |
. . . . . . . . . . . 12
                   |
73 | 68, 72 | syl5eq 2517 |
. . . . . . . . . . 11
                 |
74 | 73 | oveq2d 6324 |
. . . . . . . . . 10
   ;          ;                |
75 | 38, 50 | rpdivcld 11381 |
. . . . . . . . . . . 12
  ;     |
76 | 75 | rpcnd 11366 |
. . . . . . . . . . 11
  ;     |
77 | 59 | sqcld 12452 |
. . . . . . . . . . 11
       |
78 | | rpexpcl 12329 |
. . . . . . . . . . . . 13
         |
79 | 69, 40, 78 | sylancl 675 |
. . . . . . . . . . . 12
       |
80 | 79 | rpcnne0d 11373 |
. . . . . . . . . . 11
             |
81 | | divass 10310 |
. . . . . . . . . . . 12
   ;                     ;               ;                |
82 | | div23 10311 |
. . . . . . . . . . . 12
   ;                     ;                ;               |
83 | 81, 82 | eqtr3d 2507 |
. . . . . . . . . . 11
   ;                    ;                 ;               |
84 | 76, 77, 80, 83 | syl3anc 1292 |
. . . . . . . . . 10
   ;                 ;               |
85 | 67, 74, 84 | 3eqtrd 2509 |
. . . . . . . . 9
        ;      ;               |
86 | 85 | oveq2d 6324 |
. . . . . . . 8
           ;          ;                |
87 | | df-3 10691 |
. . . . . . . . . . . . 13
   |
88 | 87 | oveq2i 6319 |
. . . . . . . . . . . 12
           |
89 | | 2nn0 10910 |
. . . . . . . . . . . . 13
 |
90 | | expp1 12317 |
. . . . . . . . . . . . 13
 
               |
91 | 59, 89, 90 | sylancl 675 |
. . . . . . . . . . . 12
               |
92 | 88, 91 | syl5eq 2517 |
. . . . . . . . . . 11
             |
93 | 77, 59 | mulcomd 9682 |
. . . . . . . . . . 11
               |
94 | 92, 93 | eqtrd 2505 |
. . . . . . . . . 10
             |
95 | 94 | oveq2d 6324 |
. . . . . . . . 9
        
        |
96 | 37 | simp3d 1044 |
. . . . . . . . . . 11
   |
97 | 96 | rpcnd 11366 |
. . . . . . . . . 10
   |
98 | 97, 59, 77 | mulassd 9684 |
. . . . . . . . 9
          
        |
99 | | 1cnd 9677 |
. . . . . . . . . . . . . . 15
   |
100 | 69 | rpreccld 11374 |
. . . . . . . . . . . . . . . 16
     |
101 | 100 | rpcnd 11366 |
. . . . . . . . . . . . . . 15
     |
102 | 99, 101, 59 | subdird 10096 |
. . . . . . . . . . . . . 14
                 |
103 | 59 | mulid2d 9679 |
. . . . . . . . . . . . . . 15
     |
104 | 59, 70, 71 | divrec2d 10409 |
. . . . . . . . . . . . . . . 16
         |
105 | 9, 104 | syl5req 2518 |
. . . . . . . . . . . . . . 15
       |
106 | 103, 105 | oveq12d 6326 |
. . . . . . . . . . . . . 14
             |
107 | 102, 106 | eqtr2d 2506 |
. . . . . . . . . . . . 13
           |
108 | 107 | oveq1d 6323 |
. . . . . . . . . . . 12
      ;                  ;           |
109 | 6 | oveq1i 6318 |
. . . . . . . . . . . . 13
          ;           |
110 | 99, 101 | subcld 10005 |
. . . . . . . . . . . . . 14
       |
111 | 75, 79 | rpdivcld 11381 |
. . . . . . . . . . . . . . 15
   ;          |
112 | 111 | rpcnd 11366 |
. . . . . . . . . . . . . 14
   ;          |
113 | 110, 112,
59 | mul32d 9861 |
. . . . . . . . . . . . 13
         ;                   ;           |
114 | 109, 113 | syl5eq 2517 |
. . . . . . . . . . . 12
            ;           |
115 | 108, 114 | eqtr4d 2508 |
. . . . . . . . . . 11
      ;             |
116 | 115 | oveq1d 6323 |
. . . . . . . . . 10
       ;                        |
117 | 35 | rpcnd 11366 |
. . . . . . . . . . 11
     |
118 | 117, 112,
77 | mulassd 9684 |
. . . . . . . . . 10
       ;                    ;                |
119 | 116, 118 | eqtr3d 2507 |
. . . . . . . . 9
               ;                |
120 | 95, 98, 119 | 3eqtr2d 2511 |
. . . . . . . 8
             ;                |
121 | 86, 120 | eqtr4d 2508 |
. . . . . . 7
           ;            |
122 | 121 | oveq2d 6324 |
. . . . . 6
            ;      
        |
123 | 122 | oveq1d 6323 |
. . . . 5
             ;            
             |
124 | 62, 123 | eqtr3d 2507 |
. . . 4
                   ;            
             |
125 | 26, 24 | remulcld 9689 |
. . . . 5
         |
126 | 125, 54 | resubcld 10068 |
. . . 4
                   ;            |
127 | 124, 126 | eqeltrrd 2550 |
. . 3
   
             |
128 | 17 | rpred 11364 |
. . . . . . . 8
   |
129 | 16 | simp2d 1043 |
. . . . . . . . 9
 
             |
130 | 129 | simp1d 1042 |
. . . . . . . 8
   |
131 | 128, 130 | rplogcld 23657 |
. . . . . . 7
       |
132 | 32, 131 | rerpdivcld 11392 |
. . . . . 6
         |
133 | | fzfid 12224 |
. . . . . . 7
             |
134 | 17 | adantr 472 |
. . . . . . . . . . . . 13
 
          
  |
135 | | elfznn 11854 |
. . . . . . . . . . . . . . 15
          
  |
136 | 135 | adantl 473 |
. . . . . . . . . . . . . 14
 
          
  |
137 | 136 | nnrpd 11362 |
. . . . . . . . . . . . 13
 
          
  |
138 | 134, 137 | rpdivcld 11381 |
. . . . . . . . . . . 12
 
          
    |
139 | 18 | ffvelrni 6036 |
. . . . . . . . . . . 12
  
        |
140 | 138, 139 | syl 17 |
. . . . . . . . . . 11
 
          
        |
141 | 140, 134 | rerpdivcld 11392 |
. . . . . . . . . 10
 
          
          |
142 | 141 | recnd 9687 |
. . . . . . . . 9
 
          
          |
143 | 142 | abscld 13575 |
. . . . . . . 8
 
          
       
      |
144 | 137 | relogcld 23651 |
. . . . . . . 8
 
          
      |
145 | 143, 144 | remulcld 9689 |
. . . . . . 7
 
          
                    |
146 | 133, 145 | fsumrecl 13877 |
. . . . . 6
 
      
                        |
147 | 132, 146 | remulcld 9689 |
. . . . 5
                            
            |
148 | 147, 57 | readdcld 9688 |
. . . 4
                             
             |
149 | 20 | recnd 9687 |
. . . . . . . . . . 11
       |
150 | 149 | abscld 13575 |
. . . . . . . . . 10
           |
151 | 150 | recnd 9687 |
. . . . . . . . 9
           |
152 | 151, 61 | mulcld 9681 |
. . . . . . . 8
                 |
153 | 132 | recnd 9687 |
. . . . . . . . 9
         |
154 | 140 | recnd 9687 |
. . . . . . . . . . . . 13
 
          
        |
155 | 154 | abscld 13575 |
. . . . . . . . . . . 12
 
          
            |
156 | 155, 144 | remulcld 9689 |
. . . . . . . . . . 11
 
          
       
          |
157 | 133, 156 | fsumrecl 13877 |
. . . . . . . . . 10
 
      
                      |
158 | 157 | recnd 9687 |
. . . . . . . . 9
 
      
                      |
159 | 153, 158 | mulcld 9681 |
. . . . . . . 8
                                       |
160 | 17 | rpcnd 11366 |
. . . . . . . 8
   |
161 | 17 | rpne0d 11369 |
. . . . . . . 8
   |
162 | 152, 159,
160, 161 | divsubdird 10444 |
. . . . . . 7
                                                                                                                 |
163 | 151, 61, 160, 161 | div23d 10442 |
. . . . . . . . 9
                                   |
164 | 149, 160,
161 | absdivd 13594 |
. . . . . . . . . . 11
                           |
165 | 17 | rprege0d 11371 |
. . . . . . . . . . . . 13
 
   |
166 | | absid 13436 |
. . . . . . . . . . . . 13
         |
167 | 165, 166 | syl 17 |
. . . . . . . . . . . 12
       |
168 | 167 | oveq2d 6324 |
. . . . . . . . . . 11
                           |
169 | 164, 168 | eqtrd 2505 |
. . . . . . . . . 10
                       |
170 | 169 | oveq1d 6323 |
. . . . . . . . 9
                                   |
171 | 163, 170 | eqtr4d 2508 |
. . . . . . . 8
                                   |
172 | 153, 158,
160, 161 | divassd 10440 |
. . . . . . . . 9
                                                      
                        |
173 | 160 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
          
  |
174 | 161 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
          
  |
175 | 154, 173,
174 | absdivd 13594 |
. . . . . . . . . . . . . . 15
 
          
       
                      |
176 | 167 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
          
      |
177 | 176 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
 
          
       
                      |
178 | 175, 177 | eqtrd 2505 |
. . . . . . . . . . . . . 14
 
          
       
                  |
179 | 178 | oveq1d 6323 |
. . . . . . . . . . . . 13
 
          
                                      |
180 | 155 | recnd 9687 |
. . . . . . . . . . . . . 14
 
          
            |
181 | 144 | recnd 9687 |
. . . . . . . . . . . . . 14
 
          
      |
182 | 17 | rpcnne0d 11373 |
. . . . . . . . . . . . . . 15
     |
183 | 182 | adantr 472 |
. . . . . . . . . . . . . 14
 
          
    |
184 | | div23 10311 |
. . . . . . . . . . . . . 14
                                                         |
185 | 180, 181,
183, 184 | syl3anc 1292 |
. . . . . . . . . . . . 13
 
          
                                      |
186 | 179, 185 | eqtr4d 2508 |
. . . . . . . . . . . 12
 
          
                                      |
187 | 186 | sumeq2dv 13846 |
. . . . . . . . . . 11
 
      
                                                      |
188 | 156 | recnd 9687 |
. . . . . . . . . . . 12
 
          
       
          |
189 | 133, 160,
188, 161 | fsumdivc 13924 |
. . . . . . . . . . 11
                                                               |
190 | 187, 189 | eqtr4d 2508 |
. . . . . . . . . 10
 
      
                       
      
                       |
191 | 190 | oveq2d 6324 |
. . . . . . . . 9
                            
                                                  |
192 | 172, 191 | eqtr4d 2508 |
. . . . . . . 8
                                                                  
            |
193 | 171, 192 | oveq12d 6326 |
. . . . . . 7
                                                                                                     
             |
194 | 162, 193 | eqtrd 2505 |
. . . . . 6
                                                                                                   
             |
195 | | 1re 9660 |
. . . . . . . . 9
 |
196 | | rexr 9704 |
. . . . . . . . 9
   |
197 | | elioopnf 11753 |
. . . . . . . . 9

   
     |
198 | 195, 196,
197 | mp2b 10 |
. . . . . . . 8
   
    |
199 | 128, 130,
198 | sylanbrc 677 |
. . . . . . 7
      |
200 | | pntlem1.C |
. . . . . . 7
                                                              |
201 | | fveq2 5879 |
. . . . . . . . . . . . 13
           |
202 | 201 | fveq2d 5883 |
. . . . . . . . . . . 12
                   |
203 | | fveq2 5879 |
. . . . . . . . . . . 12
           |
204 | 202, 203 | oveq12d 6326 |
. . . . . . . . . . 11
                               |
205 | 203 | oveq2d 6324 |
. . . . . . . . . . . 12
               |
206 | | oveq2 6316 |
. . . . . . . . . . . . . . . . 17
       |
207 | 206 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
               |
208 | 207 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
                       |
209 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
210 | 208, 209 | oveq12d 6326 |
. . . . . . . . . . . . . 14
                                   |
211 | 210 | cbvsumv 13839 |
. . . . . . . . . . . . 13
                            
                            |
212 | | oveq1 6315 |
. . . . . . . . . . . . . . . 16
       |
213 | 212 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
               |
214 | 213 | oveq2d 6324 |
. . . . . . . . . . . . . 14
                       |
215 | | simpl 464 |
. . . . . . . . . . . . . . . . . 18
 
      
      |
216 | 215 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
 
      
          |
217 | 216 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
 
      
                  |
218 | 217 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
 
      
                          |
219 | 218 | oveq1d 6323 |
. . . . . . . . . . . . . 14
 
      
                                      |
220 | 214, 219 | sumeq12rdv 13850 |
. . . . . . . . . . . . 13
                                                           |
221 | 211, 220 | syl5eq 2517 |
. . . . . . . . . . . 12
                             
      
                      |
222 | 205, 221 | oveq12d 6326 |
. . . . . . . . . . 11
                                                                           |
223 | 204, 222 | oveq12d 6326 |
. . . . . . . . . 10
                       
                                                                                   |
224 | | id 22 |
. . . . . . . . . 10
   |
225 | 223, 224 | oveq12d 6326 |
. . . . . . . . 9
                        
                                                                                      |
226 | 225 | breq1d 4405 |
. . . . . . . 8
                                                       
                                                         |
227 | 226 | rspcv 3132 |
. . . . . . 7
   
 
                           
                                                                                       |
228 | 199, 200,
227 | sylc 61 |
. . . . . 6
                                                         |
229 | 194, 228 | eqbrtrrd 4418 |
. . . . 5
                                             
             |
230 | 25, 147, 57 | lesubadd2d 10233 |
. . . . 5
                                                         
                                            
              |
231 | 229, 230 | mpbid 215 |
. . . 4
                                             
             |
232 | | 2cnd 10704 |
. . . . . . 7
   |
233 | 143 | recnd 9687 |
. . . . . . . . 9
 
          
       
      |
234 | 233, 181 | mulcld 9681 |
. . . . . . . 8
 
          
                    |
235 | 133, 234 | fsumcl 13876 |
. . . . . . 7
 
      
                        |
236 | 131 | rpne0d 11369 |
. . . . . . 7
       |
237 | 232, 235,
61, 236 | div23d 10442 |
. . . . . 6
   
      
                                                                    |
238 | 24 | resqcld 12480 |
. . . . . . . . . . . 12
           |
239 | 52, 238 | remulcld 9689 |
. . . . . . . . . . 11
         ;              |
240 | 36, 239 | remulcld 9689 |
. . . . . . . . . 10
            ;               |
241 | | remulcl 9642 |
. . . . . . . . . 10
             ;                          ;                |
242 | 31, 240, 241 | sylancr 676 |
. . . . . . . . 9
             ;                |
243 | 30, 24 | remulcld 9689 |
. . . . . . . . 9
                 |
244 | | remulcl 9642 |
. . . . . . . . . 10
         
                        
      
                         |
245 | 31, 146, 244 | sylancr 676 |
. . . . . . . . 9
                      
            |
246 | 26 | adantr 472 |
. . . . . . . . . . . . . . 15
 
          
  |
247 | 246, 136 | nndivred 10680 |
. . . . . . . . . . . . . 14
 
          
    |
248 | 247, 143 | resubcld 10068 |
. . . . . . . . . . . . 13
 
          
                  |
249 | 248, 144 | remulcld 9689 |
. . . . . . . . . . . 12
 
          
           
            |
250 | 133, 249 | fsumrecl 13877 |
. . . . . . . . . . 11
 
      
                            |
251 | 32, 250 | remulcld 9689 |
. . . . . . . . . 10
                                       |
252 | 243, 245 | resubcld 10068 |
. . . . . . . . . 10
                 
      
                          |
253 | | pntlem1.m |
. . . . . . . . . . . 12
                 |
254 | | pntlem1.n |
. . . . . . . . . . . 12
                 |
255 | | pntlem1.U |
. . . . . . . . . . . 12
               
  |
256 | | pntlem1.K |
. . . . . . . . . . . 12
      
       
      ![[,] [,]](_icc.gif)                      |
257 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 253, 254, 255, 256 | pntlemf 24522 |
. . . . . . . . . . 11
            ;                                                 |
258 | | 2pos 10723 |
. . . . . . . . . . . . 13
 |
259 | 258 | a1i 11 |
. . . . . . . . . . . 12
   |
260 | | lemul2 10480 |
. . . . . . . . . . . 12
             ;             
      
                            
            ;                                              
            ;                                                     |
261 | 240, 250,
32, 259, 260 | syl112anc 1296 |
. . . . . . . . . . 11
             ;                                              
            ;                                                     |
262 | 257, 261 | mpbid 215 |
. . . . . . . . . 10
             ;                                                    |
263 | 247 | recnd 9687 |
. . . . . . . . . . . . . . . 16
 
          
    |
264 | 263, 233,
181 | subdird 10096 |
. . . . . . . . . . . . . . 15
 
          
           
                           
            |
265 | 264 | sumeq2dv 13846 |
. . . . . . . . . . . . . 14
 
      
                                                                    |
266 | 247, 144 | remulcld 9689 |
. . . . . . . . . . . . . . . 16
 
          
          |
267 | 266 | recnd 9687 |
. . . . . . . . . . . . . . 15
 
          
          |
268 | 133, 267,
234 | fsumsub 13926 |
. . . . . . . . . . . . . 14
 
      
                     
                                                   
            |
269 | 265, 268 | eqtrd 2505 |
. . . . . . . . . . . . 13
 
      
                           
      
                   
                         |
270 | 269 | oveq2d 6324 |
. . . . . . . . . . . 12
                                                                                             |
271 | 133, 266 | fsumrecl 13877 |
. . . . . . . . . . . . . 14
 
      
              |
272 | 271 | recnd 9687 |
. . . . . . . . . . . . 13
 
      
              |
273 | 232, 272,
235 | subdid 10095 |
. . . . . . . . . . . 12
          
                   
                                                                                  |
274 | 270, 273 | eqtrd 2505 |
. . . . . . . . . . 11
                                                                                               |
275 | | remulcl 9642 |
. . . . . . . . . . . . 13
         
                                     |
276 | 31, 271, 275 | sylancr 676 |
. . . . . . . . . . . 12
                         |
277 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 253, 254, 255, 256 | pntlemk 24523 |
. . . . . . . . . . . 12
                                       |
278 | 276, 243,
245, 277 | lesub1dd 10250 |
. . . . . . . . . . 11
   
      
              
      
                                                                          |
279 | 274, 278 | eqbrtrd 4416 |
. . . . . . . . . 10
                                                                                       |
280 | 242, 251,
252, 262, 279 | letrd 9809 |
. . . . . . . . 9
             ;                              
      
                          |
281 | 242, 243,
245, 280 | lesubd 10238 |
. . . . . . . 8
                      
         
                           ;                 |
282 | 30 | recnd 9687 |
. . . . . . . . . 10
           |
283 | 55 | recnd 9687 |
. . . . . . . . . 10
             ;            |
284 | 282, 283,
61 | subdird 10096 |
. . . . . . . . 9
                       ;                                            ;                  |
285 | 54 | recnd 9687 |
. . . . . . . . . . . 12
            ;           |
286 | 232, 285,
61 | mulassd 9684 |
. . . . . . . . . . 11
              ;                            ;                 |
287 | 60, 61, 61 | mulassd 9684 |
. . . . . . . . . . . . 13
             ;                         ;                 |
288 | 61 | sqvald 12451 |
. . . . . . . . . . . . . 14
                     |
289 | 288 | oveq2d 6324 |
. . . . . . . . . . . . 13
            ;                        ;                 |
290 | 51 | rpcnd 11366 |
. . . . . . . . . . . . . 14
        ;     |
291 | 238 | recnd 9687 |
. . . . . . . . . . . . . 14
           |
292 | 117, 290,
291 | mulassd 9684 |
. . . . . . . . . . . . 13
            ;                        ;               |
293 | 287, 289,
292 | 3eqtr2d 2511 |
. . . . . . . . . . . 12
             ;                         ;               |
294 | 293 | oveq2d 6324 |
. . . . . . . . . . 11
              ;                           ;                |
295 | 286, 294 | eqtrd 2505 |
. . . . . . . . . 10
              ;                           ;                |
296 | 295 | oveq2d 6324 |
. . . . . . . . 9
                             ;                                           ;                 |
297 | 284, 296 | eqtrd 2505 |
. . . . . . . 8
                       ;                                           ;                 |
298 | 281, 297 | breqtrrd 4422 |
. . . . . . 7
                      
         
                      ;                  |
299 | 245, 56, 131 | ledivmul2d 11415 |
. . . . . . 7
                                                             ;                                
         
                      ;                   |
300 | 298, 299 | mpbird 240 |
. . . . . 6
   
      
                                                 ;             |
301 | 237, 300 | eqbrtrrd 4418 |
. . . . 5
                            
         
 
                   ;             |
302 | 147, 56, 57, 301 | leadd1dd 10248 |
. . . 4
                             
                                 ;              |
303 | 25, 148, 58, 231, 302 | letrd 9809 |
. . 3
                                       ;              |
304 | | remulcl 9642 |
. . . . . . . . 9
 
     |
305 | 26, 27, 304 | sylancl 675 |
. . . . . . . 8
     |
306 | 305, 57 | readdcld 9688 |
. . . . . . 7
       |
307 | 16 | simp3d 1044 |
. . . . . . . 8
                                     
           ;            |
308 | 307 | simp3d 1044 |
. . . . . . 7
    
           ;           |
309 | 306, 54, 125, 308 | leadd2dd 10249 |
. . . . . 6
                               ;            |
310 | 28 | recnd 9687 |
. . . . . . . . 9
   |
311 | 59, 61, 310 | adddid 9685 |
. . . . . . . 8
                     |
312 | 311 | oveq1d 6323 |
. . . . . . 7
                         |
313 | 125 | recnd 9687 |
. . . . . . . 8
         |
314 | 59, 310 | mulcld 9681 |
. . . . . . . 8
     |
315 | 13 | rpcnd 11366 |
. . . . . . . 8
   |
316 | 313, 314,
315 | addassd 9683 |
. . . . . . 7
                           |
317 | 312, 316 | eqtrd 2505 |
. . . . . 6
                         |
318 | 285 | 2timesd 10878 |
. . . . . . . 8
             ;                      ;                    ;            |
319 | 318 | oveq2d 6324 |
. . . . . . 7
                    ;                      ;                              ;                      ;                    ;             |
320 | 313, 285,
285 | nppcan3d 10032 |
. . . . . . 7
                    ;                      ;                    ;                             ;            |
321 | 319, 320 | eqtrd 2505 |
. . . . . 6
                    ;                      ;                             ;            |
322 | 309, 317,
321 | 3brtr4d 4426 |
. . . . 5
                              ;                  |