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 𝑀 ∈ ℕ
ballotth.n 𝑁 ∈ ℕ
ballotth.o 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
ballotth.p 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
ballotth.f 𝐹 = ( 𝑐𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
ballotth.e 𝐸 = { 𝑐𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹𝑐 ) ‘ 𝑖 ) }
Assertion ballotlem4 ( 𝐶𝑂 → ( ¬ 1 ∈ 𝐶 → ¬ 𝐶𝐸 ) )

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 nnaddcl ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
8 1 2 7 mp2an ( 𝑀 + 𝑁 ) ∈ ℕ
9 elnnuz ( ( 𝑀 + 𝑁 ) ∈ ℕ ↔ ( 𝑀 + 𝑁 ) ∈ ( ℤ ‘ 1 ) )
10 8 9 mpbi ( 𝑀 + 𝑁 ) ∈ ( ℤ ‘ 1 )
11 eluzfz1 ( ( 𝑀 + 𝑁 ) ∈ ( ℤ ‘ 1 ) → 1 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
12 10 11 ax-mp 1 ∈ ( 1 ... ( 𝑀 + 𝑁 ) )
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 ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) = ( ( 𝐹𝐶 ) ‘ 0 )
26 1 2 3 4 5 ballotlemfval0 ( 𝐶𝑂 → ( ( 𝐹𝐶 ) ‘ 0 ) = 0 )
27 25 26 syl5eq ( 𝐶𝑂 → ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) = 0 )
28 27 oveq1d ( 𝐶𝑂 → ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) = ( 0 − 1 ) )
29 28 breq2d ( 𝐶𝑂 → ( 0 < ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) ↔ 0 < ( 0 − 1 ) ) )
30 23 29 mtbiri ( 𝐶𝑂 → ¬ 0 < ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) )
31 30 adantr ( ( 𝐶𝑂 ∧ ¬ 1 ∈ 𝐶 ) → ¬ 0 < ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) )
32 simpl ( ( 𝐶𝑂 ∧ 1 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → 𝐶𝑂 )
33 1nn 1 ∈ ℕ
34 33 a1i ( ( 𝐶𝑂 ∧ 1 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → 1 ∈ ℕ )
35 1 2 3 4 5 32 34 ballotlemfp1 ( ( 𝐶𝑂 ∧ 1 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( ¬ 1 ∈ 𝐶 → ( ( 𝐹𝐶 ) ‘ 1 ) = ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) ) ∧ ( 1 ∈ 𝐶 → ( ( 𝐹𝐶 ) ‘ 1 ) = ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) ) ) )
36 35 simpld ( ( 𝐶𝑂 ∧ 1 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ¬ 1 ∈ 𝐶 → ( ( 𝐹𝐶 ) ‘ 1 ) = ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) ) )
37 12 36 mpan2 ( 𝐶𝑂 → ( ¬ 1 ∈ 𝐶 → ( ( 𝐹𝐶 ) ‘ 1 ) = ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) ) )
38 37 imp ( ( 𝐶𝑂 ∧ ¬ 1 ∈ 𝐶 ) → ( ( 𝐹𝐶 ) ‘ 1 ) = ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) )
39 38 breq2d ( ( 𝐶𝑂 ∧ ¬ 1 ∈ 𝐶 ) → ( 0 < ( ( 𝐹𝐶 ) ‘ 1 ) ↔ 0 < ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) ) )
40 31 39 mtbird ( ( 𝐶𝑂 ∧ ¬ 1 ∈ 𝐶 ) → ¬ 0 < ( ( 𝐹𝐶 ) ‘ 1 ) )
41 fveq2 ( 𝑖 = 1 → ( ( 𝐹𝐶 ) ‘ 𝑖 ) = ( ( 𝐹𝐶 ) ‘ 1 ) )
42 41 breq2d ( 𝑖 = 1 → ( 0 < ( ( 𝐹𝐶 ) ‘ 𝑖 ) ↔ 0 < ( ( 𝐹𝐶 ) ‘ 1 ) ) )
43 42 notbid ( 𝑖 = 1 → ( ¬ 0 < ( ( 𝐹𝐶 ) ‘ 𝑖 ) ↔ ¬ 0 < ( ( 𝐹𝐶 ) ‘ 1 ) ) )
44 43 rspcev ( ( 1 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ¬ 0 < ( ( 𝐹𝐶 ) ‘ 1 ) ) → ∃ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ¬ 0 < ( ( 𝐹𝐶 ) ‘ 𝑖 ) )
45 12 40 44 sylancr ( ( 𝐶𝑂 ∧ ¬ 1 ∈ 𝐶 ) → ∃ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ¬ 0 < ( ( 𝐹𝐶 ) ‘ 𝑖 ) )
46 rexnal ( ∃ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ¬ 0 < ( ( 𝐹𝐶 ) ‘ 𝑖 ) ↔ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹𝐶 ) ‘ 𝑖 ) )
47 45 46 sylib ( ( 𝐶𝑂 ∧ ¬ 1 ∈ 𝐶 ) → ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹𝐶 ) ‘ 𝑖 ) )
48 1 2 3 4 5 6 ballotleme ( 𝐶𝐸 ↔ ( 𝐶𝑂 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹𝐶 ) ‘ 𝑖 ) ) )
49 48 simprbi ( 𝐶𝐸 → ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹𝐶 ) ‘ 𝑖 ) )
50 47 49 nsyl ( ( 𝐶𝑂 ∧ ¬ 1 ∈ 𝐶 ) → ¬ 𝐶𝐸 )
51 50 ex ( 𝐶𝑂 → ( ¬ 1 ∈ 𝐶 → ¬ 𝐶𝐸 ) )