Step | Hyp | Ref
| Expression |
1 | | etransclem46.l |
. . . 4
                                   |
2 | 1 | a1i 11 |
. . 3
                                     |
3 | | etransclem46.h |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)               |
4 | 3 | oveq2i 6301 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif)                |
5 | 4 | a1i 11 |
. . . . . . . . . . . 12
 
           ![[,] [,]](_icc.gif)                 |
6 | | etransclem46.s |
. . . . . . . . . . . . . 14
      |
7 | 6 | adantr 467 |
. . . . . . . . . . . . 13
 
          |
8 | | ere 14143 |
. . . . . . . . . . . . . . . . . . . 20
 |
9 | 8 | recni 9655 |
. . . . . . . . . . . . . . . . . . 19
 |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
   |
11 | | recn 9629 |
. . . . . . . . . . . . . . . . . . 19
   |
12 | 11 | negcld 9973 |
. . . . . . . . . . . . . . . . . 18
    |
13 | 10, 12 | cxpcld 23653 |
. . . . . . . . . . . . . . . . 17
       |
14 | 13 | adantl 468 |
. . . . . . . . . . . . . . . 16
 

      |
15 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
 

  |
16 | | fzfid 12186 |
. . . . . . . . . . . . . . . . . . 19
 

      |
17 | | elfznn0 11887 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
18 | 6 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

     |
19 | | etransclem46.x |
. . . . . . . . . . . . . . . . . . . . . . . 24
    ℂfld ↾t    |
20 | 19 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

   ℂfld
↾t    |
21 | | etransclem46.p |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
22 | 21 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

  |
23 | | etransclem46.m |
. . . . . . . . . . . . . . . . . . . . . . . . 25
deg   |
24 | | etransclem46.q |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  Poly        |
25 | 24 | eldifad 3416 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 Poly    |
26 | | dgrcl 23187 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 Poly  deg    |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 deg    |
28 | 23, 27 | syl5eqel 2533 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
29 | 28 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

  |
30 | | etransclem46.f |
. . . . . . . . . . . . . . . . . . . . . . 23
                       |
31 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

  |
32 | 18, 20, 22, 29, 30, 31 | etransclem33 38132 |
. . . . . . . . . . . . . . . . . . . . . 22
 

              |
33 | 17, 32 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . 21
 
                   |
34 | 33 | adantlr 721 |
. . . . . . . . . . . . . . . . . . . 20
                       |
35 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . 20
           |
36 | 34, 35 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . . . 19
                       |
37 | 16, 36 | fsumcl 13799 |
. . . . . . . . . . . . . . . . . 18
 

                    |
38 | | etransclem46.g |
. . . . . . . . . . . . . . . . . . 19
                     |
39 | 38 | fvmpt2 5957 |
. . . . . . . . . . . . . . . . . 18
                         
                   |
40 | 15, 37, 39 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
 

                        |
41 | 40, 37 | eqeltrd 2529 |
. . . . . . . . . . . . . . . 16
 

      |
42 | 14, 41 | mulcld 9663 |
. . . . . . . . . . . . . . 15
 

            |
43 | 42 | negcld 9973 |
. . . . . . . . . . . . . 14
 

             |
44 | 43 | adantlr 721 |
. . . . . . . . . . . . 13
                      |
45 | 6, 19 | dvdmsscn 37811 |
. . . . . . . . . . . . . . . . . . 19

  |
46 | 45, 21, 30 | etransclem8 38107 |
. . . . . . . . . . . . . . . . . 18
       |
47 | 46 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . 17
 

      |
48 | 14, 47 | mulcld 9663 |
. . . . . . . . . . . . . . . 16
 

            |
49 | 48 | negcld 9973 |
. . . . . . . . . . . . . . 15
 

             |
50 | 49 | negcld 9973 |
. . . . . . . . . . . . . 14
 

              |
51 | 50 | adantlr 721 |
. . . . . . . . . . . . 13
                       |
52 | 8 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
   |
53 | | 0re 9643 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
54 | | epos 14259 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
55 | 53, 8, 54 | ltleii 9757 |
. . . . . . . . . . . . . . . . . . . . 21
 |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
   |
57 | | renegcl 9937 |
. . . . . . . . . . . . . . . . . . . 20
    |
58 | 52, 56, 57 | recxpcld 23668 |
. . . . . . . . . . . . . . . . . . 19
       |
59 | 58 | renegcld 10046 |
. . . . . . . . . . . . . . . . . 18
        |
60 | 59 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 

       |
61 | | reelprrecn 9631 |
. . . . . . . . . . . . . . . . . . . . . 22
    |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
     |
63 | | cnelprrecn 9632 |
. . . . . . . . . . . . . . . . . . . . . 22
    |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
     |
65 | 12 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
     |
66 | | neg1rr 10714 |
. . . . . . . . . . . . . . . . . . . . . 22
  |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
     |
68 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
69 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
70 | 68, 69 | cxpcld 23653 |
. . . . . . . . . . . . . . . . . . . . . 22
      |
71 | 70 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
       |
72 | 11 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
    |
73 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . . 22
    |
74 | 62 | dvmptid 22911 |
. . . . . . . . . . . . . . . . . . . . . 22
        |
75 | 62, 72, 73, 74 | dvmptneg 22920 |
. . . . . . . . . . . . . . . . . . . . 21
          |
76 | | epr 14260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
77 | | dvcxp2 23681 |
. . . . . . . . . . . . . . . . . . . . . . . 24

                    |
78 | 76, 77 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
79 | | loge 23536 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
80 | 79 | oveq1i 6300 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
81 | 70 | mulid2d 9661 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
82 | 80, 81 | syl5eq 2497 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
         |
83 | 82 | mpteq2ia 4485 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
84 | 78, 83 | eqtri 2473 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
        
     |
86 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . . 21
           |
87 | 62, 64, 65, 67, 71, 71, 75, 85, 86, 86 | dvmptco 22926 |
. . . . . . . . . . . . . . . . . . . 20
                   |
88 | 87 | trud 1453 |
. . . . . . . . . . . . . . . . . . 19
                  |
89 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
    |
90 | 89 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . 22
    |
91 | 13, 90 | mulcomd 9664 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
92 | 13 | mulm1d 10070 |
. . . . . . . . . . . . . . . . . . . . 21
         
     |
93 | 91, 92 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . . 20
               |
94 | 93 | mpteq2ia 4485 |
. . . . . . . . . . . . . . . . . . 19
           
     |
95 | 88, 94 | eqtri 2473 |
. . . . . . . . . . . . . . . . . 18
                |
96 | 95 | a1i 11 |
. . . . . . . . . . . . . . . . 17
                  |
97 | 17 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
98 | | peano2nn0 10910 |
. . . . . . . . . . . . . . . . . . . . . 22

    |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 
         |
100 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
101 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
     |
102 | 101 | anbi2d 710 |
. . . . . . . . . . . . . . . . . . . . . . 23
    

       |
103 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       |
104 | 103 | feq1d 5714 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 |
105 | 102, 104 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . 22
     
             
                       |
106 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
107 | 106 | anbi2d 710 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

     |
108 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   |
109 | 108 | feq1d 5714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                             |
110 | 107, 109 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
             
                   |
111 | 110, 32 | chvarv 2107 |
. . . . . . . . . . . . . . . . . . . . . 22
 

              |
112 | 100, 105,
111 | vtocl 3100 |
. . . . . . . . . . . . . . . . . . . . 21
 
                   |
113 | 99, 112 | syldan 473 |
. . . . . . . . . . . . . . . . . . . 20
 
                     |
114 | 113 | adantlr 721 |
. . . . . . . . . . . . . . . . . . 19
                         |
115 | 114, 35 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . . 18
                         |
116 | 16, 115 | fsumcl 13799 |
. . . . . . . . . . . . . . . . 17
 

                      |
117 | 21, 28, 30, 38 | etransclem39 38138 |
. . . . . . . . . . . . . . . . . . . . 21
       |
118 | 117 | feqmptd 5918 |
. . . . . . . . . . . . . . . . . . . 20
         |
119 | 118 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . 19
         |
120 | 119 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . 18
             |
121 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . 19
   |
122 | | elfznn0 11887 |
. . . . . . . . . . . . . . . . . . . 20
         |
123 | 122, 32 | sylan2 477 |
. . . . . . . . . . . . . . . . . . 19
 
   
                 |
124 | 121, 46, 123, 38 | etransclem2 38101 |
. . . . . . . . . . . . . . . . . 18
                           |
125 | 120, 124 | eqtrd 2485 |
. . . . . . . . . . . . . . . . 17
                                 |
126 | 6, 14, 60, 96, 41, 116, 125 | dvmptmul 22915 |
. . . . . . . . . . . . . . . 16
                                                          |
127 | 116, 14 | mulcomd 9664 |
. . . . . . . . . . . . . . . . . . 19
 

 
                             
                      |
128 | 127 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . 18
 

                                                                                |
129 | 14 | negcld 9973 |
. . . . . . . . . . . . . . . . . . . 20
 

       |
130 | 129, 41 | mulcld 9663 |
. . . . . . . . . . . . . . . . . . 19
 

  
          |
131 | 14, 116 | mulcld 9663 |
. . . . . . . . . . . . . . . . . . 19
 

     
                      |
132 | 130, 131 | addcomd 9835 |
. . . . . . . . . . . . . . . . . 18
 

                 
                                                              |
133 | 131, 42 | negsubd 9992 |
. . . . . . . . . . . . . . . . . . . 20
 

      
                                                                        |
134 | 14, 41 | mulneg1d 10071 |
. . . . . . . . . . . . . . . . . . . . 21
 

  
                     |
135 | 134 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . 20
 

      
                                                                         |
136 | 116, 41, 14 | subdir2d 37529 |
. . . . . . . . . . . . . . . . . . . 20
 

                                      
                                 |
137 | 133, 135,
136 | 3eqtr4d 2495 |
. . . . . . . . . . . . . . . . . . 19
 

      
                                                                  |
138 | 40 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . 21
 

 
                                                                  |
139 | 16, 115, 36 | fsumsub 13849 |
. . . . . . . . . . . . . . . . . . . . 21
 

                                                                            |
140 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
141 | 140 | fveq1d 5867 |
. . . . . . . . . . . . . . . . . . . . . 22
                           |
142 | 103 | fveq1d 5867 |
. . . . . . . . . . . . . . . . . . . . . 22
                               |
143 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
144 | 143 | fveq1d 5867 |
. . . . . . . . . . . . . . . . . . . . . 22
                           |
145 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
                       |
146 | 145 | fveq1d 5867 |
. . . . . . . . . . . . . . . . . . . . . 22
                       
       |
147 | | etransclem46.r |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
148 | 21 | nnnn0d 10925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
149 | 28, 148 | nn0mulcld 10930 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
150 | | nnm1nn0 10911 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
151 | 21, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
152 | 149, 151 | nn0addcld 10929 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
153 | 147, 152 | syl5eqel 2533 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
154 | 153 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

  |
155 | 154 | nn0zd 11038 |
. . . . . . . . . . . . . . . . . . . . . 22
 

  |
156 | | peano2nn0 10910 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

    |
157 | 153, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
158 | | nn0uz 11193 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
159 | 157, 158 | syl6eleq 2539 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
160 | 159 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
 

        |
161 | | elfznn0 11887 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
162 | 161, 111 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   
                 |
163 | 162 | adantlr 721 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
                 |
164 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
     |
165 | 163, 164 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . . . . . . 22
       
                 |
166 | 141, 142,
144, 146, 155, 160, 165 | telfsum2 13865 |
. . . . . . . . . . . . . . . . . . . . 21
 

                                           
                    |
167 | 138, 139,
166 | 3eqtr2d 2491 |
. . . . . . . . . . . . . . . . . . . 20
 

 
                                 
                    |
168 | 167 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . 19
 

                                                                    |
169 | 153 | nn0red 10926 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
170 | 169 | ltp1d 10537 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
171 | 147, 170 | syl5eqbrr 4437 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
172 | | etransclem5 38104 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                           |
173 | 6, 19, 21, 28, 30, 157, 171, 172 | etransclem32 38131 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
      |
174 | 173 | fveq1d 5867 |
. . . . . . . . . . . . . . . . . . . . . . 23
                       |
175 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
176 | 175 | fvmpt2 5957 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
         |
177 | 53, 176 | mpan2 677 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
178 | 174, 177 | sylan9eq 2505 |
. . . . . . . . . . . . . . . . . . . . . 22
 

        
       |
179 | | cnex 9620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
180 | 179 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
181 | | etransclem46.rex |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

  |
182 | 6, 181 | ssexd 4550 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
183 | | elpm2r 7489 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               |
184 | 180, 182,
46, 181, 183 | syl22anc 1269 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
185 | | dvn0 22878 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
             |
186 | 45, 184, 185 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
187 | 186 | fveq1d 5867 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
188 | 187 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
 

                  |
189 | 178, 188 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . . 21
 

         
                          |
190 | | df-neg 9863 |
. . . . . . . . . . . . . . . . . . . . 21
            |
191 | 189, 190 | syl6eqr 2503 |
. . . . . . . . . . . . . . . . . . . 20
 

         
                         |
192 | 191 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . 19
 

                                               |
193 | 137, 168,
192 | 3eqtrd 2489 |
. . . . . . . . . . . . . . . . . 18
 

      
                                             |
194 | 128, 132,
193 | 3eqtrd 2489 |
. . . . . . . . . . . . . . . . 17
 

                                                    |
195 | 194 | mpteq2dva 4489 |
. . . . . . . . . . . . . . . 16
                                                         |
196 | 14, 47 | mulneg2d 10072 |
. . . . . . . . . . . . . . . . 17
 

                        |
197 | 196 | mpteq2dva 4489 |
. . . . . . . . . . . . . . . 16
                             |
198 | 126, 195,
197 | 3eqtrd 2489 |
. . . . . . . . . . . . . . 15
                              |
199 | 6, 42, 49, 198 | dvmptneg 22920 |
. . . . . . . . . . . . . 14
                                |
200 | 199 | adantr 467 |
. . . . . . . . . . . . 13
 
                                    |
201 | | 0red 9644 |
. . . . . . . . . . . . . 14
 
       |
202 | | elfzelz 11800 |
. . . . . . . . . . . . . . . 16
       |
203 | 202 | zred 11040 |
. . . . . . . . . . . . . . 15
       |
204 | 203 | adantl 468 |
. . . . . . . . . . . . . 14
 
       |
205 | 201, 204 | iccssred 37602 |
. . . . . . . . . . . . 13
 
       ![[,] [,]](_icc.gif)    |
206 | | eqid 2451 |
. . . . . . . . . . . . . 14
  ℂfld   ℂfld |
207 | 206 | tgioo2 21821 |
. . . . . . . . . . . . 13
       ℂfld
↾t   |
208 | | 0red 9644 |
. . . . . . . . . . . . . . 15
       |
209 | | iccntr 21839 |
. . . . . . . . . . . . . . 15
 
       
      ![[,] [,]](_icc.gif)         |
210 | 208, 203,
209 | syl2anc 667 |
. . . . . . . . . . . . . 14
           
      ![[,] [,]](_icc.gif)         |
211 | 210 | adantl 468 |
. . . . . . . . . . . . 13
 
           
      ![[,] [,]](_icc.gif)         |
212 | 7, 44, 51, 200, 205, 207, 206, 211 | dvmptres2 22916 |
. . . . . . . . . . . 12
 
         ![[,] [,]](_icc.gif)                                   |
213 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
       |
214 | | elioore 11666 |
. . . . . . . . . . . . . . . . . . . 20
       |
215 | 214 | recnd 9669 |
. . . . . . . . . . . . . . . . . . 19
       |
216 | 215 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
 
       |
217 | 216 | negcld 9973 |
. . . . . . . . . . . . . . . . 17
 
        |
218 | 213, 217 | cxpcld 23653 |
. . . . . . . . . . . . . . . 16
 
           |
219 | 46 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
           |
220 | 214 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 
       |
221 | 219, 220 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . 16
 
           |
222 | 218, 221 | mulcld 9663 |
. . . . . . . . . . . . . . 15
 
                 |
223 | 222 | negnegd 9977 |
. . . . . . . . . . . . . 14
 
                             |
224 | 223 | mpteq2dva 4489 |
. . . . . . . . . . . . 13
                                     |
225 | 224 | adantr 467 |
. . . . . . . . . . . 12
 
                                         |
226 | 5, 212, 225 | 3eqtrd 2489 |
. . . . . . . . . . 11
 
                         |
227 | 226 | fveq1d 5867 |
. . . . . . . . . 10
 
                                 |
228 | 227 | adantr 467 |
. . . . . . . . 9
                                         |
229 | | simpr 463 |
. . . . . . . . . . 11
 
           |
230 | | eqid 2451 |
. . . . . . . . . . . 12
                                 |
231 | 230 | fvmpt2 5957 |
. . . . . . . . . . 11
                                                 |
232 | 229, 222,
231 | syl2anc 667 |
. . . . . . . . . 10
 
                                     |
233 | 232 | adantlr 721 |
. . . . . . . . 9
                                             |
234 | 228, 233 | eqtr2d 2486 |
. . . . . . . 8
                               |
235 | 234 | itgeq2d 37860 |
. . . . . . 7
 
                                     |
236 | | elfzle1 11802 |
. . . . . . . . 9
       |
237 | 236 | adantl 468 |
. . . . . . . 8
 
       |
238 | | eqid 2451 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)              |
239 | | eqidd 2452 |
. . . . . . . . . . . . . . . 16
     
  ![[,] [,]](_icc.gif)               |
240 | 86 | adantl 468 |
. . . . . . . . . . . . . . . 16
         ![[,] [,]](_icc.gif)              |
241 | 208, 203 | iccssred 37602 |
. . . . . . . . . . . . . . . . . . 19
       ![[,] [,]](_icc.gif)    |
242 | | ax-resscn 9596 |
. . . . . . . . . . . . . . . . . . 19
 |
243 | 241, 242 | syl6ss 3444 |
. . . . . . . . . . . . . . . . . 18
       ![[,] [,]](_icc.gif)    |
244 | 243 | sselda 3432 |
. . . . . . . . . . . . . . . . 17
     
  ![[,] [,]](_icc.gif)     |
245 | 244 | negcld 9973 |
. . . . . . . . . . . . . . . 16
     
  ![[,] [,]](_icc.gif)      |
246 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
   |
247 | | negcl 9875 |
. . . . . . . . . . . . . . . . . 18
    |
248 | 246, 247 | cxpcld 23653 |
. . . . . . . . . . . . . . . . 17
       |
249 | 244, 248 | syl 17 |
. . . . . . . . . . . . . . . 16
     
  ![[,] [,]](_icc.gif)         |
250 | 239, 240,
245, 249 | fvmptd 5954 |
. . . . . . . . . . . . . . 15
     
  ![[,] [,]](_icc.gif)                   |
251 | 250 | eqcomd 2457 |
. . . . . . . . . . . . . 14
     
  ![[,] [,]](_icc.gif)                   |
252 | 251 | adantll 720 |
. . . . . . . . . . . . 13
          ![[,] [,]](_icc.gif)                   |
253 | 252 | mpteq2dva 4489 |
. . . . . . . . . . . 12
 
        ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)               |
254 | | mnfxr 11414 |
. . . . . . . . . . . . . . . . . 18
 |
255 | 254 | a1i 11 |
. . . . . . . . . . . . . . . . 17

  |
256 | | 0red 9644 |
. . . . . . . . . . . . . . . . 17

  |
257 | | rpxr 11309 |
. . . . . . . . . . . . . . . . 17

  |
258 | | rpgt0 11313 |
. . . . . . . . . . . . . . . . 17

  |
259 | 255, 256,
257, 258 | gtnelioc 37587 |
. . . . . . . . . . . . . . . 16

 ![(,] (,]](_ioc.gif)    |
260 | 76, 259 | ax-mp 5 |
. . . . . . . . . . . . . . 15
 ![(,] (,]](_ioc.gif)   |
261 | | eldif 3414 |
. . . . . . . . . . . . . . 15
   ![(,] (,]](_ioc.gif)     ![(,] (,]](_ioc.gif)     |
262 | 9, 260, 261 | mpbir2an 931 |
. . . . . . . . . . . . . 14

 ![(,] (,]](_ioc.gif)    |
263 | | cxpcncf2 37778 |
. . . . . . . . . . . . . 14
   ![(,] (,]](_ioc.gif)  
           |
264 | 262, 263 | mp1i 13 |
. . . . . . . . . . . . 13
 
                |
265 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     |
266 | 265 | negcncf 21950 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)       |
267 | 243, 266 | syl 17 |
. . . . . . . . . . . . . 14
        ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)       |
268 | 267 | adantl 468 |
. . . . . . . . . . . . 13
 
        ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)       |
269 | 264, 268 | cncfmpt1f 21945 |
. . . . . . . . . . . 12
 
        ![[,] [,]](_icc.gif)    
           ![[,] [,]](_icc.gif)       |
270 | 253, 269 | eqeltrd 2529 |
. . . . . . . . . . 11
 
        ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       |
271 | 242 | a1i 11 |
. . . . . . . . . . . . . 14
          ![[,] [,]](_icc.gif)     |
272 | 21 | ad2antrr 732 |
. . . . . . . . . . . . . 14
          ![[,] [,]](_icc.gif)     |
273 | 28 | ad2antrr 732 |
. . . . . . . . . . . . . 14
          ![[,] [,]](_icc.gif)     |
274 | | etransclem6 38105 |
. . . . . . . . . . . . . . 15
                                             |
275 | 30, 274 | eqtri 2473 |
. . . . . . . . . . . . . 14
                       |
276 | 241 | sselda 3432 |
. . . . . . . . . . . . . . 15
     
  ![[,] [,]](_icc.gif)     |
277 | 276 | adantll 720 |
. . . . . . . . . . . . . 14
          ![[,] [,]](_icc.gif)     |
278 | 271, 272,
273, 275, 277 | etransclem13 38112 |
. . . . . . . . . . . . 13
          ![[,] [,]](_icc.gif)                            |
279 | 278 | mpteq2dva 4489 |
. . . . . . . . . . . 12
 
        ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                        |
280 | 243 | adantl 468 |
. . . . . . . . . . . . 13
 
       ![[,] [,]](_icc.gif)    |
281 | | fzfid 12186 |
. . . . . . . . . . . . 13
 
           |
282 | 277 | recnd 9669 |
. . . . . . . . . . . . . . . 16
          ![[,] [,]](_icc.gif)     |
283 | 282 | 3adant3 1028 |
. . . . . . . . . . . . . . 15
          ![[,] [,]](_icc.gif) 
       |
284 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . 17
       |
285 | 284 | zcnd 11041 |
. . . . . . . . . . . . . . . 16
       |
286 | 285 | 3ad2ant3 1031 |
. . . . . . . . . . . . . . 15
          ![[,] [,]](_icc.gif) 
       |
287 | 283, 286 | subcld 9986 |
. . . . . . . . . . . . . 14
          ![[,] [,]](_icc.gif) 
         |
288 | 21 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)     |
289 | 288, 150 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)   
   |
290 | 148 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)     |
291 | 289, 290 | ifcld 3924 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)            |
292 | 291 | 3adant3 1028 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif) 
              |
293 | 292 | 3adant1r 1261 |
. . . . . . . . . . . . . 14
          ![[,] [,]](_icc.gif) 
              |
294 | 287, 293 | expcld 12416 |
. . . . . . . . . . . . 13
          ![[,] [,]](_icc.gif) 
                    |
295 | | nfv 1761 |
. . . . . . . . . . . . . 14
   
           |
296 | 243 | adantr 467 |
. . . . . . . . . . . . . . . . 17
     
       ![[,] [,]](_icc.gif)    |
297 | | ssid 3451 |
. . . . . . . . . . . . . . . . . 18
 |
298 | 297 | a1i 11 |
. . . . . . . . . . . . . . . . 17
     
       |
299 | 296, 298 | idcncfg 37749 |
. . . . . . . . . . . . . . . 16
     
        ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
300 | 285 | adantl 468 |
. . . . . . . . . . . . . . . . 17
     
       |
301 | 296, 300,
298 | constcncfg 37748 |
. . . . . . . . . . . . . . . 16
     
        ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
302 | 299, 301 | subcncf 37746 |
. . . . . . . . . . . . . . 15
     
        ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       |
303 | 302 | adantll 720 |
. . . . . . . . . . . . . 14
                ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       |
304 | 151, 148 | ifcld 3924 |
. . . . . . . . . . . . . . . 16
          |
305 | | expcncf 21954 |
. . . . . . . . . . . . . . . 16
                           |
306 | 304, 305 | syl 17 |
. . . . . . . . . . . . . . 15
                    |
307 | 306 | ad2antrr 732 |
. . . . . . . . . . . . . 14
                                |
308 | 297 | a1i 11 |
. . . . . . . . . . . . . 14
               |
309 | | oveq1 6297 |
. . . . . . . . . . . . . 14
                             |
310 | 295, 303,
307, 308, 309 | cncfcompt2 37777 |
. . . . . . . . . . . . 13
                ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)       |
311 | 280, 281,
294, 310 | fprodcncf 37779 |
. . . . . . . . . . . 12
 
        ![[,] [,]](_icc.gif)                         ![[,] [,]](_icc.gif)       |
312 | 279, 311 | eqeltrd 2529 |
. . . . . . . . . . 11
 
        ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       |
313 | 270, 312 | mulcncf 22398 |
. . . . . . . . . 10
 
        ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)       |
314 | | ioossicc 11720 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)   |
315 | 314 | a1i 11 |
. . . . . . . . . 10
 
           ![[,] [,]](_icc.gif)    |
316 | 297 | a1i 11 |
. . . . . . . . . 10
 
       |
317 | 222 | adantlr 721 |
. . . . . . . . . 10
                         |
318 | 238, 313,
315, 316, 317 | cncfmptssg 37747 |
. . . . . . . . 9
 
                               |
319 | 226, 318 | eqeltrd 2529 |
. . . . . . . 8
 
                 |
320 | 19 | adantr 467 |
. . . . . . . . . 10
 
        ℂfld
↾t    |
321 | 21 | adantr 467 |
. . . . . . . . . 10
 
       |
322 | 28 | adantr 467 |
. . . . . . . . . 10
 
       |
323 | | oveq2 6298 |
. . . . . . . . . . . . . . 15
       |
324 | 323 | oveq1d 6305 |
. . . . . . . . . . . . . 14
               |
325 | 324 | cbvprodv 13970 |
. . . . . . . . . . . . 13
                         |
326 | 325 | oveq2i 6301 |
. . . . . . . . . . . 12
                        
                |
327 | 326 | mpteq2i 4486 |
. . . . . . . . . . 11
                                             |
328 | 30, 327 | eqtri 2473 |
. . . . . . . . . 10
                       |
329 | 7, 320, 321, 322, 328, 201, 204 | etransclem18 38117 |
. . . . . . . . 9
 
                        |
330 | 226, 329 | eqeltrd 2529 |
. . . . . . . 8
 
          |
331 | | eqid 2451 |
. . . . . . . . . . . 12
             |
332 | 6, 19, 21, 28, 30, 38 | etransclem43 38142 |
. . . . . . . . . . . . . 14
       |
333 | 119, 332 | eqeltrd 2529 |
. . . . . . . . . . . . 13
             |
334 | 333 | adantr 467 |
. . . . . . . . . . . 12
 
                 |
335 | 117 | ad2antrr 732 |
. . . . . . . . . . . . 13
          ![[,] [,]](_icc.gif)         |
336 | 335, 277 | ffvelrnd 6023 |
. . . . . . . . . . . 12
          ![[,] [,]](_icc.gif)         |
337 | 331, 334,
205, 316, 336 | cncfmptssg 37747 |
. . . . . . . . . . 11
 
        ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       |
338 | 270, 337 | mulcncf 22398 |
. . . . . . . . . 10
 
        ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)       |
339 | 338 | negcncfg 37758 |
. . . . . . . . 9
 
        ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)       |
340 | 3, 339 | syl5eqel 2533 |
. . . . . . . 8
 
        ![[,] [,]](_icc.gif)       |
341 | 201, 204,
237, 319, 330, 340 | ftc2 22996 |
. . . . . . 7
 
                              |
342 | 3 | a1i 11 |
. . . . . . . . . 10
 
        ![[,] [,]](_icc.gif)                |
343 | | negeq 9867 |
. . . . . . . . . . . . . 14
     |
344 | 343 | oveq2d 6306 |
. . . . . . . . . . . . 13
           |
345 | | fveq2 5865 |
. . . . . . . . . . . . 13
           |
346 | 344, 345 | oveq12d 6308 |
. . . . . . . . . . . 12
                       |
347 | 346 | negeqd 9869 |
. . . . . . . . . . 11
                         |
348 | 347 | adantl 468 |
. . . . . . . . . 10
                                 |
349 | 201 | rexrd 9690 |
. . . . . . . . . . 11
 
       |
350 | 204 | rexrd 9690 |
. . . . . . . . . . 11
 
       |
351 | | ubicc2 11749 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)    |
352 | 349, 350,
237, 351 | syl3anc 1268 |
. . . . . . . . . 10
 
       ![[,] [,]](_icc.gif)    |
353 | 9 | a1i 11 |
. . . . . . . . . . . . . 14
       |
354 | 203 | recnd 9669 |
. . . . . . . . . . . . . . 15
       |
355 | 354 | negcld 9973 |
. . . . . . . . . . . . . 14
        |
356 | 353, 355 | cxpcld 23653 |
. . . . . . . . . . . . 13
           |
357 | 356 | adantl 468 |
. . . . . . . . . . . 12
 
           |
358 | 117 | adantr 467 |
. . . . . . . . . . . . 13
 
           |
359 | 358, 204 | ffvelrnd 6023 |
. . . . . . . . . . . 12
 
           |
360 | 357, 359 | mulcld 9663 |
. . . . . . . . . . 11
 
                 |
361 | 360 | negcld 9973 |
. . . . . . . . . 10
 
                  |
362 | 342, 348,
352, 361 | fvmptd 5954 |
. . . . . . . . 9
 
                      |
363 | | negeq 9867 |
. . . . . . . . . . . . . . . 16
     |
364 | 363 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
           |
365 | | neg0 9920 |
. . . . . . . . . . . . . . . . 17
  |
366 | 365 | oveq2i 6301 |
. . . . . . . . . . . . . . . 16
        |
367 | | cxp0 23615 |
. . . . . . . . . . . . . . . . 17
      |
368 | 9, 367 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
    |
369 | 366, 368 | eqtri 2473 |
. . . . . . . . . . . . . . 15
     |
370 | 364, 369 | syl6eq 2501 |
. . . . . . . . . . . . . 14
       |
371 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
372 | 370, 371 | oveq12d 6308 |
. . . . . . . . . . . . 13
                   |
373 | | 0red 9644 |
. . . . . . . . . . . . . . 15
   |
374 | 117, 373 | ffvelrnd 6023 |
. . . . . . . . . . . . . 14
       |
375 | 374 | mulid2d 9661 |
. . . . . . . . . . . . 13
             |
376 | 372, 375 | sylan9eqr 2507 |
. . . . . . . . . . . 12
 
                 |
377 | 376 | negeqd 9869 |
. . . . . . . . . . 11
 
                   |
378 | 377 | adantlr 721 |
. . . . . . . . . 10
                           |
379 | | lbicc2 11748 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)    |
380 | 349, 350,
237, 379 | syl3anc 1268 |
. . . . . . . . . 10
 
       ![[,] [,]](_icc.gif)    |
381 | 374 | negcld 9973 |
. . . . . . . . . . 11
        |
382 | 381 | adantr 467 |
. . . . . . . . . 10
 
            |
383 | 342, 378,
380, 382 | fvmptd 5954 |
. . . . . . . . 9
 
                |
384 | 362, 383 | oveq12d 6308 |
. . . . . . . 8
 
                                   |
385 | 374 | adantr 467 |
. . . . . . . . 9
 
           |
386 | 361, 385 | subnegd 9993 |
. . . . . . . 8
 
                                          |
387 | 361, 385 | addcomd 9835 |
. . . . . . . . 9
 
                                         |
388 | 385, 360 | negsubd 9992 |
. . . . . . . . 9
 
                                        |
389 | 387, 388 | eqtrd 2485 |
. . . . . . . 8
 
                                        |
390 | 384, 386,
389 | 3eqtrd 2489 |
. . . . . . 7
 
                                 |
391 | 235, 341,
390 | 3eqtrd 2489 |
. . . . . 6
 
                                        |
392 | 391 | oveq2d 6306 |
. . . . 5
 
                                                              |
393 | 25 | adantr 467 |
. . . . . . . . . 10
 
     Poly    |
394 | | 0zd 10949 |
. . . . . . . . . 10
 
       |
395 | | etransclem46.a |
. . . . . . . . . . 11
coeff   |
396 | 395 | coef2 23185 |
. . . . . . . . . 10
  Poly 
       |
397 | 393, 394,
396 | syl2anc 667 |
. . . . . . . . 9
 
           |
398 | | elfznn0 11887 |
. . . . . . . . . 10
       |
399 | 398 | adantl 468 |
. . . . . . . . 9
 
       |
400 | 397, 399 | ffvelrnd 6023 |
. . . . . . . 8
 
           |
401 | 400 | zcnd 11041 |
. . . . . . 7
 
           |
402 | 353, 354 | cxpcld 23653 |
. . . . . . . 8
          |
403 | 402 | adantl 468 |
. . . . . . 7
 
          |
404 | 401, 403 | mulcld 9663 |
. . . . . 6
 
                |
405 | 404, 385,
360 | subdid 10074 |
. . . . 5
 
                                                                        |
406 | 392, 405 | eqtrd 2485 |
. . . 4
 
                                                                         |
407 | 406 | sumeq2dv 13769 |
. . 3
                                                                                 |
408 | | fzfid 12186 |
. . . . 5
       |
409 | 404, 385 | mulcld 9663 |
. . . . 5
 
                      |
410 | 404, 360 | mulcld 9663 |
. . . . 5
 
                            |
411 | 408, 409,
410 | fsumsub 13849 |
. . . 4
                                                                                                 |
412 | | etransclem46.qe0 |
. . . . . . . . 9
    
  |
413 | 412 | eqcomd 2457 |
. . . . . . . 8
       |
414 | 395, 23 | coeid2 23193 |
. . . . . . . . 9
  Poly 

                      |
415 | 25, 9, 414 | sylancl 668 |
. . . . . . . 8
    
                  |
416 | | cxpexp 23613 |
. . . . . . . . . . . . 13
 
          |
417 | 353, 398,
416 | syl2anc 667 |
. . . . . . . . . . . 12
              |
418 | 417 | eqcomd 2457 |
. . . . . . . . . . 11
              |
419 | 418 | oveq2d 6306 |
. . . . . . . . . 10
                          |
420 | 419 | adantl 468 |
. . . . . . . . 9
 
                          |
421 | 420 | sumeq2dv 13769 |
. . . . . . . 8
                                  |
422 | 413, 415,
421 | 3eqtrd 2489 |
. . . . . . 7
                  |
423 | 422 | oveq1d 6305 |
. . . . . 6
        
                     |
424 | 374 | mul02d 9831 |
. . . . . 6
         |
425 | 408, 374,
404 | fsummulc1 13846 |
. . . . . 6
                                             |
426 | 423, 424,
425 | 3eqtr3rd 2494 |
. . . . 5
                        |
427 | 38 | a1i 11 |
. . . . . . . . . . 11
 
                           |
428 | | fveq2 5865 |
. . . . . . . . . . . . 13
                           |
429 | 428 | sumeq2sdv 13770 |
. . . . . . . . . . . 12
                                       |
430 | 429 | adantl 468 |
. . . . . . . . . . 11
                                               |
431 | | fzfid 12186 |
. . . . . . . . . . . 12
 
           |
432 | 33 | adantlr 721 |
. . . . . . . . . . . . 13
                           |
433 | 204 | adantr 467 |
. . . . . . . . . . . . 13
               |
434 | 432, 433 | ffvelrnd 6023 |
. . . . . . . . . . . 12
                           |
435 | 431, 434 | fsumcl 13799 |
. . . . . . . . . . 11
 
                         |
436 | 427, 430,
204, 435 | fvmptd 5954 |
. . . . . . . . . 10
 
                             |
437 | 436 | oveq2d 6306 |
. . . . . . . . 9
 
                    
                    |
438 | 437 | oveq2d 6306 |
. . . . . . . 8
 
                                         
                     |
439 | 357, 435 | mulcld 9663 |
. . . . . . . . 9
 
          
                    |
440 | 401, 403,
439 | mulassd 9666 |
. . . . . . . 8
 
                    
                                 
                      |
441 | 368 | eqcomi 2460 |
. . . . . . . . . . . . . . 15
    |
442 | 441 | a1i 11 |
. . . . . . . . . . . . . 14
          |
443 | 354 | negidd 9976 |
. . . . . . . . . . . . . . . 16
          |
444 | 443 | eqcomd 2457 |
. . . . . . . . . . . . . . 15
          |
445 | 444 | oveq2d 6306 |
. . . . . . . . . . . . . 14
                |
446 | 53, 54 | gtneii 9746 |
. . . . . . . . . . . . . . . 16
 |
447 | 446 | a1i 11 |
. . . . . . . . . . . . . . 15
       |
448 | 353, 447,
354, 355 | cxpaddd 23662 |
. . . . . . . . . . . . . 14
                      |
449 | 442, 445,
448 | 3eqtrd 2489 |
. . . . . . . . . . . . 13
                |
450 | 449 | oveq1d 6305 |
. . . . . . . . . . . 12
                                   
                    |
451 | 450 | adantl 468 |
. . . . . . . . . . 11
 
                                   
                    |
452 | 435 | mulid2d 9661 |
. . . . . . . . . . 11
 
                                             |
453 | 403, 357,
435 | mulassd 9666 |
. . . . . . . . . . 11
 
                                                                 |
454 | 451, 452,
453 | 3eqtr3rd 2494 |
. . . . . . . . . 10
 
              
                              |