Proof of Theorem ballotlem4
Step | Hyp | Ref
| Expression |
1 | | ballotth.m |
. . . . . . . 8
⊢ 𝑀 ∈ ℕ |
2 | | ballotth.n |
. . . . . . . 8
⊢ 𝑁 ∈ ℕ |
3 | | nnaddcl 11853 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) |
4 | 1, 2, 3 | mp2an 692 |
. . . . . . 7
⊢ (𝑀 + 𝑁) ∈ ℕ |
5 | | elnnuz 12478 |
. . . . . . 7
⊢ ((𝑀 + 𝑁) ∈ ℕ ↔ (𝑀 + 𝑁) ∈
(ℤ≥‘1)) |
6 | 4, 5 | mpbi 233 |
. . . . . 6
⊢ (𝑀 + 𝑁) ∈
(ℤ≥‘1) |
7 | | eluzfz1 13119 |
. . . . . 6
⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘1)
→ 1 ∈ (1...(𝑀 +
𝑁))) |
8 | 6, 7 | ax-mp 5 |
. . . . 5
⊢ 1 ∈
(1...(𝑀 + 𝑁)) |
9 | | 0le1 11355 |
. . . . . . . . . 10
⊢ 0 ≤
1 |
10 | | 0re 10835 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
11 | | 1re 10833 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
12 | 10, 11 | lenlti 10952 |
. . . . . . . . . 10
⊢ (0 ≤ 1
↔ ¬ 1 < 0) |
13 | 9, 12 | mpbi 233 |
. . . . . . . . 9
⊢ ¬ 1
< 0 |
14 | | ltsub13 11313 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (0 < (0
− 1) ↔ 1 < (0 − 0))) |
15 | 10, 10, 11, 14 | mp3an 1463 |
. . . . . . . . . 10
⊢ (0 <
(0 − 1) ↔ 1 < (0 − 0)) |
16 | | 0m0e0 11950 |
. . . . . . . . . . 11
⊢ (0
− 0) = 0 |
17 | 16 | breq2i 5061 |
. . . . . . . . . 10
⊢ (1 <
(0 − 0) ↔ 1 < 0) |
18 | 15, 17 | bitri 278 |
. . . . . . . . 9
⊢ (0 <
(0 − 1) ↔ 1 < 0) |
19 | 13, 18 | mtbir 326 |
. . . . . . . 8
⊢ ¬ 0
< (0 − 1) |
20 | | 1m1e0 11902 |
. . . . . . . . . . . 12
⊢ (1
− 1) = 0 |
21 | 20 | fveq2i 6720 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝐶)‘(1 − 1)) = ((𝐹‘𝐶)‘0) |
22 | | ballotth.o |
. . . . . . . . . . . 12
⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} |
23 | | ballotth.p |
. . . . . . . . . . . 12
⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) |
24 | | ballotth.f |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑐)) −
(♯‘((1...𝑖)
∖ 𝑐))))) |
25 | 1, 2, 22, 23, 24 | ballotlemfval0 32174 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘0) = 0) |
26 | 21, 25 | syl5eq 2790 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘(1 − 1)) = 0) |
27 | 26 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑂 → (((𝐹‘𝐶)‘(1 − 1)) − 1) = (0
− 1)) |
28 | 27 | breq2d 5065 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑂 → (0 < (((𝐹‘𝐶)‘(1 − 1)) − 1) ↔ 0
< (0 − 1))) |
29 | 19, 28 | mtbiri 330 |
. . . . . . 7
⊢ (𝐶 ∈ 𝑂 → ¬ 0 < (((𝐹‘𝐶)‘(1 − 1)) −
1)) |
30 | 29 | adantr 484 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑂 ∧ ¬ 1 ∈ 𝐶) → ¬ 0 < (((𝐹‘𝐶)‘(1 − 1)) −
1)) |
31 | | simpl 486 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ 𝑂 ∧ 1 ∈ (1...(𝑀 + 𝑁))) → 𝐶 ∈ 𝑂) |
32 | | 1nn 11841 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
33 | 32 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ 𝑂 ∧ 1 ∈ (1...(𝑀 + 𝑁))) → 1 ∈
ℕ) |
34 | 1, 2, 22, 23, 24, 31, 33 | ballotlemfp1 32170 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ 𝑂 ∧ 1 ∈ (1...(𝑀 + 𝑁))) → ((¬ 1 ∈ 𝐶 → ((𝐹‘𝐶)‘1) = (((𝐹‘𝐶)‘(1 − 1)) − 1)) ∧ (1
∈ 𝐶 → ((𝐹‘𝐶)‘1) = (((𝐹‘𝐶)‘(1 − 1)) +
1)))) |
35 | 34 | simpld 498 |
. . . . . . . . 9
⊢ ((𝐶 ∈ 𝑂 ∧ 1 ∈ (1...(𝑀 + 𝑁))) → (¬ 1 ∈ 𝐶 → ((𝐹‘𝐶)‘1) = (((𝐹‘𝐶)‘(1 − 1)) −
1))) |
36 | 8, 35 | mpan2 691 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑂 → (¬ 1 ∈ 𝐶 → ((𝐹‘𝐶)‘1) = (((𝐹‘𝐶)‘(1 − 1)) −
1))) |
37 | 36 | imp 410 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑂 ∧ ¬ 1 ∈ 𝐶) → ((𝐹‘𝐶)‘1) = (((𝐹‘𝐶)‘(1 − 1)) −
1)) |
38 | 37 | breq2d 5065 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑂 ∧ ¬ 1 ∈ 𝐶) → (0 < ((𝐹‘𝐶)‘1) ↔ 0 < (((𝐹‘𝐶)‘(1 − 1)) −
1))) |
39 | 30, 38 | mtbird 328 |
. . . . 5
⊢ ((𝐶 ∈ 𝑂 ∧ ¬ 1 ∈ 𝐶) → ¬ 0 < ((𝐹‘𝐶)‘1)) |
40 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑖 = 1 → ((𝐹‘𝐶)‘𝑖) = ((𝐹‘𝐶)‘1)) |
41 | 40 | breq2d 5065 |
. . . . . . 7
⊢ (𝑖 = 1 → (0 < ((𝐹‘𝐶)‘𝑖) ↔ 0 < ((𝐹‘𝐶)‘1))) |
42 | 41 | notbid 321 |
. . . . . 6
⊢ (𝑖 = 1 → (¬ 0 <
((𝐹‘𝐶)‘𝑖) ↔ ¬ 0 < ((𝐹‘𝐶)‘1))) |
43 | 42 | rspcev 3537 |
. . . . 5
⊢ ((1
∈ (1...(𝑀 + 𝑁)) ∧ ¬ 0 < ((𝐹‘𝐶)‘1)) → ∃𝑖 ∈ (1...(𝑀 + 𝑁)) ¬ 0 < ((𝐹‘𝐶)‘𝑖)) |
44 | 8, 39, 43 | sylancr 590 |
. . . 4
⊢ ((𝐶 ∈ 𝑂 ∧ ¬ 1 ∈ 𝐶) → ∃𝑖 ∈ (1...(𝑀 + 𝑁)) ¬ 0 < ((𝐹‘𝐶)‘𝑖)) |
45 | | rexnal 3160 |
. . . 4
⊢
(∃𝑖 ∈
(1...(𝑀 + 𝑁)) ¬ 0 < ((𝐹‘𝐶)‘𝑖) ↔ ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)) |
46 | 44, 45 | sylib 221 |
. . 3
⊢ ((𝐶 ∈ 𝑂 ∧ ¬ 1 ∈ 𝐶) → ¬ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)) |
47 | | ballotth.e |
. . . . 5
⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} |
48 | 1, 2, 22, 23, 24, 47 | ballotleme 32175 |
. . . 4
⊢ (𝐶 ∈ 𝐸 ↔ (𝐶 ∈ 𝑂 ∧ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖))) |
49 | 48 | simprbi 500 |
. . 3
⊢ (𝐶 ∈ 𝐸 → ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)) |
50 | 46, 49 | nsyl 142 |
. 2
⊢ ((𝐶 ∈ 𝑂 ∧ ¬ 1 ∈ 𝐶) → ¬ 𝐶 ∈ 𝐸) |
51 | 50 | ex 416 |
1
⊢ (𝐶 ∈ 𝑂 → (¬ 1 ∈ 𝐶 → ¬ 𝐶 ∈ 𝐸)) |