Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ballotlemsv Structured version   Unicode version

Theorem ballotlemsv 24772
 Description: Value of evaluated at for a given counting . (Contributed by Thierry Arnoux, 12-Apr-2017.)
Hypotheses
Ref Expression
ballotth.m
ballotth.n
ballotth.o
ballotth.p
ballotth.f
ballotth.e
ballotth.mgtn
ballotth.i
ballotth.s
Assertion
Ref Expression
ballotlemsv
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,,,   ,,   ,,   ,   ,,   ,   ,,
Allowed substitution hints:   (,)   (,,,)   (,,,)   ()   ()   ()   (,,,)   ()   ()   ()

Proof of Theorem ballotlemsv
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ballotth.m . . . . 5
2 ballotth.n . . . . 5
3 ballotth.o . . . . 5
4 ballotth.p . . . . 5
5 ballotth.f . . . . 5
6 ballotth.e . . . . 5
7 ballotth.mgtn . . . . 5
8 ballotth.i . . . . 5
9 ballotth.s . . . . 5
101, 2, 3, 4, 5, 6, 7, 8, 9ballotlemsval 24771 . . . 4
11 breq1 4218 . . . . . 6
12 oveq2 6092 . . . . . 6
13 id 21 . . . . . 6
1411, 12, 13ifbieq12d 3763 . . . . 5
1514cbvmptv 4303 . . . 4
1610, 15syl6eq 2486 . . 3
18 simpr 449 . . . . 5
1918breq1d 4225 . . . 4
2018oveq2d 6100 . . . 4
2119, 20, 18ifbieq12d 3763 . . 3