Metamath Proof Explorer

Theorem ballotlemimin

Description: ( IC ) is the first tie. (Contributed by Thierry Arnoux, 1-Dec-2016) (Revised by AV, 6-Oct-2020)

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 ballotlemimin ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ¬ ∃ 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )

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 elfzle2 ⊢ ( 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) → 𝑘 ≤ ( ( 𝐼 ‘ 𝐶 ) − 1 ) )
10 9 adantl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ) → 𝑘 ≤ ( ( 𝐼 ‘ 𝐶 ) − 1 ) )
11 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) → 𝑘 ∈ ℤ )
12 1 2 3 4 5 6 7 8 ballotlemiex ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
13 12 simpld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
14 elfznn ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝐼 ‘ 𝐶 ) ∈ ℕ )
15 13 14 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ℕ )
16 15 nnzd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
17 zltlem1 ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝐼 ‘ 𝐶 ) ∈ ℤ ) → ( 𝑘 < ( 𝐼 ‘ 𝐶 ) ↔ 𝑘 ≤ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) )
18 11 16 17 syl2anr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ) → ( 𝑘 < ( 𝐼 ‘ 𝐶 ) ↔ 𝑘 ≤ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) )
19 10 18 mpbird ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ) → 𝑘 < ( 𝐼 ‘ 𝐶 ) )
20 19 adantr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ) → 𝑘 < ( 𝐼 ‘ 𝐶 ) )
21 1zzd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → 1 ∈ ℤ )
22 16 21 zsubcld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) − 1 ) ∈ ℤ )
23 22 zred ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) − 1 ) ∈ ℝ )
24 nnaddcl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
25 1 2 24 mp2an ⊢ ( 𝑀 + 𝑁 ) ∈ ℕ
26 25 a1i ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
27 26 nnred ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
28 elfzle2 ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) )
29 13 28 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) )
30 26 nnzd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
31 zlem1lt ⊢ ( ( ( 𝐼 ‘ 𝐶 ) ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) ↔ ( ( 𝐼 ‘ 𝐶 ) − 1 ) < ( 𝑀 + 𝑁 ) ) )
32 16 30 31 syl2anc ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ≤ ( 𝑀 + 𝑁 ) ↔ ( ( 𝐼 ‘ 𝐶 ) − 1 ) < ( 𝑀 + 𝑁 ) ) )
33 29 32 mpbid ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) − 1 ) < ( 𝑀 + 𝑁 ) )
34 23 27 33 ltled ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) − 1 ) ≤ ( 𝑀 + 𝑁 ) )
35 eluz ⊢ ( ( ( ( 𝐼 ‘ 𝐶 ) − 1 ) ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ↔ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ≤ ( 𝑀 + 𝑁 ) ) )
36 22 30 35 syl2anc ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ↔ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ≤ ( 𝑀 + 𝑁 ) ) )
37 34 36 mpbird ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) )
38 fzss2 ⊢ ( ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) → ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
39 37 38 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ⊆ ( 1 ... ( 𝑀 + 𝑁 ) ) )
40 39 sseld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) → 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) )
41 rabid ⊢ ( 𝑘 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ↔ ( 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ) )
42 1 2 3 4 5 6 7 8 ballotlemsup ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ∃ 𝑧 ∈ ℝ ( ∀ 𝑤 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } 𝑦 < 𝑤 ) ) )
43 ltso ⊢ < Or ℝ
44 43 a1i ⊢ ( ∃ 𝑧 ∈ ℝ ( ∀ 𝑤 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } 𝑦 < 𝑤 ) ) → < Or ℝ )
45 id ⊢ ( ∃ 𝑧 ∈ ℝ ( ∀ 𝑤 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } 𝑦 < 𝑤 ) ) → ∃ 𝑧 ∈ ℝ ( ∀ 𝑤 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } 𝑦 < 𝑤 ) ) )
46 44 45 inflb ⊢ ( ∃ 𝑧 ∈ ℝ ( ∀ 𝑤 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } ¬ 𝑤 < 𝑧 ∧ ∀ 𝑤 ∈ ℝ ( 𝑧 < 𝑤 → ∃ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } 𝑦 < 𝑤 ) ) → ( 𝑘 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } → ¬ 𝑘 < inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) ) )
47 42 46 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑘 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } → ¬ 𝑘 < inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) ) )
48 1 2 3 4 5 6 7 8 ballotlemi ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) = inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
49 48 breq2d ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑘 < ( 𝐼 ‘ 𝐶 ) ↔ 𝑘 < inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) ) )
50 49 notbid ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ¬ 𝑘 < ( 𝐼 ‘ 𝐶 ) ↔ ¬ 𝑘 < inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) ) )
51 47 50 sylibrd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑘 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } → ¬ 𝑘 < ( 𝐼 ‘ 𝐶 ) ) )
52 41 51 syl5bir ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ) → ¬ 𝑘 < ( 𝐼 ‘ 𝐶 ) ) )
53 40 52 syland ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ) → ¬ 𝑘 < ( 𝐼 ‘ 𝐶 ) ) )
54 53 imp ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ) ) → ¬ 𝑘 < ( 𝐼 ‘ 𝐶 ) )
55 biid ⊢ ( 𝑘 < ( 𝐼 ‘ 𝐶 ) ↔ 𝑘 < ( 𝐼 ‘ 𝐶 ) )
56 54 55 sylnib ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ( 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ) ) → ¬ 𝑘 < ( 𝐼 ‘ 𝐶 ) )
57 56 anassrs ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ) → ¬ 𝑘 < ( 𝐼 ‘ 𝐶 ) )
58 20 57 pm2.65da ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ) → ¬ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )
59 58 nrexdv ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ¬ ∃ 𝑘 ∈ ( 1 ... ( ( 𝐼 ‘ 𝐶 ) − 1 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 )