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

Theorem trilpolemlt1 14442
Description: Lemma for trilpo 14444. 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 7132 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 7960 . . . 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 14438 . . . 4  |-  ( ph  ->  A  e.  RR )
51, 4resubcld 8325 . . 3  |-  ( ph  ->  ( 1  -  A
)  e.  RR )
6 trilpolemlt1.a . . . 4  |-  ( ph  ->  A  <  1 )
74, 1posdifd 8476 . . . 4  |-  ( ph  ->  ( A  <  1  <->  0  <  ( 1  -  A ) ) )
86, 7mpbid 147 . . 3  |-  ( ph  ->  0  <  ( 1  -  A ) )
9 nnrecl 9160 . . 3  |-  ( ( ( 1  -  A
)  e.  RR  /\  0  <  ( 1  -  A ) )  ->  E. n  e.  NN  ( 1  /  n
)  <  ( 1  -  A ) )
105, 8, 9syl2anc 411 . 2  |-  ( ph  ->  E. n  e.  NN  ( 1  /  n
)  <  ( 1  -  A ) )
11 elfznn 10037 . . . . . . 7  |-  ( x  e.  ( 1 ... n )  ->  x  e.  NN )
1211ad2antrl 490 . . . . . 6  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  ( x  e.  ( 1 ... n )  /\  (
( F  |`  (
1 ... n ) ) `
 x )  =  0 ) )  ->  x  e.  NN )
13 simprl 529 . . . . . . . 8  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  ( x  e.  ( 1 ... n )  /\  (
( F  |`  (
1 ... n ) ) `
 x )  =  0 ) )  ->  x  e.  ( 1 ... n ) )
1413fvresd 5536 . . . . . . 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 531 . . . . . . 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 2212 . . . . . 6  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  ( x  e.  ( 1 ... n )  /\  (
( F  |`  (
1 ... n ) ) `
 x )  =  0 ) )  -> 
( F `  x
)  =  0 )
1712, 16jca 306 . . . . 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 115 . . . 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 2576 . . 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 9642 . . . . . . . . . 10  |-  2  e.  RR+
2120a1i 9 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
2  e.  RR+ )
22 simprl 529 . . . . . . . . . 10  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  n  e.  NN )
2322nnzd 9360 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  n  e.  ZZ )
2421, 23rpexpcld 10660 . . . . . . . 8  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 2 ^ n
)  e.  RR+ )
2524rprecred 9692 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1  /  (
2 ^ n ) )  e.  RR )
2622nnrecred 8952 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1  /  n
)  e.  RR )
275adantr 276 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1  -  A
)  e.  RR )
28 2z 9267 . . . . . . . . . 10  |-  2  e.  ZZ
29 uzid 9528 . . . . . . . . . 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 9215 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  n  e.  NN0 )
32 bernneq3 10625 . . . . . . . . 9  |-  ( ( 2  e.  ( ZZ>= ` 
2 )  /\  n  e.  NN0 )  ->  n  <  ( 2 ^ n
) )
3330, 31, 32syl2anc 411 . . . . . . . 8  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  n  <  ( 2 ^ n ) )
3422nnrpd 9678 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  n  e.  RR+ )
3534, 24ltrecd 9699 . . . . . . . 8  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( n  <  (
2 ^ n )  <-> 
( 1  /  (
2 ^ n ) )  <  ( 1  /  n ) ) )
3633, 35mpbid 147 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1  /  (
2 ^ n ) )  <  ( 1  /  n ) )
37 simprr 531 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1  /  n
)  <  ( 1  -  A ) )
3825, 26, 27, 36, 37lttrd 8070 . . . . . 6  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1  /  (
2 ^ n ) )  <  ( 1  -  A ) )
3938adantr 276 . . . . 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 276 . . . . . 6  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( 1  -  A )  e.  RR )
4125adantr 276 . . . . . 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 7960 . . . . . . 7  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  1  e.  RR )
434ad2antrr 488 . . . . . . 7  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  A  e.  RR )
44 0red 7946 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  0  e.  RR )
45 eqid 2177 . . . . . . . . . . 11  |-  ( ZZ>= `  ( n  +  1
) )  =  (
ZZ>= `  ( n  + 
1 ) )
4622adantr 276 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  n  e.  NN )
4746peano2nnd 8920 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( n  + 
1 )  e.  NN )
4847nnzd 9360 . . . . . . . . . . 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 9586 . . . . . . . . . . . . 13  |-  ( ( ( n  +  1 )  e.  NN  /\  i  e.  ( ZZ>= `  ( n  +  1
) ) )  -> 
i  e.  NN )
5047, 49sylan 283 . . . . . . . . . . . 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 2177 . . . . . . . . . . . . 13  |-  ( j  e.  NN  |->  ( ( 1  /  ( 2 ^ j ) )  x.  ( F `  j ) ) )  =  ( j  e.  NN  |->  ( ( 1  /  ( 2 ^ j ) )  x.  ( F `  j
) ) )
52 oveq2 5877 . . . . . . . . . . . . . . 15  |-  ( j  =  i  ->  (
2 ^ j )  =  ( 2 ^ i ) )
5352oveq2d 5885 . . . . . . . . . . . . . 14  |-  ( j  =  i  ->  (
1  /  ( 2 ^ j ) )  =  ( 1  / 
( 2 ^ i
) ) )
54 fveq2 5511 . . . . . . . . . . . . . 14  |-  ( j  =  i  ->  ( F `  j )  =  ( F `  i ) )
5553, 54oveq12d 5887 . . . . . . . . . . . . 13  |-  ( j  =  i  ->  (
( 1  /  (
2 ^ j ) )  x.  ( F `
 j ) )  =  ( ( 1  /  ( 2 ^ i ) )  x.  ( F `  i
) ) )
56 simpr 110 . . . . . . . . . . . . 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 9360 . . . . . . . . . . . . . . . 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 10660 . . . . . . . . . . . . . . 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 9692 . . . . . . . . . . . . . 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 7945 . . . . . . . . . . . . . . . 16  |-  0  e.  RR
62 1re 7944 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
63 prssi 3749 . . . . . . . . . . . . . . . 16  |-  ( ( 0  e.  RR  /\  1  e.  RR )  ->  { 0 ,  1 }  C_  RR )
6461, 62, 63mp2an 426 . . . . . . . . . . . . . . 15  |-  { 0 ,  1 }  C_  RR
652adantr 276 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  F : NN --> { 0 ,  1 } )
6665ad2antrr 488 . . . . . . . . . . . . . . . 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, 56ffvelcdmd 5648 . . . . . . . . . . . . . . 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, 67sselid 3153 . . . . . . . . . . . . . 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 7975 . . . . . . . . . . . . 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 5605 . . . . . . . . . . . 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 282 . . . . . . . . . . 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 282 . . . . . . . . . . 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 276 . . . . . . . . . . . . 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 14437 . . . . . . . . . . . 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 9549 . . . . . . . . . . . . 13  |-  NN  =  ( ZZ>= `  1 )
7669recnd 7973 . . . . . . . . . . . . . 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 2254 . . . . . . . . . . . . 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 11328 . . . . . . . . . . . 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 147 . . . . . . . . . . 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 11418 . . . . . . . . . 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 9266 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
1  e.  ZZ )
8281, 23fzfigd 10414 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1 ... n
)  e.  Fin )
8382adantr 276 . . . . . . . . . . 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 10008 . . . . . . . . . . . . . 14  |-  ( i  e.  ( 1 ... n )  ->  i  e.  ZZ )
8685adantl 277 . . . . . . . . . . . . 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 10660 . . . . . . . . . . . 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 9692 . . . . . . . . . . 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 11390 . . . . . . . . . 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 282 . . . . . . . . . . . 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 282 . . . . . . . . . . . 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 9691 . . . . . . . . . . . . . 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 282 . . . . . . . . . . . . 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 9684 . . . . . . . . . . . 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 8994 . . . . . . . . . . . . . 14  |-  0  <_  0
96 simpr 110 . . . . . . . . . . . . . 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 4038 . . . . . . . . . . . . 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 8425 . . . . . . . . . . . . . 14  |-  0  <_  1
99 simpr 110 . . . . . . . . . . . . . 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 4038 . . . . . . . . . . . . 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 276 . . . . . . . . . . . . . . 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, 50ffvelcdmd 5648 . . . . . . . . . . . . . 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 3614 . . . . . . . . . . . . . 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 798 . . . . . . . . . . . 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 8565 . . . . . . . . . . 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 11419 . . . . . . . . . 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 8504 . . . . . . . . 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 7973 . . . . . . . . . . 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 8093 . . . . . . . . . 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 2183 . . . . . . . . 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 11480 . . . . . . . . . . 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, 112eqtrid 2222 . . . . . . . . . 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 8919 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  n  e.  CC )
115 1cnd 7961 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  1  e.  CC )
116114, 115pncand 8256 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
n  e.  NN  /\  ( 1  /  n
)  <  ( 1  -  A ) ) )  /\  A. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  1 )  ->  ( ( n  +  1 )  - 
1 )  =  n )
117116oveq2d 5885 . . . . . . . . . . . 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 110 . . . . . . . . . . . . . . . 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 5536 . . . . . . . . . . . . . . 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 5520 . . . . . . . . . . . . . . . 16  |-  ( x  =  i  ->  (
( ( F  |`  ( 1 ... n
) ) `  x
)  =  1  <->  (
( F  |`  (
1 ... n ) ) `
 i )  =  1 ) )
121 simplr 528 . . . . . . . . . . . . . . . 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 2846 . . . . . . . . . . . . . . 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 2212 . . . . . . . . . . . . . 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 5885 . . . . . . . . . . . . 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 9691 . . . . . . . . . . . . . . 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 9682 . . . . . . . . . . . . . 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 7962 . . . . . . . . . . . . 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 2210 . . . . . . . . . . . 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 11362 . . . . . . . . . . 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 5884 . . . . . . . . . 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 2210 . . . . . . . . 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 4032 . . . . . . . 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 11503 . . . . . . . . . 10  |-  ( ( n  e.  NN  /\  1  e.  CC )  -> 
sum_ i  e.  ( 1 ... n ) ( 1  /  (
2 ^ i ) )  =  ( 1  -  ( 1  / 
( 2 ^ n
) ) ) )
134133breq1d 4010 . . . . . . . . 9  |-  ( ( n  e.  NN  /\  1  e.  CC )  ->  ( sum_ i  e.  ( 1 ... n ) ( 1  /  (
2 ^ i ) )  <_  A  <->  ( 1  -  ( 1  / 
( 2 ^ n
) ) )  <_  A ) )
13546, 115, 134syl2anc 411 . . . . . . . 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 147 . . . . . . 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 8492 . . . . . 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 8066 . . . . 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 620 . . . 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 115 . . 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 5510 . . . . . . 7  |-  ( f  =  ( F  |`  ( 1 ... n
) )  ->  (
f `  x )  =  ( ( F  |`  ( 1 ... n
) ) `  x
) )
142141eqeq1d 2186 . . . . . 6  |-  ( f  =  ( F  |`  ( 1 ... n
) )  ->  (
( f `  x
)  =  0  <->  (
( F  |`  (
1 ... n ) ) `
 x )  =  0 ) )
143142rexbidv 2478 . . . . 5  |-  ( f  =  ( F  |`  ( 1 ... n
) )  ->  ( E. x  e.  (
1 ... n ) ( f `  x )  =  0  <->  E. x  e.  ( 1 ... n
) ( ( F  |`  ( 1 ... n
) ) `  x
)  =  0 ) )
144141eqeq1d 2186 . . . . . 6  |-  ( f  =  ( F  |`  ( 1 ... n
) )  ->  (
( f `  x
)  =  1  <->  (
( F  |`  (
1 ... n ) ) `
 x )  =  1 ) )
145144ralbidv 2477 . . . . 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 793 . . . 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 7132 . . . . . 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 14432 . . . . . 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 147 . . . 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 10039 . . . . . . 7  |-  ( 1 ... n )  C_  NN
153152a1i 9 . . . . . 6  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( 1 ... n
)  C_  NN )
15465, 153fssresd 5388 . . . . 5  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( F  |`  (
1 ... n ) ) : ( 1 ... n ) --> { 0 ,  1 } )
155 0red 7946 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
0  e.  RR )
156 1red 7960 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
1  e.  RR )
157 prexg 4208 . . . . . . 7  |-  ( ( 0  e.  RR  /\  1  e.  RR )  ->  { 0 ,  1 }  e.  _V )
158155, 156, 157syl2anc 411 . . . . . 6  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  { 0 ,  1 }  e.  _V )
159158, 82elmapd 6656 . . . . 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 167 . . . 4  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  -> 
( F  |`  (
1 ... n ) )  e.  ( { 0 ,  1 }  ^m  ( 1 ... n
) ) )
161146, 151, 160rspcdva 2846 . . 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 718 . 2  |-  ( (
ph  /\  ( n  e.  NN  /\  ( 1  /  n )  < 
( 1  -  A
) ) )  ->  E. x  e.  NN  ( F `  x )  =  0 )
16310, 162rexlimddv 2599 1  |-  ( ph  ->  E. x  e.  NN  ( F `  x )  =  0 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 708    = wceq 1353    e. wcel 2148   A.wral 2455   E.wrex 2456   _Vcvv 2737    C_ wss 3129   {cpr 3592   class class class wbr 4000    |-> cmpt 4061   dom cdm 4623    |` cres 4625   -->wf 5208   ` cfv 5212  (class class class)co 5869    ^m cmap 6642   Fincfn 6734  Omnicomni 7126   CCcc 7797   RRcr 7798   0cc0 7799   1c1 7800    + caddc 7802    x. cmul 7804    < clt 7979    <_ cle 7980    - cmin 8115    / cdiv 8615   NNcn 8905   2c2 8956   NN0cn0 9162   ZZcz 9239   ZZ>=cuz 9514   RR+crp 9637   ...cfz 9992    seqcseq 10428   ^cexp 10502    ~~> cli 11267   sum_csu 11342
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584  ax-cnex 7890  ax-resscn 7891  ax-1cn 7892  ax-1re 7893  ax-icn 7894  ax-addcl 7895  ax-addrcl 7896  ax-mulcl 7897  ax-mulrcl 7898  ax-addcom 7899  ax-mulcom 7900  ax-addass 7901  ax-mulass 7902  ax-distr 7903  ax-i2m1 7904  ax-0lt1 7905  ax-1rid 7906  ax-0id 7907  ax-rnegex 7908  ax-precex 7909  ax-cnre 7910  ax-pre-ltirr 7911  ax-pre-ltwlin 7912  ax-pre-lttrn 7913  ax-pre-apti 7914  ax-pre-ltadd 7915  ax-pre-mulgt0 7916  ax-pre-mulext 7917  ax-arch 7918  ax-caucvg 7919
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-po 4293  df-iso 4294  df-iord 4363  df-on 4365  df-ilim 4366  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-isom 5221  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-recs 6300  df-irdg 6365  df-frec 6386  df-1o 6411  df-2o 6412  df-oadd 6415  df-er 6529  df-map 6644  df-en 6735  df-dom 6736  df-fin 6737  df-omni 7127  df-pnf 7981  df-mnf 7982  df-xr 7983  df-ltxr 7984  df-le 7985  df-sub 8117  df-neg 8118  df-reap 8519  df-ap 8526  df-div 8616  df-inn 8906  df-2 8964  df-3 8965  df-4 8966  df-n0 9163  df-z 9240  df-uz 9515  df-q 9606  df-rp 9638  df-ico 9878  df-fz 9993  df-fzo 10126  df-seqfrec 10429  df-exp 10503  df-ihash 10737  df-cj 10832  df-re 10833  df-im 10834  df-rsqrt 10988  df-abs 10989  df-clim 11268  df-sumdc 11343
This theorem is referenced by:  trilpolemres  14443  neapmkvlem  14467
  Copyright terms: Public domain W3C validator