Metamath Proof Explorer

Theorem ballotlem1c

Description: If the first vote is for A, the vote on the first tie is for B. (Contributed by Thierry Arnoux, 4-Apr-2017)

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 ballotlem1c ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 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 ballotlemii ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 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 fveq2 ⊢ ( 𝑖 = 1 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) )
23 22 breq2d ⊢ ( 𝑖 = 1 → ( 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ↔ 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) ) )
24 elnnuz ⊢ ( ( ( 𝐼 ‘ 𝐶 ) − 1 ) ∈ ℕ ↔ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
25 24 biimpi ⊢ ( ( ( 𝐼 ‘ 𝐶 ) − 1 ) ∈ ℕ → ( ( 𝐼 ‘ 𝐶 ) − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
26 eluzfz1 ⊢ ( ( ( 𝐼 ‘ 𝐶 ) − 1 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) )
27 20 25 26 3syl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → 1 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) )
28 27 adantr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → 1 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) )
29 0le1 ⊢ 0 ≤ 1
30 1e0p1 ⊢ 1 = ( 0 + 1 )
31 29 30 breqtri ⊢ 0 ≤ ( 0 + 1 )
32 1nn ⊢ 1 ∈ ℕ
33 32 a1i ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 1 ∈ ℕ )
34 1 2 3 4 5 9 33 ballotlemfp1 ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( ¬ 1 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) ) ∧ ( 1 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) ) ) )
35 34 simprd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 1 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) ) )
36 35 imp ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) )
37 1m1e0 ⊢ ( 1 − 1 ) = 0
38 37 fveq2i ⊢ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 0 )
39 38 oveq1i ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) + 1 )
40 39 a1i ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) + 1 ) )
41 1 2 3 4 5 ballotlemfval0 ⊢ ( 𝐶 ∈ 𝑂 → ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) = 0 )
42 9 41 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) = 0 )
43 42 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) = 0 )
44 43 oveq1d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) + 1 ) = ( 0 + 1 ) )
45 36 40 44 3eqtrrd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ( 0 + 1 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) )
46 31 45 breqtrid ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) )
47 46 adantr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) )
48 23 28 47 rspcedvdw ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → ∃ 𝑖 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) 0 ≤ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) )
49 df-neg ⊢ - 1 = ( 0 − 1 )
50 1 2 3 4 5 9 14 ballotlemfp1 ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( ¬ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) − 1 ) ) ∧ ( ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) + 1 ) ) ) )
51 50 simprd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) + 1 ) ) )
52 51 imp ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) + 1 ) )
53 11 simprd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 )
54 53 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 )
55 52 54 eqtr3d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) + 1 ) = 0 )
56 0cnd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → 0 ∈ ℂ )
57 1cnd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → 1 ∈ ℂ )
58 9 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → 𝐶 ∈ 𝑂 )
59 14 nnzd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
60 59 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
61 1zzd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → 1 ∈ ℤ )
62 60 61 zsubcld ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → ( ( 𝐼 ‘ 𝐶 ) − 1 ) ∈ ℤ )
63 1 2 3 4 5 58 62 ballotlemfelz ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ∈ ℤ )
64 63 zcnd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ∈ ℂ )
65 56 57 64 subadd2d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → ( ( 0 − 1 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ↔ ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) + 1 ) = 0 ) )
66 55 65 mpbird ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → ( 0 − 1 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) )
67 49 66 eqtrid ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → - 1 = ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) )
68 neg1lt0 ⊢ - 1 < 0
69 67 68 eqbrtrrdi ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) < 0 )
70 69 adantlr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) < 0 )
71 1 2 3 4 5 10 21 48 70 ballotlemfcc ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → ∃ 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
72 1 2 3 4 5 6 7 8 ballotlemimin ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ¬ ∃ 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
73 72 ad2antrr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) ∧ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 ) → ¬ ∃ 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
74 71 73 pm2.65da ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 1 ∈ 𝐶 ) → ¬ ( 𝐼 ‘ 𝐶 ) ∈ 𝐶 )