Step | Hyp | Ref
| Expression |
1 | | elfzle2 12216 |
. . . . . 6
⊢ (𝑘 ∈ (1...((𝐼‘𝐶) − 1)) → 𝑘 ≤ ((𝐼‘𝐶) − 1)) |
2 | 1 | adantl 481 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝑘 ∈ (1...((𝐼‘𝐶) − 1))) → 𝑘 ≤ ((𝐼‘𝐶) − 1)) |
3 | | elfzelz 12213 |
. . . . . 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 29890 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0)) |
13 | 12 | simpld 474 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁))) |
14 | | elfznn 12241 |
. . . . . . . 8
⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝐼‘𝐶) ∈ ℕ) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℕ) |
16 | 15 | nnzd 11357 |
. . . . . 6
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℤ) |
17 | | zltlem1 11307 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ (𝐼‘𝐶) ∈ ℤ) → (𝑘 < (𝐼‘𝐶) ↔ 𝑘 ≤ ((𝐼‘𝐶) − 1))) |
18 | 3, 16, 17 | syl2anr 494 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝑘 ∈ (1...((𝐼‘𝐶) − 1))) → (𝑘 < (𝐼‘𝐶) ↔ 𝑘 ≤ ((𝐼‘𝐶) − 1))) |
19 | 2, 18 | mpbird 246 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝑘 ∈ (1...((𝐼‘𝐶) − 1))) → 𝑘 < (𝐼‘𝐶)) |
20 | 19 | adantr 480 |
. . 3
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝑘 ∈ (1...((𝐼‘𝐶) − 1))) ∧ ((𝐹‘𝐶)‘𝑘) = 0) → 𝑘 < (𝐼‘𝐶)) |
21 | | 1zzd 11285 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → 1 ∈ ℤ) |
22 | 16, 21 | zsubcld 11363 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) − 1) ∈
ℤ) |
23 | 22 | zred 11358 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) − 1) ∈
ℝ) |
24 | | nnaddcl 10919 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) |
25 | 4, 5, 24 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑀 + 𝑁) ∈ ℕ |
26 | 25 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈ ℕ) |
27 | 26 | nnred 10912 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈ ℝ) |
28 | | elfzle2 12216 |
. . . . . . . . . . . . 13
⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) |
29 | 13, 28 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) |
30 | 26 | nnzd 11357 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈ ℤ) |
31 | | zlem1lt 11306 |
. . . . . . . . . . . . 13
⊢ (((𝐼‘𝐶) ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → ((𝐼‘𝐶) ≤ (𝑀 + 𝑁) ↔ ((𝐼‘𝐶) − 1) < (𝑀 + 𝑁))) |
32 | 16, 30, 31 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ≤ (𝑀 + 𝑁) ↔ ((𝐼‘𝐶) − 1) < (𝑀 + 𝑁))) |
33 | 29, 32 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) − 1) < (𝑀 + 𝑁)) |
34 | 23, 27, 33 | ltled 10064 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) − 1) ≤ (𝑀 + 𝑁)) |
35 | | eluz 11577 |
. . . . . . . . . . 11
⊢ ((((𝐼‘𝐶) − 1) ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → ((𝑀 + 𝑁) ∈
(ℤ≥‘((𝐼‘𝐶) − 1)) ↔ ((𝐼‘𝐶) − 1) ≤ (𝑀 + 𝑁))) |
36 | 22, 30, 35 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝑀 + 𝑁) ∈
(ℤ≥‘((𝐼‘𝐶) − 1)) ↔ ((𝐼‘𝐶) − 1) ≤ (𝑀 + 𝑁))) |
37 | 34, 36 | mpbird 246 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈
(ℤ≥‘((𝐼‘𝐶) − 1))) |
38 | | fzss2 12252 |
. . . . . . . . 9
⊢ ((𝑀 + 𝑁) ∈
(ℤ≥‘((𝐼‘𝐶) − 1)) → (1...((𝐼‘𝐶) − 1)) ⊆ (1...(𝑀 + 𝑁))) |
39 | 37, 38 | syl 17 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (1...((𝐼‘𝐶) − 1)) ⊆ (1...(𝑀 + 𝑁))) |
40 | 39 | sseld 3567 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑘 ∈ (1...((𝐼‘𝐶) − 1)) → 𝑘 ∈ (1...(𝑀 + 𝑁)))) |
41 | | rabid 3095 |
. . . . . . . 8
⊢ (𝑘 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} ↔ (𝑘 ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘𝑘) = 0)) |
42 | 4, 5, 6, 7, 8, 9, 10, 11 | ballotlemsup 29893 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ∃𝑧 ∈ ℝ (∀𝑤 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} ¬ 𝑤 < 𝑧 ∧ ∀𝑤 ∈ ℝ (𝑧 < 𝑤 → ∃𝑦 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}𝑦 < 𝑤))) |
43 | | ltso 9997 |
. . . . . . . . . . . 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 8278 |
. . . . . . . . . 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 29889 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) = inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}, ℝ, < )) |
49 | 48 | breq2d 4595 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑘 < (𝐼‘𝐶) ↔ 𝑘 < inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}, ℝ, < ))) |
50 | 49 | notbid 307 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (¬ 𝑘 < (𝐼‘𝐶) ↔ ¬ 𝑘 < inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}, ℝ, < ))) |
51 | 47, 50 | sylibrd 248 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑘 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} → ¬ 𝑘 < (𝐼‘𝐶))) |
52 | 41, 51 | syl5bir 232 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝑘 ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘𝑘) = 0) → ¬ 𝑘 < (𝐼‘𝐶))) |
53 | 40, 52 | syland 497 |
. . . . . 6
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝑘 ∈ (1...((𝐼‘𝐶) − 1)) ∧ ((𝐹‘𝐶)‘𝑘) = 0) → ¬ 𝑘 < (𝐼‘𝐶))) |
54 | 53 | imp 444 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝑘 ∈ (1...((𝐼‘𝐶) − 1)) ∧ ((𝐹‘𝐶)‘𝑘) = 0)) → ¬ 𝑘 < (𝐼‘𝐶)) |
55 | | biid 250 |
. . . . 5
⊢ (𝑘 < (𝐼‘𝐶) ↔ 𝑘 < (𝐼‘𝐶)) |
56 | 54, 55 | sylnib 317 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝑘 ∈ (1...((𝐼‘𝐶) − 1)) ∧ ((𝐹‘𝐶)‘𝑘) = 0)) → ¬ 𝑘 < (𝐼‘𝐶)) |
57 | 56 | anassrs 678 |
. . 3
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝑘 ∈ (1...((𝐼‘𝐶) − 1))) ∧ ((𝐹‘𝐶)‘𝑘) = 0) → ¬ 𝑘 < (𝐼‘𝐶)) |
58 | 20, 57 | pm2.65da 598 |
. 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝑘 ∈ (1...((𝐼‘𝐶) − 1))) → ¬ ((𝐹‘𝐶)‘𝑘) = 0) |
59 | 58 | nrexdv 2984 |
1
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ¬ ∃𝑘 ∈ (1...((𝐼‘𝐶) − 1))((𝐹‘𝐶)‘𝑘) = 0) |