Step | Hyp | Ref
| Expression |
1 | | df-ov 6311 |
. 2
 FinSum  FinSum       |
2 | | df-bj-finsum 31771 |
. . . 4
FinSum       CMnd 
                            
                                 |
3 | 2 | a1i 11 |
. . 3
 FinSum     
 CMnd                              
                                  |
4 | | simpr 468 |
. . . . . . . . . 10
 
         |
5 | 4 | fveq2d 5883 |
. . . . . . . . 9
 
                 |
6 | | bj-finsumval0.1 |
. . . . . . . . . . 11
 CMnd |
7 | 6 | adantr 472 |
. . . . . . . . . 10
 
    CMnd |
8 | | bj-finsumval0.3 |
. . . . . . . . . . . 12
           |
9 | | bj-finsumval0.2 |
. . . . . . . . . . . 12
   |
10 | | fex 6155 |
. . . . . . . . . . . 12
             |
11 | 8, 9, 10 | syl2anc 673 |
. . . . . . . . . . 11
   |
12 | 11 | adantr 472 |
. . . . . . . . . 10
 
      |
13 | | op1stg 6824 |
. . . . . . . . . 10
  CMnd           |
14 | 7, 12, 13 | syl2anc 673 |
. . . . . . . . 9
 
             |
15 | 5, 14 | eqtrd 2505 |
. . . . . . . 8
 
          |
16 | 4 | fveq2d 5883 |
. . . . . . . . 9
 
                 |
17 | | op2ndg 6825 |
. . . . . . . . . 10
  CMnd           |
18 | 7, 12, 17 | syl2anc 673 |
. . . . . . . . 9
 
             |
19 | 16, 18 | eqtrd 2505 |
. . . . . . . 8
 
          |
20 | 19 | dmeqd 5042 |
. . . . . . . . 9
 
   
      |
21 | | fdm 5745 |
. . . . . . . . . . 11
           |
22 | 8, 21 | syl 17 |
. . . . . . . . . 10
   |
23 | 22 | adantr 472 |
. . . . . . . . 9
 
   
  |
24 | 20, 23 | eqtrd 2505 |
. . . . . . . 8
 
   
      |
25 | | f1oeq3 5820 |
. . . . . . . . . . . . . . 15
                             |
26 | 25 | biimpd 212 |
. . . . . . . . . . . . . 14
                 
           |
27 | 26 | ad2antll 743 |
. . . . . . . . . . . . 13
                
            
           |
28 | 27 | adantrd 475 |
. . . . . . . . . . . 12
                
             
                             
           |
29 | 28 | adantr 472 |
. . . . . . . . . . 11
                                
                             
           |
30 | | eqidd 2472 |
. . . . . . . . . . . . . . . . 17
                                   |
31 | | simprl 772 |
. . . . . . . . . . . . . . . . . . 19
                                     |
32 | 31 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . 18
                                           |
33 | 32 | adantrr 731 |
. . . . . . . . . . . . . . . . 17
                                 
           |
34 | | simprrl 782 |
. . . . . . . . . . . . . . . . . . . . 21
                                     |
35 | 34 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
              
                        |
36 | 35 | fveq1d 5881 |
. . . . . . . . . . . . . . . . . . 19
              
                                        |
37 | 36 | mpteq2dva 4482 |
. . . . . . . . . . . . . . . . . 18
                                                         |
38 | 37 | adantrr 731 |
. . . . . . . . . . . . . . . . 17
                                                           |
39 | 30, 33, 38 | seqeq123d 12260 |
. . . . . . . . . . . . . . . 16
                                                                               |
40 | | simpr 468 |
. . . . . . . . . . . . . . . . . 18
                     |
41 | | simprr 774 |
. . . . . . . . . . . . . . . . . . 19
                
      |
42 | 41 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
                         |
43 | 40, 42 | jca 541 |
. . . . . . . . . . . . . . . . 17
                           |
44 | | hashfz1 12567 |
. . . . . . . . . . . . . . . . . . . . 21

          |
45 | 44 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . 20

          |
46 | 45 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . 19
              
     
          |
47 | | fzfid 12224 |
. . . . . . . . . . . . . . . . . . . . . 22
             
       |
48 | | f1ofo 5835 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
              |
49 | 48 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
               |
50 | | fornex 6781 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 
       |
51 | 47, 49, 50 | sylc 61 |
. . . . . . . . . . . . . . . . . . . . . 22
             
       |
52 | 47, 51 | jca 541 |
. . . . . . . . . . . . . . . . . . . . 21
             
             |
53 | 52 | adantrr 731 |
. . . . . . . . . . . . . . . . . . . 20
              
     
    
       |
54 | | 19.8a 1955 |
. . . . . . . . . . . . . . . . . . . . 21
            
               |
55 | 54 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
              
     
               |
56 | | hasheqf1oi 12572 |
. . . . . . . . . . . . . . . . . . . 20
                        
                   |
57 | 53, 55, 56 | sylc 61 |
. . . . . . . . . . . . . . . . . . 19
              
     
                  |
58 | 46, 57 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . 18
              
     
          |
59 | | simprr 774 |
. . . . . . . . . . . . . . . . . . 19
              
     
      |
60 | 59 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . 18
              
     
              |
61 | 58, 60 | eqtrd 2505 |
. . . . . . . . . . . . . . . . 17
              
     
      |
62 | 43, 61 | sylan2 482 |
. . . . . . . . . . . . . . . 16
                                
      |
63 | 39, 62 | fveq12d 5885 |
. . . . . . . . . . . . . . 15
                                                                                         |
64 | 63 | eqeq2d 2481 |
. . . . . . . . . . . . . 14
                                                                                           |
65 | 64 | biimpd 212 |
. . . . . . . . . . . . 13
                                                                                           |
66 | 65 | impancom 447 |
. . . . . . . . . . . 12
             
                             
                  
                            |
67 | 66 | com12 31 |
. . . . . . . . . . 11
                                
                             
                            |
68 | 29, 67 | jcad 542 |
. . . . . . . . . 10
                                
                             
        
                             |
69 | 25 | biimprd 231 |
. . . . . . . . . . . . . 14
                             |
70 | 69 | ad2antll 743 |
. . . . . . . . . . . . 13
                
        
               |
71 | 70 | adantr 472 |
. . . . . . . . . . . 12
                                           |
72 | 71 | adantrd 475 |
. . . . . . . . . . 11
                                                                      |
73 | | eqidd 2472 |
. . . . . . . . . . . . . . . . 17
                               |
74 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . 21
                
      |
75 | | tru 1456 |
. . . . . . . . . . . . . . . . . . . . 21
 |
76 | 74, 75 | jctir 547 |
. . . . . . . . . . . . . . . . . . . 20
                
       |
77 | 76 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . 19
                                    |
78 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . 20
     
      |
79 | 78 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . 19
     
      |
80 | 77, 79 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                            
      |
81 | 80 | fveq2d 5883 |
. . . . . . . . . . . . . . . . 17
                             
           |
82 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
83 | 82 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
84 | 83 | ad2antll 743 |
. . . . . . . . . . . . . . . . . . . . 21
                                 |
85 | 84 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
                           
       |
86 | 85 | fveq1d 5881 |
. . . . . . . . . . . . . . . . . . 19
                           
                       |
87 | 86 | adantlrr 735 |
. . . . . . . . . . . . . . . . . 18
                             
                       |
88 | 87 | mpteq2dva 4482 |
. . . . . . . . . . . . . . . . 17
                                                       |
89 | 73, 81, 88 | seqeq123d 12260 |
. . . . . . . . . . . . . . . 16
                                                                           |
90 | 71 | com12 31 |
. . . . . . . . . . . . . . . . . . 19
        
                                  |
91 | 90 | imp 436 |
. . . . . . . . . . . . . . . . . 18
                                           |
92 | | simprr 774 |
. . . . . . . . . . . . . . . . . 18
                            
  |
93 | 41 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . 18
                                   |
94 | 91, 92, 93, 61 | syl12anc 1290 |
. . . . . . . . . . . . . . . . 17
                            
      |
95 | 94 | eqcomd 2477 |
. . . . . . . . . . . . . . . 16
                                   |
96 | 89, 95 | fveq12d 5885 |
. . . . . . . . . . . . . . 15
                                                                                     |
97 | 96 | eqeq2d 2481 |
. . . . . . . . . . . . . 14
                                                      
                                |
98 | 97 | biimpd 212 |
. . . . . . . . . . . . 13
                                                      
                                |
99 | 98 | impancom 447 |
. . . . . . . . . . . 12
         
                         
                  
                                |
100 | 99 | com12 31 |
. . . . . . . . . . 11
                                                                                       |
101 | 72, 100 | jcad 542 |
. . . . . . . . . 10
                                                                   
                                 |
102 | 68, 101 | impbid 195 |
. . . . . . . . 9
                                
                                                                    |
103 | 102 | ex 441 |
. . . . . . . 8
                

             
                                                                     |
104 | 15, 19, 24, 103 | syl12anc 1290 |
. . . . . . 7
 
                  
                                                                     |
105 | 104 | imp 436 |
. . . . . 6
                     
                                                                    |
106 | 105 | exbidv 1776 |
. . . . 5
                       
                                        
                             |
107 | 106 | rexbidva 2889 |
. . . 4
 
                    
                                                                       |
108 | 107 | iotabidv 5574 |
. . 3
 
       
              
                                             
                             |
109 | | eleq1 2537 |
. . . . . . . . . 10
 
   |
110 | | feq2 5721 |
. . . . . . . . . 10
         
           |
111 | 109, 110 | anbi12d 725 |
. . . . . . . . 9
            
            |
112 | 111 | ceqsexgv 3159 |
. . . . . . . 8
                             |
113 | 9, 112 | syl 17 |
. . . . . . 7
               
             |
114 | 9, 8, 113 | mpbir2and 936 |
. . . . . 6
                 |
115 | | exsimpr 1738 |
. . . . . 6
                             |
116 | 114, 115 | syl 17 |
. . . . 5
               |
117 | | df-rex 2762 |
. . . . 5
         
              |
118 | 116, 117 | sylibr 217 |
. . . 4
            |
119 | | eleq1 2537 |
. . . . . . 7
  CMnd
CMnd  |
120 | | fveq2 5879 |
. . . . . . . . 9
           |
121 | 120 | feq3d 5726 |
. . . . . . . 8
                     |
122 | 121 | rexbidv 2892 |
. . . . . . 7
  
       
            |
123 | 119, 122 | anbi12d 725 |
. . . . . 6
   CMnd          
 CMnd              |
124 | | feq1 5720 |
. . . . . . . 8
                     |
125 | 124 | rexbidv 2892 |
. . . . . . 7
  
       
            |
126 | 125 | anbi2d 718 |
. . . . . 6
   CMnd          
 CMnd              |
127 | 123, 126 | opelopabg 4719 |
. . . . 5
  CMnd         
 CMnd           
 CMnd              |
128 | 6, 11, 127 | syl2anc 673 |
. . . 4
          CMnd 
         
 CMnd              |
129 | 6, 118, 128 | mpbir2and 936 |
. . 3
       
 CMnd              |
130 | | iotaex 5570 |
. . . 4
              
                            |
131 | 130 | a1i 11 |
. . 3
                                             |
132 | 3, 108, 129, 131 | fvmptd 5969 |
. 2
 FinSum                    
                             |
133 | 1, 132 | syl5eq 2517 |
1
  FinSum     
                                        |