Step | Hyp | Ref
| Expression |
1 | | perfectALTVlem.2 |
. . . 4
   |
2 | | 1re 9660 |
. . . . . 6
 |
3 | 2 | a1i 11 |
. . . . 5
   |
4 | | perfectALTVlem.1 |
. . . . . . . 8
   |
5 | | perfectALTVlem.3 |
. . . . . . . 8
 Odd  |
6 | | perfectALTVlem.4 |
. . . . . . . 8
                   |
7 | 4, 1, 5, 6 | perfectALTVlem1 38988 |
. . . . . . 7
                
    
       |
8 | 7 | simp3d 1044 |
. . . . . 6
      
      |
9 | 8 | nnred 10646 |
. . . . 5
      
      |
10 | 1 | nnred 10646 |
. . . . 5
   |
11 | 8 | nnge1d 10674 |
. . . . 5

            |
12 | | 2cn 10702 |
. . . . . . . . . . 11
 |
13 | | exp1 12316 |
. . . . . . . . . . 11
       |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . 10
     |
15 | | df-2 10690 |
. . . . . . . . . 10
   |
16 | 14, 15 | eqtri 2493 |
. . . . . . . . 9
       |
17 | | 2re 10701 |
. . . . . . . . . . 11
 |
18 | 17 | a1i 11 |
. . . . . . . . . 10
   |
19 | | 1zzd 10992 |
. . . . . . . . . 10
   |
20 | 4 | peano2nnd 10648 |
. . . . . . . . . . 11
     |
21 | 20 | nnzd 11062 |
. . . . . . . . . 10
     |
22 | | 1lt2 10799 |
. . . . . . . . . . 11
 |
23 | 22 | a1i 11 |
. . . . . . . . . 10
   |
24 | 4 | nnrpd 11362 |
. . . . . . . . . . . 12
   |
25 | | ltaddrp 11359 |
. . . . . . . . . . . 12
 

    |
26 | 2, 24, 25 | sylancr 676 |
. . . . . . . . . . 11
     |
27 | | ax-1cn 9615 |
. . . . . . . . . . . 12
 |
28 | 4 | nncnd 10647 |
. . . . . . . . . . . 12
   |
29 | | addcom 9837 |
. . . . . . . . . . . 12
 
       |
30 | 27, 28, 29 | sylancr 676 |
. . . . . . . . . . 11
       |
31 | 26, 30 | breqtrd 4420 |
. . . . . . . . . 10
     |
32 | | ltexp2a 12362 |
. . . . . . . . . 10
   
                   |
33 | 18, 19, 21, 23, 31, 32 | syl32anc 1300 |
. . . . . . . . 9
             |
34 | 16, 33 | syl5eqbrr 4430 |
. . . . . . . 8
           |
35 | 7 | simp1d 1042 |
. . . . . . . . . 10
    
    |
36 | 35 | nnred 10646 |
. . . . . . . . 9
    
    |
37 | 3, 3, 36 | ltaddsubd 10234 |
. . . . . . . 8
                     |
38 | 34, 37 | mpbid 215 |
. . . . . . 7
           |
39 | | 1rp 11329 |
. . . . . . . . 9
 |
40 | 39 | a1i 11 |
. . . . . . . 8
   |
41 | | peano2rem 9961 |
. . . . . . . . . . 11
           
     |
42 | 36, 41 | syl 17 |
. . . . . . . . . 10
           |
43 | | expgt1 12348 |
. . . . . . . . . . . 12
  
 
        |
44 | 18, 20, 23, 43 | syl3anc 1292 |
. . . . . . . . . . 11
         |
45 | | posdif 10128 |
. . . . . . . . . . . 12
     
       
      
      |
46 | 2, 36, 45 | sylancr 676 |
. . . . . . . . . . 11
                   |
47 | 44, 46 | mpbid 215 |
. . . . . . . . . 10
           |
48 | 42, 47 | jca 541 |
. . . . . . . . 9
                     |
49 | | elrp 11327 |
. . . . . . . . 9
     
  
                    |
50 | 48, 49 | sylibr 217 |
. . . . . . . 8
           |
51 | | nnrp 11334 |
. . . . . . . . 9
   |
52 | 1, 51 | syl 17 |
. . . . . . . 8
   |
53 | 40, 50, 52 | ltdiv2d 11387 |
. . . . . . 7
      
        
         |
54 | 38, 53 | mpbid 215 |
. . . . . 6
      
        |
55 | 1 | nncnd 10647 |
. . . . . . 7
   |
56 | 55 | div1d 10397 |
. . . . . 6
     |
57 | 54, 56 | breqtrd 4420 |
. . . . 5
      
      |
58 | 3, 9, 10, 11, 57 | lelttrd 9810 |
. . . 4
   |
59 | | eluz2b2 11254 |
. . . 4
         |
60 | 1, 58, 59 | sylanbrc 677 |
. . 3
       |
61 | | fzfid 12224 |
. . . . . . . . . . . 12
       |
62 | | sgmss 24112 |
. . . . . . . . . . . . 13
  
      |
63 | 1, 62 | syl 17 |
. . . . . . . . . . . 12
 
       |
64 | | ssfi 7810 |
. . . . . . . . . . . 12
              
  |
65 | 61, 63, 64 | syl2anc 673 |
. . . . . . . . . . 11
 
   |
66 | 65 | ad2antrr 740 |
. . . . . . . . . 10
                     
  |
67 | | ssrab2 3500 |
. . . . . . . . . . . . 13
 
 |
68 | 67 | a1i 11 |
. . . . . . . . . . . 12
                     
  |
69 | 68 | sselda 3418 |
. . . . . . . . . . 11
    
                
 
  |
70 | 69 | nnred 10646 |
. . . . . . . . . 10
    
                
 
  |
71 | 69 | nnnn0d 10949 |
. . . . . . . . . . 11
    
                
 
  |
72 | 71 | nn0ge0d 10952 |
. . . . . . . . . 10
    
                
 
  |
73 | | df-tp 3964 |
. . . . . . . . . . . 12
             
       
          |
74 | | prssi 4119 |
. . . . . . . . . . . . . . 15
       
   
                |
75 | 8, 1, 74 | syl2anc 673 |
. . . . . . . . . . . . . 14
                |
76 | 75 | ad2antrr 740 |
. . . . . . . . . . . . 13
                                   |
77 | | simplrl 778 |
. . . . . . . . . . . . . 14
                      |
78 | 77 | snssd 4108 |
. . . . . . . . . . . . 13
                        |
79 | 76, 78 | unssd 3601 |
. . . . . . . . . . . 12
                                 
     |
80 | 73, 79 | syl5eqss 3462 |
. . . . . . . . . . 11
                                    |
81 | | eltpi 4007 |
. . . . . . . . . . . . 13
                             |
82 | 7 | simp2d 1043 |
. . . . . . . . . . . . . . . . . . 19
           |
83 | 82 | nnzd 11062 |
. . . . . . . . . . . . . . . . . 18
           |
84 | 8 | nnzd 11062 |
. . . . . . . . . . . . . . . . . 18
      
      |
85 | | dvdsmul2 14402 |
. . . . . . . . . . . . . . . . . 18
          
    
                                     |
86 | 83, 84, 85 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
      
         
                |
87 | 82 | nncnd 10647 |
. . . . . . . . . . . . . . . . . 18
           |
88 | 82 | nnne0d 10676 |
. . . . . . . . . . . . . . . . . 18
           |
89 | 55, 87, 88 | divcan2d 10407 |
. . . . . . . . . . . . . . . . 17
                       |
90 | 86, 89 | breqtrd 4420 |
. . . . . . . . . . . . . . . 16
      
      |
91 | | breq1 4398 |
. . . . . . . . . . . . . . . 16
           
             |
92 | 90, 91 | syl5ibrcom 230 |
. . . . . . . . . . . . . . 15
               |
93 | 92 | ad2antrr 740 |
. . . . . . . . . . . . . 14
                                  |
94 | 1 | nnzd 11062 |
. . . . . . . . . . . . . . . . 17
   |
95 | | iddvds 14393 |
. . . . . . . . . . . . . . . . 17
   |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . 16
   |
97 | | breq1 4398 |
. . . . . . . . . . . . . . . 16
 
   |
98 | 96, 97 | syl5ibrcom 230 |
. . . . . . . . . . . . . . 15
     |
99 | 98 | ad2antrr 740 |
. . . . . . . . . . . . . 14
                        |
100 | | simplrr 779 |
. . . . . . . . . . . . . . 15
                      |
101 | | breq1 4398 |
. . . . . . . . . . . . . . 15
 
   |
102 | 100, 101 | syl5ibrcom 230 |
. . . . . . . . . . . . . 14
                        |
103 | 93, 99, 102 | 3jaod 1358 |
. . . . . . . . . . . . 13
                                
   |
104 | 81, 103 | syl5 32 |
. . . . . . . . . . . 12
                                      |
105 | 104 | imp 436 |
. . . . . . . . . . 11
    
                                 |
106 | 80, 105 | ssrabdv 3494 |
. . . . . . . . . 10
                                      |
107 | 66, 70, 72, 106 | fsumless 13933 |
. . . . . . . . 9
                                          |
108 | | simpr 468 |
. . . . . . . . . . . 12
                   
               |
109 | | disjsn 4023 |
. . . . . . . . . . . 12
                 
               |
110 | 108, 109 | sylibr 217 |
. . . . . . . . . . 11
                                       |
111 | 73 | a1i 11 |
. . . . . . . . . . 11
                                 
       
           |
112 | | tpfi 7865 |
. . . . . . . . . . . 12
             
 |
113 | 112 | a1i 11 |
. . . . . . . . . . 11
                                 
  |
114 | 80 | sselda 3418 |
. . . . . . . . . . . 12
    
                                 |
115 | 114 | nncnd 10647 |
. . . . . . . . . . 11
    
                                 |
116 | 110, 111,
113, 115 | fsumsplit 13883 |
. . . . . . . . . 10
                                            
              |
117 | 8 | nncnd 10647 |
. . . . . . . . . . . . . . 15
      
      |
118 | | id 22 |
. . . . . . . . . . . . . . . 16
                       |
119 | 118 | sumsn 13884 |
. . . . . . . . . . . . . . 15
       
    
    
            
           
      |
120 | 8, 117, 119 | syl2anc 673 |
. . . . . . . . . . . . . 14
        
           
      |
121 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
122 | 121 | sumsn 13884 |
. . . . . . . . . . . . . . 15
 
       |
123 | 1, 55, 122 | syl2anc 673 |
. . . . . . . . . . . . . 14
       |
124 | 120, 123 | oveq12d 6326 |
. . . . . . . . . . . . 13
         
                         |
125 | | incom 3616 |
. . . . . . . . . . . . . . 15
         
                       |
126 | 9, 57 | gtned 9787 |
. . . . . . . . . . . . . . . 16
             |
127 | | disjsn2 4024 |
. . . . . . . . . . . . . . . 16
                    
        |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . 15
                   |
129 | 125, 128 | syl5eqr 2519 |
. . . . . . . . . . . . . 14
                   |
130 | | df-pr 3962 |
. . . . . . . . . . . . . . 15
                              |
131 | 130 | a1i 11 |
. . . . . . . . . . . . . 14
             
       
          |
132 | | prfi 7864 |
. . . . . . . . . . . . . . 15
              |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . 14
             
  |
134 | 75 | sselda 3418 |
. . . . . . . . . . . . . . 15
 
      
      
  |
135 | 134 | nncnd 10647 |
. . . . . . . . . . . . . 14
 
      
      
  |
136 | 129, 131,
133, 135 | fsumsplit 13883 |
. . . . . . . . . . . . 13
        
        
                    |
137 | 87, 55 | mulcld 9681 |
. . . . . . . . . . . . . . 15
             |
138 | 55, 137, 87, 88 | divdird 10443 |
. . . . . . . . . . . . . 14
                  
                     
                |
139 | 35 | nncnd 10647 |
. . . . . . . . . . . . . . . . . . . 20
    
    |
140 | 27 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
   |
141 | 139, 140,
55 | subdird 10096 |
. . . . . . . . . . . . . . . . . . 19
                
        |
142 | 55 | mulid2d 9679 |
. . . . . . . . . . . . . . . . . . . 20
     |
143 | 142 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . 19
                  
      |
144 | 141, 143 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . 18
                
      |
145 | 144 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
                           |
146 | 139, 55 | mulcld 9681 |
. . . . . . . . . . . . . . . . . 18
           |
147 | 55, 146 | pncan3d 10008 |
. . . . . . . . . . . . . . . . 17
                       |
148 | 145, 147 | eqtrd 2505 |
. . . . . . . . . . . . . . . 16
                       |
149 | 148 | oveq1d 6323 |
. . . . . . . . . . . . . . 15
                  
         
              |
150 | 139, 55, 87, 88 | divassd 10440 |
. . . . . . . . . . . . . . 15
              
                        |
151 | 149, 150 | eqtrd 2505 |
. . . . . . . . . . . . . 14
                  
                        |
152 | 55, 87, 88 | divcan3d 10410 |
. . . . . . . . . . . . . . 15
                
      |
153 | 152 | oveq2d 6324 |
. . . . . . . . . . . . . 14
                                               |
154 | 138, 151,
153 | 3eqtr3d 2513 |
. . . . . . . . . . . . 13
                                 |
155 | 124, 136,
154 | 3eqtr4d 2515 |
. . . . . . . . . . . 12
        
                           |
156 | 155 | ad2antrr 740 |
. . . . . . . . . . 11
                                       
               |
157 | 77 | nncnd 10647 |
. . . . . . . . . . . 12
                      |
158 | | id 22 |
. . . . . . . . . . . . 13
   |
159 | 158 | sumsn 13884 |
. . . . . . . . . . . 12
 
       |
160 | 157, 157,
159 | syl2anc 673 |
. . . . . . . . . . 11
                          |
161 | 156, 160 | oveq12d 6326 |
. . . . . . . . . 10
                                                               |
162 | 116, 161 | eqtrd 2505 |
. . . . . . . . 9
                                                 
        |
163 | 4 | nnnn0d 10949 |
. . . . . . . . . . . . . . . . 17
   |
164 | | expp1 12317 |
. . . . . . . . . . . . . . . . 17
 
    
          |
165 | 12, 163, 164 | sylancr 676 |
. . . . . . . . . . . . . . . 16
    
          |
166 | | 2nn 10790 |
. . . . . . . . . . . . . . . . . . 19
 |
167 | | nnexpcl 12323 |
. . . . . . . . . . . . . . . . . . 19
 
       |
168 | 166, 163,
167 | sylancr 676 |
. . . . . . . . . . . . . . . . . 18
       |
169 | 168 | nncnd 10647 |
. . . . . . . . . . . . . . . . 17
       |
170 | | mulcom 9643 |
. . . . . . . . . . . . . . . . 17
     
               |
171 | 169, 12, 170 | sylancl 675 |
. . . . . . . . . . . . . . . 16
               |
172 | 165, 171 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
    
          |
173 | 172 | oveq1d 6323 |
. . . . . . . . . . . . . 14
                   |
174 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
175 | 174, 169,
55 | mulassd 9684 |
. . . . . . . . . . . . . 14
                   |
176 | | isodd7 38940 |
. . . . . . . . . . . . . . . . . . 19
 Odd       |
177 | | simpr 468 |
. . . . . . . . . . . . . . . . . . 19
         |
178 | 176, 177 | sylbi 200 |
. . . . . . . . . . . . . . . . . 18
 Odd     |
179 | 5, 178 | syl 17 |
. . . . . . . . . . . . . . . . 17
     |
180 | | 2z 10993 |
. . . . . . . . . . . . . . . . . . 19
 |
181 | 180 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
   |
182 | | rpexp1i 14752 |
. . . . . . . . . . . . . . . . . 18
 
             |
183 | 181, 94, 163, 182 | syl3anc 1292 |
. . . . . . . . . . . . . . . . 17
             |
184 | 179, 183 | mpd 15 |
. . . . . . . . . . . . . . . 16
         |
185 | | sgmmul 24208 |
. . . . . . . . . . . . . . . 16
              
                    |
186 | 140, 168,
1, 184, 185 | syl13anc 1294 |
. . . . . . . . . . . . . . 15
                     |
187 | | pncan 9901 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
188 | 28, 27, 187 | sylancl 675 |
. . . . . . . . . . . . . . . . . . 19
       |
189 | 188 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
               |
190 | 189 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
                   |
191 | | 1sgm2ppw 24207 |
. . . . . . . . . . . . . . . . . 18
                       |
192 | 20, 191 | syl 17 |
. . . . . . . . . . . . . . . . 17
                     |
193 | 190, 192 | eqtr3d 2507 |
. . . . . . . . . . . . . . . 16
                 |
194 | 193 | oveq1d 6323 |
. . . . . . . . . . . . . . 15
                         |
195 | 186, 6, 194 | 3eqtr3d 2513 |
. . . . . . . . . . . . . 14
              
        |
196 | 173, 175,
195 | 3eqtrd 2509 |
. . . . . . . . . . . . 13
              
        |
197 | 196 | oveq1d 6323 |
. . . . . . . . . . . 12
              
                            |
198 | | 1nn0 10909 |
. . . . . . . . . . . . . . 15
 |
199 | | sgmnncl 24153 |
. . . . . . . . . . . . . . 15
 
     |
200 | 198, 1, 199 | sylancr 676 |
. . . . . . . . . . . . . 14
     |
201 | 200 | nncnd 10647 |
. . . . . . . . . . . . 13
     |
202 | 201, 87, 88 | divcan3d 10410 |
. . . . . . . . . . . 12
                           |
203 | 197, 150,
202 | 3eqtr3d 2513 |
. . . . . . . . . . 11
                       |
204 | | sgmval 24148 |
. . . . . . . . . . . 12
 
           |
205 | 27, 1, 204 | sylancr 676 |
. . . . . . . . . . 11
           |
206 | | simpr 468 |
. . . . . . . . . . . . . . 15
 
       |
207 | 67, 206 | sseldi 3416 |
. . . . . . . . . . . . . 14
 
     |
208 | 207 | nncnd 10647 |
. . . . . . . . . . . . 13
 
     |
209 | 208 | cxp1d 23730 |
. . . . . . . . . . . 12
 
        |
210 | 209 | sumeq2dv 13846 |
. . . . . . . . . . 11
        
    |
211 | 203, 205,
210 | 3eqtrrd 2510 |
. . . . . . . . . 10
                 
       |
212 | 211 | ad2antrr 740 |
. . . . . . . . 9
                     
                      |
213 | 107, 162,
212 | 3brtr3d 4425 |
. . . . . . . 8
                                                            |
214 | 36, 9 | remulcld 9689 |
. . . . . . . . . . 11
                     |
215 | 214 | ad2antrr 740 |
. . . . . . . . . 10
                        
               |
216 | 77 | nnrpd 11362 |
. . . . . . . . . 10
                      |
217 | 215, 216 | ltaddrpd 11394 |
. . . . . . . . 9
                        
                                   |
218 | 77 | nnred 10646 |
. . . . . . . . . . 11
                      |
219 | 215, 218 | readdcld 9688 |
. . . . . . . . . 10
                                          |
220 | 215, 219 | ltnled 9799 |
. . . . . . . . 9
                                                          
                                         |
221 | 217, 220 | mpbid 215 |
. . . . . . . 8
                                 
     
                    |
222 | 213, 221 | condan 811 |
. . . . . . 7
 
  
               |
223 | | elpri 3976 |
. . . . . . 7
                            |
224 | 222, 223 | syl 17 |
. . . . . 6
 
                 |
225 | 224 | expr 626 |
. . . . 5
 

                |
226 | 225 | ralrimiva 2809 |
. . . 4
  
               |
227 | 3, 58 | gtned 9787 |
. . . . . . . . . 10
   |
228 | 227 | necomd 2698 |
. . . . . . . . 9
   |
229 | | 1nn 10642 |
. . . . . . . . . . . . 13
 |
230 | 229 | a1i 11 |
. . . . . . . . . . . 12
   |
231 | | 1dvds 14394 |
. . . . . . . . . . . . 13
   |
232 | 94, 231 | syl 17 |
. . . . . . . . . . . 12
   |
233 | | breq1 4398 |
. . . . . . . . . . . . . 14
 
   |
234 | | eqeq1 2475 |
. . . . . . . . . . . . . . 15
           

    
       |
235 | | eqeq1 2475 |
. . . . . . . . . . . . . . 15
 
   |
236 | 234, 235 | orbi12d 724 |
. . . . . . . . . . . . . 14
                    
        |
237 | 233, 236 | imbi12d 327 |
. . . . . . . . . . . . 13
               
                 |
238 | 237 | rspcv 3132 |
. . . . . . . . . . . 12
  

             
                |
239 | 230, 226,
232, 238 | syl3c 62 |
. . . . . . . . . . 11
               |
240 | 239 | ord 384 |
. . . . . . . . . 10
       
   
   |
241 | 240 | necon1ad 2660 |
. . . . . . . . 9
               |
242 | 228, 241 | mpd 15 |
. . . . . . . 8
             |
243 | 242 | eqeq2d 2481 |
. . . . . . 7
               |
244 | 243 | orbi1d 717 |
. . . . . 6
   
               |
245 | 244 | imbi2d 323 |
. . . . 5
     

                |
246 | 245 | ralbidv 2829 |
. . . 4
      
        
         |
247 | 226, 246 | mpbird 240 |
. . 3
  
     |
248 | | isprm2 14711 |
. . 3

      
      |
249 | 60, 247, 248 | sylanbrc 677 |
. 2
   |
250 | 214 | ltp1d 10559 |
. . . 4
                                         |
251 | | peano2re 9824 |
. . . . . 6
     
                                   |
252 | 214, 251 | syl 17 |
. . . . 5
              
        |
253 | 214, 252 | ltnled 9799 |
. . . 4
              
                        
                                         |
254 | 250, 253 | mpbid 215 |
. . 3
                         
               |
255 | 207 | nnred 10646 |
. . . . . . . 8
 
     |
256 | 207 | nnnn0d 10949 |
. . . . . . . . 9
 
     |
257 | 256 | nn0ge0d 10952 |
. . . . . . . 8
 
     |
258 | | df-tp 3964 |
. . . . . . . . . 10
                     
          |
259 | | snssi 4107 |
. . . . . . . . . . . 12
  
  |
260 | 229, 259 | mp1i 13 |
. . . . . . . . . . 11
     |
261 | 75, 260 | unssd 3601 |
. . . . . . . . . 10
                    |
262 | 258, 261 | syl5eqss 3462 |
. . . . . . . . 9
                 |
263 | | eltpi 4007 |
. . . . . . . . . . 11
                     
       |
264 | | breq1 4398 |
. . . . . . . . . . . . 13
 
   |
265 | 232, 264 | syl5ibrcom 230 |
. . . . . . . . . . . 12
     |
266 | 92, 98, 265 | 3jaod 1358 |
. . . . . . . . . . 11
        
        |
267 | 263, 266 | syl5 32 |
. . . . . . . . . 10
        
          |
268 | 267 | imp 436 |
. . . . . . . . 9
 
      
          |
269 | 262, 268 | ssrabdv 3494 |
. . . . . . . 8
                   |
270 | 65, 255, 257, 269 | fsumless 13933 |
. . . . . . 7
        
              |
271 | 270 | adantr 472 |
. . . . . 6
 
                               |
272 | 55, 87, 88 | diveq1ad 10414 |
. . . . . . . . . . . . 13
                       |
273 | 272 | necon3bid 2687 |
. . . . . . . . . . . 12
                       |
274 | 273 | biimpar 493 |
. . . . . . . . . . 11
 
                     |
275 | 274 | necomd 2698 |
. . . . . . . . . 10
 
              
      |
276 | 228 | adantr 472 |
. . . . . . . . . 10
 
           |
277 | 275, 276 | nelprd 3981 |
. . . . . . . . 9
 
        
               |
278 | | disjsn 4023 |
. . . . . . . . 9
                 
               |
279 | 277, 278 | sylibr 217 |
. . . . . . . 8
 
                            |
280 | 258 | a1i 11 |
. . . . . . . 8
 
                              
           |
281 | | tpfi 7865 |
. . . . . . . . 9
               |
282 | 281 | a1i 11 |
. . . . . . . 8
 
                         |
283 | 262 | adantr 472 |
. . . . . . . . . 10
 
                      
  |
284 | 283 | sselda 3418 |
. . . . . . . . 9
                             |
285 | 284 | nncnd 10647 |
. . . . . . . 8
                             |
286 | 279, 280,
282, 285 | fsumsplit 13883 |
. . . . . . 7
 
                                         
      |
287 | | id 22 |
. . . . . . . . . . 11
   |
288 | 287 | sumsn 13884 |
. . . . . . . . . 10
 
       |
289 | 140, 27, 288 | sylancl 675 |
. . . . . . . . 9
       |
290 | 155, 289 | oveq12d 6326 |
. . . . . . . 8
         
                 
                |
291 | 290 | adantr 472 |
. . . . . . 7
 
                                                    |
292 | 286, 291 | eqtrd 2505 |
. . . . . 6
 
                                               |
293 | 211 | adantr 472 |
. . . . . 6
 
          
                      |
294 | 271, 292,
293 | 3brtr3d 4425 |
. . . . 5
 
                                                 |
295 | 294 | ex 441 |
. . . 4
      
                           
                |
296 | 295 | necon1bd 2661 |
. . 3
       
                                    
      |
297 | 254, 296 | mpd 15 |
. 2
           |
298 | 249, 297 | jca 541 |
1
             |