Proof of Theorem ballotlemfrceq
Step | Hyp | Ref
| Expression |
1 | | ballotth.m |
. . . . . . . . 9
⊢ 𝑀 ∈ ℕ |
2 | | ballotth.n |
. . . . . . . . 9
⊢ 𝑁 ∈ ℕ |
3 | | ballotth.o |
. . . . . . . . 9
⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} |
4 | | ballotth.p |
. . . . . . . . 9
⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) |
5 | | ballotth.f |
. . . . . . . . 9
⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) |
6 | | ballotth.e |
. . . . . . . . 9
⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} |
7 | | ballotth.mgtn |
. . . . . . . . 9
⊢ 𝑁 < 𝑀 |
8 | | ballotth.i |
. . . . . . . . 9
⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) |
9 | | ballotth.s |
. . . . . . . . 9
⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | ballotlemsel1i 30574 |
. . . . . . . 8
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝐼‘𝐶))) |
11 | | 1zzd 11408 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 1 ∈
ℤ) |
12 | 1, 2, 3, 4, 5, 6, 7, 8 | ballotlemiex 30563 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0)) |
13 | 12 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0)) |
14 | 13 | simpld 475 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁))) |
15 | | elfzelz 12342 |
. . . . . . . . . 10
⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝐼‘𝐶) ∈ ℤ) |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (𝐼‘𝐶) ∈ ℤ) |
17 | | elfzuz3 12339 |
. . . . . . . . . . . . 13
⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝑀 + 𝑁) ∈
(ℤ≥‘(𝐼‘𝐶))) |
18 | | fzss2 12381 |
. . . . . . . . . . . . 13
⊢ ((𝑀 + 𝑁) ∈
(ℤ≥‘(𝐼‘𝐶)) → (1...(𝐼‘𝐶)) ⊆ (1...(𝑀 + 𝑁))) |
19 | 14, 17, 18 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (1...(𝐼‘𝐶)) ⊆ (1...(𝑀 + 𝑁))) |
20 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐽 ∈ (1...(𝐼‘𝐶))) |
21 | 19, 20 | sseldd 3604 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐽 ∈ (1...(𝑀 + 𝑁))) |
22 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | ballotlemsdom 30573 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝑀 + 𝑁))) |
23 | 21, 22 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝑀 + 𝑁))) |
24 | | elfzelz 12342 |
. . . . . . . . . 10
⊢ (((𝑆‘𝐶)‘𝐽) ∈ (1...(𝑀 + 𝑁)) → ((𝑆‘𝐶)‘𝐽) ∈ ℤ) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ∈ ℤ) |
26 | | fzsubel 12377 |
. . . . . . . . 9
⊢ (((1
∈ ℤ ∧ (𝐼‘𝐶) ∈ ℤ) ∧ (((𝑆‘𝐶)‘𝐽) ∈ ℤ ∧ 1 ∈ ℤ))
→ (((𝑆‘𝐶)‘𝐽) ∈ (1...(𝐼‘𝐶)) ↔ (((𝑆‘𝐶)‘𝐽) − 1) ∈ ((1 − 1)...((𝐼‘𝐶) − 1)))) |
27 | 11, 16, 25, 11, 26 | syl22anc 1327 |
. . . . . . . 8
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (((𝑆‘𝐶)‘𝐽) ∈ (1...(𝐼‘𝐶)) ↔ (((𝑆‘𝐶)‘𝐽) − 1) ∈ ((1 − 1)...((𝐼‘𝐶) − 1)))) |
28 | 10, 27 | mpbid 222 |
. . . . . . 7
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (((𝑆‘𝐶)‘𝐽) − 1) ∈ ((1 − 1)...((𝐼‘𝐶) − 1))) |
29 | | 1m1e0 11089 |
. . . . . . . 8
⊢ (1
− 1) = 0 |
30 | 29 | oveq1i 6660 |
. . . . . . 7
⊢ ((1
− 1)...((𝐼‘𝐶) − 1)) = (0...((𝐼‘𝐶) − 1)) |
31 | 28, 30 | syl6eleq 2711 |
. . . . . 6
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (((𝑆‘𝐶)‘𝐽) − 1) ∈ (0...((𝐼‘𝐶) − 1))) |
32 | 12 | simpld 475 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁))) |
33 | 32, 15 | syl 17 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℤ) |
34 | | 1zzd 11408 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → 1 ∈ ℤ) |
35 | 33, 34 | zsubcld 11487 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) − 1) ∈
ℤ) |
36 | | nnaddcl 11042 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) |
37 | 1, 2, 36 | mp2an 708 |
. . . . . . . . . . 11
⊢ (𝑀 + 𝑁) ∈ ℕ |
38 | 37 | nnzi 11401 |
. . . . . . . . . 10
⊢ (𝑀 + 𝑁) ∈ ℤ |
39 | 38 | a1i 11 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈ ℤ) |
40 | | elfzle2 12345 |
. . . . . . . . . . 11
⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) |
41 | 32, 40 | syl 17 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ≤ (𝑀 + 𝑁)) |
42 | | zlem1lt 11429 |
. . . . . . . . . . . 12
⊢ (((𝐼‘𝐶) ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → ((𝐼‘𝐶) ≤ (𝑀 + 𝑁) ↔ ((𝐼‘𝐶) − 1) < (𝑀 + 𝑁))) |
43 | 33, 39, 42 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ≤ (𝑀 + 𝑁) ↔ ((𝐼‘𝐶) − 1) < (𝑀 + 𝑁))) |
44 | 35 | zred 11482 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) − 1) ∈
ℝ) |
45 | 39 | zred 11482 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈ ℝ) |
46 | | ltle 10126 |
. . . . . . . . . . . 12
⊢ ((((𝐼‘𝐶) − 1) ∈ ℝ ∧ (𝑀 + 𝑁) ∈ ℝ) → (((𝐼‘𝐶) − 1) < (𝑀 + 𝑁) → ((𝐼‘𝐶) − 1) ≤ (𝑀 + 𝑁))) |
47 | 44, 45, 46 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (((𝐼‘𝐶) − 1) < (𝑀 + 𝑁) → ((𝐼‘𝐶) − 1) ≤ (𝑀 + 𝑁))) |
48 | 43, 47 | sylbid 230 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ≤ (𝑀 + 𝑁) → ((𝐼‘𝐶) − 1) ≤ (𝑀 + 𝑁))) |
49 | 41, 48 | mpd 15 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) − 1) ≤ (𝑀 + 𝑁)) |
50 | | eluz2 11693 |
. . . . . . . . 9
⊢ ((𝑀 + 𝑁) ∈
(ℤ≥‘((𝐼‘𝐶) − 1)) ↔ (((𝐼‘𝐶) − 1) ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ ((𝐼‘𝐶) − 1) ≤ (𝑀 + 𝑁))) |
51 | 35, 39, 49, 50 | syl3anbrc 1246 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑀 + 𝑁) ∈
(ℤ≥‘((𝐼‘𝐶) − 1))) |
52 | | fzss2 12381 |
. . . . . . . 8
⊢ ((𝑀 + 𝑁) ∈
(ℤ≥‘((𝐼‘𝐶) − 1)) → (0...((𝐼‘𝐶) − 1)) ⊆ (0...(𝑀 + 𝑁))) |
53 | 51, 52 | syl 17 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (0...((𝐼‘𝐶) − 1)) ⊆ (0...(𝑀 + 𝑁))) |
54 | 53 | sselda 3603 |
. . . . . 6
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (((𝑆‘𝐶)‘𝐽) − 1) ∈ (0...((𝐼‘𝐶) − 1))) → (((𝑆‘𝐶)‘𝐽) − 1) ∈ (0...(𝑀 + 𝑁))) |
55 | 31, 54 | syldan 487 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (((𝑆‘𝐶)‘𝐽) − 1) ∈ (0...(𝑀 + 𝑁))) |
56 | | ballotth.r |
. . . . . 6
⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐)) |
57 | | ballotlemg |
. . . . . 6
⊢ ↑ = (𝑢 ∈ Fin, 𝑣 ∈ Fin ↦ ((#‘(𝑣 ∩ 𝑢)) − (#‘(𝑣 ∖ 𝑢)))) |
58 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 56,
57 | ballotlemfg 30587 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (((𝑆‘𝐶)‘𝐽) − 1) ∈ (0...(𝑀 + 𝑁))) → ((𝐹‘𝐶)‘(((𝑆‘𝐶)‘𝐽) − 1)) = (𝐶 ↑ (1...(((𝑆‘𝐶)‘𝐽) − 1)))) |
59 | 55, 58 | syldan 487 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐹‘𝐶)‘(((𝑆‘𝐶)‘𝐽) − 1)) = (𝐶 ↑ (1...(((𝑆‘𝐶)‘𝐽) − 1)))) |
60 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 56,
57 | ballotlemfrc 30588 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐹‘(𝑅‘𝐶))‘𝐽) = (𝐶 ↑ (((𝑆‘𝐶)‘𝐽)...(𝐼‘𝐶)))) |
61 | 59, 60 | oveq12d 6668 |
. . 3
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (((𝐹‘𝐶)‘(((𝑆‘𝐶)‘𝐽) − 1)) + ((𝐹‘(𝑅‘𝐶))‘𝐽)) = ((𝐶 ↑ (1...(((𝑆‘𝐶)‘𝐽) − 1))) + (𝐶 ↑ (((𝑆‘𝐶)‘𝐽)...(𝐼‘𝐶))))) |
62 | | fzsplit3 29553 |
. . . . . 6
⊢ (((𝑆‘𝐶)‘𝐽) ∈ (1...(𝐼‘𝐶)) → (1...(𝐼‘𝐶)) = ((1...(((𝑆‘𝐶)‘𝐽) − 1)) ∪ (((𝑆‘𝐶)‘𝐽)...(𝐼‘𝐶)))) |
63 | 10, 62 | syl 17 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (1...(𝐼‘𝐶)) = ((1...(((𝑆‘𝐶)‘𝐽) − 1)) ∪ (((𝑆‘𝐶)‘𝐽)...(𝐼‘𝐶)))) |
64 | 63 | oveq2d 6666 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (𝐶 ↑ (1...(𝐼‘𝐶))) = (𝐶 ↑ ((1...(((𝑆‘𝐶)‘𝐽) − 1)) ∪ (((𝑆‘𝐶)‘𝐽)...(𝐼‘𝐶))))) |
65 | | 1eluzge0 11732 |
. . . . . . . . 9
⊢ 1 ∈
(ℤ≥‘0) |
66 | | fzss1 12380 |
. . . . . . . . 9
⊢ (1 ∈
(ℤ≥‘0) → (1...(𝑀 + 𝑁)) ⊆ (0...(𝑀 + 𝑁))) |
67 | 65, 66 | ax-mp 5 |
. . . . . . . 8
⊢
(1...(𝑀 + 𝑁)) ⊆ (0...(𝑀 + 𝑁)) |
68 | 67 | sseli 3599 |
. . . . . . 7
⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝐼‘𝐶) ∈ (0...(𝑀 + 𝑁))) |
69 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 56,
57 | ballotlemfg 30587 |
. . . . . . 7
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ (0...(𝑀 + 𝑁))) → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = (𝐶 ↑ (1...(𝐼‘𝐶)))) |
70 | 68, 69 | sylan2 491 |
. . . . . 6
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁))) → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = (𝐶 ↑ (1...(𝐼‘𝐶)))) |
71 | 14, 70 | syldan 487 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = (𝐶 ↑ (1...(𝐼‘𝐶)))) |
72 | 13 | simprd 479 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0) |
73 | 71, 72 | eqtr3d 2658 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (𝐶 ↑ (1...(𝐼‘𝐶))) = 0) |
74 | | fzfi 12771 |
. . . . . . 7
⊢
(1...(𝑀 + 𝑁)) ∈ Fin |
75 | | eldifi 3732 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → 𝐶 ∈ 𝑂) |
76 | 1, 2, 3 | ballotlemelo 30549 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑂 ↔ (𝐶 ⊆ (1...(𝑀 + 𝑁)) ∧ (#‘𝐶) = 𝑀)) |
77 | 76 | simplbi 476 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑂 → 𝐶 ⊆ (1...(𝑀 + 𝑁))) |
78 | 75, 77 | syl 17 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → 𝐶 ⊆ (1...(𝑀 + 𝑁))) |
79 | | ssfi 8180 |
. . . . . . 7
⊢
(((1...(𝑀 + 𝑁)) ∈ Fin ∧ 𝐶 ⊆ (1...(𝑀 + 𝑁))) → 𝐶 ∈ Fin) |
80 | 74, 78, 79 | sylancr 695 |
. . . . . 6
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → 𝐶 ∈ Fin) |
81 | 80 | adantr 481 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐶 ∈ Fin) |
82 | | fzfid 12772 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (1...(((𝑆‘𝐶)‘𝐽) − 1)) ∈ Fin) |
83 | | fzfid 12772 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (((𝑆‘𝐶)‘𝐽)...(𝐼‘𝐶)) ∈ Fin) |
84 | 25 | zred 11482 |
. . . . . 6
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ∈ ℝ) |
85 | | ltm1 10863 |
. . . . . 6
⊢ (((𝑆‘𝐶)‘𝐽) ∈ ℝ → (((𝑆‘𝐶)‘𝐽) − 1) < ((𝑆‘𝐶)‘𝐽)) |
86 | | fzdisj 12368 |
. . . . . 6
⊢ ((((𝑆‘𝐶)‘𝐽) − 1) < ((𝑆‘𝐶)‘𝐽) → ((1...(((𝑆‘𝐶)‘𝐽) − 1)) ∩ (((𝑆‘𝐶)‘𝐽)...(𝐼‘𝐶))) = ∅) |
87 | 84, 85, 86 | 3syl 18 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((1...(((𝑆‘𝐶)‘𝐽) − 1)) ∩ (((𝑆‘𝐶)‘𝐽)...(𝐼‘𝐶))) = ∅) |
88 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 56,
57, 81, 82, 83, 87 | ballotlemgun 30586 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (𝐶 ↑ ((1...(((𝑆‘𝐶)‘𝐽) − 1)) ∪ (((𝑆‘𝐶)‘𝐽)...(𝐼‘𝐶)))) = ((𝐶 ↑ (1...(((𝑆‘𝐶)‘𝐽) − 1))) + (𝐶 ↑ (((𝑆‘𝐶)‘𝐽)...(𝐼‘𝐶))))) |
89 | 64, 73, 88 | 3eqtr3rd 2665 |
. . 3
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐶 ↑ (1...(((𝑆‘𝐶)‘𝐽) − 1))) + (𝐶 ↑ (((𝑆‘𝐶)‘𝐽)...(𝐼‘𝐶)))) = 0) |
90 | 61, 89 | eqtrd 2656 |
. 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (((𝐹‘𝐶)‘(((𝑆‘𝐶)‘𝐽) − 1)) + ((𝐹‘(𝑅‘𝐶))‘𝐽)) = 0) |
91 | 75 | adantr 481 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐶 ∈ 𝑂) |
92 | 25, 11 | zsubcld 11487 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (((𝑆‘𝐶)‘𝐽) − 1) ∈
ℤ) |
93 | 1, 2, 3, 4, 5, 91,
92 | ballotlemfelz 30552 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐹‘𝐶)‘(((𝑆‘𝐶)‘𝐽) − 1)) ∈
ℤ) |
94 | 93 | zcnd 11483 |
. . 3
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐹‘𝐶)‘(((𝑆‘𝐶)‘𝐽) − 1)) ∈
ℂ) |
95 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 56 | ballotlemro 30584 |
. . . . . 6
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑅‘𝐶) ∈ 𝑂) |
96 | 95 | adantr 481 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → (𝑅‘𝐶) ∈ 𝑂) |
97 | | elfzelz 12342 |
. . . . . 6
⊢ (𝐽 ∈ (1...(𝐼‘𝐶)) → 𝐽 ∈ ℤ) |
98 | 20, 97 | syl 17 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → 𝐽 ∈ ℤ) |
99 | 1, 2, 3, 4, 5, 96,
98 | ballotlemfelz 30552 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐹‘(𝑅‘𝐶))‘𝐽) ∈ ℤ) |
100 | 99 | zcnd 11483 |
. . 3
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐹‘(𝑅‘𝐶))‘𝐽) ∈ ℂ) |
101 | | addeq0 29510 |
. . 3
⊢ ((((𝐹‘𝐶)‘(((𝑆‘𝐶)‘𝐽) − 1)) ∈ ℂ ∧ ((𝐹‘(𝑅‘𝐶))‘𝐽) ∈ ℂ) → ((((𝐹‘𝐶)‘(((𝑆‘𝐶)‘𝐽) − 1)) + ((𝐹‘(𝑅‘𝐶))‘𝐽)) = 0 ↔ ((𝐹‘𝐶)‘(((𝑆‘𝐶)‘𝐽) − 1)) = -((𝐹‘(𝑅‘𝐶))‘𝐽))) |
102 | 94, 100, 101 | syl2anc 693 |
. 2
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((((𝐹‘𝐶)‘(((𝑆‘𝐶)‘𝐽) − 1)) + ((𝐹‘(𝑅‘𝐶))‘𝐽)) = 0 ↔ ((𝐹‘𝐶)‘(((𝑆‘𝐶)‘𝐽) − 1)) = -((𝐹‘(𝑅‘𝐶))‘𝐽))) |
103 | 90, 102 | mpbid 222 |
1
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝐹‘𝐶)‘(((𝑆‘𝐶)‘𝐽) − 1)) = -((𝐹‘(𝑅‘𝐶))‘𝐽)) |