Step | Hyp | Ref
| Expression |
1 | | fveq2 5870 |
. . . . . . . . . 10
           |
2 | 1 | sseq2d 3462 |
. . . . . . . . 9
     
       |
3 | | seqeq1 12223 |
. . . . . . . . . 10
         |
4 | 3 | breq1d 4415 |
. . . . . . . . 9
   
      |
5 | 2, 4 | anbi12d 718 |
. . . . . . . 8
                       |
6 | 5 | cbvrexv 3022 |
. . . . . . 7
      
   
            |
7 | | reeanv 2960 |
. . . . . . . . 9
  
                                            |
8 | | simprlr 774 |
. . . . . . . . . . . . 13
   
 
     
    
               |
9 | | summo.1 |
. . . . . . . . . . . . . 14
        |
10 | | simpll 761 |
. . . . . . . . . . . . . . 15
   
 
     
    
            |
11 | | summo.2 |
. . . . . . . . . . . . . . 15
 
   |
12 | 10, 11 | sylan 474 |
. . . . . . . . . . . . . 14
    
   
                      |
13 | | simplrl 771 |
. . . . . . . . . . . . . 14
   
 
     
    
            |
14 | | simplrr 772 |
. . . . . . . . . . . . . 14
   
 
     
    
            |
15 | | simprll 773 |
. . . . . . . . . . . . . 14
   
 
     
    
                |
16 | | simprrl 775 |
. . . . . . . . . . . . . 14
   
 
     
    
                |
17 | 9, 12, 13, 14, 15, 16 | sumrb 13791 |
. . . . . . . . . . . . 13
   
 
     
    
            
      |
18 | 8, 17 | mpbid 214 |
. . . . . . . . . . . 12
   
 
     
    
               |
19 | | simprrr 776 |
. . . . . . . . . . . 12
   
 
     
    
               |
20 | | climuni 13628 |
. . . . . . . . . . . 12
          |
21 | 18, 19, 20 | syl2anc 667 |
. . . . . . . . . . 11
   
 
     
    
            |
22 | 21 | exp31 609 |
. . . . . . . . . 10
                        
    |
23 | 22 | rexlimdvv 2887 |
. . . . . . . . 9
         
    
        
   |
24 | 7, 23 | syl5bir 222 |
. . . . . . . 8
                       
   |
25 | 24 | expdimp 439 |
. . . . . . 7
 
          
 
    
   
   |
26 | 6, 25 | syl5bi 221 |
. . . . . 6
 
          
 
    
   
   |
27 | | summo.3 |
. . . . . . 7
       ![]_ ]_](_urbrack.gif)   |
28 | 9, 11, 27 | summolem2 13794 |
. . . . . 6
 
          
 
                 
   |
29 | 26, 28 | jaod 382 |
. . . . 5
 
          
  

                   
       
   |
30 | 9, 11, 27 | summolem2 13794 |
. . . . . . . 8
 
          
 
                     |
31 | | equcom 1864 |
. . . . . . . 8

  |
32 | 30, 31 | syl6ib 230 |
. . . . . . 7
 
          
 
                 
   |
33 | 32 | impancom 442 |
. . . . . 6
 
           
                      |
34 | | oveq2 6303 |
. . . . . . . . . . . 12
           |
35 | | f1oeq2 5811 |
. . . . . . . . . . . 12
                 
           |
36 | 34, 35 | syl 17 |
. . . . . . . . . . 11
         
           |
37 | | fveq2 5870 |
. . . . . . . . . . . 12
               |
38 | 37 | eqeq2d 2463 |
. . . . . . . . . . 11
                 |
39 | 36, 38 | anbi12d 718 |
. . . . . . . . . 10
                 
                   |
40 | 39 | exbidv 1770 |
. . . . . . . . 9
                   
                     |
41 | | f1oeq1 5810 |
. . . . . . . . . . 11
         
           |
42 | | fveq1 5869 |
. . . . . . . . . . . . . . . . 17
           |
43 | 42 | csbeq1d 3372 |
. . . . . . . . . . . . . . . 16
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
44 | 43 | mpteq2dv 4493 |
. . . . . . . . . . . . . . 15
        ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)    |
45 | 27, 44 | syl5eq 2499 |
. . . . . . . . . . . . . 14
        ![]_ ]_](_urbrack.gif)    |
46 | 45 | seqeq3d 12228 |
. . . . . . . . . . . . 13
             ![]_ ]_](_urbrack.gif)     |
47 | 46 | fveq1d 5872 |
. . . . . . . . . . . 12
                ![]_ ]_](_urbrack.gif)        |
48 | 47 | eqeq2d 2463 |
. . . . . . . . . . 11
                 ![]_ ]_](_urbrack.gif)         |
49 | 41, 48 | anbi12d 718 |
. . . . . . . . . 10
                 
                  ![]_ ]_](_urbrack.gif)          |
50 | 49 | cbvexv 2119 |
. . . . . . . . 9
                  
                    ![]_ ]_](_urbrack.gif)         |
51 | 40, 50 | syl6bb 265 |
. . . . . . . 8
                   
                    ![]_ ]_](_urbrack.gif)          |
52 | 51 | cbvrexv 3022 |
. . . . . . 7
                   
           
         ![]_ ]_](_urbrack.gif)         |
53 | | reeanv 2960 |
. . . . . . . . 9
  
                                       ![]_ ]_](_urbrack.gif)                    
       
                    ![]_ ]_](_urbrack.gif)          |
54 | | eeanv 2080 |
. . . . . . . . . . 11
                                        ![]_ ]_](_urbrack.gif)                   
                           ![]_ ]_](_urbrack.gif)          |
55 | | an4 834 |
. . . . . . . . . . . . 13
                                    ![]_ ]_](_urbrack.gif)                                 
         ![]_ ]_](_urbrack.gif)          |
56 | | simpll 761 |
. . . . . . . . . . . . . . . . 17
   
 
                     |
57 | 56, 11 | sylan 474 |
. . . . . . . . . . . . . . . 16
    
                    
   |
58 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . . 19
           |
59 | 58 | csbeq1d 3372 |
. . . . . . . . . . . . . . . . . 18
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
60 | 59 | cbvmptv 4498 |
. . . . . . . . . . . . . . . . 17
       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   |
61 | 27, 60 | eqtri 2475 |
. . . . . . . . . . . . . . . 16
       ![]_ ]_](_urbrack.gif)   |
62 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . 18
           |
63 | 62 | csbeq1d 3372 |
. . . . . . . . . . . . . . . . 17
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
64 | 63 | cbvmptv 4498 |
. . . . . . . . . . . . . . . 16
       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   |
65 | | simplr 763 |
. . . . . . . . . . . . . . . 16
   
 
                       |
66 | | simprl 765 |
. . . . . . . . . . . . . . . 16
   
 
                             |
67 | | simprr 767 |
. . . . . . . . . . . . . . . 16
   
 
                             |
68 | 9, 57, 61, 64, 65, 66, 67 | summolem3 13792 |
. . . . . . . . . . . . . . 15
   
 
                                  ![]_ ]_](_urbrack.gif)        |
69 | | eqeq12 2466 |
. . . . . . . . . . . . . . 15
       
         ![]_ ]_](_urbrack.gif)                       ![]_ ]_](_urbrack.gif)         |
70 | 68, 69 | syl5ibrcom 226 |
. . . . . . . . . . . . . 14
   
 
                          
         ![]_ ]_](_urbrack.gif)      
   |
71 | 70 | expimpd 608 |
. . . . . . . . . . . . 13
 
                             
         ![]_ ]_](_urbrack.gif)           |
72 | 55, 71 | syl5bi 221 |
. . . . . . . . . . . 12
 
                                       ![]_ ]_](_urbrack.gif)           |
73 | 72 | exlimdvv 1782 |
. . . . . . . . . . 11
 
                                           ![]_ ]_](_urbrack.gif)           |
74 | 54, 73 | syl5bir 222 |
. . . . . . . . . 10
 
                                           ![]_ ]_](_urbrack.gif)           |
75 | 74 | rexlimdvva 2888 |
. . . . . . . . 9
                                           ![]_ ]_](_urbrack.gif)           |
76 | 53, 75 | syl5bir 222 |
. . . . . . . 8
              
       
                    ![]_ ]_](_urbrack.gif)           |
77 | 76 | expdimp 439 |
. . . . . . 7
 
           
                    
         ![]_ ]_](_urbrack.gif)      
   |
78 | 52, 77 | syl5bi 221 |
. . . . . 6
 
           
                    
          |
79 | 33, 78 | jaod 382 |
. . . . 5
 
           
                               
       
   |
80 | 29, 79 | jaodan 795 |
. . . 4
 
 
    
                        
  

                   
       
   |
81 | 80 | expimpd 608 |
. . 3
         
                                              
            |
82 | 81 | alrimivv 1776 |
. 2
             
                                              
            |
83 | | breq2 4409 |
. . . . . 6
   
      |
84 | 83 | anbi2d 711 |
. . . . 5
                       |
85 | 84 | rexbidv 2903 |
. . . 4
  

        

           |
86 | | eqeq1 2457 |
. . . . . . 7
                 |
87 | 86 | anbi2d 711 |
. . . . . 6
                 
                   |
88 | 87 | exbidv 1770 |
. . . . 5
                   
                     |
89 | 88 | rexbidv 2903 |
. . . 4
  
                 
           
          |
90 | 85, 89 | orbi12d 717 |
. . 3
                        
       
 
    
                           |
91 | 90 | mo4 2348 |
. 2
                         
       
        
                   
          
                   
            |
92 | 82, 91 | sylibr 216 |
1
         
                          |