Step | Hyp | Ref
| Expression |
1 | | eldif 3550 |
. 2
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) ↔ (𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝐸)) |
2 | | df-or 384 |
. . . 4
⊢ (((𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝑂) ∨ (𝐶 ∈ 𝑂 ∧ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖))) ↔ (¬ (𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝑂) → (𝐶 ∈ 𝑂 ∧ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)))) |
3 | | pm3.24 922 |
. . . . 5
⊢ ¬
(𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝑂) |
4 | 3 | a1bi 351 |
. . . 4
⊢ ((𝐶 ∈ 𝑂 ∧ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)) ↔ (¬ (𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝑂) → (𝐶 ∈ 𝑂 ∧ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)))) |
5 | 2, 4 | bitr4i 266 |
. . 3
⊢ (((𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝑂) ∨ (𝐶 ∈ 𝑂 ∧ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖))) ↔ (𝐶 ∈ 𝑂 ∧ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖))) |
6 | | ballotth.m |
. . . . . . 7
⊢ 𝑀 ∈ ℕ |
7 | | ballotth.n |
. . . . . . 7
⊢ 𝑁 ∈ ℕ |
8 | | ballotth.o |
. . . . . . 7
⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} |
9 | | ballotth.p |
. . . . . . 7
⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) |
10 | | ballotth.f |
. . . . . . 7
⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) |
11 | | ballotth.e |
. . . . . . 7
⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} |
12 | 6, 7, 8, 9, 10, 11 | ballotleme 29885 |
. . . . . 6
⊢ (𝐶 ∈ 𝐸 ↔ (𝐶 ∈ 𝑂 ∧ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖))) |
13 | 12 | notbii 309 |
. . . . 5
⊢ (¬
𝐶 ∈ 𝐸 ↔ ¬ (𝐶 ∈ 𝑂 ∧ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖))) |
14 | 13 | anbi2i 726 |
. . . 4
⊢ ((𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝐸) ↔ (𝐶 ∈ 𝑂 ∧ ¬ (𝐶 ∈ 𝑂 ∧ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)))) |
15 | | ianor 508 |
. . . . 5
⊢ (¬
(𝐶 ∈ 𝑂 ∧ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)) ↔ (¬ 𝐶 ∈ 𝑂 ∨ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖))) |
16 | 15 | anbi2i 726 |
. . . 4
⊢ ((𝐶 ∈ 𝑂 ∧ ¬ (𝐶 ∈ 𝑂 ∧ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖))) ↔ (𝐶 ∈ 𝑂 ∧ (¬ 𝐶 ∈ 𝑂 ∨ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)))) |
17 | | andi 907 |
. . . 4
⊢ ((𝐶 ∈ 𝑂 ∧ (¬ 𝐶 ∈ 𝑂 ∨ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖))) ↔ ((𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝑂) ∨ (𝐶 ∈ 𝑂 ∧ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)))) |
18 | 14, 16, 17 | 3bitri 285 |
. . 3
⊢ ((𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝐸) ↔ ((𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝑂) ∨ (𝐶 ∈ 𝑂 ∧ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)))) |
19 | | 0p1e1 11009 |
. . . . . . . . . . . . 13
⊢ (0 + 1) =
1 |
20 | 19 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢ ((0 +
1)...(𝑀 + 𝑁)) = (1...(𝑀 + 𝑁)) |
21 | | 0z 11265 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℤ |
22 | | fzp1ss 12262 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℤ → ((0 + 1)...(𝑀 + 𝑁)) ⊆ (0...(𝑀 + 𝑁))) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((0 +
1)...(𝑀 + 𝑁)) ⊆ (0...(𝑀 + 𝑁)) |
24 | 20, 23 | eqsstr3i 3599 |
. . . . . . . . . . 11
⊢
(1...(𝑀 + 𝑁)) ⊆ (0...(𝑀 + 𝑁)) |
25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝑂 → (1...(𝑀 + 𝑁)) ⊆ (0...(𝑀 + 𝑁))) |
26 | 25 | sseld 3567 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑂 → (𝑖 ∈ (1...(𝑀 + 𝑁)) → 𝑖 ∈ (0...(𝑀 + 𝑁)))) |
27 | 26 | imdistani 722 |
. . . . . . . 8
⊢ ((𝐶 ∈ 𝑂 ∧ 𝑖 ∈ (1...(𝑀 + 𝑁))) → (𝐶 ∈ 𝑂 ∧ 𝑖 ∈ (0...(𝑀 + 𝑁)))) |
28 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ 𝑂 ∧ 𝑗 ∈ (0...(𝑀 + 𝑁))) → 𝐶 ∈ 𝑂) |
29 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (0...(𝑀 + 𝑁)) → 𝑗 ∈ ℤ) |
30 | 29 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ 𝑂 ∧ 𝑗 ∈ (0...(𝑀 + 𝑁))) → 𝑗 ∈ ℤ) |
31 | 6, 7, 8, 9, 10, 28, 30 | ballotlemfelz 29879 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ 𝑂 ∧ 𝑗 ∈ (0...(𝑀 + 𝑁))) → ((𝐹‘𝐶)‘𝑗) ∈ ℤ) |
32 | 31 | zred 11358 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ 𝑂 ∧ 𝑗 ∈ (0...(𝑀 + 𝑁))) → ((𝐹‘𝐶)‘𝑗) ∈ ℝ) |
33 | 32 | sbimi 1873 |
. . . . . . . . 9
⊢ ([𝑖 / 𝑗](𝐶 ∈ 𝑂 ∧ 𝑗 ∈ (0...(𝑀 + 𝑁))) → [𝑖 / 𝑗]((𝐹‘𝐶)‘𝑗) ∈ ℝ) |
34 | | sban 2387 |
. . . . . . . . . 10
⊢ ([𝑖 / 𝑗](𝐶 ∈ 𝑂 ∧ 𝑗 ∈ (0...(𝑀 + 𝑁))) ↔ ([𝑖 / 𝑗]𝐶 ∈ 𝑂 ∧ [𝑖 / 𝑗]𝑗 ∈ (0...(𝑀 + 𝑁)))) |
35 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝐶 ∈ 𝑂 |
36 | 35 | sbf 2368 |
. . . . . . . . . . 11
⊢ ([𝑖 / 𝑗]𝐶 ∈ 𝑂 ↔ 𝐶 ∈ 𝑂) |
37 | | clelsb3 2716 |
. . . . . . . . . . 11
⊢ ([𝑖 / 𝑗]𝑗 ∈ (0...(𝑀 + 𝑁)) ↔ 𝑖 ∈ (0...(𝑀 + 𝑁))) |
38 | 36, 37 | anbi12i 729 |
. . . . . . . . . 10
⊢ (([𝑖 / 𝑗]𝐶 ∈ 𝑂 ∧ [𝑖 / 𝑗]𝑗 ∈ (0...(𝑀 + 𝑁))) ↔ (𝐶 ∈ 𝑂 ∧ 𝑖 ∈ (0...(𝑀 + 𝑁)))) |
39 | 34, 38 | bitri 263 |
. . . . . . . . 9
⊢ ([𝑖 / 𝑗](𝐶 ∈ 𝑂 ∧ 𝑗 ∈ (0...(𝑀 + 𝑁))) ↔ (𝐶 ∈ 𝑂 ∧ 𝑖 ∈ (0...(𝑀 + 𝑁)))) |
40 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑗((𝐹‘𝐶)‘𝑖) ∈ ℝ |
41 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑖 → ((𝐹‘𝐶)‘𝑗) = ((𝐹‘𝐶)‘𝑖)) |
42 | 41 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑖 → (((𝐹‘𝐶)‘𝑗) ∈ ℝ ↔ ((𝐹‘𝐶)‘𝑖) ∈ ℝ)) |
43 | 40, 42 | sbie 2396 |
. . . . . . . . 9
⊢ ([𝑖 / 𝑗]((𝐹‘𝐶)‘𝑗) ∈ ℝ ↔ ((𝐹‘𝐶)‘𝑖) ∈ ℝ) |
44 | 33, 39, 43 | 3imtr3i 279 |
. . . . . . . 8
⊢ ((𝐶 ∈ 𝑂 ∧ 𝑖 ∈ (0...(𝑀 + 𝑁))) → ((𝐹‘𝐶)‘𝑖) ∈ ℝ) |
45 | 27, 44 | syl 17 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑂 ∧ 𝑖 ∈ (1...(𝑀 + 𝑁))) → ((𝐹‘𝐶)‘𝑖) ∈ ℝ) |
46 | | 0red 9920 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑂 ∧ 𝑖 ∈ (1...(𝑀 + 𝑁))) → 0 ∈
ℝ) |
47 | 45, 46 | lenltd 10062 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑂 ∧ 𝑖 ∈ (1...(𝑀 + 𝑁))) → (((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ¬ 0 < ((𝐹‘𝐶)‘𝑖))) |
48 | 47 | rexbidva 3031 |
. . . . 5
⊢ (𝐶 ∈ 𝑂 → (∃𝑖 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ∃𝑖 ∈ (1...(𝑀 + 𝑁)) ¬ 0 < ((𝐹‘𝐶)‘𝑖))) |
49 | | rexnal 2978 |
. . . . 5
⊢
(∃𝑖 ∈
(1...(𝑀 + 𝑁)) ¬ 0 < ((𝐹‘𝐶)‘𝑖) ↔ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)) |
50 | 48, 49 | syl6bb 275 |
. . . 4
⊢ (𝐶 ∈ 𝑂 → (∃𝑖 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑖) ≤ 0 ↔ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖))) |
51 | 50 | pm5.32i 667 |
. . 3
⊢ ((𝐶 ∈ 𝑂 ∧ ∃𝑖 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑖) ≤ 0) ↔ (𝐶 ∈ 𝑂 ∧ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖))) |
52 | 5, 18, 51 | 3bitr4i 291 |
. 2
⊢ ((𝐶 ∈ 𝑂 ∧ ¬ 𝐶 ∈ 𝐸) ↔ (𝐶 ∈ 𝑂 ∧ ∃𝑖 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑖) ≤ 0)) |
53 | 1, 52 | bitri 263 |
1
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) ↔ (𝐶 ∈ 𝑂 ∧ ∃𝑖 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑖) ≤ 0)) |