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

Theorem gsumval2 14788
 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 2438 . . . 4
3 gsumval2.p . . . 4
4 eqid 2438 . . . 4
5 gsumval2.g . . . . 5
65adantr 453 . . . 4
7 ovex 6109 . . . . 5
87a1i 11 . . . 4
9 gsumval2.f . . . . . . 7
10 ffn 5594 . . . . . . 7
119, 10syl 16 . . . . . 6
1211adantr 453 . . . . 5
13 simpr 449 . . . . 5
14 df-f 5461 . . . . 5
1512, 13, 14sylanbrc 647 . . . 4
161, 2, 3, 4, 6, 8, 15gsumval1 14784 . . 3 g
17 simpl 445 . . . . . . . . 9
1817ralimi 2783 . . . . . . . 8
1918a1i 11 . . . . . . 7
2019ss2rabi 3427 . . . . . 6
21 fvex 5745 . . . . . . . 8
2221snid 3843 . . . . . . 7
23 fdm 5598 . . . . . . . . . . . . . 14
249, 23syl 16 . . . . . . . . . . . . 13
25 gsumval2.n . . . . . . . . . . . . . 14
26 eluzfz1 11069 . . . . . . . . . . . . . 14
27 ne0i 3636 . . . . . . . . . . . . . 14
2825, 26, 273syl 19 . . . . . . . . . . . . 13
2924, 28eqnetrd 2621 . . . . . . . . . . . 12
30 dm0rn0 5089 . . . . . . . . . . . . 13
3130necon3bii 2635 . . . . . . . . . . . 12
3229, 31sylib 190 . . . . . . . . . . 11
3332adantr 453 . . . . . . . . . 10
34 ssn0 3662 . . . . . . . . . 10
3513, 33, 34syl2anc 644 . . . . . . . . 9
3635neneqd 2619 . . . . . . . 8
371, 2, 3, 4gsumvallem1 14776 . . . . . . . . . . 11
385, 37syl 16 . . . . . . . . . 10
39 sssn 3959 . . . . . . . . . 10
4038, 39sylib 190 . . . . . . . . 9
4140orcanai 881 . . . . . . . 8
4236, 41syldan 458 . . . . . . 7
4322, 42syl5eleqr 2525 . . . . . 6
4420, 43sseldi 3348 . . . . 5
45 oveq1 6091 . . . . . . . . 9
4645eqeq1d 2446 . . . . . . . 8
4746ralbidv 2727 . . . . . . 7
4847elrab 3094 . . . . . 6
49 oveq2 6092 . . . . . . . 8
50 id 21 . . . . . . . 8
5149, 50eqeq12d 2452 . . . . . . 7
5251rspcva 3052 . . . . . 6
5348, 52sylbi 189 . . . . 5
5444, 53syl 16 . . . 4
5525adantr 453 . . . 4
5638ad2antrr 708 . . . . . 6
5715ffvelrnda 5873 . . . . . 6
5856, 57sseldd 3351 . . . . 5
59 elsni 3840 . . . . 5
6058, 59syl 16 . . . 4
6154, 55, 60seqid3 11372 . . 3
6216, 61eqtr4d 2473 . 2 g