Proof of Theorem ballotlem1c
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 | | eldifi 4015 |
. . . 4
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → 𝐶 ∈ 𝑂) |
7 | 6 | ad2antrr 726 |
. . 3
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → 𝐶 ∈ 𝑂) |
8 | | ballotth.e |
. . . . . . . . . 10
⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} |
9 | | ballotth.mgtn |
. . . . . . . . . 10
⊢ 𝑁 < 𝑀 |
10 | | ballotth.i |
. . . . . . . . . 10
⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) |
11 | 1, 2, 3, 4, 5, 8, 9, 10 | ballotlemiex 32030 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0)) |
12 | 11 | simpld 498 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁))) |
13 | | elfznn 13020 |
. . . . . . . 8
⊢ ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) → (𝐼‘𝐶) ∈ ℕ) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℕ) |
15 | 14 | adantr 484 |
. . . . . 6
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (𝐼‘𝐶) ∈ ℕ) |
16 | 1, 2, 3, 4, 5, 8, 9, 10 | ballotlemii 32032 |
. . . . . 6
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (𝐼‘𝐶) ≠ 1) |
17 | | eluz2b3 12397 |
. . . . . 6
⊢ ((𝐼‘𝐶) ∈ (ℤ≥‘2)
↔ ((𝐼‘𝐶) ∈ ℕ ∧ (𝐼‘𝐶) ≠ 1)) |
18 | 15, 16, 17 | sylanbrc 586 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (𝐼‘𝐶) ∈
(ℤ≥‘2)) |
19 | | uz2m1nn 12398 |
. . . . 5
⊢ ((𝐼‘𝐶) ∈ (ℤ≥‘2)
→ ((𝐼‘𝐶) − 1) ∈
ℕ) |
20 | 18, 19 | syl 17 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → ((𝐼‘𝐶) − 1) ∈
ℕ) |
21 | 20 | adantr 484 |
. . 3
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐼‘𝐶) − 1) ∈
ℕ) |
22 | | elnnuz 12357 |
. . . . . . 7
⊢ (((𝐼‘𝐶) − 1) ∈ ℕ ↔ ((𝐼‘𝐶) − 1) ∈
(ℤ≥‘1)) |
23 | 22 | biimpi 219 |
. . . . . 6
⊢ (((𝐼‘𝐶) − 1) ∈ ℕ → ((𝐼‘𝐶) − 1) ∈
(ℤ≥‘1)) |
24 | | eluzfz1 12998 |
. . . . . 6
⊢ (((𝐼‘𝐶) − 1) ∈
(ℤ≥‘1) → 1 ∈ (1...((𝐼‘𝐶) − 1))) |
25 | 20, 23, 24 | 3syl 18 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → 1 ∈ (1...((𝐼‘𝐶) − 1))) |
26 | 25 | adantr 484 |
. . . 4
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → 1 ∈ (1...((𝐼‘𝐶) − 1))) |
27 | | 0le1 11234 |
. . . . . . 7
⊢ 0 ≤
1 |
28 | | 1e0p1 12214 |
. . . . . . 7
⊢ 1 = (0 +
1) |
29 | 27, 28 | breqtri 5052 |
. . . . . 6
⊢ 0 ≤ (0
+ 1) |
30 | | 1nn 11720 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
31 | 30 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → 1 ∈ ℕ) |
32 | 1, 2, 3, 4, 5, 6, 31 | ballotlemfp1 32020 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((¬ 1 ∈ 𝐶 → ((𝐹‘𝐶)‘1) = (((𝐹‘𝐶)‘(1 − 1)) − 1)) ∧ (1
∈ 𝐶 → ((𝐹‘𝐶)‘1) = (((𝐹‘𝐶)‘(1 − 1)) +
1)))) |
33 | 32 | simprd 499 |
. . . . . . . 8
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (1 ∈ 𝐶 → ((𝐹‘𝐶)‘1) = (((𝐹‘𝐶)‘(1 − 1)) +
1))) |
34 | 33 | imp 410 |
. . . . . . 7
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → ((𝐹‘𝐶)‘1) = (((𝐹‘𝐶)‘(1 − 1)) +
1)) |
35 | | 1m1e0 11781 |
. . . . . . . . . 10
⊢ (1
− 1) = 0 |
36 | 35 | fveq2i 6671 |
. . . . . . . . 9
⊢ ((𝐹‘𝐶)‘(1 − 1)) = ((𝐹‘𝐶)‘0) |
37 | 36 | oveq1i 7174 |
. . . . . . . 8
⊢ (((𝐹‘𝐶)‘(1 − 1)) + 1) = (((𝐹‘𝐶)‘0) + 1) |
38 | 37 | a1i 11 |
. . . . . . 7
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (((𝐹‘𝐶)‘(1 − 1)) + 1) = (((𝐹‘𝐶)‘0) + 1)) |
39 | 1, 2, 3, 4, 5 | ballotlemfval0 32024 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘0) = 0) |
40 | 6, 39 | syl 17 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐹‘𝐶)‘0) = 0) |
41 | 40 | adantr 484 |
. . . . . . . 8
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → ((𝐹‘𝐶)‘0) = 0) |
42 | 41 | oveq1d 7179 |
. . . . . . 7
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (((𝐹‘𝐶)‘0) + 1) = (0 + 1)) |
43 | 34, 38, 42 | 3eqtrrd 2778 |
. . . . . 6
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (0 + 1) = ((𝐹‘𝐶)‘1)) |
44 | 29, 43 | breqtrid 5064 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → 0 ≤ ((𝐹‘𝐶)‘1)) |
45 | 44 | adantr 484 |
. . . 4
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → 0 ≤ ((𝐹‘𝐶)‘1)) |
46 | | fveq2 6668 |
. . . . . 6
⊢ (𝑖 = 1 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘1)) |
47 | 46 | breq2d 5039 |
. . . . 5
⊢ (𝑖 = 1 → (0 ≤ ((𝐹‘𝐶)‘𝑖) ↔ 0 ≤ ((𝐹‘𝐶)‘1))) |
48 | 47 | rspcev 3524 |
. . . 4
⊢ ((1
∈ (1...((𝐼‘𝐶) − 1)) ∧ 0 ≤
((𝐹‘𝐶)‘1)) → ∃𝑖 ∈ (1...((𝐼‘𝐶) − 1))0 ≤ ((𝐹‘𝐶)‘𝑖)) |
49 | 26, 45, 48 | syl2anc 587 |
. . 3
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → ∃𝑖 ∈ (1...((𝐼‘𝐶) − 1))0 ≤ ((𝐹‘𝐶)‘𝑖)) |
50 | | df-neg 10944 |
. . . . . 6
⊢ -1 = (0
− 1) |
51 | 1, 2, 3, 4, 5, 6, 14 | ballotlemfp1 32020 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((¬ (𝐼‘𝐶) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = (((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) − 1)) ∧ ((𝐼‘𝐶) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = (((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) + 1)))) |
52 | 51 | simprd 499 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ∈ 𝐶 → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = (((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) + 1))) |
53 | 52 | imp 410 |
. . . . . . . 8
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = (((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) + 1)) |
54 | 11 | simprd 499 |
. . . . . . . . 9
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0) |
55 | 54 | adantr 484 |
. . . . . . . 8
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0) |
56 | 53, 55 | eqtr3d 2775 |
. . . . . . 7
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → (((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) + 1) = 0) |
57 | | 0cnd 10705 |
. . . . . . . 8
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → 0 ∈ ℂ) |
58 | | 1cnd 10707 |
. . . . . . . 8
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → 1 ∈ ℂ) |
59 | 6 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → 𝐶 ∈ 𝑂) |
60 | 14 | nnzd 12160 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) ∈ ℤ) |
61 | 60 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → (𝐼‘𝐶) ∈ ℤ) |
62 | | 1zzd 12087 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → 1 ∈ ℤ) |
63 | 61, 62 | zsubcld 12166 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐼‘𝐶) − 1) ∈
ℤ) |
64 | 1, 2, 3, 4, 5, 59,
63 | ballotlemfelz 32019 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) ∈
ℤ) |
65 | 64 | zcnd 12162 |
. . . . . . . 8
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) ∈
ℂ) |
66 | 57, 58, 65 | subadd2d 11087 |
. . . . . . 7
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((0 − 1) = ((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) ↔ (((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) + 1) = 0)) |
67 | 56, 66 | mpbird 260 |
. . . . . 6
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → (0 − 1) = ((𝐹‘𝐶)‘((𝐼‘𝐶) − 1))) |
68 | 50, 67 | syl5eq 2785 |
. . . . 5
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → -1 = ((𝐹‘𝐶)‘((𝐼‘𝐶) − 1))) |
69 | | neg1lt0 11826 |
. . . . 5
⊢ -1 <
0 |
70 | 68, 69 | eqbrtrrdi 5067 |
. . . 4
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) < 0) |
71 | 70 | adantlr 715 |
. . 3
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → ((𝐹‘𝐶)‘((𝐼‘𝐶) − 1)) < 0) |
72 | 1, 2, 3, 4, 5, 7, 21, 49, 71 | ballotlemfcc 32022 |
. 2
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → ∃𝑘 ∈ (1...((𝐼‘𝐶) − 1))((𝐹‘𝐶)‘𝑘) = 0) |
73 | 1, 2, 3, 4, 5, 8, 9, 10 | ballotlemimin 32034 |
. . 3
⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ¬ ∃𝑘 ∈ (1...((𝐼‘𝐶) − 1))((𝐹‘𝐶)‘𝑘) = 0) |
74 | 73 | ad2antrr 726 |
. 2
⊢ (((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) ∧ (𝐼‘𝐶) ∈ 𝐶) → ¬ ∃𝑘 ∈ (1...((𝐼‘𝐶) − 1))((𝐹‘𝐶)‘𝑘) = 0) |
75 | 72, 74 | pm2.65da 817 |
1
⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → ¬ (𝐼‘𝐶) ∈ 𝐶) |