Metamath Proof Explorer

Theorem ballotlemodife

Description: Elements of ( O \ E ) . (Contributed by Thierry Arnoux, 7-Dec-2016)

Ref Expression
Hypotheses ballotth.m ⊢ 𝑀 ∈ ℕ
ballotth.n ⊢ 𝑁 ∈ ℕ
ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
ballotth.e ⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
Assertion ballotlemodife ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ↔ ( 𝐶 ∈ 𝑂 ∧ ∃ 𝑖 ∈ ( 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 eldif ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ↔ ( 𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝐸 ) )
8 df-or ⊢ ( ( ( 𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝑂 ) ∨ ( 𝐶 ∈ 𝑂 ∧ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) ) ↔ ( ¬ ( 𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝑂 ) → ( 𝐶 ∈ 𝑂 ∧ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) ) )
9 pm3.24 ⊢ ¬ ( 𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝑂 )
10 9 a1bi ⊢ ( ( 𝐶 ∈ 𝑂 ∧ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) ↔ ( ¬ ( 𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝑂 ) → ( 𝐶 ∈ 𝑂 ∧ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) ) )
11 8 10 bitr4i ⊢ ( ( ( 𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝑂 ) ∨ ( 𝐶 ∈ 𝑂 ∧ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) ) ↔ ( 𝐶 ∈ 𝑂 ∧ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) )
12 1 2 3 4 5 6 ballotleme ⊢ ( 𝐶 ∈ 𝐸 ↔ ( 𝐶 ∈ 𝑂 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) )
13 12 notbii ⊢ ( ¬ 𝐶 ∈ 𝐸 ↔ ¬ ( 𝐶 ∈ 𝑂 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) )
14 13 anbi2i ⊢ ( ( 𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝐸 ) ↔ ( 𝐶 ∈ 𝑂 ∧ ¬ ( 𝐶 ∈ 𝑂 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) ) )
15 ianor ⊢ ( ¬ ( 𝐶 ∈ 𝑂 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) ↔ ( ¬ 𝐶 ∈ 𝑂 ∨ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) )
16 15 anbi2i ⊢ ( ( 𝐶 ∈ 𝑂 ∧ ¬ ( 𝐶 ∈ 𝑂 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) ) ↔ ( 𝐶 ∈ 𝑂 ∧ ( ¬ 𝐶 ∈ 𝑂 ∨ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) ) )
17 andi ⊢ ( ( 𝐶 ∈ 𝑂 ∧ ( ¬ 𝐶 ∈ 𝑂 ∨ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) ) ↔ ( ( 𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝑂 ) ∨ ( 𝐶 ∈ 𝑂 ∧ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) ) )
18 14 16 17 3bitri ⊢ ( ( 𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝐸 ) ↔ ( ( 𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝑂 ) ∨ ( 𝐶 ∈ 𝑂 ∧ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) ) )
19 fz1ssfz0 ⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ⊆ ( 0 ... ( 𝑀 + 𝑁 ) )
20 19 a1i ⊢ ( 𝐶 ∈ 𝑂 → ( 1 ... ( 𝑀 + 𝑁 ) ) ⊆ ( 0 ... ( 𝑀 + 𝑁 ) ) )
21 20 sseld ⊢ ( 𝐶 ∈ 𝑂 → ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 𝑖 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) )
22 21 imdistani ⊢ ( ( 𝐶 ∈ 𝑂 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( 𝐶 ∈ 𝑂 ∧ 𝑖 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) )
23 simpl ⊢ ( ( 𝐶 ∈ 𝑂 ∧ 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → 𝐶 ∈ 𝑂 )
24 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) → 𝑗 ∈ ℤ )
25 24 adantl ⊢ ( ( 𝐶 ∈ 𝑂 ∧ 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → 𝑗 ∈ ℤ )
26 1 2 3 4 5 23 25 ballotlemfelz ⊢ ( ( 𝐶 ∈ 𝑂 ∧ 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑗 ) ∈ ℤ )
27 26 zred ⊢ ( ( 𝐶 ∈ 𝑂 ∧ 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑗 ) ∈ ℝ )
28 27 sbimi ⊢ ( [ 𝑖 / 𝑗 ] ( 𝐶 ∈ 𝑂 ∧ 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → [ 𝑖 / 𝑗 ] ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑗 ) ∈ ℝ )
29 sban ⊢ ( [ 𝑖 / 𝑗 ] ( 𝐶 ∈ 𝑂 ∧ 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ↔ ( [ 𝑖 / 𝑗 ] 𝐶 ∈ 𝑂 ∧ [ 𝑖 / 𝑗 ] 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) )
30 sbv ⊢ ( [ 𝑖 / 𝑗 ] 𝐶 ∈ 𝑂 ↔ 𝐶 ∈ 𝑂 )
31 clelsb3 ⊢ ( [ 𝑖 / 𝑗 ] 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ↔ 𝑖 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) )
32 30 31 anbi12i ⊢ ( ( [ 𝑖 / 𝑗 ] 𝐶 ∈ 𝑂 ∧ [ 𝑖 / 𝑗 ] 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ↔ ( 𝐶 ∈ 𝑂 ∧ 𝑖 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) )
33 29 32 bitri ⊢ ( [ 𝑖 / 𝑗 ] ( 𝐶 ∈ 𝑂 ∧ 𝑗 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) ↔ ( 𝐶 ∈ 𝑂 ∧ 𝑖 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) )
34 nfv ⊢ Ⅎ 𝑗 ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ∈ ℝ
35 fveq2 ⊢ ( 𝑗 = 𝑖 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑗 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) )
36 35 eleq1d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑗 ) ∈ ℝ ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ∈ ℝ ) )
37 34 36 sbiev ⊢ ( [ 𝑖 / 𝑗 ] ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑗 ) ∈ ℝ ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ∈ ℝ )
38 28 33 37 3imtr3i ⊢ ( ( 𝐶 ∈ 𝑂 ∧ 𝑖 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ∈ ℝ )
39 22 38 syl ⊢ ( ( 𝐶 ∈ 𝑂 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ∈ ℝ )
40 0red ⊢ ( ( 𝐶 ∈ 𝑂 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → 0 ∈ ℝ )
41 39 40 lenltd ⊢ ( ( 𝐶 ∈ 𝑂 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ↔ ¬ 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) )
42 41 rexbidva ⊢ ( 𝐶 ∈ 𝑂 → ( ∃ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ↔ ∃ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ¬ 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) )
43 rexnal ⊢ ( ∃ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ¬ 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ↔ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) )
44 42 43 bitrdi ⊢ ( 𝐶 ∈ 𝑂 → ( ∃ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ↔ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) )
45 44 pm5.32i ⊢ ( ( 𝐶 ∈ 𝑂 ∧ ∃ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ) ↔ ( 𝐶 ∈ 𝑂 ∧ ¬ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ) )
46 11 18 45 3bitr4i ⊢ ( ( 𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝐸 ) ↔ ( 𝐶 ∈ 𝑂 ∧ ∃ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ) )
47 7 46 bitri ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ↔ ( 𝐶 ∈ 𝑂 ∧ ∃ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑖 ) ≤ 0 ) )