Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsumval2 Structured version   Unicode version

Theorem gsumval2 16466
 Description: Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014.)
Hypotheses
Ref Expression
gsumval2.b
gsumval2.p
gsumval2.g
gsumval2.n
gsumval2.f
Assertion
Ref Expression
gsumval2 g

Proof of Theorem gsumval2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumval2.b . . . 4
2 eqid 2428 . . . 4
3 gsumval2.p . . . 4
4 eqid 2428 . . . 4
5 gsumval2.g . . . . 5
65adantr 466 . . . 4
7 ovex 6277 . . . . 5
87a1i 11 . . . 4
9 gsumval2.f . . . . . . 7
10 ffn 5689 . . . . . . 7
119, 10syl 17 . . . . . 6
1211adantr 466 . . . . 5
13 simpr 462 . . . . 5
14 df-f 5548 . . . . 5
1512, 13, 14sylanbrc 668 . . . 4
161, 2, 3, 4, 6, 8, 15gsumval1 16463 . . 3 g
17 simpl 458 . . . . . . . . 9
1817ralimi 2758 . . . . . . . 8
1918a1i 11 . . . . . . 7
2019ss2rabi 3486 . . . . . 6
21 fvex 5835 . . . . . . . 8
2221snid 3969 . . . . . . 7
23 fdm 5693 . . . . . . . . . . . . . 14
249, 23syl 17 . . . . . . . . . . . . 13
25 gsumval2.n . . . . . . . . . . . . . 14
26 eluzfz1 11757 . . . . . . . . . . . . . 14
27 ne0i 3710 . . . . . . . . . . . . . 14
2825, 26, 273syl 18 . . . . . . . . . . . . 13
2924, 28eqnetrd 2668 . . . . . . . . . . . 12
30 dm0rn0 5013 . . . . . . . . . . . . 13
3130necon3bii 2653 . . . . . . . . . . . 12
3229, 31sylib 199 . . . . . . . . . . 11
3332adantr 466 . . . . . . . . . 10
34 ssn0 3740 . . . . . . . . . 10
3513, 33, 34syl2anc 665 . . . . . . . . 9
3635neneqd 2606 . . . . . . . 8
371, 2, 3, 4mgmidsssn0 16455 . . . . . . . . . . 11
385, 37syl 17 . . . . . . . . . 10
39 sssn 4101 . . . . . . . . . 10
4038, 39sylib 199 . . . . . . . . 9
4140orcanai 921 . . . . . . . 8
4236, 41syldan 472 . . . . . . 7
4322, 42syl5eleqr 2513 . . . . . 6
4420, 43sseldi 3405 . . . . 5
45 oveq1 6256 . . . . . . . . 9
4645eqeq1d 2430 . . . . . . . 8
4746ralbidv 2804 . . . . . . 7
4847elrab 3171 . . . . . 6
49 oveq2 6257 . . . . . . . 8
50 id 22 . . . . . . . 8
5149, 50eqeq12d 2443 . . . . . . 7
5251rspcva 3123 . . . . . 6
5348, 52sylbi 198 . . . . 5
5444, 53syl 17 . . . 4
5525adantr 466 . . . 4
5638ad2antrr 730 . . . . . 6
5715ffvelrnda 5981 . . . . . 6
5856, 57sseldd 3408 . . . . 5
59 elsni 3966 . . . . 5
6058, 59syl 17 . . . 4
6154, 55, 60seqid3 12207 . . 3
6216, 61eqtr4d 2465 . 2 g