Step | Hyp | Ref
| Expression |
1 | | gsumval3a.n |
. . . . . 6
   |
2 | 1 | neneqd 2628 |
. . . . 5
   |
3 | | gsumval3a.t |
. . . . . . 7
   |
4 | | fz1f1o 13769 |
. . . . . . 7
 
                      |
5 | 3, 4 | syl 17 |
. . . . . 6
                        |
6 | 5 | ord 379 |
. . . . 5
                        |
7 | 2, 6 | mpd 15 |
. . . 4
                      |
8 | 7 | simprd 465 |
. . 3
                |
9 | | excom 1926 |
. . . 4
                              
                                |
10 | | exancom 1721 |
. . . . . 6
                            
                              |
11 | | fvex 5873 |
. . . . . . 7
             |
12 | | biidd 241 |
. . . . . . 7
  

                                     |
13 | 11, 12 | ceqsexv 3083 |
. . . . . 6
                            
              |
14 | 10, 13 | bitri 253 |
. . . . 5
                            
              |
15 | 14 | exbii 1717 |
. . . 4
                              
               |
16 | 9, 15 | bitri 253 |
. . 3
                              
               |
17 | 8, 16 | sylibr 216 |
. 2
                 
               |
18 | | eeanv 2077 |
. . . 4
                  
                                                                                                    |
19 | | an4 832 |
. . . . . 6
                                                      
                                       
                |
20 | | gsumval3.g |
. . . . . . . . . . 11
   |
21 | 20 | adantr 467 |
. . . . . . . . . 10
 
                             |
22 | | gsumval3.b |
. . . . . . . . . . . 12
     |
23 | | gsumval3.p |
. . . . . . . . . . . 12
    |
24 | 22, 23 | mndcl 16538 |
. . . . . . . . . . 11
 
     |
25 | 24 | 3expb 1208 |
. . . . . . . . . 10
  
  
   |
26 | 21, 25 | sylan 474 |
. . . . . . . . 9
                              
 
    |
27 | | gsumval3.c |
. . . . . . . . . . . . 13
       |
28 | 27 | adantr 467 |
. . . . . . . . . . . 12
 
                                 |
29 | 28 | sselda 3431 |
. . . . . . . . . . 11
                              
      |
30 | 29 | adantrr 722 |
. . . . . . . . . 10
                              
        |
31 | | simprr 765 |
. . . . . . . . . 10
                              
    |
32 | | gsumval3.z |
. . . . . . . . . . 11
Cntz   |
33 | 23, 32 | cntzi 16976 |
. . . . . . . . . 10
    


      |
34 | 30, 31, 33 | syl2anc 666 |
. . . . . . . . 9
                              
  
     |
35 | 22, 23 | mndass 16539 |
. . . . . . . . . 10
  
    
       |
36 | 21, 35 | sylan 474 |
. . . . . . . . 9
                              
 
 
        |
37 | 7 | simpld 461 |
. . . . . . . . . . 11
       |
38 | 37 | adantr 467 |
. . . . . . . . . 10
 
                                 |
39 | | nnuz 11191 |
. . . . . . . . . 10
     |
40 | 38, 39 | syl6eleq 2538 |
. . . . . . . . 9
 
                                     |
41 | | gsumval3.f |
. . . . . . . . . . 11
       |
42 | 41 | adantr 467 |
. . . . . . . . . 10
 
                                 |
43 | | frn 5733 |
. . . . . . . . . 10
    
  |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
 
                             |
45 | | simprr 765 |
. . . . . . . . . . 11
 
                                         |
46 | | f1ocnv 5824 |
. . . . . . . . . . 11
            
               |
47 | 45, 46 | syl 17 |
. . . . . . . . . 10
 
                                          |
48 | | simprl 763 |
. . . . . . . . . 10
 
                                         |
49 | | f1oco 5834 |
. . . . . . . . . 10
                             
                       |
50 | 47, 48, 49 | syl2anc 666 |
. . . . . . . . 9
 
                            
                       |
51 | | f1of 5812 |
. . . . . . . . . . . 12
            
              |
52 | 45, 51 | syl 17 |
. . . . . . . . . . 11
 
                                         |
53 | | fvco3 5940 |
. . . . . . . . . . 11
             
                         |
54 | 52, 53 | sylan 474 |
. . . . . . . . . 10
                                      
 
              |
55 | | ffn 5726 |
. . . . . . . . . . . . 13
    
  |
56 | 42, 55 | syl 17 |
. . . . . . . . . . . 12
 
                             |
57 | 56 | adantr 467 |
. . . . . . . . . . 11
                                      
  |
58 | | gsumval3a.s |
. . . . . . . . . . . . . 14

  |
59 | 58 | adantr 467 |
. . . . . . . . . . . . 13
 
                             |
60 | 52, 59 | fssd 5736 |
. . . . . . . . . . . 12
 
                                         |
61 | 60 | ffvelrnda 6020 |
. . . . . . . . . . 11
                                      
      |
62 | | fnfvelrn 6017 |
. . . . . . . . . . 11
                 |
63 | 57, 61, 62 | syl2anc 666 |
. . . . . . . . . 10
                                      
          |
64 | 54, 63 | eqeltrd 2528 |
. . . . . . . . 9
                                      
 
      |
65 | | f1of 5812 |
. . . . . . . . . . . . . . 15
            
              |
66 | 48, 65 | syl 17 |
. . . . . . . . . . . . . 14
 
                                         |
67 | | fvco3 5940 |
. . . . . . . . . . . . . 14
             
                           |
68 | 66, 67 | sylan 474 |
. . . . . . . . . . . . 13
                                      
  
               |
69 | 68 | fveq2d 5867 |
. . . . . . . . . . . 12
                                      
                          |
70 | 45 | adantr 467 |
. . . . . . . . . . . . 13
                                      
              |
71 | 66 | ffvelrnda 6020 |
. . . . . . . . . . . . 13
                                      
      |
72 | | f1ocnvfv2 6174 |
. . . . . . . . . . . . 13
                                      |
73 | 70, 71, 72 | syl2anc 666 |
. . . . . . . . . . . 12
                                      
                   |
74 | 69, 73 | eqtr2d 2485 |
. . . . . . . . . . 11
                                      
         
       |
75 | 74 | fveq2d 5867 |
. . . . . . . . . 10
                                      
                         |
76 | | fvco3 5940 |
. . . . . . . . . . 11
             
                         |
77 | 66, 76 | sylan 474 |
. . . . . . . . . 10
                                      
 
              |
78 | | f1of 5812 |
. . . . . . . . . . . . 13
  
                                              |
79 | 50, 78 | syl 17 |
. . . . . . . . . . . 12
 
                            
                       |
80 | 79 | ffvelrnda 6020 |
. . . . . . . . . . 11
                                      
  
              |
81 | | fvco3 5940 |
. . . . . . . . . . . 12
                                                   
        |
82 | 60, 81 | sylan 474 |
. . . . . . . . . . 11
                                                                            |
83 | 80, 82 | syldan 473 |
. . . . . . . . . 10
                                      
 
                   
        |
84 | 75, 77, 83 | 3eqtr4d 2494 |
. . . . . . . . 9
                                      
 
           
       |
85 | 26, 34, 36, 40, 44, 50, 64, 84 | seqf1o 12251 |
. . . . . . . 8
 
                                        

           |
86 | | eqeq12 2463 |
. . . . . . . 8
                           
             

            |
87 | 85, 86 | syl5ibrcom 226 |
. . . . . . 7
 
                                                     
   |
88 | 87 | expimpd 607 |
. . . . . 6
                               

        
 

              |
89 | 19, 88 | syl5bir 222 |
. . . . 5
                                         
                 |
90 | 89 | exlimdvv 1779 |
. . . 4
                                             
                 |
91 | 18, 90 | syl5bir 222 |
. . 3
                 
                           
                 |
92 | 91 | alrimivv 1773 |
. 2
                     
                           
                 |
93 | | eqeq1 2454 |
. . . . . 6
                             |
94 | 93 | anbi2d 709 |
. . . . 5
              
                                          |
95 | 94 | exbidv 1767 |
. . . 4
                             
              
                |
96 | | f1oeq1 5803 |
. . . . . 6
                             |
97 | | coeq2 4992 |
. . . . . . . . 9
 
     |
98 | 97 | seqeq3d 12218 |
. . . . . . . 8
             |
99 | 98 | fveq1d 5865 |
. . . . . . 7
              

           |
100 | 99 | eqeq2d 2460 |
. . . . . 6
                             |
101 | 96, 100 | anbi12d 716 |
. . . . 5
              
                                          |
102 | 101 | cbvexv 2116 |
. . . 4
                            
              
               |
103 | 95, 102 | syl6bb 265 |
. . 3
                             
              
                |
104 | 103 | eu4 2346 |
. 2
                              
                                                                                             
    |
105 | 17, 92, 104 | sylanbrc 669 |
1
                 
               |