Step | Hyp | Ref
| Expression |
1 | | elfzle2 12914 |
. . . . . 6
⊢ (𝑘 ∈ (1...((𝐼‘𝐶) − 1)) → 𝑘 ≤ ((𝐼‘𝐶) − 1)) |
2 | 1 | adantl 484 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝑘 ∈ (1...((𝐼‘𝐶) − 1))) → 𝑘 ≤ ((𝐼‘𝐶) − 1)) |
3 | | elfzelz 12911 |
. . . . . 6
⊢ (𝑘 ∈ (1...((𝐼‘𝐶) − 1)) → 𝑘 ∈ ℤ) |
4 | | ballotth.m |
. . . . . . . . . 10
⊢ 𝑀 ∈ ℕ |
5 | | ballotth.n |
. . . . . . . . . 10
⊢ 𝑁 ∈ ℕ |
6 | | ballotth.o |
. . . . . . . . . 10
⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} |
7 | | ballotth.p |
. . . . . . . . . 10
⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) |
8 | | ballotth.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑐)) −
(♯‘((1...𝑖)
∖ 𝑐))))) |
9 | | ballotth.e |
. . . . . . . . . 10
⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} |
10 | | ballotth.mgtn |
. . . . . . . . . 10
⊢ 𝑁 < 𝑀 |
11 | | ballotth.i |
. . . . . . . . . 10
⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) |
12 | 4, 5, 6, 7, 8, 9, 10, 11 | ballotlemiex 31761 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0)) |
13 | 12 | simpld 497 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁))) |
14 | | elfznn 12939 |
. . . . . . . 8
⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝐼‘𝐶) ∈ ℕ) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℕ) |
16 | 15 | nnzd 12089 |
. . . . . 6
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℤ) |
17 | | zltlem1 12038 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ (𝐼‘𝐶) ∈ ℤ) → (𝑘 < (𝐼‘𝐶) ↔ 𝑘 ≤ ((𝐼‘𝐶) − 1))) |
18 | 3, 16, 17 | syl2anr 598 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝑘 ∈ (1...((𝐼‘𝐶) − 1))) → (𝑘 < (𝐼‘𝐶) ↔ 𝑘 ≤ ((𝐼‘𝐶) − 1))) |
19 | 2, 18 | mpbird 259 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝑘 ∈ (1...((𝐼‘𝐶) − 1))) → 𝑘 < (𝐼‘𝐶)) |
20 | 19 | adantr 483 |
. . 3
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝑘 ∈ (1...((𝐼‘𝐶) − 1))) ∧ ((𝐹‘𝐶)‘𝑘) = 0) → 𝑘 < (𝐼‘𝐶)) |
21 | | 1zzd 12016 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → 1 ∈ ℤ) |
22 | 16, 21 | zsubcld 12095 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) − 1) ∈
ℤ) |
23 | 22 | zred 12090 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) − 1) ∈
ℝ) |
24 | | nnaddcl 11663 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) |
25 | 4, 5, 24 | mp2an 690 |
. . . . . . . . . . . . 13
⊢ (𝑀 + 𝑁) ∈ ℕ |
26 | 25 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈ ℕ) |
27 | 26 | nnred 11655 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈ ℝ) |
28 | | elfzle2 12914 |
. . . . . . . . . . . . 13
⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) |
29 | 13, 28 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) |
30 | 26 | nnzd 12089 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈ ℤ) |
31 | | zlem1lt 12037 |
. . . . . . . . . . . . 13
⊢ (((𝐼‘𝐶) ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → ((𝐼‘𝐶) ≤ (𝑀 + 𝑁) ↔ ((𝐼‘𝐶) − 1) < (𝑀 + 𝑁))) |
32 | 16, 30, 31 | syl2anc 586 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ≤ (𝑀 + 𝑁) ↔ ((𝐼‘𝐶) − 1) < (𝑀 + 𝑁))) |
33 | 29, 32 | mpbid 234 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) − 1) < (𝑀 + 𝑁)) |
34 | 23, 27, 33 | ltled 10790 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) − 1) ≤ (𝑀 + 𝑁)) |
35 | | eluz 12260 |
. . . . . . . . . . 11
⊢ ((((𝐼‘𝐶) − 1) ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → ((𝑀 + 𝑁) ∈
(ℤ≥‘((𝐼‘𝐶) − 1)) ↔ ((𝐼‘𝐶) − 1) ≤ (𝑀 + 𝑁))) |
36 | 22, 30, 35 | syl2anc 586 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝑀 + 𝑁) ∈
(ℤ≥‘((𝐼‘𝐶) − 1)) ↔ ((𝐼‘𝐶) − 1) ≤ (𝑀 + 𝑁))) |
37 | 34, 36 | mpbird 259 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈
(ℤ≥‘((𝐼‘𝐶) − 1))) |
38 | | fzss2 12950 |
. . . . . . . . 9
⊢ ((𝑀 + 𝑁) ∈
(ℤ≥‘((𝐼‘𝐶) − 1)) → (1...((𝐼‘𝐶) − 1)) ⊆ (1...(𝑀 + 𝑁))) |
39 | 37, 38 | syl 17 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (1...((𝐼‘𝐶) − 1)) ⊆ (1...(𝑀 + 𝑁))) |
40 | 39 | sseld 3968 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑘 ∈ (1...((𝐼‘𝐶) − 1)) → 𝑘 ∈ (1...(𝑀 + 𝑁)))) |
41 | | rabid 3380 |
. . . . . . . 8
⊢ (𝑘 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} ↔ (𝑘 ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘𝑘) = 0)) |
42 | 4, 5, 6, 7, 8, 9, 10, 11 | ballotlemsup 31764 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ∃𝑧 ∈ ℝ (∀𝑤 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} ¬ 𝑤 < 𝑧 ∧ ∀𝑤 ∈ ℝ (𝑧 < 𝑤 → ∃𝑦 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}𝑦 < 𝑤))) |
43 | | ltso 10723 |
. . . . . . . . . . . 12
⊢ < Or
ℝ |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢
(∃𝑧 ∈
ℝ (∀𝑤 ∈
{𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} ¬ 𝑤 < 𝑧 ∧ ∀𝑤 ∈ ℝ (𝑧 < 𝑤 → ∃𝑦 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}𝑦 < 𝑤)) → < Or ℝ) |
45 | | id 22 |
. . . . . . . . . . 11
⊢
(∃𝑧 ∈
ℝ (∀𝑤 ∈
{𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} ¬ 𝑤 < 𝑧 ∧ ∀𝑤 ∈ ℝ (𝑧 < 𝑤 → ∃𝑦 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}𝑦 < 𝑤)) → ∃𝑧 ∈ ℝ (∀𝑤 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} ¬ 𝑤 < 𝑧 ∧ ∀𝑤 ∈ ℝ (𝑧 < 𝑤 → ∃𝑦 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}𝑦 < 𝑤))) |
46 | 44, 45 | inflb 8955 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
ℝ (∀𝑤 ∈
{𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} ¬ 𝑤 < 𝑧 ∧ ∀𝑤 ∈ ℝ (𝑧 < 𝑤 → ∃𝑦 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}𝑦 < 𝑤)) → (𝑘 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} → ¬ 𝑘 < inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}, ℝ, < ))) |
47 | 42, 46 | syl 17 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑘 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} → ¬ 𝑘 < inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}, ℝ, < ))) |
48 | 4, 5, 6, 7, 8, 9, 10, 11 | ballotlemi 31760 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) = inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}, ℝ, < )) |
49 | 48 | breq2d 5080 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑘 < (𝐼‘𝐶) ↔ 𝑘 < inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}, ℝ, < ))) |
50 | 49 | notbid 320 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (¬ 𝑘 < (𝐼‘𝐶) ↔ ¬ 𝑘 < inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}, ℝ, < ))) |
51 | 47, 50 | sylibrd 261 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑘 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} → ¬ 𝑘 < (𝐼‘𝐶))) |
52 | 41, 51 | syl5bir 245 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝑘 ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘𝑘) = 0) → ¬ 𝑘 < (𝐼‘𝐶))) |
53 | 40, 52 | syland 604 |
. . . . . 6
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝑘 ∈ (1...((𝐼‘𝐶) − 1)) ∧ ((𝐹‘𝐶)‘𝑘) = 0) → ¬ 𝑘 < (𝐼‘𝐶))) |
54 | 53 | imp 409 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝑘 ∈ (1...((𝐼‘𝐶) − 1)) ∧ ((𝐹‘𝐶)‘𝑘) = 0)) → ¬ 𝑘 < (𝐼‘𝐶)) |
55 | | biid 263 |
. . . . 5
⊢ (𝑘 < (𝐼‘𝐶) ↔ 𝑘 < (𝐼‘𝐶)) |
56 | 54, 55 | sylnib 330 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝑘 ∈ (1...((𝐼‘𝐶) − 1)) ∧ ((𝐹‘𝐶)‘𝑘) = 0)) → ¬ 𝑘 < (𝐼‘𝐶)) |
57 | 56 | anassrs 470 |
. . 3
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝑘 ∈ (1...((𝐼‘𝐶) − 1))) ∧ ((𝐹‘𝐶)‘𝑘) = 0) → ¬ 𝑘 < (𝐼‘𝐶)) |
58 | 20, 57 | pm2.65da 815 |
. 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝑘 ∈ (1...((𝐼‘𝐶) − 1))) → ¬ ((𝐹‘𝐶)‘𝑘) = 0) |
59 | 58 | nrexdv 3272 |
1
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ¬ ∃𝑘 ∈ (1...((𝐼‘𝐶) − 1))((𝐹‘𝐶)‘𝑘) = 0) |