Step | Hyp | Ref
| Expression |
1 | | eqid 2461 |
. . . 4
       |
2 | 1 | mpt2fun 6424 |
. . 3
    |
3 | 2 | a1i 11 |
. 2
      |
4 | | gsum2d2.u |
. . 3
   |
5 | | gsum2d2.f |
. . . . . 6
 

 
  |
6 | 5 | ralrimivva 2820 |
. . . . 5
  
  |
7 | 1 | fmpt2x 6885 |
. . . . 5
 

              |
8 | 6, 7 | sylib 201 |
. . . 4
  
   
        |
9 | | relxp 4960 |
. . . . . . . 8
     |
10 | 9 | rgenw 2760 |
. . . . . . 7

     |
11 | | reliun 4972 |
. . . . . . 7
 
   

      |
12 | 10, 11 | mpbir 214 |
. . . . . 6

     |
13 | | eldifi 3566 |
. . . . . . 7
  
   
 
      |
14 | 13 | adantl 472 |
. . . . . 6
 
               |
15 | | elrel 4955 |
. . . . . 6
                     |
16 | 12, 14, 15 | sylancr 674 |
. . . . 5
 
          
     |
17 | | nfv 1771 |
. . . . . . 7
   |
18 | | nfiu1 4321 |
. . . . . . . . 9
  
     |
19 | | nfcv 2602 |
. . . . . . . . 9
   |
20 | 18, 19 | nfdif 3565 |
. . . . . . . 8
          |
21 | 20 | nfcri 2596 |
. . . . . . 7
  
      |
22 | 17, 21 | nfan 2021 |
. . . . . 6
            |
23 | | nfmpt21 6384 |
. . . . . . . 8
   
  |
24 | | nfcv 2602 |
. . . . . . . 8
   |
25 | 23, 24 | nffv 5894 |
. . . . . . 7
          |
26 | 25 | nfeq1 2615 |
. . . . . 6
          |
27 | | nfv 1771 |
. . . . . . 7
            |
28 | | nfmpt22 6385 |
. . . . . . . . 9
   
  |
29 | | nfcv 2602 |
. . . . . . . . 9
   |
30 | 28, 29 | nffv 5894 |
. . . . . . . 8
          |
31 | 30 | nfeq1 2615 |
. . . . . . 7
          |
32 | | simprr 771 |
. . . . . . . . . 10
 
       
          |
33 | 32 | fveq2d 5891 |
. . . . . . . . 9
 
       
              
         |
34 | | df-ov 6317 |
. . . . . . . . . 10
   
              |
35 | | simprl 769 |
. . . . . . . . . . . . . . 15
 
       
      
       |
36 | 32, 35 | eqeltrrd 2540 |
. . . . . . . . . . . . . 14
 
       
                 |
37 | 36 | eldifad 3427 |
. . . . . . . . . . . . 13
 
       
               |
38 | | opeliunxp 4904 |
. . . . . . . . . . . . 13
        

   |
39 | 37, 38 | sylib 201 |
. . . . . . . . . . . 12
 
       
     
   |
40 | 39 | simpld 465 |
. . . . . . . . . . 11
 
       
       |
41 | 39 | simprd 469 |
. . . . . . . . . . 11
 
       
       |
42 | 39, 5 | syldan 477 |
. . . . . . . . . . 11
 
       
    
  |
43 | 1 | ovmpt4g 6445 |
. . . . . . . . . . 11
 
          |
44 | 40, 41, 42, 43 | syl3anc 1276 |
. . . . . . . . . 10
 
       
              |
45 | 34, 44 | syl5eqr 2509 |
. . . . . . . . 9
 
       
                 |
46 | | eldifn 3567 |
. . . . . . . . . . . . 13
  
   
   |
47 | 46 | ad2antrl 739 |
. . . . . . . . . . . 12
 
       
    
  |
48 | 32 | eleq1d 2523 |
. . . . . . . . . . . . 13
 
       
            |
49 | | df-br 4416 |
. . . . . . . . . . . . 13
  
  
  |
50 | 48, 49 | syl6bbr 271 |
. . . . . . . . . . . 12
 
       
           |
51 | 47, 50 | mtbid 306 |
. . . . . . . . . . 11
 
       
         |
52 | 39, 51 | jca 539 |
. . . . . . . . . 10
 
       
             |
53 | | gsum2d2.n |
. . . . . . . . . 10
 
 
      |
54 | 52, 53 | syldan 477 |
. . . . . . . . 9
 
       
    
 |
55 | 33, 45, 54 | 3eqtrd 2499 |
. . . . . . . 8
 
       
             |
56 | 55 | expr 624 |
. . . . . . 7
 
              
      |
57 | 27, 31, 56 | exlimd 2007 |
. . . . . 6
 
         
            |
58 | 22, 26, 57 | exlimd 2007 |
. . . . 5
 
                        |
59 | 16, 58 | mpd 15 |
. . . 4
 
          
     |
60 | 8, 59 | suppss 6971 |
. . 3
     supp   |
61 | | ssfi 7817 |
. . 3
      supp      supp
  |
62 | 4, 60, 61 | syl2anc 671 |
. 2
     supp
  |
63 | | gsum2d2.a |
. . . 4
   |
64 | | gsum2d2.r |
. . . . 5
 
   |
65 | 64 | ralrimiva 2813 |
. . . 4
 
  |
66 | 1 | mpt2exxg 6893 |
. . . 4
         |
67 | 63, 65, 66 | syl2anc 671 |
. . 3
  
   |
68 | | gsum2d2.z |
. . . . 5
     |
69 | | fvex 5897 |
. . . . 5
     |
70 | 68, 69 | eqeltri 2535 |
. . . 4
 |
71 | 70 | a1i 11 |
. . 3
   |
72 | | isfsupp 7912 |
. . 3
   
      finSupp   
   
 supp     |
73 | 67, 71, 72 | syl2anc 671 |
. 2
     finSupp   
   
 supp     |
74 | 3, 62, 73 | mpbir2and 938 |
1
  
 finSupp  |