Metamath Proof Explorer


Theorem ballotlemsgt1

Description: S maps values less than ( IC ) to values greater than 1. (Contributed by Thierry Arnoux, 28-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 } , ℝ , < ) )
ballotth.s 𝑆 = ( 𝑐 ∈ ( 𝑂𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼𝑐 ) , ( ( ( 𝐼𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
Assertion ballotlemsgt1 ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 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 ballotth.s 𝑆 = ( 𝑐 ∈ ( 𝑂𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼𝑐 ) , ( ( ( 𝐼𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
10 elfzelz ( 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 𝐽 ∈ ℤ )
11 10 3ad2ant2 ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → 𝐽 ∈ ℤ )
12 11 zred ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → 𝐽 ∈ ℝ )
13 1 2 3 4 5 6 7 8 ballotlemiex ( 𝐶 ∈ ( 𝑂𝐸 ) → ( ( 𝐼𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹𝐶 ) ‘ ( 𝐼𝐶 ) ) = 0 ) )
14 13 simpld ( 𝐶 ∈ ( 𝑂𝐸 ) → ( 𝐼𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
15 14 elfzelzd ( 𝐶 ∈ ( 𝑂𝐸 ) → ( 𝐼𝐶 ) ∈ ℤ )
16 15 3ad2ant1 ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → ( 𝐼𝐶 ) ∈ ℤ )
17 16 zred ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → ( 𝐼𝐶 ) ∈ ℝ )
18 1red ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → 1 ∈ ℝ )
19 17 18 readdcld ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → ( ( 𝐼𝐶 ) + 1 ) ∈ ℝ )
20 simp3 ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → 𝐽 < ( 𝐼𝐶 ) )
21 16 zcnd ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → ( 𝐼𝐶 ) ∈ ℂ )
22 1cnd ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → 1 ∈ ℂ )
23 21 22 pncand ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → ( ( ( 𝐼𝐶 ) + 1 ) − 1 ) = ( 𝐼𝐶 ) )
24 20 23 breqtrrd ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → 𝐽 < ( ( ( 𝐼𝐶 ) + 1 ) − 1 ) )
25 12 19 18 24 ltsub13d ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → 1 < ( ( ( 𝐼𝐶 ) + 1 ) − 𝐽 ) )
26 1 2 3 4 5 6 7 8 9 ballotlemsv ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆𝐶 ) ‘ 𝐽 ) = if ( 𝐽 ≤ ( 𝐼𝐶 ) , ( ( ( 𝐼𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) )
27 26 3adant3 ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → ( ( 𝑆𝐶 ) ‘ 𝐽 ) = if ( 𝐽 ≤ ( 𝐼𝐶 ) , ( ( ( 𝐼𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) )
28 12 17 20 ltled ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → 𝐽 ≤ ( 𝐼𝐶 ) )
29 28 iftrued ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → if ( 𝐽 ≤ ( 𝐼𝐶 ) , ( ( ( 𝐼𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) = ( ( ( 𝐼𝐶 ) + 1 ) − 𝐽 ) )
30 27 29 eqtrd ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → ( ( 𝑆𝐶 ) ‘ 𝐽 ) = ( ( ( 𝐼𝐶 ) + 1 ) − 𝐽 ) )
31 25 30 breqtrrd ( ( 𝐶 ∈ ( 𝑂𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝐽 < ( 𝐼𝐶 ) ) → 1 < ( ( 𝑆𝐶 ) ‘ 𝐽 ) )