Proof of Theorem ballotlemsel1i
Step | Hyp | Ref
| Expression |
1 | | 1zzd 11760 |
. 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 1 ∈
ℤ) |
2 | | ballotth.m |
. . . . . 6
⊢ 𝑀 ∈ ℕ |
3 | | ballotth.n |
. . . . . 6
⊢ 𝑁 ∈ ℕ |
4 | | ballotth.o |
. . . . . 6
⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} |
5 | | ballotth.p |
. . . . . 6
⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) |
6 | | ballotth.f |
. . . . . 6
⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑐)) −
(♯‘((1...𝑖)
∖ 𝑐))))) |
7 | | ballotth.e |
. . . . . 6
⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} |
8 | | ballotth.mgtn |
. . . . . 6
⊢ 𝑁 < 𝑀 |
9 | | ballotth.i |
. . . . . 6
⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) |
10 | 2, 3, 4, 5, 6, 7, 8, 9 | ballotlemiex 31162 |
. . . . 5
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0)) |
11 | 10 | simpld 490 |
. . . 4
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁))) |
12 | | elfzelz 12659 |
. . . 4
⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝐼‘𝐶) ∈ ℤ) |
13 | 11, 12 | syl 17 |
. . 3
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℤ) |
14 | 13 | adantr 474 |
. 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (𝐼‘𝐶) ∈ ℤ) |
15 | | nnaddcl 11398 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) |
16 | 2, 3, 15 | mp2an 682 |
. . . . . . . . 9
⊢ (𝑀 + 𝑁) ∈ ℕ |
17 | 16 | nnzi 11753 |
. . . . . . . 8
⊢ (𝑀 + 𝑁) ∈ ℤ |
18 | 17 | a1i 11 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈ ℤ) |
19 | | elfzle2 12662 |
. . . . . . . 8
⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) |
20 | 11, 19 | syl 17 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) |
21 | | eluz2 11998 |
. . . . . . 7
⊢ ((𝑀 + 𝑁) ∈
(ℤ≥‘(𝐼‘𝐶)) ↔ ((𝐼‘𝐶) ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ (𝐼‘𝐶) ≤ (𝑀 + 𝑁))) |
22 | 13, 18, 20, 21 | syl3anbrc 1400 |
. . . . . 6
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈
(ℤ≥‘(𝐼‘𝐶))) |
23 | | fzss2 12698 |
. . . . . 6
⊢ ((𝑀 + 𝑁) ∈
(ℤ≥‘(𝐼‘𝐶)) → (1...(𝐼‘𝐶)) ⊆ (1...(𝑀 + 𝑁))) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (1...(𝐼‘𝐶)) ⊆ (1...(𝑀 + 𝑁))) |
25 | 24 | sselda 3820 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐽 ∈ (1...(𝑀 + 𝑁))) |
26 | | ballotth.s |
. . . . 5
⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) |
27 | 2, 3, 4, 5, 6, 7, 8, 9, 26 | ballotlemsdom 31172 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝑀 + 𝑁))) |
28 | 25, 27 | syldan 585 |
. . 3
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝑀 + 𝑁))) |
29 | | elfzelz 12659 |
. . 3
⊢ (((𝑆‘𝐶)‘𝐽) ∈ (1...(𝑀 + 𝑁)) → ((𝑆‘𝐶)‘𝐽) ∈ ℤ) |
30 | 28, 29 | syl 17 |
. 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ∈ ℤ) |
31 | | elfzelz 12659 |
. . . . . 6
⊢ (𝐽 ∈ (1...(𝐼‘𝐶)) → 𝐽 ∈ ℤ) |
32 | 31 | adantl 475 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐽 ∈ ℤ) |
33 | 32 | zred 11834 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐽 ∈ ℝ) |
34 | 14 | zred 11834 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (𝐼‘𝐶) ∈ ℝ) |
35 | | 1red 10377 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 1 ∈
ℝ) |
36 | 34, 35 | readdcld 10406 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐼‘𝐶) + 1) ∈ ℝ) |
37 | | elfzle2 12662 |
. . . . . 6
⊢ (𝐽 ∈ (1...(𝐼‘𝐶)) → 𝐽 ≤ (𝐼‘𝐶)) |
38 | 37 | adantl 475 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐽 ≤ (𝐼‘𝐶)) |
39 | 14 | zcnd 11835 |
. . . . . 6
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (𝐼‘𝐶) ∈ ℂ) |
40 | | 1cnd 10371 |
. . . . . 6
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 1 ∈
ℂ) |
41 | 39, 40 | pncand 10735 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (((𝐼‘𝐶) + 1) − 1) = (𝐼‘𝐶)) |
42 | 38, 41 | breqtrrd 4914 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐽 ≤ (((𝐼‘𝐶) + 1) − 1)) |
43 | 33, 36, 35, 42 | lesubd 10979 |
. . 3
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 1 ≤ (((𝐼‘𝐶) + 1) − 𝐽)) |
44 | 2, 3, 4, 5, 6, 7, 8, 9, 26 | ballotlemsv 31170 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) = if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽)) |
45 | 25, 44 | syldan 585 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) = if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽)) |
46 | 38 | iftrued 4314 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽) = (((𝐼‘𝐶) + 1) − 𝐽)) |
47 | 45, 46 | eqtrd 2813 |
. . 3
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) = (((𝐼‘𝐶) + 1) − 𝐽)) |
48 | 43, 47 | breqtrrd 4914 |
. 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 1 ≤ ((𝑆‘𝐶)‘𝐽)) |
49 | 13 | adantr 474 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → (𝐼‘𝐶) ∈ ℤ) |
50 | | elfznn 12687 |
. . . . . 6
⊢ (𝐽 ∈ (1...(𝑀 + 𝑁)) → 𝐽 ∈ ℕ) |
51 | 50 | adantl 475 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → 𝐽 ∈ ℕ) |
52 | 49, 51 | ltesubnnd 30132 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → (((𝐼‘𝐶) + 1) − 𝐽) ≤ (𝐼‘𝐶)) |
53 | 25, 52 | syldan 585 |
. . 3
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (((𝐼‘𝐶) + 1) − 𝐽) ≤ (𝐼‘𝐶)) |
54 | 47, 53 | eqbrtrd 4908 |
. 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ≤ (𝐼‘𝐶)) |
55 | | elfz4 12652 |
. 2
⊢ (((1
∈ ℤ ∧ (𝐼‘𝐶) ∈ ℤ ∧ ((𝑆‘𝐶)‘𝐽) ∈ ℤ) ∧ (1 ≤ ((𝑆‘𝐶)‘𝐽) ∧ ((𝑆‘𝐶)‘𝐽) ≤ (𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝐼‘𝐶))) |
56 | 1, 14, 30, 48, 54, 55 | syl32anc 1446 |
1
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝐼‘𝐶))) |