Proof of Theorem ballotlemsdom
Step | Hyp | Ref
| Expression |
1 | | ballotth.m |
. . 3
⊢ 𝑀 ∈ ℕ |
2 | | ballotth.n |
. . 3
⊢ 𝑁 ∈ ℕ |
3 | | ballotth.o |
. . 3
⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} |
4 | | ballotth.p |
. . 3
⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) |
5 | | ballotth.f |
. . 3
⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑐)) −
(♯‘((1...𝑖)
∖ 𝑐))))) |
6 | | ballotth.e |
. . 3
⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} |
7 | | ballotth.mgtn |
. . 3
⊢ 𝑁 < 𝑀 |
8 | | ballotth.i |
. . 3
⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) |
9 | | ballotth.s |
. . 3
⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | ballotlemsv 31113 |
. 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) = if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽)) |
11 | | fzssuz 12682 |
. . . . . . . 8
⊢
(1...(𝑀 + 𝑁)) ⊆
(ℤ≥‘1) |
12 | | uzssz 11995 |
. . . . . . . 8
⊢
(ℤ≥‘1) ⊆ ℤ |
13 | 11, 12 | sstri 3836 |
. . . . . . 7
⊢
(1...(𝑀 + 𝑁)) ⊆
ℤ |
14 | 1, 2, 3, 4, 5, 6, 7, 8 | ballotlemiex 31105 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0)) |
15 | 14 | simpld 490 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁))) |
16 | 13, 15 | sseldi 3825 |
. . . . . 6
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℤ) |
17 | 16 | ad2antrr 717 |
. . . . 5
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (𝐼‘𝐶) ∈ ℤ) |
18 | | nnaddcl 11381 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) |
19 | 1, 2, 18 | mp2an 683 |
. . . . . . 7
⊢ (𝑀 + 𝑁) ∈ ℕ |
20 | 19 | nnzi 11736 |
. . . . . 6
⊢ (𝑀 + 𝑁) ∈ ℤ |
21 | 20 | a1i 11 |
. . . . 5
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (𝑀 + 𝑁) ∈ ℤ) |
22 | 15 | ad2antrr 717 |
. . . . . 6
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁))) |
23 | | elfzle2 12645 |
. . . . . 6
⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) |
25 | | eluz2 11981 |
. . . . . 6
⊢ ((𝑀 + 𝑁) ∈
(ℤ≥‘(𝐼‘𝐶)) ↔ ((𝐼‘𝐶) ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ (𝐼‘𝐶) ≤ (𝑀 + 𝑁))) |
26 | | fzss2 12681 |
. . . . . 6
⊢ ((𝑀 + 𝑁) ∈
(ℤ≥‘(𝐼‘𝐶)) → (1...(𝐼‘𝐶)) ⊆ (1...(𝑀 + 𝑁))) |
27 | 25, 26 | sylbir 227 |
. . . . 5
⊢ (((𝐼‘𝐶) ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) → (1...(𝐼‘𝐶)) ⊆ (1...(𝑀 + 𝑁))) |
28 | 17, 21, 24, 27 | syl3anc 1494 |
. . . 4
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (1...(𝐼‘𝐶)) ⊆ (1...(𝑀 + 𝑁))) |
29 | | 1zzd 11743 |
. . . . . . 7
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → 1 ∈ ℤ) |
30 | | simplr 785 |
. . . . . . . 8
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → 𝐽 ∈ (1...(𝑀 + 𝑁))) |
31 | 13, 30 | sseldi 3825 |
. . . . . . 7
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → 𝐽 ∈ ℤ) |
32 | | elfzle1 12644 |
. . . . . . . 8
⊢ (𝐽 ∈ (1...(𝑀 + 𝑁)) → 1 ≤ 𝐽) |
33 | 30, 32 | syl 17 |
. . . . . . 7
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → 1 ≤ 𝐽) |
34 | | simpr 479 |
. . . . . . 7
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → 𝐽 ≤ (𝐼‘𝐶)) |
35 | | elfz4 12635 |
. . . . . . 7
⊢ (((1
∈ ℤ ∧ (𝐼‘𝐶) ∈ ℤ ∧ 𝐽 ∈ ℤ) ∧ (1 ≤ 𝐽 ∧ 𝐽 ≤ (𝐼‘𝐶))) → 𝐽 ∈ (1...(𝐼‘𝐶))) |
36 | 29, 17, 31, 33, 34, 35 | syl32anc 1501 |
. . . . . 6
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → 𝐽 ∈ (1...(𝐼‘𝐶))) |
37 | | fzrev3i 12708 |
. . . . . 6
⊢ (𝐽 ∈ (1...(𝐼‘𝐶)) → ((1 + (𝐼‘𝐶)) − 𝐽) ∈ (1...(𝐼‘𝐶))) |
38 | 36, 37 | syl 17 |
. . . . 5
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → ((1 + (𝐼‘𝐶)) − 𝐽) ∈ (1...(𝐼‘𝐶))) |
39 | | 1cnd 10358 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → 1 ∈ ℂ) |
40 | 16 | zcnd 11818 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℂ) |
41 | 39, 40 | addcomd 10564 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (1 + (𝐼‘𝐶)) = ((𝐼‘𝐶) + 1)) |
42 | 41 | oveq1d 6925 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((1 + (𝐼‘𝐶)) − 𝐽) = (((𝐼‘𝐶) + 1) − 𝐽)) |
43 | 42 | eleq1d 2891 |
. . . . . 6
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (((1 + (𝐼‘𝐶)) − 𝐽) ∈ (1...(𝐼‘𝐶)) ↔ (((𝐼‘𝐶) + 1) − 𝐽) ∈ (1...(𝐼‘𝐶)))) |
44 | 43 | ad2antrr 717 |
. . . . 5
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (((1 + (𝐼‘𝐶)) − 𝐽) ∈ (1...(𝐼‘𝐶)) ↔ (((𝐼‘𝐶) + 1) − 𝐽) ∈ (1...(𝐼‘𝐶)))) |
45 | 38, 44 | mpbid 224 |
. . . 4
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (((𝐼‘𝐶) + 1) − 𝐽) ∈ (1...(𝐼‘𝐶))) |
46 | 28, 45 | sseldd 3828 |
. . 3
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (((𝐼‘𝐶) + 1) − 𝐽) ∈ (1...(𝑀 + 𝑁))) |
47 | | simplr 785 |
. . 3
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ ¬ 𝐽 ≤ (𝐼‘𝐶)) → 𝐽 ∈ (1...(𝑀 + 𝑁))) |
48 | 46, 47 | ifclda 4342 |
. 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽) ∈ (1...(𝑀 + 𝑁))) |
49 | 10, 48 | eqeltrd 2906 |
1
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝑀 + 𝑁))) |