MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rpnnen2 Unicode version

Theorem rpnnen2 12754
Description: The other half of rpnnen 12755, where we show an injection from sets of natural numbers to real numbers. The obvious choice for this is binary expansion, but it has the unfortunate property that it does not produce an injection on numbers which end with all 0's or all 1's (the more well-known decimal version of this is 0.999... 12587). Instead, we opt for a ternary expansion, which produces (a scaled version of) the Cantor set. Since the Cantor set is riddled with gaps, we can show that any two sequences that are not equal must differ somewhere, and when they do, they are placed a finite distance apart, thus ensuring that the map is injective.

Our map assigns to each subset  A of the natural numbers the number  sum_ k  e.  A ( 3 ^
-u k )  = 
sum_ k  e.  NN ( ( F `  A ) `  k
), where  ( ( F `  A ) `  k )  =  if ( k  e.  A ,  ( 3 ^
-u k ) ,  0 ) ) (rpnnen2lem1 12743). This is an infinite sum of real numbers (rpnnen2lem2 12744), and since  A 
C_  B implies  ( F `  A )  <_  ( F `  B ) (rpnnen2lem4 12746) and  ( F `  NN ) converges to  1  /  2 (rpnnen2lem3 12745) by geoisum1 12585, the sum is convergent to some real (rpnnen2lem5 12747 and rpnnen2lem6 12748) by the comparison test for convergence cvgcmp 12524. The comparison test also tells us that  A  C_  B implies  sum_ ( F `  A )  <_ 
sum_ ( F `  B ) (rpnnen2lem7 12749).

Putting it all together, if we have two sets  x  =/=  y, there must differ somewhere, and so there must be an  m such that  A. n  < 
m ( n  e.  x  <->  n  e.  y
) but  m  e.  ( x  \  y ) or vice versa. In this case, we split off the first  m  -  1 terms (rpnnen2lem8 12750) and cancel them (rpnnen2lem10 12752), since these are the same for both sets. For the remaining terms, we use the subset property to establish that  sum_ ( F `
 y )  <_  sum_ ( F `  ( NN  \  { m }
) ) and  sum_ ( F `
 { m }
)  <_  sum_ ( F `
 x ) (where these sums are only over  ( ZZ>= `  m
)), and since  sum_ ( F `
 ( NN  \  { m } ) )  =  ( 3 ^ -u m )  /  2 (rpnnen2lem9 12751) and  sum_ ( F `  { m } )  =  ( 3 ^
-u m ), we establish that  sum_ ( F `
 y )  <  sum_ ( F `  x
) (rpnnen2lem11 12753) so that they must be different. By contraposition, we find that this map is an injection. (Contributed by Mario Carneiro, 13-May-2013.) (Proof shortened by Mario Carneiro, 30-Apr-2014.)

Hypothesis
Ref Expression
rpnnen2.1  |-  F  =  ( x  e.  ~P NN  |->  ( n  e.  NN  |->  if ( n  e.  x ,  ( ( 1  /  3
) ^ n ) ,  0 ) ) )
Assertion
Ref Expression
rpnnen2  |-  ~P NN  ~<_  ( 0 [,] 1
)
Distinct variable group:    x, n
Allowed substitution hints:    F( x, n)

Proof of Theorem rpnnen2
Dummy variables  m  y  z  k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovex 6047 . 2  |-  ( 0 [,] 1 )  e. 
_V
2 elpwi 3752 . . . . 5  |-  ( y  e.  ~P NN  ->  y 
C_  NN )
3 nnuz 10455 . . . . . . 7  |-  NN  =  ( ZZ>= `  1 )
43sumeq1i 12421 . . . . . 6  |-  sum_ k  e.  NN  ( ( F `
 y ) `  k )  =  sum_ k  e.  ( ZZ>= ` 
1 ) ( ( F `  y ) `
 k )
5 1nn 9945 . . . . . . 7  |-  1  e.  NN
6 rpnnen2.1 . . . . . . . 8  |-  F  =  ( x  e.  ~P NN  |->  ( n  e.  NN  |->  if ( n  e.  x ,  ( ( 1  /  3
) ^ n ) ,  0 ) ) )
76rpnnen2lem6 12748 . . . . . . 7  |-  ( ( y  C_  NN  /\  1  e.  NN )  ->  sum_ k  e.  ( ZZ>= `  1 )
( ( F `  y ) `  k
)  e.  RR )
85, 7mpan2 653 . . . . . 6  |-  ( y 
C_  NN  ->  sum_ k  e.  ( ZZ>= `  1 )
( ( F `  y ) `  k
)  e.  RR )
94, 8syl5eqel 2473 . . . . 5  |-  ( y 
C_  NN  ->  sum_ k  e.  NN  ( ( F `
 y ) `  k )  e.  RR )
102, 9syl 16 . . . 4  |-  ( y  e.  ~P NN  ->  sum_ k  e.  NN  (
( F `  y
) `  k )  e.  RR )
11 1z 10245 . . . . . 6  |-  1  e.  ZZ
1211a1i 11 . . . . 5  |-  ( y  e.  ~P NN  ->  1  e.  ZZ )
13 eqidd 2390 . . . . 5  |-  ( ( y  e.  ~P NN  /\  k  e.  NN )  ->  ( ( F `
 y ) `  k )  =  ( ( F `  y
) `  k )
)
146rpnnen2lem2 12744 . . . . . . 7  |-  ( y 
C_  NN  ->  ( F `
 y ) : NN --> RR )
152, 14syl 16 . . . . . 6  |-  ( y  e.  ~P NN  ->  ( F `  y ) : NN --> RR )
1615ffvelrnda 5811 . . . . 5  |-  ( ( y  e.  ~P NN  /\  k  e.  NN )  ->  ( ( F `
 y ) `  k )  e.  RR )
176rpnnen2lem5 12747 . . . . . 6  |-  ( ( y  C_  NN  /\  1  e.  NN )  ->  seq  1 (  +  , 
( F `  y
) )  e.  dom  ~~>  )
182, 5, 17sylancl 644 . . . . 5  |-  ( y  e.  ~P NN  ->  seq  1 (  +  , 
( F `  y
) )  e.  dom  ~~>  )
19 ssid 3312 . . . . . . . 8  |-  NN  C_  NN
206rpnnen2lem4 12746 . . . . . . . 8  |-  ( ( y  C_  NN  /\  NN  C_  NN  /\  k  e.  NN )  ->  (
0  <_  ( ( F `  y ) `  k )  /\  (
( F `  y
) `  k )  <_  ( ( F `  NN ) `  k ) ) )
2119, 20mp3an2 1267 . . . . . . 7  |-  ( ( y  C_  NN  /\  k  e.  NN )  ->  (
0  <_  ( ( F `  y ) `  k )  /\  (
( F `  y
) `  k )  <_  ( ( F `  NN ) `  k ) ) )
2221simpld 446 . . . . . 6  |-  ( ( y  C_  NN  /\  k  e.  NN )  ->  0  <_  ( ( F `  y ) `  k
) )
232, 22sylan 458 . . . . 5  |-  ( ( y  e.  ~P NN  /\  k  e.  NN )  ->  0  <_  (
( F `  y
) `  k )
)
243, 12, 13, 16, 18, 23isumge0 12479 . . . 4  |-  ( y  e.  ~P NN  ->  0  <_  sum_ k  e.  NN  ( ( F `  y ) `  k
) )
25 1re 9025 . . . . . . 7  |-  1  e.  RR
2625rehalfcli 10150 . . . . . 6  |-  ( 1  /  2 )  e.  RR
2726a1i 11 . . . . 5  |-  ( y  e.  ~P NN  ->  ( 1  /  2 )  e.  RR )
2825a1i 11 . . . . 5  |-  ( y  e.  ~P NN  ->  1  e.  RR )
296rpnnen2lem7 12749 . . . . . . . . 9  |-  ( ( y  C_  NN  /\  NN  C_  NN  /\  1  e.  NN )  ->  sum_ k  e.  ( ZZ>= `  1 )
( ( F `  y ) `  k
)  <_  sum_ k  e.  ( ZZ>= `  1 )
( ( F `  NN ) `  k ) )
3019, 5, 29mp3an23 1271 . . . . . . . 8  |-  ( y 
C_  NN  ->  sum_ k  e.  ( ZZ>= `  1 )
( ( F `  y ) `  k
)  <_  sum_ k  e.  ( ZZ>= `  1 )
( ( F `  NN ) `  k ) )
312, 30syl 16 . . . . . . 7  |-  ( y  e.  ~P NN  ->  sum_ k  e.  ( ZZ>= ` 
1 ) ( ( F `  y ) `
 k )  <_  sum_ k  e.  ( ZZ>= ` 
1 ) ( ( F `  NN ) `
 k ) )
32 eqid 2389 . . . . . . . 8  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  1 )
33 eqidd 2390 . . . . . . . 8  |-  ( ( y  e.  ~P NN  /\  k  e.  ( ZZ>= ` 
1 ) )  -> 
( ( F `  NN ) `  k )  =  ( ( F `
 NN ) `  k ) )
34 elnnuz 10456 . . . . . . . . . 10  |-  ( k  e.  NN  <->  k  e.  ( ZZ>= `  1 )
)
356rpnnen2lem2 12744 . . . . . . . . . . . . 13  |-  ( NN  C_  NN  ->  ( F `  NN ) : NN --> RR )
3619, 35ax-mp 8 . . . . . . . . . . . 12  |-  ( F `
 NN ) : NN --> RR
3736ffvelrni 5810 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( F `  NN ) `  k )  e.  RR )
3837recnd 9049 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
( F `  NN ) `  k )  e.  CC )
3934, 38sylbir 205 . . . . . . . . 9  |-  ( k  e.  ( ZZ>= `  1
)  ->  ( ( F `  NN ) `  k )  e.  CC )
4039adantl 453 . . . . . . . 8  |-  ( ( y  e.  ~P NN  /\  k  e.  ( ZZ>= ` 
1 ) )  -> 
( ( F `  NN ) `  k )  e.  CC )
416rpnnen2lem3 12745 . . . . . . . . 9  |-  seq  1
(  +  ,  ( F `  NN ) )  ~~>  ( 1  / 
2 )
4241a1i 11 . . . . . . . 8  |-  ( y  e.  ~P NN  ->  seq  1 (  +  , 
( F `  NN ) )  ~~>  ( 1  /  2 ) )
4332, 12, 33, 40, 42isumclim 12470 . . . . . . 7  |-  ( y  e.  ~P NN  ->  sum_ k  e.  ( ZZ>= ` 
1 ) ( ( F `  NN ) `
 k )  =  ( 1  /  2
) )
4431, 43breqtrd 4179 . . . . . 6  |-  ( y  e.  ~P NN  ->  sum_ k  e.  ( ZZ>= ` 
1 ) ( ( F `  y ) `
 k )  <_ 
( 1  /  2
) )
454, 44syl5eqbr 4188 . . . . 5  |-  ( y  e.  ~P NN  ->  sum_ k  e.  NN  (
( F `  y
) `  k )  <_  ( 1  /  2
) )
46 halflt1 10123 . . . . . . 7  |-  ( 1  /  2 )  <  1
4726, 25, 46ltleii 9129 . . . . . 6  |-  ( 1  /  2 )  <_ 
1
4847a1i 11 . . . . 5  |-  ( y  e.  ~P NN  ->  ( 1  /  2 )  <_  1 )
4910, 27, 28, 45, 48letrd 9161 . . . 4  |-  ( y  e.  ~P NN  ->  sum_ k  e.  NN  (
( F `  y
) `  k )  <_  1 )
50 0re 9026 . . . . 5  |-  0  e.  RR
5150, 25elicc2i 10910 . . . 4  |-  ( sum_ k  e.  NN  (
( F `  y
) `  k )  e.  ( 0 [,] 1
)  <->  ( sum_ k  e.  NN  ( ( F `
 y ) `  k )  e.  RR  /\  0  <_  sum_ k  e.  NN  ( ( F `
 y ) `  k )  /\  sum_ k  e.  NN  (
( F `  y
) `  k )  <_  1 ) )
5210, 24, 49, 51syl3anbrc 1138 . . 3  |-  ( y  e.  ~P NN  ->  sum_ k  e.  NN  (
( F `  y
) `  k )  e.  ( 0 [,] 1
) )
53 elpwi 3752 . . . . . . . . . . 11  |-  ( z  e.  ~P NN  ->  z 
C_  NN )
54 ssdifss 3423 . . . . . . . . . . . 12  |-  ( y 
C_  NN  ->  ( y 
\  z )  C_  NN )
55 ssdifss 3423 . . . . . . . . . . . 12  |-  ( z 
C_  NN  ->  ( z 
\  y )  C_  NN )
56 unss 3466 . . . . . . . . . . . . 13  |-  ( ( ( y  \  z
)  C_  NN  /\  (
z  \  y )  C_  NN )  <->  ( (
y  \  z )  u.  ( z  \  y
) )  C_  NN )
5756biimpi 187 . . . . . . . . . . . 12  |-  ( ( ( y  \  z
)  C_  NN  /\  (
z  \  y )  C_  NN )  ->  (
( y  \  z
)  u.  ( z 
\  y ) ) 
C_  NN )
5854, 55, 57syl2an 464 . . . . . . . . . . 11  |-  ( ( y  C_  NN  /\  z  C_  NN )  ->  (
( y  \  z
)  u.  ( z 
\  y ) ) 
C_  NN )
592, 53, 58syl2an 464 . . . . . . . . . 10  |-  ( ( y  e.  ~P NN  /\  z  e.  ~P NN )  ->  ( ( y 
\  z )  u.  ( z  \  y
) )  C_  NN )
60 eqss 3308 . . . . . . . . . . . . 13  |-  ( y  =  z  <->  ( y  C_  z  /\  z  C_  y ) )
61 ssdif0 3631 . . . . . . . . . . . . . 14  |-  ( y 
C_  z  <->  ( y  \  z )  =  (/) )
62 ssdif0 3631 . . . . . . . . . . . . . 14  |-  ( z 
C_  y  <->  ( z  \  y )  =  (/) )
6361, 62anbi12i 679 . . . . . . . . . . . . 13  |-  ( ( y  C_  z  /\  z  C_  y )  <->  ( (
y  \  z )  =  (/)  /\  ( z 
\  y )  =  (/) ) )
64 un00 3608 . . . . . . . . . . . . 13  |-  ( ( ( y  \  z
)  =  (/)  /\  (
z  \  y )  =  (/) )  <->  ( (
y  \  z )  u.  ( z  \  y
) )  =  (/) )
6560, 63, 643bitri 263 . . . . . . . . . . . 12  |-  ( y  =  z  <->  ( (
y  \  z )  u.  ( z  \  y
) )  =  (/) )
6665necon3bii 2584 . . . . . . . . . . 11  |-  ( y  =/=  z  <->  ( (
y  \  z )  u.  ( z  \  y
) )  =/=  (/) )
6766biimpi 187 . . . . . . . . . 10  |-  ( y  =/=  z  ->  (
( y  \  z
)  u.  ( z 
\  y ) )  =/=  (/) )
68 nnwo 10476 . . . . . . . . . 10  |-  ( ( ( ( y  \ 
z )  u.  (
z  \  y )
)  C_  NN  /\  (
( y  \  z
)  u.  ( z 
\  y ) )  =/=  (/) )  ->  E. m  e.  ( ( y  \ 
z )  u.  (
z  \  y )
) A. n  e.  ( ( y  \ 
z )  u.  (
z  \  y )
) m  <_  n
)
6959, 67, 68syl2an 464 . . . . . . . . 9  |-  ( ( ( y  e.  ~P NN  /\  z  e.  ~P NN )  /\  y  =/=  z )  ->  E. m  e.  ( ( y  \ 
z )  u.  (
z  \  y )
) A. n  e.  ( ( y  \ 
z )  u.  (
z  \  y )
) m  <_  n
)
7069ex 424 . . . . . . . 8  |-  ( ( y  e.  ~P NN  /\  z  e.  ~P NN )  ->  ( y  =/=  z  ->  E. m  e.  ( ( y  \ 
z )  u.  (
z  \  y )
) A. n  e.  ( ( y  \ 
z )  u.  (
z  \  y )
) m  <_  n
) )
7159sselda 3293 . . . . . . . . . 10  |-  ( ( ( y  e.  ~P NN  /\  z  e.  ~P NN )  /\  m  e.  ( ( y  \ 
z )  u.  (
z  \  y )
) )  ->  m  e.  NN )
72 df-ral 2656 . . . . . . . . . . . 12  |-  ( A. n  e.  ( (
y  \  z )  u.  ( z  \  y
) ) m  <_  n 
<-> 
A. n ( n  e.  ( ( y 
\  z )  u.  ( z  \  y
) )  ->  m  <_  n ) )
73 con34b 284 . . . . . . . . . . . . . 14  |-  ( ( n  e.  ( ( y  \  z )  u.  ( z  \ 
y ) )  ->  m  <_  n )  <->  ( -.  m  <_  n  ->  -.  n  e.  ( (
y  \  z )  u.  ( z  \  y
) ) ) )
74 eldif 3275 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( y  \ 
z )  <->  ( n  e.  y  /\  -.  n  e.  z ) )
75 eldif 3275 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( z  \ 
y )  <->  ( n  e.  z  /\  -.  n  e.  y ) )
7674, 75orbi12i 508 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  ( y 
\  z )  \/  n  e.  ( z 
\  y ) )  <-> 
( ( n  e.  y  /\  -.  n  e.  z )  \/  (
n  e.  z  /\  -.  n  e.  y
) ) )
77 elun 3433 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  ( ( y 
\  z )  u.  ( z  \  y
) )  <->  ( n  e.  ( y  \  z
)  \/  n  e.  ( z  \  y
) ) )
78 xor 862 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( n  e.  y  <-> 
n  e.  z )  <-> 
( ( n  e.  y  /\  -.  n  e.  z )  \/  (
n  e.  z  /\  -.  n  e.  y
) ) )
7976, 77, 783bitr4ri 270 . . . . . . . . . . . . . . . 16  |-  ( -.  ( n  e.  y  <-> 
n  e.  z )  <-> 
n  e.  ( ( y  \  z )  u.  ( z  \ 
y ) ) )
8079con1bii 322 . . . . . . . . . . . . . . 15  |-  ( -.  n  e.  ( ( y  \  z )  u.  ( z  \ 
y ) )  <->  ( n  e.  y  <->  n  e.  z
) )
8180imbi2i 304 . . . . . . . . . . . . . 14  |-  ( ( -.  m  <_  n  ->  -.  n  e.  ( ( y  \  z
)  u.  ( z 
\  y ) ) )  <->  ( -.  m  <_  n  ->  ( n  e.  y  <->  n  e.  z
) ) )
8273, 81bitri 241 . . . . . . . . . . . . 13  |-  ( ( n  e.  ( ( y  \  z )  u.  ( z  \ 
y ) )  ->  m  <_  n )  <->  ( -.  m  <_  n  ->  (
n  e.  y  <->  n  e.  z ) ) )
8382albii 1572 . . . . . . . . . . . 12  |-  ( A. n ( n  e.  ( ( y  \ 
z )  u.  (
z  \  y )
)  ->  m  <_  n )  <->  A. n ( -.  m  <_  n  ->  ( n  e.  y  <->  n  e.  z ) ) )
8472, 83bitri 241 . . . . . . . . . . 11  |-  ( A. n  e.  ( (
y  \  z )  u.  ( z  \  y
) ) m  <_  n 
<-> 
A. n ( -.  m  <_  n  ->  ( n  e.  y  <->  n  e.  z ) ) )
85 alral 2709 . . . . . . . . . . . 12  |-  ( A. n ( -.  m  <_  n  ->  ( n  e.  y  <->  n  e.  z
) )  ->  A. n  e.  NN  ( -.  m  <_  n  ->  ( n  e.  y  <->  n  e.  z
) ) )
86 nnre 9941 . . . . . . . . . . . . . . 15  |-  ( n  e.  NN  ->  n  e.  RR )
87 nnre 9941 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN  ->  m  e.  RR )
88 ltnle 9090 . . . . . . . . . . . . . . 15  |-  ( ( n  e.  RR  /\  m  e.  RR )  ->  ( n  <  m  <->  -.  m  <_  n )
)
8986, 87, 88syl2anr 465 . . . . . . . . . . . . . 14  |-  ( ( m  e.  NN  /\  n  e.  NN )  ->  ( n  <  m  <->  -.  m  <_  n )
)
9089imbi1d 309 . . . . . . . . . . . . 13  |-  ( ( m  e.  NN  /\  n  e.  NN )  ->  ( ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) )  <->  ( -.  m  <_  n  ->  (
n  e.  y  <->  n  e.  z ) ) ) )
9190ralbidva 2667 . . . . . . . . . . . 12  |-  ( m  e.  NN  ->  ( A. n  e.  NN  ( n  <  m  -> 
( n  e.  y  <-> 
n  e.  z ) )  <->  A. n  e.  NN  ( -.  m  <_  n  ->  ( n  e.  y  <->  n  e.  z
) ) ) )
9285, 91syl5ibr 213 . . . . . . . . . . 11  |-  ( m  e.  NN  ->  ( A. n ( -.  m  <_  n  ->  ( n  e.  y  <->  n  e.  z
) )  ->  A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) ) )
9384, 92syl5bi 209 . . . . . . . . . 10  |-  ( m  e.  NN  ->  ( A. n  e.  (
( y  \  z
)  u.  ( z 
\  y ) ) m  <_  n  ->  A. n  e.  NN  (
n  <  m  ->  ( n  e.  y  <->  n  e.  z ) ) ) )
9471, 93syl 16 . . . . . . . . 9  |-  ( ( ( y  e.  ~P NN  /\  z  e.  ~P NN )  /\  m  e.  ( ( y  \ 
z )  u.  (
z  \  y )
) )  ->  ( A. n  e.  (
( y  \  z
)  u.  ( z 
\  y ) ) m  <_  n  ->  A. n  e.  NN  (
n  <  m  ->  ( n  e.  y  <->  n  e.  z ) ) ) )
9594reximdva 2763 . . . . . . . 8  |-  ( ( y  e.  ~P NN  /\  z  e.  ~P NN )  ->  ( E. m  e.  ( ( y  \ 
z )  u.  (
z  \  y )
) A. n  e.  ( ( y  \ 
z )  u.  (
z  \  y )
) m  <_  n  ->  E. m  e.  ( ( y  \  z
)  u.  ( z 
\  y ) ) A. n  e.  NN  ( n  <  m  -> 
( n  e.  y  <-> 
n  e.  z ) ) ) )
9670, 95syld 42 . . . . . . 7  |-  ( ( y  e.  ~P NN  /\  z  e.  ~P NN )  ->  ( y  =/=  z  ->  E. m  e.  ( ( y  \ 
z )  u.  (
z  \  y )
) A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) ) )
97 rexun 3472 . . . . . . 7  |-  ( E. m  e.  ( ( y  \  z )  u.  ( z  \ 
y ) ) A. n  e.  NN  (
n  <  m  ->  ( n  e.  y  <->  n  e.  z ) )  <->  ( E. m  e.  ( y  \  z ) A. n  e.  NN  (
n  <  m  ->  ( n  e.  y  <->  n  e.  z ) )  \/ 
E. m  e.  ( z  \  y ) A. n  e.  NN  ( n  <  m  -> 
( n  e.  y  <-> 
n  e.  z ) ) ) )
9896, 97syl6ib 218 . . . . . 6  |-  ( ( y  e.  ~P NN  /\  z  e.  ~P NN )  ->  ( y  =/=  z  ->  ( E. m  e.  ( y  \  z ) A. n  e.  NN  (
n  <  m  ->  ( n  e.  y  <->  n  e.  z ) )  \/ 
E. m  e.  ( z  \  y ) A. n  e.  NN  ( n  <  m  -> 
( n  e.  y  <-> 
n  e.  z ) ) ) ) )
99 simpll 731 . . . . . . . . . 10  |-  ( ( ( y  C_  NN  /\  z  C_  NN )  /\  ( m  e.  ( y  \  z )  /\  A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) ) )  ->  y  C_  NN )
100 simplr 732 . . . . . . . . . 10  |-  ( ( ( y  C_  NN  /\  z  C_  NN )  /\  ( m  e.  ( y  \  z )  /\  A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) ) )  ->  z  C_  NN )
101 simprl 733 . . . . . . . . . 10  |-  ( ( ( y  C_  NN  /\  z  C_  NN )  /\  ( m  e.  ( y  \  z )  /\  A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) ) )  ->  m  e.  ( y  \  z ) )
102 simprr 734 . . . . . . . . . 10  |-  ( ( ( y  C_  NN  /\  z  C_  NN )  /\  ( m  e.  ( y  \  z )  /\  A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) ) )  ->  A. n  e.  NN  ( n  <  m  -> 
( n  e.  y  <-> 
n  e.  z ) ) )
103 biid 228 . . . . . . . . . 10  |-  ( sum_ k  e.  NN  (
( F `  y
) `  k )  =  sum_ k  e.  NN  ( ( F `  z ) `  k
)  <->  sum_ k  e.  NN  ( ( F `  y ) `  k
)  =  sum_ k  e.  NN  ( ( F `
 z ) `  k ) )
1046, 99, 100, 101, 102, 103rpnnen2lem11 12753 . . . . . . . . 9  |-  ( ( ( y  C_  NN  /\  z  C_  NN )  /\  ( m  e.  ( y  \  z )  /\  A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) ) )  ->  -.  sum_ k  e.  NN  ( ( F `
 y ) `  k )  =  sum_ k  e.  NN  (
( F `  z
) `  k )
)
105104rexlimdvaa 2776 . . . . . . . 8  |-  ( ( y  C_  NN  /\  z  C_  NN )  ->  ( E. m  e.  (
y  \  z ) A. n  e.  NN  ( n  <  m  -> 
( n  e.  y  <-> 
n  e.  z ) )  ->  -.  sum_ k  e.  NN  ( ( F `
 y ) `  k )  =  sum_ k  e.  NN  (
( F `  z
) `  k )
) )
106 simplr 732 . . . . . . . . . 10  |-  ( ( ( y  C_  NN  /\  z  C_  NN )  /\  ( m  e.  ( z  \  y )  /\  A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) ) )  ->  z  C_  NN )
107 simpll 731 . . . . . . . . . 10  |-  ( ( ( y  C_  NN  /\  z  C_  NN )  /\  ( m  e.  ( z  \  y )  /\  A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) ) )  ->  y  C_  NN )
108 simprl 733 . . . . . . . . . 10  |-  ( ( ( y  C_  NN  /\  z  C_  NN )  /\  ( m  e.  ( z  \  y )  /\  A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) ) )  ->  m  e.  ( z  \  y ) )
109 simprr 734 . . . . . . . . . . 11  |-  ( ( ( y  C_  NN  /\  z  C_  NN )  /\  ( m  e.  ( z  \  y )  /\  A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) ) )  ->  A. n  e.  NN  ( n  <  m  -> 
( n  e.  y  <-> 
n  e.  z ) ) )
110 bicom 192 . . . . . . . . . . . . 13  |-  ( ( n  e.  z  <->  n  e.  y )  <->  ( n  e.  y  <->  n  e.  z
) )
111110imbi2i 304 . . . . . . . . . . . 12  |-  ( ( n  <  m  -> 
( n  e.  z  <-> 
n  e.  y ) )  <->  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) )
112111ralbii 2675 . . . . . . . . . . 11  |-  ( A. n  e.  NN  (
n  <  m  ->  ( n  e.  z  <->  n  e.  y ) )  <->  A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) )
113109, 112sylibr 204 . . . . . . . . . 10  |-  ( ( ( y  C_  NN  /\  z  C_  NN )  /\  ( m  e.  ( z  \  y )  /\  A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) ) )  ->  A. n  e.  NN  ( n  <  m  -> 
( n  e.  z  <-> 
n  e.  y ) ) )
114 eqcom 2391 . . . . . . . . . 10  |-  ( sum_ k  e.  NN  (
( F `  y
) `  k )  =  sum_ k  e.  NN  ( ( F `  z ) `  k
)  <->  sum_ k  e.  NN  ( ( F `  z ) `  k
)  =  sum_ k  e.  NN  ( ( F `
 y ) `  k ) )
1156, 106, 107, 108, 113, 114rpnnen2lem11 12753 . . . . . . . . 9  |-  ( ( ( y  C_  NN  /\  z  C_  NN )  /\  ( m  e.  ( z  \  y )  /\  A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) ) )  ->  -.  sum_ k  e.  NN  ( ( F `
 y ) `  k )  =  sum_ k  e.  NN  (
( F `  z
) `  k )
)
116115rexlimdvaa 2776 . . . . . . . 8  |-  ( ( y  C_  NN  /\  z  C_  NN )  ->  ( E. m  e.  (
z  \  y ) A. n  e.  NN  ( n  <  m  -> 
( n  e.  y  <-> 
n  e.  z ) )  ->  -.  sum_ k  e.  NN  ( ( F `
 y ) `  k )  =  sum_ k  e.  NN  (
( F `  z
) `  k )
) )
117105, 116jaod 370 . . . . . . 7  |-  ( ( y  C_  NN  /\  z  C_  NN )  ->  (
( E. m  e.  ( y  \  z
) A. n  e.  NN  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) )  \/  E. m  e.  ( z  \  y ) A. n  e.  NN  (
n  <  m  ->  ( n  e.  y  <->  n  e.  z ) ) )  ->  -.  sum_ k  e.  NN  ( ( F `
 y ) `  k )  =  sum_ k  e.  NN  (
( F `  z
) `  k )
) )
1182, 53, 117syl2an 464 . . . . . 6  |-  ( ( y  e.  ~P NN  /\  z  e.  ~P NN )  ->  ( ( E. m  e.  ( y 
\  z ) A. n  e.  NN  (
n  <  m  ->  ( n  e.  y  <->  n  e.  z ) )  \/ 
E. m  e.  ( z  \  y ) A. n  e.  NN  ( n  <  m  -> 
( n  e.  y  <-> 
n  e.  z ) ) )  ->  -.  sum_ k  e.  NN  (
( F `  y
) `  k )  =  sum_ k  e.  NN  ( ( F `  z ) `  k
) ) )
11998, 118syld 42 . . . . 5  |-  ( ( y  e.  ~P NN  /\  z  e.  ~P NN )  ->  ( y  =/=  z  ->  -.  sum_ k  e.  NN  ( ( F `
 y ) `  k )  =  sum_ k  e.  NN  (
( F `  z
) `  k )
) )
120119necon4ad 2613 . . . 4  |-  ( ( y  e.  ~P NN  /\  z  e.  ~P NN )  ->  ( sum_ k  e.  NN  ( ( F `
 y ) `  k )  =  sum_ k  e.  NN  (
( F `  z
) `  k )  ->  y  =  z ) )
121 fveq2 5670 . . . . . 6  |-  ( y  =  z  ->  ( F `  y )  =  ( F `  z ) )
122121fveq1d 5672 . . . . 5  |-  ( y  =  z  ->  (
( F `  y
) `  k )  =  ( ( F `
 z ) `  k ) )
123122sumeq2sdv 12427 . . . 4  |-  ( y  =  z  ->  sum_ k  e.  NN  ( ( F `
 y ) `  k )  =  sum_ k  e.  NN  (
( F `  z
) `  k )
)
124120, 123impbid1 195 . . 3  |-  ( ( y  e.  ~P NN  /\  z  e.  ~P NN )  ->  ( sum_ k  e.  NN  ( ( F `
 y ) `  k )  =  sum_ k  e.  NN  (
( F `  z
) `  k )  <->  y  =  z ) )
12552, 124dom2 7088 . 2  |-  ( ( 0 [,] 1 )  e.  _V  ->  ~P NN 
~<_  ( 0 [,] 1
) )
1261, 125ax-mp 8 1  |-  ~P NN  ~<_  ( 0 [,] 1
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359   A.wal 1546    = wceq 1649    e. wcel 1717    =/= wne 2552   A.wral 2651   E.wrex 2652   _Vcvv 2901    \ cdif 3262    u. cun 3263    C_ wss 3265   (/)c0 3573   ifcif 3684   ~Pcpw 3744   class class class wbr 4155    e. cmpt 4209   dom cdm 4820   -->wf 5392   ` cfv 5396  (class class class)co 6022    ~<_ cdom 7045   CCcc 8923   RRcr 8924   0cc0 8925   1c1 8926    + caddc 8928    < clt 9055    <_ cle 9056    / cdiv 9611   NNcn 9934   2c2 9983   3c3 9984   ZZcz 10216   ZZ>=cuz 10422   [,]cicc 10853    seq cseq 11252   ^cexp 11311    ~~> cli 12207   sum_csu 12408
This theorem is referenced by:  rpnnen  12755  opnreen  18735
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-rep 4263  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643  ax-inf2 7531  ax-cnex 8981  ax-resscn 8982  ax-1cn 8983  ax-icn 8984  ax-addcl 8985  ax-addrcl 8986  ax-mulcl 8987  ax-mulrcl 8988  ax-mulcom 8989  ax-addass 8990  ax-mulass 8991  ax-distr 8992  ax-i2m1 8993  ax-1ne0 8994  ax-1rid 8995  ax-rnegex 8996  ax-rrecex 8997  ax-cnre 8998  ax-pre-lttri 8999  ax-pre-lttrn 9000  ax-pre-ltadd 9001  ax-pre-mulgt0 9002  ax-pre-sup 9003
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-nel 2555  df-ral 2656  df-rex 2657  df-reu 2658  df-rmo 2659  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-pss 3281  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-tp 3767  df-op 3768  df-uni 3960  df-int 3995  df-iun 4039  df-br 4156  df-opab 4210  df-mpt 4211  df-tr 4246  df-eprel 4437  df-id 4441  df-po 4446  df-so 4447  df-fr 4484  df-se 4485  df-we 4486  df-ord 4527  df-on 4528  df-lim 4529  df-suc 4530  df-om 4788  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-isom 5405  df-ov 6025  df-oprab 6026  df-mpt2 6027  df-1st 6290  df-2nd 6291  df-riota 6487  df-recs 6571  df-rdg 6606  df-1o 6662  df-oadd 6666  df-er 6843  df-pm 6959  df-en 7048  df-dom 7049  df-sdom 7050  df-fin 7051  df-sup 7383  df-oi 7414  df-card 7761  df-pnf 9057  df-mnf 9058  df-xr 9059  df-ltxr 9060  df-le 9061  df-sub 9227  df-neg 9228  df-div 9612  df-nn 9935  df-2 9992  df-3 9993  df-n0 10156  df-z 10217  df-uz 10423  df-rp 10547  df-ico 10856  df-icc 10857  df-fz 10978  df-fzo 11068  df-fl 11131  df-seq 11253  df-exp 11312  df-hash 11548  df-cj 11833  df-re 11834  df-im 11835  df-sqr 11969  df-abs 11970  df-limsup 12194  df-clim 12211  df-rlim 12212  df-sum 12409
  Copyright terms: Public domain W3C validator