Metamath Proof Explorer

Theorem ballotlem4

Description: If the first pick is a vote for B, A is not ahead throughout the count. (Contributed by Thierry Arnoux, 25-Nov-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
Assertion ballotlem4 ⊢ C ∈ O → ¬ 1 ∈ C → ¬ C ∈ E

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 nnaddcl ⊢ M ∈ ℕ ∧ N ∈ ℕ → M + N ∈ ℕ
8 1 2 7 mp2an ⊢ M + N ∈ ℕ
9 elnnuz ⊢ M + N ∈ ℕ ↔ M + N ∈ ℤ ≥ 1
10 8 9 mpbi ⊢ M + N ∈ ℤ ≥ 1
11 eluzfz1 ⊢ M + N ∈ ℤ ≥ 1 → 1 ∈ 1 … M + N
12 10 11 ax-mp ⊢ 1 ∈ 1 … M + N
13 0le1 ⊢ 0 ≤ 1
14 0re ⊢ 0 ∈ ℝ
15 1re ⊢ 1 ∈ ℝ
16 14 15 lenlti ⊢ 0 ≤ 1 ↔ ¬ 1 < 0
17 13 16 mpbi ⊢ ¬ 1 < 0
18 ltsub13 ⊢ 0 ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ → 0 < 0 − 1 ↔ 1 < 0 − 0
19 14 14 15 18 mp3an ⊢ 0 < 0 − 1 ↔ 1 < 0 − 0
20 0m0e0 ⊢ 0 − 0 = 0
21 20 breq2i ⊢ 1 < 0 − 0 ↔ 1 < 0
22 19 21 bitri ⊢ 0 < 0 − 1 ↔ 1 < 0
23 17 22 mtbir ⊢ ¬ 0 < 0 − 1
24 1m1e0 ⊢ 1 − 1 = 0
25 24 fveq2i ⊢ F ⁡ C ⁡ 1 − 1 = F ⁡ C ⁡ 0
26 1 2 3 4 5 ballotlemfval0 ⊢ C ∈ O → F ⁡ C ⁡ 0 = 0
27 25 26 eqtrid ⊢ C ∈ O → F ⁡ C ⁡ 1 − 1 = 0
28 27 oveq1d ⊢ C ∈ O → F ⁡ C ⁡ 1 − 1 − 1 = 0 − 1
29 28 breq2d ⊢ C ∈ O → 0 < F ⁡ C ⁡ 1 − 1 − 1 ↔ 0 < 0 − 1
30 23 29 mtbiri ⊢ C ∈ O → ¬ 0 < F ⁡ C ⁡ 1 − 1 − 1
31 30 adantr ⊢ C ∈ O ∧ ¬ 1 ∈ C → ¬ 0 < F ⁡ C ⁡ 1 − 1 − 1
32 simpl ⊢ C ∈ O ∧ 1 ∈ 1 … M + N → C ∈ O
33 1nn ⊢ 1 ∈ ℕ
34 33 a1i ⊢ C ∈ O ∧ 1 ∈ 1 … M + N → 1 ∈ ℕ
35 1 2 3 4 5 32 34 ballotlemfp1 ⊢ C ∈ O ∧ 1 ∈ 1 … M + N → ¬ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 − 1 ∧ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 + 1
36 35 simpld ⊢ C ∈ O ∧ 1 ∈ 1 … M + N → ¬ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 − 1
37 12 36 mpan2 ⊢ C ∈ O → ¬ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 − 1
38 37 imp ⊢ C ∈ O ∧ ¬ 1 ∈ C → F ⁡ C ⁡ 1 = F ⁡ C ⁡ 1 − 1 − 1
39 38 breq2d ⊢ C ∈ O ∧ ¬ 1 ∈ C → 0 < F ⁡ C ⁡ 1 ↔ 0 < F ⁡ C ⁡ 1 − 1 − 1
40 31 39 mtbird ⊢ C ∈ O ∧ ¬ 1 ∈ C → ¬ 0 < F ⁡ C ⁡ 1
41 fveq2 ⊢ i = 1 → F ⁡ C ⁡ i = F ⁡ C ⁡ 1
42 41 breq2d ⊢ i = 1 → 0 < F ⁡ C ⁡ i ↔ 0 < F ⁡ C ⁡ 1
43 42 notbid ⊢ i = 1 → ¬ 0 < F ⁡ C ⁡ i ↔ ¬ 0 < F ⁡ C ⁡ 1
44 43 rspcev ⊢ 1 ∈ 1 … M + N ∧ ¬ 0 < F ⁡ C ⁡ 1 → ∃ i ∈ 1 … M + N ¬ 0 < F ⁡ C ⁡ i
45 12 40 44 sylancr ⊢ C ∈ O ∧ ¬ 1 ∈ C → ∃ i ∈ 1 … M + N ¬ 0 < F ⁡ C ⁡ i
46 rexnal ⊢ ∃ i ∈ 1 … M + N ¬ 0 < F ⁡ C ⁡ i ↔ ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
47 45 46 sylib ⊢ C ∈ O ∧ ¬ 1 ∈ C → ¬ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
48 1 2 3 4 5 6 ballotleme ⊢ C ∈ E ↔ C ∈ O ∧ ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
49 48 simprbi ⊢ C ∈ E → ∀ i ∈ 1 … M + N 0 < F ⁡ C ⁡ i
50 47 49 nsyl ⊢ C ∈ O ∧ ¬ 1 ∈ C → ¬ C ∈ E
51 50 ex ⊢ C ∈ O → ¬ 1 ∈ C → ¬ C ∈ E