Metamath Proof Explorer

Theorem ballotth

Description: Bertrand's ballot problem : the probability that A is ahead throughout the counting. The proof formalized here is a proof "by reflection", as opposed to other known proofs "by induction" or "by permutation". This is Metamath 100 proof #30. (Contributed by Thierry Arnoux, 7-Dec-2016)

Ref Expression
Hypotheses ballotth.m ⊢ 𝑀 ∈ ℕ
ballotth.n ⊢ 𝑁 ∈ ℕ
ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
ballotth.e ⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
ballotth.mgtn ⊢ 𝑁 < 𝑀
ballotth.i ⊢ 𝐼 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
ballotth.r ⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
Assertion ballotth ( 𝑃 ‘ 𝐸 ) = ( ( 𝑀 − 𝑁 ) / ( 𝑀 + 𝑁 ) )

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢ 𝑀 ∈ ℕ
2 ballotth.n ⊢ 𝑁 ∈ ℕ
3 ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4 ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5 ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6 ballotth.e ⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
7 ballotth.mgtn ⊢ 𝑁 < 𝑀
8 ballotth.i ⊢ 𝐼 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
9 ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
10 ballotth.r ⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
11 ssrab2 ⊢ { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) } ⊆ 𝑂
12 6 11 eqsstri ⊢ 𝐸 ⊆ 𝑂
13 fzfi ⊢ ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin
14 pwfi ⊢ ( ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin ↔ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin )
15 13 14 mpbi ⊢ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin
16 ssrab2 ⊢ { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 } ⊆ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) )
17 3 16 eqsstri ⊢ 𝑂 ⊆ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) )
18 ssfi ⊢ ( ( 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin ∧ 𝑂 ⊆ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ) → 𝑂 ∈ Fin )
19 15 17 18 mp2an ⊢ 𝑂 ∈ Fin
20 ssfi ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐸 ⊆ 𝑂 ) → 𝐸 ∈ Fin )
21 19 12 20 mp2an ⊢ 𝐸 ∈ Fin
22 21 elexi ⊢ 𝐸 ∈ V
23 22 elpw ⊢ ( 𝐸 ∈ 𝒫 𝑂 ↔ 𝐸 ⊆ 𝑂 )
24 fveq2 ⊢ ( 𝑥 = 𝐸 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐸 ) )
25 24 oveq1d ⊢ ( 𝑥 = 𝐸 → ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) = ( ( ♯ ‘ 𝐸 ) / ( ♯ ‘ 𝑂 ) ) )
26 ovex ⊢ ( ( ♯ ‘ 𝐸 ) / ( ♯ ‘ 𝑂 ) ) ∈ V
27 25 4 26 fvmpt ⊢ ( 𝐸 ∈ 𝒫 𝑂 → ( 𝑃 ‘ 𝐸 ) = ( ( ♯ ‘ 𝐸 ) / ( ♯ ‘ 𝑂 ) ) )
28 23 27 sylbir ⊢ ( 𝐸 ⊆ 𝑂 → ( 𝑃 ‘ 𝐸 ) = ( ( ♯ ‘ 𝐸 ) / ( ♯ ‘ 𝑂 ) ) )
29 12 28 ax-mp ⊢ ( 𝑃 ‘ 𝐸 ) = ( ( ♯ ‘ 𝐸 ) / ( ♯ ‘ 𝑂 ) )
30 hashssdif ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐸 ⊆ 𝑂 ) → ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) = ( ( ♯ ‘ 𝑂 ) − ( ♯ ‘ 𝐸 ) ) )
31 19 12 30 mp2an ⊢ ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) = ( ( ♯ ‘ 𝑂 ) − ( ♯ ‘ 𝐸 ) )
32 31 eqcomi ⊢ ( ( ♯ ‘ 𝑂 ) − ( ♯ ‘ 𝐸 ) ) = ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) )
33 hashcl ⊢ ( 𝑂 ∈ Fin → ( ♯ ‘ 𝑂 ) ∈ ℕ0 )
34 19 33 ax-mp ⊢ ( ♯ ‘ 𝑂 ) ∈ ℕ0
35 34 nn0cni ⊢ ( ♯ ‘ 𝑂 ) ∈ ℂ
36 hashcl ⊢ ( 𝐸 ∈ Fin → ( ♯ ‘ 𝐸 ) ∈ ℕ0 )
37 21 36 ax-mp ⊢ ( ♯ ‘ 𝐸 ) ∈ ℕ0
38 37 nn0cni ⊢ ( ♯ ‘ 𝐸 ) ∈ ℂ
39 difss ⊢ ( 𝑂 ∖ 𝐸 ) ⊆ 𝑂
40 ssfi ⊢ ( ( 𝑂 ∈ Fin ∧ ( 𝑂 ∖ 𝐸 ) ⊆ 𝑂 ) → ( 𝑂 ∖ 𝐸 ) ∈ Fin )
41 19 39 40 mp2an ⊢ ( 𝑂 ∖ 𝐸 ) ∈ Fin
42 hashcl ⊢ ( ( 𝑂 ∖ 𝐸 ) ∈ Fin → ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) ∈ ℕ0 )
43 41 42 ax-mp ⊢ ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) ∈ ℕ0
44 43 nn0cni ⊢ ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) ∈ ℂ
45 35 38 44 subsub23i ⊢ ( ( ( ♯ ‘ 𝑂 ) − ( ♯ ‘ 𝐸 ) ) = ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) ↔ ( ( ♯ ‘ 𝑂 ) − ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) ) = ( ♯ ‘ 𝐸 ) )
46 32 45 mpbi ⊢ ( ( ♯ ‘ 𝑂 ) − ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) ) = ( ♯ ‘ 𝐸 )
47 46 oveq1i ⊢ ( ( ( ♯ ‘ 𝑂 ) − ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) ) / ( ♯ ‘ 𝑂 ) ) = ( ( ♯ ‘ 𝐸 ) / ( ♯ ‘ 𝑂 ) )
48 29 47 eqtr4i ⊢ ( 𝑃 ‘ 𝐸 ) = ( ( ( ♯ ‘ 𝑂 ) − ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) ) / ( ♯ ‘ 𝑂 ) )
49 1 2 3 ballotlem1 ⊢ ( ♯ ‘ 𝑂 ) = ( ( 𝑀 + 𝑁 ) C 𝑀 )
50 1 nnnn0i ⊢ 𝑀 ∈ ℕ0
51 nnaddcl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
52 1 2 51 mp2an ⊢ ( 𝑀 + 𝑁 ) ∈ ℕ
53 52 nnnn0i ⊢ ( 𝑀 + 𝑁 ) ∈ ℕ0
54 1 nnrei ⊢ 𝑀 ∈ ℝ
55 2 nnnn0i ⊢ 𝑁 ∈ ℕ0
56 54 55 nn0addge1i ⊢ 𝑀 ≤ ( 𝑀 + 𝑁 )
57 elfz2nn0 ⊢ ( 𝑀 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) ↔ ( 𝑀 ∈ ℕ0 ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ∧ 𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
58 50 53 56 57 mpbir3an ⊢ 𝑀 ∈ ( 0 ... ( 𝑀 + 𝑁 ) )
59 bccl2 ⊢ ( 𝑀 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) → ( ( 𝑀 + 𝑁 ) C 𝑀 ) ∈ ℕ )
60 58 59 ax-mp ⊢ ( ( 𝑀 + 𝑁 ) C 𝑀 ) ∈ ℕ
61 60 nnne0i ⊢ ( ( 𝑀 + 𝑁 ) C 𝑀 ) ≠ 0
62 49 61 eqnetri ⊢ ( ♯ ‘ 𝑂 ) ≠ 0
63 35 62 pm3.2i ⊢ ( ( ♯ ‘ 𝑂 ) ∈ ℂ ∧ ( ♯ ‘ 𝑂 ) ≠ 0 )
64 divsubdir ⊢ ( ( ( ♯ ‘ 𝑂 ) ∈ ℂ ∧ ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) ∈ ℂ ∧ ( ( ♯ ‘ 𝑂 ) ∈ ℂ ∧ ( ♯ ‘ 𝑂 ) ≠ 0 ) ) → ( ( ( ♯ ‘ 𝑂 ) − ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) ) / ( ♯ ‘ 𝑂 ) ) = ( ( ( ♯ ‘ 𝑂 ) / ( ♯ ‘ 𝑂 ) ) − ( ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) / ( ♯ ‘ 𝑂 ) ) ) )
65 35 44 63 64 mp3an ⊢ ( ( ( ♯ ‘ 𝑂 ) − ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) ) / ( ♯ ‘ 𝑂 ) ) = ( ( ( ♯ ‘ 𝑂 ) / ( ♯ ‘ 𝑂 ) ) − ( ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) / ( ♯ ‘ 𝑂 ) ) )
66 35 62 dividi ⊢ ( ( ♯ ‘ 𝑂 ) / ( ♯ ‘ 𝑂 ) ) = 1
67 66 oveq1i ⊢ ( ( ( ♯ ‘ 𝑂 ) / ( ♯ ‘ 𝑂 ) ) − ( ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) / ( ♯ ‘ 𝑂 ) ) ) = ( 1 − ( ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) / ( ♯ ‘ 𝑂 ) ) )
68 48 65 67 3eqtri ⊢ ( 𝑃 ‘ 𝐸 ) = ( 1 − ( ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) / ( ♯ ‘ 𝑂 ) ) )
69 1 2 3 4 5 6 7 8 9 10 ballotlem8 ⊢ ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ) = ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } )
70 69 oveq1i ⊢ ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ) + ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ) = ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) + ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) )
71 70 oveq1i ⊢ ( ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ) + ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ) / ( ♯ ‘ 𝑂 ) ) = ( ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) + ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ) / ( ♯ ‘ 𝑂 ) )
72 rabxm ⊢ ( 𝑂 ∖ 𝐸 ) = ( { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ∪ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } )
73 72 fveq2i ⊢ ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) = ( ♯ ‘ ( { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ∪ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) )
74 ssrab2 ⊢ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ⊆ ( 𝑂 ∖ 𝐸 )
75 74 39 sstri ⊢ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ⊆ 𝑂
76 75 17 sstri ⊢ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ⊆ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) )
77 ssfi ⊢ ( ( 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin ∧ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ⊆ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ) → { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ∈ Fin )
78 15 76 77 mp2an ⊢ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ∈ Fin
79 ssrab2 ⊢ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ⊆ ( 𝑂 ∖ 𝐸 )
80 79 39 sstri ⊢ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ⊆ 𝑂
81 80 17 sstri ⊢ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ⊆ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) )
82 ssfi ⊢ ( ( 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∈ Fin ∧ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ⊆ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ) → { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ∈ Fin )
83 15 81 82 mp2an ⊢ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ∈ Fin
84 rabnc ⊢ ( { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ∩ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) = ∅
85 hashun ⊢ ( ( { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ∈ Fin ∧ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ∈ Fin ∧ ( { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ∩ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) = ∅ ) → ( ♯ ‘ ( { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ∪ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ) = ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ) + ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ) )
86 78 83 84 85 mp3an ⊢ ( ♯ ‘ ( { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ∪ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ) = ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ) + ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) )
87 73 86 eqtri ⊢ ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) = ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ) + ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) )
88 87 oveq1i ⊢ ( ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) / ( ♯ ‘ 𝑂 ) ) = ( ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ 1 ∈ 𝑐 } ) + ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ) / ( ♯ ‘ 𝑂 ) )
89 ssrab2 ⊢ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ⊆ 𝑂
90 19 elexi ⊢ 𝑂 ∈ V
91 90 elpw2 ⊢ ( { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ∈ 𝒫 𝑂 ↔ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ⊆ 𝑂 )
92 89 91 mpbir ⊢ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ∈ 𝒫 𝑂
93 fveq2 ⊢ ( 𝑥 = { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) )
94 93 oveq1d ⊢ ( 𝑥 = { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } → ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) = ( ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) / ( ♯ ‘ 𝑂 ) ) )
95 ovex ⊢ ( ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) / ( ♯ ‘ 𝑂 ) ) ∈ V
96 94 4 95 fvmpt ⊢ ( { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ∈ 𝒫 𝑂 → ( 𝑃 ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) = ( ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) / ( ♯ ‘ 𝑂 ) ) )
97 92 96 ax-mp ⊢ ( 𝑃 ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) = ( ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) / ( ♯ ‘ 𝑂 ) )
98 1 2 3 4 ballotlem2 ⊢ ( 𝑃 ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) = ( 𝑁 / ( 𝑀 + 𝑁 ) )
99 nfrab1 ⊢ Ⅎ 𝑐 { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 }
100 nfrab1 ⊢ Ⅎ 𝑐 { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 }
101 99 100 dfss2f ⊢ ( { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ⊆ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ↔ ∀ 𝑐 ( 𝑐 ∈ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } → 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) )
102 1 2 3 4 5 6 ballotlem4 ⊢ ( 𝑐 ∈ 𝑂 → ( ¬ 1 ∈ 𝑐 → ¬ 𝑐 ∈ 𝐸 ) )
103 102 imdistani ⊢ ( ( 𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐 ) → ( 𝑐 ∈ 𝑂 ∧ ¬ 𝑐 ∈ 𝐸 ) )
104 rabid ⊢ ( 𝑐 ∈ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ↔ ( 𝑐 ∈ 𝑂 ∧ ¬ 1 ∈ 𝑐 ) )
105 eldif ⊢ ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↔ ( 𝑐 ∈ 𝑂 ∧ ¬ 𝑐 ∈ 𝐸 ) )
106 103 104 105 3imtr4i ⊢ ( 𝑐 ∈ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } → 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) )
107 104 simprbi ⊢ ( 𝑐 ∈ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } → ¬ 1 ∈ 𝑐 )
108 rabid ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ↔ ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∧ ¬ 1 ∈ 𝑐 ) )
109 106 107 108 sylanbrc ⊢ ( 𝑐 ∈ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } → 𝑐 ∈ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } )
110 101 109 mpgbir ⊢ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ⊆ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 }
111 rabss2 ⊢ ( ( 𝑂 ∖ 𝐸 ) ⊆ 𝑂 → { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ⊆ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } )
112 39 111 ax-mp ⊢ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ⊆ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 }
113 110 112 eqssi ⊢ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } = { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 }
114 113 fveq2i ⊢ ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) = ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } )
115 114 oveq1i ⊢ ( ( ♯ ‘ { 𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐 } ) / ( ♯ ‘ 𝑂 ) ) = ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) / ( ♯ ‘ 𝑂 ) )
116 97 98 115 3eqtr3i ⊢ ( 𝑁 / ( 𝑀 + 𝑁 ) ) = ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) / ( ♯ ‘ 𝑂 ) )
117 116 oveq2i ⊢ ( 2 · ( 𝑁 / ( 𝑀 + 𝑁 ) ) ) = ( 2 · ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) / ( ♯ ‘ 𝑂 ) ) )
118 2cn ⊢ 2 ∈ ℂ
119 hashcl ⊢ ( { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ∈ Fin → ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ∈ ℕ0 )
120 83 119 ax-mp ⊢ ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ∈ ℕ0
121 120 nn0cni ⊢ ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ∈ ℂ
122 118 121 35 62 divassi ⊢ ( ( 2 · ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ) / ( ♯ ‘ 𝑂 ) ) = ( 2 · ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) / ( ♯ ‘ 𝑂 ) ) )
123 121 2timesi ⊢ ( 2 · ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ) = ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) + ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) )
124 123 oveq1i ⊢ ( ( 2 · ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ) / ( ♯ ‘ 𝑂 ) ) = ( ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) + ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ) / ( ♯ ‘ 𝑂 ) )
125 117 122 124 3eqtr2i ⊢ ( 2 · ( 𝑁 / ( 𝑀 + 𝑁 ) ) ) = ( ( ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) + ( ♯ ‘ { 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ∣ ¬ 1 ∈ 𝑐 } ) ) / ( ♯ ‘ 𝑂 ) )
126 71 88 125 3eqtr4ri ⊢ ( 2 · ( 𝑁 / ( 𝑀 + 𝑁 ) ) ) = ( ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) / ( ♯ ‘ 𝑂 ) )
127 126 oveq2i ⊢ ( 1 − ( 2 · ( 𝑁 / ( 𝑀 + 𝑁 ) ) ) ) = ( 1 − ( ( ♯ ‘ ( 𝑂 ∖ 𝐸 ) ) / ( ♯ ‘ 𝑂 ) ) )
128 52 nncni ⊢ ( 𝑀 + 𝑁 ) ∈ ℂ
129 2 nncni ⊢ 𝑁 ∈ ℂ
130 118 129 mulcli ⊢ ( 2 · 𝑁 ) ∈ ℂ
131 52 nnne0i ⊢ ( 𝑀 + 𝑁 ) ≠ 0
132 128 131 pm3.2i ⊢ ( ( 𝑀 + 𝑁 ) ∈ ℂ ∧ ( 𝑀 + 𝑁 ) ≠ 0 )
133 divsubdir ⊢ ( ( ( 𝑀 + 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ∈ ℂ ∧ ( ( 𝑀 + 𝑁 ) ∈ ℂ ∧ ( 𝑀 + 𝑁 ) ≠ 0 ) ) → ( ( ( 𝑀 + 𝑁 ) − ( 2 · 𝑁 ) ) / ( 𝑀 + 𝑁 ) ) = ( ( ( 𝑀 + 𝑁 ) / ( 𝑀 + 𝑁 ) ) − ( ( 2 · 𝑁 ) / ( 𝑀 + 𝑁 ) ) ) )
134 128 130 132 133 mp3an ⊢ ( ( ( 𝑀 + 𝑁 ) − ( 2 · 𝑁 ) ) / ( 𝑀 + 𝑁 ) ) = ( ( ( 𝑀 + 𝑁 ) / ( 𝑀 + 𝑁 ) ) − ( ( 2 · 𝑁 ) / ( 𝑀 + 𝑁 ) ) )
135 129 2timesi ⊢ ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 )
136 135 oveq2i ⊢ ( ( 𝑀 + 𝑁 ) − ( 2 · 𝑁 ) ) = ( ( 𝑀 + 𝑁 ) − ( 𝑁 + 𝑁 ) )
137 1 nncni ⊢ 𝑀 ∈ ℂ
138 137 129 129 129 addsub4i ⊢ ( ( 𝑀 + 𝑁 ) − ( 𝑁 + 𝑁 ) ) = ( ( 𝑀 − 𝑁 ) + ( 𝑁 − 𝑁 ) )
139 129 subidi ⊢ ( 𝑁 − 𝑁 ) = 0
140 139 oveq2i ⊢ ( ( 𝑀 − 𝑁 ) + ( 𝑁 − 𝑁 ) ) = ( ( 𝑀 − 𝑁 ) + 0 )
141 137 129 subcli ⊢ ( 𝑀 − 𝑁 ) ∈ ℂ
142 141 addid1i ⊢ ( ( 𝑀 − 𝑁 ) + 0 ) = ( 𝑀 − 𝑁 )
143 138 140 142 3eqtri ⊢ ( ( 𝑀 + 𝑁 ) − ( 𝑁 + 𝑁 ) ) = ( 𝑀 − 𝑁 )
144 136 143 eqtri ⊢ ( ( 𝑀 + 𝑁 ) − ( 2 · 𝑁 ) ) = ( 𝑀 − 𝑁 )
145 144 oveq1i ⊢ ( ( ( 𝑀 + 𝑁 ) − ( 2 · 𝑁 ) ) / ( 𝑀 + 𝑁 ) ) = ( ( 𝑀 − 𝑁 ) / ( 𝑀 + 𝑁 ) )
146 128 131 dividi ⊢ ( ( 𝑀 + 𝑁 ) / ( 𝑀 + 𝑁 ) ) = 1
147 118 129 128 131 divassi ⊢ ( ( 2 · 𝑁 ) / ( 𝑀 + 𝑁 ) ) = ( 2 · ( 𝑁 / ( 𝑀 + 𝑁 ) ) )
148 146 147 oveq12i ⊢ ( ( ( 𝑀 + 𝑁 ) / ( 𝑀 + 𝑁 ) ) − ( ( 2 · 𝑁 ) / ( 𝑀 + 𝑁 ) ) ) = ( 1 − ( 2 · ( 𝑁 / ( 𝑀 + 𝑁 ) ) ) )
149 134 145 148 3eqtr3ri ⊢ ( 1 − ( 2 · ( 𝑁 / ( 𝑀 + 𝑁 ) ) ) ) = ( ( 𝑀 − 𝑁 ) / ( 𝑀 + 𝑁 ) )
150 68 127 149 3eqtr2i ⊢ ( 𝑃 ‘ 𝐸 ) = ( ( 𝑀 − 𝑁 ) / ( 𝑀 + 𝑁 ) )