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 30535
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 3685 . . . . 5 {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂
2 ballotth.m . . . . . . 7 𝑀 ∈ ℕ
3 ballotth.n . . . . . . 7 𝑁 ∈ ℕ
4 ballotth.o . . . . . . 7 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}
52, 3, 4ballotlemoex 30532 . . . . . 6 𝑂 ∈ V
65elpw2 4826 . . . . 5 ({𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 ↔ {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ⊆ 𝑂)
71, 6mpbir 221 . . . 4 {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂
8 fveq2 6189 . . . . . 6 (𝑥 = {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} → (#‘𝑥) = (#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}))
98oveq1d 6662 . . . . 5 (𝑥 = {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} → ((#‘𝑥) / (#‘𝑂)) = ((#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)))
10 ballotth.p . . . . 5 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((#‘𝑥) / (#‘𝑂)))
11 ovex 6675 . . . . 5 ((#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)) ∈ V
129, 10, 11fvmpt 6280 . . . 4 ({𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} ∈ 𝒫 𝑂 → (𝑃‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)))
137, 12ax-mp 5 . . 3 (𝑃‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂))
14 an32 839 . . . . . . . . 9 (((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (#‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
15 2eluzge1 11731 . . . . . . . . . . . . . . 15 2 ∈ (ℤ‘1)
16 fzss1 12377 . . . . . . . . . . . . . . 15 (2 ∈ (ℤ‘1) → (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁)))
1715, 16ax-mp 5 . . . . . . . . . . . . . 14 (2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁))
18 sspwb 4915 . . . . . . . . . . . . . 14 ((2...(𝑀 + 𝑁)) ⊆ (1...(𝑀 + 𝑁)) ↔ 𝒫 (2...(𝑀 + 𝑁)) ⊆ 𝒫 (1...(𝑀 + 𝑁)))
1917, 18mpbi 220 . . . . . . . . . . . . 13 𝒫 (2...(𝑀 + 𝑁)) ⊆ 𝒫 (1...(𝑀 + 𝑁))
2019sseli 3597 . . . . . . . . . . . 12 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → 𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)))
21 1lt2 11191 . . . . . . . . . . . . . . . . 17 1 < 2
22 1re 10036 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
23 2re 11087 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
2422, 23ltnlei 10155 . . . . . . . . . . . . . . . . 17 (1 < 2 ↔ ¬ 2 ≤ 1)
2521, 24mpbi 220 . . . . . . . . . . . . . . . 16 ¬ 2 ≤ 1
26 elfzle1 12341 . . . . . . . . . . . . . . . 16 (1 ∈ (2...(𝑀 + 𝑁)) → 2 ≤ 1)
2725, 26mto 188 . . . . . . . . . . . . . . 15 ¬ 1 ∈ (2...(𝑀 + 𝑁))
28 elelpwi 4169 . . . . . . . . . . . . . . 15 ((1 ∈ 𝑐𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) → 1 ∈ (2...(𝑀 + 𝑁)))
2927, 28mto 188 . . . . . . . . . . . . . 14 ¬ (1 ∈ 𝑐𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)))
30 ancom 466 . . . . . . . . . . . . . 14 ((1 ∈ 𝑐𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁))) ↔ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐))
3129, 30mtbi 312 . . . . . . . . . . . . 13 ¬ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ 1 ∈ 𝑐)
3231imnani 439 . . . . . . . . . . . 12 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → ¬ 1 ∈ 𝑐)
3320, 32jca 554 . . . . . . . . . . 11 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) → (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐))
34 ssin 3833 . . . . . . . . . . . . 13 ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) ↔ 𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}))
35 1le2 11238 . . . . . . . . . . . . . . . . . . . . . 22 1 ≤ 2
36 1p1e2 11131 . . . . . . . . . . . . . . . . . . . . . . 23 (1 + 1) = 2
37 nnge1 11043 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℕ → 1 ≤ 𝑀)
382, 37ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ≤ 𝑀
39 nnge1 11043 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → 1 ≤ 𝑁)
403, 39ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ≤ 𝑁
412nnrei 11026 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 ∈ ℝ
423nnrei 11026 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑁 ∈ ℝ
4322, 22, 41, 42le2addi 10588 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1 ≤ 𝑀 ∧ 1 ≤ 𝑁) → (1 + 1) ≤ (𝑀 + 𝑁))
4438, 40, 43mp2an 708 . . . . . . . . . . . . . . . . . . . . . . 23 (1 + 1) ≤ (𝑀 + 𝑁)
4536, 44eqbrtrri 4674 . . . . . . . . . . . . . . . . . . . . . 22 2 ≤ (𝑀 + 𝑁)
4641, 42readdcli 10050 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 + 𝑁) ∈ ℝ
4722, 23, 46letri 10163 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ≤ 2 ∧ 2 ≤ (𝑀 + 𝑁)) → 1 ≤ (𝑀 + 𝑁))
4835, 45, 47mp2an 708 . . . . . . . . . . . . . . . . . . . . 21 1 ≤ (𝑀 + 𝑁)
49 1z 11404 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℤ
50 nnaddcl 11039 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ)
512, 3, 50mp2an 708 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 + 𝑁) ∈ ℕ
5251nnzi 11398 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 + 𝑁) ∈ ℤ
53 eluz 11698 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → ((𝑀 + 𝑁) ∈ (ℤ‘1) ↔ 1 ≤ (𝑀 + 𝑁)))
5449, 52, 53mp2an 708 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 + 𝑁) ∈ (ℤ‘1) ↔ 1 ≤ (𝑀 + 𝑁))
5548, 54mpbir 221 . . . . . . . . . . . . . . . . . . . 20 (𝑀 + 𝑁) ∈ (ℤ‘1)
56 elfzp12 12415 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 + 𝑁) ∈ (ℤ‘1) → (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))))
5755, 56ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...(𝑀 + 𝑁)) ↔ (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))
5857biimpi 206 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...(𝑀 + 𝑁)) → (𝑖 = 1 ∨ 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁))))
5958orcanai 952 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ ((1 + 1)...(𝑀 + 𝑁)))
6036oveq1i 6657 . . . . . . . . . . . . . . . . 17 ((1 + 1)...(𝑀 + 𝑁)) = (2...(𝑀 + 𝑁))
6159, 60syl6eleq 2710 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1) → 𝑖 ∈ (2...(𝑀 + 𝑁)))
6261ss2abi 3672 . . . . . . . . . . . . . . 15 {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} ⊆ {𝑖𝑖 ∈ (2...(𝑀 + 𝑁))}
63 inab 3893 . . . . . . . . . . . . . . . 16 ({𝑖𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)}
64 abid2 2744 . . . . . . . . . . . . . . . . 17 {𝑖𝑖 ∈ (1...(𝑀 + 𝑁))} = (1...(𝑀 + 𝑁))
6564ineq1i 3808 . . . . . . . . . . . . . . . 16 ({𝑖𝑖 ∈ (1...(𝑀 + 𝑁))} ∩ {𝑖 ∣ ¬ 𝑖 = 1}) = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
6663, 65eqtr3i 2645 . . . . . . . . . . . . . . 15 {𝑖 ∣ (𝑖 ∈ (1...(𝑀 + 𝑁)) ∧ ¬ 𝑖 = 1)} = ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1})
67 abid2 2744 . . . . . . . . . . . . . . 15 {𝑖𝑖 ∈ (2...(𝑀 + 𝑁))} = (2...(𝑀 + 𝑁))
6862, 66, 673sstr3i 3641 . . . . . . . . . . . . . 14 ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))
69 sstr 3609 . . . . . . . . . . . . . 14 ((𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ∧ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) ⊆ (2...(𝑀 + 𝑁))) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
7068, 69mpan2 707 . . . . . . . . . . . . 13 (𝑐 ⊆ ((1...(𝑀 + 𝑁)) ∩ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
7134, 70sylbi 207 . . . . . . . . . . . 12 ((𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}) → 𝑐 ⊆ (2...(𝑀 + 𝑁)))
72 selpw 4163 . . . . . . . . . . . . 13 (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (1...(𝑀 + 𝑁)))
73 ssab 3670 . . . . . . . . . . . . . 14 (𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1} ↔ ∀𝑖(𝑖𝑐 → ¬ 𝑖 = 1))
74 df-ex 1704 . . . . . . . . . . . . . . . . 17 (∃𝑖(𝑖 = 1 ∧ 𝑖𝑐) ↔ ¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐))
7574bicomi 214 . . . . . . . . . . . . . . . 16 (¬ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐) ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖𝑐))
7675con1bii 346 . . . . . . . . . . . . . . 15 (¬ ∃𝑖(𝑖 = 1 ∧ 𝑖𝑐) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐))
77 df-clel 2617 . . . . . . . . . . . . . . . 16 (1 ∈ 𝑐 ↔ ∃𝑖(𝑖 = 1 ∧ 𝑖𝑐))
7877notbii 310 . . . . . . . . . . . . . . 15 (¬ 1 ∈ 𝑐 ↔ ¬ ∃𝑖(𝑖 = 1 ∧ 𝑖𝑐))
79 imnang 1768 . . . . . . . . . . . . . . . 16 (∀𝑖(𝑖𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖𝑐𝑖 = 1))
80 ancom 466 . . . . . . . . . . . . . . . . . 18 ((𝑖 = 1 ∧ 𝑖𝑐) ↔ (𝑖𝑐𝑖 = 1))
8180notbii 310 . . . . . . . . . . . . . . . . 17 (¬ (𝑖 = 1 ∧ 𝑖𝑐) ↔ ¬ (𝑖𝑐𝑖 = 1))
8281albii 1746 . . . . . . . . . . . . . . . 16 (∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐) ↔ ∀𝑖 ¬ (𝑖𝑐𝑖 = 1))
8379, 82bitr4i 267 . . . . . . . . . . . . . . 15 (∀𝑖(𝑖𝑐 → ¬ 𝑖 = 1) ↔ ∀𝑖 ¬ (𝑖 = 1 ∧ 𝑖𝑐))
8476, 78, 833bitr4ri 293 . . . . . . . . . . . . . 14 (∀𝑖(𝑖𝑐 → ¬ 𝑖 = 1) ↔ ¬ 1 ∈ 𝑐)
8573, 84bitr2i 265 . . . . . . . . . . . . 13 (¬ 1 ∈ 𝑐𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1})
8672, 85anbi12i 733 . . . . . . . . . . . 12 ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ↔ (𝑐 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝑐 ⊆ {𝑖 ∣ ¬ 𝑖 = 1}))
87 selpw 4163 . . . . . . . . . . . 12 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ 𝑐 ⊆ (2...(𝑀 + 𝑁)))
8871, 86, 873imtr4i 281 . . . . . . . . . . 11 ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) → 𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)))
8933, 88impbii 199 . . . . . . . . . 10 (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐))
9089anbi1i 731 . . . . . . . . 9 ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ ¬ 1 ∈ 𝑐) ∧ (#‘𝑐) = 𝑀))
914rabeq2i 3195 . . . . . . . . . 10 (𝑐𝑂 ↔ (𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀))
9291anbi1i 731 . . . . . . . . 9 ((𝑐𝑂 ∧ ¬ 1 ∈ 𝑐) ↔ ((𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀) ∧ ¬ 1 ∈ 𝑐))
9314, 90, 923bitr4i 292 . . . . . . . 8 ((𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀) ↔ (𝑐𝑂 ∧ ¬ 1 ∈ 𝑐))
9493abbii 2738 . . . . . . 7 {𝑐 ∣ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀)} = {𝑐 ∣ (𝑐𝑂 ∧ ¬ 1 ∈ 𝑐)}
95 df-rab 2920 . . . . . . 7 {𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} = {𝑐 ∣ (𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∧ (#‘𝑐) = 𝑀)}
96 df-rab 2920 . . . . . . 7 {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐} = {𝑐 ∣ (𝑐𝑂 ∧ ¬ 1 ∈ 𝑐)}
9794, 95, 963eqtr4i 2653 . . . . . 6 {𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀} = {𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}
9897fveq2i 6192 . . . . 5 (#‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}) = (#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐})
99 fzfi 12766 . . . . . . 7 (2...(𝑀 + 𝑁)) ∈ Fin
1002nnzi 11398 . . . . . . 7 𝑀 ∈ ℤ
101 hashbc 13232 . . . . . . 7 (((2...(𝑀 + 𝑁)) ∈ Fin ∧ 𝑀 ∈ ℤ) → ((#‘(2...(𝑀 + 𝑁)))C𝑀) = (#‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}))
10299, 100, 101mp2an 708 . . . . . 6 ((#‘(2...(𝑀 + 𝑁)))C𝑀) = (#‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀})
103 2z 11406 . . . . . . . . . . . 12 2 ∈ ℤ
104103eluz1i 11692 . . . . . . . . . . 11 ((𝑀 + 𝑁) ∈ (ℤ‘2) ↔ ((𝑀 + 𝑁) ∈ ℤ ∧ 2 ≤ (𝑀 + 𝑁)))
10552, 45, 104mpbir2an 955 . . . . . . . . . 10 (𝑀 + 𝑁) ∈ (ℤ‘2)
106 hashfz 13209 . . . . . . . . . 10 ((𝑀 + 𝑁) ∈ (ℤ‘2) → (#‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1))
107105, 106ax-mp 5 . . . . . . . . 9 (#‘(2...(𝑀 + 𝑁))) = (((𝑀 + 𝑁) − 2) + 1)
1082nncni 11027 . . . . . . . . . . 11 𝑀 ∈ ℂ
1093nncni 11027 . . . . . . . . . . 11 𝑁 ∈ ℂ
110108, 109addcli 10041 . . . . . . . . . 10 (𝑀 + 𝑁) ∈ ℂ
111 2cn 11088 . . . . . . . . . 10 2 ∈ ℂ
112 ax-1cn 9991 . . . . . . . . . 10 1 ∈ ℂ
113 subadd23 10290 . . . . . . . . . 10 (((𝑀 + 𝑁) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2)))
114110, 111, 112, 113mp3an 1423 . . . . . . . . 9 (((𝑀 + 𝑁) − 2) + 1) = ((𝑀 + 𝑁) + (1 − 2))
115111, 112negsubdi2i 10364 . . . . . . . . . . 11 -(2 − 1) = (1 − 2)
116 2m1e1 11132 . . . . . . . . . . . 12 (2 − 1) = 1
117116negeqi 10271 . . . . . . . . . . 11 -(2 − 1) = -1
118115, 117eqtr3i 2645 . . . . . . . . . 10 (1 − 2) = -1
119118oveq2i 6658 . . . . . . . . 9 ((𝑀 + 𝑁) + (1 − 2)) = ((𝑀 + 𝑁) + -1)
120107, 114, 1193eqtri 2647 . . . . . . . 8 (#‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) + -1)
121110, 112negsubi 10356 . . . . . . . 8 ((𝑀 + 𝑁) + -1) = ((𝑀 + 𝑁) − 1)
122120, 121eqtri 2643 . . . . . . 7 (#‘(2...(𝑀 + 𝑁))) = ((𝑀 + 𝑁) − 1)
123122oveq1i 6657 . . . . . 6 ((#‘(2...(𝑀 + 𝑁)))C𝑀) = (((𝑀 + 𝑁) − 1)C𝑀)
124102, 123eqtr3i 2645 . . . . 5 (#‘{𝑐 ∈ 𝒫 (2...(𝑀 + 𝑁)) ∣ (#‘𝑐) = 𝑀}) = (((𝑀 + 𝑁) − 1)C𝑀)
12598, 124eqtr3i 2645 . . . 4 (#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = (((𝑀 + 𝑁) − 1)C𝑀)
1262, 3, 4ballotlem1 30533 . . . 4 (#‘𝑂) = ((𝑀 + 𝑁)C𝑀)
127125, 126oveq12i 6659 . . 3 ((#‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) / (#‘𝑂)) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
12813, 127eqtri 2643 . 2 (𝑃‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀))
129 0le1 10548 . . . . 5 0 ≤ 1
130 0re 10037 . . . . . 6 0 ∈ ℝ
131130, 22, 41letri 10163 . . . . 5 ((0 ≤ 1 ∧ 1 ≤ 𝑀) → 0 ≤ 𝑀)
132129, 38, 131mp2an 708 . . . 4 0 ≤ 𝑀
1333nngt0i 11051 . . . . . 6 0 < 𝑁
13442, 133elrpii 11832 . . . . 5 𝑁 ∈ ℝ+
135 ltaddrp 11864 . . . . 5 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → 𝑀 < (𝑀 + 𝑁))
13641, 134, 135mp2an 708 . . . 4 𝑀 < (𝑀 + 𝑁)
137 0z 11385 . . . . 5 0 ∈ ℤ
138 elfzm11 12407 . . . . 5 ((0 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ) → (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀𝑀 < (𝑀 + 𝑁))))
139137, 52, 138mp2an 708 . . . 4 (𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀𝑀 < (𝑀 + 𝑁)))
140100, 132, 136, 139mpbir3an 1243 . . 3 𝑀 ∈ (0...((𝑀 + 𝑁) − 1))
141 bcm1n 29539 . . 3 ((𝑀 ∈ (0...((𝑀 + 𝑁) − 1)) ∧ (𝑀 + 𝑁) ∈ ℕ) → ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)))
142140, 51, 141mp2an 708 . 2 ((((𝑀 + 𝑁) − 1)C𝑀) / ((𝑀 + 𝑁)C𝑀)) = (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁))
143 pncan2 10285 . . . 4 ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑀 + 𝑁) − 𝑀) = 𝑁)
144108, 109, 143mp2an 708 . . 3 ((𝑀 + 𝑁) − 𝑀) = 𝑁
145144oveq1i 6657 . 2 (((𝑀 + 𝑁) − 𝑀) / (𝑀 + 𝑁)) = (𝑁 / (𝑀 + 𝑁))
146128, 142, 1453eqtri 2647 1 (𝑃‘{𝑐𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1037  wal 1480   = wceq 1482  wex 1703  wcel 1989  {cab 2607  {crab 2915  cin 3571  wss 3572  𝒫 cpw 4156   class class class wbr 4651  cmpt 4727  cfv 5886  (class class class)co 6647  Fincfn 7952  cc 9931  cr 9932  0cc0 9933  1c1 9934   + caddc 9936   < clt 10071  cle 10072  cmin 10263  -cneg 10264   / cdiv 10681  cn 11017  2c2 11067  cz 11374  cuz 11684  +crp 11829  ...cfz 12323  Ccbc 13084  #chash 13112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-1o 7557  df-2o 7558  df-oadd 7561  df-er 7739  df-map 7856  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-card 8762  df-cda 8987  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-div 10682  df-nn 11018  df-2 11076  df-n0 11290  df-z 11375  df-uz 11685  df-rp 11830  df-fz 12324  df-seq 12797  df-fac 13056  df-bc 13085  df-hash 13113
This theorem is referenced by:  ballotth  30584
  Copyright terms: Public domain W3C validator