Step | Hyp | Ref
| Expression |
1 | | simpr 110 |
. . . 4
 

  |
2 | 1 | iftrued 3564 |
. . 3
 

         
                   |
3 | | gsummptfidmadd.b |
. . . . 5
     |
4 | | eqid 2193 |
. . . . 5
         |
5 | | gsummptfidmadd.p |
. . . . 5
    |
6 | | gsummptfidmadd.g |
. . . . 5
 CMnd |
7 | | gsumfzmptfidmadd.m |
. . . . 5
   |
8 | | gsumfzmptfidmadd.n |
. . . . 5
   |
9 | 6 | cmnmndd 13367 |
. . . . . . . 8
   |
10 | 9 | adantr 276 |
. . . . . . 7
 
    
  |
11 | | gsumfzmptfidmadd.c |
. . . . . . 7
 
    
  |
12 | | gsumfzmptfidmadd.d |
. . . . . . 7
 
    
  |
13 | 3, 5 | mndcl 12994 |
. . . . . . 7
 
     |
14 | 10, 11, 12, 13 | syl3anc 1249 |
. . . . . 6
 
    
    |
15 | 14 | fmpttd 5705 |
. . . . 5
                   |
16 | 3, 4, 5, 6, 7, 8, 15 | gsumfzval 12964 |
. . . 4
  g                                   |
17 | 16 | adantr 276 |
. . 3
 

 g                                   |
18 | | gsumfzmptfidmadd.f |
. . . . . . . . 9
       |
19 | 11, 18 | fmptd 5704 |
. . . . . . . 8
           |
20 | 3, 4, 5, 6, 7, 8, 19 | gsumfzval 12964 |
. . . . . . 7
  g                   |
21 | 20 | adantr 276 |
. . . . . 6
 

 g                   |
22 | 1 | iftrued 3564 |
. . . . . 6
 

         
           |
23 | 21, 22 | eqtrd 2226 |
. . . . 5
 

 g        |
24 | | gsumfzmptfidmadd.h |
. . . . . . . . 9
       |
25 | 12, 24 | fmptd 5704 |
. . . . . . . 8
           |
26 | 3, 4, 5, 6, 7, 8, 25 | gsumfzval 12964 |
. . . . . . 7
  g                   |
27 | 26 | adantr 276 |
. . . . . 6
 

 g                   |
28 | 1 | iftrued 3564 |
. . . . . 6
 

         
           |
29 | 27, 28 | eqtrd 2226 |
. . . . 5
 

 g        |
30 | 23, 29 | oveq12d 5928 |
. . . 4
 

  g   g               |
31 | 3, 4 | mndidcl 13001 |
. . . . . 6
       |
32 | 3, 5, 4 | mndlid 13006 |
. . . . . 6
                       |
33 | 9, 31, 32 | syl2anc2 412 |
. . . . 5
                 |
34 | 33 | adantr 276 |
. . . 4
 

                |
35 | 30, 34 | eqtrd 2226 |
. . 3
 

  g   g         |
36 | 2, 17, 35 | 3eqtr4d 2236 |
. 2
 

 g            g   g     |
37 | 9 | ad2antrr 488 |
. . . . 5
    
    |
38 | | simprl 529 |
. . . . 5
    
    |
39 | | simprr 531 |
. . . . 5
    
    |
40 | 3, 5 | mndcl 12994 |
. . . . 5
 
     |
41 | 37, 38, 39, 40 | syl3anc 1249 |
. . . 4
    
  
   |
42 | 6 | ad2antrr 488 |
. . . . 5
    
  CMnd |
43 | 3, 5 | cmncom 13361 |
. . . . 5
  CMnd
 
     |
44 | 42, 38, 39, 43 | syl3anc 1249 |
. . . 4
    
  
     |
45 | 9 | ad2antrr 488 |
. . . . 5
    
    |
46 | 3, 5 | mndass 12995 |
. . . . 5
  
    
       |
47 | 45, 46 | sylancom 420 |
. . . 4
    
    
       |
48 | 7 | adantr 276 |
. . . . 5
 
   |
49 | 8 | adantr 276 |
. . . . 5
 
   |
50 | 48 | zred 9429 |
. . . . . 6
 
   |
51 | 49 | zred 9429 |
. . . . . 6
 
   |
52 | | simpr 110 |
. . . . . 6
 
   |
53 | 50, 51, 52 | nltled 8130 |
. . . . 5
 
   |
54 | | eluz2 9588 |
. . . . 5
         |
55 | 48, 49, 53, 54 | syl3anbrc 1183 |
. . . 4
 
       |
56 | 19 | adantr 276 |
. . . . 5
 
           |
57 | 56 | ffvelcdmda 5685 |
. . . 4
   
           |
58 | 25 | adantr 276 |
. . . . 5
 
           |
59 | 58 | ffvelcdmda 5685 |
. . . 4
   
           |
60 | 7, 8 | fzfigd 10492 |
. . . . . . . 8
       |
61 | 18 | a1i 9 |
. . . . . . . 8
         |
62 | 24 | a1i 9 |
. . . . . . . 8
         |
63 | 60, 11, 12, 61, 62 | offval2 6138 |
. . . . . . 7
              |
64 | 63 | fveq1d 5548 |
. . . . . 6
                      |
65 | 64 | ad2antrr 488 |
. . . . 5
   
                          |
66 | 19 | ffnd 5396 |
. . . . . . 7
       |
67 | 25 | ffnd 5396 |
. . . . . . 7
       |
68 | | inidm 3368 |
. . . . . . 7
               |
69 | | eqidd 2194 |
. . . . . . 7
 
    
          |
70 | | eqidd 2194 |
. . . . . . 7
 
    
          |
71 | 9 | adantr 276 |
. . . . . . . 8
 
    
  |
72 | 19 | ffvelcdmda 5685 |
. . . . . . . 8
 
    
      |
73 | 25 | ffvelcdmda 5685 |
. . . . . . . 8
 
    
      |
74 | 3, 5 | mndcl 12994 |
. . . . . . . 8
               
       |
75 | 71, 72, 73, 74 | syl3anc 1249 |
. . . . . . 7
 
    
            |
76 | 66, 67, 60, 60, 68, 69, 70, 75 | ofvalg 6132 |
. . . . . 6
 
    
                   |
77 | 76 | adantlr 477 |
. . . . 5
   
                
       |
78 | 65, 77 | eqtr3d 2228 |
. . . 4
   
                     
       |
79 | | plusgslid 12720 |
. . . . . . . 8
 Slot      
  |
80 | 79 | slotex 12635 |
. . . . . . 7
 CMnd      |
81 | 6, 80 | syl 14 |
. . . . . 6
      |
82 | 5, 81 | eqeltrid 2280 |
. . . . 5
   |
83 | 82 | adantr 276 |
. . . 4
 
   |
84 | 19, 60 | fexd 5780 |
. . . . 5
   |
85 | 84 | adantr 276 |
. . . 4
 
   |
86 | 25, 60 | fexd 5780 |
. . . . 5
   |
87 | 86 | adantr 276 |
. . . 4
 
   |
88 | 15, 60 | fexd 5780 |
. . . . 5
           |
89 | 88 | adantr 276 |
. . . 4
 
           |
90 | 41, 44, 47, 55, 57, 59, 78, 83, 85, 87, 89 | seqcaoprg 10557 |
. . 3
 
                               |
91 | 16 | adantr 276 |
. . . 4
 
  g                                   |
92 | 52 | iffalsed 3567 |
. . . 4
 
  
                                     |
93 | 91, 92 | eqtrd 2226 |
. . 3
 
  g                          |
94 | 20 | adantr 276 |
. . . . 5
 
  g                   |
95 | 52 | iffalsed 3567 |
. . . . 5
 
  
                     |
96 | 94, 95 | eqtrd 2226 |
. . . 4
 
  g          |
97 | 26 | adantr 276 |
. . . . 5
 
  g                   |
98 | 52 | iffalsed 3567 |
. . . . 5
 
  
                     |
99 | 97, 98 | eqtrd 2226 |
. . . 4
 
  g          |
100 | 96, 99 | oveq12d 5928 |
. . 3
 
   g   g     
   
         |
101 | 90, 93, 100 | 3eqtr4d 2236 |
. 2
 
  g            g   g     |
102 | | zdclt 9384 |
. . . 4
 
 DECID   |
103 | 8, 7, 102 | syl2anc 411 |
. . 3
 DECID   |
104 | | exmiddc 837 |
. . 3
DECID
    |
105 | 103, 104 | syl 14 |
. 2
     |
106 | 36, 101, 105 | mpjaodan 799 |
1
  g            g   g     |