Step | Hyp | Ref
| Expression |
1 | | ssid 3451 |
. 2
 |
2 | | fsumo1.2 |
. . 3
   |
3 | | sseq1 3453 |
. . . . . 6


   |
4 | | sumeq1 13755 |
. . . . . . . . 9


   |
5 | | sum0 13787 |
. . . . . . . . 9
  |
6 | 4, 5 | syl6eq 2501 |
. . . . . . . 8


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

 
     |
8 | 7 | eleq1d 2513 |
. . . . . 6

      

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

 
      
          |
10 | 9 | imbi2d 318 |
. . . 4

                       |
11 | | sseq1 3453 |
. . . . . 6
 
   |
12 | | sumeq1 13755 |
. . . . . . . 8
 
   |
13 | 12 | mpteq2dv 4490 |
. . . . . . 7
     
   |
14 | 13 | eleq1d 2513 |
. . . . . 6
                 |
15 | 11, 14 | imbi12d 322 |
. . . . 5
                     |
16 | 15 | imbi2d 318 |
. . . 4
  
         
            |
17 | | sseq1 3453 |
. . . . . 6
             |
18 | | sumeq1 13755 |
. . . . . . . 8
     
        |
19 | 18 | mpteq2dv 4490 |
. . . . . . 7
                  |
20 | 19 | eleq1d 2513 |
. . . . . 6
       
                  |
21 | 17, 20 | imbi12d 322 |
. . . . 5
             
                    |
22 | 21 | imbi2d 318 |
. . . 4
                                      |
23 | | sseq1 3453 |
. . . . . 6
 
   |
24 | | sumeq1 13755 |
. . . . . . . 8
 
   |
25 | 24 | mpteq2dv 4490 |
. . . . . . 7
     
   |
26 | 25 | eleq1d 2513 |
. . . . . 6
                 |
27 | 23, 26 | imbi12d 322 |
. . . . 5
                     |
28 | 27 | imbi2d 318 |
. . . 4
  
         
            |
29 | | fsumo1.1 |
. . . . . 6

  |
30 | | 0cn 9635 |
. . . . . 6
 |
31 | | o1const 13683 |
. . . . . 6
 
        |
32 | 29, 30, 31 | sylancl 668 |
. . . . 5
        |
33 | 32 | a1d 26 |
. . . 4
 
        |
34 | | ssun1 3597 |
. . . . . . . . . 10
     |
35 | | sstr 3440 |
. . . . . . . . . 10
 
        
  |
36 | 34, 35 | mpan 676 |
. . . . . . . . 9
    
  |
37 | 36 | imim1i 60 |
. . . . . . . 8
 
                     |
38 | | simprl 764 |
. . . . . . . . . . . . . . . . . . 19
 

     
  |
39 | | disjsn 4032 |
. . . . . . . . . . . . . . . . . . 19
    
  |
40 | 38, 39 | sylibr 216 |
. . . . . . . . . . . . . . . . . 18
 

            |
41 | 40 | adantr 467 |
. . . . . . . . . . . . . . . . 17
   
     
       |
42 | | eqidd 2452 |
. . . . . . . . . . . . . . . . 17
   
     
           |
43 | 2 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 

     
  |
44 | | simprr 766 |
. . . . . . . . . . . . . . . . . . 19
 

            |
45 | | ssfi 7792 |
. . . . . . . . . . . . . . . . . . 19
             |
46 | 43, 44, 45 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
 

            |
47 | 46 | adantr 467 |
. . . . . . . . . . . . . . . . 17
   
     
       |
48 | 44 | sselda 3432 |
. . . . . . . . . . . . . . . . . . 19
   
     
    
  |
49 | 48 | adantlr 721 |
. . . . . . . . . . . . . . . . . 18
    
      
       |
50 | | fsumo1.3 |
. . . . . . . . . . . . . . . . . . . . . 22
 

 
  |
51 | 50 | anass1rs 816 |
. . . . . . . . . . . . . . . . . . . . 21
       |
52 | | fsumo1.4 |
. . . . . . . . . . . . . . . . . . . . 21
 
        |
53 | 51, 52 | o1mptrcl 13686 |
. . . . . . . . . . . . . . . . . . . 20
       |
54 | 53 | an32s 813 |
. . . . . . . . . . . . . . . . . . 19
       |
55 | 54 | adantllr 725 |
. . . . . . . . . . . . . . . . . 18
    
      
   |
56 | 49, 55 | syldan 473 |
. . . . . . . . . . . . . . . . 17
    
      
       |
57 | 41, 42, 47, 56 | fsumsplit 13806 |
. . . . . . . . . . . . . . . 16
   
     
                |
58 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . 19
   |
59 | | nfcsb1v 3379 |
. . . . . . . . . . . . . . . . . . 19
  
 ![]_ ]_](_urbrack.gif)  |
60 | | csbeq1a 3372 |
. . . . . . . . . . . . . . . . . . 19
   ![]_ ]_](_urbrack.gif)   |
61 | 58, 59, 60 | cbvsumi 13763 |
. . . . . . . . . . . . . . . . . 18
          ![]_ ]_](_urbrack.gif)  |
62 | 44 | unssbd 3612 |
. . . . . . . . . . . . . . . . . . . . 21
 

          |
63 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
64 | 63 | snss 4096 |
. . . . . . . . . . . . . . . . . . . . 21

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

        |
66 | 65 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
   
     
   |
67 | 55 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . . . . 20
   
     
 
  |
68 | | nfcsb1v 3379 |
. . . . . . . . . . . . . . . . . . . . . 22
  
 ![]_ ]_](_urbrack.gif)  |
69 | 68 | nfel1 2606 |
. . . . . . . . . . . . . . . . . . . . 21
    ![]_ ]_](_urbrack.gif)
 |
70 | | csbeq1a 3372 |
. . . . . . . . . . . . . . . . . . . . . 22
   ![]_ ]_](_urbrack.gif)   |
71 | 70 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . . . . 21
 
  ![]_ ]_](_urbrack.gif)    |
72 | 69, 71 | rspc 3144 |
. . . . . . . . . . . . . . . . . . . 20
  
  ![]_ ]_](_urbrack.gif)
   |
73 | 66, 67, 72 | sylc 62 |
. . . . . . . . . . . . . . . . . . 19
   
     
   ![]_ ]_](_urbrack.gif)
  |
74 | | csbeq1 3366 |
. . . . . . . . . . . . . . . . . . . 20
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
75 | 74 | sumsn 13807 |
. . . . . . . . . . . . . . . . . . 19
    ![]_ ]_](_urbrack.gif)
 
     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
76 | 66, 73, 75 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
   
     
 
     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
77 | 61, 76 | syl5eq 2497 |
. . . . . . . . . . . . . . . . 17
   
     
       ![]_ ]_](_urbrack.gif)   |
78 | 77 | oveq2d 6306 |
. . . . . . . . . . . . . . . 16
   
     
         
  ![]_ ]_](_urbrack.gif)    |
79 | 57, 78 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
   
     
           ![]_ ]_](_urbrack.gif)    |
80 | 79 | mpteq2dva 4489 |
. . . . . . . . . . . . . 14
 

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

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

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

     
  |
85 | | sumex 13754 |
. . . . . . . . . . . . . . . 16

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

              |
88 | | eqidd 2452 |
. . . . . . . . . . . . . . 15
 

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

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

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

      

      |
95 | | nfcv 2592 |
. . . . . . . . . . . . . . . . 17
   |
96 | 95, 68 | nfmpt 4491 |
. . . . . . . . . . . . . . . 16
     ![]_ ]_](_urbrack.gif)   |
97 | 96 | nfel1 2606 |
. . . . . . . . . . . . . . 15
     ![]_ ]_](_urbrack.gif)      |
98 | 70 | mpteq2dv 4490 |
. . . . . . . . . . . . . . . 16
      ![]_ ]_](_urbrack.gif)    |
99 | 98 | eleq1d 2513 |
. . . . . . . . . . . . . . 15
          ![]_ ]_](_urbrack.gif)        |
100 | 97, 99 | rspc 3144 |
. . . . . . . . . . . . . 14
  

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

         ![]_ ]_](_urbrack.gif)       |
102 | | o1add 13677 |
. . . . . . . . . . . . 13
           ![]_ ]_](_urbrack.gif)        
 
   ![]_ ]_](_urbrack.gif)        |
103 | 92, 101, 102 | syl2anr 481 |
. . . . . . . . . . . 12
   
      
        
 
   ![]_ ]_](_urbrack.gif)        |
104 | 91, 103 | eqeltrd 2529 |
. . . . . . . . . . 11
   
      
                   |
105 | 104 | ex 436 |
. . . . . . . . . 10
 

                           |
106 | 105 | expr 620 |
. . . . . . . . 9
 
        
                   |
107 | 106 | a2d 29 |
. . . . . . . 8
 
                                  |
108 | 37, 107 | syl5 33 |
. . . . . . 7
 
              
               |
109 | 108 | expcom 437 |
. . . . . 6
 
 
                            |
110 | 109 | a2d 29 |
. . . . 5
   
                              |
111 | 110 | adantl 468 |
. . . 4
 

          
                      |
112 | 10, 16, 22, 28, 33, 111 | findcard2s 7812 |
. . 3
             |
113 | 2, 112 | mpcom 37 |
. 2
           |
114 | 1, 113 | mpi 20 |
1
         |