Proof of Theorem abelthlem7
Step | Hyp | Ref
| Expression |
1 | | abelth.1 |
. . . . 5
       |
2 | | abelth.2 |
. . . . 5
     |
3 | | abelth.3 |
. . . . 5
   |
4 | | abelth.4 |
. . . . 5

  |
5 | | abelth.5 |
. . . . 5
      
          |
6 | | abelth.6 |
. . . . 5
 
            |
7 | 1, 2, 3, 4, 5, 6 | abelthlem4 23382 |
. . . 4
       |
8 | | abelthlem6.1 |
. . . . 5
       |
9 | 8 | eldifad 3415 |
. . . 4
   |
10 | 7, 9 | ffvelrnd 6021 |
. . 3
       |
11 | 10 | abscld 13491 |
. 2
           |
12 | | ax-1cn 9594 |
. . . . . 6
 |
13 | | abelth.7 |
. . . . . . . 8
      |
14 | 1, 2, 3, 4, 5, 6, 13, 8 | abelthlem7a 23385 |
. . . . . . 7
       
           |
15 | 14 | simpld 461 |
. . . . . 6
   |
16 | | subcl 9871 |
. . . . . 6
 
     |
17 | 12, 15, 16 | sylancr 668 |
. . . . 5
     |
18 | | fzfid 12183 |
. . . . . 6
    
    |
19 | | elfznn0 11884 |
. . . . . . 7
         |
20 | | nn0uz 11190 |
. . . . . . . . . 10
     |
21 | | 0zd 10946 |
. . . . . . . . . 10
   |
22 | 1 | ffvelrnda 6020 |
. . . . . . . . . 10
 

      |
23 | 20, 21, 22 | serf 12238 |
. . . . . . . . 9
          |
24 | 23 | ffvelrnda 6020 |
. . . . . . . 8
 

        |
25 | | expcl 12287 |
. . . . . . . . 9
 
       |
26 | 15, 25 | sylan 474 |
. . . . . . . 8
 

      |
27 | 24, 26 | mulcld 9660 |
. . . . . . 7
 

              |
28 | 19, 27 | sylan2 477 |
. . . . . 6
 
   
                 |
29 | 18, 28 | fsumcl 13792 |
. . . . 5
 
                     |
30 | 17, 29 | mulcld 9660 |
. . . 4
                           |
31 | 30 | abscld 13491 |
. . 3
           
                   |
32 | | eqid 2450 |
. . . . . 6
         |
33 | | abelthlem7.3 |
. . . . . . 7
   |
34 | 33 | nn0zd 11035 |
. . . . . 6
   |
35 | | eluznn0 11225 |
. . . . . . . 8
 
    
  |
36 | 33, 35 | sylan 474 |
. . . . . . 7
 
    
  |
37 | | fveq2 5863 |
. . . . . . . . 9
               |
38 | | oveq2 6296 |
. . . . . . . . 9
           |
39 | 37, 38 | oveq12d 6306 |
. . . . . . . 8
                           |
40 | | eqid 2450 |
. . . . . . . 8

             
              |
41 | | ovex 6316 |
. . . . . . . 8
             |
42 | 39, 40, 41 | fvmpt 5946 |
. . . . . . 7

                                |
43 | 36, 42 | syl 17 |
. . . . . 6
 
    
                                |
44 | 36, 27 | syldan 473 |
. . . . . 6
 
    
              |
45 | 1, 2, 3, 4, 5 | abelthlem2 23380 |
. . . . . . . . . 10
                  |
46 | 45 | simprd 465 |
. . . . . . . . 9
                |
47 | 46, 8 | sseldd 3432 |
. . . . . . . 8
            |
48 | 1, 2, 3, 4, 5, 6, 13 | abelthlem5 23383 |
. . . . . . . 8
 
         
                  |
49 | 47, 48 | mpdan 673 |
. . . . . . 7
                   |
50 | 42 | adantl 468 |
. . . . . . . . 9
 

                                |
51 | 50, 27 | eqeltrd 2528 |
. . . . . . . 8
 

                    |
52 | 20, 33, 51 | iserex 13713 |
. . . . . . 7
   
                                 |
53 | 49, 52 | mpbid 214 |
. . . . . 6
                   |
54 | 32, 34, 43, 44, 53 | isumcl 13815 |
. . . . 5
 
                   |
55 | 17, 54 | mulcld 9660 |
. . . 4
                         |
56 | 55 | abscld 13491 |
. . 3
                             |
57 | 31, 56 | readdcld 9667 |
. 2
            
                                              |
58 | | peano2re 9803 |
. . . 4
 
   |
59 | 3, 58 | syl 17 |
. . 3
     |
60 | | abelthlem7.2 |
. . . 4
   |
61 | 60 | rpred 11338 |
. . 3
   |
62 | 59, 61 | remulcld 9668 |
. 2
       |
63 | 1, 2, 3, 4, 5, 6, 13, 8 | abelthlem6 23384 |
. . . . 5
                        |
64 | 20, 32, 33, 50, 27, 49 | isumsplit 13891 |
. . . . . 6
 
             
                                        |
65 | 64 | oveq2d 6304 |
. . . . 5
    
                     
                                     |
66 | 17, 29, 54 | adddid 9664 |
. . . . 5
                                                                                               |
67 | 63, 65, 66 | 3eqtrd 2488 |
. . . 4
             
                                         |
68 | 67 | fveq2d 5867 |
. . 3
                
                                              |
69 | 30, 55 | abstrid 13511 |
. . 3
                                                    
       
                                                  |
70 | 68, 69 | eqbrtrd 4422 |
. 2
        
       
                                                  |
71 | 3, 61 | remulcld 9668 |
. . . 4
     |
72 | 17 | abscld 13491 |
. . . . . 6
         |
73 | 24 | abscld 13491 |
. . . . . . . . 9
 

            |
74 | 19, 73 | sylan2 477 |
. . . . . . . 8
 
   
               |
75 | 18, 74 | fsumrecl 13793 |
. . . . . . 7
 
                   |
76 | | peano2re 9803 |
. . . . . . 7
           
        
                    |
77 | 75, 76 | syl 17 |
. . . . . 6
                       |
78 | 72, 77 | remulcld 9668 |
. . . . 5
                   
           |
79 | 17, 29 | absmuld 13509 |
. . . . . 6
           
                                                   |
80 | 29 | abscld 13491 |
. . . . . . 7
                           |
81 | 17 | absge0d 13499 |
. . . . . . 7

        |
82 | 27 | abscld 13491 |
. . . . . . . . . . . 12
 

                  |
83 | 19, 82 | sylan2 477 |
. . . . . . . . . . 11
 
   
                     |
84 | 18, 83 | fsumrecl 13793 |
. . . . . . . . . 10
 
                         |
85 | 18, 28 | fsumabs 13854 |
. . . . . . . . . 10
                        
    
                     |
86 | 15 | abscld 13491 |
. . . . . . . . . . . . . . 15
       |
87 | | reexpcl 12286 |
. . . . . . . . . . . . . . 15
     
           |
88 | 86, 87 | sylan 474 |
. . . . . . . . . . . . . 14
 

          |
89 | | 1red 9655 |
. . . . . . . . . . . . . 14
 

  |
90 | 24 | absge0d 13499 |
. . . . . . . . . . . . . 14
 

            |
91 | 86 | adantr 467 |
. . . . . . . . . . . . . . 15
 

      |
92 | 15 | absge0d 13499 |
. . . . . . . . . . . . . . . 16

      |
93 | 92 | adantr 467 |
. . . . . . . . . . . . . . 15
 

      |
94 | | 0cn 9632 |
. . . . . . . . . . . . . . . . . . . 20
 |
95 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . 21

  |
96 | 95 | cnmetdval 21784 |
. . . . . . . . . . . . . . . . . . . 20
 
   
          |
97 | 15, 94, 96 | sylancl 667 |
. . . . . . . . . . . . . . . . . . 19
   
          |
98 | 15 | subid1d 9972 |
. . . . . . . . . . . . . . . . . . . 20
     |
99 | 98 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . 19
    
        |
100 | 97, 99 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . 18
   
        |
101 | | cnxmet 21786 |
. . . . . . . . . . . . . . . . . . . . 21

      |
102 | | 1rp 11303 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
103 | | rpxr 11306 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
104 | 102, 103 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
 |
105 | | elbl3 21400 |
. . . . . . . . . . . . . . . . . . . . 21
   
                  
  
     |
106 | 101, 104,
105 | mpanl12 687 |
. . . . . . . . . . . . . . . . . . . 20
 
          
  
     |
107 | 94, 15, 106 | sylancr 668 |
. . . . . . . . . . . . . . . . . . 19
          
  
     |
108 | 47, 107 | mpbid 214 |
. . . . . . . . . . . . . . . . . 18
   
    |
109 | 100, 108 | eqbrtrrd 4424 |
. . . . . . . . . . . . . . . . 17
    
  |
110 | | 1re 9639 |
. . . . . . . . . . . . . . . . . 18
 |
111 | | ltle 9719 |
. . . . . . . . . . . . . . . . . 18
     
     
       |
112 | 86, 110, 111 | sylancl 667 |
. . . . . . . . . . . . . . . . 17
     
       |
113 | 109, 112 | mpd 15 |
. . . . . . . . . . . . . . . 16
    
  |
114 | 113 | adantr 467 |
. . . . . . . . . . . . . . 15
 

      |
115 | | simpr 463 |
. . . . . . . . . . . . . . 15
 

  |
116 | | exple1 12329 |
. . . . . . . . . . . . . . 15
          
    

          |
117 | 91, 93, 114, 115, 116 | syl31anc 1270 |
. . . . . . . . . . . . . 14
 

          |
118 | 88, 89, 73, 90, 117 | lemul2ad 10544 |
. . . . . . . . . . . . 13
 

                       
          |
119 | 24, 26 | absmuld 13509 |
. . . . . . . . . . . . . 14
 

                                      |
120 | | absexp 13360 |
. . . . . . . . . . . . . . . 16
 
                   |
121 | 15, 120 | sylan 474 |
. . . . . . . . . . . . . . 15
 

                  |
122 | 121 | oveq2d 6304 |
. . . . . . . . . . . . . 14
 

                                          |
123 | 119, 122 | eqtr2d 2485 |
. . . . . . . . . . . . 13
 

                                      |
124 | 73 | recnd 9666 |
. . . . . . . . . . . . . 14
 

            |
125 | 124 | mulid1d 9657 |
. . . . . . . . . . . . 13
 

                        |
126 | 118, 123,
125 | 3brtr3d 4431 |
. . . . . . . . . . . 12
 

                            |
127 | 19, 126 | sylan2 477 |
. . . . . . . . . . 11
 
   
                  
            |
128 | 18, 83, 74, 127 | fsumle 13852 |
. . . . . . . . . 10
 
                      
    
               |
129 | 80, 84, 75, 85, 128 | letrd 9789 |
. . . . . . . . 9
                        
    
               |
130 | 75 | ltp1d 10534 |
. . . . . . . . 9
 
                                       |
131 | 80, 75, 77, 129, 130 | lelttrd 9790 |
. . . . . . . 8
                                    
          |
132 | 80, 77, 131 | ltled 9780 |
. . . . . . 7
                        
           
          |
133 | 80, 77, 72, 81, 132 | lemul2ad 10544 |
. . . . . 6
                                                               |
134 | 79, 133 | eqbrtrd 4422 |
. . . . 5
           
                                   
           |
135 | | abelthlem7.5 |
. . . . . 6
             
                 |
136 | | 0red 9641 |
. . . . . . . 8
   |
137 | 19, 90 | sylan2 477 |
. . . . . . . . 9
 
   
               |
138 | 18, 74, 137 | fsumge0 13848 |
. . . . . . . 8

    
               |
139 | 136, 75, 77, 138, 130 | lelttrd 9790 |
. . . . . . 7
            
          |
140 | | ltmuldiv 10475 |
. . . . . . 7
       
                          
                                                                            |
141 | 72, 61, 77, 139, 140 | syl112anc 1271 |
. . . . . 6
                                                             |
142 | 135, 141 | mpbird 236 |
. . . . 5
                   
           |
143 | 31, 78, 61, 134, 142 | lelttrd 9790 |
. . . 4
           
                   |
144 | 17, 54 | absmuld 13509 |
. . . . 5
                                                           |
145 | 54 | abscld 13491 |
. . . . . . 7
                         |
146 | 39 | fveq2d 5867 |
. . . . . . . . . 10
                                   |
147 | | eqid 2450 |
. . . . . . . . . 10

                                    |
148 | | fvex 5873 |
. . . . . . . . . 10
                 |
149 | 146, 147,
148 | fvmpt 5946 |
. . . . . . . . 9

                                        |
150 | 36, 149 | syl 17 |
. . . . . . . 8
 
    
                                        |
151 | 44 | abscld 13491 |
. . . . . . . 8
 
    
                  |
152 | | uzid 11170 |
. . . . . . . . . 10
       |
153 | 34, 152 | syl 17 |
. . . . . . . . 9
       |
154 | | oveq2 6296 |
. . . . . . . . . . . 12
                   |
155 | | eqid 2450 |
. . . . . . . . . . . 12

                    |
156 | | ovex 6316 |
. . . . . . . . . . . 12
         |
157 | 154, 155,
156 | fvmpt 5946 |
. . . . . . . . . . 11

                        |
158 | 36, 157 | syl 17 |
. . . . . . . . . 10
 
    
                        |
159 | 36, 88 | syldan 473 |
. . . . . . . . . 10
 
    
          |
160 | 158, 159 | eqeltrd 2528 |
. . . . . . . . 9
 
    
                |
161 | 151 | recnd 9666 |
. . . . . . . . . 10
 
    
                  |
162 | 150, 161 | eqeltrd 2528 |
. . . . . . . . 9
 
    
                        |
163 | 86 | recnd 9666 |
. . . . . . . . . . 11
       |
164 | | absidm 13379 |
. . . . . . . . . . . . 13
               |
165 | 15, 164 | syl 17 |
. . . . . . . . . . . 12
               |
166 | 165, 109 | eqbrtrd 4422 |
. . . . . . . . . . 11
           |
167 | 163, 166,
33, 158 | geolim2 13920 |
. . . . . . . . . 10
                                |
168 | | seqex 12212 |
. . . . . . . . . . 11
              |
169 | | ovex 6316 |
. . . . . . . . . . 11
                 |
170 | 168, 169 | breldm 5038 |
. . . . . . . . . 10
                                           |
171 | 167, 170 | syl 17 |
. . . . . . . . 9
               |
172 | 119, 122 | eqtrd 2484 |
. . . . . . . . . . . 12
 

                                      |
173 | 36, 172 | syldan 473 |
. . . . . . . . . . 11
 
    
                                      |
174 | 36, 73 | syldan 473 |
. . . . . . . . . . . 12
 
    
            |
175 | 61 | adantr 467 |
. . . . . . . . . . . 12
 
    
  |
176 | 86 | adantr 467 |
. . . . . . . . . . . . 13
 
    
      |
177 | 92 | adantr 467 |
. . . . . . . . . . . . 13
 
    
      |
178 | 176, 36, 177 | expge0d 12431 |
. . . . . . . . . . . 12
 
    
          |
179 | | abelthlem7.4 |
. . . . . . . . . . . . . 14
                   |
180 | 37 | fveq2d 5867 |
. . . . . . . . . . . . . . . 16
             
         |
181 | 180 | breq1d 4411 |
. . . . . . . . . . . . . . 15
                         |
182 | 181 | rspccva 3148 |
. . . . . . . . . . . . . 14
                 
                 |
183 | 179, 182 | sylan 474 |
. . . . . . . . . . . . 13
 
    
            |
184 | 174, 175,
183 | ltled 9780 |
. . . . . . . . . . . 12
 
    
            |
185 | 174, 175,
159, 178, 184 | lemul1ad 10543 |
. . . . . . . . . . 11
 
    
                                |
186 | 173, 185 | eqbrtrd 4422 |
. . . . . . . . . 10
 
    
                            |
187 | 150 | fveq2d 5867 |
. . . . . . . . . . 11
 
    
                                                |
188 | | absidm 13379 |
. . . . . . . . . . . 12
                                                   |
189 | 44, 188 | syl 17 |
. . . . . . . . . . 11
 
    
                                      |
190 | 187, 189 | eqtrd 2484 |
. . . . . . . . . 10
 
    
                                            |
191 | 158 | oveq2d 6304 |
. . . . . . . . . 10
 
    
                            |
192 | 186, 190,
191 | 3brtr4d 4432 |
. . . . . . . . 9
 
    
                          
                 |
193 | 32, 153, 160, 162, 171, 61, 192 | cvgcmpce 13871 |
. . . . . . . 8
                       |
194 | 32, 34, 150, 151, 193 | isumrecl 13819 |
. . . . . . 7
 
                       |
195 | | eldifsni 4097 |
. . . . . . . . . . . 12
       |
196 | 8, 195 | syl 17 |
. . . . . . . . . . 11
   |
197 | 196 | necomd 2678 |
. . . . . . . . . 10
   |
198 | | subeq0 9897 |
. . . . . . . . . . . 12
 
       |
199 | 198 | necon3bid 2667 |
. . . . . . . . . . 11
 
       |
200 | 12, 15, 199 | sylancr 668 |
. . . . . . . . . 10
       |
201 | 197, 200 | mpbird 236 |
. . . . . . . . 9
     |
202 | 17, 201 | absrpcld 13503 |
. . . . . . . 8
         |
203 | 71, 202 | rerpdivcld 11366 |
. . . . . . 7
             |
204 | 32, 34, 43, 44, 53 | isumclim2 13812 |
. . . . . . . 8
                                      |
205 | 32, 34, 150, 161, 193 | isumclim2 13812 |
. . . . . . . 8
                                              |
206 | 36, 51 | syldan 473 |
. . . . . . . 8
 
    
                    |
207 | 43 | fveq2d 5867 |
. . . . . . . . 9
 
    
                                        |
208 | 150, 207 | eqtr4d 2487 |
. . . . . . . 8
 
    
                                              |
209 | 32, 204, 205, 34, 206, 208 | iserabs 13868 |
. . . . . . 7
                      
                        |
210 | 86, 33 | reexpcld 12430 |
. . . . . . . . . 10
           |
211 | | difrp 11334 |
. . . . . . . . . . . 12
     
     
         |
212 | 86, 110, 211 | sylancl 667 |
. . . . . . . . . . 11
     
         |
213 | 109, 212 | mpbid 214 |
. . . . . . . . . 10
         |
214 | 210, 213 | rerpdivcld 11366 |
. . . . . . . . 9
                   |
215 | 61, 214 | remulcld 9668 |
. . . . . . . 8
                     |
216 | 154 | oveq2d 6304 |
. . . . . . . . . . . 12
 
                     |
217 | | eqid 2450 |
. . . . . . . . . . . 12

            
           |
218 | | ovex 6316 |
. . . . . . . . . . . 12
           |
219 | 216, 217,
218 | fvmpt 5946 |
. . . . . . . . . . 11

                            |
220 | 36, 219 | syl 17 |
. . . . . . . . . 10
 
    
                            |
221 | 175, 159 | remulcld 9668 |
. . . . . . . . . 10
 
    
            |
222 | 60 | rpcnd 11340 |
. . . . . . . . . . . 12
   |
223 | 160 | recnd 9666 |
. . . . . . . . . . . 12
 
    
                |
224 | 220, 191 | eqtr4d 2487 |
. . . . . . . . . . . 12
 
    
                                  |
225 | 32, 34, 222, 167, 223, 224 | isermulc2 13714 |
. . . . . . . . . . 11
                                    |
226 | | seqex 12212 |
. . . . . . . . . . . 12
                |
227 | | ovex 6316 |
. . . . . . . . . . . 12
                   |
228 | 226, 227 | breldm 5038 |
. . . . . . . . . . 11
   
                                
            |
229 | 225, 228 | syl 17 |
. . . . . . . . . 10
                 |
230 | 32, 34, 150, 151, 220, 221, 186, 193, 229 | isumle 13895 |
. . . . . . . . 9
 
                    
                  |
231 | 221 | recnd 9666 |
. . . . . . . . . 10
 
    
            |
232 | 32, 34, 220, 231, 225 | isumclim 13811 |
. . . . . . . . 9
 
                                   |
233 | 230, 232 | breqtrd 4426 |
. . . . . . . 8
 
                    
                    |
234 | 60, 213 | rpdivcld 11355 |
. . . . . . . . . 10
           |
235 | 234 | rpred 11338 |
. . . . . . . . 9
           |
236 | 210 | recnd 9666 |
. . . . . . . . . . 11
           |
237 | 213 | rpcnd 11340 |
. . . . . . . . . . 11
         |
238 | 213 | rpne0d 11343 |
. . . . . . . . . . 11
         |
239 | 222, 236,
237, 238 | div12d 10416 |
. . . . . . . . . 10
                                       |
240 | | 1red 9655 |
. . . . . . . . . . . 12
   |
241 | 234 | rpge0d 11342 |
. . . . . . . . . . . 12

          |
242 | | exple1 12329 |
. . . . . . . . . . . . 13
          
    

          |
243 | 86, 92, 113, 33, 242 | syl31anc 1270 |
. . . . . . . . . . . 12
           |
244 | 210, 240,
235, 241, 243 | lemul1ad 10543 |
. . . . . . . . . . 11
                               |
245 | 234 | rpcnd 11340 |
. . . . . . . . . . . 12
           |
246 | 245 | mulid2d 9658 |
. . . . . . . . . . 11
                     |
247 | 244, 246 | breqtrd 4426 |
. . . . . . . . . 10
                             |
248 | 239, 247 | eqbrtrd 4422 |
. . . . . . . . 9
                             |
249 | 14 | simprd 465 |
. . . . . . . . . . . . . 14
      
          |
250 | | resubcl 9935 |
. . . . . . . . . . . . . . . . 17
               |
251 | 110, 86, 250 | sylancr 668 |
. . . . . . . . . . . . . . . 16
         |
252 | 3, 251 | remulcld 9668 |
. . . . . . . . . . . . . . 15
           |
253 | 72, 252, 60 | lemul2d 11379 |
. . . . . . . . . . . . . 14
       
               
             |
254 | 249, 253 | mpbid 214 |
. . . . . . . . . . . . 13
          
          |
255 | 3 | recnd 9666 |
. . . . . . . . . . . . . . 15
   |
256 | 222, 255,
237 | mul12d 9839 |
. . . . . . . . . . . . . 14
  
         
          |
257 | 222, 237 | mulcomd 9661 |
. . . . . . . . . . . . . . 15
                   |
258 | 257 | oveq2d 6304 |
. . . . . . . . . . . . . 14
  
                    |
259 | 255, 237,
222 | mul12d 9839 |
. . . . . . . . . . . . . 14
                  
    |
260 | 256, 258,
259 | 3eqtrd 2488 |
. . . . . . . . . . . . 13
  
               
    |
261 | 254, 260 | breqtrd 4426 |
. . . . . . . . . . . 12
                
    |
262 | 251, 71 | remulcld 9668 |
. . . . . . . . . . . . 13
        
    |
263 | 61, 262, 202 | lemuldivd 11384 |
. . . . . . . . . . . 12
         
         
        
            |
264 | 261, 263 | mpbid 214 |
. . . . . . . . . . 11

                    |
265 | 71 | recnd 9666 |
. . . . . . . . . . . 12
     |
266 | 72 | recnd 9666 |
. . . . . . . . . . . 12
         |
267 | 202 | rpne0d 11343 |
. . . . . . . . . . . 12
         |
268 | 237, 265,
266, 267 | divassd 10415 |
. . . . . . . . . . 11
         
                             |
269 | 264, 268 | breqtrd 4426 |
. . . . . . . . . 10

                    |
270 | | posdif 10104 |
. . . . . . . . . . . . 13
     
     
         |
271 | 86, 110, 270 | sylancl 667 |
. . . . . . . . . . . 12
     
         |
272 | 109, 271 | mpbid 214 |
. . . . . . . . . . 11
         |
273 | | ledivmul 10478 |
. . . . . . . . . . 11
                                             
                     |
274 | 61, 203, 251, 272, 273 | syl112anc 1271 |
. . . . . . . . . 10
         
 
       
                     |
275 | 269, 274 | mpbird 236 |
. . . . . . . . 9
                     |
276 | 215, 235,
203, 248, 275 | letrd 9789 |
. . . . . . . 8
                               |
277 | 194, 215,
203, 233, 276 | letrd 9789 |
. . . . . . 7
 
                    
 
          |
278 | 145, 194,
203, 209, 277 | letrd 9789 |
. . . . . 6
                      
 
          |
279 | 145, 71, 202 | lemuldiv2d 11385 |
. . . . . 6
                                 
   
                               |
280 | 278, 279 | mpbird 236 |
. . . . 5
                                   |
281 | 144, 280 | eqbrtrd 4422 |
. . . 4
                               |
282 | 31, 56, 61, 71, 143, 281 | ltleaddd 10231 |
. . 3
            
                                                  |
283 | | 1cnd 9656 |
. . . . 5
   |
284 | 255, 283,
222 | adddird 9665 |
. . . 4
             |
285 | 222 | mulid2d 9658 |
. . . . 5
     |
286 | 285 | oveq2d 6304 |
. . . 4
             |
287 | 265, 222 | addcomd 9832 |
. . . 4
           |
288 | 284, 286,
287 | 3eqtrd 2488 |
. . 3
           |
289 | 282, 288 | breqtrrd 4428 |
. 2
            
                                                  |
290 | 11, 57, 62, 70, 289 | lelttrd 9790 |
1
        
 
    |