Step | Hyp | Ref
| Expression |
1 | | etransclem44.k |
. . . 4
                                                    
    |
2 | 1 | a1i 11 |
. . 3
  
                                                        |
3 | | nfv 1761 |
. . . . 5
   |
4 | | nfcv 2592 |
. . . . 5
               
       |
5 | | fzfi 12185 |
. . . . . . 7
     |
6 | | fzfi 12185 |
. . . . . . 7
           |
7 | | xpfi 7842 |
. . . . . . 7
                                   |
8 | 5, 6, 7 | mp2an 678 |
. . . . . 6
                 |
9 | 8 | a1i 11 |
. . . . 5
                   |
10 | | etransclem44.a |
. . . . . . . . 9
       |
11 | 10 | adantr 467 |
. . . . . . . 8
 
                
      |
12 | | fzssnn0 37539 |
. . . . . . . . . 10
     |
13 | | xp1st 6823 |
. . . . . . . . . 10
                           |
14 | 12, 13 | sseldi 3430 |
. . . . . . . . 9
                       |
15 | 14 | adantl 468 |
. . . . . . . 8
 
                
      |
16 | 11, 15 | ffvelrnd 6023 |
. . . . . . 7
 
                
          |
17 | | reelprrecn 9631 |
. . . . . . . . 9
    |
18 | 17 | a1i 11 |
. . . . . . . 8
 
                
     |
19 | | reopn 37502 |
. . . . . . . . . 10
     |
20 | | eqid 2451 |
. . . . . . . . . . 11
  ℂfld   ℂfld |
21 | 20 | tgioo2 21821 |
. . . . . . . . . 10
       ℂfld
↾t   |
22 | 19, 21 | eleqtri 2527 |
. . . . . . . . 9
   ℂfld
↾t   |
23 | 22 | a1i 11 |
. . . . . . . 8
 
                
   ℂfld
↾t    |
24 | | etransclem44.p |
. . . . . . . . . 10
   |
25 | | prmnn 14625 |
. . . . . . . . . 10

  |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
   |
27 | 26 | adantr 467 |
. . . . . . . 8
 
                
  |
28 | | etransclem44.m |
. . . . . . . . 9
   |
29 | 28 | adantr 467 |
. . . . . . . 8
 
                
  |
30 | | etransclem44.f |
. . . . . . . 8
                       |
31 | | xp2nd 6824 |
. . . . . . . . . 10
                                 |
32 | | elfznn0 11887 |
. . . . . . . . . 10
                     |
33 | 31, 32 | syl 17 |
. . . . . . . . 9
                       |
34 | 33 | adantl 468 |
. . . . . . . 8
 
                
      |
35 | 15 | nn0red 10926 |
. . . . . . . 8
 
                
      |
36 | 15 | nn0zd 11038 |
. . . . . . . 8
 
                
      |
37 | 18, 23, 27, 29, 30, 34, 35, 36 | etransclem42 38141 |
. . . . . . 7
 
                
                      |
38 | 16, 37 | zmulcld 11046 |
. . . . . 6
 
                
                                |
39 | 38 | zcnd 11041 |
. . . . 5
 
                
                                |
40 | | nn0uz 11193 |
. . . . . . . 8
     |
41 | 28, 40 | syl6eleq 2539 |
. . . . . . 7
       |
42 | | eluzfz1 11806 |
. . . . . . 7
    
      |
43 | 41, 42 | syl 17 |
. . . . . 6
       |
44 | | 0zd 10949 |
. . . . . . . . 9
   |
45 | 28 | nn0zd 11038 |
. . . . . . . . . . 11
   |
46 | 26 | nnzd 11039 |
. . . . . . . . . . 11
   |
47 | 45, 46 | zmulcld 11046 |
. . . . . . . . . 10
     |
48 | | nnm1nn0 10911 |
. . . . . . . . . . . 12
 
   |
49 | 26, 48 | syl 17 |
. . . . . . . . . . 11
     |
50 | 49 | nn0zd 11038 |
. . . . . . . . . 10
     |
51 | 47, 50 | zaddcld 11044 |
. . . . . . . . 9
         |
52 | 44, 51, 50 | 3jca 1188 |
. . . . . . . 8
        
    |
53 | 49 | nn0ge0d 10928 |
. . . . . . . 8

    |
54 | 26 | nnnn0d 10925 |
. . . . . . . . . . 11
   |
55 | 28, 54 | nn0mulcld 10930 |
. . . . . . . . . 10
     |
56 | 55 | nn0ge0d 10928 |
. . . . . . . . 9

    |
57 | 49 | nn0red 10926 |
. . . . . . . . . 10
     |
58 | 47 | zred 11040 |
. . . . . . . . . 10
     |
59 | 57, 58 | addge02d 10202 |
. . . . . . . . 9
  
            |
60 | 56, 59 | mpbid 214 |
. . . . . . . 8
  
 
      |
61 | 52, 53, 60 | jca32 538 |
. . . . . . 7
            
  

 
        |
62 | | elfz2 11791 |
. . . . . . 7
            
        
                 |
63 | 61, 62 | sylibr 216 |
. . . . . 6
               |
64 | | opelxp 4864 |
. . . . . 6
                                          |
65 | 43, 63, 64 | sylanbrc 670 |
. . . . 5
                        |
66 | | fveq2 5865 |
. . . . . . . 8
                     |
67 | | 0re 9643 |
. . . . . . . . 9
 |
68 | | ovex 6318 |
. . . . . . . . 9
   |
69 | | op1stg 6805 |
. . . . . . . . 9
  
      
      |
70 | 67, 68, 69 | mp2an 678 |
. . . . . . . 8
        
 |
71 | 66, 70 | syl6eq 2501 |
. . . . . . 7
            |
72 | 71 | fveq2d 5869 |
. . . . . 6
                    |
73 | | fveq2 5865 |
. . . . . . . . 9
                     |
74 | | op2ndg 6806 |
. . . . . . . . . 10
  
      
        |
75 | 67, 68, 74 | mp2an 678 |
. . . . . . . . 9
        

  |
76 | 73, 75 | syl6eq 2501 |
. . . . . . . 8
              |
77 | 76 | fveq2d 5869 |
. . . . . . 7
                         
    |
78 | 77, 71 | fveq12d 5871 |
. . . . . 6
                                  
       |
79 | 72, 78 | oveq12d 6308 |
. . . . 5
                                                          |
80 | 3, 4, 9, 39, 65, 79 | fsumsplit1 37651 |
. . . 4
                                                                                                                                  |
81 | 80 | oveq1d 6305 |
. . 3
                                                     
                                                                                      
     |
82 | 12, 43 | sseldi 3430 |
. . . . . . 7
   |
83 | 10, 82 | ffvelrnd 6023 |
. . . . . 6
       |
84 | 17 | a1i 11 |
. . . . . . 7
      |
85 | 22 | a1i 11 |
. . . . . . 7
    ℂfld ↾t    |
86 | 67 | a1i 11 |
. . . . . . 7
   |
87 | 84, 85, 26, 28, 30, 49, 86, 44 | etransclem42 38141 |
. . . . . 6
                 |
88 | 83, 87 | zmulcld 11046 |
. . . . 5
              
        |
89 | 88 | zcnd 11041 |
. . . 4
              
        |
90 | | difss 3560 |
. . . . . . . 8
                                          |
91 | | ssfi 7792 |
. . . . . . . 8
                                                                                       |
92 | 8, 90, 91 | mp2an 678 |
. . . . . . 7
                          |
93 | 92 | a1i 11 |
. . . . . 6
                            |
94 | | eldifi 3555 |
. . . . . . 7
                                            |
95 | 94, 38 | sylan2 477 |
. . . . . 6
 
                                                          |
96 | 93, 95 | fsumzcl 13801 |
. . . . 5
                                                            |
97 | 96 | zcnd 11041 |
. . . 4
                                                            |
98 | 49 | faccld 37533 |
. . . . 5
    
    |
99 | 98 | nncnd 10625 |
. . . 4
    
    |
100 | 98 | nnne0d 10654 |
. . . 4
    
    |
101 | 89, 97, 99, 100 | divdird 10421 |
. . 3
                                                                                    
                            
                                                                
      |
102 | 2, 81, 101 | 3eqtrd 2489 |
. 2
                
              
                                                           
      |
103 | 26 | nnne0d 10654 |
. . 3
   |
104 | 83 | zcnd 11041 |
. . . . 5
       |
105 | 87 | zcnd 11041 |
. . . . 5
                 |
106 | 104, 105,
99, 100 | divassd 10418 |
. . . 4
                         
                 
               |
107 | | etransclem5 38104 |
. . . . . . 7
                                           |
108 | | etransclem11 38110 |
. . . . . . 7

           
                                    |
109 | 84, 85, 26, 28, 30, 49, 107, 108, 43, 86 | etransclem37 38136 |
. . . . . 6
    
          
       |
110 | 98 | nnzd 11039 |
. . . . . . 7
    
    |
111 | | dvdsval2 14308 |
. . . . . . 7
     
                
                          
         
               |
112 | 110, 100,
87, 111 | syl3anc 1268 |
. . . . . 6
     
          
              
        
      |
113 | 109, 112 | mpbid 214 |
. . . . 5
                   
     |
114 | 83, 113 | zmulcld 11046 |
. . . 4
                               |
115 | 106, 114 | eqeltrd 2529 |
. . 3
                         
     |
116 | 94, 39 | sylan2 477 |
. . . . 5
 
                                                          |
117 | 93, 99, 116, 100 | fsumdivc 13847 |
. . . 4
                                                              
   
                                                            
     |
118 | 16 | zcnd 11041 |
. . . . . . . 8
 
                
          |
119 | 94, 118 | sylan2 477 |
. . . . . . 7
 
                                    |
120 | 94, 37 | sylan2 477 |
. . . . . . . 8
 
                                                |
121 | 120 | zcnd 11041 |
. . . . . . 7
 
                                                |
122 | 99 | adantr 467 |
. . . . . . 7
 
                             
    |
123 | 100 | adantr 467 |
. . . . . . 7
 
                             
    |
124 | 119, 121,
122, 123 | divassd 10418 |
. . . . . 6
 
                                                            
                                    
      |
125 | 94, 16 | sylan2 477 |
. . . . . . 7
 
                                    |
126 | 17 | a1i 11 |
. . . . . . . . 9
 
                               |
127 | 22 | a1i 11 |
. . . . . . . . 9
 
                             ℂfld ↾t    |
128 | 26 | adantr 467 |
. . . . . . . . 9
 
                         
  |
129 | 28 | adantr 467 |
. . . . . . . . 9
 
                         
  |
130 | 94 | adantl 468 |
. . . . . . . . . 10
 
                                            |
131 | 130, 33 | syl 17 |
. . . . . . . . 9
 
                                |
132 | 130, 13 | syl 17 |
. . . . . . . . 9
 
                                    |
133 | 94, 35 | sylan2 477 |
. . . . . . . . 9
 
                                |
134 | 126, 127,
128, 129, 30, 131, 107, 108, 132, 133 | etransclem37 38136 |
. . . . . . . 8
 
                             
                        |
135 | 110 | adantr 467 |
. . . . . . . . 9
 
                             
    |
136 | | dvdsval2 14308 |
. . . . . . . . 9
     
                                 
                     
                        
      |
137 | 135, 123,
120, 136 | syl3anc 1268 |
. . . . . . . 8
 
                              
                     
                        
      |
138 | 134, 137 | mpbid 214 |
. . . . . . 7
 
                                                        |
139 | 125, 138 | zmulcld 11046 |
. . . . . 6
 
                                                           
      |
140 | 124, 139 | eqeltrd 2529 |
. . . . 5
 
                                                            
     |
141 | 93, 140 | fsumzcl 13801 |
. . . 4
                                                              
     |
142 | 117, 141 | eqeltrd 2529 |
. . 3
                                                              
     |
143 | | 1zzd 10968 |
. . . . . . . . . . . 12
   |
144 | | zabscl 13376 |
. . . . . . . . . . . . 13
               |
145 | 83, 144 | syl 17 |
. . . . . . . . . . . 12
           |
146 | 143, 50, 145 | 3jca 1188 |
. . . . . . . . . . 11
               |
147 | | nn0abscl 13375 |
. . . . . . . . . . . . . 14
               |
148 | 83, 147 | syl 17 |
. . . . . . . . . . . . 13
           |
149 | | etransclem44.a0 |
. . . . . . . . . . . . . 14
       |
150 | 104, 149 | absne0d 13509 |
. . . . . . . . . . . . 13
           |
151 | | elnnne0 10883 |
. . . . . . . . . . . . 13
        
        
           |
152 | 148, 150,
151 | sylanbrc 670 |
. . . . . . . . . . . 12
           |
153 | 152 | nnge1d 10652 |
. . . . . . . . . . 11

          |
154 | | etransclem44.ap |
. . . . . . . . . . . 12
        
  |
155 | | zltlem1 10989 |
. . . . . . . . . . . . 13
         
         
        
    |
156 | 145, 46, 155 | syl2anc 667 |
. . . . . . . . . . . 12
         
        
    |
157 | 154, 156 | mpbid 214 |
. . . . . . . . . . 11
        
    |
158 | 146, 153,
157 | jca32 538 |
. . . . . . . . . 10
                      
        
     |
159 | | elfz2 11791 |
. . . . . . . . . 10
              
  
                                 |
160 | 158, 159 | sylibr 216 |
. . . . . . . . 9
                 |
161 | | fzm1ndvds 14357 |
. . . . . . . . 9
                
          |
162 | 26, 160, 161 | syl2anc 667 |
. . . . . . . 8
           |
163 | | dvdsabsb 14322 |
. . . . . . . . 9
                       |
164 | 46, 83, 163 | syl2anc 667 |
. . . . . . . 8
                 |
165 | 162, 164 | mtbird 303 |
. . . . . . 7
       |
166 | | etransclem44.mp |
. . . . . . . 8
    
  |
167 | 28, 24, 166, 30 | etransclem41 38140 |
. . . . . . 7
                         |
168 | 165, 167 | jca 535 |
. . . . . 6
                        
      |
169 | | pm4.56 498 |
. . . . . 6
                            
                       
      |
170 | 168, 169 | sylib 200 |
. . . . 5
                               |
171 | | euclemma 14665 |
. . . . . 6
               
                            
                                            |
172 | 24, 83, 113, 171 | syl3anc 1268 |
. . . . 5
                
                                            |
173 | 170, 172 | mtbird 303 |
. . . 4
               
               |
174 | 106 | breq2d 4414 |
. . . 4
                
            
              
        
       |
175 | 173, 174 | mtbird 303 |
. . 3
               
               |
176 | 46 | adantr 467 |
. . . . . . . 8
 
                         
  |
177 | 176, 125,
138 | 3jca 1188 |
. . . . . . 7
 
                                                           
      |
178 | | eldifn 3556 |
. . . . . . . . . 10
                         
         |
179 | 94 | adantr 467 |
. . . . . . . . . . . . 13
                                       
                  |
180 | | 1st2nd2 6830 |
. . . . . . . . . . . . 13
                              |
181 | 179, 180 | syl 17 |
. . . . . . . . . . . 12
                                       
             |
182 | | simpr 463 |
. . . . . . . . . . . . . 14
                   |
183 | | simpl 459 |
. . . . . . . . . . . . . 14
                     |
184 | 182, 183 | opeq12d 4174 |
. . . . . . . . . . . . 13
                         
     |
185 | 184 | adantl 468 |
. . . . . . . . . . . 12
                                       
          
       |
186 | 181, 185 | eqtrd 2485 |
. . . . . . . . . . 11
                                       
       |
187 | | elsn 3982 |
. . . . . . . . . . 11
       
       |
188 | 186, 187 | sylibr 216 |
. . . . . . . . . 10
                                       
         |
189 | 178, 188 | mtand 665 |
. . . . . . . . 9
                                        |
190 | 189 | adantl 468 |
. . . . . . . 8
 
                                        |
191 | 128, 129,
30, 131, 132, 190, 108 | etransclem38 38137 |
. . . . . . 7
 
                                                        |
192 | | dvdsmultr2 14340 |
. . . . . . 7
                                  
                                                                          |
193 | 177, 191,
192 | sylc 62 |
. . . . . 6
 
                                                           
      |
194 | 193, 124 | breqtrrd 4429 |
. . . . 5
 
                                                                  |
195 | 93, 46, 140, 194 | fsumdvds 14348 |
. . . 4
                                                                    |
196 | 195, 117 | breqtrrd 4429 |
. . 3
  
                                                           
     |
197 | 46, 103, 115, 142, 175, 196 | etransclem9 38108 |
. 2
                          
                                                                
      |
198 | 102, 197 | eqnetrd 2691 |
1
   |