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

Theorem ballotth 23043
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 3219 . . . . . . 7  |-  { c  e.  O  |  A. i  e.  ( 1 ... ( M  +  N ) ) 0  <  ( ( F `
 c ) `  i ) }  C_  O
31, 2eqsstri 3169 . . . . . 6  |-  E  C_  O
4 fzfi 10986 . . . . . . . . . . . 12  |-  ( 1 ... ( M  +  N ) )  e. 
Fin
5 pwfi 7105 . . . . . . . . . . . 12  |-  ( ( 1 ... ( M  +  N ) )  e.  Fin  <->  ~P (
1 ... ( M  +  N ) )  e. 
Fin )
64, 5mpbi 201 . . . . . . . . . . 11  |-  ~P (
1 ... ( M  +  N ) )  e. 
Fin
7 ssrab2 3219 . . . . . . . . . . . 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 3163 . . . . . . . . . . . 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 7037 . . . . . . . . . . 11  |-  ( ( ~P ( 1 ... ( M  +  N
) )  e.  Fin  /\  O  C_  ~P (
1 ... ( M  +  N ) ) )  ->  O  e.  Fin )
126, 10, 11mp2an 656 . . . . . . . . . 10  |-  O  e. 
Fin
13 ssfi 7037 . . . . . . . . . 10  |-  ( ( O  e.  Fin  /\  E  C_  O )  ->  E  e.  Fin )
1412, 3, 13mp2an 656 . . . . . . . . 9  |-  E  e. 
Fin
1514elexi 2766 . . . . . . . 8  |-  E  e. 
_V
1615elpw 3591 . . . . . . 7  |-  ( E  e.  ~P O  <->  E  C_  O
)
17 fveq2 5444 . . . . . . . . 9  |-  ( x  =  E  ->  ( # `
 x )  =  ( # `  E
) )
1817oveq1d 5793 . . . . . . . 8  |-  ( x  =  E  ->  (
( # `  x )  /  ( # `  O
) )  =  ( ( # `  E
)  /  ( # `  O ) ) )
19 ballotth.p . . . . . . . 8  |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `
 O ) ) )
20 ovex 5803 . . . . . . . 8  |-  ( (
# `  E )  /  ( # `  O
) )  e.  _V
2118, 19, 20fvmpt 5522 . . . . . . 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 11325 . . . . . . . . 9  |-  ( ( O  e.  Fin  /\  E  C_  O )  -> 
( # `  ( O 
\  E ) )  =  ( ( # `  O )  -  ( # `
 E ) ) )
2512, 3, 24mp2an 656 . . . . . . . 8  |-  ( # `  ( O  \  E
) )  =  ( ( # `  O
)  -  ( # `  E ) )
2625eqcomi 2260 . . . . . . 7  |-  ( (
# `  O )  -  ( # `  E
) )  =  (
# `  ( O  \  E ) )
27 hashcl 11302 . . . . . . . . . 10  |-  ( O  e.  Fin  ->  ( # `
 O )  e. 
NN0 )
2812, 27ax-mp 10 . . . . . . . . 9  |-  ( # `  O )  e.  NN0
2928nn0cni 9930 . . . . . . . 8  |-  ( # `  O )  e.  CC
30 hashcl 11302 . . . . . . . . . 10  |-  ( E  e.  Fin  ->  ( # `
 E )  e. 
NN0 )
3114, 30ax-mp 10 . . . . . . . . 9  |-  ( # `  E )  e.  NN0
3231nn0cni 9930 . . . . . . . 8  |-  ( # `  E )  e.  CC
33 difss 3264 . . . . . . . . . . 11  |-  ( O 
\  E )  C_  O
34 ssfi 7037 . . . . . . . . . . 11  |-  ( ( O  e.  Fin  /\  ( O  \  E ) 
C_  O )  -> 
( O  \  E
)  e.  Fin )
3512, 33, 34mp2an 656 . . . . . . . . . 10  |-  ( O 
\  E )  e. 
Fin
36 hashcl 11302 . . . . . . . . . 10  |-  ( ( O  \  E )  e.  Fin  ->  ( # `
 ( O  \  E ) )  e. 
NN0 )
3735, 36ax-mp 10 . . . . . . . . 9  |-  ( # `  ( O  \  E
) )  e.  NN0
3837nn0cni 9930 . . . . . . . 8  |-  ( # `  ( O  \  E
) )  e.  CC
39 subsub23 9010 . . . . . . . 8  |-  ( ( ( # `  O
)  e.  CC  /\  ( # `  E )  e.  CC  /\  ( # `
 ( O  \  E ) )  e.  CC )  ->  (
( ( # `  O
)  -  ( # `  E ) )  =  ( # `  ( O  \  E ) )  <-> 
( ( # `  O
)  -  ( # `  ( O  \  E
) ) )  =  ( # `  E
) ) )
4029, 32, 38, 39mp3an 1282 . . . . . . 7  |-  ( ( ( # `  O
)  -  ( # `  E ) )  =  ( # `  ( O  \  E ) )  <-> 
( ( # `  O
)  -  ( # `  ( O  \  E
) ) )  =  ( # `  E
) )
4126, 40mpbi 201 . . . . . 6  |-  ( (
# `  O )  -  ( # `  ( O  \  E ) ) )  =  ( # `  E )
4241oveq1i 5788 . . . . 5  |-  ( ( ( # `  O
)  -  ( # `  ( O  \  E
) ) )  / 
( # `  O ) )  =  ( (
# `  E )  /  ( # `  O
) )
4323, 42eqtr4i 2279 . . . 4  |-  ( P `
 E )  =  ( ( ( # `  O )  -  ( # `
 ( O  \  E ) ) )  /  ( # `  O
) )
44 ballotth.m . . . . . . . 8  |-  M  e.  NN
45 ballotth.n . . . . . . . 8  |-  N  e.  NN
4644, 45, 8ballotlem1 22992 . . . . . . 7  |-  ( # `  O )  =  ( ( M  +  N
)  _C  M )
4744nnnn0i 9926 . . . . . . . . . 10  |-  M  e. 
NN0
4844, 45pm3.2i 443 . . . . . . . . . . . 12  |-  ( M  e.  NN  /\  N  e.  NN )
49 nnaddcl 9722 . . . . . . . . . . . 12  |-  ( ( M  e.  NN  /\  N  e.  NN )  ->  ( M  +  N
)  e.  NN )
5048, 49ax-mp 10 . . . . . . . . . . 11  |-  ( M  +  N )  e.  NN
5150nnnn0i 9926 . . . . . . . . . 10  |-  ( M  +  N )  e. 
NN0
5244nnrei 9709 . . . . . . . . . . 11  |-  M  e.  RR
5345nnnn0i 9926 . . . . . . . . . . 11  |-  N  e. 
NN0
5452, 53nn0addge1i 9965 . . . . . . . . . 10  |-  M  <_ 
( M  +  N
)
55 elfz2nn0 10773 . . . . . . . . . 10  |-  ( M  e.  ( 0 ... ( M  +  N
) )  <->  ( M  e.  NN0  /\  ( M  +  N )  e. 
NN0  /\  M  <_  ( M  +  N ) ) )
5647, 51, 54, 55mpbir3an 1139 . . . . . . . . 9  |-  M  e.  ( 0 ... ( M  +  N )
)
57 bccl2 11287 . . . . . . . . 9  |-  ( M  e.  ( 0 ... ( M  +  N
) )  ->  (
( M  +  N
)  _C  M )  e.  NN )
5856, 57ax-mp 10 . . . . . . . 8  |-  ( ( M  +  N )  _C  M )  e.  NN
5958nnne0i 9734 . . . . . . 7  |-  ( ( M  +  N )  _C  M )  =/=  0
6046, 59eqnetri 2436 . . . . . 6  |-  ( # `  O )  =/=  0
6129, 60pm3.2i 443 . . . . 5  |-  ( (
# `  O )  e.  CC  /\  ( # `  O )  =/=  0
)
62 divsubdir 9410 . . . . 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 1282 . . . 4  |-  ( ( ( # `  O
)  -  ( # `  ( O  \  E
) ) )  / 
( # `  O ) )  =  ( ( ( # `  O
)  /  ( # `  O ) )  -  ( ( # `  ( O  \  E ) )  /  ( # `  O
) ) )
6429, 60dividi 9447 . . . . 5  |-  ( (
# `  O )  /  ( # `  O
) )  =  1
6564oveq1i 5788 . . . 4  |-  ( ( ( # `  O
)  /  ( # `  O ) )  -  ( ( # `  ( O  \  E ) )  /  ( # `  O
) ) )  =  ( 1  -  (
( # `  ( O 
\  E ) )  /  ( # `  O
) ) )
6643, 63, 653eqtri 2280 . . 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 23042 . . . . . . 7  |-  ( # `  { c  e.  ( O  \  E )  |  1  e.  c } )  =  (
# `  { c  e.  ( O  \  E
)  |  -.  1  e.  c } )
7372oveq1i 5788 . . . . . 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 5788 . . . . 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 3438 . . . . . . . 8  |-  ( O 
\  E )  =  ( { c  e.  ( O  \  E
)  |  1  e.  c }  u.  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } )
7675fveq2i 5447 . . . . . . 7  |-  ( # `  ( O  \  E
) )  =  (
# `  ( {
c  e.  ( O 
\  E )  |  1  e.  c }  u.  { c  e.  ( O  \  E
)  |  -.  1  e.  c } ) )
77 ssrab2 3219 . . . . . . . . . . 11  |-  { c  e.  ( O  \  E )  |  1  e.  c }  C_  ( O  \  E )
7877, 33sstri 3149 . . . . . . . . . 10  |-  { c  e.  ( O  \  E )  |  1  e.  c }  C_  O
7978, 10sstri 3149 . . . . . . . . 9  |-  { c  e.  ( O  \  E )  |  1  e.  c }  C_  ~P ( 1 ... ( M  +  N )
)
80 ssfi 7037 . . . . . . . . 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 656 . . . . . . . 8  |-  { c  e.  ( O  \  E )  |  1  e.  c }  e.  Fin
82 ssrab2 3219 . . . . . . . . . . 11  |-  { c  e.  ( O  \  E )  |  -.  1  e.  c }  C_  ( O  \  E
)
8382, 33sstri 3149 . . . . . . . . . 10  |-  { c  e.  ( O  \  E )  |  -.  1  e.  c }  C_  O
8483, 10sstri 3149 . . . . . . . . 9  |-  { c  e.  ( O  \  E )  |  -.  1  e.  c }  C_ 
~P ( 1 ... ( M  +  N
) )
85 ssfi 7037 . . . . . . . . 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 656 . . . . . . . 8  |-  { c  e.  ( O  \  E )  |  -.  1  e.  c }  e.  Fin
87 rabnc 3439 . . . . . . . 8  |-  ( { c  e.  ( O 
\  E )  |  1  e.  c }  i^i  { c  e.  ( O  \  E
)  |  -.  1  e.  c } )  =  (/)
88 hashun 11316 . . . . . . . 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 1282 . . . . . . 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 2276 . . . . . 6  |-  ( # `  ( O  \  E
) )  =  ( ( # `  {
c  e.  ( O 
\  E )  |  1  e.  c } )  +  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } ) )
9190oveq1i 5788 . . . . 5  |-  ( (
# `  ( O  \  E ) )  / 
( # `  O ) )  =  ( ( ( # `  {
c  e.  ( O 
\  E )  |  1  e.  c } )  +  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } ) )  /  ( # `  O
) )
9244, 45, 8, 19ballotlem2 22994 . . . . . . . . 9  |-  ( P `
 { c  e.  O  |  -.  1  e.  c } )  =  ( N  /  ( M  +  N )
)
9344, 45, 8, 19, 67, 1ballotlem4 23004 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  O  ->  ( -.  1  e.  c  ->  -.  c  e.  E
) )
9493imdistani 674 . . . . . . . . . . . . . . . 16  |-  ( ( c  e.  O  /\  -.  1  e.  c
)  ->  ( c  e.  O  /\  -.  c  e.  E ) )
95 rabid 2689 . . . . . . . . . . . . . . . 16  |-  ( c  e.  { c  e.  O  |  -.  1  e.  c }  <->  ( c  e.  O  /\  -.  1  e.  c ) )
96 df-dif 3116 . . . . . . . . . . . . . . . . . 18  |-  ( O 
\  E )  =  { c  |  ( c  e.  O  /\  -.  c  e.  E
) }
9796eleq2i 2320 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  ( O  \  E )  <->  c  e.  { c  |  ( c  e.  O  /\  -.  c  e.  E ) } )
98 abid 2244 . . . . . . . . . . . . . . . . 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 2689 . . . . . . . . . . . . . . . 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 645 . . . . . . . . . . . . . 14  |-  ( c  e.  { c  e.  O  |  -.  1  e.  c }  ->  c  e.  { c  e.  ( O  \  E )  |  -.  1  e.  c } )
105104ax-gen 1536 . . . . . . . . . . . . 13  |-  A. c
( c  e.  {
c  e.  O  |  -.  1  e.  c }  ->  c  e.  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } )
106 nfrab1 2693 . . . . . . . . . . . . . 14  |-  F/_ c { c  e.  O  |  -.  1  e.  c }
107 nfrab1 2693 . . . . . . . . . . . . . 14  |-  F/_ c { c  e.  ( O  \  E )  |  -.  1  e.  c }
108106, 107dfss2f 3132 . . . . . . . . . . . . 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 3149 . . . . . . . . . . 11  |-  { c  e.  O  |  -.  1  e.  c }  C_  O
11112elexi 2766 . . . . . . . . . . . . 13  |-  O  e. 
_V
112111rabex 4125 . . . . . . . . . . . 12  |-  { c  e.  O  |  -.  1  e.  c }  e.  _V
113112elpw 3591 . . . . . . . . . . 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 5444 . . . . . . . . . . . 12  |-  ( x  =  { c  e.  O  |  -.  1  e.  c }  ->  ( # `
 x )  =  ( # `  {
c  e.  O  |  -.  1  e.  c } ) )
116115oveq1d 5793 . . . . . . . . . . 11  |-  ( x  =  { c  e.  O  |  -.  1  e.  c }  ->  (
( # `  x )  /  ( # `  O
) )  =  ( ( # `  {
c  e.  O  |  -.  1  e.  c } )  /  ( # `
 O ) ) )
117 ovex 5803 . . . . . . . . . . 11  |-  ( (
# `  { c  e.  O  |  -.  1  e.  c }
)  /  ( # `  O ) )  e. 
_V
118116, 19, 117fvmpt 5522 . . . . . . . . . 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 2278 . . . . . . . 8  |-  ( N  /  ( M  +  N ) )  =  ( ( # `  {
c  e.  O  |  -.  1  e.  c } )  /  ( # `
 O ) )
121 rabss2 3217 . . . . . . . . . . . 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 3156 . . . . . . . . . 10  |-  { c  e.  O  |  -.  1  e.  c }  =  { c  e.  ( O  \  E )  |  -.  1  e.  c }
124123fveq2i 5447 . . . . . . . . 9  |-  ( # `  { c  e.  O  |  -.  1  e.  c } )  =  (
# `  { c  e.  ( O  \  E
)  |  -.  1  e.  c } )
125124oveq1i 5788 . . . . . . . 8  |-  ( (
# `  { c  e.  O  |  -.  1  e.  c }
)  /  ( # `  O ) )  =  ( ( # `  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } )  /  ( # `
 O ) )
126120, 125eqtri 2276 . . . . . . 7  |-  ( N  /  ( M  +  N ) )  =  ( ( # `  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } )  /  ( # `
 O ) )
127126oveq2i 5789 . . . . . 6  |-  ( 2  x.  ( N  / 
( M  +  N
) ) )  =  ( 2  x.  (
( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c }
)  /  ( # `  O ) ) )
128 2cn 9770 . . . . . . 7  |-  2  e.  CC
129 hashcl 11302 . . . . . . . . 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 9930 . . . . . . 7  |-  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } )  e.  CC
132 divass 9396 . . . . . . 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 1282 . . . . . 6  |-  ( ( 2  x.  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } ) )  /  ( # `  O
) )  =  ( 2  x.  ( (
# `  { c  e.  ( O  \  E
)  |  -.  1  e.  c } )  / 
( # `  O ) ) )
1341312timesi 9798 . . . . . . 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 5788 . . . . . 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 2282 . . . . 5  |-  ( 2  x.  ( N  / 
( M  +  N
) ) )  =  ( ( ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } )  +  ( # `  {
c  e.  ( O 
\  E )  |  -.  1  e.  c } ) )  / 
( # `  O ) )
13774, 91, 1363eqtr4ri 2287 . . . 4  |-  ( 2  x.  ( N  / 
( M  +  N
) ) )  =  ( ( # `  ( O  \  E ) )  /  ( # `  O
) )
138137oveq2i 5789 . . 3  |-  ( 1  -  ( 2  x.  ( N  /  ( M  +  N )
) ) )  =  ( 1  -  (
( # `  ( O 
\  E ) )  /  ( # `  O
) ) )
13966, 138eqtr4i 2279 . 2  |-  ( P `
 E )  =  ( 1  -  (
2  x.  ( N  /  ( M  +  N ) ) ) )
14050nncni 9710 . . . 4  |-  ( M  +  N )  e.  CC
14145nncni 9710 . . . . 5  |-  N  e.  CC
142128, 141mulcli 8796 . . . 4  |-  ( 2  x.  N )  e.  CC
14350nnne0i 9734 . . . . 5  |-  ( M  +  N )  =/=  0
144140, 143pm3.2i 443 . . . 4  |-  ( ( M  +  N )  e.  CC  /\  ( M  +  N )  =/=  0 )
145 divsubdir 9410 . . . 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 1282 . . 3  |-  ( ( ( M  +  N
)  -  ( 2  x.  N ) )  /  ( M  +  N ) )  =  ( ( ( M  +  N )  / 
( M  +  N
) )  -  (
( 2  x.  N
)  /  ( M  +  N ) ) )
1471412timesi 9798 . . . . . 6  |-  ( 2  x.  N )  =  ( N  +  N
)
148147oveq2i 5789 . . . . 5  |-  ( ( M  +  N )  -  ( 2  x.  N ) )  =  ( ( M  +  N )  -  ( N  +  N )
)
14944nncni 9710 . . . . . . 7  |-  M  e.  CC
150149, 141, 141, 141addsub4i 9096 . . . . . 6  |-  ( ( M  +  N )  -  ( N  +  N ) )  =  ( ( M  -  N )  +  ( N  -  N ) )
151141subidi 9071 . . . . . . 7  |-  ( N  -  N )  =  0
152151oveq2i 5789 . . . . . 6  |-  ( ( M  -  N )  +  ( N  -  N ) )  =  ( ( M  -  N )  +  0 )
153149, 141subcli 9076 . . . . . . 7  |-  ( M  -  N )  e.  CC
154153addid1i 8953 . . . . . 6  |-  ( ( M  -  N )  +  0 )  =  ( M  -  N
)
155150, 152, 1543eqtri 2280 . . . . 5  |-  ( ( M  +  N )  -  ( N  +  N ) )  =  ( M  -  N
)
156148, 155eqtri 2276 . . . 4  |-  ( ( M  +  N )  -  ( 2  x.  N ) )  =  ( M  -  N
)
157156oveq1i 5788 . . 3  |-  ( ( ( M  +  N
)  -  ( 2  x.  N ) )  /  ( M  +  N ) )  =  ( ( M  -  N )  /  ( M  +  N )
)
158140, 143dividi 9447 . . . 4  |-  ( ( M  +  N )  /  ( M  +  N ) )  =  1
159 divass 9396 . . . . 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 1282 . . . 4  |-  ( ( 2  x.  N )  /  ( M  +  N ) )  =  ( 2  x.  ( N  /  ( M  +  N ) ) )
161158, 160oveq12i 5790 . . 3  |-  ( ( ( M  +  N
)  /  ( M  +  N ) )  -  ( ( 2  x.  N )  / 
( M  +  N
) ) )  =  ( 1  -  (
2  x.  ( N  /  ( M  +  N ) ) ) )
162146, 157, 1613eqtr3ri 2285 . 2  |-  ( 1  -  ( 2  x.  ( N  /  ( M  +  N )
) ) )  =  ( ( M  -  N )  /  ( M  +  N )
)
163139, 162eqtri 2276 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 1532    = wceq 1619    e. wcel 1621   {cab 2242    =/= wne 2419   A.wral 2516   {crab 2520    \ cdif 3110    u. cun 3111    i^i cin 3112    C_ wss 3113   (/)c0 3416   ifcif 3525   ~Pcpw 3585   class class class wbr 3983    e. cmpt 4037   `'ccnv 4646   "cima 4650   ` cfv 4659  (class class class)co 5778   Fincfn 6817   supcsup 7147   CCcc 8689   RRcr 8690   0cc0 8691   1c1 8692    + caddc 8694    x. cmul 8696    < clt 8821    <_ cle 8822    - cmin 8991    / cdiv 9377   NNcn 9700   2c2 9749   NN0cn0 9918   ZZcz 9977   ...cfz 10734    _C cbc 11267   #chash 11289
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-rep 4091  ax-sep 4101  ax-nul 4109  ax-pow 4146  ax-pr 4172  ax-un 4470  ax-cnex 8747  ax-resscn 8748  ax-1cn 8749  ax-icn 8750  ax-addcl 8751  ax-addrcl 8752  ax-mulcl 8753  ax-mulrcl 8754  ax-mulcom 8755  ax-addass 8756  ax-mulass 8757  ax-distr 8758  ax-i2m1 8759  ax-1ne0 8760  ax-1rid 8761  ax-rnegex 8762  ax-rrecex 8763  ax-cnre 8764  ax-pre-lttri 8765  ax-pre-lttrn 8766  ax-pre-ltadd 8767  ax-pre-mulgt0 8768
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-nel 2422  df-ral 2521  df-rex 2522  df-reu 2523  df-rmo 2524  df-rab 2525  df-v 2759  df-sbc 2953  df-csb 3043  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-pss 3129  df-nul 3417  df-if 3526  df-pw 3587  df-sn 3606  df-pr 3607  df-tp 3608  df-op 3609  df-uni 3788  df-int 3823  df-iun 3867  df-br 3984  df-opab 4038  df-mpt 4039  df-tr 4074  df-eprel 4263  df-id 4267  df-po 4272  df-so 4273  df-fr 4310  df-we 4312  df-ord 4353  df-on 4354  df-lim 4355  df-suc 4356  df-om 4615  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fun 4669  df-fn 4670  df-f 4671  df-f1 4672  df-fo 4673  df-f1o 4674  df-fv 4675  df-ov 5781  df-oprab 5782  df-mpt2 5783  df-1st 6042  df-2nd 6043  df-iota 6211  df-riota 6258  df-recs 6342  df-rdg 6377  df-1o 6433  df-2o 6434  df-oadd 6437  df-er 6614  df-map 6728  df-en 6818  df-dom 6819  df-sdom 6820  df-fin 6821  df-sup 7148  df-card 7526  df-cda 7748  df-pnf 8823  df-mnf 8824  df-xr 8825  df-ltxr 8826  df-le 8827  df-sub 8993  df-neg 8994  df-div 9378  df-n 9701  df-2 9758  df-n0 9919  df-z 9978  df-uz 10184  df-rp 10308  df-fz 10735  df-seq 10999  df-fac 11241  df-bc 11268  df-hash 11290
  Copyright terms: Public domain W3C validator