Step | Hyp | Ref
| Expression |
1 | | gsumval.b |
. . 3
     |
2 | | gsumval.z |
. . 3
     |
3 | | gsumval.p |
. . 3
    |
4 | | gsumval.g |
. . 3
   |
5 | | gsumfzval.m |
. . . 4
   |
6 | | gsumfzval.n |
. . . 4
   |
7 | 5, 6 | fzfigd 10492 |
. . 3
       |
8 | | gsumfzval.f |
. . 3
           |
9 | 1, 2, 3, 4, 7, 8 | igsumval 12963 |
. 2
  g                           
           |
10 | | fn0g 12948 |
. . . . . 6
 |
11 | 4 | elexd 2773 |
. . . . . 6
   |
12 | | funfvex 5563 |
. . . . . . 7
         |
13 | 12 | funfni 5346 |
. . . . . 6
 
       |
14 | 10, 11, 13 | sylancr 414 |
. . . . 5
       |
15 | 2, 14 | eqeltrid 2280 |
. . . 4
   |
16 | | seqex 10510 |
. . . . 5
 
  |
17 | | fvexg 5565 |
. . . . 5
      
      |
18 | 16, 6, 17 | sylancr 414 |
. . . 4
         |
19 | 15, 18 | ifexd 4513 |
. . 3
             |
20 | | zdclt 9384 |
. . . . . . . 8
 
 DECID   |
21 | 6, 5, 20 | syl2anc 411 |
. . . . . . 7
 DECID   |
22 | | eqifdc 3592 |
. . . . . . 7
DECID
          
  
           |
23 | 21, 22 | syl 14 |
. . . . . 6
           
  
           |
24 | | fzn 10098 |
. . . . . . . . 9
 
         |
25 | 5, 6, 24 | syl2anc 411 |
. . . . . . . 8
         |
26 | 25 | anbi1d 465 |
. . . . . . 7
  
        |
27 | 5 | adantr 276 |
. . . . . . . . . 10
 

       
  |
28 | 27 | zred 9429 |
. . . . . . . . . . . . 13
 

       
  |
29 | 6 | adantr 276 |
. . . . . . . . . . . . . 14
 

       
  |
30 | 29 | zred 9429 |
. . . . . . . . . . . . 13
 

       
  |
31 | | simprl 529 |
. . . . . . . . . . . . 13
 

       
  |
32 | 28, 30, 31 | nltled 8130 |
. . . . . . . . . . . 12
 

       
  |
33 | | eluz 9595 |
. . . . . . . . . . . . 13
 
     
   |
34 | 27, 29, 33 | syl2anc 411 |
. . . . . . . . . . . 12
 

       
        |
35 | 32, 34 | mpbird 167 |
. . . . . . . . . . 11
 

       
      |
36 | | oveq2 5918 |
. . . . . . . . . . . . . 14
           |
37 | 36 | eqeq2d 2205 |
. . . . . . . . . . . . 13
         
           |
38 | | fveq2 5546 |
. . . . . . . . . . . . . 14
               |
39 | 38 | eqeq2d 2205 |
. . . . . . . . . . . . 13
       
         |
40 | 37, 39 | anbi12d 473 |
. . . . . . . . . . . 12
                 
        
          |
41 | 40 | adantl 277 |
. . . . . . . . . . 11
   
       
          
      
        
          |
42 | | eqidd 2194 |
. . . . . . . . . . . 12
 

       
          |
43 | | simprr 531 |
. . . . . . . . . . . 12
 

       
        |
44 | 42, 43 | jca 306 |
. . . . . . . . . . 11
 

       
        
         |
45 | 35, 41, 44 | rspcedvd 2870 |
. . . . . . . . . 10
 

       
                        |
46 | | fveq2 5546 |
. . . . . . . . . . . 12
           |
47 | | oveq1 5917 |
. . . . . . . . . . . . . 14
           |
48 | 47 | eqeq2d 2205 |
. . . . . . . . . . . . 13
         
           |
49 | | seqeq1 10511 |
. . . . . . . . . . . . . . 15
         |
50 | 49 | fveq1d 5548 |
. . . . . . . . . . . . . 14
               |
51 | 50 | eqeq2d 2205 |
. . . . . . . . . . . . 13
       
         |
52 | 48, 51 | anbi12d 473 |
. . . . . . . . . . . 12
                 
        
          |
53 | 46, 52 | rexeqbidv 2707 |
. . . . . . . . . . 11
  
             
      
                         |
54 | 53 | spcegv 2848 |
. . . . . . . . . 10
  
             
         
             
          |
55 | 27, 45, 54 | sylc 62 |
. . . . . . . . 9
 

       
  
             
         |
56 | 55 | ex 115 |
. . . . . . . 8
                                     |
57 | | eluzel2 9587 |
. . . . . . . . . . . . . . 15
    
  |
58 | 57 | ad2antlr 489 |
. . . . . . . . . . . . . 14
       
        
       
  |
59 | 58 | zred 9429 |
. . . . . . . . . . . . 13
       
        
       
  |
60 | | eluzelre 9592 |
. . . . . . . . . . . . . 14
    
  |
61 | 60 | ad2antlr 489 |
. . . . . . . . . . . . 13
       
        
       
  |
62 | | eluzle 9594 |
. . . . . . . . . . . . . 14
    
  |
63 | 62 | ad2antlr 489 |
. . . . . . . . . . . . 13
       
        
          |
64 | 59, 61, 63 | lensymd 8131 |
. . . . . . . . . . . 12
       
        
       
  |
65 | | simprl 529 |
. . . . . . . . . . . . . . . 16
       
        
                  |
66 | 65 | eqcomd 2199 |
. . . . . . . . . . . . . . 15
       
        
                  |
67 | | fzopth 10117 |
. . . . . . . . . . . . . . . 16
    
              |
68 | 67 | ad2antlr 489 |
. . . . . . . . . . . . . . 15
       
        
                      |
69 | 66, 68 | mpbid 147 |
. . . . . . . . . . . . . 14
       
        
            |
70 | 69 | simprd 114 |
. . . . . . . . . . . . 13
       
        
       
  |
71 | 69 | simpld 112 |
. . . . . . . . . . . . 13
       
        
       
  |
72 | 70, 71 | breq12d 4042 |
. . . . . . . . . . . 12
       
        
            |
73 | 64, 72 | mtbid 673 |
. . . . . . . . . . 11
       
        
       
  |
74 | | simprr 531 |
. . . . . . . . . . . 12
       
        
       
        |
75 | 71 | seqeq1d 10514 |
. . . . . . . . . . . . 13
       
        
                |
76 | 75, 70 | fveq12d 5553 |
. . . . . . . . . . . 12
       
        
                      |
77 | 74, 76 | eqtrd 2226 |
. . . . . . . . . . 11
       
        
       
        |
78 | 73, 77 | jca 306 |
. . . . . . . . . 10
       
        
        
         |
79 | 78 | rexlimdva2 2614 |
. . . . . . . . 9
                        
          |
80 | 79 | exlimdv 1830 |
. . . . . . . 8
    
             
 
    

          |
81 | 56, 80 | impbid 129 |
. . . . . . 7
                                     |
82 | 26, 81 | orbi12d 794 |
. . . . . 6
    
       
                      
           |
83 | 23, 82 | bitr2d 189 |
. . . . 5
       
                
       
             |
84 | 83 | adantr 276 |
. . . 4
 
                 
                
       
             |
85 | 84 | iota5 5228 |
. . 3
 
                                    
                     |
86 | 19, 85 | mpdan 421 |
. 2
                                                |
87 | 9, 86 | eqtrd 2226 |
1
  g              |