Step | Hyp | Ref
| Expression |
1 | | etransclem24.d |
. . . . . . . 8
       |
2 | | etransclem24.c |
. . . . . . . . 9
      
                  |
3 | | etransclem24.i |
. . . . . . . . 9
   |
4 | 2, 3 | etransclem12 38121 |
. . . . . . . 8
                
            |
5 | 1, 4 | eleqtrd 2533 |
. . . . . . 7
            
            |
6 | | fveq1 5869 |
. . . . . . . . . 10
           |
7 | 6 | sumeq2ad 37654 |
. . . . . . . . 9
           
           |
8 | 7 | eqeq1d 2455 |
. . . . . . . 8
           
             |
9 | 8 | elrab 3198 |
. . . . . . 7
                                               |
10 | 5, 9 | sylib 200 |
. . . . . 6
      
                  |
11 | 10 | simprd 465 |
. . . . 5
             |
12 | 11 | ad2antrr 733 |
. . . 4
                                 |
13 | | ralnex 2836 |
. . . . 5
 
       
            |
14 | | etransclem24.m |
. . . . . . . . . . 11
   |
15 | | nn0uz 11200 |
. . . . . . . . . . 11
     |
16 | 14, 15 | syl6eleq 2541 |
. . . . . . . . . 10
       |
17 | 16 | ad2antrr 733 |
. . . . . . . . 9
                          |
18 | | fzsscn 37541 |
. . . . . . . . . . 11
     |
19 | | ssrab2 3516 |
. . . . . . . . . . . . . . 15
           
                     |
20 | 4, 19 | syl6eqss 3484 |
. . . . . . . . . . . . . 14
    
            |
21 | 20, 1 | sseldd 3435 |
. . . . . . . . . . . . 13
             |
22 | | elmapi 7498 |
. . . . . . . . . . . . 13
                         |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
               |
24 | 23 | ffvelrnda 6027 |
. . . . . . . . . . 11
 
               |
25 | 18, 24 | sseldi 3432 |
. . . . . . . . . 10
 
           |
26 | 25 | adant423 37377 |
. . . . . . . . 9
                         
      |
27 | | fveq2 5870 |
. . . . . . . . 9
           |
28 | 17, 26, 27 | fsum1p 13826 |
. . . . . . . 8
                                                  |
29 | | simplr 763 |
. . . . . . . . 9
                            |
30 | | 0p1e1 10728 |
. . . . . . . . . . . . . 14
   |
31 | 30 | oveq1i 6305 |
. . . . . . . . . . . . 13
           |
32 | 31 | sumeq1i 13776 |
. . . . . . . . . . . 12
            
          |
33 | 32 | a1i 11 |
. . . . . . . . . . 11
 
                      
           |
34 | | fveq2 5870 |
. . . . . . . . . . . . . . . . 17
           |
35 | 34 | eleq1d 2515 |
. . . . . . . . . . . . . . . 16
     
       |
36 | 35 | notbid 296 |
. . . . . . . . . . . . . . 15
     
       |
37 | 36 | rspccva 3151 |
. . . . . . . . . . . . . 14
               
      |
38 | 37 | adantll 721 |
. . . . . . . . . . . . 13
   
             
      |
39 | | fzssnn0 37549 |
. . . . . . . . . . . . . . . 16
     |
40 | | fz1ssfz0 37538 |
. . . . . . . . . . . . . . . . . 18
         |
41 | 40 | sseli 3430 |
. . . . . . . . . . . . . . . . 17
           |
42 | 41, 24 | sylan2 477 |
. . . . . . . . . . . . . . . 16
 
               |
43 | 39, 42 | sseldi 3432 |
. . . . . . . . . . . . . . 15
 
           |
44 | | elnn0 10878 |
. . . . . . . . . . . . . . 15
    
            |
45 | 43, 44 | sylib 200 |
. . . . . . . . . . . . . 14
 
                 |
46 | 45 | adantlr 722 |
. . . . . . . . . . . . 13
   
             
            |
47 | | orel1 384 |
. . . . . . . . . . . . 13
                       |
48 | 38, 46, 47 | sylc 62 |
. . . . . . . . . . . 12
   
             
      |
49 | 48 | sumeq2dv 13781 |
. . . . . . . . . . 11
 
                    
       |
50 | | fzfi 12192 |
. . . . . . . . . . . . 13
     |
51 | 50 | olci 393 |
. . . . . . . . . . . 12
               |
52 | | sumz 13800 |
. . . . . . . . . . . 12
     
                 |
53 | 51, 52 | mp1i 13 |
. . . . . . . . . . 11
 
                  |
54 | 33, 49, 53 | 3eqtrd 2491 |
. . . . . . . . . 10
 
                        |
55 | 54 | adantlr 722 |
. . . . . . . . 9
                                  |
56 | 29, 55 | oveq12d 6313 |
. . . . . . . 8
                                            |
57 | | etransclem24.p |
. . . . . . . . . . . . 13
   |
58 | | nnm1nn0 10918 |
. . . . . . . . . . . . 13
 
   |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . 12
     |
60 | 59 | nn0red 10933 |
. . . . . . . . . . 11
     |
61 | 60 | recnd 9674 |
. . . . . . . . . 10
     |
62 | 61 | addid1d 9838 |
. . . . . . . . 9
         |
63 | 62 | ad2antrr 733 |
. . . . . . . 8
                            |
64 | 28, 56, 63 | 3eqtrd 2491 |
. . . . . . 7
                                  |
65 | | etransclem24.ip |
. . . . . . . . 9
     |
66 | 65 | necomd 2681 |
. . . . . . . 8
     |
67 | 66 | ad2antrr 733 |
. . . . . . 7
                        |
68 | 64, 67 | eqnetrd 2693 |
. . . . . 6
                                |
69 | 68 | neneqd 2631 |
. . . . 5
                   
            |
70 | 13, 69 | sylan2br 479 |
. . . 4
                    
            |
71 | 12, 70 | condan 804 |
. . 3
 
                   |
72 | 57 | nnzd 11046 |
. . . . . . . . 9
   |
73 | 11 | eqcomd 2459 |
. . . . . . . . . . . . 13
             |
74 | 73 | fveq2d 5874 |
. . . . . . . . . . . 12
                     |
75 | 74 | oveq1d 6310 |
. . . . . . . . . . 11
                                                     |
76 | | nfcv 2594 |
. . . . . . . . . . . 12
   |
77 | | fzfid 12193 |
. . . . . . . . . . . 12
       |
78 | | nn0ex 10882 |
. . . . . . . . . . . . . 14
 |
79 | | mapss 7519 |
. . . . . . . . . . . . . 14
     
                   |
80 | 78, 39, 79 | mp2an 679 |
. . . . . . . . . . . . 13
                 |
81 | 80, 21 | sseldi 3432 |
. . . . . . . . . . . 12
         |
82 | 76, 77, 81 | mccl 37688 |
. . . . . . . . . . 11
                                 |
83 | 75, 82 | eqeltrd 2531 |
. . . . . . . . . 10
                       |
84 | 83 | nnzd 11046 |
. . . . . . . . 9
                       |
85 | | fzfid 12193 |
. . . . . . . . . 10
       |
86 | 57 | adantr 467 |
. . . . . . . . . . 11
 
       |
87 | 23 | adantr 467 |
. . . . . . . . . . 11
 
                   |
88 | 41 | adantl 468 |
. . . . . . . . . . 11
 
           |
89 | | etransclem24.j |
. . . . . . . . . . . . 13
   |
90 | | 0zd 10956 |
. . . . . . . . . . . . 13
   |
91 | 89, 90 | eqeltrd 2531 |
. . . . . . . . . . . 12
   |
92 | 91 | adantr 467 |
. . . . . . . . . . 11
 
       |
93 | 86, 87, 88, 92 | etransclem3 38112 |
. . . . . . . . . 10
 
      
                            
          |
94 | 85, 93 | fprodzcl 14020 |
. . . . . . . . 9
                        
                       |
95 | 72, 84, 94 | 3jca 1189 |
. . . . . . . 8
                                                          
           |
96 | 95 | 3ad2ant1 1030 |
. . . . . . 7
 
   
                          
                                               |
97 | 72 | adantr 467 |
. . . . . . . . . . 11
 
       |
98 | 57 | adantr 467 |
. . . . . . . . . . . 12
 
       |
99 | 23 | adantr 467 |
. . . . . . . . . . . 12
 
                   |
100 | 40 | sseli 3430 |
. . . . . . . . . . . . 13
           |
101 | 100 | adantl 468 |
. . . . . . . . . . . 12
 
           |
102 | 91 | adantr 467 |
. . . . . . . . . . . 12
 
       |
103 | 98, 99, 101, 102 | etransclem3 38112 |
. . . . . . . . . . 11
 
      
                            
          |
104 | | difss 3562 |
. . . . . . . . . . . . . . 15
       
     |
105 | | ssfi 7797 |
. . . . . . . . . . . . . . 15
                       
     |
106 | 50, 104, 105 | mp2an 679 |
. . . . . . . . . . . . . 14
         |
107 | 106 | a1i 11 |
. . . . . . . . . . . . 13
           |
108 | 57 | adantr 467 |
. . . . . . . . . . . . . 14
 
           |
109 | 23 | adantr 467 |
. . . . . . . . . . . . . 14
 
                       |
110 | 104, 40 | sstri 3443 |
. . . . . . . . . . . . . . . 16
       
     |
111 | 110 | sseli 3430 |
. . . . . . . . . . . . . . 15
               |
112 | 111 | adantl 468 |
. . . . . . . . . . . . . 14
 
               |
113 | 91 | adantr 467 |
. . . . . . . . . . . . . 14
 
           |
114 | 108, 109,
112, 113 | etransclem3 38112 |
. . . . . . . . . . . . 13
 
                          
            
          |
115 | 107, 114 | fprodzcl 14020 |
. . . . . . . . . . . 12
      
                                  
          |
116 | 115 | adantr 467 |
. . . . . . . . . . 11
 
                                
                       |
117 | 97, 103, 116 | 3jca 1189 |
. . . . . . . . . 10
 
     
 
                            
        
    
                                  
           |
118 | 117 | 3adant3 1029 |
. . . . . . . . 9
 
   
                                    
        
    
                                  
           |
119 | | dvds0 14330 |
. . . . . . . . . . . . . 14
   |
120 | 72, 119 | syl 17 |
. . . . . . . . . . . . 13
   |
121 | 120 | adantr 467 |
. . . . . . . . . . . 12
 
    
  |
122 | 121 | 3ad2antl1 1171 |
. . . . . . . . . . 11
      
         
  |
123 | | iftrue 3889 |
. . . . . . . . . . . . 13
      
                            
          |
124 | 123 | eqcomd 2459 |
. . . . . . . . . . . 12
                      
                       |
125 | 124 | adantl 468 |
. . . . . . . . . . 11
      
         
                                         |
126 | 122, 125 | breqtrd 4430 |
. . . . . . . . . 10
      
         
 
                            
          |
127 | 97 | adantr 467 |
. . . . . . . . . . . . . 14
            
  |
128 | | 0zd 10956 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
129 | 99, 101 | ffvelrnd 6028 |
. . . . . . . . . . . . . . . . . . . . . 22
 
               |
130 | 129 | elfzelzd 37546 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
131 | 97, 130 | zsubcld 11052 |
. . . . . . . . . . . . . . . . . . . 20
 
     
       |
132 | 128, 97, 131 | 3jca 1189 |
. . . . . . . . . . . . . . . . . . 19
 
     

        |
133 | 132 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
              
        |
134 | | fzssre 37545 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
135 | 134, 129 | sseldi 3432 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
136 | 135 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
                   |
137 | 127 | zred 11047 |
. . . . . . . . . . . . . . . . . . . 20
            
  |
138 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . 20
            
      |
139 | 136, 137,
138 | nltled 9790 |
. . . . . . . . . . . . . . . . . . 19
                
  |
140 | 137, 136 | subge0d 10210 |
. . . . . . . . . . . . . . . . . . 19
              
    
       |
141 | 139, 140 | mpbird 236 |
. . . . . . . . . . . . . . . . . 18
            
        |
142 | | elfzle1 11809 |
. . . . . . . . . . . . . . . . . . . . 21
               |
143 | 129, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
           |
144 | 143 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
            
      |
145 | 137, 136 | subge02d 10212 |
. . . . . . . . . . . . . . . . . . 19
                           |
146 | 144, 145 | mpbid 214 |
. . . . . . . . . . . . . . . . . 18
                  
  |
147 | 133, 141,
146 | jca32 538 |
. . . . . . . . . . . . . . . . 17
                      
      
    
    |
148 | | elfz2 11798 |
. . . . . . . . . . . . . . . . 17
          
 

      
      
    
    |
149 | 147, 148 | sylibr 216 |
. . . . . . . . . . . . . . . 16
                         |
150 | | permnn 12518 |
. . . . . . . . . . . . . . . 16
                             |
151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . . 15
                               |
152 | 151 | nnzd 11046 |
. . . . . . . . . . . . . 14
                               |
153 | 101 | elfzelzd 37546 |
. . . . . . . . . . . . . . . . 17
 
       |
154 | 102, 153 | zsubcld 11052 |
. . . . . . . . . . . . . . . 16
 
     
   |
155 | 154 | adantr 467 |
. . . . . . . . . . . . . . 15
                 |
156 | 131 | adantr 467 |
. . . . . . . . . . . . . . . 16
                     |
157 | | elnn0z 10957 |
. . . . . . . . . . . . . . . 16
      
                |
158 | 156, 141,
157 | sylanbrc 671 |
. . . . . . . . . . . . . . 15
                     |
159 | | zexpcl 12294 |
. . . . . . . . . . . . . . 15
    
           
        |
160 | 155, 158,
159 | syl2anc 667 |
. . . . . . . . . . . . . 14
                  
        |
161 | 127, 152,
160 | 3jca 1189 |
. . . . . . . . . . . . 13
                                   
         |
162 | 161 | 3adantl3 1167 |
. . . . . . . . . . . 12
      
          
                               |
163 | 127 | 3adantl3 1167 |
. . . . . . . . . . . . . 14
      
            |
164 | 59 | nn0zd 11045 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
165 | 164 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
     
   |
166 | 128, 165,
131 | 3jca 1189 |
. . . . . . . . . . . . . . . . . . . 20
 
      
 
        |
167 | 166 | 3adant3 1029 |
. . . . . . . . . . . . . . . . . . 19
 
   
                 |
168 | 167 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
      
           
 
        |
169 | 141 | 3adantl3 1167 |
. . . . . . . . . . . . . . . . . 18
      
                  |
170 | | 1red 9663 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
171 | | nnre 10623 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
172 | 171 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
173 | 57 | nnred 10631 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
174 | 173 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
175 | | nnge1 10642 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
176 | 175 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
177 | 170, 172,
174, 176 | lesub2dd 10237 |
. . . . . . . . . . . . . . . . . . . 20
 
          
    |
178 | 177 | 3adant2 1028 |
. . . . . . . . . . . . . . . . . . 19
 
   
          
    |
179 | 178 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
      
          
         |
180 | 168, 169,
179 | jca32 538 |
. . . . . . . . . . . . . . . . 17
      
              
            
            |
181 | | elfz2 11798 |
. . . . . . . . . . . . . . . . 17
            
  
 
            
            |
182 | 180, 181 | sylibr 216 |
. . . . . . . . . . . . . . . 16
      
          
        
    |
183 | | permnn 12518 |
. . . . . . . . . . . . . . . 16
                 
               |
184 | 182, 183 | syl 17 |
. . . . . . . . . . . . . . 15
      
              
               |
185 | 184 | nnzd 11046 |
. . . . . . . . . . . . . 14
      
              
               |
186 | | dvdsmul1 14336 |
. . . . . . . . . . . . . 14
      
              
          
          |
187 | 163, 185,
186 | syl2anc 667 |
. . . . . . . . . . . . 13
      
               
                |
188 | 57 | nncnd 10632 |
. . . . . . . . . . . . . . . . . . . . 21
   |
189 | | 1cnd 9664 |
. . . . . . . . . . . . . . . . . . . . 21
   |
190 | 188, 189 | npcand 9995 |
. . . . . . . . . . . . . . . . . . . 20
       |
191 | 190 | eqcomd 2459 |
. . . . . . . . . . . . . . . . . . 19
       |
192 | 191 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . 18
               |
193 | | facp1 12471 |
. . . . . . . . . . . . . . . . . . 19
  
            
         |
194 | 59, 193 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                       |
195 | 190 | oveq2d 6311 |
. . . . . . . . . . . . . . . . . . 19
     
                 |
196 | 59 | faccld 37543 |
. . . . . . . . . . . . . . . . . . . . 21
    
    |
197 | 196 | nncnd 10632 |
. . . . . . . . . . . . . . . . . . . 20
    
    |
198 | 197, 188 | mulcomd 9669 |
. . . . . . . . . . . . . . . . . . 19
     
       
     |
199 | 195, 198 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . 18
     
           
     |
200 | 192, 194,
199 | 3eqtrd 2491 |
. . . . . . . . . . . . . . . . 17
         
     |
201 | 200 | oveq1d 6310 |
. . . . . . . . . . . . . . . 16
                             
         |
202 | 201 | adantr 467 |
. . . . . . . . . . . . . . 15
 
                                           |
203 | 202 | 3ad2antl1 1171 |
. . . . . . . . . . . . . 14
      
                                                |
204 | 188 | ad2antrr 733 |
. . . . . . . . . . . . . . . 16
            
  |
205 | 197 | ad2antrr 733 |
. . . . . . . . . . . . . . . 16
                
    |
206 | 158 | faccld 37543 |
. . . . . . . . . . . . . . . . 17
                
        |
207 | 206 | nncnd 10632 |
. . . . . . . . . . . . . . . 16
                
        |
208 | 206 | nnne0d 10661 |
. . . . . . . . . . . . . . . 16
                
        |
209 | 204, 205,
207, 208 | divassd 10425 |
. . . . . . . . . . . . . . 15
                                      
                |
210 | 209 | 3adantl3 1167 |
. . . . . . . . . . . . . 14
      
                                   
                |
211 | 203, 210 | eqtr2d 2488 |
. . . . . . . . . . . . 13
      
          
          
                
         |
212 | 187, 211 | breqtrd 4430 |
. . . . . . . . . . . 12
      
                            |
213 | | dvdsmultr1 14350 |
. . . . . . . . . . . 12
                       
                                 
            
          |
214 | 162, 212,
213 | sylc 62 |
. . . . . . . . . . 11
      
                   
                      |
215 | | iffalse 3892 |
. . . . . . . . . . . 12
                                                     
            
         |
216 | 215 | adantl 468 |
. . . . . . . . . . 11
      
           
                            
                                        |
217 | 214, 216 | breqtrrd 4432 |
. . . . . . . . . 10
      
                           
                       |
218 | 126, 217 | pm2.61dan 801 |
. . . . . . . . 9
 
   
      
                            
          |
219 | | dvdsmultr1 14350 |
. . . . . . . . 9
                                                                    
                        
                            
                          
            
                                   
                         |
220 | 118, 218,
219 | sylc 62 |
. . . . . . . 8
 
   
                                                  
                                  
           |
221 | | fzfid 12193 |
. . . . . . . . 9
 
   
           |
222 | 93 | zcnd 11048 |
. . . . . . . . . 10
 
      
                            
          |
223 | 222 | 3ad2antl1 1171 |
. . . . . . . . 9
      
         
                 
            
          |
224 | | simp2 1010 |
. . . . . . . . 9
 
   
           |
225 | | fveq2 5870 |
. . . . . . . . . . . 12
           |
226 | 225 | breq2d 4417 |
. . . . . . . . . . 11
     
       |
227 | 225 | oveq2d 6311 |
. . . . . . . . . . . . . 14
 
             |
228 | 227 | fveq2d 5874 |
. . . . . . . . . . . . 13
              
        |
229 | 228 | oveq2d 6311 |
. . . . . . . . . . . 12
                                   |
230 | | oveq2 6303 |
. . . . . . . . . . . . 13
 
     |
231 | 230, 227 | oveq12d 6313 |
. . . . . . . . . . . 12
                           |
232 | 229, 231 | oveq12d 6313 |
. . . . . . . . . . 11
                                        
                      |
233 | 226, 232 | ifbieq2d 3908 |
. . . . . . . . . 10
  
                            
                                                 |
234 | 233 | adantl 468 |
. . . . . . . . 9
      
     
                 
            
                                                 |
235 | 221, 223,
224, 234 | fprodsplit1 37683 |
. . . . . . . 8
 
   
                            
                                                    
                                   
                        |
236 | 220, 235 | breqtrrd 4432 |
. . . . . . 7
 
   
                                         
          |
237 | | dvdsmultr2 14352 |
. . . . . . 7
                                                          
                                                                                                   
                         |
238 | 96, 236, 237 | sylc 62 |
. . . . . 6
 
   
                                                 
                        |
239 | 238 | 3adant1r 1262 |
. . . . 5
         
                                                                  
           |
240 | | simpr 463 |
. . . . . . . . . . . . . 14
 
               |
241 | | eluzfz1 11813 |
. . . . . . . . . . . . . . . . . . 19
    
      |
242 | 16, 241 | syl 17 |
. . . . . . . . . . . . . . . . . 18
       |
243 | 23, 242 | ffvelrnd 6028 |
. . . . . . . . . . . . . . . . 17
           |
244 | 134, 243 | sseldi 3432 |
. . . . . . . . . . . . . . . 16
       |
245 | 244 | adantr 467 |
. . . . . . . . . . . . . . 15
 
             |
246 | 60 | adantr 467 |
. . . . . . . . . . . . . . 15
 
       
   |
247 | 245, 246 | lttri3d 9780 |
. . . . . . . . . . . . . 14
 
             
       

        |
248 | 240, 247 | mpbid 214 |
. . . . . . . . . . . . 13
 
           
           |
249 | 248 | simprd 465 |
. . . . . . . . . . . 12
 
       

      |
250 | 249 | iffalsed 3894 |
. . . . . . . . . . 11
 
                      
      
                                                          |
251 | | oveq2 6303 |
. . . . . . . . . . . . . . . . 17
                  
    |
252 | 61 | subidd 9979 |
. . . . . . . . . . . . . . . . 17
    
    |
253 | 251, 252 | sylan9eqr 2509 |
. . . . . . . . . . . . . . . 16
 
                 |
254 | 253 | fveq2d 5874 |
. . . . . . . . . . . . . . 15
 
           
             |
255 | | fac0 12469 |
. . . . . . . . . . . . . . 15
     |
256 | 254, 255 | syl6eq 2503 |
. . . . . . . . . . . . . 14
 
           
         |
257 | 256 | oveq2d 6311 |
. . . . . . . . . . . . 13
 
           
                   
     |
258 | 197 | div1d 10382 |
. . . . . . . . . . . . . 14
     
           |
259 | 258 | adantr 467 |
. . . . . . . . . . . . 13
 
           
      
    |
260 | 257, 259 | eqtrd 2487 |
. . . . . . . . . . . 12
 
           
                  
    |
261 | 253 | oveq2d 6311 |
. . . . . . . . . . . . 13
 
                         |
262 | 91 | zcnd 11048 |
. . . . . . . . . . . . . . 15
   |
263 | 262 | exp0d 12417 |
. . . . . . . . . . . . . 14
       |
264 | 263 | adantr 467 |
. . . . . . . . . . . . 13
 
             |
265 | 261, 264 | eqtrd 2487 |
. . . . . . . . . . . 12
 
                     |
266 | 260, 265 | oveq12d 6313 |
. . . . . . . . . . 11
 
            
      
                         
     |
267 | 197 | mulid1d 9665 |
. . . . . . . . . . . 12
     
           |
268 | 267 | adantr 467 |
. . . . . . . . . . 11
 
           
      
    |
269 | 250, 266,
268 | 3eqtrd 2491 |
. . . . . . . . . 10
 
                      
      
                         
    |
270 | 269 | oveq1d 6310 |
. . . . . . . . 9
 
                       
      
                                             
                                                    
                        |
271 | 270 | oveq2d 6311 |
. . . . . . . 8
 
                                            
                             
                                                                          
                                                |
272 | 271 | oveq1d 6310 |
. . . . . . 7
 
                                             
      
                                             
                                                           
                                                       |
273 | 83 | nncnd 10632 |
. . . . . . . . 9
                       |
274 | 94 | zcnd 11048 |
. . . . . . . . . 10
                        
                       |
275 | 197, 274 | mulcld 9668 |
. . . . . . . . 9
     
                                      
           |
276 | 196 | nnne0d 10661 |
. . . . . . . . 9
    
    |
277 | 273, 275,
197, 276 | divassd 10425 |
. . . . . . . 8
                           
                         
            
             
                             
                         
            
            
      |
278 | 277 | adantr 467 |
. . . . . . 7
 
                                                           
                                                        
                                      
            
      |
279 | 274, 197,
276 | divcan3d 10395 |
. . . . . . . . 9
         
                                                                           
                       |
280 | 279 | oveq2d 6311 |
. . . . . . . 8
                           
                         
            
            
                                                
            
           |
281 | 280 | adantr 467 |
. . . . . . 7
 
                                                           
                                                                                       
           |
282 | 272, 278,
281 | 3eqtrd 2491 |
. . . . . 6
 
                                             
      
                                             
                                                                                       
           |
283 | 282 | 3ad2ant1 1030 |
. . . . 5
         
                                               
      
                                             
                                                                                       
           |
284 | 239, 283 | breqtrrd 4432 |
. . . 4
         
                                               
      
                                             
                                |
285 | 284 | rexlimdv3a 2883 |
. . 3
 
        
                                               
      
                                             
                                 |
286 | 71, 285 | mpd 15 |
. 2
 
                                             
      
                                             
                                |
287 | 120 | adantr 467 |
. . 3
 
         |
288 | | simpr 463 |
. . . . . . . . . . 11
          
              |
289 | 288 | iftrued 3891 |
. . . . . . . . . 10
          
                     
      
                        |
290 | | simpr 463 |
. . . . . . . . . . . 12
          

    
        |
291 | 290 | iffalsed 3894 |
. . . . . . . . . . 11
          

                                                                                      |
292 | | simpll 761 |
. . . . . . . . . . . 12
          

       |
293 | 244 | ad2antrr 733 |
. . . . . . . . . . . . 13
          

           |
294 | 60 | ad2antrr 733 |
. . . . . . . . . . . . 13
          

         |
295 | 293, 294,
290 | nltled 9790 |
. . . . . . . . . . . . 13
          

         
   |
296 | | id 22 |
. . . . . . . . . . . . . . 15
               |
297 | 296 | necomd 2681 |
. . . . . . . . . . . . . 14
       
       |
298 | 297 | ad2antlr 734 |
. . . . . . . . . . . . 13
          

             |
299 | 293, 294,
295, 298 | leneltd 9794 |
. . . . . . . . . . . 12
          

         
   |
300 | 89 | oveq1d 6310 |
. . . . . . . . . . . . . . . 16
                           |
301 | 300 | adantr 467 |
. . . . . . . . . . . . . . 15
 
                                 |
302 | 243 | elfzelzd 37546 |
. . . . . . . . . . . . . . . . . . 19
       |
303 | 164, 302 | zsubcld 11052 |
. . . . . . . . . . . . . . . . . 18
           |
304 | 303 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
                 |
305 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
 
               |
306 | 244 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
             |
307 | 60 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
       
   |
308 | 306, 307 | posdifd 10207 |
. . . . . . . . . . . . . . . . . 18
 
           
 
           |
309 | 305, 308 | mpbid 214 |
. . . . . . . . . . . . . . . . 17
 
                 |
310 | | elnnz 10954 |
. . . . . . . . . . . . . . . . 17
        
                    |
311 | 304, 309,
310 | sylanbrc 671 |
. . . . . . . . . . . . . . . 16
 
                 |
312 | 311 | 0expd 12439 |
. . . . . . . . . . . . . . 15
 
 |