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 32049 |
. 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) = if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽)) |
11 | 1, 2, 3, 4, 5, 6, 7, 8 | ballotlemiex 32041 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0)) |
12 | 11 | simpld 498 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁))) |
13 | 12 | elfzelzd 13002 |
. . . . . 6
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℤ) |
14 | 13 | ad2antrr 726 |
. . . . 5
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (𝐼‘𝐶) ∈ ℤ) |
15 | | nnaddcl 11742 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) |
16 | 1, 2, 15 | mp2an 692 |
. . . . . . 7
⊢ (𝑀 + 𝑁) ∈ ℕ |
17 | 16 | nnzi 12090 |
. . . . . 6
⊢ (𝑀 + 𝑁) ∈ ℤ |
18 | 17 | a1i 11 |
. . . . 5
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (𝑀 + 𝑁) ∈ ℤ) |
19 | 12 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁))) |
20 | | elfzle2 13005 |
. . . . . 6
⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) |
22 | | eluz2 12333 |
. . . . . 6
⊢ ((𝑀 + 𝑁) ∈
(ℤ≥‘(𝐼‘𝐶)) ↔ ((𝐼‘𝐶) ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ (𝐼‘𝐶) ≤ (𝑀 + 𝑁))) |
23 | | fzss2 13041 |
. . . . . 6
⊢ ((𝑀 + 𝑁) ∈
(ℤ≥‘(𝐼‘𝐶)) → (1...(𝐼‘𝐶)) ⊆ (1...(𝑀 + 𝑁))) |
24 | 22, 23 | sylbir 238 |
. . . . 5
⊢ (((𝐼‘𝐶) ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) → (1...(𝐼‘𝐶)) ⊆ (1...(𝑀 + 𝑁))) |
25 | 14, 18, 21, 24 | syl3anc 1372 |
. . . 4
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (1...(𝐼‘𝐶)) ⊆ (1...(𝑀 + 𝑁))) |
26 | | 1zzd 12097 |
. . . . . . 7
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → 1 ∈ ℤ) |
27 | | simplr 769 |
. . . . . . . 8
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → 𝐽 ∈ (1...(𝑀 + 𝑁))) |
28 | 27 | elfzelzd 13002 |
. . . . . . 7
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → 𝐽 ∈ ℤ) |
29 | | elfzle1 13004 |
. . . . . . . 8
⊢ (𝐽 ∈ (1...(𝑀 + 𝑁)) → 1 ≤ 𝐽) |
30 | 27, 29 | syl 17 |
. . . . . . 7
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → 1 ≤ 𝐽) |
31 | | simpr 488 |
. . . . . . 7
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → 𝐽 ≤ (𝐼‘𝐶)) |
32 | 26, 14, 28, 30, 31 | elfzd 12992 |
. . . . . 6
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → 𝐽 ∈ (1...(𝐼‘𝐶))) |
33 | | fzrev3i 13068 |
. . . . . 6
⊢ (𝐽 ∈ (1...(𝐼‘𝐶)) → ((1 + (𝐼‘𝐶)) − 𝐽) ∈ (1...(𝐼‘𝐶))) |
34 | 32, 33 | syl 17 |
. . . . 5
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → ((1 + (𝐼‘𝐶)) − 𝐽) ∈ (1...(𝐼‘𝐶))) |
35 | | 1cnd 10717 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → 1 ∈ ℂ) |
36 | 13 | zcnd 12172 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℂ) |
37 | 35, 36 | addcomd 10923 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (1 + (𝐼‘𝐶)) = ((𝐼‘𝐶) + 1)) |
38 | 37 | oveq1d 7188 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((1 + (𝐼‘𝐶)) − 𝐽) = (((𝐼‘𝐶) + 1) − 𝐽)) |
39 | 38 | eleq1d 2818 |
. . . . . 6
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (((1 + (𝐼‘𝐶)) − 𝐽) ∈ (1...(𝐼‘𝐶)) ↔ (((𝐼‘𝐶) + 1) − 𝐽) ∈ (1...(𝐼‘𝐶)))) |
40 | 39 | ad2antrr 726 |
. . . . 5
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (((1 + (𝐼‘𝐶)) − 𝐽) ∈ (1...(𝐼‘𝐶)) ↔ (((𝐼‘𝐶) + 1) − 𝐽) ∈ (1...(𝐼‘𝐶)))) |
41 | 34, 40 | mpbid 235 |
. . . 4
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (((𝐼‘𝐶) + 1) − 𝐽) ∈ (1...(𝐼‘𝐶))) |
42 | 25, 41 | sseldd 3879 |
. . 3
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ 𝐽 ≤ (𝐼‘𝐶)) → (((𝐼‘𝐶) + 1) − 𝐽) ∈ (1...(𝑀 + 𝑁))) |
43 | | simplr 769 |
. . 3
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) ∧ ¬ 𝐽 ≤ (𝐼‘𝐶)) → 𝐽 ∈ (1...(𝑀 + 𝑁))) |
44 | 42, 43 | ifclda 4450 |
. 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽) ∈ (1...(𝑀 + 𝑁))) |
45 | 10, 44 | eqeltrd 2834 |
1
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝑀 + 𝑁))) |