Metamath Proof Explorer

Theorem ballotlemfg

Description: Express the value of ( FC ) in terms of .^ . (Contributed by Thierry Arnoux, 21-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
ballotth.r ⊢R=c∈O∖E⟼S⁡cc
ballotlemg ⊢×˙=u∈Fin,v∈Fin⟼v∩u−v∖u
Assertion ballotlemfg ⊢C∈O∖E∧J∈0…M+N→F⁡C⁡J=C×˙1…J

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 ballotth.r ⊢R=c∈O∖E⟼S⁡cc
11 ballotlemg ⊢×˙=u∈Fin,v∈Fin⟼v∩u−v∖u
12 eldifi ⊢C∈O∖E→C∈O
13 12 adantr ⊢C∈O∖E∧J∈0…M+N→C∈O
14 elfzelz ⊢J∈0…M+N→J∈ℤ
15 14 adantl ⊢C∈O∖E∧J∈0…M+N→J∈ℤ
16 1 2 3 4 5 13 15 ballotlemfval ⊢C∈O∖E∧J∈0…M+N→F⁡C⁡J=1…J∩C−1…J∖C
17 fzfi ⊢1…M+N∈Fin
18 1 2 3 ballotlemelo ⊢C∈O↔C⊆1…M+N∧C=M
19 18 simplbi ⊢C∈O→C⊆1…M+N
20 ssfi ⊢1…M+N∈Fin∧C⊆1…M+N→C∈Fin
21 17 19 20 sylancr ⊢C∈O→C∈Fin
22 13 21 syl ⊢C∈O∖E∧J∈0…M+N→C∈Fin
23 fzfid ⊢C∈O∖E∧J∈0…M+N→1…J∈Fin
24 1 2 3 4 5 6 7 8 9 10 11 ballotlemgval ⊢C∈Fin∧1…J∈Fin→C×˙1…J=1…J∩C−1…J∖C
25 22 23 24 syl2anc ⊢C∈O∖E∧J∈0…M+N→C×˙1…J=1…J∩C−1…J∖C
26 16 25 eqtr4d ⊢C∈O∖E∧J∈0…M+N→F⁡C⁡J=C×˙1…J