Metamath Proof Explorer


Theorem ballotlemii

Description: The first tie cannot be reached at the first pick. (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 ballotlemii ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 1 ∈ 𝐶 ) → ( 𝐼𝐶 ) ≠ 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 1e0p1 1 = ( 0 + 1 )
10 ax-1ne0 1 ≠ 0
11 9 10 eqnetrri ( 0 + 1 ) ≠ 0
12 11 neii ¬ ( 0 + 1 ) = 0
13 eldifi ( 𝐶 ∈ ( 𝑂𝐸 ) → 𝐶𝑂 )
14 1nn 1 ∈ ℕ
15 14 a1i ( 𝐶 ∈ ( 𝑂𝐸 ) → 1 ∈ ℕ )
16 1 2 3 4 5 13 15 ballotlemfp1 ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( ¬ 1 ∈ 𝐶 → ( ( 𝐹𝐶 ) ‘ 1 ) = ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) ) ∧ ( 1 ∈ 𝐶 → ( ( 𝐹𝐶 ) ‘ 1 ) = ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) ) ) )
17 16 simprd ( 𝐶 ∈ ( 𝑂𝐸 ) → ( 1 ∈ 𝐶 → ( ( 𝐹𝐶 ) ‘ 1 ) = ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) ) )
18 17 imp ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 1 ∈ 𝐶 ) → ( ( 𝐹𝐶 ) ‘ 1 ) = ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) )
19 1m1e0 ( 1 − 1 ) = 0
20 19 fveq2i ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) = ( ( 𝐹𝐶 ) ‘ 0 )
21 20 oveq1i ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) = ( ( ( 𝐹𝐶 ) ‘ 0 ) + 1 )
22 21 a1i ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 1 ∈ 𝐶 ) → ( ( ( 𝐹𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) = ( ( ( 𝐹𝐶 ) ‘ 0 ) + 1 ) )
23 1 2 3 4 5 ballotlemfval0 ( 𝐶𝑂 → ( ( 𝐹𝐶 ) ‘ 0 ) = 0 )
24 13 23 syl ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( 𝐹𝐶 ) ‘ 0 ) = 0 )
25 24 adantr ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 1 ∈ 𝐶 ) → ( ( 𝐹𝐶 ) ‘ 0 ) = 0 )
26 25 oveq1d ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 1 ∈ 𝐶 ) → ( ( ( 𝐹𝐶 ) ‘ 0 ) + 1 ) = ( 0 + 1 ) )
27 18 22 26 3eqtrrd ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 1 ∈ 𝐶 ) → ( 0 + 1 ) = ( ( 𝐹𝐶 ) ‘ 1 ) )
28 27 eqeq1d ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 1 ∈ 𝐶 ) → ( ( 0 + 1 ) = 0 ↔ ( ( 𝐹𝐶 ) ‘ 1 ) = 0 ) )
29 12 28 mtbii ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 1 ∈ 𝐶 ) → ¬ ( ( 𝐹𝐶 ) ‘ 1 ) = 0 )
30 1 2 3 4 5 6 7 8 ballotlemiex ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( 𝐼𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹𝐶 ) ‘ ( 𝐼𝐶 ) ) = 0 ) )
31 30 simprd ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( 𝐹𝐶 ) ‘ ( 𝐼𝐶 ) ) = 0 )
32 31 ad2antrr ( ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 1 ∈ 𝐶 ) ∧ ( 𝐼𝐶 ) = 1 ) → ( ( 𝐹𝐶 ) ‘ ( 𝐼𝐶 ) ) = 0 )
33 fveqeq2 ( ( 𝐼𝐶 ) = 1 → ( ( ( 𝐹𝐶 ) ‘ ( 𝐼𝐶 ) ) = 0 ↔ ( ( 𝐹𝐶 ) ‘ 1 ) = 0 ) )
34 33 adantl ( ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 1 ∈ 𝐶 ) ∧ ( 𝐼𝐶 ) = 1 ) → ( ( ( 𝐹𝐶 ) ‘ ( 𝐼𝐶 ) ) = 0 ↔ ( ( 𝐹𝐶 ) ‘ 1 ) = 0 ) )
35 32 34 mpbid ( ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 1 ∈ 𝐶 ) ∧ ( 𝐼𝐶 ) = 1 ) → ( ( 𝐹𝐶 ) ‘ 1 ) = 0 )
36 29 35 mtand ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 1 ∈ 𝐶 ) → ¬ ( 𝐼𝐶 ) = 1 )
37 36 neqned ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 1 ∈ 𝐶 ) → ( 𝐼𝐶 ) ≠ 1 )