Metamath Proof Explorer

Theorem ballotlemsval

Description: Value of S . (Contributed by Thierry Arnoux, 12-Apr-2017)

Ref Expression
Hypotheses ballotth.m ⊢M∈ℕ
ballotth.n ⊢N∈ℕ
ballotth.o ⊢O=c∈𝒫1…M+N|c=M
ballotth.p ⊢P=x∈𝒫O⟼xO
ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
ballotth.mgtn ⊢N<M
ballotth.i ⊢I=c∈O∖E⟼supk∈1…M+N|F⁡c⁡k=0ℝ<
ballotth.s ⊢S=c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii
Assertion ballotlemsval ⊢C∈O∖E→S⁡C=i∈1…M+N⟼ifi≤I⁡CI⁡C+1-ii

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢M∈ℕ
2 ballotth.n ⊢N∈ℕ
3 ballotth.o ⊢O=c∈𝒫1…M+N|c=M
4 ballotth.p ⊢P=x∈𝒫O⟼xO
5 ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
6 ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
7 ballotth.mgtn ⊢N<M
8 ballotth.i ⊢I=c∈O∖E⟼supk∈1…M+N|F⁡c⁡k=0ℝ<
9 ballotth.s ⊢S=c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii
10 simpl ⊢d=C∧i∈1…M+N→d=C
11 10 fveq2d ⊢d=C∧i∈1…M+N→I⁡d=I⁡C
12 11 breq2d ⊢d=C∧i∈1…M+N→i≤I⁡d↔i≤I⁡C
13 11 oveq1d ⊢d=C∧i∈1…M+N→I⁡d+1=I⁡C+1
14 13 oveq1d ⊢d=C∧i∈1…M+N→I⁡d+1-i=I⁡C+1-i
15 12 14 ifbieq1d ⊢d=C∧i∈1…M+N→ifi≤I⁡dI⁡d+1-ii=ifi≤I⁡CI⁡C+1-ii
16 15 mpteq2dva ⊢d=C→i∈1…M+N⟼ifi≤I⁡dI⁡d+1-ii=i∈1…M+N⟼ifi≤I⁡CI⁡C+1-ii
17 simpl ⊢c=d∧i∈1…M+N→c=d
18 17 fveq2d ⊢c=d∧i∈1…M+N→I⁡c=I⁡d
19 18 breq2d ⊢c=d∧i∈1…M+N→i≤I⁡c↔i≤I⁡d
20 18 oveq1d ⊢c=d∧i∈1…M+N→I⁡c+1=I⁡d+1
21 20 oveq1d ⊢c=d∧i∈1…M+N→I⁡c+1-i=I⁡d+1-i
22 19 21 ifbieq1d ⊢c=d∧i∈1…M+N→ifi≤I⁡cI⁡c+1-ii=ifi≤I⁡dI⁡d+1-ii
23 22 mpteq2dva ⊢c=d→i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii=i∈1…M+N⟼ifi≤I⁡dI⁡d+1-ii
24 23 cbvmptv ⊢c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii=d∈O∖E⟼i∈1…M+N⟼ifi≤I⁡dI⁡d+1-ii
25 9 24 eqtri ⊢S=d∈O∖E⟼i∈1…M+N⟼ifi≤I⁡dI⁡d+1-ii
26 ovex ⊢1…M+N∈V
27 26 mptex ⊢i∈1…M+N⟼ifi≤I⁡CI⁡C+1-ii∈V
28 16 25 27 fvmpt ⊢C∈O∖E→S⁡C=i∈1…M+N⟼ifi≤I⁡CI⁡C+1-ii