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

Theorem ballotlemsv 24215
 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 24214 . . . 4
11 nfcv 2502 . . . . 5
12 nfcv 2502 . . . . 5
13 breq1 4128 . . . . . 6
14 oveq2 5989 . . . . . 6
15 id 19 . . . . . 6
1613, 14, 15ifbieq12d 3676 . . . . 5
1711, 12, 16cbvmpt 4212 . . . 4
1810, 17syl6eq 2414 . . 3
20 simpr 447 . . . . 5
2120breq1d 4135 . . . 4
2220oveq2d 5997 . . . 4
2321, 22, 20ifbieq12d 3676 . . 3