Step | Hyp | Ref
| Expression |
1 | | ssid 3486 |
. 2
 |
2 | | fsumo1.2 |
. . 3
   |
3 | | sseq1 3488 |
. . . . . 6


   |
4 | | sumeq1 13287 |
. . . . . . . . 9


   |
5 | | sum0 13319 |
. . . . . . . . 9
  |
6 | 4, 5 | syl6eq 2511 |
. . . . . . . 8


  |
7 | 6 | mpteq2dv 4490 |
. . . . . . 7

 
     |
8 | 7 | eleq1d 2523 |
. . . . . 6

      

       |
9 | 3, 8 | imbi12d 320 |
. . . . 5

 
      
          |
10 | 9 | imbi2d 316 |
. . . 4

                       |
11 | | sseq1 3488 |
. . . . . 6
 
   |
12 | | sumeq1 13287 |
. . . . . . . 8
 
   |
13 | 12 | mpteq2dv 4490 |
. . . . . . 7
     
   |
14 | 13 | eleq1d 2523 |
. . . . . 6
                 |
15 | 11, 14 | imbi12d 320 |
. . . . 5
                     |
16 | 15 | imbi2d 316 |
. . . 4
  
         
            |
17 | | sseq1 3488 |
. . . . . 6
             |
18 | | sumeq1 13287 |
. . . . . . . 8
     
        |
19 | 18 | mpteq2dv 4490 |
. . . . . . 7
                  |
20 | 19 | eleq1d 2523 |
. . . . . 6
       
                  |
21 | 17, 20 | imbi12d 320 |
. . . . 5
             
                    |
22 | 21 | imbi2d 316 |
. . . 4
                                      |
23 | | sseq1 3488 |
. . . . . 6
 
   |
24 | | sumeq1 13287 |
. . . . . . . 8
 
   |
25 | 24 | mpteq2dv 4490 |
. . . . . . 7
     
   |
26 | 25 | eleq1d 2523 |
. . . . . 6
                 |
27 | 23, 26 | imbi12d 320 |
. . . . 5
                     |
28 | 27 | imbi2d 316 |
. . . 4
  
         
            |
29 | | fsumo1.1 |
. . . . . 6

  |
30 | | 0cn 9492 |
. . . . . 6
 |
31 | | o1const 13218 |
. . . . . 6
 
        |
32 | 29, 30, 31 | sylancl 662 |
. . . . 5
        |
33 | 32 | a1d 25 |
. . . 4
 
        |
34 | | ssun1 3630 |
. . . . . . . . . 10
     |
35 | | sstr 3475 |
. . . . . . . . . 10
 
        
  |
36 | 34, 35 | mpan 670 |
. . . . . . . . 9
    
  |
37 | 36 | imim1i 58 |
. . . . . . . 8
 
                     |
38 | | simprl 755 |
. . . . . . . . . . . . . . . . . . 19
 

     
  |
39 | | disjsn 4047 |
. . . . . . . . . . . . . . . . . . 19
    
  |
40 | 38, 39 | sylibr 212 |
. . . . . . . . . . . . . . . . . 18
 

            |
41 | 40 | adantr 465 |
. . . . . . . . . . . . . . . . 17
   
     
       |
42 | | eqidd 2455 |
. . . . . . . . . . . . . . . . 17
   
     
           |
43 | 2 | adantr 465 |
. . . . . . . . . . . . . . . . . . 19
 

     
  |
44 | | simprr 756 |
. . . . . . . . . . . . . . . . . . 19
 

            |
45 | | ssfi 7647 |
. . . . . . . . . . . . . . . . . . 19
             |
46 | 43, 44, 45 | syl2anc 661 |
. . . . . . . . . . . . . . . . . 18
 

            |
47 | 46 | adantr 465 |
. . . . . . . . . . . . . . . . 17
   
     
       |
48 | 44 | sselda 3467 |
. . . . . . . . . . . . . . . . . . 19
   
     
    
  |
49 | 48 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
    
      
       |
50 | | fsumo1.3 |
. . . . . . . . . . . . . . . . . . . . . 22
 

 
  |
51 | 50 | anass1rs 805 |
. . . . . . . . . . . . . . . . . . . . 21
       |
52 | | fsumo1.4 |
. . . . . . . . . . . . . . . . . . . . 21
 
        |
53 | 51, 52 | o1mptrcl 13221 |
. . . . . . . . . . . . . . . . . . . 20
       |
54 | 53 | an32s 802 |
. . . . . . . . . . . . . . . . . . 19
       |
55 | 54 | adantllr 718 |
. . . . . . . . . . . . . . . . . 18
    
      
   |
56 | 49, 55 | syldan 470 |
. . . . . . . . . . . . . . . . 17
    
      
       |
57 | 41, 42, 47, 56 | fsumsplit 13337 |
. . . . . . . . . . . . . . . 16
   
     
                |
58 | | nfcv 2616 |
. . . . . . . . . . . . . . . . . . 19
   |
59 | | nfcsb1v 3414 |
. . . . . . . . . . . . . . . . . . 19
  
 ![]_ ]_](_urbrack.gif)  |
60 | | csbeq1a 3407 |
. . . . . . . . . . . . . . . . . . 19
   ![]_ ]_](_urbrack.gif)   |
61 | 58, 59, 60 | cbvsumi 13295 |
. . . . . . . . . . . . . . . . . 18
          ![]_ ]_](_urbrack.gif)  |
62 | 44 | unssbd 3645 |
. . . . . . . . . . . . . . . . . . . . 21
 

          |
63 | | vex 3081 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
64 | 63 | snss 4110 |
. . . . . . . . . . . . . . . . . . . . 21

    |
65 | 62, 64 | sylibr 212 |
. . . . . . . . . . . . . . . . . . . 20
 

        |
66 | 65 | adantr 465 |
. . . . . . . . . . . . . . . . . . 19
   
     
   |
67 | 55 | ralrimiva 2830 |
. . . . . . . . . . . . . . . . . . . 20
   
     
 
  |
68 | | nfcsb1v 3414 |
. . . . . . . . . . . . . . . . . . . . . 22
  
 ![]_ ]_](_urbrack.gif)  |
69 | 68 | nfel1 2632 |
. . . . . . . . . . . . . . . . . . . . 21
    ![]_ ]_](_urbrack.gif)
 |
70 | | csbeq1a 3407 |
. . . . . . . . . . . . . . . . . . . . . 22
   ![]_ ]_](_urbrack.gif)   |
71 | 70 | eleq1d 2523 |
. . . . . . . . . . . . . . . . . . . . 21
 
  ![]_ ]_](_urbrack.gif)    |
72 | 69, 71 | rspc 3173 |
. . . . . . . . . . . . . . . . . . . 20
  
  ![]_ ]_](_urbrack.gif)
   |
73 | 66, 67, 72 | sylc 60 |
. . . . . . . . . . . . . . . . . . 19
   
     
   ![]_ ]_](_urbrack.gif)
  |
74 | | csbeq1 3401 |
. . . . . . . . . . . . . . . . . . . 20
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
75 | 74 | sumsn 13338 |
. . . . . . . . . . . . . . . . . . 19
    ![]_ ]_](_urbrack.gif)
 
     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
76 | 66, 73, 75 | syl2anc 661 |
. . . . . . . . . . . . . . . . . 18
   
     
 
     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
77 | 61, 76 | syl5eq 2507 |
. . . . . . . . . . . . . . . . 17
   
     
       ![]_ ]_](_urbrack.gif)   |
78 | 77 | oveq2d 6219 |
. . . . . . . . . . . . . . . 16
   
     
         
  ![]_ ]_](_urbrack.gif)    |
79 | 57, 78 | eqtrd 2495 |
. . . . . . . . . . . . . . 15
   
     
           ![]_ ]_](_urbrack.gif)    |
80 | 79 | mpteq2dva 4489 |
. . . . . . . . . . . . . 14
 

                
  ![]_ ]_](_urbrack.gif)     |
81 | 29 | adantr 465 |
. . . . . . . . . . . . . . . 16
 

        |
82 | | reex 9487 |
. . . . . . . . . . . . . . . . 17
 |
83 | 82 | ssex 4547 |
. . . . . . . . . . . . . . . 16

  |
84 | 81, 83 | syl 16 |
. . . . . . . . . . . . . . 15
 

     
  |
85 | | sumex 13286 |
. . . . . . . . . . . . . . . 16

 |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . 15
   
     
    |
87 | | eqidd 2455 |
. . . . . . . . . . . . . . 15
 

              |
88 | | eqidd 2455 |
. . . . . . . . . . . . . . 15
 

         ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    |
89 | 84, 86, 73, 87, 88 | offval2 6449 |
. . . . . . . . . . . . . 14
 

              ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)     |
90 | 80, 89 | eqtr4d 2498 |
. . . . . . . . . . . . 13
 

                
 
   ![]_ ]_](_urbrack.gif)     |
91 | 90 | adantr 465 |
. . . . . . . . . . . 12
   
      
                
 
   ![]_ ]_](_urbrack.gif)     |
92 | | id 22 |
. . . . . . . . . . . . 13
               |
93 | 52 | ralrimiva 2830 |
. . . . . . . . . . . . . . 15
  
      |
94 | 93 | adantr 465 |
. . . . . . . . . . . . . 14
 

      

      |
95 | | nfcv 2616 |
. . . . . . . . . . . . . . . . 17
   |
96 | 95, 68 | nfmpt 4491 |
. . . . . . . . . . . . . . . 16
     ![]_ ]_](_urbrack.gif)   |
97 | 96 | nfel1 2632 |
. . . . . . . . . . . . . . 15
     ![]_ ]_](_urbrack.gif)      |
98 | 70 | mpteq2dv 4490 |
. . . . . . . . . . . . . . . 16
      ![]_ ]_](_urbrack.gif)    |
99 | 98 | eleq1d 2523 |
. . . . . . . . . . . . . . 15
          ![]_ ]_](_urbrack.gif)        |
100 | 97, 99 | rspc 3173 |
. . . . . . . . . . . . . 14
  

       ![]_ ]_](_urbrack.gif)        |
101 | 65, 94, 100 | sylc 60 |
. . . . . . . . . . . . 13
 

         ![]_ ]_](_urbrack.gif)       |
102 | | o1add 13212 |
. . . . . . . . . . . . 13
           ![]_ ]_](_urbrack.gif)        
 
   ![]_ ]_](_urbrack.gif)        |
103 | 92, 101, 102 | syl2anr 478 |
. . . . . . . . . . . 12
   
      
        
 
   ![]_ ]_](_urbrack.gif)        |
104 | 91, 103 | eqeltrd 2542 |
. . . . . . . . . . 11
   
      
                   |
105 | 104 | ex 434 |
. . . . . . . . . 10
 

                           |
106 | 105 | expr 615 |
. . . . . . . . 9
 
        
                   |
107 | 106 | a2d 26 |
. . . . . . . 8
 
                                  |
108 | 37, 107 | syl5 32 |
. . . . . . 7
 
              
               |
109 | 108 | expcom 435 |
. . . . . 6
 
 
                            |
110 | 109 | a2d 26 |
. . . . 5
   
                              |
111 | 110 | adantl 466 |
. . . 4
 

          
                      |
112 | 10, 16, 22, 28, 33, 111 | findcard2s 7667 |
. . 3
             |
113 | 2, 112 | mpcom 36 |
. 2
           |
114 | 1, 113 | mpi 17 |
1
         |