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 eqtrid ⊢ ( 𝐶 ∈ 𝑂 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 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 ∈ 𝐶 → ¬ 𝐶 ∈ 𝐸 ) )