Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ballotlem2 Structured version   Visualization version   GIF version

Theorem ballotlem2 30869
Description: The probability that the first vote picked in a count is a B. (Contributed by Thierry Arnoux, 23-Nov-2016.)
Hypotheses
Ref Expression
ballotth.m 𝑀 ∈ ℕ
ballotth.n 𝑁 ∈ ℕ
ballotth.o 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}
ballotth.p 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))
Assertion
Ref Expression
ballotlem2 (𝑃‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁))
Distinct variable groups:   𝑀,𝑐   𝑁,𝑐   𝑂,𝑐,𝑥
Allowed substitution hints:   𝑃(𝑥,𝑐)   𝑀(𝑥)   𝑁(𝑥)

Proof of Theorem ballotlem2
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 ssrab2 3878 . . . . 5 {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂
2 ballotth.m . . . . . . 7 𝑀 ∈ ℕ
3 ballotth.n . . . . . . 7 𝑁 ∈ ℕ
4 ballotth.o . . . . . . 7 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}
52, 3, 4ballotlemoex 30866 . . . . . 6 𝑂 ∈ V
65elpw2 5014 . . . . 5 ({𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 ↔ {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂)
71, 6mpbir 222 . . . 4 {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂
8 fveq2 6402 . . . . . 6 (𝑥 = {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} → (♯‘𝑥) = (♯‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}))
98oveq1d 6883 . . . . 5 (𝑥 = {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} → ((♯‘𝑥) / (♯‘𝑂)) = ((♯‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)))
10 ballotth.p . . . . 5 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂)))
11 ovex 6900 . . . . 5 ((♯‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) ∈ V
129, 10, 11fvmpt 6497 . . . 4 ({𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 → (𝑃‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)))
137, 12ax-mp 5 . . 3 (𝑃‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((♯‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂))
14 an32 628 . . . . . . . . 9 (((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (♯‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
15 2eluzge1 11946 . . . . . . . . . . . . . . 15 2 ∈ (ℤ‘1)
16 fzss1 12597 . . . . . . . . . . . . . . 15 (2 ∈ (ℤ‘1) → (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁)))
1715, 16ax-mp 5 . . . . . . . . . . . . . 14 (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁))
18 sspwb 5101 . . . . . . . . . . . . . 14 ((2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁)) ↔ 𝒫 (2...(𝑀 + 𝑁)) ⊆ 𝒫 (1...(𝑀 + 𝑁)))
1917, 18mpbi 221 . . . . . . . . . . . . 13 𝒫 (2...(𝑀 + 𝑁)) ⊆ 𝒫 (1...(𝑀 + 𝑁))
2019sseli 3788 . . . . . . . . . . . 12 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → 𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)))
21 1lt2 11464 . . . . . . . . . . . . . . . . 17 1 < 2
22 1re 10319 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
23 2re 11368 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
2422, 23ltnlei 10437 . . . . . . . . . . . . . . . . 17 (1 < 2 ↔ ¬ 2 ≤ 1)
2521, 24mpbi 221 . . . . . . . . . . . . . . . 16 ¬ 2 ≤ 1
26 elfzle1 12561 . . . . . . . . . . . . . . . 16 (1 ∈ (2...(𝑀 + 𝑁)) → 2 ≤ 1)
2725, 26mto 188 . . . . . . . . . . . . . . 15 ¬ 1 ∈ (2...(𝑀 + 𝑁))
28 elelpwi 4358 . . . . . . . . . . . . . . 15 ((1 ∈ 𝑐𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) → 1 ∈ (2...(𝑀 + 𝑁)))
2927, 28mto 188 . . . . . . . . . . . . . 14 ¬ (1 ∈ 𝑐𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)))
30 ancom 450 . . . . . . . . . . . . . 14 ((1 ∈ 𝑐𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) ↔ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐))
3129, 30mtbi 313 . . . . . . . . . . . . 13 ¬ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐)
3231imnani 389 . . . . . . . . . . . 12 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → ¬ 1 ∈ 𝑐)
3320, 32jca 503 . . . . . . . . . . 11 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐))
34 ssin 4025 . . . . . . . . . . . . 13 ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) ↔ 𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}))
35 1le2 11502 . . . . . . . . . . . . . . . . . . . . . 22 1 ≤ 2
36 1p1e2 11411 . . . . . . . . . . . . . . . . . . . . . . 23 (1 + 1) = 2
37 nnge1 11326 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℕ → 1 ≤ 𝑀)
382, 37ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ≤ 𝑀
39 nnge1 11326 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → 1 ≤ 𝑁)
403, 39ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ≤ 𝑁
412nnrei 11308 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 ∈ ℝ
423nnrei 11308 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑁 ∈ ℝ
4322, 22, 41, 42le2addi 10870 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1 ≤ 𝑀 ∧ 1 ≤ 𝑁) → (1 + 1) ≤ (𝑀 + 𝑁))
4438, 40, 43mp2an 675 . . . . . . . . . . . . . . . . . . . . . . 23 (1 + 1) ≤ (𝑀 + 𝑁)
4536, 44eqbrtrri 4860 . . . . . . . . . . . . . . . . . . . . . 22 2 ≤ (𝑀 + 𝑁)
4641, 42readdcli 10334 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 + 𝑁) ∈ ℝ
4722, 23, 46letri 10445 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ≤ 2 ∧ 2 ≤ (𝑀 + 𝑁)) → 1 ≤ (𝑀 + 𝑁))
4835, 45, 47mp2an 675 . . . . . . . . . . . . . . . . . . . . 21 1 ≤ (𝑀 + 𝑁)
49 1z 11667 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℤ
50 nnaddcl 11321 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ)
512, 3, 50mp2an 675 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 + 𝑁) ∈ ℕ
5251nnzi 11661 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 + 𝑁) ∈ ℤ
53 eluz 11912 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → ((𝑀 + 𝑁) ∈ (ℤ‘1) ↔ 1 ≤ (𝑀 + 𝑁)))
5449, 52, 53mp2an 675 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 + 𝑁) ∈ (ℤ‘1) ↔ 1 ≤ (𝑀 + 𝑁))
5548, 54mpbir 222 . . . . . . . . . . . . . . . . . . . 20 (𝑀 + 𝑁) ∈ (ℤ‘1)
56 elfzp12 12636 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 + 𝑁) ∈ (ℤ‘1) → (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))))
5755, 56ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))
5857biimpi 207 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...(𝑀 + 𝑁)) → (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))
5958orcanai 1016 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))
6036oveq1i 6878 . . . . . . . . . . . . . . . . 17 ((1 + 1)...(𝑀 + 𝑁)) = (2...(𝑀 + 𝑁))
6159, 60syl6eleq 2891 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ (2...(𝑀 + 𝑁)))
6261ss2abi 3865 . . . . . . . . . . . . . . 15 {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} ⊆ {𝑖𝑖 ∈ (2...(𝑀 + 𝑁))}
63 inab 4090 . . . . . . . . . . . . . . . 16 ({𝑖𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)}
64 abid2 2925 . . . . . . . . . . . . . . . . 17 {𝑖𝑖 ∈ (1...(𝑀 + 𝑁))} = (1...(𝑀 + 𝑁))
6564ineq1i 4003 . . . . . . . . . . . . . . . 16 ({𝑖𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
6663, 65eqtr3i 2826 . . . . . . . . . . . . . . 15 {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
67 abid2 2925 . . . . . . . . . . . . . . 15 {𝑖𝑖 ∈ (2...(𝑀 + 𝑁))} = (2...(𝑀 + 𝑁))
6862, 66, 673sstr3i 3834 . . . . . . . . . . . . . 14 ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))
69 sstr 3800 . . . . . . . . . . . . . 14 ((𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ∧ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
7068, 69mpan2 674 . . . . . . . . . . . . 13 (𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
7134, 70sylbi 208 . . . . . . . . . . . 12 ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
72 selpw 4352 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (1...(𝑀 + 𝑁)))
73 ssab 3863 . . . . . . . . . . . . . 14 (𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1} ↔ ∀𝑖(𝑖𝑐 → ¬ 𝑖 = 1))
74 df-ex 1860 . . . . . . . . . . . . . . . . 17 (∃𝑖(𝑖 = 1 ∧ 𝑖𝑐) ↔ ¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐))
7574bicomi 215 . . . . . . . . . . . . . . . 16 (¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐) ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖𝑐))
7675con1bii 347 . . . . . . . . . . . . . . 15 (¬ ∃𝑖(𝑖 = 1 ∧ 𝑖𝑐) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐))
77 df-clel 2798 . . . . . . . . . . . . . . . 16 (1 ∈ 𝑐 ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖𝑐))
7877notbii 311 . . . . . . . . . . . . . . 15 (¬ 1 ∈ 𝑐 ↔ ¬ ∃𝑖(𝑖 = 1 ∧ 𝑖𝑐))
79 imnang 1928 . . . . . . . . . . . . . . . 16 (∀𝑖(𝑖𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖𝑐𝑖 = 1))
80 ancom 450 . . . . . . . . . . . . . . . . . 18 ((𝑖 = 1 ∧ 𝑖𝑐) ↔ (𝑖𝑐𝑖 = 1))
8180notbii 311 . . . . . . . . . . . . . . . . 17 (¬ (𝑖 = 1 ∧ 𝑖𝑐) ↔ ¬ (𝑖𝑐𝑖 = 1))
8281albii 1904 . . . . . . . . . . . . . . . 16 (∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐) ↔ ∀𝑖 ¬ (𝑖𝑐𝑖 = 1))
8379, 82bitr4i 269 . . . . . . . . . . . . . . 15 (∀𝑖(𝑖𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐))
8476, 78, 833bitr4ri 295 . . . . . . . . . . . . . 14 (∀𝑖(𝑖𝑐 → ¬ 𝑖 = 1) ↔ ¬ 1 ∈ 𝑐)
8573, 84bitr2i 267 . . . . . . . . . . . . 13 (¬ 1 ∈ 𝑐𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1})
8672, 85anbi12i 614 . . . . . . . . . . . 12 ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ↔ (𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}))
87 selpw 4352 . . . . . . . . . . . 12 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (2...(𝑀 + 𝑁)))
8871, 86, 873imtr4i 283 . . . . . . . . . . 11 ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) → 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)))
8933, 88impbii 200 . . . . . . . . . 10 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐))
9089anbi1i 612 . . . . . . . . 9 ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (♯‘𝑐) = 𝑀))
914rabeq2i 3383 . . . . . . . . . 10 (𝑐𝑂 ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀))
9291anbi1i 612 . . . . . . . . 9 ((𝑐𝑂 ∧ ¬ 1 ∈ 𝑐) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
9314, 90, 923bitr4i 294 . . . . . . . 8 ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀) ↔ (𝑐𝑂 ∧ ¬ 1 ∈ 𝑐))
9493abbii 2919 . . . . . . 7 {𝑐 ∣ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀)} = {𝑐 ∣ (𝑐𝑂 ∧ ¬ 1 ∈ 𝑐)}
95 df-rab 3101 . . . . . . 7 {𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} = {𝑐 ∣ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (♯‘𝑐) = 𝑀)}
96 df-rab 3101 . . . . . . 7 {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} = {𝑐 ∣ (𝑐𝑂 ∧ ¬ 1 ∈ 𝑐)}
9794, 95, 963eqtr4i 2834 . . . . . 6 {𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} = {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}
9897fveq2i 6405 . . . . 5 (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}) = (♯‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐})
99 fzfi 12989 . . . . . . 7 (2...(𝑀 + 𝑁)) ∈ Fin
1002nnzi 11661 . . . . . . 7 𝑀 ∈ ℤ
101 hashbc 13448 . . . . . . 7 (((2...(𝑀 + 𝑁)) ∈ Fin ∧ 𝑀 ∈ ℤ) → ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}))
10299, 100, 101mp2an 675 . . . . . 6 ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀})
103 2z 11669 . . . . . . . . . . . 12 2 ∈ ℤ
104103eluz1i 11906 . . . . . . . . . . 11 ((𝑀 + 𝑁) ∈ (ℤ‘2) ↔ ((𝑀 + 𝑁) ∈ ℤ ∧ 2 ≤ (𝑀 + 𝑁)))
10552, 45, 104mpbir2an 693 . . . . . . . . . 10 (𝑀 + 𝑁) ∈ (ℤ‘2)
106 hashfz 13425 . . . . . . . . . 10 ((𝑀 + 𝑁) ∈ (ℤ‘2) → (♯‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1))
107105, 106ax-mp 5 . . . . . . . . 9 (♯‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1)
1082nncni 11309 . . . . . . . . . . 11 𝑀 ∈ ℂ
1093nncni 11309 . . . . . . . . . . 11 𝑁 ∈ ℂ
110108, 109addcli 10325 . . . . . . . . . 10 (𝑀 + 𝑁) ∈ ℂ
111 2cn 11369 . . . . . . . . . 10 2 ∈ ℂ
112 ax-1cn 10273 . . . . . . . . . 10 1 ∈ ℂ
113 subadd23 10572 . . . . . . . . . 10 (((𝑀 + 𝑁) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2)))
114110, 111, 112, 113mp3an 1578 . . . . . . . . 9 (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2))
115111, 112negsubdi2i 10646 . . . . . . . . . . 11 -(2 − 1) = (1 − 2)
116 2m1e1 11412 . . . . . . . . . . . 12 (2 − 1) = 1
117116negeqi 10553 . . . . . . . . . . 11 -(2 − 1) = -1
118115, 117eqtr3i 2826 . . . . . . . . . 10 (1 − 2) = -1
119118oveq2i 6879 . . . . . . . . 9 ((𝑀 + 𝑁) + (1 − 2)) = ((𝑀 + 𝑁) + -1)
120107, 114, 1193eqtri 2828 . . . . . . . 8 (♯‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) + -1)
121110, 112negsubi 10638 . . . . . . . 8 ((𝑀 + 𝑁) + -1) = ((𝑀 + 𝑁) − 1)
122120, 121eqtri 2824 . . . . . . 7 (♯‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) − 1)
123122oveq1i 6878 . . . . . 6 ((♯‘(2...(𝑀 + 𝑁)))C𝑀) = (((𝑀 + 𝑁) − 1)C𝑀)
124102, 123eqtr3i 2826 . . . . 5 (♯‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀}) = (((𝑀 + 𝑁) − 1)C𝑀)
12598, 124eqtr3i 2826 . . . 4 (♯‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = (((𝑀 + 𝑁) − 1)C𝑀)
1262, 3, 4ballotlem1 30867 . . . 4 (♯‘𝑂) = ((𝑀 + 𝑁)C𝑀)
127125, 126oveq12i 6880 . . 3 ((♯‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (♯‘𝑂)) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
12813, 127eqtri 2824 . 2 (𝑃‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
129 0le1 10830 . . . . 5 0 ≤ 1
130 0re 10321 . . . . . 6 0 ∈ ℝ
131130, 22, 41letri 10445 . . . . 5 ((0 ≤ 1 ∧ 1 ≤ 𝑀) → 0 ≤ 𝑀)
132129, 38, 131mp2an 675 . . . 4 0 ≤ 𝑀
1333nngt0i 11334 . . . . . 6 0 < 𝑁
13442, 133elrpii 12043 . . . . 5 𝑁 ∈ ℝ+
135 ltaddrp 12075 . . . . 5 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → 𝑀 < (𝑀 + 𝑁))
13641, 134, 135mp2an 675 . . . 4 𝑀 < (𝑀 + 𝑁)
137 0z 11648 . . . . 5 0 ∈ ℤ
138 elfzm11 12628 . . . . 5 ((0 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀𝑀 < (𝑀 + 𝑁))))
139137, 52, 138mp2an 675 . . . 4 (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀𝑀 < (𝑀 + 𝑁)))
140100, 132, 136, 139mpbir3an 1434 . . 3 𝑀 ∈ (0...((𝑀 + 𝑁) − 1))
141 bcm1n 29875 . . 3 ((𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ∧ (𝑀 + 𝑁) ∈ ℕ) → ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)))
142140, 51, 141mp2an 675 . 2 ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁))
143 pncan2 10567 . . . 4 ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑀 + 𝑁) − 𝑀) = 𝑁)
144108, 109, 143mp2an 675 . . 3 ((𝑀 + 𝑁) − 𝑀) = 𝑁
145144oveq1i 6878 . 2 (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)) = (𝑁 / (𝑀 + 𝑁))
146128, 142, 1453eqtri 2828 1 (𝑃‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100  wal 1635   = wceq 1637  wex 1859  wcel 2155  {cab 2788  {crab 3096  cin 3762  wss 3763  𝒫 cpw 4345   class class class wbr 4837  cmpt 4916  cfv 6095  (class class class)co 6868  Fincfn 8186  cc 10213  cr 10214  0cc0 10215  1c1 10216   + caddc 10218   < clt 10353  cle 10354  cmin 10545  -cneg 10546   / cdiv 10963  cn 11299  2c2 11350  cz 11637  cuz 11898  +crp 12040  ...cfz 12543  Ccbc 13303  chash 13331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-rep 4957  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-cnex 10271  ax-resscn 10272  ax-1cn 10273  ax-icn 10274  ax-addcl 10275  ax-addrcl 10276  ax-mulcl 10277  ax-mulrcl 10278  ax-mulcom 10279  ax-addass 10280  ax-mulass 10281  ax-distr 10282  ax-i2m1 10283  ax-1ne0 10284  ax-1rid 10285  ax-rnegex 10286  ax-rrecex 10287  ax-cnre 10288  ax-pre-lttri 10289  ax-pre-lttrn 10290  ax-pre-ltadd 10291  ax-pre-mulgt0 10292
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-nel 3078  df-ral 3097  df-rex 3098  df-reu 3099  df-rmo 3100  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-int 4663  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-pred 5887  df-ord 5933  df-on 5934  df-lim 5935  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-riota 6829  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-om 7290  df-1st 7392  df-2nd 7393  df-wrecs 7636  df-recs 7698  df-rdg 7736  df-1o 7790  df-2o 7791  df-oadd 7794  df-er 7973  df-map 8088  df-en 8187  df-dom 8188  df-sdom 8189  df-fin 8190  df-card 9042  df-cda 9269  df-pnf 10355  df-mnf 10356  df-xr 10357  df-ltxr 10358  df-le 10359  df-sub 10547  df-neg 10548  df-div 10964  df-nn 11300  df-2 11358  df-n0 11554  df-z 11638  df-uz 11899  df-rp 12041  df-fz 12544  df-seq 13019  df-fac 13275  df-bc 13304  df-hash 13332
This theorem is referenced by:  ballotth  30918
  Copyright terms: Public domain W3C validator