Metamath Proof Explorer


Theorem ballotlemic

Description: If the first vote is for B, the vote on the first tie is for A. (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 𝑁 < 𝑀
ballotth.i 𝐼 = ( 𝑐 ∈ ( 𝑂𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
Assertion ballotlemic ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 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 ballotth.mgtn 𝑁 < 𝑀
8 ballotth.i 𝐼 = ( 𝑐 ∈ ( 𝑂𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
9 eldifi ( 𝐶 ∈ ( 𝑂𝐸 ) → 𝐶𝑂 )
10 9 ad2antrr ( ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → 𝐶𝑂 )
11 1 2 3 4 5 6 7 8 ballotlemiex ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( 𝐼𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹𝐶 ) ‘ ( 𝐼𝐶 ) ) = 0 ) )
12 11 simpld ( 𝐶 ∈ ( 𝑂𝐸 ) → ( 𝐼𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
13 elfznn ( ( 𝐼𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝐼𝐶 ) ∈ ℕ )
14 12 13 syl ( 𝐶 ∈ ( 𝑂𝐸 ) → ( 𝐼𝐶 ) ∈ ℕ )
15 14 adantr ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( 𝐼𝐶 ) ∈ ℕ )
16 1 2 3 4 5 6 7 8 ballotlemi1 ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( 𝐼𝐶 ) ≠ 1 )
17 eluz2b3 ( ( 𝐼𝐶 ) ∈ ( ℤ ‘ 2 ) ↔ ( ( 𝐼𝐶 ) ∈ ℕ ∧ ( 𝐼𝐶 ) ≠ 1 ) )
18 15 16 17 sylanbrc ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( 𝐼𝐶 ) ∈ ( ℤ ‘ 2 ) )
19 uz2m1nn ( ( 𝐼𝐶 ) ∈ ( ℤ ‘ 2 ) → ( ( 𝐼𝐶 ) − 1 ) ∈ ℕ )
20 18 19 syl ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( ( 𝐼𝐶 ) − 1 ) ∈ ℕ )
21 20 adantr ( ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → ( ( 𝐼𝐶 ) − 1 ) ∈ ℕ )
22 elnnuz ( ( ( 𝐼𝐶 ) − 1 ) ∈ ℕ ↔ ( ( 𝐼𝐶 ) − 1 ) ∈ ( ℤ ‘ 1 ) )
23 22 biimpi ( ( ( 𝐼𝐶 ) − 1 ) ∈ ℕ → ( ( 𝐼𝐶 ) − 1 ) ∈ ( ℤ ‘ 1 ) )
24 eluzfz1 ( ( ( 𝐼𝐶 ) − 1 ) ∈ ( ℤ ‘ 1 ) → 1 ∈ ( 1 ... ( ( 𝐼𝐶 ) − 1 ) ) )
25 20 23 24 3syl ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → 1 ∈ ( 1 ... ( ( 𝐼𝐶 ) − 1 ) ) )
26 25 adantr ( ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → 1 ∈ ( 1 ... ( ( 𝐼𝐶 ) − 1 ) ) )
27 1nn 1 ∈ ℕ
28 27 a1i ( 𝐶 ∈ ( 𝑂𝐸 ) → 1 ∈ ℕ )
29 1 2 3 4 5 9 28 ballotlemfp1 ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( ¬ 1 ∈ 𝐶 → ( ( 𝐹𝐶 ) ‘ 1 ) = ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) ) ∧ ( 1 ∈ 𝐶 → ( ( 𝐹𝐶 ) ‘ 1 ) = ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) ) ) )
30 29 simpld ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ¬ 1 ∈ 𝐶 → ( ( 𝐹𝐶 ) ‘ 1 ) = ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) ) )
31 30 imp ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( ( 𝐹𝐶 ) ‘ 1 ) = ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) )
32 1m1e0 ( 1 − 1 ) = 0
33 32 fveq2i ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) = ( ( 𝐹𝐶 ) ‘ 0 )
34 33 oveq1i ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) = ( ( ( 𝐹𝐶 ) ‘ 0 ) − 1 )
35 34 a1i ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) = ( ( ( 𝐹𝐶 ) ‘ 0 ) − 1 ) )
36 1 2 3 4 5 ballotlemfval0 ( 𝐶𝑂 → ( ( 𝐹𝐶 ) ‘ 0 ) = 0 )
37 9 36 syl ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( 𝐹𝐶 ) ‘ 0 ) = 0 )
38 37 adantr ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( ( 𝐹𝐶 ) ‘ 0 ) = 0 )
39 38 oveq1d ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( ( ( 𝐹𝐶 ) ‘ 0 ) − 1 ) = ( 0 − 1 ) )
40 31 35 39 3eqtrrd ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( 0 − 1 ) = ( ( 𝐹𝐶 ) ‘ 1 ) )
41 0le1 0 ≤ 1
42 0re 0 ∈ ℝ
43 1re 1 ∈ ℝ
44 suble0 ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 0 − 1 ) ≤ 0 ↔ 0 ≤ 1 ) )
45 42 43 44 mp2an ( ( 0 − 1 ) ≤ 0 ↔ 0 ≤ 1 )
46 41 45 mpbir ( 0 − 1 ) ≤ 0
47 40 46 eqbrtrrdi ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( ( 𝐹𝐶 ) ‘ 1 ) ≤ 0 )
48 47 adantr ( ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → ( ( 𝐹𝐶 ) ‘ 1 ) ≤ 0 )
49 fveq2 ( 𝑖 = 1 → ( ( 𝐹𝐶 ) ‘ 𝑖 ) = ( ( 𝐹𝐶 ) ‘ 1 ) )
50 49 breq1d ( 𝑖 = 1 → ( ( ( 𝐹𝐶 ) ‘ 𝑖 ) ≤ 0 ↔ ( ( 𝐹𝐶 ) ‘ 1 ) ≤ 0 ) )
51 50 rspcev ( ( 1 ∈ ( 1 ... ( ( 𝐼𝐶 ) − 1 ) ) ∧ ( ( 𝐹𝐶 ) ‘ 1 ) ≤ 0 ) → ∃ 𝑖 ∈ ( 1 ... ( ( 𝐼𝐶 ) − 1 ) ) ( ( 𝐹𝐶 ) ‘ 𝑖 ) ≤ 0 )
52 26 48 51 syl2anc ( ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → ∃ 𝑖 ∈ ( 1 ... ( ( 𝐼𝐶 ) − 1 ) ) ( ( 𝐹𝐶 ) ‘ 𝑖 ) ≤ 0 )
53 0lt1 0 < 1
54 1p0e1 ( 1 + 0 ) = 1
55 1 2 3 4 5 9 14 ballotlemfp1 ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( ¬ ( 𝐼𝐶 ) ∈ 𝐶 → ( ( 𝐹𝐶 ) ‘ ( 𝐼𝐶 ) ) = ( ( ( 𝐹𝐶 ) ‘ ( ( 𝐼𝐶 ) − 1 ) ) − 1 ) ) ∧ ( ( 𝐼𝐶 ) ∈ 𝐶 → ( ( 𝐹𝐶 ) ‘ ( 𝐼𝐶 ) ) = ( ( ( 𝐹𝐶 ) ‘ ( ( 𝐼𝐶 ) − 1 ) ) + 1 ) ) ) )
56 55 simpld ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ¬ ( 𝐼𝐶 ) ∈ 𝐶 → ( ( 𝐹𝐶 ) ‘ ( 𝐼𝐶 ) ) = ( ( ( 𝐹𝐶 ) ‘ ( ( 𝐼𝐶 ) − 1 ) ) − 1 ) ) )
57 56 imp ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → ( ( 𝐹𝐶 ) ‘ ( 𝐼𝐶 ) ) = ( ( ( 𝐹𝐶 ) ‘ ( ( 𝐼𝐶 ) − 1 ) ) − 1 ) )
58 11 simprd ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( 𝐹𝐶 ) ‘ ( 𝐼𝐶 ) ) = 0 )
59 58 adantr ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → ( ( 𝐹𝐶 ) ‘ ( 𝐼𝐶 ) ) = 0 )
60 57 59 eqtr3d ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → ( ( ( 𝐹𝐶 ) ‘ ( ( 𝐼𝐶 ) − 1 ) ) − 1 ) = 0 )
61 9 adantr ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → 𝐶𝑂 )
62 14 nnzd ( 𝐶 ∈ ( 𝑂𝐸 ) → ( 𝐼𝐶 ) ∈ ℤ )
63 62 adantr ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → ( 𝐼𝐶 ) ∈ ℤ )
64 1zzd ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → 1 ∈ ℤ )
65 63 64 zsubcld ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → ( ( 𝐼𝐶 ) − 1 ) ∈ ℤ )
66 1 2 3 4 5 61 65 ballotlemfelz ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → ( ( 𝐹𝐶 ) ‘ ( ( 𝐼𝐶 ) − 1 ) ) ∈ ℤ )
67 66 zcnd ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → ( ( 𝐹𝐶 ) ‘ ( ( 𝐼𝐶 ) − 1 ) ) ∈ ℂ )
68 1cnd ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → 1 ∈ ℂ )
69 0cnd ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → 0 ∈ ℂ )
70 67 68 69 subaddd ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → ( ( ( ( 𝐹𝐶 ) ‘ ( ( 𝐼𝐶 ) − 1 ) ) − 1 ) = 0 ↔ ( 1 + 0 ) = ( ( 𝐹𝐶 ) ‘ ( ( 𝐼𝐶 ) − 1 ) ) ) )
71 60 70 mpbid ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → ( 1 + 0 ) = ( ( 𝐹𝐶 ) ‘ ( ( 𝐼𝐶 ) − 1 ) ) )
72 54 71 eqtr3id ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → 1 = ( ( 𝐹𝐶 ) ‘ ( ( 𝐼𝐶 ) − 1 ) ) )
73 53 72 breqtrid ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → 0 < ( ( 𝐹𝐶 ) ‘ ( ( 𝐼𝐶 ) − 1 ) ) )
74 73 adantlr ( ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → 0 < ( ( 𝐹𝐶 ) ‘ ( ( 𝐼𝐶 ) − 1 ) ) )
75 1 2 3 4 5 10 21 52 74 ballotlemfc0 ( ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → ∃ 𝑘 ∈ ( 1 ... ( ( 𝐼𝐶 ) − 1 ) ) ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 )
76 1 2 3 4 5 6 7 8 ballotlemimin ( 𝐶 ∈ ( 𝑂𝐸 ) → ¬ ∃ 𝑘 ∈ ( 1 ... ( ( 𝐼𝐶 ) − 1 ) ) ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 )
77 76 ad2antrr ( ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) ∧ ¬ ( 𝐼𝐶 ) ∈ 𝐶 ) → ¬ ∃ 𝑘 ∈ ( 1 ... ( ( 𝐼𝐶 ) − 1 ) ) ( ( 𝐹𝐶 ) ‘ 𝑘 ) = 0 )
78 75 77 condan ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( 𝐼𝐶 ) ∈ 𝐶 )