Description: Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gsumval2.b | |
|
gsumval2.p | |
||
gsumval2.g | |
||
gsumval2.n | |
||
gsumval2.f | |
||
gsumval2a.o | |
||
gsumval2a.f | |
||
Assertion | gsumval2a | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gsumval2.b | |
|
2 | gsumval2.p | |
|
3 | gsumval2.g | |
|
4 | gsumval2.n | |
|
5 | gsumval2.f | |
|
6 | gsumval2a.o | |
|
7 | gsumval2a.f | |
|
8 | eqid | |
|
9 | eqidd | |
|
10 | ovexd | |
|
11 | 1 8 2 6 9 3 10 5 | gsumval | |
12 | 7 | iffalsed | |
13 | fzf | |
|
14 | ffn | |
|
15 | 13 14 | ax-mp | |
16 | eluzel2 | |
|
17 | 4 16 | syl | |
18 | eluzelz | |
|
19 | 4 18 | syl | |
20 | fnovrn | |
|
21 | 15 17 19 20 | mp3an2i | |
22 | 21 | iftrued | |
23 | 12 22 | eqtrd | |
24 | 11 23 | eqtrd | |
25 | fvex | |
|
26 | fzopth | |
|
27 | 4 26 | syl | |
28 | simpl | |
|
29 | 28 | seqeq1d | |
30 | simpr | |
|
31 | 29 30 | fveq12d | |
32 | 31 | eqcomd | |
33 | eqeq1 | |
|
34 | 32 33 | syl5ibrcom | |
35 | 27 34 | syl6bi | |
36 | 35 | impd | |
37 | 36 | rexlimdvw | |
38 | 37 | exlimdv | |
39 | 17 | adantr | |
40 | oveq2 | |
|
41 | 40 | eqcomd | |
42 | 41 | biantrurd | |
43 | fveq2 | |
|
44 | 43 | eqeq2d | |
45 | 42 44 | bitr3d | |
46 | 45 | rspcev | |
47 | 4 46 | sylan | |
48 | fveq2 | |
|
49 | oveq1 | |
|
50 | 49 | eqeq2d | |
51 | seqeq1 | |
|
52 | 51 | fveq1d | |
53 | 52 | eqeq2d | |
54 | 50 53 | anbi12d | |
55 | 48 54 | rexeqbidv | |
56 | 55 | spcegv | |
57 | 39 47 56 | sylc | |
58 | 57 | ex | |
59 | 38 58 | impbid | |
60 | 59 | adantr | |
61 | 60 | iota5 | |
62 | 25 61 | mpan2 | |
63 | 24 62 | eqtrd | |