Step | Hyp | Ref
| Expression |
1 | | oddpwdc.f |
. . 3
 
        |
2 | | 2nn 10767 |
. . . . . . . 8
 |
3 | 2 | a1i 11 |
. . . . . . 7
 
   |
4 | | simpl 459 |
. . . . . . 7
 
   |
5 | 3, 4 | nnexpcld 12437 |
. . . . . 6
 
       |
6 | | oddpwdc.j |
. . . . . . . 8
   |
7 | | ssrab2 3514 |
. . . . . . . 8
   |
8 | 6, 7 | eqsstri 3462 |
. . . . . . 7
 |
9 | | simpr 463 |
. . . . . . 7
 
   |
10 | 8, 9 | sseldi 3430 |
. . . . . 6
 
   |
11 | 5, 10 | nnmulcld 10657 |
. . . . 5
 
         |
12 | 11 | ancoms 455 |
. . . 4
 
         |
13 | 12 | adantl 468 |
. . 3
            |
14 | | id 22 |
. . . . . . 7
   |
15 | 2 | a1i 11 |
. . . . . . . 8
   |
16 | | nn0ssre 10873 |
. . . . . . . . . . 11
 |
17 | | ltso 9714 |
. . . . . . . . . . 11
 |
18 | | soss 4773 |
. . . . . . . . . . 11

   |
19 | 16, 17, 18 | mp2 9 |
. . . . . . . . . 10
 |
20 | 19 | a1i 11 |
. . . . . . . . 9
   |
21 | | 0zd 10949 |
. . . . . . . . . 10
   |
22 | | ssrab2 3514 |
. . . . . . . . . . 11

      |
23 | 22 | a1i 11 |
. . . . . . . . . 10
 
       |
24 | | nnz 10959 |
. . . . . . . . . . 11
   |
25 | | oveq2 6298 |
. . . . . . . . . . . . . . 15
           |
26 | 25 | breq1d 4412 |
. . . . . . . . . . . . . 14
     
       |
27 | 26 | elrab 3196 |
. . . . . . . . . . . . 13
 
    

       |
28 | | simprl 764 |
. . . . . . . . . . . . . . 15
  
   
 
  |
29 | 28 | nn0red 10926 |
. . . . . . . . . . . . . 14
  
   
 
  |
30 | 2 | a1i 11 |
. . . . . . . . . . . . . . . 16
  
   
 
  |
31 | 30, 28 | nnexpcld 12437 |
. . . . . . . . . . . . . . 15
  
   
 
      |
32 | 31 | nnred 10624 |
. . . . . . . . . . . . . 14
  
   
 
      |
33 | | simpl 459 |
. . . . . . . . . . . . . . 15
  
   
 
  |
34 | 33 | nnred 10624 |
. . . . . . . . . . . . . 14
  
   
 
  |
35 | | 2re 10679 |
. . . . . . . . . . . . . . . 16
 |
36 | 35 | leidi 10148 |
. . . . . . . . . . . . . . . 16
 |
37 | | nexple 28831 |
. . . . . . . . . . . . . . . 16
 
       |
38 | 35, 36, 37 | mp3an23 1356 |
. . . . . . . . . . . . . . 15

      |
39 | 38 | ad2antrl 734 |
. . . . . . . . . . . . . 14
  
   
 
      |
40 | 31 | nnzd 11039 |
. . . . . . . . . . . . . . 15
  
   
 
      |
41 | | simprr 766 |
. . . . . . . . . . . . . . 15
  
   
 
      |
42 | | dvdsle 14350 |
. . . . . . . . . . . . . . . 16
     
         
   |
43 | 42 | imp 431 |
. . . . . . . . . . . . . . 15
            
      |
44 | 40, 33, 41, 43 | syl21anc 1267 |
. . . . . . . . . . . . . 14
  
   
 
      |
45 | 29, 32, 34, 39, 44 | letrd 9792 |
. . . . . . . . . . . . 13
  
   
 
  |
46 | 27, 45 | sylan2b 478 |
. . . . . . . . . . . 12
 
         |
47 | 46 | ralrimiva 2802 |
. . . . . . . . . . 11
      
 
  |
48 | | breq2 4406 |
. . . . . . . . . . . . 13
 
   |
49 | 48 | ralbidv 2827 |
. . . . . . . . . . . 12
  

           
 
   |
50 | 49 | rspcev 3150 |
. . . . . . . . . . 11
   
             
 
  |
51 | 24, 47, 50 | syl2anc 667 |
. . . . . . . . . 10
       
 
  |
52 | | nn0uz 11193 |
. . . . . . . . . . 11
     |
53 | 52 | uzsupss 11256 |
. . . . . . . . . 10
      

      
 
        

 
 
          |
54 | 21, 23, 51, 53 | syl3anc 1268 |
. . . . . . . . 9
        

 
 
          |
55 | 20, 54 | supcl 7972 |
. . . . . . . 8
       
     |
56 | 15, 55 | nnexpcld 12437 |
. . . . . . 7
          
      |
57 | | fzfi 12185 |
. . . . . . . . . . . 12
     |
58 | | 0zd 10949 |
. . . . . . . . . . . . . . 15
 
         |
59 | 24 | adantr 467 |
. . . . . . . . . . . . . . 15
 
         |
60 | 27, 28 | sylan2b 478 |
. . . . . . . . . . . . . . . 16
 
         |
61 | 60 | nn0zd 11038 |
. . . . . . . . . . . . . . 15
 
         |
62 | 60 | nn0ge0d 10928 |
. . . . . . . . . . . . . . 15
 
         |
63 | | elfz4 11793 |
. . . . . . . . . . . . . . 15
  
 
 
      |
64 | 58, 59, 61, 62, 46, 63 | syl32anc 1276 |
. . . . . . . . . . . . . 14
 
             |
65 | 64 | ex 436 |
. . . . . . . . . . . . 13
  
            |
66 | 65 | ssrdv 3438 |
. . . . . . . . . . . 12
 
           |
67 | | ssfi 7792 |
. . . . . . . . . . . 12
          
      
       |
68 | 57, 66, 67 | sylancr 669 |
. . . . . . . . . . 11
 
       |
69 | | 0nn0 10884 |
. . . . . . . . . . . . . 14
 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
   |
71 | | 2cn 10680 |
. . . . . . . . . . . . . . 15
 |
72 | | exp0 12276 |
. . . . . . . . . . . . . . 15
       |
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . . . . . 14
     |
74 | | 1dvds 14317 |
. . . . . . . . . . . . . . 15
   |
75 | 24, 74 | syl 17 |
. . . . . . . . . . . . . 14
   |
76 | 73, 75 | syl5eqbr 4436 |
. . . . . . . . . . . . 13
       |
77 | | oveq2 6298 |
. . . . . . . . . . . . . . 15
           |
78 | 77 | breq1d 4412 |
. . . . . . . . . . . . . 14
     
       |
79 | 78 | elrab 3196 |
. . . . . . . . . . . . 13
 
    

       |
80 | 70, 76, 79 | sylanbrc 670 |
. . . . . . . . . . . 12
     
   |
81 | | ne0i 3737 |
. . . . . . . . . . . 12
 
    

       |
82 | 80, 81 | syl 17 |
. . . . . . . . . . 11
 
       |
83 | | fisupcl 7985 |
. . . . . . . . . . 11
      
 
     
    
 
      
       
   |
84 | 20, 68, 82, 23, 83 | syl13anc 1270 |
. . . . . . . . . 10
       
       
   |
85 | | oveq2 6298 |
. . . . . . . . . . . 12
           |
86 | 85 | breq1d 4412 |
. . . . . . . . . . 11
     
       |
87 | 86 | cbvrabv 3044 |
. . . . . . . . . 10

         
  |
88 | 84, 87 | syl6eleq 2539 |
. . . . . . . . 9
       
       
   |
89 | | oveq2 6298 |
. . . . . . . . . . 11
       
                
      |
90 | 89 | breq1d 4412 |
. . . . . . . . . 10
       
                 
   
   |
91 | 90 | elrab 3196 |
. . . . . . . . 9
   
       
    
       
            
   
   |
92 | 88, 91 | sylib 200 |
. . . . . . . 8
    
                
   
   |
93 | 92 | simprd 465 |
. . . . . . 7
          
   
  |
94 | | nndivdvds 14311 |
. . . . . . . 8
           
               
   
      
            |
95 | 94 | biimpa 487 |
. . . . . . 7
            
          
                   
       |
96 | 14, 56, 93, 95 | syl21anc 1267 |
. . . . . 6
           
       |
97 | | 1nn0 10885 |
. . . . . . . . . . 11
 |
98 | 97 | a1i 11 |
. . . . . . . . . 10
   |
99 | 55, 98 | nn0addcld 10929 |
. . . . . . . . 9
    
          |
100 | 55 | nn0red 10926 |
. . . . . . . . . . . . . 14
       
     |
101 | 100 | ltp1d 10537 |
. . . . . . . . . . . . 13
       
          
      |
102 | 20, 54 | supub 7973 |
. . . . . . . . . . . . 13
         
        
       
          
       |
103 | 101, 102 | mt2d 121 |
. . . . . . . . . . . 12
    
            
   |
104 | 87 | eleq2i 2521 |
. . . . . . . . . . . 12
    
            
    
            
   |
105 | 103, 104 | sylnib 306 |
. . . . . . . . . . 11
    
            
   |
106 | | oveq2 6298 |
. . . . . . . . . . . . 13
        
                  
       |
107 | 106 | breq1d 4412 |
. . . . . . . . . . . 12
        
               
            |
108 | 107 | elrab 3196 |
. . . . . . . . . . 11
    
            
         
   
          
        |
109 | 105, 108 | sylnib 306 |
. . . . . . . . . 10
         
   
          
        |
110 | | imnan 424 |
. . . . . . . . . 10
         
   
          
     
        
   
          
        |
111 | 109, 110 | sylibr 216 |
. . . . . . . . 9
         
   
          
        |
112 | 99, 111 | mpd 15 |
. . . . . . . 8
       
           |
113 | | expp1 12279 |
. . . . . . . . . 10
    
              
                   
       |
114 | 71, 55, 113 | sylancr 669 |
. . . . . . . . 9
       
                   
       |
115 | 114 | breq1d 4412 |
. . . . . . . 8
        
        
          
        |
116 | 112, 115 | mtbid 302 |
. . . . . . 7
       
           |
117 | | nncn 10617 |
. . . . . . . . . . 11
   |
118 | 56 | nncnd 10625 |
. . . . . . . . . . 11
          
      |
119 | 56 | nnne0d 10654 |
. . . . . . . . . . 11
          
      |
120 | 117, 118,
119 | divcan2d 10385 |
. . . . . . . . . 10
           
          
            |
121 | 120 | eqcomd 2457 |
. . . . . . . . 9
           
          
            |
122 | 121 | breq2d 4414 |
. . . . . . . 8
        
               
               
                  
         |
123 | 15 | nnzd 11039 |
. . . . . . . . 9
   |
124 | 96 | nnzd 11039 |
. . . . . . . . 9
           
       |
125 | 56 | nnzd 11039 |
. . . . . . . . 9
          
      |
126 | | dvdscmulr 14331 |
. . . . . . . . 9
            
           
                 
     
           
               
          
         
          
        |
127 | 123, 124,
125, 119, 126 | syl112anc 1272 |
. . . . . . . 8
        
               
                  
     
          
        |
128 | 122, 127 | bitrd 257 |
. . . . . . 7
        
               
            |
129 | 116, 128 | mtbid 302 |
. . . . . 6
           
       |
130 | | breq2 4406 |
. . . . . . . 8
           
     
          
        |
131 | 130 | notbid 296 |
. . . . . . 7
           
     
          
        |
132 | 131, 6 | elrab2 3198 |
. . . . . 6
           
                
               
        |
133 | 96, 129, 132 | sylanbrc 670 |
. . . . 5
           
       |
134 | 133, 55 | jca 535 |
. . . 4
            
       
          |
135 | 134 | adantl 468 |
. . 3
             
       
          |
136 | | simpr 463 |
. . . . . . 7
  
       
        |
137 | 2 | a1i 11 |
. . . . . . . . 9
  
       
  |
138 | | simplr 762 |
. . . . . . . . 9
  
       
  |
139 | 137, 138 | nnexpcld 12437 |
. . . . . . . 8
  
       
      |
140 | 8 | sseli 3428 |
. . . . . . . . 9
   |
141 | 140 | ad2antrr 732 |
. . . . . . . 8
  
       
  |
142 | 139, 141 | nnmulcld 10657 |
. . . . . . 7
  
       
        |
143 | 136, 142 | eqeltrd 2529 |
. . . . . 6
  
       
  |
144 | | simplll 768 |
. . . . . . . . . 10
              
          |
145 | | breq2 4406 |
. . . . . . . . . . . . . 14
 
   |
146 | 145 | notbid 296 |
. . . . . . . . . . . . 13
 
   |
147 | 146, 6 | elrab2 3198 |
. . . . . . . . . . . 12

    |
148 | 147 | simprbi 466 |
. . . . . . . . . . 11
   |
149 | | 2z 10969 |
. . . . . . . . . . . . . 14
 |
150 | 138 | adantr 467 |
. . . . . . . . . . . . . . . 16
              
          |
151 | 150 | nn0zd 11038 |
. . . . . . . . . . . . . . 15
              
          |
152 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . 17
              
       
  |
153 | 143, 54 | syl 17 |
. . . . . . . . . . . . . . . . . 18
  
       
       

 
 
          |
154 | 153 | adantr 467 |
. . . . . . . . . . . . . . . . 17
              
               

 
 
          |
155 | 152, 154 | supcl 7972 |
. . . . . . . . . . . . . . . 16
              
          
         |
156 | 155 | nn0zd 11038 |
. . . . . . . . . . . . . . 15
              
          
         |
157 | | simpr 463 |
. . . . . . . . . . . . . . 15
              
              
     |
158 | | znnsub 10983 |
. . . . . . . . . . . . . . . 16
    
           
              
       |
159 | 158 | biimpa 487 |
. . . . . . . . . . . . . . 15
     
          
               
      |
160 | 151, 156,
157, 159 | syl21anc 1267 |
. . . . . . . . . . . . . 14
              
               
      |
161 | | iddvdsexp 14326 |
. . . . . . . . . . . . . 14
     
               
           |
162 | 149, 160,
161 | sylancr 669 |
. . . . . . . . . . . . 13
              
              
           |
163 | 149 | a1i 11 |
. . . . . . . . . . . . . 14
              
          |
164 | 143, 124 | syl 17 |
. . . . . . . . . . . . . . 15
  
       
      
           |
165 | 164 | adantr 467 |
. . . . . . . . . . . . . 14
              
                  
       |
166 | 160 | nnnn0d 10925 |
. . . . . . . . . . . . . . 15
              
               
      |
167 | | zexpcl 12287 |
. . . . . . . . . . . . . . 15
     
                   
       |
168 | 149, 166,
167 | sylancr 669 |
. . . . . . . . . . . . . 14
              
                  
       |
169 | | dvdsmultr2 14340 |
. . . . . . . . . . . . . 14
            
           
                 
        
           
           
             |
170 | 163, 165,
168, 169 | syl3anc 1268 |
. . . . . . . . . . . . 13
              
               
        
           
           
             |
171 | 162, 170 | mpd 15 |
. . . . . . . . . . . 12
              
                   
           
            |
172 | 141 | adantr 467 |
. . . . . . . . . . . . . . 15
              
          |
173 | 172 | nncnd 10625 |
. . . . . . . . . . . . . 14
              
          |
174 | | 2cnd 10682 |
. . . . . . . . . . . . . . . 16
              
          |
175 | 174, 166 | expcld 12416 |
. . . . . . . . . . . . . . 15
              
                  
       |
176 | 143 | adantr 467 |
. . . . . . . . . . . . . . . . 17
              
          |
177 | 176 | nncnd 10625 |
. . . . . . . . . . . . . . . 16
              
          |
178 | 176, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
              
             
          |
179 | | 2ne0 10702 |
. . . . . . . . . . . . . . . . . 18
 |
180 | 179 | a1i 11 |
. . . . . . . . . . . . . . . . 17
              
          |
181 | 174, 180,
156 | expne0d 12422 |
. . . . . . . . . . . . . . . 16
              
             
          |
182 | 177, 178,
181 | divcld 10383 |
. . . . . . . . . . . . . . 15
              
                  
       |
183 | 175, 182 | mulcld 9663 |
. . . . . . . . . . . . . 14
              
                   
               
        |
184 | 174, 150 | expcld 12416 |
. . . . . . . . . . . . . 14
              
              |
185 | 174, 180,
151 | expne0d 12422 |
. . . . . . . . . . . . . 14
              
              |
186 | 176, 121 | syl 17 |
. . . . . . . . . . . . . . . 16
              
                  
          
            |
187 | | simplr 762 |
. . . . . . . . . . . . . . . 16
              
                |
188 | 150 | nn0cnd 10927 |
. . . . . . . . . . . . . . . . . . . 20
              
          |
189 | 155 | nn0cnd 10927 |
. . . . . . . . . . . . . . . . . . . 20
              
          
         |
190 | 188, 189 | pncan3d 9989 |
. . . . . . . . . . . . . . . . . . 19
              
                
           
     |
191 | 190 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . 18
              
               
               
          |
192 | 174, 166,
150 | expaddd 12418 |
. . . . . . . . . . . . . . . . . 18
              
               
                     
            |
193 | 191, 192 | eqtr3d 2487 |
. . . . . . . . . . . . . . . . 17
              
             
                   
            |
194 | 193 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
              
                  
          
                      
                    
        |
195 | 186, 187,
194 | 3eqtr3d 2493 |
. . . . . . . . . . . . . . 15
              
                          
                    
        |
196 | 184, 175,
182 | mulassd 9666 |
. . . . . . . . . . . . . . 15
              
                        
            
                      
               
             |
197 | 195, 196 | eqtrd 2485 |
. . . . . . . . . . . . . 14
              
                          
               
             |
198 | 173, 183,
184, 185, 197 | mulcanad 10247 |
. . . . . . . . . . . . 13
              
               
               
            |
199 | 182, 175 | mulcomd 9664 |
. . . . . . . . . . . . 13
              
               
                   
             
               
            |
200 | 198, 199 | eqtr4d 2488 |
. . . . . . . . . . . 12
              
                   
           
            |
201 | 171, 200 | breqtrrd 4429 |
. . . . . . . . . . 11
              
          |
202 | 148, 201 | nsyl3 123 |
. . . . . . . . . 10
              
       
  |
203 | 144, 202 | pm2.65da 580 |
. . . . . . . . 9
  
       
  
         |
204 | 141 | nnzd 11039 |
. . . . . . . . . . . 12
  
       
  |
205 | 139 | nnzd 11039 |
. . . . . . . . . . . 12
  
       
      |
206 | 143 | nnzd 11039 |
. . . . . . . . . . . 12
  
       
  |
207 | 139 | nncnd 10625 |
. . . . . . . . . . . . . 14
  
       
      |
208 | 141 | nncnd 10625 |
. . . . . . . . . . . . . 14
  
       
  |
209 | 207, 208 | mulcomd 9664 |
. . . . . . . . . . . . 13
  
       
              |
210 | 136, 209 | eqtr2d 2486 |
. . . . . . . . . . . 12
  
       
        |
211 | | dvds0lem 14313 |
. . . . . . . . . . . 12
      
              |
212 | 204, 205,
206, 210, 211 | syl31anc 1271 |
. . . . . . . . . . 11
  
       
      |
213 | | oveq2 6298 |
. . . . . . . . . . . . 13
           |
214 | 213 | breq1d 4412 |
. . . . . . . . . . . 12
     
       |
215 | 214 | elrab 3196 |
. . . . . . . . . . 11
 
    

       |
216 | 138, 212,
215 | sylanbrc 670 |
. . . . . . . . . 10
  
       
    
   |
217 | 19 | a1i 11 |
. . . . . . . . . . 11
  
       
  |
218 | 217, 153 | supub 7973 |
. . . . . . . . . 10
  
       
     
       
      |
219 | 216, 218 | mpd 15 |
. . . . . . . . 9
  
       
      
     |
220 | 138 | nn0red 10926 |
. . . . . . . . . 10
  
       
  |
221 | 143, 100 | syl 17 |
. . . . . . . . . 10
  
       
      
     |
222 | 220, 221 | lttri3d 9775 |
. . . . . . . . 9
  
       
   
      
   
         
           |
223 | 203, 219,
222 | mpbir2and 933 |
. . . . . . . 8
  
       
  
         |
224 | | simplr 762 |
. . . . . . . . . . 11
           
      
   
        |
225 | 143 | adantr 467 |
. . . . . . . . . . . . 13
           
      
   
  |
226 | 225 | nncnd 10625 |
. . . . . . . . . . . 12
           
      
   
  |
227 | 141 | adantr 467 |
. . . . . . . . . . . . 13
           
      
   
  |
228 | 227 | nncnd 10625 |
. . . . . . . . . . . 12
           
      
   
  |
229 | | nnexpcl 12285 |
. . . . . . . . . . . . . . . 16
 
       |
230 | 2, 229 | mpan 676 |
. . . . . . . . . . . . . . 15

      |
231 | 230 | nncnd 10625 |
. . . . . . . . . . . . . 14

      |
232 | 230 | nnne0d 10654 |
. . . . . . . . . . . . . 14

      |
233 | 231, 232 | jca 535 |
. . . . . . . . . . . . 13

            |
234 | 233 | ad3antlr 737 |
. . . . . . . . . . . 12
           
      
   
            |
235 | | divmul2 10274 |
. . . . . . . . . . . 12
 
          
      
         |
236 | 226, 228,
234, 235 | syl3anc 1268 |
. . . . . . . . . . 11
           
      
   
      
         |
237 | 224, 236 | mpbird 236 |
. . . . . . . . . 10
           
      
   
        |
238 | | simpr 463 |
. . . . . . . . . . . 12
           
      
   
  
         |
239 | 238 | oveq2d 6306 |
. . . . . . . . . . 11
           
      
   
             
      |
240 | 239 | oveq2d 6306 |
. . . . . . . . . 10
           
      
   
                
       |
241 | 237, 240 | eqtr3d 2487 |
. . . . . . . . 9
           
      
   
          
       |
242 | 241 | ex 436 |
. . . . . . . 8
  
       
   
      
      
            |
243 | 223, 242 | jcai 539 |
. . . . . . 7
  
       
   
      
      
            |
244 | 243 | ancomd 453 |
. . . . . 6
  
       
           
       
          |
245 | 143, 244 | jca 535 |
. . . . 5
  
       
            
       
           |
246 | | simprl 764 |
. . . . . . 7
  
          
       
        
          
       |
247 | 133 | adantr 467 |
. . . . . . 7
  
          
       
        
      
           |
248 | 246, 247 | eqeltrd 2529 |
. . . . . 6
  
          
       
        
  |
249 | | simprr 766 |
. . . . . . 7
  
          
       
        
  
         |
250 | 55 | adantr 467 |
. . . . . . 7
  
          
       
        
      
     |
251 | 249, 250 | eqeltrd 2529 |
. . . . . 6
  
          
       
        
  |
252 | 121 | adantr 467 |
. . . . . . 7
  
          
       
        
      
                  
        |
253 | 249 | oveq2d 6306 |
. . . . . . . 8
  
          
       
        
             
      |
254 | 253, 246 | oveq12d 6308 |
. . . . . . 7
  
          
       
        
            
                  
        |
255 | 252, 254 | eqtr4d 2488 |
. . . . . 6
  
          
       
        
        |
256 | 248, 251,
255 | jca31 537 |
. . . . 5
  
          
       
        
 

         |
257 | 245, 256 | impbii 191 |
. . . 4
  
                    
       
           |
258 | 257 | a1i 11 |
. . 3
          
            
       
            |
259 | 1, 13, 135, 258 | f1od2 28309 |
. 2
        |
260 | 259 | trud 1453 |
1
       |