Step | Hyp | Ref
| Expression |
1 | | sum0 11049 |
. . . 4
  |
2 | | fsumf1o.3 |
. . . . . . . 8
       |
3 | | f1oeq2 5315 |
. . . . . . . 8

            |
4 | 2, 3 | syl5ibcom 154 |
. . . . . . 7
         |
5 | 4 | imp 123 |
. . . . . 6
 

      |
6 | | f1ofo 5330 |
. . . . . 6
           |
7 | | fo00 5359 |
. . . . . . 7
    
    |
8 | 7 | simprbi 271 |
. . . . . 6
    
  |
9 | 5, 6, 8 | 3syl 17 |
. . . . 5
 

  |
10 | 9 | sumeq1d 11027 |
. . . 4
 

 
  |
11 | | simpr 109 |
. . . . . 6
 

  |
12 | 11 | sumeq1d 11027 |
. . . . 5
 

    |
13 | | sum0 11049 |
. . . . 5
  |
14 | 12, 13 | syl6eq 2163 |
. . . 4
 

   |
15 | 1, 10, 14 | 3eqtr4a 2173 |
. . 3
 

    |
16 | 15 | ex 114 |
. 2
  
    |
17 | | 2fveq3 5380 |
. . . . . . . 8
                               |
18 | | simprl 503 |
. . . . . . . 8
 
 ♯       ♯       ♯    |
19 | | simprr 504 |
. . . . . . . 8
 
 ♯       ♯            ♯       |
20 | | f1of 5323 |
. . . . . . . . . . . 12
    
      |
21 | 2, 20 | syl 14 |
. . . . . . . . . . 11
       |
22 | 21 | ffvelrnda 5509 |
. . . . . . . . . 10
 
       |
23 | | fsumf1o.5 |
. . . . . . . . . . . 12
 
   |
24 | 23 | fmpttd 5529 |
. . . . . . . . . . 11
         |
25 | 24 | ffvelrnda 5509 |
. . . . . . . . . 10
 
    
            |
26 | 22, 25 | syldan 278 |
. . . . . . . . 9
 
             |
27 | 26 | adantlr 466 |
. . . . . . . 8
    ♯       ♯                    |
28 | 2 | adantr 272 |
. . . . . . . . . . . 12
 
 ♯       ♯             |
29 | | f1oco 5346 |
. . . . . . . . . . . 12
           ♯      
      ♯       |
30 | 28, 19, 29 | syl2anc 406 |
. . . . . . . . . . 11
 
 ♯       ♯              ♯       |
31 | | f1of 5323 |
. . . . . . . . . . 11
        ♯            ♯       |
32 | 30, 31 | syl 14 |
. . . . . . . . . 10
 
 ♯       ♯              ♯       |
33 | | fvco3 5446 |
. . . . . . . . . 10
         ♯    
   ♯                            |
34 | 32, 33 | sylan 279 |
. . . . . . . . 9
    ♯       ♯          ♯                            |
35 | | f1of 5323 |
. . . . . . . . . . . 12
      ♯          ♯       |
36 | 35 | ad2antll 480 |
. . . . . . . . . . 11
 
 ♯       ♯            ♯       |
37 | | fvco3 5446 |
. . . . . . . . . . 11
       ♯    
   ♯                    |
38 | 36, 37 | sylan 279 |
. . . . . . . . . 10
    ♯       ♯          ♯                    |
39 | 38 | fveq2d 5379 |
. . . . . . . . 9
    ♯       ♯          ♯                                |
40 | 34, 39 | eqtrd 2147 |
. . . . . . . 8
    ♯       ♯          ♯                              |
41 | 17, 18, 19, 27, 40 | fsum3 11048 |
. . . . . . 7
 
 ♯       ♯                       ♯                   ♯     |
42 | | eqid 2115 |
. . . . . . . . . . . . 13
     |
43 | | fsumf1o.1 |
. . . . . . . . . . . . 13
   |
44 | | fsumf1o.4 |
. . . . . . . . . . . . . 14
 
       |
45 | 21 | ffvelrnda 5509 |
. . . . . . . . . . . . . 14
 
       |
46 | 44, 45 | eqeltrrd 2192 |
. . . . . . . . . . . . 13
 
   |
47 | 43 | eleq1d 2183 |
. . . . . . . . . . . . . 14
 
   |
48 | 23 | ralrimiva 2479 |
. . . . . . . . . . . . . . 15
 
  |
49 | 48 | adantr 272 |
. . . . . . . . . . . . . 14
 
 
  |
50 | 47, 49, 46 | rspcdva 2765 |
. . . . . . . . . . . . 13
 
   |
51 | 42, 43, 46, 50 | fvmptd3 5468 |
. . . . . . . . . . . 12
 
         |
52 | 44 | fveq2d 5379 |
. . . . . . . . . . . 12
 
                   |
53 | | simpr 109 |
. . . . . . . . . . . . 13
 
   |
54 | | eqid 2115 |
. . . . . . . . . . . . . 14
     |
55 | 54 | fvmpt2 5458 |
. . . . . . . . . . . . 13
 
         |
56 | 53, 50, 55 | syl2anc 406 |
. . . . . . . . . . . 12
 
         |
57 | 51, 52, 56 | 3eqtr4rd 2158 |
. . . . . . . . . . 11
 
                   |
58 | 57 | ralrimiva 2479 |
. . . . . . . . . 10
                    |
59 | | nffvmpt1 5386 |
. . . . . . . . . . . 12
         |
60 | 59 | nfeq1 2265 |
. . . . . . . . . . 11
                   |
61 | | fveq2 5375 |
. . . . . . . . . . . 12
               |
62 | | 2fveq3 5380 |
. . . . . . . . . . . 12
                       |
63 | 61, 62 | eqeq12d 2129 |
. . . . . . . . . . 11
                                     |
64 | 60, 63 | rspc 2754 |
. . . . . . . . . 10
  
               
                   |
65 | 58, 64 | mpan9 277 |
. . . . . . . . 9
 
                   |
66 | 65 | adantlr 466 |
. . . . . . . 8
    ♯       ♯                          |
67 | 66 | sumeq2dv 11029 |
. . . . . . 7
 
 ♯       ♯              
            |
68 | | fveq2 5375 |
. . . . . . . 8
                           |
69 | 24 | adantr 272 |
. . . . . . . . 9
 
 ♯       ♯               |
70 | 69 | ffvelrnda 5509 |
. . . . . . . 8
    ♯       ♯                |
71 | 68, 18, 30, 70, 34 | fsum3 11048 |
. . . . . . 7
 
 ♯       ♯                   ♯                   ♯     |
72 | 41, 67, 71 | 3eqtr4rd 2158 |
. . . . . 6
 
 ♯       ♯              
        |
73 | | sumfct 11035 |
. . . . . . . 8
 
          |
74 | 48, 73 | syl 14 |
. . . . . . 7
 
      
  |
75 | 74 | adantr 272 |
. . . . . 6
 
 ♯       ♯              
  |
76 | 50 | ralrimiva 2479 |
. . . . . . . 8
 
  |
77 | | sumfct 11035 |
. . . . . . . 8
 
       
  |
78 | 76, 77 | syl 14 |
. . . . . . 7
 
         |
79 | 78 | adantr 272 |
. . . . . 6
 
 ♯       ♯              
  |
80 | 72, 75, 79 | 3eqtr3d 2155 |
. . . . 5
 
 ♯       ♯           |
81 | 80 | expr 370 |
. . . 4
 
♯         ♯          |
82 | 81 | exlimdv 1773 |
. . 3
 
♯          ♯    
     |
83 | 82 | expimpd 358 |
. 2
   ♯        ♯      
    |
84 | | fsumf1o.2 |
. . 3
   |
85 | | fz1f1o 11036 |
. . 3
 
 ♯        ♯         |
86 | 84, 85 | syl 14 |
. 2
   ♯        ♯         |
87 | 16, 83, 86 | mpjaod 690 |
1
 
   |