Step Hyp Ref
Expression 1 0cn 9609 . . . . . . . 8
2 fsumrelem.3 . . . . . . . . 9
3 2 ffvelrni 6030 . . . . . . . 8
4 1 , 3 ax-mp 5 . . . . . . 7
5 4 addid1i 9788 . . . . . 6
6 oveq1 6303 . . . . . . . . . 10
7 6 fveq2d 5875 . . . . . . . . 9
8 fveq2 5871 . . . . . . . . . 10
9 8 oveq1d 6311 . . . . . . . . 9
10 7 , 9 eqeq12d 2479 . . . . . . . 8
11 oveq2 6304 . . . . . . . . . . 11
12 00id 9776 . . . . . . . . . . 11
13 11 , 12 syl6eq 2514 . . . . . . . . . 10
14 13 fveq2d 5875 . . . . . . . . 9
15 fveq2 5871 . . . . . . . . . 10
16 15 oveq2d 6312 . . . . . . . . 9
17 14 , 16 eqeq12d 2479 . . . . . . . 8
18 fsumrelem.4 . . . . . . . 8
19 10 , 17 , 18 vtocl2ga 3175 . . . . . . 7
20 1 , 1 , 19 mp2an 672 . . . . . 6
21 5 , 20 eqtr2i 2487 . . . . 5
22 4 , 4 , 1 addcani 9794 . . . . 5
23 21 , 22 mpbi 208 . . . 4
24 sumeq1 13511 . . . . . 6
25 sum0 13543 . . . . . 6
26 24 , 25 syl6eq 2514 . . . . 5
27 26 fveq2d 5875 . . . 4
28 sumeq1 13511 . . . . 5
29 sum0 13543 . . . . 5
30 28 , 29 syl6eq 2514 . . . 4
31 23 , 27 , 30 3eqtr4a 2524 . . 3
32 31 a1i 11 . 2
33 addcl 9595 . . . . . . . . 9
34 33 adantl 466 . . . . . . . 8
35 fsumre.2 . . . . . . . . . . . 12
36 eqid 2457 . . . . . . . . . . . 12
37 35 , 36 fmptd 6055 . . . . . . . . . . 11
38 37 adantr 465 . . . . . . . . . 10
39 simprr 757 . . . . . . . . . . 11
40 f1of 5821 . . . . . . . . . . 11
41 39 , 40 syl 16 . . . . . . . . . 10
42 fco 5746 . . . . . . . . . 10
43 38 , 41 , 42 syl2anc 661 . . . . . . . . 9
44 43 ffvelrnda 6031 . . . . . . . 8
45 simprl 756 . . . . . . . . 9
46 nnuz 11145 . . . . . . . . 9
47 45 , 46 syl6eleq 2555 . . . . . . . 8
48 18 adantl 466 . . . . . . . 8
49 41 ffvelrnda 6031 . . . . . . . . . 10
50 simpr 461 . . . . . . . . . . . . . . 15
51 36 fvmpt2 5963 . . . . . . . . . . . . . . 15
52 50 , 35 , 51 syl2anc 661 . . . . . . . . . . . . . 14
53 52 fveq2d 5875 . . . . . . . . . . . . 13
54 fvex 5881 . . . . . . . . . . . . . 14
55 eqid 2457 . . . . . . . . . . . . . . 15
56 55 fvmpt2 5963 . . . . . . . . . . . . . 14
57 50 , 54 , 56 sylancl 662 . . . . . . . . . . . . 13
58 53 , 57 eqtr4d 2501 . . . . . . . . . . . 12
59 58 ralrimiva 2871 . . . . . . . . . . 11
60 59 ad2antrr 725 . . . . . . . . . 10
61 nfcv 2619 . . . . . . . . . . . . 13
62 nffvmpt1 5879 . . . . . . . . . . . . 13
63 61 , 62 nffv 5878 . . . . . . . . . . . 12
64 nffvmpt1 5879 . . . . . . . . . . . 12
65 63 , 64 nfeq 2630 . . . . . . . . . . 11
66 fveq2 5871 . . . . . . . . . . . . 13
67 66 fveq2d 5875 . . . . . . . . . . . 12
68 fveq2 5871 . . . . . . . . . . . 12
69 67 , 68 eqeq12d 2479 . . . . . . . . . . 11
70 65 , 69 rspc 3204 . . . . . . . . . 10
71 49 , 60 , 70 sylc 60 . . . . . . . . 9
72 fvco3 5950 . . . . . . . . . . 11
73 41 , 72 sylan 471 . . . . . . . . . 10
74 73 fveq2d 5875 . . . . . . . . 9
75 fvco3 5950 . . . . . . . . . 10
76 41 , 75 sylan 471 . . . . . . . . 9
77 71 , 74 , 76 3eqtr4d 2508 . . . . . . . 8
78 34 , 44 , 47 , 48 , 77 seqhomo 12154 . . . . . . 7
79 fveq2 5871 . . . . . . . . 9
80 38 ffvelrnda 6031 . . . . . . . . 9
81 79 , 45 , 39 , 80 , 73 fsum 13542 . . . . . . . 8
82 81 fveq2d 5875 . . . . . . 7
83 fveq2 5871 . . . . . . . 8
84 2 ffvelrni 6030 . . . . . . . . . . . 12
85 35 , 84 syl 16 . . . . . . . . . . 11
86 85 , 55 fmptd 6055 . . . . . . . . . 10
87 86 adantr 465 . . . . . . . . 9
88 87 ffvelrnda 6031 . . . . . . . 8
89 83 , 45 , 39 , 88 , 76 fsum 13542 . . . . . . 7
90 78 , 82 , 89 3eqtr4d 2508 . . . . . 6
91 sumfc 13531 . . . . . . 7
92 91 fveq2i 5874 . . . . . 6
93 sumfc 13531 . . . . . 6
94 90 , 92 , 93 3eqtr3g 2521 . . . . 5
95 94 expr 615 . . . 4
96 95 exlimdv 1724 . . 3
97 96 expimpd 603 . 2
98 fsumre.1 . . 3
99 fz1f1o 13532 . . 3
100 98 , 99 syl 16 . 2
101 32 , 97 , 100 mpjaod 381 1
