Proof of Theorem ballotth
| Step | Hyp | Ref
| Expression |
| 1 | | ballotth.e |
. . . . . 6
⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} |
| 2 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} ⊆ 𝑂 |
| 3 | 1, 2 | eqsstri 4030 |
. . . . 5
⊢ 𝐸 ⊆ 𝑂 |
| 4 | | fzfi 14013 |
. . . . . . . . . . 11
⊢
(1...(𝑀 + 𝑁)) ∈ Fin |
| 5 | | pwfi 9357 |
. . . . . . . . . . 11
⊢
((1...(𝑀 + 𝑁)) ∈ Fin ↔ 𝒫
(1...(𝑀 + 𝑁)) ∈ Fin) |
| 6 | 4, 5 | mpbi 230 |
. . . . . . . . . 10
⊢ 𝒫
(1...(𝑀 + 𝑁)) ∈ Fin |
| 7 | | ballotth.o |
. . . . . . . . . . 11
⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} |
| 8 | | ssrab2 4080 |
. . . . . . . . . . 11
⊢ {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} ⊆ 𝒫 (1...(𝑀 + 𝑁)) |
| 9 | 7, 8 | eqsstri 4030 |
. . . . . . . . . 10
⊢ 𝑂 ⊆ 𝒫 (1...(𝑀 + 𝑁)) |
| 10 | | ssfi 9213 |
. . . . . . . . . 10
⊢
((𝒫 (1...(𝑀
+ 𝑁)) ∈ Fin ∧
𝑂 ⊆ 𝒫
(1...(𝑀 + 𝑁))) → 𝑂 ∈ Fin) |
| 11 | 6, 9, 10 | mp2an 692 |
. . . . . . . . 9
⊢ 𝑂 ∈ Fin |
| 12 | | ssfi 9213 |
. . . . . . . . 9
⊢ ((𝑂 ∈ Fin ∧ 𝐸 ⊆ 𝑂) → 𝐸 ∈ Fin) |
| 13 | 11, 3, 12 | mp2an 692 |
. . . . . . . 8
⊢ 𝐸 ∈ Fin |
| 14 | 13 | elexi 3503 |
. . . . . . 7
⊢ 𝐸 ∈ V |
| 15 | 14 | elpw 4604 |
. . . . . 6
⊢ (𝐸 ∈ 𝒫 𝑂 ↔ 𝐸 ⊆ 𝑂) |
| 16 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = 𝐸 → (♯‘𝑥) = (♯‘𝐸)) |
| 17 | 16 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑥 = 𝐸 → ((♯‘𝑥) / (♯‘𝑂)) = ((♯‘𝐸) / (♯‘𝑂))) |
| 18 | | ballotth.p |
. . . . . . 7
⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) |
| 19 | | ovex 7464 |
. . . . . . 7
⊢
((♯‘𝐸) /
(♯‘𝑂)) ∈
V |
| 20 | 17, 18, 19 | fvmpt 7016 |
. . . . . 6
⊢ (𝐸 ∈ 𝒫 𝑂 → (𝑃‘𝐸) = ((♯‘𝐸) / (♯‘𝑂))) |
| 21 | 15, 20 | sylbir 235 |
. . . . 5
⊢ (𝐸 ⊆ 𝑂 → (𝑃‘𝐸) = ((♯‘𝐸) / (♯‘𝑂))) |
| 22 | 3, 21 | ax-mp 5 |
. . . 4
⊢ (𝑃‘𝐸) = ((♯‘𝐸) / (♯‘𝑂)) |
| 23 | | hashssdif 14451 |
. . . . . . . 8
⊢ ((𝑂 ∈ Fin ∧ 𝐸 ⊆ 𝑂) → (♯‘(𝑂 ∖ 𝐸)) = ((♯‘𝑂) − (♯‘𝐸))) |
| 24 | 11, 3, 23 | mp2an 692 |
. . . . . . 7
⊢
(♯‘(𝑂
∖ 𝐸)) =
((♯‘𝑂) −
(♯‘𝐸)) |
| 25 | 24 | eqcomi 2746 |
. . . . . 6
⊢
((♯‘𝑂)
− (♯‘𝐸))
= (♯‘(𝑂 ∖
𝐸)) |
| 26 | | hashcl 14395 |
. . . . . . . . 9
⊢ (𝑂 ∈ Fin →
(♯‘𝑂) ∈
ℕ0) |
| 27 | 11, 26 | ax-mp 5 |
. . . . . . . 8
⊢
(♯‘𝑂)
∈ ℕ0 |
| 28 | 27 | nn0cni 12538 |
. . . . . . 7
⊢
(♯‘𝑂)
∈ ℂ |
| 29 | | hashcl 14395 |
. . . . . . . . 9
⊢ (𝐸 ∈ Fin →
(♯‘𝐸) ∈
ℕ0) |
| 30 | 13, 29 | ax-mp 5 |
. . . . . . . 8
⊢
(♯‘𝐸)
∈ ℕ0 |
| 31 | 30 | nn0cni 12538 |
. . . . . . 7
⊢
(♯‘𝐸)
∈ ℂ |
| 32 | | difss 4136 |
. . . . . . . . . 10
⊢ (𝑂 ∖ 𝐸) ⊆ 𝑂 |
| 33 | | ssfi 9213 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ Fin ∧ (𝑂 ∖ 𝐸) ⊆ 𝑂) → (𝑂 ∖ 𝐸) ∈ Fin) |
| 34 | 11, 32, 33 | mp2an 692 |
. . . . . . . . 9
⊢ (𝑂 ∖ 𝐸) ∈ Fin |
| 35 | | hashcl 14395 |
. . . . . . . . 9
⊢ ((𝑂 ∖ 𝐸) ∈ Fin → (♯‘(𝑂 ∖ 𝐸)) ∈
ℕ0) |
| 36 | 34, 35 | ax-mp 5 |
. . . . . . . 8
⊢
(♯‘(𝑂
∖ 𝐸)) ∈
ℕ0 |
| 37 | 36 | nn0cni 12538 |
. . . . . . 7
⊢
(♯‘(𝑂
∖ 𝐸)) ∈
ℂ |
| 38 | 28, 31, 37 | subsub23i 11599 |
. . . . . 6
⊢
(((♯‘𝑂)
− (♯‘𝐸))
= (♯‘(𝑂 ∖
𝐸)) ↔
((♯‘𝑂) −
(♯‘(𝑂 ∖
𝐸))) = (♯‘𝐸)) |
| 39 | 25, 38 | mpbi 230 |
. . . . 5
⊢
((♯‘𝑂)
− (♯‘(𝑂
∖ 𝐸))) =
(♯‘𝐸) |
| 40 | 39 | oveq1i 7441 |
. . . 4
⊢
(((♯‘𝑂)
− (♯‘(𝑂
∖ 𝐸))) /
(♯‘𝑂)) =
((♯‘𝐸) /
(♯‘𝑂)) |
| 41 | 22, 40 | eqtr4i 2768 |
. . 3
⊢ (𝑃‘𝐸) = (((♯‘𝑂) − (♯‘(𝑂 ∖ 𝐸))) / (♯‘𝑂)) |
| 42 | | ballotth.m |
. . . . . . 7
⊢ 𝑀 ∈ ℕ |
| 43 | | ballotth.n |
. . . . . . 7
⊢ 𝑁 ∈ ℕ |
| 44 | 42, 43, 7 | ballotlem1 34489 |
. . . . . 6
⊢
(♯‘𝑂) =
((𝑀 + 𝑁)C𝑀) |
| 45 | 42 | nnnn0i 12534 |
. . . . . . . . 9
⊢ 𝑀 ∈
ℕ0 |
| 46 | | nnaddcl 12289 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) |
| 47 | 42, 43, 46 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝑀 + 𝑁) ∈ ℕ |
| 48 | 47 | nnnn0i 12534 |
. . . . . . . . 9
⊢ (𝑀 + 𝑁) ∈
ℕ0 |
| 49 | 42 | nnrei 12275 |
. . . . . . . . . 10
⊢ 𝑀 ∈ ℝ |
| 50 | 43 | nnnn0i 12534 |
. . . . . . . . . 10
⊢ 𝑁 ∈
ℕ0 |
| 51 | 49, 50 | nn0addge1i 12574 |
. . . . . . . . 9
⊢ 𝑀 ≤ (𝑀 + 𝑁) |
| 52 | | elfz2nn0 13658 |
. . . . . . . . 9
⊢ (𝑀 ∈ (0...(𝑀 + 𝑁)) ↔ (𝑀 ∈ ℕ0 ∧ (𝑀 + 𝑁) ∈ ℕ0 ∧ 𝑀 ≤ (𝑀 + 𝑁))) |
| 53 | 45, 48, 51, 52 | mpbir3an 1342 |
. . . . . . . 8
⊢ 𝑀 ∈ (0...(𝑀 + 𝑁)) |
| 54 | | bccl2 14362 |
. . . . . . . 8
⊢ (𝑀 ∈ (0...(𝑀 + 𝑁)) → ((𝑀 + 𝑁)C𝑀) ∈ ℕ) |
| 55 | 53, 54 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑀 + 𝑁)C𝑀) ∈ ℕ |
| 56 | 55 | nnne0i 12306 |
. . . . . 6
⊢ ((𝑀 + 𝑁)C𝑀) ≠ 0 |
| 57 | 44, 56 | eqnetri 3011 |
. . . . 5
⊢
(♯‘𝑂)
≠ 0 |
| 58 | 28, 57 | pm3.2i 470 |
. . . 4
⊢
((♯‘𝑂)
∈ ℂ ∧ (♯‘𝑂) ≠ 0) |
| 59 | | divsubdir 11961 |
. . . 4
⊢
(((♯‘𝑂)
∈ ℂ ∧ (♯‘(𝑂 ∖ 𝐸)) ∈ ℂ ∧
((♯‘𝑂) ∈
ℂ ∧ (♯‘𝑂) ≠ 0)) → (((♯‘𝑂) − (♯‘(𝑂 ∖ 𝐸))) / (♯‘𝑂)) = (((♯‘𝑂) / (♯‘𝑂)) − ((♯‘(𝑂 ∖ 𝐸)) / (♯‘𝑂)))) |
| 60 | 28, 37, 58, 59 | mp3an 1463 |
. . 3
⊢
(((♯‘𝑂)
− (♯‘(𝑂
∖ 𝐸))) /
(♯‘𝑂)) =
(((♯‘𝑂) /
(♯‘𝑂)) −
((♯‘(𝑂 ∖
𝐸)) / (♯‘𝑂))) |
| 61 | 28, 57 | dividi 12000 |
. . . 4
⊢
((♯‘𝑂) /
(♯‘𝑂)) =
1 |
| 62 | 61 | oveq1i 7441 |
. . 3
⊢
(((♯‘𝑂)
/ (♯‘𝑂))
− ((♯‘(𝑂
∖ 𝐸)) /
(♯‘𝑂))) = (1
− ((♯‘(𝑂
∖ 𝐸)) /
(♯‘𝑂))) |
| 63 | 41, 60, 62 | 3eqtri 2769 |
. 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 34539 |
. . . . . 6
⊢
(♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) = (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) |
| 70 | 69 | oveq1i 7441 |
. . . . 5
⊢
((♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) = ((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) |
| 71 | 70 | oveq1i 7441 |
. . . 4
⊢
(((♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (♯‘𝑂)) = (((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (♯‘𝑂)) |
| 72 | | rabxm 4390 |
. . . . . . 7
⊢ (𝑂 ∖ 𝐸) = ({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∪ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) |
| 73 | 72 | fveq2i 6909 |
. . . . . 6
⊢
(♯‘(𝑂
∖ 𝐸)) =
(♯‘({𝑐 ∈
(𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∪ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) |
| 74 | | ssrab2 4080 |
. . . . . . . . . 10
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ⊆ (𝑂 ∖ 𝐸) |
| 75 | 74, 32 | sstri 3993 |
. . . . . . . . 9
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ⊆ 𝑂 |
| 76 | 75, 9 | sstri 3993 |
. . . . . . . 8
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ⊆ 𝒫 (1...(𝑀 + 𝑁)) |
| 77 | | ssfi 9213 |
. . . . . . . 8
⊢
((𝒫 (1...(𝑀
+ 𝑁)) ∈ Fin ∧
{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ⊆ 𝒫 (1...(𝑀 + 𝑁))) → {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∈ Fin) |
| 78 | 6, 76, 77 | mp2an 692 |
. . . . . . 7
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∈ Fin |
| 79 | | ssrab2 4080 |
. . . . . . . . . 10
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ (𝑂 ∖ 𝐸) |
| 80 | 79, 32 | sstri 3993 |
. . . . . . . . 9
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂 |
| 81 | 80, 9 | sstri 3993 |
. . . . . . . 8
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ 𝒫 (1...(𝑀 + 𝑁)) |
| 82 | | ssfi 9213 |
. . . . . . . 8
⊢
((𝒫 (1...(𝑀
+ 𝑁)) ∈ Fin ∧
{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ 𝒫 (1...(𝑀 + 𝑁))) → {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ∈ Fin) |
| 83 | 6, 81, 82 | mp2an 692 |
. . . . . . 7
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ∈ Fin |
| 84 | | rabnc 4391 |
. . . . . . 7
⊢ ({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∩ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) = ∅ |
| 85 | | hashun 14421 |
. . . . . . 7
⊢ (({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∈ Fin ∧ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ∈ Fin ∧ ({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∩ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) = ∅) → (♯‘({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∪ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) = ((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}))) |
| 86 | 78, 83, 84, 85 | mp3an 1463 |
. . . . . 6
⊢
(♯‘({𝑐
∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∪ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) = ((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) |
| 87 | 73, 86 | eqtri 2765 |
. . . . 5
⊢
(♯‘(𝑂
∖ 𝐸)) =
((♯‘{𝑐 ∈
(𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) |
| 88 | 87 | oveq1i 7441 |
. . . 4
⊢
((♯‘(𝑂
∖ 𝐸)) /
(♯‘𝑂)) =
(((♯‘{𝑐 ∈
(𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (♯‘𝑂)) |
| 89 | | ssrab2 4080 |
. . . . . . . . 9
⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂 |
| 90 | 11 | elexi 3503 |
. . . . . . . . . 10
⊢ 𝑂 ∈ V |
| 91 | 90 | elpw2 5334 |
. . . . . . . . 9
⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 ↔ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂) |
| 92 | 89, 91 | mpbir 231 |
. . . . . . . 8
⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 |
| 93 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → (♯‘𝑥) = (♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐})) |
| 94 | 93 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → ((♯‘𝑥) / (♯‘𝑂)) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂))) |
| 95 | | ovex 7464 |
. . . . . . . . 9
⊢
((♯‘{𝑐
∈ 𝑂 ∣ ¬ 1
∈ 𝑐}) /
(♯‘𝑂)) ∈
V |
| 96 | 94, 18, 95 | fvmpt 7016 |
. . . . . . . 8
⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 → (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂))) |
| 97 | 92, 96 | ax-mp 5 |
. . . . . . 7
⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) |
| 98 | 42, 43, 7, 18 | ballotlem2 34491 |
. . . . . . 7
⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁)) |
| 99 | | nfrab1 3457 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑐{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} |
| 100 | | nfrab1 3457 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑐{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} |
| 101 | 99, 100 | dfssf 3974 |
. . . . . . . . . . 11
⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ↔ ∀𝑐(𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → 𝑐 ∈ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) |
| 102 | 42, 43, 7, 18, 64, 1 | ballotlem4 34501 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ 𝑂 → (¬ 1 ∈ 𝑐 → ¬ 𝑐 ∈ 𝐸)) |
| 103 | 102 | imdistani 568 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐) → (𝑐 ∈ 𝑂 ∧ ¬ 𝑐 ∈ 𝐸)) |
| 104 | | rabid 3458 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ↔ (𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐)) |
| 105 | | eldif 3961 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ (𝑂 ∖ 𝐸) ↔ (𝑐 ∈ 𝑂 ∧ ¬ 𝑐 ∈ 𝐸)) |
| 106 | 103, 104,
105 | 3imtr4i 292 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → 𝑐 ∈ (𝑂 ∖ 𝐸)) |
| 107 | 104 | simprbi 496 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → ¬ 1 ∈ 𝑐) |
| 108 | | rabid 3458 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ↔ (𝑐 ∈ (𝑂 ∖ 𝐸) ∧ ¬ 1 ∈ 𝑐)) |
| 109 | 106, 107,
108 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → 𝑐 ∈ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) |
| 110 | 101, 109 | mpgbir 1799 |
. . . . . . . . . 10
⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} |
| 111 | | rabss2 4078 |
. . . . . . . . . . 11
⊢ ((𝑂 ∖ 𝐸) ⊆ 𝑂 → {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) |
| 112 | 32, 111 | ax-mp 5 |
. . . . . . . . . 10
⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ⊆ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} |
| 113 | 110, 112 | eqssi 4000 |
. . . . . . . . 9
⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} = {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} |
| 114 | 113 | fveq2i 6909 |
. . . . . . . 8
⊢
(♯‘{𝑐
∈ 𝑂 ∣ ¬ 1
∈ 𝑐}) =
(♯‘{𝑐 ∈
(𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) |
| 115 | 114 | oveq1i 7441 |
. . . . . . 7
⊢
((♯‘{𝑐
∈ 𝑂 ∣ ¬ 1
∈ 𝑐}) /
(♯‘𝑂)) =
((♯‘{𝑐 ∈
(𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) |
| 116 | 97, 98, 115 | 3eqtr3i 2773 |
. . . . . 6
⊢ (𝑁 / (𝑀 + 𝑁)) = ((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) |
| 117 | 116 | oveq2i 7442 |
. . . . 5
⊢ (2
· (𝑁 / (𝑀 + 𝑁))) = (2 · ((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂))) |
| 118 | | 2cn 12341 |
. . . . . 6
⊢ 2 ∈
ℂ |
| 119 | | hashcl 14395 |
. . . . . . . 8
⊢ ({𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ∈ Fin → (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) ∈
ℕ0) |
| 120 | 83, 119 | ax-mp 5 |
. . . . . . 7
⊢
(♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) ∈
ℕ0 |
| 121 | 120 | nn0cni 12538 |
. . . . . 6
⊢
(♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) ∈
ℂ |
| 122 | 118, 121,
28, 57 | divassi 12023 |
. . . . 5
⊢ ((2
· (♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (♯‘𝑂)) = (2 ·
((♯‘{𝑐 ∈
(𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂))) |
| 123 | 121 | 2timesi 12404 |
. . . . . 6
⊢ (2
· (♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) = ((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) |
| 124 | 123 | oveq1i 7441 |
. . . . 5
⊢ ((2
· (♯‘{𝑐
∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (♯‘𝑂)) = (((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (♯‘𝑂)) |
| 125 | 117, 122,
124 | 3eqtr2i 2771 |
. . . 4
⊢ (2
· (𝑁 / (𝑀 + 𝑁))) = (((♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐}) + (♯‘{𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐})) / (♯‘𝑂)) |
| 126 | 71, 88, 125 | 3eqtr4ri 2776 |
. . 3
⊢ (2
· (𝑁 / (𝑀 + 𝑁))) = ((♯‘(𝑂 ∖ 𝐸)) / (♯‘𝑂)) |
| 127 | 126 | oveq2i 7442 |
. 2
⊢ (1
− (2 · (𝑁 /
(𝑀 + 𝑁)))) = (1 − ((♯‘(𝑂 ∖ 𝐸)) / (♯‘𝑂))) |
| 128 | 47 | nncni 12276 |
. . . 4
⊢ (𝑀 + 𝑁) ∈ ℂ |
| 129 | 43 | nncni 12276 |
. . . . 5
⊢ 𝑁 ∈ ℂ |
| 130 | 118, 129 | mulcli 11268 |
. . . 4
⊢ (2
· 𝑁) ∈
ℂ |
| 131 | 47 | nnne0i 12306 |
. . . . 5
⊢ (𝑀 + 𝑁) ≠ 0 |
| 132 | 128, 131 | pm3.2i 470 |
. . . 4
⊢ ((𝑀 + 𝑁) ∈ ℂ ∧ (𝑀 + 𝑁) ≠ 0) |
| 133 | | divsubdir 11961 |
. . . 4
⊢ (((𝑀 + 𝑁) ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ ((𝑀 + 𝑁) ∈ ℂ ∧ (𝑀 + 𝑁) ≠ 0)) → (((𝑀 + 𝑁) − (2 · 𝑁)) / (𝑀 + 𝑁)) = (((𝑀 + 𝑁) / (𝑀 + 𝑁)) − ((2 · 𝑁) / (𝑀 + 𝑁)))) |
| 134 | 128, 130,
132, 133 | mp3an 1463 |
. . 3
⊢ (((𝑀 + 𝑁) − (2 · 𝑁)) / (𝑀 + 𝑁)) = (((𝑀 + 𝑁) / (𝑀 + 𝑁)) − ((2 · 𝑁) / (𝑀 + 𝑁))) |
| 135 | 129 | 2timesi 12404 |
. . . . . 6
⊢ (2
· 𝑁) = (𝑁 + 𝑁) |
| 136 | 135 | oveq2i 7442 |
. . . . 5
⊢ ((𝑀 + 𝑁) − (2 · 𝑁)) = ((𝑀 + 𝑁) − (𝑁 + 𝑁)) |
| 137 | 42 | nncni 12276 |
. . . . . . 7
⊢ 𝑀 ∈ ℂ |
| 138 | 137, 129,
129, 129 | addsub4i 11605 |
. . . . . 6
⊢ ((𝑀 + 𝑁) − (𝑁 + 𝑁)) = ((𝑀 − 𝑁) + (𝑁 − 𝑁)) |
| 139 | 129 | subidi 11580 |
. . . . . . 7
⊢ (𝑁 − 𝑁) = 0 |
| 140 | 139 | oveq2i 7442 |
. . . . . 6
⊢ ((𝑀 − 𝑁) + (𝑁 − 𝑁)) = ((𝑀 − 𝑁) + 0) |
| 141 | 137, 129 | subcli 11585 |
. . . . . . 7
⊢ (𝑀 − 𝑁) ∈ ℂ |
| 142 | 141 | addridi 11448 |
. . . . . 6
⊢ ((𝑀 − 𝑁) + 0) = (𝑀 − 𝑁) |
| 143 | 138, 140,
142 | 3eqtri 2769 |
. . . . 5
⊢ ((𝑀 + 𝑁) − (𝑁 + 𝑁)) = (𝑀 − 𝑁) |
| 144 | 136, 143 | eqtri 2765 |
. . . 4
⊢ ((𝑀 + 𝑁) − (2 · 𝑁)) = (𝑀 − 𝑁) |
| 145 | 144 | oveq1i 7441 |
. . 3
⊢ (((𝑀 + 𝑁) − (2 · 𝑁)) / (𝑀 + 𝑁)) = ((𝑀 − 𝑁) / (𝑀 + 𝑁)) |
| 146 | 128, 131 | dividi 12000 |
. . . 4
⊢ ((𝑀 + 𝑁) / (𝑀 + 𝑁)) = 1 |
| 147 | 118, 129,
128, 131 | divassi 12023 |
. . . 4
⊢ ((2
· 𝑁) / (𝑀 + 𝑁)) = (2 · (𝑁 / (𝑀 + 𝑁))) |
| 148 | 146, 147 | oveq12i 7443 |
. . 3
⊢ (((𝑀 + 𝑁) / (𝑀 + 𝑁)) − ((2 · 𝑁) / (𝑀 + 𝑁))) = (1 − (2 · (𝑁 / (𝑀 + 𝑁)))) |
| 149 | 134, 145,
148 | 3eqtr3ri 2774 |
. 2
⊢ (1
− (2 · (𝑁 /
(𝑀 + 𝑁)))) = ((𝑀 − 𝑁) / (𝑀 + 𝑁)) |
| 150 | 63, 127, 149 | 3eqtr2i 2771 |
1
⊢ (𝑃‘𝐸) = ((𝑀 − 𝑁) / (𝑀 + 𝑁)) |