Proof of Theorem stoweidlem26
Step | Hyp | Ref
| Expression |
1 | | 1re 9668 |
. . . . . . . 8
 |
2 | | eleq1 2528 |
. . . . . . . 8
 
   |
3 | 1, 2 | mpbiri 241 |
. . . . . . 7
   |
4 | 3 | adantl 472 |
. . . . . 6
 
   |
5 | | 4re 10714 |
. . . . . . . 8
 |
6 | 5 | a1i 11 |
. . . . . . 7
 
   |
7 | | 3re 10711 |
. . . . . . . 8
 |
8 | 7 | a1i 11 |
. . . . . . 7
 
   |
9 | | 3ne0 10732 |
. . . . . . . 8
 |
10 | 9 | a1i 11 |
. . . . . . 7
 
   |
11 | 6, 8, 10 | redivcld 10463 |
. . . . . 6
 
     |
12 | 4, 11 | resubcld 10075 |
. . . . 5
 
 
     |
13 | | stoweidlem26.11 |
. . . . . . 7
   |
14 | 13 | rpred 11370 |
. . . . . 6
   |
15 | 14 | adantr 471 |
. . . . 5
 
   |
16 | 12, 15 | remulcld 9697 |
. . . 4
 
         |
17 | | 0red 9670 |
. . . 4
 
   |
18 | | fzfid 12218 |
. . . . . 6
       |
19 | 14 | adantr 471 |
. . . . . . 7
 
       |
20 | | stoweidlem26.13 |
. . . . . . . 8
 
               |
21 | | stoweidlem26.9 |
. . . . . . . . . . . . . 14
         
     |
22 | | eldif 3426 |
. . . . . . . . . . . . . 14
         
  
    
   
     |
23 | 21, 22 | sylib 201 |
. . . . . . . . . . . . 13
         
     |
24 | 23 | simpld 465 |
. . . . . . . . . . . 12
       |
25 | | 1e0p1 11108 |
. . . . . . . . . . . . . . . 16
   |
26 | 25 | oveq1i 6325 |
. . . . . . . . . . . . . . 15
           |
27 | | 0z 10977 |
. . . . . . . . . . . . . . . 16
 |
28 | | fzp1ss 11876 |
. . . . . . . . . . . . . . . 16
             |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . . . . 15
           |
30 | 26, 29 | eqsstri 3474 |
. . . . . . . . . . . . . 14
         |
31 | | stoweidlem26.8 |
. . . . . . . . . . . . . 14
       |
32 | 30, 31 | sseldi 3442 |
. . . . . . . . . . . . 13
       |
33 | | stoweidlem26.7 |
. . . . . . . . . . . . . 14
   |
34 | | rabexg 4567 |
. . . . . . . . . . . . . 14
               |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . 13
               |
36 | | oveq1 6322 |
. . . . . . . . . . . . . . . . 17
           |
37 | 36 | oveq1d 6330 |
. . . . . . . . . . . . . . . 16
               |
38 | 37 | breq2d 4428 |
. . . . . . . . . . . . . . 15
     
     
             |
39 | 38 | rabbidv 3048 |
. . . . . . . . . . . . . 14
                           |
40 | | stoweidlem26.4 |
. . . . . . . . . . . . . 14
                   |
41 | 39, 40 | fvmptg 5969 |
. . . . . . . . . . . . 13
          
 
                        |
42 | 32, 35, 41 | syl2anc 671 |
. . . . . . . . . . . 12
                   |
43 | 24, 42 | eleqtrd 2542 |
. . . . . . . . . . 11
               |
44 | | nfcv 2603 |
. . . . . . . . . . . 12
   |
45 | | nfcv 2603 |
. . . . . . . . . . . 12
   |
46 | | stoweidlem26.1 |
. . . . . . . . . . . . . 14
   |
47 | 46, 44 | nffv 5895 |
. . . . . . . . . . . . 13
       |
48 | | nfcv 2603 |
. . . . . . . . . . . . 13
  |
49 | | nfcv 2603 |
. . . . . . . . . . . . 13
         |
50 | 47, 48, 49 | nfbr 4461 |
. . . . . . . . . . . 12
     
 
     |
51 | | fveq2 5888 |
. . . . . . . . . . . . 13
           |
52 | 51 | breq1d 4426 |
. . . . . . . . . . . 12
     
 
   
             |
53 | 44, 45, 50, 52 | elrabf 3206 |
. . . . . . . . . . 11
            

             |
54 | 43, 53 | sylib 201 |
. . . . . . . . . 10
     
 
       |
55 | 54 | simpld 465 |
. . . . . . . . 9
   |
56 | 55 | adantr 471 |
. . . . . . . 8
 
       |
57 | 20, 56 | ffvelrnd 6046 |
. . . . . . 7
 
               |
58 | 19, 57 | remulcld 9697 |
. . . . . 6
 
     
           |
59 | 18, 58 | fsumrecl 13849 |
. . . . 5
                   |
60 | 59 | adantr 471 |
. . . 4
 
                   |
61 | 5, 7, 9 | redivcli 10402 |
. . . . . . 7
   |
62 | 61 | a1i 11 |
. . . . . 6
 
     |
63 | 4, 62 | resubcld 10075 |
. . . . 5
 
 
     |
64 | 4 | recnd 9695 |
. . . . . . . 8
 
   |
65 | 64 | subid1d 10001 |
. . . . . . 7
 
 
   |
66 | | 3cn 10712 |
. . . . . . . . . 10
 |
67 | 66, 9 | dividi 10368 |
. . . . . . . . 9
   |
68 | | 3lt4 10808 |
. . . . . . . . . 10
 |
69 | | 3pos 10731 |
. . . . . . . . . . 11
 |
70 | 7, 5, 7, 69 | ltdiv1ii 10564 |
. . . . . . . . . 10

      |
71 | 68, 70 | mpbi 213 |
. . . . . . . . 9
     |
72 | 67, 71 | eqbrtrri 4438 |
. . . . . . . 8
   |
73 | | breq1 4419 |
. . . . . . . . 9
   
     |
74 | 73 | adantl 472 |
. . . . . . . 8
 
   
     |
75 | 72, 74 | mpbiri 241 |
. . . . . . 7
 
     |
76 | 65, 75 | eqbrtrd 4437 |
. . . . . 6
 
 
     |
77 | 4, 17, 62, 76 | ltsub23d 10246 |
. . . . 5
 
 
     |
78 | 13 | rpgt0d 11373 |
. . . . . 6
   |
79 | 78 | adantr 471 |
. . . . 5
 
   |
80 | | mulltgt0 37383 |
. . . . 5
                    
  |
81 | 63, 77, 15, 79, 80 | syl22anc 1277 |
. . . 4
 
         |
82 | | 0cn 9661 |
. . . . . . . 8
 |
83 | | fsumconst 13900 |
. . . . . . . 8
     
                   |
84 | 18, 82, 83 | sylancl 673 |
. . . . . . 7
                   |
85 | | hashcl 12570 |
. . . . . . . . 9
               |
86 | | nn0cn 10908 |
. . . . . . . . 9
                   |
87 | 18, 85, 86 | 3syl 18 |
. . . . . . . 8
           |
88 | 87 | mul01d 9858 |
. . . . . . 7
             |
89 | 84, 88 | eqtrd 2496 |
. . . . . 6
         |
90 | 89 | adantr 471 |
. . . . 5
 
         |
91 | | 0red 9670 |
. . . . . . 7
 
       |
92 | 13 | rpge0d 11374 |
. . . . . . . . 9

  |
93 | 92 | adantr 471 |
. . . . . . . 8
 
       |
94 | | stoweidlem26.3 |
. . . . . . . . . . . 12
   |
95 | | nfv 1772 |
. . . . . . . . . . . 12
      |
96 | 94, 95 | nfan 2022 |
. . . . . . . . . . 11
         |
97 | | nfv 1772 |
. . . . . . . . . . 11
 
         |
98 | 96, 97 | nfim 2014 |
. . . . . . . . . 10
   
               |
99 | | fveq2 5888 |
. . . . . . . . . . . 12
                   |
100 | 99 | breq2d 4428 |
. . . . . . . . . . 11
 
       
           |
101 | 100 | imbi2d 322 |
. . . . . . . . . 10
   
                                 |
102 | | stoweidlem26.14 |
. . . . . . . . . . . 12
 
   
           |
103 | 102 | 3expia 1217 |
. . . . . . . . . . 11
 
     
           |
104 | 103 | com12 32 |
. . . . . . . . . 10
  
                |
105 | 44, 98, 101, 104 | vtoclgaf 3124 |
. . . . . . . . 9
  
                |
106 | 56, 105 | mpcom 37 |
. . . . . . . 8
 
               |
107 | 19, 57, 93, 106 | mulge0d 10218 |
. . . . . . 7
 
                 |
108 | 18, 91, 58, 107 | fsumle 13908 |
. . . . . 6
      
                  |
109 | 108 | adantr 471 |
. . . . 5
 
                         |
110 | 90, 109 | eqbrtrrd 4439 |
. . . 4
 
                   |
111 | 16, 17, 60, 81, 110 | ltletrd 9821 |
. . 3
 
                         |
112 | | elfzelz 11829 |
. . . . . . . . 9
       |
113 | | zre 10970 |
. . . . . . . . 9
   |
114 | 31, 112, 113 | 3syl 18 |
. . . . . . . 8
   |
115 | 5 | a1i 11 |
. . . . . . . . 9
   |
116 | 7 | a1i 11 |
. . . . . . . . 9
   |
117 | 9 | a1i 11 |
. . . . . . . . 9
   |
118 | 115, 116,
117 | redivcld 10463 |
. . . . . . . 8
     |
119 | 114, 118 | resubcld 10075 |
. . . . . . 7
       |
120 | 119, 14 | remulcld 9697 |
. . . . . 6
         |
121 | 120 | adantr 471 |
. . . . 5
 
         |
122 | 1 | a1i 11 |
. . . . . . . . 9
   |
123 | | stoweidlem26.6 |
. . . . . . . . . 10
   |
124 | 14, 123 | nndivred 10686 |
. . . . . . . . 9
     |
125 | 122, 124 | resubcld 10075 |
. . . . . . . 8
       |
126 | 114, 122 | resubcld 10075 |
. . . . . . . 8
     |
127 | 125, 126 | remulcld 9697 |
. . . . . . 7
      
    |
128 | 14, 127 | remulcld 9697 |
. . . . . 6
             |
129 | 128 | adantr 471 |
. . . . 5
 
             |
130 | | fzfid 12218 |
. . . . . . . 8
    
    |
131 | 31, 112 | syl 17 |
. . . . . . . . . . . . . 14
   |
132 | | 2z 10998 |
. . . . . . . . . . . . . . 15
 |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . 14
   |
134 | 131, 133 | zsubcld 11074 |
. . . . . . . . . . . . 13
     |
135 | 123 | nnzd 11068 |
. . . . . . . . . . . . 13
   |
136 | 131 | zred 11069 |
. . . . . . . . . . . . . . 15
   |
137 | | 2re 10707 |
. . . . . . . . . . . . . . . 16
 |
138 | 137 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
139 | 136, 138 | resubcld 10075 |
. . . . . . . . . . . . . 14
     |
140 | 123 | nnred 10652 |
. . . . . . . . . . . . . 14
   |
141 | | 0le2 10728 |
. . . . . . . . . . . . . . . 16
 |
142 | | 0red 9670 |
. . . . . . . . . . . . . . . . 17
   |
143 | 142, 138,
136 | lesub2d 10249 |
. . . . . . . . . . . . . . . 16
         |
144 | 141, 143 | mpbii 216 |
. . . . . . . . . . . . . . 15
  
    |
145 | 131 | zcnd 11070 |
. . . . . . . . . . . . . . . 16
   |
146 | 145 | subid1d 10001 |
. . . . . . . . . . . . . . 15
     |
147 | 144, 146 | breqtrd 4441 |
. . . . . . . . . . . . . 14
  
  |
148 | | elfzle2 11832 |
. . . . . . . . . . . . . . 15
       |
149 | 31, 148 | syl 17 |
. . . . . . . . . . . . . 14

  |
150 | 139, 136,
140, 147, 149 | letrd 9818 |
. . . . . . . . . . . . 13
  
  |
151 | 134, 135,
150 | 3jca 1194 |
. . . . . . . . . . . 12
    

   |
152 | | eluz2 11194 |
. . . . . . . . . . . 12
    
          |
153 | 151, 152 | sylibr 217 |
. . . . . . . . . . 11
    
    |
154 | | fzss2 11867 |
. . . . . . . . . . 11
    
 
            |
155 | 153, 154 | syl 17 |
. . . . . . . . . 10
    
 
      |
156 | 155 | sselda 3444 |
. . . . . . . . 9
 
   
         |
157 | 156, 57 | syldan 477 |
. . . . . . . 8
 
   
             |
158 | 130, 157 | fsumrecl 13849 |
. . . . . . 7
                   |
159 | 14, 158 | remulcld 9697 |
. . . . . 6
  
                  |
160 | 159 | adantr 471 |
. . . . 5
 
  
                  |
161 | 14, 126 | remulcld 9697 |
. . . . . . . . 9
  
    |
162 | 14, 14 | remulcld 9697 |
. . . . . . . . 9
     |
163 | 161, 162 | resubcld 10075 |
. . . . . . . 8
   
  
    |
164 | 126, 123 | nndivred 10686 |
. . . . . . . . . 10
       |
165 | 162, 164 | remulcld 9697 |
. . . . . . . . 9
           |
166 | 161, 165 | resubcld 10075 |
. . . . . . . 8
   
             |
167 | 126, 14 | resubcld 10075 |
. . . . . . . . . 10
       |
168 | 122, 14 | readdcld 9696 |
. . . . . . . . . . . 12
     |
169 | 1, 7, 9 | redivcli 10402 |
. . . . . . . . . . . . . . 15
   |
170 | 169 | a1i 11 |
. . . . . . . . . . . . . 14
     |
171 | | stoweidlem26.12 |
. . . . . . . . . . . . . 14
     |
172 | 14, 170, 122, 171 | ltadd2dd 9820 |
. . . . . . . . . . . . 13
  
      |
173 | | ax-1cn 9623 |
. . . . . . . . . . . . . . 15
 |
174 | 66, 173, 66, 9 | divdiri 10392 |
. . . . . . . . . . . . . 14
           |
175 | | 3p1e4 10764 |
. . . . . . . . . . . . . . 15
   |
176 | 175 | oveq1i 6325 |
. . . . . . . . . . . . . 14
       |
177 | 67 | oveq1i 6325 |
. . . . . . . . . . . . . 14
           |
178 | 174, 176,
177 | 3eqtr3ri 2493 |
. . . . . . . . . . . . 13
       |
179 | 172, 178 | syl6breq 4456 |
. . . . . . . . . . . 12
  
    |
180 | 168, 118,
114, 179 | ltsub2dd 10254 |
. . . . . . . . . . 11
           |
181 | 173 | a1i 11 |
. . . . . . . . . . . 12
   |
182 | 13 | rpcnd 11372 |
. . . . . . . . . . . 12
   |
183 | 145, 181,
182 | subsub4d 10043 |
. . . . . . . . . . 11
           |
184 | 180, 183 | breqtrrd 4443 |
. . . . . . . . . 10
           |
185 | 119, 167,
13, 184 | ltmul1dd 11422 |
. . . . . . . . 9
      
        |
186 | 145, 181 | subcld 10012 |
. . . . . . . . . . . 12
     |
187 | 186, 182 | subcld 10012 |
. . . . . . . . . . 11
       |
188 | 182, 187 | mulcomd 9690 |
. . . . . . . . . 10
               |
189 | 182, 186,
182 | subdid 10102 |
. . . . . . . . . 10
                 |
190 | 188, 189 | eqtr3d 2498 |
. . . . . . . . 9
                 |
191 | 185, 190 | breqtrd 4441 |
. . . . . . . 8
      
 
        |
192 | | 1zzd 10997 |
. . . . . . . . . . . . . . . . 17
   |
193 | | elfz 11819 |
. . . . . . . . . . . . . . . . 17
 
 
   
     |
194 | 131, 192,
135, 193 | syl3anc 1276 |
. . . . . . . . . . . . . . . 16
      
    |
195 | 31, 194 | mpbid 215 |
. . . . . . . . . . . . . . 15
 
   |
196 | 195 | simprd 469 |
. . . . . . . . . . . . . 14

  |
197 | | zlem1lt 11017 |
. . . . . . . . . . . . . . 15
 
       |
198 | 131, 135,
197 | syl2anc 671 |
. . . . . . . . . . . . . 14
       |
199 | 196, 198 | mpbid 215 |
. . . . . . . . . . . . 13
     |
200 | 123 | nngt0d 10681 |
. . . . . . . . . . . . . 14
   |
201 | | ltdiv1 10497 |
. . . . . . . . . . . . . 14
   

              |
202 | 126, 140,
140, 200, 201 | syl112anc 1280 |
. . . . . . . . . . . . 13
             |
203 | 199, 202 | mpbid 215 |
. . . . . . . . . . . 12
    
    |
204 | 123 | nncnd 10653 |
. . . . . . . . . . . . 13
   |
205 | 123 | nnne0d 10682 |
. . . . . . . . . . . . 13
   |
206 | 204, 205 | dividd 10409 |
. . . . . . . . . . . 12
     |
207 | 203, 206 | breqtrd 4441 |
. . . . . . . . . . 11
    
  |
208 | 14, 14, 78, 78 | mulgt0d 9816 |
. . . . . . . . . . . 12
     |
209 | | ltmul2 10484 |
. . . . . . . . . . . 12
     
                           |
210 | 164, 122,
162, 208, 209 | syl112anc 1280 |
. . . . . . . . . . 11
                     |
211 | 207, 210 | mpbid 215 |
. . . . . . . . . 10
               |
212 | 182, 182 | mulcld 9689 |
. . . . . . . . . . 11
     |
213 | 212 | mulid1d 9686 |
. . . . . . . . . 10
         |
214 | 211, 213 | breqtrd 4441 |
. . . . . . . . 9
             |
215 | 165, 162,
161, 214 | ltsub2dd 10254 |
. . . . . . . 8
   
  
 
 
              |
216 | 120, 163,
166, 191, 215 | lttrd 9822 |
. . . . . . 7
      
 
              |
217 | 182, 204,
205 | divcld 10411 |
. . . . . . . . . . 11
     |
218 | 181, 217,
186 | subdird 10103 |
. . . . . . . . . 10
      
                |
219 | 186 | mulid2d 9687 |
. . . . . . . . . . 11
  
      |
220 | 219 | oveq1d 6330 |
. . . . . . . . . 10
                         |
221 | 218, 220 | eqtrd 2496 |
. . . . . . . . 9
      
              |
222 | 221 | oveq2d 6331 |
. . . . . . . 8
                         |
223 | 217, 186 | mulcld 9689 |
. . . . . . . . 9
    
    |
224 | 182, 186,
223 | subdid 10102 |
. . . . . . . 8
                      
      |
225 | 182, 204,
186, 205 | div32d 10434 |
. . . . . . . . . . 11
    
          |
226 | 225 | oveq2d 6331 |
. . . . . . . . . 10
                   |
227 | 186, 204,
205 | divcld 10411 |
. . . . . . . . . . 11
       |
228 | 182, 182,
227 | mulassd 9692 |
. . . . . . . . . 10
                   |
229 | 226, 228 | eqtr4d 2499 |
. . . . . . . . 9
                   |
230 | 229 | oveq2d 6331 |
. . . . . . . 8
   
  
                        |
231 | 222, 224,
230 | 3eqtrd 2500 |
. . . . . . 7
                           |
232 | 216, 231 | breqtrrd 4443 |
. . . . . 6
      
      
     |
233 | 232 | adantr 471 |
. . . . 5
 
      
      
     |
234 | 181, 217 | subcld 10012 |
. . . . . . . . . 10
       |
235 | | fsumconst 13900 |
. . . . . . . . . 10
     
                          
          |
236 | 130, 234,
235 | syl2anc 671 |
. . . . . . . . 9
                    
          |
237 | 236 | adantr 471 |
. . . . . . . 8
 
                    
          |
238 | | 0zd 10978 |
. . . . . . . . . . . . 13
 
   |
239 | 31 | adantr 471 |
. . . . . . . . . . . . . . 15
 

      |
240 | 239, 112 | syl 17 |
. . . . . . . . . . . . . 14
 

  |
241 | 132 | a1i 11 |
. . . . . . . . . . . . . 14
 
   |
242 | 240, 241 | zsubcld 11074 |
. . . . . . . . . . . . 13
 
     |
243 | | elnnuz 11224 |
. . . . . . . . . . . . . . . . . . . 20

      |
244 | 123, 243 | sylib 201 |
. . . . . . . . . . . . . . . . . . 19
       |
245 | | elfzp12 11902 |
. . . . . . . . . . . . . . . . . . 19
    
                |
246 | 244, 245 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                 |
247 | 31, 246 | mpbid 215 |
. . . . . . . . . . . . . . . . 17
           |
248 | 247 | orcanai 929 |
. . . . . . . . . . . . . . . 16
 

        |
249 | | 1p1e2 10751 |
. . . . . . . . . . . . . . . . . 18
   |
250 | 249 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
     |
251 | 250 | oveq1d 6330 |
. . . . . . . . . . . . . . . 16
 
             |
252 | 248, 251 | eleqtrd 2542 |
. . . . . . . . . . . . . . 15
 

      |
253 | | elfzle1 11831 |
. . . . . . . . . . . . . . 15
       |
254 | 252, 253 | syl 17 |
. . . . . . . . . . . . . 14
 

  |
255 | 114 | adantr 471 |
. . . . . . . . . . . . . . 15
 

  |
256 | 137 | a1i 11 |
. . . . . . . . . . . . . . 15
 
   |
257 | 255, 256 | subge0d 10231 |
. . . . . . . . . . . . . 14
 
  

   |
258 | 254, 257 | mpbird 240 |
. . . . . . . . . . . . 13
 

    |
259 | 238, 242,
258 | 3jca 1194 |
. . . . . . . . . . . 12
 
         |
260 | | eluz2 11194 |
. . . . . . . . . . . 12
               |
261 | 259, 260 | sylibr 217 |
. . . . . . . . . . 11
 
         |
262 | | hashfz 12632 |
. . . . . . . . . . 11
      
                  |
263 | 261, 262 | syl 17 |
. . . . . . . . . 10
 
                   |
264 | | 2cn 10708 |
. . . . . . . . . . . . . . . 16
 |
265 | 264 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
266 | 145, 265 | subcld 10012 |
. . . . . . . . . . . . . 14
     |
267 | 266 | subid1d 10001 |
. . . . . . . . . . . . 13
         |
268 | 267 | oveq1d 6330 |
. . . . . . . . . . . 12
             |
269 | 145, 265,
181 | subadd23d 10034 |
. . . . . . . . . . . 12
           |
270 | 264, 173 | negsubdi2i 9987 |
. . . . . . . . . . . . . . . 16
      |
271 | | 2m1e1 10752 |
. . . . . . . . . . . . . . . . 17
   |
272 | 271 | negeqi 9894 |
. . . . . . . . . . . . . . . 16
     |
273 | 270, 272 | eqtr3i 2486 |
. . . . . . . . . . . . . . 15
    |
274 | 273 | a1i 11 |
. . . . . . . . . . . . . 14
      |
275 | 274 | oveq2d 6331 |
. . . . . . . . . . . . 13
          |
276 | 145, 181 | negsubd 10018 |
. . . . . . . . . . . . 13
        |
277 | 275, 276 | eqtrd 2496 |
. . . . . . . . . . . 12
         |
278 | 268, 269,
277 | 3eqtrd 2500 |
. . . . . . . . . . 11
           |
279 | 278 | adantr 471 |
. . . . . . . . . 10
 
           |
280 | 263, 279 | eqtrd 2496 |
. . . . . . . . 9
 
               |
281 | 280 | oveq1d 6330 |
. . . . . . . 8
 
                           |
282 | 186, 234 | mulcomd 9690 |
. . . . . . . . 9
                   |
283 | 282 | adantr 471 |
. . . . . . . 8
 
                   |
284 | 237, 281,
283 | 3eqtrd 2500 |
. . . . . . 7
 
                       |
285 | | fzfid 12218 |
. . . . . . . 8
 
    
    |
286 | | fzn0 11842 |
. . . . . . . . 9
               |
287 | 261, 286 | sylibr 217 |
. . . . . . . 8
 
    
    |
288 | 125 | ad2antrr 737 |
. . . . . . . 8
  
       
      |
289 | | simpll 765 |
. . . . . . . . 9
  
       
  |
290 | 156 | adantlr 726 |
. . . . . . . . 9
  
       
      |
291 | 289, 290,
57 | syl2anc 671 |
. . . . . . . 8
  
       
          |
292 | 55 | adantr 471 |
. . . . . . . . . . . 12
 
   
     |
293 | | elfzelz 11829 |
. . . . . . . . . . . . . . . . 17
         |
294 | 293 | zred 11069 |
. . . . . . . . . . . . . . . 16
         |
295 | 294 | adantl 472 |
. . . . . . . . . . . . . . 15
 
   
     |
296 | 169 | a1i 11 |
. . . . . . . . . . . . . . 15
 
   
       |
297 | 295, 296 | readdcld 9696 |
. . . . . . . . . . . . . 14
 
   
         |
298 | 14 | adantr 471 |
. . . . . . . . . . . . . 14
 
   
     |
299 | 297, 298 | remulcld 9697 |
. . . . . . . . . . . . 13
 
   
           |
300 | 114 | adantr 471 |
. . . . . . . . . . . . . . . 16
 
   
     |
301 | 137 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
   
     |
302 | 300, 301 | resubcld 10075 |
. . . . . . . . . . . . . . 15
 
   
   
   |
303 | 302, 296 | readdcld 9696 |
. . . . . . . . . . . . . 14
 
   
           |
304 | 303, 298 | remulcld 9697 |
. . . . . . . . . . . . 13
 
   
             |
305 | | stoweidlem26.10 |
. . . . . . . . . . . . . . . 16
       |
306 | 305, 55 | jca 539 |
. . . . . . . . . . . . . . 15
         |
307 | 306 | adantr 471 |
. . . . . . . . . . . . . 14
 
   
       
   |
308 | | ffvelrn 6043 |
. . . . . . . . . . . . . 14
     
       |
309 | 307, 308 | syl 17 |
. . . . . . . . . . . . 13
 
   
         |
310 | | elfzle2 11832 |
. . . . . . . . . . . . . . . 16
           |
311 | 310 | adantl 472 |
. . . . . . . . . . . . . . 15
 
   
       |
312 | 295, 302,
296, 311 | leadd1dd 10255 |
. . . . . . . . . . . . . 14
 
   
               |
313 | 14, 78 | jca 539 |
. . . . . . . . . . . . . . . 16
     |
314 | 313 | adantr 471 |
. . . . . . . . . . . . . . 15
 
   
   
   |
315 | | lemul1 10485 |
. . . . . . . . . . . . . . 15
            
 
          
                 |
316 | 297, 303,
314, 315 | syl3anc 1276 |
. . . . . . . . . . . . . 14
 
   
       
 
   
                 |
317 | 312, 316 | mpbid 215 |
. . . . . . . . . . . . 13
 
   
                   |
318 | 114, 138 | resubcld 10075 |
. . . . . . . . . . . . . . . . 17
     |
319 | 318, 170 | readdcld 9696 |
. . . . . . . . . . . . . . . 16
         |
320 | 319, 14 | remulcld 9697 |
. . . . . . . . . . . . . . 15
           |
321 | 305, 55 | ffvelrnd 6046 |
. . . . . . . . . . . . . . 15
       |
322 | 126, 170 | resubcld 10075 |
. . . . . . . . . . . . . . . . 17
         |
323 | 322, 14 | remulcld 9697 |
. . . . . . . . . . . . . . . 16
           |
324 | | addid1 9839 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
325 | 324 | eqcomd 2468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
326 | 173, 325 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
327 | 181 | subidd 10000 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
328 | 327 | eqcomd 2468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
329 | 328 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
330 | | addsubass 9911 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
           |
331 | 330 | eqcomd 2468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
           |
332 | 181, 181,
181, 331 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
333 | 326, 329,
332 | 3eqtrd 2500 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
334 | 333 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . . . 21
           |
335 | 249 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
336 | 335 | oveq1d 6330 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
337 | 336 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . . . 21
             |
338 | 145, 265,
181 | subsubd 10040 |
. . . . . . . . . . . . . . . . . . . . 21
           |
339 | 334, 337,
338 | 3eqtrd 2500 |
. . . . . . . . . . . . . . . . . . . 20
         |
340 | 339 | oveq1d 6330 |
. . . . . . . . . . . . . . . . . . 19
                 |
341 | 264, 66, 9 | divcli 10377 |
. . . . . . . . . . . . . . . . . . . . 21
   |
342 | 341 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
     |
343 | 266, 181,
342 | addsubassd 10032 |
. . . . . . . . . . . . . . . . . . 19
                   |
344 | 173, 66, 9 | divcli 10377 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
345 | | df-3 10697 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
346 | 345 | oveq1i 6325 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
347 | 264, 173,
66, 9 | divdiri 10392 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
348 | 346, 67, 347 | 3eqtr3ri 2493 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
349 | 173, 341,
344, 348 | subaddrii 9990 |
. . . . . . . . . . . . . . . . . . . . 21
       |
350 | 349 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
         |
351 | 350 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . 19
                 |
352 | 340, 343,
351 | 3eqtrd 2500 |
. . . . . . . . . . . . . . . . . 18
               |
353 | 137, 7, 9 | redivcli 10402 |
. . . . . . . . . . . . . . . . . . . 20
   |
354 | 353 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
     |
355 | | 1lt2 10805 |
. . . . . . . . . . . . . . . . . . . 20
 |
356 | 7, 69 | pm3.2i 461 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
357 | 1, 137, 356 | 3pm3.2i 1192 |
. . . . . . . . . . . . . . . . . . . . 21
     |
358 | | ltdiv1 10497 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
359 | 357, 358 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
         |
360 | 355, 359 | mpbii 216 |
. . . . . . . . . . . . . . . . . . 19
  
    |
361 | 170, 354,
126, 360 | ltsub2dd 10254 |
. . . . . . . . . . . . . . . . . 18
               |
362 | 352, 361 | eqbrtrrd 4439 |
. . . . . . . . . . . . . . . . 17
               |
363 | 319, 322,
13, 362 | ltmul1dd 11422 |
. . . . . . . . . . . . . . . 16
        
          |
364 | 23 | simprd 469 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
365 | 195 | simpld 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

  |
366 | 140, 122 | readdcld 9696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
367 | 140 | lep1d 10566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

    |
368 | 114, 140,
366, 196, 367 | letrd 9818 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

    |
369 | 135 | peano2zd 11072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
370 | | elfz 11819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

         
      |
371 | 131, 192,
369, 370 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        
      |
372 | 365, 368,
371 | mpbir2and 938 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
373 | 145, 181 | npcand 10016 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
374 | | 0p1e1 10749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
375 | 374 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
376 | 375 | oveq1d 6330 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
          |
377 | 372, 373,
376 | 3eltr4d 2555 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
378 | | 0zd 10978 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
379 | 131, 192 | zsubcld 11074 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
380 | | fzaddel 11862 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                               |
381 | 378, 135,
379, 192, 380 | syl22anc 1277 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                       |
382 | 377, 381 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
383 | | rabexg 4567 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 |
384 | 33, 383 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
385 | | oveq1 6322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
               |
386 | 385 | oveq1d 6330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                   |
387 | 386 | breq2d 4428 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
     
               |
388 | 387 | rabbidv 3048 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                               |
389 | 388, 40 | fvmptg 5969 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
             
                  |
390 | 382, 384,
389 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                  |
391 | 364, 390 | neleqtrd 2561 |
. . . . . . . . . . . . . . . . . . . . . 22
     
           |
392 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
393 | 47, 48, 392 | nfbr 4461 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
         |
394 | 51 | breq1d 4426 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
       
               |
395 | 44, 45, 393, 394 | elrabf 3206 |
. . . . . . . . . . . . . . . . . . . . . 22
              

               |
396 | 391, 395 | sylnib 310 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
397 | | ianor 495 |
. . . . . . . . . . . . . . . . . . . . 21
     
                         |
398 | 396, 397 | sylib 201 |
. . . . . . . . . . . . . . . . . . . 20
                 |
399 | | olc 390 |
. . . . . . . . . . . . . . . . . . . . 21
     
           |
400 | 399 | anim1i 576 |
. . . . . . . . . . . . . . . . . . . 20
  
                             
                |
401 | 55, 398, 400 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . 19
                
                |
402 | | orcom 393 |
. . . . . . . . . . . . . . . . . . . 20
                               |
403 | 402 | anbi2i 705 |
. . . . . . . . . . . . . . . . . . 19
                
             
     
                          |
404 | 401, 403 | sylib 201 |
. . . . . . . . . . . . . . . . . 18
                    
            |
405 | | pm4.43 943 |
. . . . . . . . . . . . . . . . . 18
    
       
     
                          |
406 | 404, 405 | sylibr 217 |
. . . . . . . . . . . . . . . . 17
               |
407 | 323, 321 | ltnled 9808 |
. . . . . . . . . . . . . . . . 17
                 
           |
408 | 406, 407 | mpbird 240 |
. . . . . . . . . . . . . . . 16
        
      |
409 | 320, 323,
321, 363, 408 | lttrd 9822 |
. . . . . . . . . . . . . . 15
        
      |
410 | 320, 321,
409 | ltled 9809 |
. . . . . . . . . . . . . 14
        
      |
411 | 410 | adantr 471 |
. . . . . . . . . . . . 13
 
   
                 |
412 | 299, 304,
309, 317, 411 | letrd 9818 |
. . . . . . . . . . . 12
 
   
               |
413 | | nfcv 2603 |
. . . . . . . . . . . . . 14
         |
414 | 413, 48, 47 | nfbr 4461 |
. . . . . . . . . . . . 13
       
     |
415 | 51 | breq2d 4428 |
. . . . . . . . . . . . 13
       
   
             |
416 | 44, 45, 414, 415 | elrabf 3206 |
. . . . . . . . . . . 12
            

             |
417 | 292, 412,
416 | sylanbrc 675 |
. . . . . . . . . . 11
 
   
                 |
418 | | rabexg 4567 |
. . . . . . . . . . . . . 14
               |
419 | 33, 418 | syl 17 |
. . . . . . . . . . . . 13
            
  |
420 | 419 | adantr 471 |
. . . . . . . . . . . 12
 
   
                 |
421 | | oveq1 6322 |
. . . . . . . . . . . . . . . 16
           |
422 | 421 | oveq1d 6330 |
. . . . . . . . . . . . . . 15
               |
423 | 422 | breq1d 4426 |
. . . . . . . . . . . . . 14
       
   
             |
424 | 423 | rabbidv 3048 |
. . . . . . . . . . . . 13
                           |
425 | | stoweidlem26.5 |
. . . . . . . . . . . . 13
                   |
426 | 424, 425 | fvmptg 5969 |
. . . . . . . . . . . 12
            
     
                  |
427 | 156, 420,
426 | syl2anc 671 |
. . . . . . . . . . 11
 
   
                     |
428 | 417, 427 | eleqtrrd 2543 |
. . . . . . . . . 10
 
   
         |
429 | 151 | 3ad2ant1 1035 |
. . . . . . . . . . . . . 14
 
   
         

    |
430 | 429, 152 | sylibr 217 |
. . . . . . . . . . . . 13
 
   
               |
431 | 430, 154 | syl 17 |
. . . . . . . . . . . 12
 
   
                   |
432 | | simp2 1015 |
. . . . . . . . . . . 12
 
   
          
    |
433 | 431, 432 | sseldd 3445 |
. . . . . . . . . . 11
 
   
             |
434 | | elex 3066 |
. . . . . . . . . . . . 13
       |
435 | 434 | 3ad2ant3 1037 |
. . . . . . . . . . . 12
 
   
    
  |
436 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . . 19
       |
437 | | nfrab1 2983 |
. . . . . . . . . . . . . . . . . . 19
               |
438 | 436, 437 | nfmpt 4505 |
. . . . . . . . . . . . . . . . . 18
                     |
439 | 425, 438 | nfcxfr 2601 |
. . . . . . . . . . . . . . . . 17
   |
440 | | nfcv 2603 |
. . . . . . . . . . . . . . . . 17
   |
441 | 439, 440 | nffv 5895 |
. . . . . . . . . . . . . . . 16
       |
442 | 441 | nfel2 2619 |
. . . . . . . . . . . . . . 15
      |
443 | 94, 95, 442 | nf3an 2024 |
. . . . . . . . . . . . . 14
      
      |
444 | | nfv 1772 |
. . . . . . . . . . . . . 14
               |
445 | 443, 444 | nfim 2014 |
. . . . . . . . . . . . 13
   
   
                   |
446 | | eleq1 2528 |
. . . . . . . . . . . . . . 15
     
       |
447 | 446 | 3anbi3d 1354 |
. . . . . . . . . . . . . 14
  
   
     
   
        |
448 | 99 | breq2d 4428 |
. . . . . . . . . . . . . 14
             
               |
449 | 447, 448 | imbi12d 326 |
. . . . . . . . . . . . 13
   
   
                 
          
                |
450 | | stoweidlem26.15 |
. . . . . . . . . . . . 13
 
   
    
              |
451 | 445, 449,
450 | vtoclg1f 3118 |
. . . . . . . . . . . 12
  
   
    
               |
452 | 435, 451 | mpcom 37 |
. . . . . . . . . . 11
 
   
    
              |
453 | 433, 452 | syld3an2 1323 |
. . . . . . . . . 10
 
   
                     |
454 | 428, 453 | mpd3an3 1374 |
. . . . . . . . 9
 
   
                 |
455 | 454 | adantlr 726 |
. . . . . . . 8
  
       
              |
456 | 285, 287,
288, 291, 455 | fsumlt 13909 |
. . . . . . 7
 
                               |
457 | 284, 456 | eqbrtrrd 4439 |
. . . . . 6
 
      
      
             |
458 | 127 | adantr 471 |
. . . . . . 7
 
      
    |
459 | 158 | adantr 471 |
. . . . . . 7
 
                   |
460 | 313 | adantr 471 |
. . . . . . 7
 
     |
461 | | ltmul2 10484 |
. . . . . . 7
       
                              
                                              |
462 | 458, 459,
460, 461 | syl3anc 1276 |
. . . . . 6
 
          
                                              |
463 | 457, 462 | mpbid 215 |
. . . . 5
 
                               |
464 | 121, 129,
160, 233, 463 | lttrd 9822 |
. . . 4
 
      
                    |
465 | 156, 58 | syldan 477 |
. . . . . . . . . 10
 
   
   
           |
466 | 465 | adantlr 726 |
. . . . . . . . 9
  
       
            |
467 | 466 | recnd 9695 |
. . . . . . . 8
  
       
            |
468 | 285, 467 | fsumcl 13848 |
. . . . . . 7
 
                     |
469 | 468 | addid1d 9859 |
. . . . . 6
 
                                         |
470 | | 0red 9670 |
. . . . . . 7
 
   |
471 | | fzfid 12218 |
. . . . . . . 8
 
         |
472 | 14 | adantr 471 |
. . . . . . . . . 10
 
         |
473 | | 0red 9670 |
. . . . . . . . . . . . 13
 
         |
474 | 126 | adantr 471 |
. . . . . . . . . . . . 13
 
       
   |
475 | | elfzelz 11829 |
. . . . . . . . . . . . . . 15
         |
476 | 475 | zred 11069 |
. . . . . . . . . . . . . 14
         |
477 | 476 | adantl 472 |
. . . . . . . . . . . . 13
 
         |
478 | | 1m1e0 10706 |
. . . . . . . . . . . . . . 15
   |
479 | 122, 114,
122, 365 | lesub1dd 10257 |
. . . . . . . . . . . . . . 15
  
    |
480 | 478, 479 | syl5eqbrr 4451 |
. . . . . . . . . . . . . 14

    |
481 | 480 | adantr 471 |
. . . . . . . . . . . . 13
 
           |
482 | | simpr 467 |
. . . . . . . . . . . . . . 15
 
               |
483 | 475 | adantl 472 |
. . . . . . . . . . . . . . . 16
 
         |
484 | 379 | adantr 471 |
. . . . . . . . . . . . . . . 16
 
       
   |
485 | 135 | adantr 471 |
. . . . . . . . . . . . . . . 16
 
         |
486 | | elfz 11819 |
. . . . . . . . . . . . . . . 16
  

          
    |
487 | 483, 484,
485, 486 | syl3anc 1276 |
. . . . . . . . . . . . . . 15
 
             
 
     |
488 | 482, 487 | mpbid 215 |
. . . . . . . . . . . . . 14
 
         
   |
489 | 488 | simpld 465 |
. . . . . . . . . . . . 13
 
       
   |
490 | 473, 474,
477, 481, 489 | letrd 9818 |
. . . . . . . . . . . 12
 
         |
491 | | elfzle2 11832 |
. . . . . . . . . . . . 13
         |
492 | 491 | adantl 472 |
. . . . . . . . . . . 12
 
         |
493 | | 0zd 10978 |
. . . . . . . . . . . . 13
 
         |
494 | | elfz 11819 |
. . . . . . . . . . . . 13
 
     
     |
495 | 483, 493,
485, 494 | syl3anc 1276 |
. . . . . . . . . . . 12
 
           
     |
496 | 490, 492,
495 | mpbir2and 938 |
. . . . . . . . . . 11
 
             |
497 | 496, 57 | syldan 477 |
. . . . . . . . . 10
 
                 |
498 | 472, 497 | remulcld 9697 |
. . . . . . . . 9
 
       
           |
499 | 498 | adantlr 726 |
. . . . . . . 8
  
       
            |
500 | 471, 499 | fsumrecl 13849 |
. . . . . . 7
 
                     |
501 | 285, 466 | fsumrecl 13849 |
. . . . . . 7
 
                     |
502 | | fzfid 12218 |
. . . . . . . . 9
         |
503 | 182 | adantr 471 |
. . . . . . . . . . 11
 
         |
504 | 503 | mul01d 9858 |
. . . . . . . . . 10
 
       
   |
505 | 496, 106 | syldan 477 |
. . . . . . . . . . 11
 
                 |
506 | 313 | adantr 471 |
. . . . . . . . . . . 12
 
       
   |
507 | | lemul2 10486 |
. . . . . . . . . . . 12
          
 
        
  
            |
508 | 473, 497,
506, 507 | syl3anc 1276 |
. . . . . . . . . . 11
 
       
       
  
            |
509 | 505, 508 | mpbid 215 |
. . . . . . . . . 10
 
       
             |
510 | 504, 509 | eqbrtrrd 4439 |
. . . . . . . . 9
 
                   |
511 | 502, 498,
510 | fsumge0 13904 |
. . . . . . . 8

                    |
512 | 511 | adantr 471 |
. . . . . . 7
 

                    |
513 | 470, 500,
501, 512 | leadd2dd 10256 |
. . . . . 6
 
                          
             
 
                  |
514 | 469, 513 | eqbrtrrd 4439 |
. . . . 5
 
                        
             
 
                  |
515 | 157 | recnd 9695 |
. . . . . . 7
 
   
             |
516 | 130, 182,
515 | fsummulc2 13894 |
. . . . . 6
  
                    
               |
517 | 516 | adantr 471 |
. . . . 5
 
  
                    
               |
518 | | stoweidlem26.2 |
. . . . . . . . 9
   |
519 | | elfzelz 11829 |
. . . . . . . . . . . . . . . 16
         |
520 | 519 | adantl 472 |
. . . . . . . . . . . . . . 15
 
   
     |
521 | 520 | zred 11069 |
. . . . . . . . . . . . . 14
 
   
     |
522 | 318 | adantr 471 |
. . . . . . . . . . . . . 14
 
   
   
   |
523 | 126 | adantr 471 |
. . . . . . . . . . . . . 14
 
   
   
   |
524 | | simpr 467 |
. . . . . . . . . . . . . . . 16
 
   
      
    |
525 | | 0zd 10978 |
. . . . . . . . . . . . . . . . 17
 
   
     |
526 | 134 | adantr 471 |
. . . . . . . . . . . . . . . . 17
 
   
   
   |
527 | | elfz 11819 |
. . . . . . . . . . . . . . . . 17
 

         
      |
528 | 520, 525,
526, 527 | syl3anc 1276 |
. . . . . . . . . . . . . . . 16
 
   
         
       |
529 | 524, 528 | mpbid 215 |
. . . . . . . . . . . . . . 15
 
   
   
     |
530 | 529 | simprd 469 |
. . . . . . . . . . . . . 14
 
   
       |
531 | 122, 138,
114 | ltsub2d 10251 |
. . . . . . . . . . . . . . . 16
         |
532 | 355, 531 | mpbii 216 |
. . . . . . . . . . . . . . 15
       |
533 | 532 | adantr 471 |
. . . . . . . . . . . . . 14
 
   
   
     |
534 | 521, 522,
523, 530, 533 | lelttrd 9819 |
. . . . . . . . . . . . 13
 
   
       |
535 | 521, 523 | ltnled 9808 |
. . . . . . . . . . . . 13
 
   
   
 

    |
536 | 534, 535 | mpbid 215 |
. . . . . . . . . . . 12
  |