Step | Hyp | Ref
| Expression |
1 | | ssrab2 3687 |
. . . . 5
⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂 |
2 | | ballotth.m |
. . . . . . 7
⊢ 𝑀 ∈ ℕ |
3 | | ballotth.n |
. . . . . . 7
⊢ 𝑁 ∈ ℕ |
4 | | ballotth.o |
. . . . . . 7
⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} |
5 | 2, 3, 4 | ballotlemoex 30547 |
. . . . . 6
⊢ 𝑂 ∈ V |
6 | 5 | elpw2 4828 |
. . . . 5
⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 ↔ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂) |
7 | 1, 6 | mpbir 221 |
. . . 4
⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 |
8 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → (#‘𝑥) = (#‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐})) |
9 | 8 | oveq1d 6665 |
. . . . 5
⊢ (𝑥 = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} → ((#‘𝑥) / (#‘𝑂)) = ((#‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂))) |
10 | | ballotth.p |
. . . . 5
⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂))) |
11 | | ovex 6678 |
. . . . 5
⊢
((#‘{𝑐 ∈
𝑂 ∣ ¬ 1 ∈
𝑐}) / (#‘𝑂)) ∈ V |
12 | 9, 10, 11 | fvmpt 6282 |
. . . 4
⊢ ({𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 → (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((#‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂))) |
13 | 7, 12 | ax-mp 5 |
. . 3
⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((#‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)) |
14 | | an32 839 |
. . . . . . . . 9
⊢ (((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (#‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐)) |
15 | | 2eluzge1 11734 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
(ℤ≥‘1) |
16 | | fzss1 12380 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
(ℤ≥‘1) → (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁))) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁)) |
18 | | sspwb 4917 |
. . . . . . . . . . . . . 14
⊢
((2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁)) ↔ 𝒫 (2...(𝑀 + 𝑁)) ⊆ 𝒫 (1...(𝑀 + 𝑁))) |
19 | 17, 18 | mpbi 220 |
. . . . . . . . . . . . 13
⊢ 𝒫
(2...(𝑀 + 𝑁)) ⊆ 𝒫 (1...(𝑀 + 𝑁)) |
20 | 19 | sseli 3599 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → 𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁))) |
21 | | 1lt2 11194 |
. . . . . . . . . . . . . . . . 17
⊢ 1 <
2 |
22 | | 1re 10039 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
23 | | 2re 11090 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
24 | 22, 23 | ltnlei 10158 |
. . . . . . . . . . . . . . . . 17
⊢ (1 < 2
↔ ¬ 2 ≤ 1) |
25 | 21, 24 | mpbi 220 |
. . . . . . . . . . . . . . . 16
⊢ ¬ 2
≤ 1 |
26 | | elfzle1 12344 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
(2...(𝑀 + 𝑁)) → 2 ≤ 1) |
27 | 25, 26 | mto 188 |
. . . . . . . . . . . . . . 15
⊢ ¬ 1
∈ (2...(𝑀 + 𝑁)) |
28 | | elelpwi 4171 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) → 1 ∈ (2...(𝑀 + 𝑁))) |
29 | 27, 28 | mto 188 |
. . . . . . . . . . . . . 14
⊢ ¬ (1
∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) |
30 | | ancom 466 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ 𝑐 ∧ 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) ↔ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐)) |
31 | 29, 30 | mtbi 312 |
. . . . . . . . . . . . 13
⊢ ¬
(𝑐 ∈ 𝒫
(2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐) |
32 | 31 | imnani 439 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → ¬ 1 ∈ 𝑐) |
33 | 20, 32 | jca 554 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐)) |
34 | | ssin 3835 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) ↔ 𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})) |
35 | | 1le2 11241 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ≤
2 |
36 | | 1p1e2 11134 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 + 1) =
2 |
37 | | nnge1 11046 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ ℕ → 1 ≤
𝑀) |
38 | 2, 37 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ≤
𝑀 |
39 | | nnge1 11046 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 1 ≤
𝑁) |
40 | 3, 39 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ≤
𝑁 |
41 | 2 | nnrei 11029 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑀 ∈ ℝ |
42 | 3 | nnrei 11029 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑁 ∈ ℝ |
43 | 22, 22, 41, 42 | le2addi 10591 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((1 ≤
𝑀 ∧ 1 ≤ 𝑁) → (1 + 1) ≤ (𝑀 + 𝑁)) |
44 | 38, 40, 43 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 + 1)
≤ (𝑀 + 𝑁) |
45 | 36, 44 | eqbrtrri 4676 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ≤
(𝑀 + 𝑁) |
46 | 41, 42 | readdcli 10053 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 + 𝑁) ∈ ℝ |
47 | 22, 23, 46 | letri 10166 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1 ≤
2 ∧ 2 ≤ (𝑀 + 𝑁)) → 1 ≤ (𝑀 + 𝑁)) |
48 | 35, 45, 47 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ≤
(𝑀 + 𝑁) |
49 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℤ |
50 | | nnaddcl 11042 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) |
51 | 2, 3, 50 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 + 𝑁) ∈ ℕ |
52 | 51 | nnzi 11401 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 + 𝑁) ∈ ℤ |
53 | | eluz 11701 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℤ ∧ (𝑀 +
𝑁) ∈ ℤ) →
((𝑀 + 𝑁) ∈ (ℤ≥‘1)
↔ 1 ≤ (𝑀 + 𝑁))) |
54 | 49, 52, 53 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘1)
↔ 1 ≤ (𝑀 + 𝑁)) |
55 | 48, 54 | mpbir 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 + 𝑁) ∈
(ℤ≥‘1) |
56 | | elfzp12 12419 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘1)
→ (𝑖 ∈
(1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))) |
58 | 57 | biimpi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...(𝑀 + 𝑁)) → (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))) |
59 | 58 | orcanai 952 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))) |
60 | 36 | oveq1i 6660 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 +
1)...(𝑀 + 𝑁)) = (2...(𝑀 + 𝑁)) |
61 | 59, 60 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ (2...(𝑀 + 𝑁))) |
62 | 61 | ss2abi 3674 |
. . . . . . . . . . . . . . 15
⊢ {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} ⊆ {𝑖 ∣ 𝑖 ∈ (2...(𝑀 + 𝑁))} |
63 | | inab 3895 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} |
64 | | abid2 2745 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} = (1...(𝑀 + 𝑁)) |
65 | 64 | ineq1i 3810 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑖 ∣ 𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) |
66 | 63, 65 | eqtr3i 2646 |
. . . . . . . . . . . . . . 15
⊢ {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) |
67 | | abid2 2745 |
. . . . . . . . . . . . . . 15
⊢ {𝑖 ∣ 𝑖 ∈ (2...(𝑀 + 𝑁))} = (2...(𝑀 + 𝑁)) |
68 | 62, 66, 67 | 3sstr3i 3643 |
. . . . . . . . . . . . . 14
⊢
((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁)) |
69 | | sstr 3611 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ∧ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))) → 𝑐 ⊆ (2...(𝑀 + 𝑁))) |
70 | 68, 69 | mpan2 707 |
. . . . . . . . . . . . 13
⊢ (𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁))) |
71 | 34, 70 | sylbi 207 |
. . . . . . . . . . . 12
⊢ ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁))) |
72 | | selpw 4165 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (1...(𝑀 + 𝑁))) |
73 | | ssab 3672 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1} ↔ ∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1)) |
74 | | df-ex 1705 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐)) |
75 | 74 | bicomi 214 |
. . . . . . . . . . . . . . . 16
⊢ (¬
∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐)) |
76 | 75 | con1bii 346 |
. . . . . . . . . . . . . . 15
⊢ (¬
∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐)) |
77 | | df-clel 2618 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
𝑐 ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐)) |
78 | 77 | notbii 310 |
. . . . . . . . . . . . . . 15
⊢ (¬ 1
∈ 𝑐 ↔ ¬
∃𝑖(𝑖 = 1 ∧ 𝑖 ∈ 𝑐)) |
79 | | imnang 1769 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1)) |
80 | | ancom 466 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1)) |
81 | 80 | notbii 310 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1)) |
82 | 81 | albii 1747 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑖 ¬
(𝑖 = 1 ∧ 𝑖 ∈ 𝑐) ↔ ∀𝑖 ¬ (𝑖 ∈ 𝑐 ∧ 𝑖 = 1)) |
83 | 79, 82 | bitr4i 267 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖 ∈ 𝑐)) |
84 | 76, 78, 83 | 3bitr4ri 293 |
. . . . . . . . . . . . . 14
⊢
(∀𝑖(𝑖 ∈ 𝑐 → ¬ 𝑖 = 1) ↔ ¬ 1 ∈ 𝑐) |
85 | 73, 84 | bitr2i 265 |
. . . . . . . . . . . . 13
⊢ (¬ 1
∈ 𝑐 ↔ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) |
86 | 72, 85 | anbi12i 733 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ↔ (𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1})) |
87 | | selpw 4165 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (2...(𝑀 + 𝑁))) |
88 | 71, 86, 87 | 3imtr4i 281 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) → 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) |
89 | 33, 88 | impbii 199 |
. . . . . . . . . 10
⊢ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐)) |
90 | 89 | anbi1i 731 |
. . . . . . . . 9
⊢ ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (#‘𝑐) = 𝑀)) |
91 | 4 | rabeq2i 3197 |
. . . . . . . . . 10
⊢ (𝑐 ∈ 𝑂 ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀)) |
92 | 91 | anbi1i 731 |
. . . . . . . . 9
⊢ ((𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐)) |
93 | 14, 90, 92 | 3bitr4i 292 |
. . . . . . . 8
⊢ ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀) ↔ (𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐)) |
94 | 93 | abbii 2739 |
. . . . . . 7
⊢ {𝑐 ∣ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀)} = {𝑐 ∣ (𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐)} |
95 | | df-rab 2921 |
. . . . . . 7
⊢ {𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} = {𝑐 ∣ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀)} |
96 | | df-rab 2921 |
. . . . . . 7
⊢ {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} = {𝑐 ∣ (𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐)} |
97 | 94, 95, 96 | 3eqtr4i 2654 |
. . . . . 6
⊢ {𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} = {𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐} |
98 | 97 | fveq2i 6194 |
. . . . 5
⊢
(#‘{𝑐 ∈
𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}) = (#‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) |
99 | | fzfi 12771 |
. . . . . . 7
⊢
(2...(𝑀 + 𝑁)) ∈ Fin |
100 | 2 | nnzi 11401 |
. . . . . . 7
⊢ 𝑀 ∈ ℤ |
101 | | hashbc 13237 |
. . . . . . 7
⊢
(((2...(𝑀 + 𝑁)) ∈ Fin ∧ 𝑀 ∈ ℤ) →
((#‘(2...(𝑀 + 𝑁)))C𝑀) = (#‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀})) |
102 | 99, 100, 101 | mp2an 708 |
. . . . . 6
⊢
((#‘(2...(𝑀 +
𝑁)))C𝑀) = (#‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}) |
103 | | 2z 11409 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
104 | 103 | eluz1i 11695 |
. . . . . . . . . . 11
⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘2)
↔ ((𝑀 + 𝑁) ∈ ℤ ∧ 2 ≤
(𝑀 + 𝑁))) |
105 | 52, 45, 104 | mpbir2an 955 |
. . . . . . . . . 10
⊢ (𝑀 + 𝑁) ∈
(ℤ≥‘2) |
106 | | hashfz 13214 |
. . . . . . . . . 10
⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘2)
→ (#‘(2...(𝑀 +
𝑁))) = (((𝑀 + 𝑁) − 2) + 1)) |
107 | 105, 106 | ax-mp 5 |
. . . . . . . . 9
⊢
(#‘(2...(𝑀 +
𝑁))) = (((𝑀 + 𝑁) − 2) + 1) |
108 | 2 | nncni 11030 |
. . . . . . . . . . 11
⊢ 𝑀 ∈ ℂ |
109 | 3 | nncni 11030 |
. . . . . . . . . . 11
⊢ 𝑁 ∈ ℂ |
110 | 108, 109 | addcli 10044 |
. . . . . . . . . 10
⊢ (𝑀 + 𝑁) ∈ ℂ |
111 | | 2cn 11091 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
112 | | ax-1cn 9994 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
113 | | subadd23 10293 |
. . . . . . . . . 10
⊢ (((𝑀 + 𝑁) ∈ ℂ ∧ 2 ∈ ℂ
∧ 1 ∈ ℂ) → (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2))) |
114 | 110, 111,
112, 113 | mp3an 1424 |
. . . . . . . . 9
⊢ (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2)) |
115 | 111, 112 | negsubdi2i 10367 |
. . . . . . . . . . 11
⊢ -(2
− 1) = (1 − 2) |
116 | | 2m1e1 11135 |
. . . . . . . . . . . 12
⊢ (2
− 1) = 1 |
117 | 116 | negeqi 10274 |
. . . . . . . . . . 11
⊢ -(2
− 1) = -1 |
118 | 115, 117 | eqtr3i 2646 |
. . . . . . . . . 10
⊢ (1
− 2) = -1 |
119 | 118 | oveq2i 6661 |
. . . . . . . . 9
⊢ ((𝑀 + 𝑁) + (1 − 2)) = ((𝑀 + 𝑁) + -1) |
120 | 107, 114,
119 | 3eqtri 2648 |
. . . . . . . 8
⊢
(#‘(2...(𝑀 +
𝑁))) = ((𝑀 + 𝑁) + -1) |
121 | 110, 112 | negsubi 10359 |
. . . . . . . 8
⊢ ((𝑀 + 𝑁) + -1) = ((𝑀 + 𝑁) − 1) |
122 | 120, 121 | eqtri 2644 |
. . . . . . 7
⊢
(#‘(2...(𝑀 +
𝑁))) = ((𝑀 + 𝑁) − 1) |
123 | 122 | oveq1i 6660 |
. . . . . 6
⊢
((#‘(2...(𝑀 +
𝑁)))C𝑀) = (((𝑀 + 𝑁) − 1)C𝑀) |
124 | 102, 123 | eqtr3i 2646 |
. . . . 5
⊢
(#‘{𝑐 ∈
𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}) = (((𝑀 + 𝑁) − 1)C𝑀) |
125 | 98, 124 | eqtr3i 2646 |
. . . 4
⊢
(#‘{𝑐 ∈
𝑂 ∣ ¬ 1 ∈
𝑐}) = (((𝑀 + 𝑁) − 1)C𝑀) |
126 | 2, 3, 4 | ballotlem1 30548 |
. . . 4
⊢
(#‘𝑂) =
((𝑀 + 𝑁)C𝑀) |
127 | 125, 126 | oveq12i 6662 |
. . 3
⊢
((#‘{𝑐 ∈
𝑂 ∣ ¬ 1 ∈
𝑐}) / (#‘𝑂)) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) |
128 | 13, 127 | eqtri 2644 |
. 2
⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) |
129 | | 0le1 10551 |
. . . . 5
⊢ 0 ≤
1 |
130 | | 0re 10040 |
. . . . . 6
⊢ 0 ∈
ℝ |
131 | 130, 22, 41 | letri 10166 |
. . . . 5
⊢ ((0 ≤
1 ∧ 1 ≤ 𝑀) → 0
≤ 𝑀) |
132 | 129, 38, 131 | mp2an 708 |
. . . 4
⊢ 0 ≤
𝑀 |
133 | 3 | nngt0i 11054 |
. . . . . 6
⊢ 0 <
𝑁 |
134 | 42, 133 | elrpii 11835 |
. . . . 5
⊢ 𝑁 ∈
ℝ+ |
135 | | ltaddrp 11867 |
. . . . 5
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ 𝑀 < (𝑀 + 𝑁)) |
136 | 41, 134, 135 | mp2an 708 |
. . . 4
⊢ 𝑀 < (𝑀 + 𝑁) |
137 | | 0z 11388 |
. . . . 5
⊢ 0 ∈
ℤ |
138 | | elfzm11 12411 |
. . . . 5
⊢ ((0
∈ ℤ ∧ (𝑀 +
𝑁) ∈ ℤ) →
(𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < (𝑀 + 𝑁)))) |
139 | 137, 52, 138 | mp2an 708 |
. . . 4
⊢ (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ∧ 𝑀 < (𝑀 + 𝑁))) |
140 | 100, 132,
136, 139 | mpbir3an 1244 |
. . 3
⊢ 𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) |
141 | | bcm1n 29554 |
. . 3
⊢ ((𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ∧ (𝑀 + 𝑁) ∈ ℕ) → ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁))) |
142 | 140, 51, 141 | mp2an 708 |
. 2
⊢ ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)) |
143 | | pncan2 10288 |
. . . 4
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑀 + 𝑁) − 𝑀) = 𝑁) |
144 | 108, 109,
143 | mp2an 708 |
. . 3
⊢ ((𝑀 + 𝑁) − 𝑀) = 𝑁 |
145 | 144 | oveq1i 6660 |
. 2
⊢ (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)) = (𝑁 / (𝑀 + 𝑁)) |
146 | 128, 142,
145 | 3eqtri 2648 |
1
⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁)) |