Metamath Proof Explorer

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 ⊢ M ∈ ℕ
ballotth.n ⊢ N ∈ ℕ
ballotth.o ⊢ O = c ∈ 𝒫 1 … M + N | c = M
ballotth.p ⊢ P = x ∈ 𝒫 O ⟼ x O
ballotth.f ⊢ F = c ∈ O ⟼ i ∈ ℤ ⟼ 1 … i ∩ c − 1 … i ∖ c
ballotth.e ⊢ E = c ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ c ⁡ i
ballotth.mgtn ⊢ N < M
Assertion ballotlem5 ⊢ C ∈ O ∖ E → ∃ k ∈ 1 … M + N F ⁡ C ⁡ k = 0

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 ⟼ x O
5 ballotth.f ⊢ F = c ∈ O ⟼ i ∈ ℤ ⟼ 1 … i ∩ c − 1 … i ∖ c
6 ballotth.e ⊢ E = c ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ c ⁡ i
7 ballotth.mgtn ⊢ N < M
8 eldifi ⊢ C ∈ O ∖ E → C ∈ O
9 1 a1i ⊢ C ∈ O ∖ E → M ∈ ℕ
10 2 a1i ⊢ C ∈ O ∖ E → N ∈ ℕ
11 9 10 nnaddcld ⊢ C ∈ O ∖ E → M + N ∈ ℕ
12 1 2 3 4 5 6 ballotlemodife ⊢ C ∈ O ∖ E ↔ C ∈ O ∧ ∃ i ∈ 1 … M + N F ⁡ C ⁡ i ≤ 0
13 12 simprbi ⊢ C ∈ O ∖ E → ∃ i ∈ 1 … M + N F ⁡ C ⁡ i ≤ 0
14 2 nnrei ⊢ N ∈ ℝ
15 1 nnrei ⊢ M ∈ ℝ
16 14 15 posdifi ⊢ N < M ↔ 0 < M − N
17 7 16 mpbi ⊢ 0 < M − N
18 1 2 3 4 5 ballotlemfmpn ⊢ C ∈ O → F ⁡ C ⁡ M + N = M − N
19 8 18 syl ⊢ C ∈ O ∖ E → F ⁡ C ⁡ M + N = M − N
20 17 19 breqtrrid ⊢ C ∈ O ∖ E → 0 < F ⁡ C ⁡ M + N
21 1 2 3 4 5 8 11 13 20 ballotlemfc0 ⊢ C ∈ O ∖ E → ∃ k ∈ 1 … M + N F ⁡ C ⁡ k = 0