Users' Mathboxes Mathbox for Jim Kingdon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  trilpolemlt1 Unicode version

Theorem trilpolemlt1 13045
Description: Lemma for trilpo 13047. The  A  <  1 case. We can use the distance between  A and one (that is,  1  -  A) to find a position in the sequence  n where terms after that point will not add up to as much as  1  -  A. By finomni 6978 we know the terms up to  n either contain a zero or are all one. But if they are all one that contradicts the way we constructed  n, so we know that the sequence contains a zero. (Contributed by Jim Kingdon, 23-Aug-2023.)
Hypotheses
Ref Expression
trilpolemgt1.f  |-  ( ph  ->  F : NN --> { 0 ,  1 } )
trilpolemgt1.a  |-  A  = 
sum_ i  e.  NN  ( ( 1  / 
( 2 ^ i
) )  x.  ( F `  i )
)
trilpolemlt1.a  |-  ( ph  ->  A  <  1 )
Assertion
Ref Expression
trilpolemlt1  |-  ( ph  ->  E. x  e.  NN  ( F `  x )  =  0 )
Distinct variable groups:    A, i, x   
x, F, i    ph, i, x

Proof of Theorem trilpolemlt1
Dummy variables  n  f  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1red 7745 . . . 4  |-  ( ph  ->  1  e.  RR )
2 trilpolemgt1.f . . . . 5  |-  ( ph  ->  F : NN --> { 0 ,  1 } )
3 trilpolemgt1.a . . . . 5  |-  A  = 
sum_ i  e.  NN  ( ( 1  / 
( 2 ^ i
) )  x.  ( F `  i )
)
42, 3trilpolemcl 13041 . . . 4  |-  ( ph  ->  A  e.  RR )
51, 4resubcld 8107 . . 3  |-  ( ph  ->  ( 1  -  A
)  e.  RR )
6 trilpolemlt1.a . . . 4  |-  ( ph  ->  A  <  1 )
74, 1posdifd 8257 . . . 4  |-  ( ph  ->  ( A  <  1  <->  0  <  ( 1  -  A ) ) )
86, 7mpbid 146 . . 3  |-  ( ph  ->  0  <  ( 1  -  A ) )
9 nnrecl 8926 . . 3  |-  ( ( ( 1  -  A
)  e.  RR  /\  0  <  ( 1  -  A ) )  ->  E. n  e.  NN  ( 1  /  n
)  <  ( 1  -  A ) )
105, 8, 9syl2anc 406 . 2  |-  ( ph  ->  E. n  e.  NN  ( 1  /  n
)  <  ( 1  -  A ) )
11 elfznn 9774 . . . . . . 7  |-  ( x  e.  ( 1 ... n )  ->  x  e.  NN )
1211ad2antrl 479 . . . . . 6  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  ( x  e.  ( 1 ... n )  /\  (
( F  |`  (
1 ... n ) ) `
 x )  =  0 ) )  ->  x  e.  NN )
13 simprl 503 . . . . . . . 8  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  ( x  e.  ( 1 ... n )  /\  (
( F  |`  (
1 ... n ) ) `
 x )  =  0 ) )  ->  x  e.  ( 1 ... n ) )
1413fvresd 5412 . . . . . . 7  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  ( x  e.  ( 1 ... n )  /\  (
( F  |`  (
1 ... n ) ) `
 x )  =  0 ) )  -> 
( ( F  |`  ( 1 ... n
) ) `  x
)  =  ( F `
 x ) )
15 simprr 504 . . . . . . 7  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  ( x  e.  ( 1 ... n )  /\  (
( F  |`  (
1 ... n ) ) `
 x )  =  0 ) )  -> 
( ( F  |`  ( 1 ... n
) ) `  x
)  =  0 )
1614, 15eqtr3d 2150 . . . . . 6  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  ( x  e.  ( 1 ... n )  /\  (
( F  |`  (
1 ... n ) ) `
 x )  =  0 ) )  -> 
( F `  x
)  =  0 )
1712, 16jca 302 . . . . 5  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  ( x  e.  ( 1 ... n )  /\  (
( F  |`  (
1 ... n ) ) `
 x )  =  0 ) )  -> 
( x  e.  NN  /\  ( F `  x
)  =  0 ) )
1817ex 114 . . . 4  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( ( x  e.  ( 1 ... n
)  /\  ( ( F  |`  ( 1 ... n ) ) `  x )  =  0 )  ->  ( x  e.  NN  /\  ( F `
 x )  =  0 ) ) )
1918reximdv2 2506 . . 3  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( E. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  0  ->  E. x  e.  NN  ( F `  x )  =  0 ) )
20 2rp 9395 . . . . . . . . . 10  |-  2  e.  RR+
2120a1i 9 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
2  e.  RR+ )
22 simprl 503 . . . . . . . . . 10  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  n  e.  NN )
2322nnzd 9123 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  n  e.  ZZ )
2421, 23rpexpcld 10388 . . . . . . . 8  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 2 ^ n
)  e.  RR+ )
2524rprecred 9441 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1  /  (
2 ^ n ) )  e.  RR )
2622nnrecred 8724 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1  /  n
)  e.  RR )
275adantr 272 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1  -  A
)  e.  RR )
28 2z 9033 . . . . . . . . . 10  |-  2  e.  ZZ
29 uzid 9289 . . . . . . . . . 10  |-  ( 2  e.  ZZ  ->  2  e.  ( ZZ>= `  2 )
)
3028, 29mp1i 10 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
2  e.  ( ZZ>= ` 
2 ) )
3122nnnn0d 8981 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  n  e.  NN0 )
32 bernneq3 10354 . . . . . . . . 9  |-  ( ( 2  e.  ( ZZ>= ` 
2 )  /\  n  e.  NN0 )  ->  n  <  ( 2 ^ n
) )
3330, 31, 32syl2anc 406 . . . . . . . 8  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  n  <  ( 2 ^ n ) )
3422nnrpd 9428 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  n  e.  RR+ )
3534, 24ltrecd 9448 . . . . . . . 8  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( n  <  (
2 ^ n )  <-> 
( 1  /  (
2 ^ n ) )  <  ( 1  /  n ) ) )
3633, 35mpbid 146 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1  /  (
2 ^ n ) )  <  ( 1  /  n ) )
37 simprr 504 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1  /  n
)  <  ( 1  -  A ) )
3825, 26, 27, 36, 37lttrd 7852 . . . . . 6  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1  /  (
2 ^ n ) )  <  ( 1  -  A ) )
3938adantr 272 . . . . 5  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( 1  / 
( 2 ^ n
) )  <  (
1  -  A ) )
4027adantr 272 . . . . . 6  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( 1  -  A )  e.  RR )
4125adantr 272 . . . . . 6  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( 1  / 
( 2 ^ n
) )  e.  RR )
42 1red 7745 . . . . . . 7  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  1  e.  RR )
434ad2antrr 477 . . . . . . 7  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  A  e.  RR )
44 0red 7731 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  0  e.  RR )
45 eqid 2115 . . . . . . . . . . 11  |-  ( ZZ>= `  ( n  +  1
) )  =  (
ZZ>= `  ( n  + 
1 ) )
4622adantr 272 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  n  e.  NN )
4746peano2nnd 8692 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( n  + 
1 )  e.  NN )
4847nnzd 9123 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( n  + 
1 )  e.  ZZ )
49 eluznn 9343 . . . . . . . . . . . . 13  |-  ( ( ( n  +  1 )  e.  NN  /\  i  e.  ( ZZ>= `  ( n  +  1
) ) )  -> 
i  e.  NN )
5047, 49sylan 279 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  ->  i  e.  NN )
51 eqid 2115 . . . . . . . . . . . . 13  |-  ( j  e.  NN  |->  ( ( 1  /  ( 2 ^ j ) )  x.  ( F `  j ) ) )  =  ( j  e.  NN  |->  ( ( 1  /  ( 2 ^ j ) )  x.  ( F `  j
) ) )
52 oveq2 5748 . . . . . . . . . . . . . . 15  |-  ( j  =  i  ->  (
2 ^ j )  =  ( 2 ^ i ) )
5352oveq2d 5756 . . . . . . . . . . . . . 14  |-  ( j  =  i  ->  (
1  /  ( 2 ^ j ) )  =  ( 1  / 
( 2 ^ i
) ) )
54 fveq2 5387 . . . . . . . . . . . . . 14  |-  ( j  =  i  ->  ( F `  j )  =  ( F `  i ) )
5553, 54oveq12d 5758 . . . . . . . . . . . . 13  |-  ( j  =  i  ->  (
( 1  /  (
2 ^ j ) )  x.  ( F `
 j ) )  =  ( ( 1  /  ( 2 ^ i ) )  x.  ( F `  i
) ) )
56 simpr 109 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  NN )  ->  i  e.  NN )
5720a1i 9 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  NN )  ->  2  e.  RR+ )
5856nnzd 9123 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  NN )  ->  i  e.  ZZ )
5957, 58rpexpcld 10388 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  NN )  ->  ( 2 ^ i )  e.  RR+ )
6059rprecred 9441 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  NN )  ->  ( 1  / 
( 2 ^ i
) )  e.  RR )
61 0re 7730 . . . . . . . . . . . . . . . 16  |-  0  e.  RR
62 1re 7729 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
63 prssi 3646 . . . . . . . . . . . . . . . 16  |-  ( ( 0  e.  RR  /\  1  e.  RR )  ->  { 0 ,  1 }  C_  RR )
6461, 62, 63mp2an 420 . . . . . . . . . . . . . . 15  |-  { 0 ,  1 }  C_  RR
652adantr 272 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  F : NN --> { 0 ,  1 } )
6665ad2antrr 477 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  NN )  ->  F : NN --> { 0 ,  1 } )
6766, 56ffvelrnd 5522 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  NN )  ->  ( F `  i )  e.  {
0 ,  1 } )
6864, 67sseldi 3063 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  NN )  ->  ( F `  i )  e.  RR )
6960, 68remulcld 7760 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  NN )  ->  ( ( 1  /  ( 2 ^ i ) )  x.  ( F `  i
) )  e.  RR )
7051, 55, 56, 69fvmptd3 5480 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  NN )  ->  ( ( j  e.  NN  |->  ( ( 1  /  ( 2 ^ j ) )  x.  ( F `  j ) ) ) `
 i )  =  ( ( 1  / 
( 2 ^ i
) )  x.  ( F `  i )
) )
7150, 70syldan 278 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  ->  ( ( j  e.  NN  |->  ( ( 1  /  ( 2 ^ j ) )  x.  ( F `  j ) ) ) `
 i )  =  ( ( 1  / 
( 2 ^ i
) )  x.  ( F `  i )
) )
7250, 69syldan 278 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  ->  ( ( 1  /  ( 2 ^ i ) )  x.  ( F `  i
) )  e.  RR )
7365adantr 272 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  F : NN --> { 0 ,  1 } )
7473, 51trilpolemclim 13040 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  seq 1 (  +  ,  ( j  e.  NN  |->  ( ( 1  /  ( 2 ^ j ) )  x.  ( F `  j
) ) ) )  e.  dom  ~~>  )
75 nnuz 9310 . . . . . . . . . . . . 13  |-  NN  =  ( ZZ>= `  1 )
7669recnd 7758 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  NN )  ->  ( ( 1  /  ( 2 ^ i ) )  x.  ( F `  i
) )  e.  CC )
7770, 76eqeltrd 2192 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  NN )  ->  ( ( j  e.  NN  |->  ( ( 1  /  ( 2 ^ j ) )  x.  ( F `  j ) ) ) `
 i )  e.  CC )
7875, 47, 77iserex 11048 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  (  seq 1
(  +  ,  ( j  e.  NN  |->  ( ( 1  /  (
2 ^ j ) )  x.  ( F `
 j ) ) ) )  e.  dom  ~~>  <->  seq ( n  +  1
) (  +  , 
( j  e.  NN  |->  ( ( 1  / 
( 2 ^ j
) )  x.  ( F `  j )
) ) )  e. 
dom 
~~>  ) )
7974, 78mpbid 146 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  seq ( n  + 
1 ) (  +  ,  ( j  e.  NN  |->  ( ( 1  /  ( 2 ^ j ) )  x.  ( F `  j
) ) ) )  e.  dom  ~~>  )
8045, 48, 71, 72, 79isumrecl 11138 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  sum_ i  e.  (
ZZ>= `  ( n  + 
1 ) ) ( ( 1  /  (
2 ^ i ) )  x.  ( F `
 i ) )  e.  RR )
81 1zzd 9032 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
1  e.  ZZ )
8281, 23fzfigd 10144 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1 ... n
)  e.  Fin )
8382adantr 272 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( 1 ... n )  e.  Fin )
8420a1i 9 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  ( 1 ... n ) )  ->  2  e.  RR+ )
85 elfzelz 9746 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 1 ... n )  ->  i  e.  ZZ )
8685adantl 273 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  ( 1 ... n ) )  ->  i  e.  ZZ )
8784, 86rpexpcld 10388 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  ( 1 ... n ) )  ->  ( 2 ^ i )  e.  RR+ )
8887rprecred 9441 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  ( 1 ... n ) )  ->  ( 1  /  ( 2 ^ i ) )  e.  RR )
8983, 88fsumrecl 11110 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  sum_ i  e.  ( 1 ... n ) ( 1  /  (
2 ^ i ) )  e.  RR )
9050, 60syldan 278 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  ->  ( 1  / 
( 2 ^ i
) )  e.  RR )
9150, 68syldan 278 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  ->  ( F `  i )  e.  RR )
9259rpreccld 9440 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  NN )  ->  ( 1  / 
( 2 ^ i
) )  e.  RR+ )
9350, 92syldan 278 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  ->  ( 1  / 
( 2 ^ i
) )  e.  RR+ )
9493rpge0d 9433 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  ->  0  <_  (
1  /  ( 2 ^ i ) ) )
95 0le0 8766 . . . . . . . . . . . . . 14  |-  0  <_  0
96 simpr 109 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  /\  ( F `  i )  =  0 )  ->  ( F `  i )  =  0 )
9795, 96breqtrrid 3934 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  /\  ( F `  i )  =  0 )  ->  0  <_  ( F `  i ) )
98 0le1 8207 . . . . . . . . . . . . . 14  |-  0  <_  1
99 simpr 109 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  /\  ( F `  i )  =  1 )  ->  ( F `  i )  =  1 )
10098, 99breqtrrid 3934 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  /\  ( F `  i )  =  1 )  ->  0  <_  ( F `  i ) )
10173adantr 272 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  ->  F : NN --> { 0 ,  1 } )
102101, 50ffvelrnd 5522 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  ->  ( F `  i )  e.  {
0 ,  1 } )
103 elpri 3518 . . . . . . . . . . . . . 14  |-  ( ( F `  i )  e.  { 0 ,  1 }  ->  (
( F `  i
)  =  0  \/  ( F `  i
)  =  1 ) )
104102, 103syl 14 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  ->  ( ( F `
 i )  =  0  \/  ( F `
 i )  =  1 ) )
10597, 100, 104mpjaodan 770 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  ->  0  <_  ( F `  i )
)
10690, 91, 94, 105mulge0d 8346 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  (
ZZ>= `  ( n  + 
1 ) ) )  ->  0  <_  (
( 1  /  (
2 ^ i ) )  x.  ( F `
 i ) ) )
10745, 48, 71, 72, 79, 106isumge0 11139 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  0  <_  sum_ i  e.  ( ZZ>= `  ( n  +  1 ) ) ( ( 1  / 
( 2 ^ i
) )  x.  ( F `  i )
) )
10844, 80, 89, 107leadd2dd 8285 . . . . . . . . 9  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( sum_ i  e.  ( 1 ... n
) ( 1  / 
( 2 ^ i
) )  +  0 )  <_  ( sum_ i  e.  ( 1 ... n ) ( 1  /  ( 2 ^ i ) )  +  sum_ i  e.  (
ZZ>= `  ( n  + 
1 ) ) ( ( 1  /  (
2 ^ i ) )  x.  ( F `
 i ) ) ) )
10989recnd 7758 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  sum_ i  e.  ( 1 ... n ) ( 1  /  (
2 ^ i ) )  e.  CC )
110109addid1d 7875 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( sum_ i  e.  ( 1 ... n
) ( 1  / 
( 2 ^ i
) )  +  0 )  =  sum_ i  e.  ( 1 ... n
) ( 1  / 
( 2 ^ i
) ) )
111110eqcomd 2121 . . . . . . . . 9  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  sum_ i  e.  ( 1 ... n ) ( 1  /  (
2 ^ i ) )  =  ( sum_ i  e.  ( 1 ... n ) ( 1  /  ( 2 ^ i ) )  +  0 ) )
11275, 45, 47, 70, 76, 74isumsplit 11200 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  sum_ i  e.  NN  ( ( 1  / 
( 2 ^ i
) )  x.  ( F `  i )
)  =  ( sum_ i  e.  ( 1 ... ( ( n  +  1 )  - 
1 ) ) ( ( 1  /  (
2 ^ i ) )  x.  ( F `
 i ) )  +  sum_ i  e.  (
ZZ>= `  ( n  + 
1 ) ) ( ( 1  /  (
2 ^ i ) )  x.  ( F `
 i ) ) ) )
1133, 112syl5eq 2160 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  A  =  (
sum_ i  e.  ( 1 ... ( ( n  +  1 )  -  1 ) ) ( ( 1  / 
( 2 ^ i
) )  x.  ( F `  i )
)  +  sum_ i  e.  ( ZZ>= `  ( n  +  1 ) ) ( ( 1  / 
( 2 ^ i
) )  x.  ( F `  i )
) ) )
11446nncnd 8691 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  n  e.  CC )
115 1cnd 7746 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  1  e.  CC )
116114, 115pncand 8038 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( ( n  +  1 )  - 
1 )  =  n )
117116oveq2d 5756 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( 1 ... ( ( n  + 
1 )  -  1 ) )  =  ( 1 ... n ) )
118 simpr 109 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  ( 1 ... n ) )  ->  i  e.  ( 1 ... n
) )
119118fvresd 5412 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  ( 1 ... n ) )  ->  ( ( F  |`  ( 1 ... n ) ) `  i )  =  ( F `  i ) )
120 fveqeq2 5396 . . . . . . . . . . . . . . . 16  |-  ( x  =  i  ->  (
( ( F  |`  ( 1 ... n
) ) `  x
)  =  1  <->  (
( F  |`  (
1 ... n ) ) `
 i )  =  1 ) )
121 simplr 502 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  ( 1 ... n ) )  ->  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )
122120, 121, 118rspcdva 2766 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  ( 1 ... n ) )  ->  ( ( F  |`  ( 1 ... n ) ) `  i )  =  1 )
123119, 122eqtr3d 2150 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  ( 1 ... n ) )  ->  ( F `  i )  =  1 )
124123oveq2d 5756 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  ( 1 ... n ) )  ->  ( (
1  /  ( 2 ^ i ) )  x.  ( F `  i ) )  =  ( ( 1  / 
( 2 ^ i
) )  x.  1 ) )
12587rpreccld 9440 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  ( 1 ... n ) )  ->  ( 1  /  ( 2 ^ i ) )  e.  RR+ )
126125rpcnd 9431 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  ( 1 ... n ) )  ->  ( 1  /  ( 2 ^ i ) )  e.  CC )
127126mulid1d 7747 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  ( 1 ... n ) )  ->  ( (
1  /  ( 2 ^ i ) )  x.  1 )  =  ( 1  /  (
2 ^ i ) ) )
128124, 127eqtrd 2148 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  /\  i  e.  ( 1 ... n ) )  ->  ( (
1  /  ( 2 ^ i ) )  x.  ( F `  i ) )  =  ( 1  /  (
2 ^ i ) ) )
129117, 128sumeq12rdv 11082 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  sum_ i  e.  ( 1 ... ( ( n  +  1 )  -  1 ) ) ( ( 1  / 
( 2 ^ i
) )  x.  ( F `  i )
)  =  sum_ i  e.  ( 1 ... n
) ( 1  / 
( 2 ^ i
) ) )
130129oveq1d 5755 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( sum_ i  e.  ( 1 ... (
( n  +  1 )  -  1 ) ) ( ( 1  /  ( 2 ^ i ) )  x.  ( F `  i
) )  +  sum_ i  e.  ( ZZ>= `  ( n  +  1
) ) ( ( 1  /  ( 2 ^ i ) )  x.  ( F `  i ) ) )  =  ( sum_ i  e.  ( 1 ... n
) ( 1  / 
( 2 ^ i
) )  +  sum_ i  e.  ( ZZ>= `  ( n  +  1
) ) ( ( 1  /  ( 2 ^ i ) )  x.  ( F `  i ) ) ) )
131113, 130eqtrd 2148 . . . . . . . . 9  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  A  =  (
sum_ i  e.  ( 1 ... n ) ( 1  /  (
2 ^ i ) )  +  sum_ i  e.  ( ZZ>= `  ( n  +  1 ) ) ( ( 1  / 
( 2 ^ i
) )  x.  ( F `  i )
) ) )
132108, 111, 1313brtr4d 3928 . . . . . . . 8  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  sum_ i  e.  ( 1 ... n ) ( 1  /  (
2 ^ i ) )  <_  A )
133 geo2sum 11223 . . . . . . . . . 10  |-  ( ( n  e.  NN  /\  1  e.  CC )  -> 
sum_ i  e.  ( 1 ... n ) ( 1  /  (
2 ^ i ) )  =  ( 1  -  ( 1  / 
( 2 ^ n
) ) ) )
134133breq1d 3907 . . . . . . . . 9  |-  ( ( n  e.  NN  /\  1  e.  CC )  ->  ( sum_ i  e.  ( 1 ... n ) ( 1  /  (
2 ^ i ) )  <_  A  <->  ( 1  -  ( 1  / 
( 2 ^ n
) ) )  <_  A ) )
13546, 115, 134syl2anc 406 . . . . . . . 8  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( sum_ i  e.  ( 1 ... n
) ( 1  / 
( 2 ^ i
) )  <_  A  <->  ( 1  -  ( 1  /  ( 2 ^ n ) ) )  <_  A ) )
136132, 135mpbid 146 . . . . . . 7  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( 1  -  ( 1  /  (
2 ^ n ) ) )  <_  A
)
13742, 41, 43, 136subled 8273 . . . . . 6  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( 1  -  A )  <_  (
1  /  ( 2 ^ n ) ) )
13840, 41, 137lensymd 7848 . . . . 5  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  -.  ( 1  /  ( 2 ^ n ) )  < 
( 1  -  A
) )
13939, 138pm2.21dd 592 . . . 4  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  E. x  e.  NN  ( F `  x )  =  0 )
140139ex 114 . . 3  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1  ->  E. x  e.  NN  ( F `  x )  =  0 ) )
141 fveq1 5386 . . . . . . 7  |-  ( f  =  ( F  |`  ( 1 ... n
) )  ->  (
f `  x )  =  ( ( F  |`  ( 1 ... n
) ) `  x
) )
142141eqeq1d 2124 . . . . . 6  |-  ( f  =  ( F  |`  ( 1 ... n
) )  ->  (
( f `  x
)  =  0  <->  (
( F  |`  (
1 ... n ) ) `
 x )  =  0 ) )
143142rexbidv 2413 . . . . 5  |-  ( f  =  ( F  |`  ( 1 ... n
) )  ->  ( E. x  e.  (
1 ... n ) ( f `  x )  =  0  <->  E. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  0 ) )
144141eqeq1d 2124 . . . . . 6  |-  ( f  =  ( F  |`  ( 1 ... n
) )  ->  (
( f `  x
)  =  1  <->  (
( F  |`  (
1 ... n ) ) `
 x )  =  1 ) )
145144ralbidv 2412 . . . . 5  |-  ( f  =  ( F  |`  ( 1 ... n
) )  ->  ( A. x  e.  (
1 ... n ) ( f `  x )  =  1  <->  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 ) )
146143, 145orbi12d 765 . . . 4  |-  ( f  =  ( F  |`  ( 1 ... n
) )  ->  (
( E. x  e.  ( 1 ... n
) ( f `  x )  =  0  \/  A. x  e.  ( 1 ... n
) ( f `  x )  =  1 )  <->  ( E. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  0  \/ 
A. x  e.  ( 1 ... n ) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 ) ) )
147 finomni 6978 . . . . . 6  |-  ( ( 1 ... n )  e.  Fin  ->  (
1 ... n )  e. Omni
)
14882, 147syl 14 . . . . 5  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1 ... n
)  e. Omni )
149 isomninn 13037 . . . . . 6  |-  ( ( 1 ... n )  e. Omni  ->  ( ( 1 ... n )  e. Omni  <->  A. f  e.  ( { 0 ,  1 }  ^m  ( 1 ... n ) ) ( E. x  e.  ( 1 ... n ) ( f `  x
)  =  0  \/ 
A. x  e.  ( 1 ... n ) ( f `  x
)  =  1 ) ) )
150148, 149syl 14 . . . . 5  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( ( 1 ... n )  e. Omni  <->  A. f  e.  ( { 0 ,  1 }  ^m  (
1 ... n ) ) ( E. x  e.  ( 1 ... n
) ( f `  x )  =  0  \/  A. x  e.  ( 1 ... n
) ( f `  x )  =  1 ) ) )
151148, 150mpbid 146 . . . 4  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  A. f  e.  ( { 0 ,  1 }  ^m  ( 1 ... n ) ) ( E. x  e.  ( 1 ... n
) ( f `  x )  =  0  \/  A. x  e.  ( 1 ... n
) ( f `  x )  =  1 ) )
152 fz1ssnn 9776 . . . . . . 7  |-  ( 1 ... n )  C_  NN
153152a1i 9 . . . . . 6  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1 ... n
)  C_  NN )
15465, 153fssresd 5267 . . . . 5  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( F  |`  (
1 ... n ) ) : ( 1 ... n ) --> { 0 ,  1 } )
155 0red 7731 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
0  e.  RR )
156 1red 7745 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
1  e.  RR )
157 prexg 4101 . . . . . . 7  |-  ( ( 0  e.  RR  /\  1  e.  RR )  ->  { 0 ,  1 }  e.  _V )
158155, 156, 157syl2anc 406 . . . . . 6  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  { 0 ,  1 }  e.  _V )
159158, 82elmapd 6522 . . . . 5  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( ( F  |`  ( 1 ... n
) )  e.  ( { 0 ,  1 }  ^m  ( 1 ... n ) )  <-> 
( F  |`  (
1 ... n ) ) : ( 1 ... n ) --> { 0 ,  1 } ) )
160154, 159mpbird 166 . . . 4  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( F  |`  (
1 ... n ) )  e.  ( { 0 ,  1 }  ^m  ( 1 ... n
) ) )
161146, 151, 160rspcdva 2766 . . 3  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( E. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  0  \/ 
A. x  e.  ( 1 ... n ) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 ) )
16219, 140, 161mpjaod 690 . 2  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  E. x  e.  NN  ( F `  x )  =  0 )
16310, 162rexlimddv 2529 1  |-  ( ph  ->  E. x  e.  NN  ( F `  x )  =  0 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 680    = wceq 1314    e. wcel 1463   A.wral 2391   E.wrex 2392   _Vcvv 2658    C_ wss 3039   {cpr 3496   class class class wbr 3897    |-> cmpt 3957   dom cdm 4507    |` cres 4509   -->wf 5087   ` cfv 5091  (class class class)co 5740    ^m cmap 6508   Fincfn 6600  Omnicomni 6970   CCcc 7582   RRcr 7583   0cc0 7584   1c1 7585    + caddc 7587    x. cmul 7589    < clt 7764    <_ cle 7765    - cmin 7897    / cdiv 8392   NNcn 8677   2c2 8728   NN0cn0 8928   ZZcz 9005   ZZ>=cuz 9275   RR+crp 9390   ...cfz 9730    seqcseq 10158   ^cexp 10232    ~~> cli 10987   sum_csu 11062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4011  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-iinf 4470  ax-cnex 7675  ax-resscn 7676  ax-1cn 7677  ax-1re 7678  ax-icn 7679  ax-addcl 7680  ax-addrcl 7681  ax-mulcl 7682  ax-mulrcl 7683  ax-addcom 7684  ax-mulcom 7685  ax-addass 7686  ax-mulass 7687  ax-distr 7688  ax-i2m1 7689  ax-0lt1 7690  ax-1rid 7691  ax-0id 7692  ax-rnegex 7693  ax-precex 7694  ax-cnre 7695  ax-pre-ltirr 7696  ax-pre-ltwlin 7697  ax-pre-lttrn 7698  ax-pre-apti 7699  ax-pre-ltadd 7700  ax-pre-mulgt0 7701  ax-pre-mulext 7702  ax-arch 7703  ax-caucvg 7704
This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-nel 2379  df-ral 2396  df-rex 2397  df-reu 2398  df-rmo 2399  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-if 3443  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-po 4186  df-iso 4187  df-iord 4256  df-on 4258  df-ilim 4259  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-isom 5100  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-1st 6004  df-2nd 6005  df-recs 6168  df-irdg 6233  df-frec 6254  df-1o 6279  df-2o 6280  df-oadd 6283  df-er 6395  df-map 6510  df-en 6601  df-dom 6602  df-fin 6603  df-omni 6972  df-pnf 7766  df-mnf 7767  df-xr 7768  df-ltxr 7769  df-le 7770  df-sub 7899  df-neg 7900  df-reap 8300  df-ap 8307  df-div 8393  df-inn 8678  df-2 8736  df-3 8737  df-4 8738  df-n0 8929  df-z 9006  df-uz 9276  df-q 9361  df-rp 9391  df-ico 9617  df-fz 9731  df-fzo 9860  df-seqfrec 10159  df-exp 10233  df-ihash 10462  df-cj 10554  df-re 10555  df-im 10556  df-rsqrt 10710  df-abs 10711  df-clim 10988  df-sumdc 11063
This theorem is referenced by:  trilpolemres  13046
  Copyright terms: Public domain W3C validator