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

Theorem gsumval2 14559
 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 2358 . . . 4
3 gsumval2.p . . . 4
4 eqid 2358 . . . 4
5 gsumval2.g . . . . 5
65adantr 451 . . . 4
7 ovex 5970 . . . . 5
87a1i 10 . . . 4
9 gsumval2.f . . . . . . 7
10 ffn 5472 . . . . . . 7
119, 10syl 15 . . . . . 6
1211adantr 451 . . . . 5
13 simpr 447 . . . . 5
14 df-f 5341 . . . . 5
1512, 13, 14sylanbrc 645 . . . 4
161, 2, 3, 4, 6, 8, 15gsumval1 14555 . . 3 g
17 simpl 443 . . . . . . . . 9
1817ralimi 2694 . . . . . . . 8
1918a1i 10 . . . . . . 7
2019ss2rabi 3331 . . . . . 6
21 fvex 5622 . . . . . . . 8
2221snid 3743 . . . . . . 7
23 fdm 5476 . . . . . . . . . . . . . 14
249, 23syl 15 . . . . . . . . . . . . 13
25 gsumval2.n . . . . . . . . . . . . . 14
26 eluzfz1 10895 . . . . . . . . . . . . . 14
27 ne0i 3537 . . . . . . . . . . . . . 14
2825, 26, 273syl 18 . . . . . . . . . . . . 13
2924, 28eqnetrd 2539 . . . . . . . . . . . 12
30 dm0rn0 4977 . . . . . . . . . . . . 13
3130necon3bii 2553 . . . . . . . . . . . 12
3229, 31sylib 188 . . . . . . . . . . 11
3332adantr 451 . . . . . . . . . 10
34 ssn0 3563 . . . . . . . . . 10
3513, 33, 34syl2anc 642 . . . . . . . . 9
3635neneqd 2537 . . . . . . . 8
371, 2, 3, 4gsumvallem1 14547 . . . . . . . . . . 11
385, 37syl 15 . . . . . . . . . 10
39 sssn 3853 . . . . . . . . . 10
4038, 39sylib 188 . . . . . . . . 9
4140orcanai 879 . . . . . . . 8
4236, 41syldan 456 . . . . . . 7
4322, 42syl5eleqr 2445 . . . . . 6
4420, 43sseldi 3254 . . . . 5
45 oveq1 5952 . . . . . . . . 9
4645eqeq1d 2366 . . . . . . . 8
4746ralbidv 2639 . . . . . . 7
4847elrab 2999 . . . . . 6
49 oveq2 5953 . . . . . . . 8
50 id 19 . . . . . . . 8
5149, 50eqeq12d 2372 . . . . . . 7
5251rspcva 2958 . . . . . 6
5348, 52sylbi 187 . . . . 5
5444, 53syl 15 . . . 4
5525adantr 451 . . . 4
5638ad2antrr 706 . . . . . 6
57 ffvelrn 5746 . . . . . . 7
5815, 57sylan 457 . . . . . 6
5956, 58sseldd 3257 . . . . 5
60 elsni 3740 . . . . 5
6159, 60syl 15 . . . 4
6254, 55, 61seqid3 11182 . . 3
6316, 62eqtr4d 2393 . 2 g