Metamath Proof Explorer

Theorem ballotlemrv2

Description: Value of R after the tie. (Contributed by Thierry Arnoux, 11-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
Assertion ballotlemrv2 ⊢C∈O∖E∧J∈1…M+N∧I⁡C<J→J∈R⁡C↔J∈C

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 1 2 3 4 5 6 7 8 9 10 ballotlemrv ⊢C∈O∖E∧J∈1…M+N→J∈R⁡C↔ifJ≤I⁡CI⁡C+1-JJ∈C
12 11 3adant3 ⊢C∈O∖E∧J∈1…M+N∧I⁡C<J→J∈R⁡C↔ifJ≤I⁡CI⁡C+1-JJ∈C
13 fzssuz ⊢1…M+N⊆ℤ≥1
14 uzssz ⊢ℤ≥1⊆ℤ
15 13 14 sstri ⊢1…M+N⊆ℤ
16 1 2 3 4 5 6 7 8 ballotlemiex ⊢C∈O∖E→I⁡C∈1…M+N∧F⁡C⁡I⁡C=0
17 16 simpld ⊢C∈O∖E→I⁡C∈1…M+N
18 15 17 sselid ⊢C∈O∖E→I⁡C∈ℤ
19 18 adantr ⊢C∈O∖E∧J∈1…M+N→I⁡C∈ℤ
20 19 zred ⊢C∈O∖E∧J∈1…M+N→I⁡C∈ℝ
21 simpr ⊢C∈O∖E∧J∈1…M+N→J∈1…M+N
22 15 21 sselid ⊢C∈O∖E∧J∈1…M+N→J∈ℤ
23 22 zred ⊢C∈O∖E∧J∈1…M+N→J∈ℝ
24 20 23 ltnled ⊢C∈O∖E∧J∈1…M+N→I⁡C<J↔¬J≤I⁡C
25 24 biimp3a ⊢C∈O∖E∧J∈1…M+N∧I⁡C<J→¬J≤I⁡C
26 25 iffalsed ⊢C∈O∖E∧J∈1…M+N∧I⁡C<J→ifJ≤I⁡CI⁡C+1-JJ=J
27 26 eleq1d ⊢C∈O∖E∧J∈1…M+N∧I⁡C<J→ifJ≤I⁡CI⁡C+1-JJ∈C↔J∈C
28 12 27 bitrd ⊢C∈O∖E∧J∈1…M+N∧I⁡C<J→J∈R⁡C↔J∈C