Step | Hyp | Ref
| Expression |
1 | | 00id 7623 |
. . . . 5
   |
2 | | sum0 10780 |
. . . . . 6
  |
3 | | sum0 10780 |
. . . . . 6
  |
4 | 2, 3 | oveq12i 5664 |
. . . . 5
 
     |
5 | | sum0 10780 |
. . . . 5
    |
6 | 1, 4, 5 | 3eqtr4ri 2119 |
. . . 4
        |
7 | | sumeq1 10744 |
. . . 4


  
    |
8 | | sumeq1 10744 |
. . . . 5


   |
9 | | sumeq1 10744 |
. . . . 5


   |
10 | 8, 9 | oveq12d 5670 |
. . . 4

 
        |
11 | 6, 7, 10 | 3eqtr4a 2146 |
. . 3


   
    |
12 | 11 | a1i 9 |
. 2
   
  
     |
13 | | simprl 498 |
. . . . . . . . 9
 
 ♯       ♯       ♯    |
14 | | nnuz 9054 |
. . . . . . . . 9
     |
15 | 13, 14 | syl6eleq 2180 |
. . . . . . . 8
 
 ♯       ♯       ♯        |
16 | | elnnuz 9055 |
. . . . . . . . . . . 12

      |
17 | 16 | biimpri 131 |
. . . . . . . . . . 11
    
  |
18 | 17 | adantl 271 |
. . . . . . . . . 10
    ♯       ♯           
  |
19 | | fsumadd.2 |
. . . . . . . . . . . . . . . 16
 
   |
20 | 19 | adantlr 461 |
. . . . . . . . . . . . . . 15
    ♯       ♯          |
21 | 20 | fmpttd 5453 |
. . . . . . . . . . . . . 14
 
 ♯       ♯               |
22 | | simprr 499 |
. . . . . . . . . . . . . . 15
 
 ♯       ♯            ♯       |
23 | | f1of 5253 |
. . . . . . . . . . . . . . 15
      ♯          ♯       |
24 | 22, 23 | syl 14 |
. . . . . . . . . . . . . 14
 
 ♯       ♯            ♯       |
25 | | fco 5176 |
. . . . . . . . . . . . . 14
             ♯               ♯       |
26 | 21, 24, 25 | syl2anc 403 |
. . . . . . . . . . . . 13
 
 ♯       ♯                ♯       |
27 | 26 | ad2antrr 472 |
. . . . . . . . . . . 12
     ♯       ♯           
♯            ♯       |
28 | | 1zzd 8777 |
. . . . . . . . . . . . . 14
     ♯       ♯           
♯     |
29 | 13 | ad2antrr 472 |
. . . . . . . . . . . . . . 15
     ♯       ♯           
♯   ♯    |
30 | 29 | nnzd 8867 |
. . . . . . . . . . . . . 14
     ♯       ♯           
♯   ♯    |
31 | | eluzelz 9028 |
. . . . . . . . . . . . . . 15
    
  |
32 | 31 | ad2antlr 473 |
. . . . . . . . . . . . . 14
     ♯       ♯           
♯  
  |
33 | 28, 30, 32 | 3jca 1123 |
. . . . . . . . . . . . 13
     ♯       ♯           
♯    ♯     |
34 | | eluzle 9031 |
. . . . . . . . . . . . . . 15
    
  |
35 | 34 | ad2antlr 473 |
. . . . . . . . . . . . . 14
     ♯       ♯           
♯  
  |
36 | | simpr 108 |
. . . . . . . . . . . . . 14
     ♯       ♯           
♯   ♯    |
37 | 35, 36 | jca 300 |
. . . . . . . . . . . . 13
     ♯       ♯           
♯   
♯     |
38 | | elfz2 9431 |
. . . . . . . . . . . . 13
    ♯     ♯    ♯      |
39 | 33, 37, 38 | sylanbrc 408 |
. . . . . . . . . . . 12
     ♯       ♯           
♯  
   ♯     |
40 | 27, 39 | ffvelrnd 5435 |
. . . . . . . . . . 11
     ♯       ♯           
♯             |
41 | | 0cnd 7481 |
. . . . . . . . . . 11
     ♯       ♯           
♯  
  |
42 | 18 | nnzd 8867 |
. . . . . . . . . . . 12
    ♯       ♯           
  |
43 | 13 | adantr 270 |
. . . . . . . . . . . . 13
    ♯       ♯           
♯    |
44 | 43 | nnzd 8867 |
. . . . . . . . . . . 12
    ♯       ♯           
♯    |
45 | | zdcle 8823 |
. . . . . . . . . . . 12
  ♯  
DECID
♯    |
46 | 42, 44, 45 | syl2anc 403 |
. . . . . . . . . . 11
    ♯       ♯           
DECID
♯    |
47 | 40, 41, 46 | ifcldadc 3420 |
. . . . . . . . . 10
    ♯       ♯           
 
♯               |
48 | | breq1 3848 |
. . . . . . . . . . . 12
 
♯ 
♯     |
49 | | fveq2 5305 |
. . . . . . . . . . . 12
                   |
50 | 48, 49 | ifbieq1d 3413 |
. . . . . . . . . . 11
   ♯               ♯               |
51 | | eqid 2088 |
. . . . . . . . . . 11
  
♯                 ♯               |
52 | 50, 51 | fvmptg 5380 |
. . . . . . . . . 10
    ♯                  ♯                   ♯               |
53 | 18, 47, 52 | syl2anc 403 |
. . . . . . . . 9
    ♯       ♯           
    ♯                   ♯               |
54 | 53, 47 | eqeltrd 2164 |
. . . . . . . 8
    ♯       ♯           
    ♯                   |
55 | | fsumadd.3 |
. . . . . . . . . . . . . . . 16
 
   |
56 | 55 | adantlr 461 |
. . . . . . . . . . . . . . 15
    ♯       ♯          |
57 | 56 | fmpttd 5453 |
. . . . . . . . . . . . . 14
 
 ♯       ♯               |
58 | 57 | ad2antrr 472 |
. . . . . . . . . . . . 13
     ♯       ♯           
♯           |
59 | 24 | ad2antrr 472 |
. . . . . . . . . . . . 13
     ♯       ♯           
♯        ♯       |
60 | | fco 5176 |
. . . . . . . . . . . . 13
             ♯               ♯       |
61 | 58, 59, 60 | syl2anc 403 |
. . . . . . . . . . . 12
     ♯       ♯           
♯            ♯       |
62 | 61, 39 | ffvelrnd 5435 |
. . . . . . . . . . 11
     ♯       ♯           
♯             |
63 | 62, 41, 46 | ifcldadc 3420 |
. . . . . . . . . 10
    ♯       ♯           
 
♯               |
64 | | fveq2 5305 |
. . . . . . . . . . . 12
                   |
65 | 48, 64 | ifbieq1d 3413 |
. . . . . . . . . . 11
   ♯               ♯               |
66 | | eqid 2088 |
. . . . . . . . . . 11
  
♯                 ♯               |
67 | 65, 66 | fvmptg 5380 |
. . . . . . . . . 10
    ♯                  ♯                   ♯               |
68 | 18, 63, 67 | syl2anc 403 |
. . . . . . . . 9
    ♯       ♯           
    ♯                   ♯               |
69 | 68, 63 | eqeltrd 2164 |
. . . . . . . 8
    ♯       ♯           
    ♯                   |
70 | | simpll 496 |
. . . . . . . . . . . 12
     ♯       ♯           
♯   
 ♯       ♯         |
71 | 24 | ffvelrnda 5434 |
. . . . . . . . . . . . . 14
    ♯       ♯          ♯          |
72 | | simpr 108 |
. . . . . . . . . . . . . . . . . 18
 
   |
73 | 19, 55 | addcld 7507 |
. . . . . . . . . . . . . . . . . 18
 
 
   |
74 | | eqid 2088 |
. . . . . . . . . . . . . . . . . . 19
         |
75 | 74 | fvmpt2 5386 |
. . . . . . . . . . . . . . . . . 18
  
              |
76 | 72, 73, 75 | syl2anc 403 |
. . . . . . . . . . . . . . . . 17
 
             |
77 | | eqid 2088 |
. . . . . . . . . . . . . . . . . . . 20
     |
78 | 77 | fvmpt2 5386 |
. . . . . . . . . . . . . . . . . . 19
 
         |
79 | 72, 19, 78 | syl2anc 403 |
. . . . . . . . . . . . . . . . . 18
 
         |
80 | | eqid 2088 |
. . . . . . . . . . . . . . . . . . . 20
     |
81 | 80 | fvmpt2 5386 |
. . . . . . . . . . . . . . . . . . 19
 
         |
82 | 72, 55, 81 | syl2anc 403 |
. . . . . . . . . . . . . . . . . 18
 
         |
83 | 79, 82 | oveq12d 5670 |
. . . . . . . . . . . . . . . . 17
 
                   |
84 | 76, 83 | eqtr4d 2123 |
. . . . . . . . . . . . . . . 16
 
                         |
85 | 84 | ralrimiva 2446 |
. . . . . . . . . . . . . . 15
                          |
86 | 85 | ad2antrr 472 |
. . . . . . . . . . . . . 14
    ♯       ♯          ♯                             |
87 | | nffvmpt1 5316 |
. . . . . . . . . . . . . . . 16
               |
88 | | nffvmpt1 5316 |
. . . . . . . . . . . . . . . . 17
             |
89 | | nfcv 2228 |
. . . . . . . . . . . . . . . . 17
  |
90 | | nffvmpt1 5316 |
. . . . . . . . . . . . . . . . 17
             |
91 | 88, 89, 90 | nfov 5679 |
. . . . . . . . . . . . . . . 16
                         |
92 | 87, 91 | nfeq 2236 |
. . . . . . . . . . . . . . 15
                                     |
93 | | fveq2 5305 |
. . . . . . . . . . . . . . . 16
                           |
94 | | fveq2 5305 |
. . . . . . . . . . . . . . . . 17
                       |
95 | | fveq2 5305 |
. . . . . . . . . . . . . . . . 17
                       |
96 | 94, 95 | oveq12d 5670 |
. . . . . . . . . . . . . . . 16
                                           |
97 | 93, 96 | eqeq12d 2102 |
. . . . . . . . . . . . . . 15
                           
                                     |
98 | 92, 97 | rspc 2716 |
. . . . . . . . . . . . . 14
      
                                                           |
99 | 71, 86, 98 | sylc 61 |
. . . . . . . . . . . . 13
    ♯       ♯          ♯                                        |
100 | | fvco3 5375 |
. . . . . . . . . . . . . 14
       ♯    
   ♯                            |
101 | 24, 100 | sylan 277 |
. . . . . . . . . . . . 13
    ♯       ♯          ♯                            |
102 | | fvco3 5375 |
. . . . . . . . . . . . . . 15
       ♯    
   ♯                        |
103 | 24, 102 | sylan 277 |
. . . . . . . . . . . . . 14
    ♯       ♯          ♯                        |
104 | | fvco3 5375 |
. . . . . . . . . . . . . . 15
       ♯    
   ♯                        |
105 | 24, 104 | sylan 277 |
. . . . . . . . . . . . . 14
    ♯       ♯          ♯                        |
106 | 103, 105 | oveq12d 5670 |
. . . . . . . . . . . . 13
    ♯       ♯          ♯                                              |
107 | 99, 101, 106 | 3eqtr4d 2130 |
. . . . . . . . . . . 12
    ♯       ♯          ♯                                  |
108 | 70, 39, 107 | syl2anc 403 |
. . . . . . . . . . 11
     ♯       ♯           
♯                                 |
109 | 36 | iftrued 3400 |
. . . . . . . . . . 11
     ♯       ♯           
♯     ♯                           |
110 | 36 | iftrued 3400 |
. . . . . . . . . . . 12
     ♯       ♯           
♯     ♯                       |
111 | 36 | iftrued 3400 |
. . . . . . . . . . . 12
     ♯       ♯           
♯     ♯                       |
112 | 110, 111 | oveq12d 5670 |
. . . . . . . . . . 11
     ♯       ♯           
♯      ♯              
♯                                  |
113 | 108, 109,
112 | 3eqtr4d 2130 |
. . . . . . . . . 10
     ♯       ♯           
♯     ♯                 
♯               ♯                |
114 | 1 | eqcomi 2092 |
. . . . . . . . . . 11
   |
115 | | simpr 108 |
. . . . . . . . . . . 12
     ♯       ♯           
♯  
♯    |
116 | 115 | iffalsed 3403 |
. . . . . . . . . . 11
     ♯       ♯           
♯  
 
♯                 |
117 | 115 | iffalsed 3403 |
. . . . . . . . . . . 12
     ♯       ♯           
♯  
 
♯               |
118 | 115 | iffalsed 3403 |
. . . . . . . . . . . 12
     ♯       ♯           
♯  
 
♯               |
119 | 117, 118 | oveq12d 5670 |
. . . . . . . . . . 11
     ♯       ♯           
♯  
  
♯               ♯                  |
120 | 114, 116,
119 | 3eqtr4a 2146 |
. . . . . . . . . 10
     ♯       ♯           
♯  
 
♯                  ♯              
♯                |
121 | | exmiddc 782 |
. . . . . . . . . . 11
DECID ♯   ♯  ♯     |
122 | 46, 121 | syl 14 |
. . . . . . . . . 10
    ♯       ♯           
 ♯  ♯     |
123 | 113, 120,
122 | mpjaodan 747 |
. . . . . . . . 9
    ♯       ♯           
 
♯                  ♯              
♯                |
124 | 73 | fmpttd 5453 |
. . . . . . . . . . . . . 14
           |
125 | 124 | ad3antrrr 476 |
. . . . . . . . . . . . 13
     ♯       ♯           
♯             |
126 | | fco 5176 |
. . . . . . . . . . . . 13
               ♯                 ♯       |
127 | 125, 59, 126 | syl2anc 403 |
. . . . . . . . . . . 12
     ♯       ♯           
♯              ♯       |
128 | 127, 39 | ffvelrnd 5435 |
. . . . . . . . . . 11
     ♯       ♯           
♯               |
129 | 128, 41, 46 | ifcldadc 3420 |
. . . . . . . . . 10
    ♯       ♯           
 
♯                 |
130 | | fveq2 5305 |
. . . . . . . . . . . 12
                       |
131 | 48, 130 | ifbieq1d 3413 |
. . . . . . . . . . 11
   ♯                 ♯                 |
132 | | eqid 2088 |
. . . . . . . . . . 11
  
♯                   ♯                 |
133 | 131, 132 | fvmptg 5380 |
. . . . . . . . . 10
    ♯                    ♯                     ♯                 |
134 | 18, 129, 133 | syl2anc 403 |
. . . . . . . . 9
    ♯       ♯           
    ♯                     ♯                 |
135 | 53, 68 | oveq12d 5670 |
. . . . . . . . 9
    ♯       ♯           
     ♯                    
♯                    
♯               ♯                |
136 | 123, 134,
135 | 3eqtr4d 2130 |
. . . . . . . 8
    ♯       ♯           
    ♯                        ♯                    
♯                    |
137 | 15, 54, 69, 136 | iseradd 9934 |
. . . . . . 7
 
 ♯       ♯            ♯                    ♯         ♯                  ♯        ♯                  ♯      |
138 | | fveq2 5305 |
. . . . . . . . 9
                           |
139 | 20, 56 | addcld 7507 |
. . . . . . . . . . 11
    ♯       ♯        
   |
140 | 139 | fmpttd 5453 |
. . . . . . . . . 10
 
 ♯       ♯                 |
141 | 140 | ffvelrnda 5434 |
. . . . . . . . 9
    ♯       ♯                  |
142 | 138, 13, 22, 141, 101 | fisum 10778 |
. . . . . . . 8
 
 ♯       ♯                     ♯                    ♯     |
143 | | breq1 3848 |
. . . . . . . . . . . 12
 
♯  ♯     |
144 | | fveq2 5305 |
. . . . . . . . . . . 12
                       |
145 | 143, 144 | ifbieq1d 3413 |
. . . . . . . . . . 11
  
♯                 ♯                 |
146 | 145 | cbvmptv 3934 |
. . . . . . . . . 10
  
♯                   ♯                 |
147 | | iseqeq3 9860 |
. . . . . . . . . 10
    ♯                  
♯                     ♯                       ♯                    |
148 | 146, 147 | ax-mp 7 |
. . . . . . . . 9
     ♯                      
♯                   |
149 | 148 | fveq1i 5306 |
. . . . . . . 8
     ♯                    ♯        ♯                    ♯    |
150 | 142, 149 | syl6eq 2136 |
. . . . . . 7
 
 ♯       ♯                     ♯                    ♯     |
151 | | fveq2 5305 |
. . . . . . . . . 10
                       |
152 | 21 | ffvelrnda 5434 |
. . . . . . . . . 10
    ♯       ♯                |
153 | 151, 13, 22, 152, 103 | fisum 10778 |
. . . . . . . . 9
 
 ♯       ♯                   ♯                  ♯     |
154 | | fveq2 5305 |
. . . . . . . . . . . . 13
                   |
155 | 143, 154 | ifbieq1d 3413 |
. . . . . . . . . . . 12
  
♯               ♯               |
156 | 155 | cbvmptv 3934 |
. . . . . . . . . . 11
  
♯                 ♯               |
157 | | iseqeq3 9860 |
. . . . . . . . . . 11
    ♯                
♯                   ♯                     ♯                  |
158 | 156, 157 | ax-mp 7 |
. . . . . . . . . 10
     ♯                    
♯                 |
159 | 158 | fveq1i 5306 |
. . . . . . . . 9
     ♯                  ♯        ♯                  ♯    |
160 | 153, 159 | syl6eq 2136 |
. . . . . . . 8
 
 ♯       ♯                   ♯                  ♯     |
161 | | fveq2 5305 |
. . . . . . . . . 10
                       |
162 | 57 | ffvelrnda 5434 |
. . . . . . . . . 10
    ♯       ♯                |
163 | 161, 13, 22, 162, 105 | fisum 10778 |
. . . . . . . . 9
 
 ♯       ♯                   ♯                  ♯     |
164 | | fveq2 5305 |
. . . . . . . . . . . . 13
                   |
165 | 143, 164 | ifbieq1d 3413 |
. . . . . . . . . . . 12
  
♯               ♯               |
166 | 165 | cbvmptv 3934 |
. . . . . . . . . . 11
  
♯                 ♯               |
167 | | iseqeq3 9860 |
. . . . . . . . . . 11
    ♯                
♯                   ♯                     ♯                  |
168 | 166, 167 | ax-mp 7 |
. . . . . . . . . 10
     ♯                    
♯                 |
169 | 168 | fveq1i 5306 |
. . . . . . . . 9
     ♯                  ♯        ♯                  ♯    |
170 | 163, 169 | syl6eq 2136 |
. . . . . . . 8
 
 ♯       ♯                   ♯                  ♯     |
171 | 160, 170 | oveq12d 5670 |
. . . . . . 7
 
 ♯       ♯                             ♯                  ♯       
♯                  ♯      |
172 | 137, 150,
171 | 3eqtr4d 2130 |
. . . . . 6
 
 ♯       ♯                                  |
173 | 73 | ralrimiva 2446 |
. . . . . . . 8
  
   |
174 | | sumfct 10763 |
. . . . . . . 8
 


          
   |
175 | 173, 174 | syl 14 |
. . . . . . 7
 
        

   |
176 | 175 | adantr 270 |
. . . . . 6
 
 ♯       ♯                
    |
177 | 19 | ralrimiva 2446 |
. . . . . . . . 9
 
  |
178 | | sumfct 10763 |
. . . . . . . . 9
 
          |
179 | 177, 178 | syl 14 |
. . . . . . . 8
 
      
  |
180 | 55 | ralrimiva 2446 |
. . . . . . . . 9
 
  |
181 | | sumfct 10763 |
. . . . . . . . 9
 
          |
182 | 180, 181 | syl 14 |
. . . . . . . 8
 
      
  |
183 | 179, 182 | oveq12d 5670 |
. . . . . . 7
                  
    |
184 | 183 | adantr 270 |
. . . . . 6
 
 ♯       ♯                        
    |
185 | 172, 176,
184 | 3eqtr3d 2128 |
. . . . 5
 
 ♯       ♯           
    |
186 | 185 | expr 367 |
. . . 4
 
♯         ♯         
     |
187 | 186 | exlimdv 1747 |
. . 3
 
♯          ♯    
    
     |
188 | 187 | expimpd 355 |
. 2
   ♯        ♯      
   
     |
189 | | fsumadd.1 |
. . 3
   |
190 | | fz1f1o 10764 |
. . 3
 
 ♯        ♯         |
191 | 189, 190 | syl 14 |
. 2
   ♯        ♯         |
192 | 12, 188, 191 | mpjaod 673 |
1
  
  
    |