Step | Hyp | Ref
| Expression |
1 | | fsummulc2.2 |
. . . 4
   |
2 | 1 | mul01d 8340 |
. . 3
     |
3 | | sumeq1 11347 |
. . . . . 6


   |
4 | | sum0 11380 |
. . . . . 6
  |
5 | 3, 4 | eqtrdi 2226 |
. . . . 5


  |
6 | 5 | oveq2d 5885 |
. . . 4

       |
7 | | sumeq1 11347 |
. . . . 5


  
    |
8 | | sum0 11380 |
. . . . 5
    |
9 | 7, 8 | eqtrdi 2226 |
. . . 4


    |
10 | 6, 9 | eqeq12d 2192 |
. . 3

  
  
      |
11 | 2, 10 | syl5ibrcom 157 |
. 2
   
 
     |
12 | | addcl 7927 |
. . . . . . . . 9
 
     |
13 | 12 | adantl 277 |
. . . . . . . 8
    ♯       ♯              |
14 | 1 | ad2antrr 488 |
. . . . . . . . 9
    ♯       ♯         
  |
15 | | simprl 529 |
. . . . . . . . 9
    ♯       ♯         
  |
16 | | simprr 531 |
. . . . . . . . 9
    ♯       ♯            |
17 | 14, 15, 16 | adddid 7972 |
. . . . . . . 8
    ♯       ♯                      |
18 | | simprl 529 |
. . . . . . . . 9
 
 ♯       ♯       ♯    |
19 | | nnuz 9552 |
. . . . . . . . 9
     |
20 | 18, 19 | eleqtrdi 2270 |
. . . . . . . 8
 
 ♯       ♯       ♯        |
21 | | elnnuz 9553 |
. . . . . . . . . . . 12

      |
22 | 21 | biimpri 133 |
. . . . . . . . . . 11
    
  |
23 | 22 | adantl 277 |
. . . . . . . . . 10
    ♯       ♯           
  |
24 | | f1of 5457 |
. . . . . . . . . . . . . . 15
      ♯          ♯       |
25 | 24 | ad2antll 491 |
. . . . . . . . . . . . . 14
 
 ♯       ♯            ♯       |
26 | 25 | ad2antrr 488 |
. . . . . . . . . . . . 13
     ♯       ♯           
♯        ♯       |
27 | | 1zzd 9269 |
. . . . . . . . . . . . . . 15
     ♯       ♯           
♯     |
28 | 18 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
     ♯       ♯           
♯   ♯    |
29 | 28 | nnzd 9363 |
. . . . . . . . . . . . . . 15
     ♯       ♯           
♯   ♯    |
30 | | eluzelz 9526 |
. . . . . . . . . . . . . . . 16
    
  |
31 | 30 | ad2antlr 489 |
. . . . . . . . . . . . . . 15
     ♯       ♯           
♯  
  |
32 | 27, 29, 31 | 3jca 1177 |
. . . . . . . . . . . . . 14
     ♯       ♯           
♯    ♯     |
33 | | eluzle 9529 |
. . . . . . . . . . . . . . . 16
    
  |
34 | 33 | ad2antlr 489 |
. . . . . . . . . . . . . . 15
     ♯       ♯           
♯  
  |
35 | | simpr 110 |
. . . . . . . . . . . . . . 15
     ♯       ♯           
♯   ♯    |
36 | 34, 35 | jca 306 |
. . . . . . . . . . . . . 14
     ♯       ♯           
♯   
♯     |
37 | | elfz2 10002 |
. . . . . . . . . . . . . 14
    ♯     ♯    ♯      |
38 | 32, 36, 37 | sylanbrc 417 |
. . . . . . . . . . . . 13
     ♯       ♯           
♯  
   ♯     |
39 | | fvco3 5583 |
. . . . . . . . . . . . 13
       ♯    
   ♯                        |
40 | 26, 38, 39 | syl2anc 411 |
. . . . . . . . . . . 12
     ♯       ♯           
♯                       |
41 | 26, 38 | ffvelcdmd 5648 |
. . . . . . . . . . . . . 14
     ♯       ♯           
♯         |
42 | | fsummulc2.3 |
. . . . . . . . . . . . . . . . 17
 
   |
43 | 42 | ralrimiva 2550 |
. . . . . . . . . . . . . . . 16
 
  |
44 | 43 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
     ♯       ♯           
♯   
  |
45 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . 17
        ![]_ ]_](_urbrack.gif)  |
46 | 45 | nfel1 2330 |
. . . . . . . . . . . . . . . 16
        ![]_ ]_](_urbrack.gif)
 |
47 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . 17
           ![]_ ]_](_urbrack.gif)   |
48 | 47 | eleq1d 2246 |
. . . . . . . . . . . . . . . 16
     
      ![]_ ]_](_urbrack.gif)    |
49 | 46, 48 | rspc 2835 |
. . . . . . . . . . . . . . 15
      
      ![]_ ]_](_urbrack.gif)
   |
50 | 41, 44, 49 | sylc 62 |
. . . . . . . . . . . . . 14
     ♯       ♯           
♯         ![]_ ]_](_urbrack.gif)
  |
51 | | eqid 2177 |
. . . . . . . . . . . . . . 15
     |
52 | 51 | fvmpts 5590 |
. . . . . . . . . . . . . 14
            ![]_ ]_](_urbrack.gif)
                 ![]_ ]_](_urbrack.gif)   |
53 | 41, 50, 52 | syl2anc 411 |
. . . . . . . . . . . . 13
     ♯       ♯           
♯                   ![]_ ]_](_urbrack.gif)   |
54 | 53, 50 | eqeltrd 2254 |
. . . . . . . . . . . 12
     ♯       ♯           
♯               |
55 | 40, 54 | eqeltrd 2254 |
. . . . . . . . . . 11
     ♯       ♯           
♯             |
56 | | 0cnd 7941 |
. . . . . . . . . . 11
     ♯       ♯           
♯  
  |
57 | 23 | nnzd 9363 |
. . . . . . . . . . . 12
    ♯       ♯           
  |
58 | 18 | adantr 276 |
. . . . . . . . . . . . 13
    ♯       ♯           
♯    |
59 | 58 | nnzd 9363 |
. . . . . . . . . . . 12
    ♯       ♯           
♯    |
60 | | zdcle 9318 |
. . . . . . . . . . . 12
  ♯  
DECID
♯    |
61 | 57, 59, 60 | syl2anc 411 |
. . . . . . . . . . 11
    ♯       ♯           
DECID
♯    |
62 | 55, 56, 61 | ifcldadc 3563 |
. . . . . . . . . 10
    ♯       ♯           
 
♯               |
63 | | breq1 4003 |
. . . . . . . . . . . 12
 
♯ 
♯     |
64 | | fveq2 5511 |
. . . . . . . . . . . 12
                   |
65 | 63, 64 | ifbieq1d 3556 |
. . . . . . . . . . 11
  
♯               ♯               |
66 | | eqid 2177 |
. . . . . . . . . . 11
  
♯                 ♯               |
67 | 65, 66 | fvmptg 5588 |
. . . . . . . . . 10
    ♯                  ♯                   ♯               |
68 | 23, 62, 67 | syl2anc 411 |
. . . . . . . . 9
    ♯       ♯           
    ♯                   ♯               |
69 | 68, 62 | eqeltrd 2254 |
. . . . . . . 8
    ♯       ♯           
    ♯                   |
70 | | csbov2g 5910 |
. . . . . . . . . . . 12
           ![]_ ]_](_urbrack.gif) 
        ![]_ ]_](_urbrack.gif)    |
71 | 41, 70 | syl 14 |
. . . . . . . . . . 11
     ♯       ♯           
♯         ![]_ ]_](_urbrack.gif) 
        ![]_ ]_](_urbrack.gif)    |
72 | 35 | iftrued 3541 |
. . . . . . . . . . . 12
     ♯       ♯           
♯     ♯                           |
73 | | fvco3 5583 |
. . . . . . . . . . . . 13
       ♯    
   ♯                            |
74 | 26, 38, 73 | syl2anc 411 |
. . . . . . . . . . . 12
     ♯       ♯           
♯                           |
75 | 1 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
     ♯       ♯           
♯  
  |
76 | 75, 50 | mulcld 7968 |
. . . . . . . . . . . . . 14
     ♯       ♯           
♯          ![]_ ]_](_urbrack.gif)    |
77 | 71, 76 | eqeltrd 2254 |
. . . . . . . . . . . . 13
     ♯       ♯           
♯         ![]_ ]_](_urbrack.gif) 
   |
78 | | eqid 2177 |
. . . . . . . . . . . . . 14
         |
79 | 78 | fvmpts 5590 |
. . . . . . . . . . . . 13
            ![]_ ]_](_urbrack.gif) 
                    ![]_ ]_](_urbrack.gif)     |
80 | 41, 77, 79 | syl2anc 411 |
. . . . . . . . . . . 12
     ♯       ♯           
♯                     ![]_ ]_](_urbrack.gif) 
   |
81 | 72, 74, 80 | 3eqtrd 2214 |
. . . . . . . . . . 11
     ♯       ♯           
♯     ♯                     ![]_ ]_](_urbrack.gif)     |
82 | 35 | iftrued 3541 |
. . . . . . . . . . . . 13
     ♯       ♯           
♯     ♯                       |
83 | 82, 40, 53 | 3eqtrd 2214 |
. . . . . . . . . . . 12
     ♯       ♯           
♯     ♯                   ![]_ ]_](_urbrack.gif)   |
84 | 83 | oveq2d 5885 |
. . . . . . . . . . 11
     ♯       ♯           
♯     
♯                     ![]_ ]_](_urbrack.gif)    |
85 | 71, 81, 84 | 3eqtr4d 2220 |
. . . . . . . . . 10
     ♯       ♯           
♯     ♯                  ♯                |
86 | 1 | ad3antrrr 492 |
. . . . . . . . . . . 12
     ♯       ♯           
♯  
  |
87 | 86 | mul01d 8340 |
. . . . . . . . . . 11
     ♯       ♯           
♯  
    |
88 | | simpr 110 |
. . . . . . . . . . . . 13
     ♯       ♯           
♯  
♯    |
89 | 88 | iffalsed 3544 |
. . . . . . . . . . . 12
     ♯       ♯           
♯  
 
♯               |
90 | 89 | oveq2d 5885 |
. . . . . . . . . . 11
     ♯       ♯           
♯  
   ♯                  |
91 | 88 | iffalsed 3544 |
. . . . . . . . . . 11
     ♯       ♯           
♯  
 
♯                 |
92 | 87, 90, 91 | 3eqtr4rd 2221 |
. . . . . . . . . 10
     ♯       ♯           
♯  
 
♯                 
♯                |
93 | | exmiddc 836 |
. . . . . . . . . . 11
DECID ♯   ♯  ♯     |
94 | 61, 93 | syl 14 |
. . . . . . . . . 10
    ♯       ♯           
 ♯  ♯     |
95 | 85, 92, 94 | mpjaodan 798 |
. . . . . . . . 9
    ♯       ♯           
 
♯                 
♯                |
96 | 80, 77 | eqeltrd 2254 |
. . . . . . . . . . . 12
     ♯       ♯           
♯                 |
97 | 74, 96 | eqeltrd 2254 |
. . . . . . . . . . 11
     ♯       ♯           
♯               |
98 | 97, 56, 61 | ifcldadc 3563 |
. . . . . . . . . 10
    ♯       ♯           
 
♯                 |
99 | | fveq2 5511 |
. . . . . . . . . . . 12
                       |
100 | 63, 99 | ifbieq1d 3556 |
. . . . . . . . . . 11
  
♯                 ♯                 |
101 | | eqid 2177 |
. . . . . . . . . . 11
  
♯                   ♯                 |
102 | 100, 101 | fvmptg 5588 |
. . . . . . . . . 10
    ♯                    ♯                     ♯                 |
103 | 23, 98, 102 | syl2anc 411 |
. . . . . . . . 9
    ♯       ♯           
    ♯                     ♯                 |
104 | 68 | oveq2d 5885 |
. . . . . . . . 9
    ♯       ♯           
     ♯                    
♯                |
105 | 95, 103, 104 | 3eqtr4d 2220 |
. . . . . . . 8
    ♯       ♯           
    ♯                        ♯                    |
106 | | mulcl 7929 |
. . . . . . . . 9
 
     |
107 | 106 | adantl 277 |
. . . . . . . 8
    ♯       ♯              |
108 | 1 | adantr 276 |
. . . . . . . 8
 
 ♯       ♯      
  |
109 | 13, 17, 20, 69, 105, 107, 108 | seq3distr 10499 |
. . . . . . 7
 
 ♯       ♯            ♯                   ♯         ♯                 ♯      |
110 | | fveq2 5511 |
. . . . . . . 8
                           |
111 | | simprr 531 |
. . . . . . . 8
 
 ♯       ♯            ♯       |
112 | 1 | adantr 276 |
. . . . . . . . . . . 12
 
   |
113 | 112, 42 | mulcld 7968 |
. . . . . . . . . . 11
 
 
   |
114 | 113 | fmpttd 5667 |
. . . . . . . . . 10
           |
115 | 114 | adantr 276 |
. . . . . . . . 9
 
 ♯       ♯                 |
116 | 115 | ffvelcdmda 5647 |
. . . . . . . 8
    ♯       ♯                  |
117 | | fvco3 5583 |
. . . . . . . . 9
       ♯    
   ♯                            |
118 | 25, 117 | sylan 283 |
. . . . . . . 8
    ♯       ♯          ♯                            |
119 | 110, 18, 111, 116, 118 | fsum3 11379 |
. . . . . . 7
 
 ♯       ♯                     ♯                   ♯     |
120 | | fveq2 5511 |
. . . . . . . . 9
                       |
121 | 42 | fmpttd 5667 |
. . . . . . . . . . 11
         |
122 | 121 | adantr 276 |
. . . . . . . . . 10
 
 ♯       ♯               |
123 | 122 | ffvelcdmda 5647 |
. . . . . . . . 9
    ♯       ♯                |
124 | | fvco3 5583 |
. . . . . . . . . 10
       ♯    
   ♯                        |
125 | 25, 124 | sylan 283 |
. . . . . . . . 9
    ♯       ♯          ♯                        |
126 | 120, 18, 111, 123, 125 | fsum3 11379 |
. . . . . . . 8
 
 ♯       ♯                   ♯                 ♯     |
127 | 126 | oveq2d 5885 |
. . . . . . 7
 
 ♯       ♯                      ♯                 ♯      |
128 | 109, 119,
127 | 3eqtr4rd 2221 |
. . . . . 6
 
 ♯       ♯                
          |
129 | | sumfct 11366 |
. . . . . . . . 9
 
          |
130 | 43, 129 | syl 14 |
. . . . . . . 8
 
      
  |
131 | 130 | oveq2d 5885 |
. . . . . . 7
               |
132 | 131 | adantr 276 |
. . . . . 6
 
 ♯       ♯                     |
133 | 113 | ralrimiva 2550 |
. . . . . . . 8
  
   |
134 | | sumfct 11366 |
. . . . . . . 8
 


          
   |
135 | 133, 134 | syl 14 |
. . . . . . 7
 
        

   |
136 | 135 | adantr 276 |
. . . . . 6
 
 ♯       ♯                
    |
137 | 128, 132,
136 | 3eqtr3d 2218 |
. . . . 5
 
 ♯       ♯        
 
    |
138 | 137 | expr 375 |
. . . 4
 
♯         ♯      
 
     |
139 | 138 | exlimdv 1819 |
. . 3
 
♯          ♯    
   

    |
140 | 139 | expimpd 363 |
. 2
   ♯        ♯      
   
    |
141 | | fsummulc2.1 |
. . 3
   |
142 | | fz1f1o 11367 |
. . 3
 
 ♯        ♯         |
143 | 141, 142 | syl 14 |
. 2
   ♯        ♯         |
144 | 11, 140, 143 | mpjaod 718 |
1
  
 
    |