Proof of Theorem ballotth
Step | Hyp | Ref
| Expression |
1 | | ballotth.e |
. . . . . 6
⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} |
2 | | ssrab2 4013 |
. . . . . 6
⊢ {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} ⊆ 𝑂 |
3 | 1, 2 | eqsstri 3955 |
. . . . 5
⊢ 𝐸 ⊆ 𝑂 |
4 | | fzfi 13692 |
. . . . . . . . . . 11
⊢
(1...(𝑀 + 𝑁)) ∈ Fin |
5 | | pwfi 8961 |
. . . . . . . . . . 11
⊢
((1...(𝑀 + 𝑁)) ∈ Fin ↔ 𝒫
(1...(𝑀 + 𝑁)) ∈ Fin) |
6 | 4, 5 | mpbi 229 |
. . . . . . . . . 10
⊢ 𝒫
(1...(𝑀 + 𝑁)) ∈ Fin |
7 | | ballotth.o |
. . . . . . . . . . 11
⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} |
8 | | ssrab2 4013 |
. . . . . . . . . . 11
⊢ {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} ⊆ 𝒫 (1...(𝑀 + 𝑁)) |
9 | 7, 8 | eqsstri 3955 |
. . . . . . . . . 10
⊢ 𝑂 ⊆ 𝒫 (1...(𝑀 + 𝑁)) |
10 | | ssfi 8956 |
. . . . . . . . . 10
⊢
((𝒫 (1...(𝑀
+ 𝑁)) ∈ Fin ∧
𝑂 ⊆ 𝒫
(1...(𝑀 + 𝑁))) → 𝑂 ∈ Fin) |
11 | 6, 9, 10 | mp2an 689 |
. . . . . . . . 9
⊢ 𝑂 ∈ Fin |
12 | | ssfi 8956 |
. . . . . . . . 9
⊢ ((𝑂 ∈ Fin ∧ 𝐸 ⊆ 𝑂) → 𝐸 ∈ Fin) |
13 | 11, 3, 12 | mp2an 689 |
. . . . . . . 8
⊢ 𝐸 ∈ Fin |
14 | 13 | elexi 3451 |
. . . . . . 7
⊢ 𝐸 ∈ V |
15 | 14 | elpw 4537 |
. . . . . 6
⊢ (𝐸 ∈ 𝒫 𝑂 ↔ 𝐸 ⊆ 𝑂) |
16 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑥 = 𝐸 → (♯‘𝑥) = (♯‘𝐸)) |
17 | 16 | oveq1d 7290 |
. . . . . . 7
⊢ (𝑥 = 𝐸 → ((♯‘𝑥) / (♯‘𝑂)) = ((♯‘𝐸) / (♯‘𝑂))) |
18 | | ballotth.p |
. . . . . . 7
⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) |
19 | | ovex 7308 |
. . . . . . 7
⊢
((♯‘𝐸) /
(♯‘𝑂)) ∈
V |
20 | 17, 18, 19 | fvmpt 6875 |
. . . . . 6
⊢ (𝐸 ∈ 𝒫 𝑂 → (𝑃‘𝐸) = ((♯‘𝐸) / (♯‘𝑂))) |
21 | 15, 20 | sylbir 234 |
. . . . 5
⊢ (𝐸 ⊆ 𝑂 → (𝑃‘𝐸) = ((♯‘𝐸) / (♯‘𝑂))) |
22 | 3, 21 | ax-mp 5 |
. . . 4
⊢ (𝑃‘𝐸) = ((♯‘𝐸) / (♯‘𝑂)) |
23 | | hashssdif 14127 |
. . . . . . . 8
⊢ ((𝑂 ∈ Fin ∧ 𝐸 ⊆ 𝑂) → (♯‘(𝑂 ∖ 𝐸)) = ((♯‘𝑂) − (♯‘𝐸))) |
24 | 11, 3, 23 | mp2an 689 |
. . . . . . 7
⊢
(♯‘(𝑂
∖ 𝐸)) =
((♯‘𝑂) −
(♯‘𝐸)) |
25 | 24 | eqcomi 2747 |
. . . . . 6
⊢
((♯‘𝑂)
− (♯‘𝐸))
= (♯‘(𝑂 ∖
𝐸)) |
26 | | hashcl 14071 |
. . . . . . . . 9
⊢ (𝑂 ∈ Fin →
(♯‘𝑂) ∈
ℕ0) |
27 | 11, 26 | ax-mp 5 |
. . . . . . . 8
⊢
(♯‘𝑂)
∈ ℕ0 |
28 | 27 | nn0cni 12245 |
. . . . . . 7
⊢
(♯‘𝑂)
∈ ℂ |
29 | | hashcl 14071 |
. . . . . . . . 9
⊢ (𝐸 ∈ Fin →
(♯‘𝐸) ∈
ℕ0) |
30 | 13, 29 | ax-mp 5 |
. . . . . . . 8
⊢
(♯‘𝐸)
∈ ℕ0 |
31 | 30 | nn0cni 12245 |
. . . . . . 7
⊢
(♯‘𝐸)
∈ ℂ |
32 | | difss 4066 |
. . . . . . . . . 10
⊢ (𝑂 ∖ 𝐸) ⊆ 𝑂 |
33 | | ssfi 8956 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ Fin ∧ (𝑂 ∖ 𝐸) ⊆ 𝑂) → (𝑂 ∖ 𝐸) ∈ Fin) |
34 | 11, 32, 33 | mp2an 689 |
. . . . . . . . 9
⊢ (𝑂 ∖ 𝐸) ∈ Fin |
35 | | hashcl 14071 |
. . . . . . . . 9
⊢ ((𝑂 ∖ 𝐸) ∈ Fin → (♯‘(𝑂 ∖ 𝐸)) ∈
ℕ0) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . 8
⊢
(♯‘(𝑂
∖ 𝐸)) ∈
ℕ0 |
37 | 36 | nn0cni 12245 |
. . . . . . 7
⊢
(♯‘(𝑂
∖ 𝐸)) ∈
ℂ |
38 | 28, 31, 37 | subsub23i 11311 |
. . . . . 6
⊢
(((♯‘𝑂)
− (♯‘𝐸))
= (♯‘(𝑂 ∖
𝐸)) ↔
((♯‘𝑂) −
(♯‘(𝑂 ∖
𝐸))) = (♯‘𝐸)) |
39 | 25, 38 | mpbi 229 |
. . . . 5
⊢
((♯‘𝑂)
− (♯‘(𝑂
∖ 𝐸))) =
(♯‘𝐸) |
40 | 39 | oveq1i 7285 |
. . . 4
⊢
(((♯‘𝑂)
− (♯‘(𝑂
∖ 𝐸))) /
(♯‘𝑂)) =
((♯‘𝐸) /
(♯‘𝑂)) |
41 | 22, 40 | eqtr4i 2769 |
. . 3
⊢ (𝑃‘𝐸) = (((♯‘𝑂) − (♯‘(𝑂 ∖ 𝐸))) / (♯‘𝑂)) |
42 | | ballotth.m |
. . . . . . 7
⊢ 𝑀 ∈ ℕ |
43 | | ballotth.n |
. . . . . . 7
⊢ 𝑁 ∈ ℕ |
44 | 42, 43, 7 | ballotlem1 32453 |
. . . . . 6
⊢
(♯‘𝑂) =
((𝑀 + 𝑁)C𝑀) |
45 | 42 | nnnn0i 12241 |
. . . . . . . . 9
⊢ 𝑀 ∈
ℕ0 |
46 | | nnaddcl 11996 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) |
47 | 42, 43, 46 | mp2an 689 |
. . . . . . . . . 10
⊢ (𝑀 + 𝑁) ∈ ℕ |
48 | 47 | nnnn0i 12241 |
. . . . . . . . 9
⊢ (𝑀 + 𝑁) ∈
ℕ0 |
49 | 42 | nnrei 11982 |
. . . . . . . . . 10
⊢ 𝑀 ∈ ℝ |
50 | 43 | nnnn0i 12241 |
. . . . . . . . . 10
⊢ 𝑁 ∈
ℕ0 |
51 | 49, 50 | nn0addge1i 12281 |
. . . . . . . . 9
⊢ 𝑀 ≤ (𝑀 + 𝑁) |
52 | | elfz2nn0 13347 |
. . . . . . . . 9
⊢ (𝑀 ∈ (0...(𝑀 + 𝑁)) ↔ (𝑀 ∈ ℕ0 ∧ (𝑀 + 𝑁) ∈ ℕ0 ∧ 𝑀 ≤ (𝑀 + 𝑁))) |
53 | 45, 48, 51, 52 | mpbir3an 1340 |
. . . . . . . 8
⊢ 𝑀 ∈ (0...(𝑀 + 𝑁)) |
54 | | bccl2 14037 |
. . . . . . . 8
⊢ (𝑀 ∈ (0...(𝑀 + 𝑁)) → ((𝑀 + 𝑁)C𝑀) ∈ ℕ) |
55 | 53, 54 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑀 + 𝑁)C𝑀) ∈ ℕ |
56 | 55 | nnne0i 12013 |
. . . . . 6
⊢ ((𝑀 + 𝑁)C𝑀) ≠ 0 |
57 | 44, 56 | eqnetri 3014 |
. . . . 5
⊢
(♯‘𝑂)
≠ 0 |
58 | 28, 57 | pm3.2i 471 |
. . . 4
⊢
((♯‘𝑂)
∈ ℂ ∧ (♯‘𝑂) ≠ 0) |
59 | | divsubdir 11669 |
. . . 4
⊢
(((♯‘𝑂)
∈ ℂ ∧ (♯‘(𝑂 ∖ 𝐸)) ∈ ℂ ∧
((♯‘𝑂) ∈
ℂ ∧ (♯‘𝑂) ≠ 0)) → (((♯‘𝑂) − (♯‘(𝑂 ∖ 𝐸))) / (♯‘𝑂)) = (((♯‘𝑂) / (♯‘𝑂)) − ((♯‘(𝑂 ∖ 𝐸)) / (♯‘𝑂)))) |
60 | 28, 37, 58, 59 | mp3an 1460 |
. . 3
⊢
(((♯‘𝑂)
− (♯‘(𝑂
∖ 𝐸))) /
(♯‘𝑂)) =
(((♯‘𝑂) /
(♯‘𝑂)) −
((♯‘(𝑂 ∖
𝐸)) / (♯‘𝑂))) |
61 | 28, 57 | dividi 11708 |
. . . 4
⊢
((♯‘𝑂) /
(♯‘𝑂)) =
1 |
62 | 61 | oveq1i 7285 |
. . 3
⊢
(((♯‘𝑂)
/ (♯‘𝑂))
− ((♯‘(𝑂
∖ 𝐸)) /
(♯‘𝑂))) = (1
− ((♯‘(𝑂
∖ 𝐸)) /
(♯‘𝑂))) |
63 | 41, 60, 62 | 3eqtri 2770 |
. 2
⊢ (𝑃‘𝐸) = (1 − ((♯‘(𝑂 ∖ 𝐸)) / (♯‘𝑂))) |
64 | | ballotth.f |
. . . . . . 7
⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑐)) −
(♯‘((1...𝑖)
∖ 𝑐))))) |
65 | | ballotth.mgtn |
. . . . . . 7
⊢ 𝑁 < 𝑀 |
66 | | ballotth.i |
. . . . . . 7
⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) |
67 | | ballotth.s |
. . . . . . 7
⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) |
68 | | ballotth.r |
. . . . . . 7
⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐)) |
69 | 42, 43, 7, 18, 64, 1, 65, 66, 67, 68 | ballotlem8 32503 |
. . . . . 6
⊢
(♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) = (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) |
70 | 69 | oveq1i 7285 |
. . . . 5
⊢
((♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) = ((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) |
71 | 70 | oveq1i 7285 |
. . . 4
⊢
(((♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (♯‘𝑂)) = (((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (♯‘𝑂)) |
72 | | rabxm 4320 |
. . . . . . 7
⊢ (𝑂 ∖ 𝐸) = ({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∪ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) |
73 | 72 | fveq2i 6777 |
. . . . . 6
⊢
(♯‘(𝑂
∖ 𝐸)) =
(♯‘({𝑐 ∈
(𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∪ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) |
74 | | ssrab2 4013 |
. . . . . . . . . 10
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ⊆ (𝑂 ∖ 𝐸) |
75 | 74, 32 | sstri 3930 |
. . . . . . . . 9
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ⊆ 𝑂 |
76 | 75, 9 | sstri 3930 |
. . . . . . . 8
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ⊆ 𝒫 (1...(𝑀 + 𝑁)) |
77 | | ssfi 8956 |
. . . . . . . 8
⊢
((𝒫 (1...(𝑀
+ 𝑁)) ∈ Fin ∧
{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ⊆ 𝒫 (1...(𝑀 + 𝑁))) → {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∈ Fin) |
78 | 6, 76, 77 | mp2an 689 |
. . . . . . 7
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∈ Fin |
79 | | ssrab2 4013 |
. . . . . . . . . 10
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ (𝑂 ∖ 𝐸) |
80 | 79, 32 | sstri 3930 |
. . . . . . . . 9
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂 |
81 | 80, 9 | sstri 3930 |
. . . . . . . 8
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ 𝒫 (1...(𝑀 + 𝑁)) |
82 | | ssfi 8956 |
. . . . . . . 8
⊢
((𝒫 (1...(𝑀
+ 𝑁)) ∈ Fin ∧
{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ 𝒫 (1...(𝑀 + 𝑁))) → {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ∈ Fin) |
83 | 6, 81, 82 | mp2an 689 |
. . . . . . 7
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ∈ Fin |
84 | | rabnc 4321 |
. . . . . . 7
⊢ ({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∩ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) = ∅ |
85 | | hashun 14097 |
. . . . . . 7
⊢ (({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∈ Fin ∧ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ∈ Fin ∧ ({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∩ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) = ∅) → (♯‘({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∪ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) = ((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}))) |
86 | 78, 83, 84, 85 | mp3an 1460 |
. . . . . 6
⊢
(♯‘({𝑐
∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∪ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) = ((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) |
87 | 73, 86 | eqtri 2766 |
. . . . 5
⊢
(♯‘(𝑂
∖ 𝐸)) =
((♯‘{𝑐 ∈
(𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) |
88 | 87 | oveq1i 7285 |
. . . 4
⊢
((♯‘(𝑂
∖ 𝐸)) /
(♯‘𝑂)) =
(((♯‘{𝑐 ∈
(𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (♯‘𝑂)) |
89 | | ssrab2 4013 |
. . . . . . . . 9
⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂 |
90 | 11 | elexi 3451 |
. . . . . . . . . 10
⊢ 𝑂 ∈ V |
91 | 90 | elpw2 5269 |
. . . . . . . . 9
⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 ↔ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂) |
92 | 89, 91 | mpbir 230 |
. . . . . . . 8
⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 |
93 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → (♯‘𝑥) = (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐})) |
94 | 93 | oveq1d 7290 |
. . . . . . . . 9
⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → ((♯‘𝑥) / (♯‘𝑂)) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂))) |
95 | | ovex 7308 |
. . . . . . . . 9
⊢
((♯‘{𝑐
∈ 𝑂 ∣ ¬ 1
∈ 𝑐}) /
(♯‘𝑂)) ∈
V |
96 | 94, 18, 95 | fvmpt 6875 |
. . . . . . . 8
⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 → (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂))) |
97 | 92, 96 | ax-mp 5 |
. . . . . . 7
⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) |
98 | 42, 43, 7, 18 | ballotlem2 32455 |
. . . . . . 7
⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁)) |
99 | | nfrab1 3317 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑐{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} |
100 | | nfrab1 3317 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑐{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} |
101 | 99, 100 | dfss2f 3911 |
. . . . . . . . . . 11
⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ↔ ∀𝑐(𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → 𝑐 ∈ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) |
102 | 42, 43, 7, 18, 64, 1 | ballotlem4 32465 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ 𝑂 → (¬ 1 ∈ 𝑐 → ¬ 𝑐 ∈ 𝐸)) |
103 | 102 | imdistani 569 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐) → (𝑐 ∈ 𝑂 ∧ ¬ 𝑐 ∈ 𝐸)) |
104 | | rabid 3310 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ↔ (𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐)) |
105 | | eldif 3897 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ (𝑂 ∖ 𝐸) ↔ (𝑐 ∈ 𝑂 ∧ ¬ 𝑐 ∈ 𝐸)) |
106 | 103, 104,
105 | 3imtr4i 292 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → 𝑐 ∈ (𝑂 ∖ 𝐸)) |
107 | 104 | simprbi 497 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → ¬ 1 ∈ 𝑐) |
108 | | rabid 3310 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ↔ (𝑐 ∈ (𝑂 ∖ 𝐸) ∧ ¬ 1 ∈ 𝑐)) |
109 | 106, 107,
108 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → 𝑐 ∈ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) |
110 | 101, 109 | mpgbir 1802 |
. . . . . . . . . 10
⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} |
111 | | rabss2 4011 |
. . . . . . . . . . 11
⊢ ((𝑂 ∖ 𝐸) ⊆ 𝑂 → {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) |
112 | 32, 111 | ax-mp 5 |
. . . . . . . . . 10
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} |
113 | 110, 112 | eqssi 3937 |
. . . . . . . . 9
⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} = {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} |
114 | 113 | fveq2i 6777 |
. . . . . . . 8
⊢
(♯‘{𝑐
∈ 𝑂 ∣ ¬ 1
∈ 𝑐}) =
(♯‘{𝑐 ∈
(𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) |
115 | 114 | oveq1i 7285 |
. . . . . . 7
⊢
((♯‘{𝑐
∈ 𝑂 ∣ ¬ 1
∈ 𝑐}) /
(♯‘𝑂)) =
((♯‘{𝑐 ∈
(𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) |
116 | 97, 98, 115 | 3eqtr3i 2774 |
. . . . . 6
⊢ (𝑁 / (𝑀 + 𝑁)) = ((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) |
117 | 116 | oveq2i 7286 |
. . . . 5
⊢ (2
· (𝑁 / (𝑀 + 𝑁))) = (2 · ((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂))) |
118 | | 2cn 12048 |
. . . . . 6
⊢ 2 ∈
ℂ |
119 | | hashcl 14071 |
. . . . . . . 8
⊢ ({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ∈ Fin → (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) ∈
ℕ0) |
120 | 83, 119 | ax-mp 5 |
. . . . . . 7
⊢
(♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) ∈
ℕ0 |
121 | 120 | nn0cni 12245 |
. . . . . 6
⊢
(♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) ∈
ℂ |
122 | 118, 121,
28, 57 | divassi 11731 |
. . . . 5
⊢ ((2
· (♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (♯‘𝑂)) = (2 ·
((♯‘{𝑐 ∈
(𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂))) |
123 | 121 | 2timesi 12111 |
. . . . . 6
⊢ (2
· (♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) = ((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) |
124 | 123 | oveq1i 7285 |
. . . . 5
⊢ ((2
· (♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (♯‘𝑂)) = (((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (♯‘𝑂)) |
125 | 117, 122,
124 | 3eqtr2i 2772 |
. . . 4
⊢ (2
· (𝑁 / (𝑀 + 𝑁))) = (((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (♯‘𝑂)) |
126 | 71, 88, 125 | 3eqtr4ri 2777 |
. . 3
⊢ (2
· (𝑁 / (𝑀 + 𝑁))) = ((♯‘(𝑂 ∖ 𝐸)) / (♯‘𝑂)) |
127 | 126 | oveq2i 7286 |
. 2
⊢ (1
− (2 · (𝑁 /
(𝑀 + 𝑁)))) = (1 − ((♯‘(𝑂 ∖ 𝐸)) / (♯‘𝑂))) |
128 | 47 | nncni 11983 |
. . . 4
⊢ (𝑀 + 𝑁) ∈ ℂ |
129 | 43 | nncni 11983 |
. . . . 5
⊢ 𝑁 ∈ ℂ |
130 | 118, 129 | mulcli 10982 |
. . . 4
⊢ (2
· 𝑁) ∈
ℂ |
131 | 47 | nnne0i 12013 |
. . . . 5
⊢ (𝑀 + 𝑁) ≠ 0 |
132 | 128, 131 | pm3.2i 471 |
. . . 4
⊢ ((𝑀 + 𝑁) ∈ ℂ ∧ (𝑀 + 𝑁) ≠ 0) |
133 | | divsubdir 11669 |
. . . 4
⊢ (((𝑀 + 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ ((𝑀 + 𝑁) ∈ ℂ ∧ (𝑀 + 𝑁) ≠ 0)) → (((𝑀 + 𝑁) − (2 · 𝑁)) / (𝑀 + 𝑁)) = (((𝑀 + 𝑁) / (𝑀 + 𝑁)) − ((2 · 𝑁) / (𝑀 + 𝑁)))) |
134 | 128, 130,
132, 133 | mp3an 1460 |
. . 3
⊢ (((𝑀 + 𝑁) − (2 · 𝑁)) / (𝑀 + 𝑁)) = (((𝑀 + 𝑁) / (𝑀 + 𝑁)) − ((2 · 𝑁) / (𝑀 + 𝑁))) |
135 | 129 | 2timesi 12111 |
. . . . . 6
⊢ (2
· 𝑁) = (𝑁 + 𝑁) |
136 | 135 | oveq2i 7286 |
. . . . 5
⊢ ((𝑀 + 𝑁) − (2 · 𝑁)) = ((𝑀 + 𝑁) − (𝑁 + 𝑁)) |
137 | 42 | nncni 11983 |
. . . . . . 7
⊢ 𝑀 ∈ ℂ |
138 | 137, 129,
129, 129 | addsub4i 11317 |
. . . . . 6
⊢ ((𝑀 + 𝑁) − (𝑁 + 𝑁)) = ((𝑀 − 𝑁) + (𝑁 − 𝑁)) |
139 | 129 | subidi 11292 |
. . . . . . 7
⊢ (𝑁 − 𝑁) = 0 |
140 | 139 | oveq2i 7286 |
. . . . . 6
⊢ ((𝑀 − 𝑁) + (𝑁 − 𝑁)) = ((𝑀 − 𝑁) + 0) |
141 | 137, 129 | subcli 11297 |
. . . . . . 7
⊢ (𝑀 − 𝑁) ∈ ℂ |
142 | 141 | addid1i 11162 |
. . . . . 6
⊢ ((𝑀 − 𝑁) + 0) = (𝑀 − 𝑁) |
143 | 138, 140,
142 | 3eqtri 2770 |
. . . . 5
⊢ ((𝑀 + 𝑁) − (𝑁 + 𝑁)) = (𝑀 − 𝑁) |
144 | 136, 143 | eqtri 2766 |
. . . 4
⊢ ((𝑀 + 𝑁) − (2 · 𝑁)) = (𝑀 − 𝑁) |
145 | 144 | oveq1i 7285 |
. . 3
⊢ (((𝑀 + 𝑁) − (2 · 𝑁)) / (𝑀 + 𝑁)) = ((𝑀 − 𝑁) / (𝑀 + 𝑁)) |
146 | 128, 131 | dividi 11708 |
. . . 4
⊢ ((𝑀 + 𝑁) / (𝑀 + 𝑁)) = 1 |
147 | 118, 129,
128, 131 | divassi 11731 |
. . . 4
⊢ ((2
· 𝑁) / (𝑀 + 𝑁)) = (2 · (𝑁 / (𝑀 + 𝑁))) |
148 | 146, 147 | oveq12i 7287 |
. . 3
⊢ (((𝑀 + 𝑁) / (𝑀 + 𝑁)) − ((2 · 𝑁) / (𝑀 + 𝑁))) = (1 − (2 · (𝑁 / (𝑀 + 𝑁)))) |
149 | 134, 145,
148 | 3eqtr3ri 2775 |
. 2
⊢ (1
− (2 · (𝑁 /
(𝑀 + 𝑁)))) = ((𝑀 − 𝑁) / (𝑀 + 𝑁)) |
150 | 63, 127, 149 | 3eqtr2i 2772 |
1
⊢ (𝑃‘𝐸) = ((𝑀 − 𝑁) / (𝑀 + 𝑁)) |