Theorem ballotlem5

Description: If A is not ahead throughout, there is a k where votes are tied. (Contributed by Thierry Arnoux, 1-Dec-2016)

	Ref	Expression
Hypotheses	ballotth.m	⊢ 𝑀 ∈ ℕ
	ballotth.n	⊢ 𝑁 ∈ ℕ
	ballotth.o	⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
	ballotth.p	⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
	ballotth.f	⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
	ballotth.e	⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
	ballotth.mgtn	⊢ 𝑁 < 𝑀
Assertion	ballotlem5	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	⊢ 𝑀 ∈ ℕ
2		ballotth.n	⊢ 𝑁 ∈ ℕ
3		ballotth.o	⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4		ballotth.p	⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5		ballotth.f	⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6		ballotth.e	⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
7		ballotth.mgtn	⊢ 𝑁 < 𝑀
8		eldifi	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 𝐶 ∈ 𝑂 )
9	1	a1i	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 𝑀 ∈ ℕ )
10	2	a1i	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 𝑁 ∈ ℕ )
11	9 10	nnaddcld	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
12	1 2 3 4 5 6	ballotlemodife	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ↔ ( 𝐶 ∈ 𝑂 ∧ ∃ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ) )
13	12	simprbi	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ∃ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 )
14	2	nnrei	⊢ 𝑁 ∈ ℝ
15	1	nnrei	⊢ 𝑀 ∈ ℝ
16	14 15	posdifi	⊢ ( 𝑁 < 𝑀 ↔ 0 < ( 𝑀 − 𝑁 ) )
17	7 16	mpbi	⊢ 0 < ( 𝑀 − 𝑁 )
18	1 2 3 4 5	ballotlemfmpn	⊢ ( 𝐶 ∈ 𝑂 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑀 + 𝑁 ) ) = ( 𝑀 − 𝑁 ) )
19	8 18	syl	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑀 + 𝑁 ) ) = ( 𝑀 − 𝑁 ) )
20	17 19	breqtrrid	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝑀 + 𝑁 ) ) )
21	1 2 3 4 5 8 11 13 20	ballotlemfc0	⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ∃ 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )