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

Theorem ballotlemieq 24805
 Description: If two countings share the same first tie, they also have the same swap function. (Contributed by Thierry Arnoux, 18-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
ballotlemieq
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,,,   ,,   ,,   ,   ,,   ,   ,,   ,   ,,
Allowed substitution hints:   (,)   (,)   (,,,)   (,,)   ()   ()   ()   ()   ()   ()

Proof of Theorem ballotlemieq
StepHypRef Expression
1 simpl 445 . . . . . 6
21breq2d 4249 . . . . 5
31oveq1d 6125 . . . . . 6
43oveq1d 6125 . . . . 5
5 eqidd 2443 . . . . 5
62, 4, 5ifbieq12d 3785 . . . 4
76mpteq2dva 4320 . . 3
9 ballotth.m . . . 4
10 ballotth.n . . . 4
11 ballotth.o . . . 4
12 ballotth.p . . . 4
13 ballotth.f . . . 4
14 ballotth.e . . . 4
15 ballotth.mgtn . . . 4
16 ballotth.i . . . 4
17 ballotth.s . . . 4
189, 10, 11, 12, 13, 14, 15, 16, 17ballotlemsval 24797 . . 3