Metamath Proof Explorer

Theorem ballotlemi1

Description: The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 12-Mar-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 ballotlemi1 ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 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 0re ⊢ 0 ∈ ℝ
10 1re ⊢ 1 ∈ ℝ
11 9 10 resubcli ⊢ ( 0 − 1 ) ∈ ℝ
12 0lt1 ⊢ 0 < 1
13 ltsub23 ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 0 − 1 ) < 0 ↔ ( 0 − 0 ) < 1 ) )
14 9 10 9 13 mp3an ⊢ ( ( 0 − 1 ) < 0 ↔ ( 0 − 0 ) < 1 )
15 0m0e0 ⊢ ( 0 − 0 ) = 0
16 15 breq1i ⊢ ( ( 0 − 0 ) < 1 ↔ 0 < 1 )
17 14 16 bitr2i ⊢ ( 0 < 1 ↔ ( 0 − 1 ) < 0 )
18 12 17 mpbi ⊢ ( 0 − 1 ) < 0
19 11 18 gtneii ⊢ 0 ≠ ( 0 − 1 )
20 19 nesymi ⊢ ¬ ( 0 − 1 ) = 0
21 eldifi ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 𝐶 ∈ 𝑂 )
22 1nn ⊢ 1 ∈ ℕ
23 22 a1i ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 1 ∈ ℕ )
24 1 2 3 4 5 21 23 ballotlemfp1 ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( ¬ 1 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) ) ∧ ( 1 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) + 1 ) ) ) )
25 24 simpld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ¬ 1 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) ) )
26 25 imp ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) )
27 1m1e0 ⊢ ( 1 − 1 ) = 0
28 27 fveq2i ⊢ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 0 )
29 28 oveq1i ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) − 1 )
30 29 a1i ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 1 − 1 ) ) − 1 ) = ( ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) − 1 ) )
31 1 2 3 4 5 ballotlemfval0 ⊢ ( 𝐶 ∈ 𝑂 → ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) = 0 )
32 21 31 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) = 0 )
33 32 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) = 0 )
34 33 oveq1d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 0 ) − 1 ) = ( 0 − 1 ) )
35 26 30 34 3eqtrrd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( 0 − 1 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) )
36 35 eqeq1d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( ( 0 − 1 ) = 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = 0 ) )
37 20 36 mtbii ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = 0 )
38 1 2 3 4 5 6 7 8 ballotlemiex ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
39 38 simprd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 )
40 39 ad2antrr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) ∧ ( 𝐼 ‘ 𝐶 ) = 1 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 )
41 fveqeq2 ⊢ ( ( 𝐼 ‘ 𝐶 ) = 1 → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = 0 ) )
42 41 adantl ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) ∧ ( 𝐼 ‘ 𝐶 ) = 1 ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = 0 ) )
43 40 42 mpbid ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) ∧ ( 𝐼 ‘ 𝐶 ) = 1 ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 1 ) = 0 )
44 37 43 mtand ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ¬ ( 𝐼 ‘ 𝐶 ) = 1 )
45 44 neqned ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝐶 ) → ( 𝐼 ‘ 𝐶 ) ≠ 1 )