Step | Hyp | Ref
| Expression |
1 | | eqid 2193 |
. . . . 5
         |
2 | | gsumz.z |
. . . . 5
     |
3 | | eqid 2193 |
. . . . 5
       |
4 | | simp1 999 |
. . . . 5
 
   |
5 | | simp2 1000 |
. . . . 5
 
   |
6 | | simp3 1001 |
. . . . 5
 
   |
7 | 1, 2 | mndidcl 13001 |
. . . . . . . 8
       |
8 | 4, 7 | syl 14 |
. . . . . . 7
 
       |
9 | 8 | adantr 276 |
. . . . . 6
  

    
      |
10 | 9 | fmpttd 5705 |
. . . . 5
 
                    |
11 | 1, 2, 3, 4, 5, 6, 10 | gsumfzval 12964 |
. . . 4
 
  g                     
       |
12 | 11 | adantr 276 |
. . 3
  

  g                             |
13 | | simpr 110 |
. . . 4
  

   |
14 | 13 | iftrued 3564 |
. . 3
  

                      |
15 | 12, 14 | eqtrd 2226 |
. 2
  

  g        |
16 | 11 | adantr 276 |
. . 3
  
 
 g                             |
17 | | simpr 110 |
. . . 4
  
 
  |
18 | 17 | iffalsed 3567 |
. . 3
  
 
                                      |
19 | 5 | adantr 276 |
. . . . . 6
  
 
  |
20 | 6 | adantr 276 |
. . . . . 6
  
 
  |
21 | 5 | zred 9429 |
. . . . . . . 8
 
   |
22 | 6 | zred 9429 |
. . . . . . . 8
 
   |
23 | 21, 22 | lenltd 8127 |
. . . . . . 7
 
 
   |
24 | 23 | biimpar 297 |
. . . . . 6
  
 
  |
25 | | eluz2 9588 |
. . . . . 6
         |
26 | 19, 20, 24, 25 | syl3anbrc 1183 |
. . . . 5
  
 
      |
27 | | eluzfz2 10088 |
. . . . 5
    
      |
28 | 26, 27 | syl 14 |
. . . 4
  
 
      |
29 | 4 | adantr 276 |
. . . 4
  
 
  |
30 | | fveqeq2 5555 |
. . . . . 6
             
               
      |
31 | 30 | imbi2d 230 |
. . . . 5
                  

                   |
32 | | fveqeq2 5555 |
. . . . . 6
             
               
      |
33 | 32 | imbi2d 230 |
. . . . 5
                  

                   |
34 | | fveqeq2 5555 |
. . . . . 6
               
               
        |
35 | 34 | imbi2d 230 |
. . . . 5
                    

                     |
36 | | fveqeq2 5555 |
. . . . . 6
             
               
      |
37 | 36 | imbi2d 230 |
. . . . 5
                  

                   |
38 | | eluzel2 9587 |
. . . . . . . . 9
    
  |
39 | 38 | adantr 276 |
. . . . . . . 8
         |
40 | 39 | adantr 276 |
. . . . . . . . . . 11
      

       |
41 | | eluzelz 9591 |
. . . . . . . . . . . 12
    
  |
42 | 41 | ad2antrr 488 |
. . . . . . . . . . 11
      

       |
43 | 40, 42 | fzfigd 10492 |
. . . . . . . . . 10
      

           |
44 | 43 | mptexd 5777 |
. . . . . . . . 9
      

         
  |
45 | | vex 2763 |
. . . . . . . . 9
 |
46 | | fvexg 5565 |
. . . . . . . . 9
             
     |
47 | 44, 45, 46 | sylancl 413 |
. . . . . . . 8
      

                |
48 | | plusgslid 12720 |
. . . . . . . . . . 11
 Slot      
  |
49 | 48 | slotex 12635 |
. . . . . . . . . 10
      |
50 | 49 | ad2antlr 489 |
. . . . . . . . 9
      
   
     |
51 | | simprr 531 |
. . . . . . . . 9
      
   
  |
52 | | ovexg 5944 |
. . . . . . . . 9
               |
53 | 45, 50, 51, 52 | mp3an2i 1353 |
. . . . . . . 8
      
   
  
      |
54 | 39, 47, 53 | seq3-1 10523 |
. . . . . . 7
                                  |
55 | | eqid 2193 |
. . . . . . . 8
         
 |
56 | | eqidd 2194 |
. . . . . . . 8
  |
57 | | eluzfz1 10087 |
. . . . . . . . 9
    
      |
58 | 57 | adantr 276 |
. . . . . . . 8
             |
59 | 7 | adantl 277 |
. . . . . . . 8
             |
60 | 55, 56, 58, 59 | fvmptd3 5643 |
. . . . . . 7
                 |
61 | 54, 60 | eqtrd 2226 |
. . . . . 6
                        |
62 | 61 | ex 115 |
. . . . 5
    

                  |
63 | | elfzouz 10207 |
. . . . . . . . . . 11
  ..^
      |
64 | 63 | adantr 276 |
. . . . . . . . . 10
   ..^        |
65 | | elfzouz2 10218 |
. . . . . . . . . . . 12
  ..^
      |
66 | | uztrn 9599 |
. . . . . . . . . . . 12
          
      |
67 | 65, 63, 66 | syl2anc 411 |
. . . . . . . . . . 11
  ..^
      |
68 | 67, 47 | sylanl1 402 |
. . . . . . . . . 10
    ..^

                |
69 | 67, 53 | sylanl1 402 |
. . . . . . . . . 10
    ..^
   
  
      |
70 | 64, 68, 69 | seq3p1 10526 |
. . . . . . . . 9
   ..^                                
                       |
71 | 70 | adantr 276 |
. . . . . . . 8
    ..^

                                              
                       |
72 | | simpr 110 |
. . . . . . . . 9
    ..^

                                 |
73 | | eqidd 2194 |
. . . . . . . . . . 11
    |
74 | | fzofzp1 10284 |
. . . . . . . . . . . 12
  ..^
        |
75 | 74 | adantr 276 |
. . . . . . . . . . 11
   ..^          |
76 | 7 | adantl 277 |
. . . . . . . . . . 11
   ..^        |
77 | 55, 73, 75, 76 | fvmptd3 5643 |
. . . . . . . . . 10
   ..^              |
78 | 77 | adantr 276 |
. . . . . . . . 9
    ..^

                            |
79 | 72, 78 | oveq12d 5928 |
. . . . . . . 8
    ..^

                            
                          |
80 | 1, 3, 2 | mndlid 13006 |
. . . . . . . . . 10
           |
81 | 7, 80 | mpdan 421 |
. . . . . . . . 9
     |
82 | 81 | ad2antlr 489 |
. . . . . . . 8
    ..^

                    |
83 | 71, 79, 82 | 3eqtrd 2230 |
. . . . . . 7
    ..^

                                   |
84 | 83 | exp31 364 |
. . . . . 6
  ..^

                            
         |
85 | 84 | a2d 26 |
. . . . 5
  ..^
 
                                      |
86 | 31, 33, 35, 37, 62, 85 | fzind2 10296 |
. . . 4
     
                  |
87 | 28, 29, 86 | sylc 62 |
. . 3
  
 
                 |
88 | 16, 18, 87 | 3eqtrd 2230 |
. 2
  
 
 g        |
89 | | zdclt 9384 |
. . . 4
 
 DECID   |
90 | 6, 5, 89 | syl2anc 411 |
. . 3
 

DECID
  |
91 | | exmiddc 837 |
. . 3
DECID
    |
92 | 90, 91 | syl 14 |
. 2
 
     |
93 | 15, 88, 92 | mpjaodan 799 |
1
 
  g        |