Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ballotth Unicode version

Theorem ballotth 23089
Description: Bertrand's ballot problem : the probability that A is ahead throughout the counting. (Contributed by Thierry Arnoux, 7-Dec-2016.)
Hypotheses
Ref Expression
ballotth.m  |-  M  e.  NN
ballotth.n  |-  N  e.  NN
ballotth.o  |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
)  |  ( # `  c )  =  M }
ballotth.p  |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `
 O ) ) )
ballotth.f  |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
( 1 ... i
)  i^i  c )
)  -  ( # `  ( ( 1 ... i )  \  c
) ) ) ) )
ballotth.e  |-  E  =  { c  e.  O  |  A. i  e.  ( 1 ... ( M  +  N ) ) 0  <  ( ( F `  c ) `
 i ) }
ballotth.mgtn  |-  N  < 
M
ballotth.i  |-  I  =  ( c  e.  ( O  \  E ) 
|->  sup ( { k  e.  ( 1 ... ( M  +  N
) )  |  ( ( F `  c
) `  k )  =  0 } ,  RR ,  `'  <  ) )
ballotth.s  |-  S  =  ( c  e.  ( O  \  E ) 
|->  ( i  e.  ( 1 ... ( M  +  N ) ) 
|->  if ( i  <_ 
( I `  c
) ,  ( ( ( I `  c
)  +  1 )  -  i ) ,  i ) ) )
ballotth.r  |-  R  =  ( c  e.  ( O  \  E ) 
|->  ( ( S `  c ) " c
) )
Assertion
Ref Expression
ballotth  |-  ( P `
 E )  =  ( ( M  -  N )  /  ( M  +  N )
)
Distinct variable groups:    M, c    N, c    O, c    i, M   
i, N    i, O    k, M    k, N    k, O    i, c, F, k   
i, E, k    k, I, c    E, c    i, I, c    S, k, i, c    R, i, k    x, c, F    x, M    x, N, k, i    x, E   
x, O
Allowed substitution hints:    P( x, i, k, c)    R( x, c)    S( x)    I( x)

Proof of Theorem ballotth
StepHypRef Expression
1 ballotth.e . . . . . . 7  |-  E  =  { c  e.  O  |  A. i  e.  ( 1 ... ( M  +  N ) ) 0  <  ( ( F `  c ) `
 i ) }
2 ssrab2 3259 . . . . . . 7  |-  { c  e.  O  |  A. i  e.  ( 1 ... ( M  +  N ) ) 0  <  ( ( F `
 c ) `  i ) }  C_  O
31, 2eqsstri 3209 . . . . . 6  |-  E  C_  O
4 fzfi 11028 . . . . . . . . . . . 12  |-  ( 1 ... ( M  +  N ) )  e. 
Fin
5 pwfi 7146 . . . . . . . . . . . 12  |-  ( ( 1 ... ( M  +  N ) )  e.  Fin  <->  ~P (
1 ... ( M  +  N ) )  e. 
Fin )
64, 5mpbi 201 . . . . . . . . . . 11  |-  ~P (
1 ... ( M  +  N ) )  e. 
Fin
7 ssrab2 3259 . . . . . . . . . . . 12  |-  { c  e.  ~P ( 1 ... ( M  +  N ) )  |  ( # `  c
)  =  M }  C_ 
~P ( 1 ... ( M  +  N
) )
8 ballotth.o . . . . . . . . . . . . 13  |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
)  |  ( # `  c )  =  M }
98sseq1i 3203 . . . . . . . . . . . 12  |-  ( O 
C_  ~P ( 1 ... ( M  +  N
) )  <->  { c  e.  ~P ( 1 ... ( M  +  N
) )  |  (
# `  c )  =  M }  C_  ~P ( 1 ... ( M  +  N )
) )
107, 9mpbir 202 . . . . . . . . . . 11  |-  O  C_  ~P ( 1 ... ( M  +  N )
)
11 ssfi 7078 . . . . . . . . . . 11  |-  ( ( ~P ( 1 ... ( M  +  N
) )  e.  Fin  /\  O  C_  ~P (
1 ... ( M  +  N ) ) )  ->  O  e.  Fin )
126, 10, 11mp2an 655 . . . . . . . . . 10  |-  O  e. 
Fin
13 ssfi 7078 . . . . . . . . . 10  |-  ( ( O  e.  Fin  /\  E  C_  O )  ->  E  e.  Fin )
1412, 3, 13mp2an 655 . . . . . . . . 9  |-  E  e. 
Fin
1514elexi 2798 . . . . . . . 8  |-  E  e. 
_V
1615elpw 3632 . . . . . . 7  |-  ( E  e.  ~P O  <->  E  C_  O
)
17 fveq2 5485 . . . . . . . . 9  |-  ( x  =  E  ->  ( # `
 x )  =  ( # `  E
) )
1817oveq1d 5834 . . . . . . . 8  |-  ( x  =  E  ->  (
( # `  x )  /  ( # `  O
) )  =  ( ( # `  E
)  /  ( # `  O ) ) )
19 ballotth.p . . . . . . . 8  |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `
 O ) ) )
20 ovex 5844 . . . . . . . 8  |-  ( (
# `  E )  /  ( # `  O
) )  e.  _V
2118, 19, 20fvmpt 5563 . . . . . . 7  |-  ( E  e.  ~P O  -> 
( P `  E
)  =  ( (
# `  E )  /  ( # `  O
) ) )
2216, 21sylbir 206 . . . . . 6  |-  ( E 
C_  O  ->  ( P `  E )  =  ( ( # `  E )  /  ( # `
 O ) ) )
233, 22ax-mp 10 . . . . 5  |-  ( P `
 E )  =  ( ( # `  E
)  /  ( # `  O ) )
24 hashssdif 11368 . . . . . . . . 9  |-  ( ( O  e.  Fin  /\  E  C_  O )  -> 
( # `  ( O 
\  E ) )  =  ( ( # `  O )  -  ( # `
 E ) ) )
2512, 3, 24mp2an 655 . . . . . . . 8  |-  ( # `  ( O  \  E
) )  =  ( ( # `  O
)  -  ( # `  E ) )
2625eqcomi 2288 . . . . . . 7  |-  ( (
# `  O )  -  ( # `  E
) )  =  (
# `  ( O  \  E ) )
27 hashcl 11344 . . . . . . . . . 10  |-  ( O  e.  Fin  ->  ( # `
 O )  e. 
NN0 )
2812, 27ax-mp 10 . . . . . . . . 9  |-  ( # `  O )  e.  NN0
2928nn0cni 9972 . . . . . . . 8  |-  ( # `  O )  e.  CC
30 hashcl 11344 . . . . . . . . . 10  |-  ( E  e.  Fin  ->  ( # `
 E )  e. 
NN0 )
3114, 30ax-mp 10 . . . . . . . . 9  |-  ( # `  E )  e.  NN0
3231nn0cni 9972 . . . . . . . 8  |-  ( # `  E )  e.  CC
33 difss 3304 . . . . . . . . . . 11  |-  ( O 
\  E )  C_  O
34 ssfi 7078 . . . . . . . . . . 11  |-  ( ( O  e.  Fin  /\  ( O  \  E ) 
C_  O )  -> 
( O  \  E
)  e.  Fin )
3512, 33, 34mp2an 655 . . . . . . . . . 10  |-  ( O 
\  E )  e. 
Fin
36 hashcl 11344 . . . . . . . . . 10  |-  ( ( O  \  E )  e.  Fin  ->  ( # `
 ( O  \  E ) )  e. 
NN0 )
3735, 36ax-mp 10 . . . . . . . . 9  |-  ( # `  ( O  \  E
) )  e.  NN0
3837nn0cni 9972 . . . . . . . 8  |-  ( # `  ( O  \  E
) )  e.  CC
39 subsub23 9051 . . . . . . . 8  |-  ( ( ( # `  O
)  e.  CC  /\  ( # `  E )  e.  CC  /\  ( # `
 ( O  \  E ) )  e.  CC )  ->  (
( ( # `  O
)  -  ( # `  E ) )  =  ( # `  ( O  \  E ) )  <-> 
( ( # `  O
)  -  ( # `  ( O  \  E
) ) )  =  ( # `  E
) ) )
4029, 32, 38, 39mp3an 1279 . . . . . . 7  |-  ( ( ( # `  O
)  -  ( # `  E ) )  =  ( # `  ( O  \  E ) )  <-> 
( ( # `  O
)  -  ( # `  ( O  \  E
) ) )  =  ( # `  E
) )
4126, 40mpbi 201 . . . . . 6  |-  ( (
# `  O )  -  ( # `  ( O  \  E ) ) )  =  ( # `  E )
4241oveq1i 5829 . . . . 5  |-  ( ( ( # `  O
)  -  ( # `  ( O  \  E
) ) )  / 
( # `  O ) )  =  ( (
# `  E )  /  ( # `  O
) )
4323, 42eqtr4i 2307 . . . 4  |-  ( P `
 E )  =  ( ( ( # `  O )  -  ( # `
 ( O  \  E ) ) )  /  ( # `  O
) )
44 ballotth.m . . . . . . . 8  |-  M  e.  NN
45 ballotth.n . . . . . . . 8  |-  N  e.  NN
4644, 45, 8ballotlem1 23038 . . . . . . 7  |-  ( # `  O )  =  ( ( M  +  N
)  _C  M )
4744nnnn0i 9968 . . . . . . . . . 10  |-  M  e. 
NN0
4844, 45pm3.2i 443 . . . . . . . . . . . 12  |-  ( M  e.  NN  /\  N  e.  NN )
49 nnaddcl 9763 . . . . . . . . . . . 12  |-  ( ( M  e.  NN  /\  N  e.  NN )  ->  ( M  +  N
)  e.  NN )
5048, 49ax-mp 10 . . . . . . . . . . 11  |-  ( M  +  N )  e.  NN
5150nnnn0i 9968 . . . . . . . . . 10  |-  ( M  +  N )  e. 
NN0
5244nnrei 9750 . . . . . . . . . . 11  |-  M  e.  RR
5345nnnn0i 9968 . . . . . . . . . . 11  |-  N  e. 
NN0
5452, 53nn0addge1i 10007 . . . . . . . . . 10  |-  M  <_ 
( M  +  N
)
55 elfz2nn0 10815 . . . . . . . . . 10  |-  ( M  e.  ( 0 ... ( M  +  N
) )  <->  ( M  e.  NN0  /\  ( M  +  N )  e. 
NN0  /\  M  <_  ( M  +  N ) ) )
5647, 51, 54, 55mpbir3an 1136 . . . . . . . . 9  |-  M  e.  ( 0 ... ( M  +  N )
)
57 bccl2 11329 . . . . . . . . 9  |-  ( M  e.  ( 0 ... ( M  +  N
) )  ->  (
( M  +  N
)  _C  M )  e.  NN )
5856, 57ax-mp 10 . . . . . . . 8  |-  ( ( M  +  N )  _C  M )  e.  NN
5958nnne0i 9775 . . . . . . 7  |-  ( ( M  +  N )  _C  M )  =/=  0
6046, 59eqnetri 2464 . . . . . 6  |-  ( # `  O )  =/=  0
6129, 60pm3.2i 443 . . . . 5  |-  ( (
# `  O )  e.  CC  /\  ( # `  O )  =/=  0
)
62 divsubdir 9451 . . . . 5  |-  ( ( ( # `  O
)  e.  CC  /\  ( # `  ( O 
\  E ) )  e.  CC  /\  (
( # `  O )  e.  CC  /\  ( # `
 O )  =/=  0 ) )  -> 
( ( ( # `  O )  -  ( # `
 ( O  \  E ) ) )  /  ( # `  O
) )  =  ( ( ( # `  O
)  /  ( # `  O ) )  -  ( ( # `  ( O  \  E ) )  /  ( # `  O
) ) ) )
6329, 38, 61, 62mp3an 1279 . . . 4  |-  ( ( ( # `  O
)  -  ( # `  ( O  \  E
) ) )  / 
( # `  O ) )  =  ( ( ( # `  O
)  /  ( # `  O ) )  -  ( ( # `  ( O  \  E ) )  /  ( # `  O
) ) )
6429, 60dividi 9488 . . . . 5  |-  ( (
# `  O )  /  ( # `  O
) )  =  1
6564oveq1i 5829 . . . 4  |-  ( ( ( # `  O
)  /  ( # `  O ) )  -  ( ( # `  ( O  \  E ) )  /  ( # `  O
) ) )  =  ( 1  -  (
( # `  ( O 
\  E ) )  /  ( # `  O
) ) )
6643, 63, 653eqtri 2308 . . 3  |-  ( P `
 E )  =  ( 1  -  (
( # `  ( O 
\  E ) )  /  ( # `  O
) ) )
67 ballotth.f . . . . . . . 8  |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
( 1 ... i
)  i^i  c )
)  -  ( # `  ( ( 1 ... i )  \  c
) ) ) ) )
68 ballotth.mgtn . . . . . . . 8  |-  N  < 
M
69 ballotth.i . . . . . . . 8  |-  I  =  ( c  e.  ( O  \  E ) 
|->  sup ( { k  e.  ( 1 ... ( M  +  N
) )  |  ( ( F `  c
) `  k )  =  0 } ,  RR ,  `'  <  ) )
70 ballotth.s . . . . . . . 8  |-  S  =  ( c  e.  ( O  \  E ) 
|->  ( i  e.  ( 1 ... ( M  +  N ) ) 
|->  if ( i  <_ 
( I `  c
) ,  ( ( ( I `  c
)  +  1 )  -  i ) ,  i ) ) )
71 ballotth.r . . . . . . . 8  |-  R  =  ( c  e.  ( O  \  E ) 
|->  ( ( S `  c ) " c
) )
7244, 45, 8, 19, 67, 1, 68, 69, 70, 71ballotlem8 23088 . . . . . . 7  |-  ( # `  { c  e.  ( O  \  E )  |  1  e.  c } )  =  (
# `  { c  e.  ( O  \  E
)  |  -.  1  e.  c } )
7372oveq1i 5829 . . . . . 6  |-  ( (
# `  { c  e.  ( O  \  E
)  |  1  e.  c } )  +  ( # `  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } ) )  =  ( ( # `  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } )  +  (
# `  { c  e.  ( O  \  E
)  |  -.  1  e.  c } ) )
7473oveq1i 5829 . . . . 5  |-  ( ( ( # `  {
c  e.  ( O 
\  E )  |  1  e.  c } )  +  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } ) )  /  ( # `  O
) )  =  ( ( ( # `  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } )  +  (
# `  { c  e.  ( O  \  E
)  |  -.  1  e.  c } ) )  /  ( # `  O
) )
75 rabxm 3478 . . . . . . . 8  |-  ( O 
\  E )  =  ( { c  e.  ( O  \  E
)  |  1  e.  c }  u.  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } )
7675fveq2i 5488 . . . . . . 7  |-  ( # `  ( O  \  E
) )  =  (
# `  ( {
c  e.  ( O 
\  E )  |  1  e.  c }  u.  { c  e.  ( O  \  E
)  |  -.  1  e.  c } ) )
77 ssrab2 3259 . . . . . . . . . . 11  |-  { c  e.  ( O  \  E )  |  1  e.  c }  C_  ( O  \  E )
7877, 33sstri 3189 . . . . . . . . . 10  |-  { c  e.  ( O  \  E )  |  1  e.  c }  C_  O
7978, 10sstri 3189 . . . . . . . . 9  |-  { c  e.  ( O  \  E )  |  1  e.  c }  C_  ~P ( 1 ... ( M  +  N )
)
80 ssfi 7078 . . . . . . . . 9  |-  ( ( ~P ( 1 ... ( M  +  N
) )  e.  Fin  /\ 
{ c  e.  ( O  \  E )  |  1  e.  c }  C_  ~P (
1 ... ( M  +  N ) ) )  ->  { c  e.  ( O  \  E
)  |  1  e.  c }  e.  Fin )
816, 79, 80mp2an 655 . . . . . . . 8  |-  { c  e.  ( O  \  E )  |  1  e.  c }  e.  Fin
82 ssrab2 3259 . . . . . . . . . . 11  |-  { c  e.  ( O  \  E )  |  -.  1  e.  c }  C_  ( O  \  E
)
8382, 33sstri 3189 . . . . . . . . . 10  |-  { c  e.  ( O  \  E )  |  -.  1  e.  c }  C_  O
8483, 10sstri 3189 . . . . . . . . 9  |-  { c  e.  ( O  \  E )  |  -.  1  e.  c }  C_ 
~P ( 1 ... ( M  +  N
) )
85 ssfi 7078 . . . . . . . . 9  |-  ( ( ~P ( 1 ... ( M  +  N
) )  e.  Fin  /\ 
{ c  e.  ( O  \  E )  |  -.  1  e.  c }  C_  ~P ( 1 ... ( M  +  N )
) )  ->  { c  e.  ( O  \  E )  |  -.  1  e.  c }  e.  Fin )
866, 84, 85mp2an 655 . . . . . . . 8  |-  { c  e.  ( O  \  E )  |  -.  1  e.  c }  e.  Fin
87 rabnc 3479 . . . . . . . 8  |-  ( { c  e.  ( O 
\  E )  |  1  e.  c }  i^i  { c  e.  ( O  \  E
)  |  -.  1  e.  c } )  =  (/)
88 hashun 11358 . . . . . . . 8  |-  ( ( { c  e.  ( O  \  E )  |  1  e.  c }  e.  Fin  /\  { c  e.  ( O 
\  E )  |  -.  1  e.  c }  e.  Fin  /\  ( { c  e.  ( O  \  E )  |  1  e.  c }  i^i  { c  e.  ( O  \  E )  |  -.  1  e.  c }
)  =  (/) )  -> 
( # `  ( { c  e.  ( O 
\  E )  |  1  e.  c }  u.  { c  e.  ( O  \  E
)  |  -.  1  e.  c } ) )  =  ( ( # `  { c  e.  ( O  \  E )  |  1  e.  c } )  +  (
# `  { c  e.  ( O  \  E
)  |  -.  1  e.  c } ) ) )
8981, 86, 87, 88mp3an 1279 . . . . . . 7  |-  ( # `  ( { c  e.  ( O  \  E
)  |  1  e.  c }  u.  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } ) )  =  ( ( # `  {
c  e.  ( O 
\  E )  |  1  e.  c } )  +  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } ) )
9076, 89eqtri 2304 . . . . . 6  |-  ( # `  ( O  \  E
) )  =  ( ( # `  {
c  e.  ( O 
\  E )  |  1  e.  c } )  +  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } ) )
9190oveq1i 5829 . . . . 5  |-  ( (
# `  ( O  \  E ) )  / 
( # `  O ) )  =  ( ( ( # `  {
c  e.  ( O 
\  E )  |  1  e.  c } )  +  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } ) )  /  ( # `  O
) )
9244, 45, 8, 19ballotlem2 23040 . . . . . . . . 9  |-  ( P `
 { c  e.  O  |  -.  1  e.  c } )  =  ( N  /  ( M  +  N )
)
9344, 45, 8, 19, 67, 1ballotlem4 23050 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  O  ->  ( -.  1  e.  c  ->  -.  c  e.  E
) )
9493imdistani 673 . . . . . . . . . . . . . . . 16  |-  ( ( c  e.  O  /\  -.  1  e.  c
)  ->  ( c  e.  O  /\  -.  c  e.  E ) )
95 rabid 2717 . . . . . . . . . . . . . . . 16  |-  ( c  e.  { c  e.  O  |  -.  1  e.  c }  <->  ( c  e.  O  /\  -.  1  e.  c ) )
96 df-dif 3156 . . . . . . . . . . . . . . . . . 18  |-  ( O 
\  E )  =  { c  |  ( c  e.  O  /\  -.  c  e.  E
) }
9796eleq2i 2348 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  ( O  \  E )  <->  c  e.  { c  |  ( c  e.  O  /\  -.  c  e.  E ) } )
98 abid 2272 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  { c  |  ( c  e.  O  /\  -.  c  e.  E
) }  <->  ( c  e.  O  /\  -.  c  e.  E ) )
9997, 98bitri 242 . . . . . . . . . . . . . . . 16  |-  ( c  e.  ( O  \  E )  <->  ( c  e.  O  /\  -.  c  e.  E ) )
10094, 95, 993imtr4i 259 . . . . . . . . . . . . . . 15  |-  ( c  e.  { c  e.  O  |  -.  1  e.  c }  ->  c  e.  ( O  \  E
) )
10195simprbi 452 . . . . . . . . . . . . . . 15  |-  ( c  e.  { c  e.  O  |  -.  1  e.  c }  ->  -.  1  e.  c )
102 rabid 2717 . . . . . . . . . . . . . . . 16  |-  ( c  e.  { c  e.  ( O  \  E
)  |  -.  1  e.  c }  <->  ( c  e.  ( O  \  E
)  /\  -.  1  e.  c ) )
103102biimpri 199 . . . . . . . . . . . . . . 15  |-  ( ( c  e.  ( O 
\  E )  /\  -.  1  e.  c
)  ->  c  e.  { c  e.  ( O 
\  E )  |  -.  1  e.  c } )
104100, 101, 103syl2anc 644 . . . . . . . . . . . . . 14  |-  ( c  e.  { c  e.  O  |  -.  1  e.  c }  ->  c  e.  { c  e.  ( O  \  E )  |  -.  1  e.  c } )
105104ax-gen 1534 . . . . . . . . . . . . 13  |-  A. c
( c  e.  {
c  e.  O  |  -.  1  e.  c }  ->  c  e.  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } )
106 nfrab1 2721 . . . . . . . . . . . . . 14  |-  F/_ c { c  e.  O  |  -.  1  e.  c }
107 nfrab1 2721 . . . . . . . . . . . . . 14  |-  F/_ c { c  e.  ( O  \  E )  |  -.  1  e.  c }
108106, 107dfss2f 3172 . . . . . . . . . . . . 13  |-  ( { c  e.  O  |  -.  1  e.  c }  C_  { c  e.  ( O  \  E
)  |  -.  1  e.  c }  <->  A. c
( c  e.  {
c  e.  O  |  -.  1  e.  c }  ->  c  e.  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } ) )
109105, 108mpbir 202 . . . . . . . . . . . 12  |-  { c  e.  O  |  -.  1  e.  c }  C_ 
{ c  e.  ( O  \  E )  |  -.  1  e.  c }
110109, 83sstri 3189 . . . . . . . . . . 11  |-  { c  e.  O  |  -.  1  e.  c }  C_  O
11112elexi 2798 . . . . . . . . . . . . 13  |-  O  e. 
_V
112111rabex 4166 . . . . . . . . . . . 12  |-  { c  e.  O  |  -.  1  e.  c }  e.  _V
113112elpw 3632 . . . . . . . . . . 11  |-  ( { c  e.  O  |  -.  1  e.  c }  e.  ~P O  <->  { c  e.  O  |  -.  1  e.  c }  C_  O )
114110, 113mpbir 202 . . . . . . . . . 10  |-  { c  e.  O  |  -.  1  e.  c }  e.  ~P O
115 fveq2 5485 . . . . . . . . . . . 12  |-  ( x  =  { c  e.  O  |  -.  1  e.  c }  ->  ( # `
 x )  =  ( # `  {
c  e.  O  |  -.  1  e.  c } ) )
116115oveq1d 5834 . . . . . . . . . . 11  |-  ( x  =  { c  e.  O  |  -.  1  e.  c }  ->  (
( # `  x )  /  ( # `  O
) )  =  ( ( # `  {
c  e.  O  |  -.  1  e.  c } )  /  ( # `
 O ) ) )
117 ovex 5844 . . . . . . . . . . 11  |-  ( (
# `  { c  e.  O  |  -.  1  e.  c }
)  /  ( # `  O ) )  e. 
_V
118116, 19, 117fvmpt 5563 . . . . . . . . . 10  |-  ( { c  e.  O  |  -.  1  e.  c }  e.  ~P O  ->  ( P `  {
c  e.  O  |  -.  1  e.  c } )  =  ( ( # `  {
c  e.  O  |  -.  1  e.  c } )  /  ( # `
 O ) ) )
119114, 118ax-mp 10 . . . . . . . . 9  |-  ( P `
 { c  e.  O  |  -.  1  e.  c } )  =  ( ( # `  {
c  e.  O  |  -.  1  e.  c } )  /  ( # `
 O ) )
12092, 119eqtr3i 2306 . . . . . . . 8  |-  ( N  /  ( M  +  N ) )  =  ( ( # `  {
c  e.  O  |  -.  1  e.  c } )  /  ( # `
 O ) )
121 rabss2 3257 . . . . . . . . . . . 12  |-  ( ( O  \  E ) 
C_  O  ->  { c  e.  ( O  \  E )  |  -.  1  e.  c }  C_ 
{ c  e.  O  |  -.  1  e.  c } )
12233, 121ax-mp 10 . . . . . . . . . . 11  |-  { c  e.  ( O  \  E )  |  -.  1  e.  c }  C_ 
{ c  e.  O  |  -.  1  e.  c }
123109, 122eqssi 3196 . . . . . . . . . 10  |-  { c  e.  O  |  -.  1  e.  c }  =  { c  e.  ( O  \  E )  |  -.  1  e.  c }
124123fveq2i 5488 . . . . . . . . 9  |-  ( # `  { c  e.  O  |  -.  1  e.  c } )  =  (
# `  { c  e.  ( O  \  E
)  |  -.  1  e.  c } )
125124oveq1i 5829 . . . . . . . 8  |-  ( (
# `  { c  e.  O  |  -.  1  e.  c }
)  /  ( # `  O ) )  =  ( ( # `  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } )  /  ( # `
 O ) )
126120, 125eqtri 2304 . . . . . . 7  |-  ( N  /  ( M  +  N ) )  =  ( ( # `  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } )  /  ( # `
 O ) )
127126oveq2i 5830 . . . . . 6  |-  ( 2  x.  ( N  / 
( M  +  N
) ) )  =  ( 2  x.  (
( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c }
)  /  ( # `  O ) ) )
128 2cn 9811 . . . . . . 7  |-  2  e.  CC
129 hashcl 11344 . . . . . . . . 9  |-  ( { c  e.  ( O 
\  E )  |  -.  1  e.  c }  e.  Fin  ->  (
# `  { c  e.  ( O  \  E
)  |  -.  1  e.  c } )  e. 
NN0 )
13086, 129ax-mp 10 . . . . . . . 8  |-  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } )  e. 
NN0
131130nn0cni 9972 . . . . . . 7  |-  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } )  e.  CC
132 divass 9437 . . . . . . 7  |-  ( ( 2  e.  CC  /\  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c }
)  e.  CC  /\  ( ( # `  O
)  e.  CC  /\  ( # `  O )  =/=  0 ) )  ->  ( ( 2  x.  ( # `  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } ) )  / 
( # `  O ) )  =  ( 2  x.  ( ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } )  / 
( # `  O ) ) ) )
133128, 131, 61, 132mp3an 1279 . . . . . 6  |-  ( ( 2  x.  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } ) )  /  ( # `  O
) )  =  ( 2  x.  ( (
# `  { c  e.  ( O  \  E
)  |  -.  1  e.  c } )  / 
( # `  O ) ) )
1341312timesi 9840 . . . . . . 7  |-  ( 2  x.  ( # `  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } ) )  =  ( ( # `  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } )  +  (
# `  { c  e.  ( O  \  E
)  |  -.  1  e.  c } ) )
135134oveq1i 5829 . . . . . 6  |-  ( ( 2  x.  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } ) )  /  ( # `  O
) )  =  ( ( ( # `  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } )  +  (
# `  { c  e.  ( O  \  E
)  |  -.  1  e.  c } ) )  /  ( # `  O
) )
136127, 133, 1353eqtr2i 2310 . . . . 5  |-  ( 2  x.  ( N  / 
( M  +  N
) ) )  =  ( ( ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } )  +  ( # `  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } ) )  / 
( # `  O ) )
13774, 91, 1363eqtr4ri 2315 . . . 4  |-  ( 2  x.  ( N  / 
( M  +  N
) ) )  =  ( ( # `  ( O  \  E ) )  /  ( # `  O
) )
138137oveq2i 5830 . . 3  |-  ( 1  -  ( 2  x.  ( N  /  ( M  +  N )
) ) )  =  ( 1  -  (
( # `  ( O 
\  E ) )  /  ( # `  O
) ) )
13966, 138eqtr4i 2307 . 2  |-  ( P `
 E )  =  ( 1  -  (
2  x.  ( N  /  ( M  +  N ) ) ) )
14050nncni 9751 . . . 4  |-  ( M  +  N )  e.  CC
14145nncni 9751 . . . . 5  |-  N  e.  CC
142128, 141mulcli 8837 . . . 4  |-  ( 2  x.  N )  e.  CC
14350nnne0i 9775 . . . . 5  |-  ( M  +  N )  =/=  0
144140, 143pm3.2i 443 . . . 4  |-  ( ( M  +  N )  e.  CC  /\  ( M  +  N )  =/=  0 )
145 divsubdir 9451 . . . 4  |-  ( ( ( M  +  N
)  e.  CC  /\  ( 2  x.  N
)  e.  CC  /\  ( ( M  +  N )  e.  CC  /\  ( M  +  N
)  =/=  0 ) )  ->  ( (
( M  +  N
)  -  ( 2  x.  N ) )  /  ( M  +  N ) )  =  ( ( ( M  +  N )  / 
( M  +  N
) )  -  (
( 2  x.  N
)  /  ( M  +  N ) ) ) )
146140, 142, 144, 145mp3an 1279 . . 3  |-  ( ( ( M  +  N
)  -  ( 2  x.  N ) )  /  ( M  +  N ) )  =  ( ( ( M  +  N )  / 
( M  +  N
) )  -  (
( 2  x.  N
)  /  ( M  +  N ) ) )
1471412timesi 9840 . . . . . 6  |-  ( 2  x.  N )  =  ( N  +  N
)
148147oveq2i 5830 . . . . 5  |-  ( ( M  +  N )  -  ( 2  x.  N ) )  =  ( ( M  +  N )  -  ( N  +  N )
)
14944nncni 9751 . . . . . . 7  |-  M  e.  CC
150149, 141, 141, 141addsub4i 9137 . . . . . 6  |-  ( ( M  +  N )  -  ( N  +  N ) )  =  ( ( M  -  N )  +  ( N  -  N ) )
151141subidi 9112 . . . . . . 7  |-  ( N  -  N )  =  0
152151oveq2i 5830 . . . . . 6  |-  ( ( M  -  N )  +  ( N  -  N ) )  =  ( ( M  -  N )  +  0 )
153149, 141subcli 9117 . . . . . . 7  |-  ( M  -  N )  e.  CC
154153addid1i 8994 . . . . . 6  |-  ( ( M  -  N )  +  0 )  =  ( M  -  N
)
155150, 152, 1543eqtri 2308 . . . . 5  |-  ( ( M  +  N )  -  ( N  +  N ) )  =  ( M  -  N
)
156148, 155eqtri 2304 . . . 4  |-  ( ( M  +  N )  -  ( 2  x.  N ) )  =  ( M  -  N
)
157156oveq1i 5829 . . 3  |-  ( ( ( M  +  N
)  -  ( 2  x.  N ) )  /  ( M  +  N ) )  =  ( ( M  -  N )  /  ( M  +  N )
)
158140, 143dividi 9488 . . . 4  |-  ( ( M  +  N )  /  ( M  +  N ) )  =  1
159 divass 9437 . . . . 5  |-  ( ( 2  e.  CC  /\  N  e.  CC  /\  (
( M  +  N
)  e.  CC  /\  ( M  +  N
)  =/=  0 ) )  ->  ( (
2  x.  N )  /  ( M  +  N ) )  =  ( 2  x.  ( N  /  ( M  +  N ) ) ) )
160128, 141, 144, 159mp3an 1279 . . . 4  |-  ( ( 2  x.  N )  /  ( M  +  N ) )  =  ( 2  x.  ( N  /  ( M  +  N ) ) )
161158, 160oveq12i 5831 . . 3  |-  ( ( ( M  +  N
)  /  ( M  +  N ) )  -  ( ( 2  x.  N )  / 
( M  +  N
) ) )  =  ( 1  -  (
2  x.  ( N  /  ( M  +  N ) ) ) )
162146, 157, 1613eqtr3ri 2313 . 2  |-  ( 1  -  ( 2  x.  ( N  /  ( M  +  N )
) ) )  =  ( ( M  -  N )  /  ( M  +  N )
)
163139, 162eqtri 2304 1  |-  ( P `
 E )  =  ( ( M  -  N )  /  ( M  +  N )
)
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    /\ wa 360   A.wal 1528    = wceq 1624    e. wcel 1685   {cab 2270    =/= wne 2447   A.wral 2544   {crab 2548    \ cdif 3150    u. cun 3151    i^i cin 3152    C_ wss 3153   (/)c0 3456   ifcif 3566   ~Pcpw 3626   class class class wbr 4024    e. cmpt 4078   `'ccnv 4687   "cima 4691   ` cfv 5221  (class class class)co 5819   Fincfn 6858   supcsup 7188   CCcc 8730   RRcr 8731   0cc0 8732   1c1 8733    + caddc 8735    x. cmul 8737    < clt 8862    <_ cle 8863    - cmin 9032    / cdiv 9418   NNcn 9741   2c2 9790   NN0cn0 9960   ZZcz 10019   ...cfz 10776    _C cbc 11309   #chash 11331
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-rep 4132  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511  ax-cnex 8788  ax-resscn 8789  ax-1cn 8790  ax-icn 8791  ax-addcl 8792  ax-addrcl 8793  ax-mulcl 8794  ax-mulrcl 8795  ax-mulcom 8796  ax-addass 8797  ax-mulass 8798  ax-distr 8799  ax-i2m1 8800  ax-1ne0 8801  ax-1rid 8802  ax-rnegex 8803  ax-rrecex 8804  ax-cnre 8805  ax-pre-lttri 8806  ax-pre-lttrn 8807  ax-pre-ltadd 8808  ax-pre-mulgt0 8809
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-nel 2450  df-ral 2549  df-rex 2550  df-reu 2551  df-rmo 2552  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pss 3169  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-tp 3649  df-op 3650  df-uni 3829  df-int 3864  df-iun 3908  df-br 4025  df-opab 4079  df-mpt 4080  df-tr 4115  df-eprel 4304  df-id 4308  df-po 4313  df-so 4314  df-fr 4351  df-we 4353  df-ord 4394  df-on 4395  df-lim 4396  df-suc 4397  df-om 4656  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229  df-ov 5822  df-oprab 5823  df-mpt2 5824  df-1st 6083  df-2nd 6084  df-iota 6252  df-riota 6299  df-recs 6383  df-rdg 6418  df-1o 6474  df-2o 6475  df-oadd 6478  df-er 6655  df-map 6769  df-en 6859  df-dom 6860  df-sdom 6861  df-fin 6862  df-sup 7189  df-card 7567  df-cda 7789  df-pnf 8864  df-mnf 8865  df-xr 8866  df-ltxr 8867  df-le 8868  df-sub 9034  df-neg 9035  df-div 9419  df-nn 9742  df-2 9799  df-n0 9961  df-z 10020  df-uz 10226  df-rp 10350  df-fz 10777  df-seq 11041  df-fac 11283  df-bc 11310  df-hash 11332
  Copyright terms: Public domain W3C validator