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

Theorem rpnnen2 13520
Description: The other half of rpnnen 13521, where we show an injection from sets of positive integers 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... 13353). 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 positive integers 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 13509). This is an infinite sum of real numbers (rpnnen2lem2 13510), and since  A 
C_  B implies  ( F `  A )  <_  ( F `  B ) (rpnnen2lem4 13512) and  ( F `  NN ) converges to  1  /  2 (rpnnen2lem3 13511) by geoisum1 13351, the sum is convergent to some real (rpnnen2lem5 13513 and rpnnen2lem6 13514) by the comparison test for convergence cvgcmp 13291. The comparison test also tells us that  A  C_  B implies  sum_ ( F `  A )  <_ 
sum_ ( F `  B ) (rpnnen2lem7 13515).

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 13516) and cancel them (rpnnen2lem10 13518), 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 13517) and  sum_ ( F `  { m } )  =  ( 3 ^
-u m ), we establish that  sum_ ( F `
 y )  <  sum_ ( F `  x
) (rpnnen2lem11 13519) 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 6128 . 2  |-  ( 0 [,] 1 )  e. 
_V
2 elpwi 3881 . . . . 5  |-  ( y  e.  ~P NN  ->  y 
C_  NN )
3 nnuz 10908 . . . . . . 7  |-  NN  =  ( ZZ>= `  1 )
43sumeq1i 13187 . . . . . 6  |-  sum_ k  e.  NN  ( ( F `
 y ) `  k )  =  sum_ k  e.  ( ZZ>= ` 
1 ) ( ( F `  y ) `
 k )
5 1nn 10345 . . . . . . 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 13514 . . . . . . 7  |-  ( ( y  C_  NN  /\  1  e.  NN )  ->  sum_ k  e.  ( ZZ>= `  1 )
( ( F `  y ) `  k
)  e.  RR )
85, 7mpan2 671 . . . . . 6  |-  ( y 
C_  NN  ->  sum_ k  e.  ( ZZ>= `  1 )
( ( F `  y ) `  k
)  e.  RR )
94, 8syl5eqel 2527 . . . . 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 1zzd 10689 . . . . 5  |-  ( y  e.  ~P NN  ->  1  e.  ZZ )
12 eqidd 2444 . . . . 5  |-  ( ( y  e.  ~P NN  /\  k  e.  NN )  ->  ( ( F `
 y ) `  k )  =  ( ( F `  y
) `  k )
)
136rpnnen2lem2 13510 . . . . . . 7  |-  ( y 
C_  NN  ->  ( F `
 y ) : NN --> RR )
142, 13syl 16 . . . . . 6  |-  ( y  e.  ~P NN  ->  ( F `  y ) : NN --> RR )
1514ffvelrnda 5855 . . . . 5  |-  ( ( y  e.  ~P NN  /\  k  e.  NN )  ->  ( ( F `
 y ) `  k )  e.  RR )
166rpnnen2lem5 13513 . . . . . 6  |-  ( ( y  C_  NN  /\  1  e.  NN )  ->  seq 1 (  +  , 
( F `  y
) )  e.  dom  ~~>  )
172, 5, 16sylancl 662 . . . . 5  |-  ( y  e.  ~P NN  ->  seq 1 (  +  , 
( F `  y
) )  e.  dom  ~~>  )
18 ssid 3387 . . . . . . . 8  |-  NN  C_  NN
196rpnnen2lem4 13512 . . . . . . . 8  |-  ( ( y  C_  NN  /\  NN  C_  NN  /\  k  e.  NN )  ->  (
0  <_  ( ( F `  y ) `  k )  /\  (
( F `  y
) `  k )  <_  ( ( F `  NN ) `  k ) ) )
2018, 19mp3an2 1302 . . . . . . 7  |-  ( ( y  C_  NN  /\  k  e.  NN )  ->  (
0  <_  ( ( F `  y ) `  k )  /\  (
( F `  y
) `  k )  <_  ( ( F `  NN ) `  k ) ) )
2120simpld 459 . . . . . 6  |-  ( ( y  C_  NN  /\  k  e.  NN )  ->  0  <_  ( ( F `  y ) `  k
) )
222, 21sylan 471 . . . . 5  |-  ( ( y  e.  ~P NN  /\  k  e.  NN )  ->  0  <_  (
( F `  y
) `  k )
)
233, 11, 12, 15, 17, 22isumge0 13245 . . . 4  |-  ( y  e.  ~P NN  ->  0  <_  sum_ k  e.  NN  ( ( F `  y ) `  k
) )
24 halfre 10552 . . . . . 6  |-  ( 1  /  2 )  e.  RR
2524a1i 11 . . . . 5  |-  ( y  e.  ~P NN  ->  ( 1  /  2 )  e.  RR )
26 1re 9397 . . . . . 6  |-  1  e.  RR
2726a1i 11 . . . . 5  |-  ( y  e.  ~P NN  ->  1  e.  RR )
286rpnnen2lem7 13515 . . . . . . . . 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 ) )
2918, 5, 28mp3an23 1306 . . . . . . . 8  |-  ( y 
C_  NN  ->  sum_ k  e.  ( ZZ>= `  1 )
( ( F `  y ) `  k
)  <_  sum_ k  e.  ( ZZ>= `  1 )
( ( F `  NN ) `  k ) )
302, 29syl 16 . . . . . . 7  |-  ( y  e.  ~P NN  ->  sum_ k  e.  ( ZZ>= ` 
1 ) ( ( F `  y ) `
 k )  <_  sum_ k  e.  ( ZZ>= ` 
1 ) ( ( F `  NN ) `
 k ) )
31 eqid 2443 . . . . . . . 8  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  1 )
32 eqidd 2444 . . . . . . . 8  |-  ( ( y  e.  ~P NN  /\  k  e.  ( ZZ>= ` 
1 ) )  -> 
( ( F `  NN ) `  k )  =  ( ( F `
 NN ) `  k ) )
33 elnnuz 10909 . . . . . . . . . 10  |-  ( k  e.  NN  <->  k  e.  ( ZZ>= `  1 )
)
346rpnnen2lem2 13510 . . . . . . . . . . . . 13  |-  ( NN  C_  NN  ->  ( F `  NN ) : NN --> RR )
3518, 34ax-mp 5 . . . . . . . . . . . 12  |-  ( F `
 NN ) : NN --> RR
3635ffvelrni 5854 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  (
( F `  NN ) `  k )  e.  RR )
3736recnd 9424 . . . . . . . . . 10  |-  ( k  e.  NN  ->  (
( F `  NN ) `  k )  e.  CC )
3833, 37sylbir 213 . . . . . . . . 9  |-  ( k  e.  ( ZZ>= `  1
)  ->  ( ( F `  NN ) `  k )  e.  CC )
3938adantl 466 . . . . . . . 8  |-  ( ( y  e.  ~P NN  /\  k  e.  ( ZZ>= ` 
1 ) )  -> 
( ( F `  NN ) `  k )  e.  CC )
406rpnnen2lem3 13511 . . . . . . . . 9  |-  seq 1
(  +  ,  ( F `  NN ) )  ~~>  ( 1  / 
2 )
4140a1i 11 . . . . . . . 8  |-  ( y  e.  ~P NN  ->  seq 1 (  +  , 
( F `  NN ) )  ~~>  ( 1  /  2 ) )
4231, 11, 32, 39, 41isumclim 13236 . . . . . . 7  |-  ( y  e.  ~P NN  ->  sum_ k  e.  ( ZZ>= ` 
1 ) ( ( F `  NN ) `
 k )  =  ( 1  /  2
) )
4330, 42breqtrd 4328 . . . . . 6  |-  ( y  e.  ~P NN  ->  sum_ k  e.  ( ZZ>= ` 
1 ) ( ( F `  y ) `
 k )  <_ 
( 1  /  2
) )
444, 43syl5eqbr 4337 . . . . 5  |-  ( y  e.  ~P NN  ->  sum_ k  e.  NN  (
( F `  y
) `  k )  <_  ( 1  /  2
) )
45 halflt1 10555 . . . . . . 7  |-  ( 1  /  2 )  <  1
4624, 26, 45ltleii 9509 . . . . . 6  |-  ( 1  /  2 )  <_ 
1
4746a1i 11 . . . . 5  |-  ( y  e.  ~P NN  ->  ( 1  /  2 )  <_  1 )
4810, 25, 27, 44, 47letrd 9540 . . . 4  |-  ( y  e.  ~P NN  ->  sum_ k  e.  NN  (
( F `  y
) `  k )  <_  1 )
49 0re 9398 . . . . 5  |-  0  e.  RR
5049, 26elicc2i 11373 . . . 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 ) )
5110, 23, 48, 50syl3anbrc 1172 . . 3  |-  ( y  e.  ~P NN  ->  sum_ k  e.  NN  (
( F `  y
) `  k )  e.  ( 0 [,] 1
) )
52 elpwi 3881 . . . . . . . . . . 11  |-  ( z  e.  ~P NN  ->  z 
C_  NN )
53 ssdifss 3499 . . . . . . . . . . . 12  |-  ( y 
C_  NN  ->  ( y 
\  z )  C_  NN )
54 ssdifss 3499 . . . . . . . . . . . 12  |-  ( z 
C_  NN  ->  ( z 
\  y )  C_  NN )
55 unss 3542 . . . . . . . . . . . . 13  |-  ( ( ( y  \  z
)  C_  NN  /\  (
z  \  y )  C_  NN )  <->  ( (
y  \  z )  u.  ( z  \  y
) )  C_  NN )
5655biimpi 194 . . . . . . . . . . . 12  |-  ( ( ( y  \  z
)  C_  NN  /\  (
z  \  y )  C_  NN )  ->  (
( y  \  z
)  u.  ( z 
\  y ) ) 
C_  NN )
5753, 54, 56syl2an 477 . . . . . . . . . . 11  |-  ( ( y  C_  NN  /\  z  C_  NN )  ->  (
( y  \  z
)  u.  ( z 
\  y ) ) 
C_  NN )
582, 52, 57syl2an 477 . . . . . . . . . 10  |-  ( ( y  e.  ~P NN  /\  z  e.  ~P NN )  ->  ( ( y 
\  z )  u.  ( z  \  y
) )  C_  NN )
59 eqss 3383 . . . . . . . . . . . . 13  |-  ( y  =  z  <->  ( y  C_  z  /\  z  C_  y ) )
60 ssdif0 3749 . . . . . . . . . . . . . 14  |-  ( y 
C_  z  <->  ( y  \  z )  =  (/) )
61 ssdif0 3749 . . . . . . . . . . . . . 14  |-  ( z 
C_  y  <->  ( z  \  y )  =  (/) )
6260, 61anbi12i 697 . . . . . . . . . . . . 13  |-  ( ( y  C_  z  /\  z  C_  y )  <->  ( (
y  \  z )  =  (/)  /\  ( z 
\  y )  =  (/) ) )
63 un00 3726 . . . . . . . . . . . . 13  |-  ( ( ( y  \  z
)  =  (/)  /\  (
z  \  y )  =  (/) )  <->  ( (
y  \  z )  u.  ( z  \  y
) )  =  (/) )
6459, 62, 633bitri 271 . . . . . . . . . . . 12  |-  ( y  =  z  <->  ( (
y  \  z )  u.  ( z  \  y
) )  =  (/) )
6564necon3bii 2652 . . . . . . . . . . 11  |-  ( y  =/=  z  <->  ( (
y  \  z )  u.  ( z  \  y
) )  =/=  (/) )
6665biimpi 194 . . . . . . . . . 10  |-  ( y  =/=  z  ->  (
( y  \  z
)  u.  ( z 
\  y ) )  =/=  (/) )
67 nnwo 10932 . . . . . . . . . 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
)
6858, 66, 67syl2an 477 . . . . . . . . 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
)
6968ex 434 . . . . . . . 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
) )
7058sselda 3368 . . . . . . . . . 10  |-  ( ( ( y  e.  ~P NN  /\  z  e.  ~P NN )  /\  m  e.  ( ( y  \ 
z )  u.  (
z  \  y )
) )  ->  m  e.  NN )
71 df-ral 2732 . . . . . . . . . . . 12  |-  ( A. n  e.  ( (
y  \  z )  u.  ( z  \  y
) ) m  <_  n 
<-> 
A. n ( n  e.  ( ( y 
\  z )  u.  ( z  \  y
) )  ->  m  <_  n ) )
72 con34b 292 . . . . . . . . . . . . . 14  |-  ( ( n  e.  ( ( y  \  z )  u.  ( z  \ 
y ) )  ->  m  <_  n )  <->  ( -.  m  <_  n  ->  -.  n  e.  ( (
y  \  z )  u.  ( z  \  y
) ) ) )
73 eldif 3350 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( y  \ 
z )  <->  ( n  e.  y  /\  -.  n  e.  z ) )
74 eldif 3350 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( z  \ 
y )  <->  ( n  e.  z  /\  -.  n  e.  y ) )
7573, 74orbi12i 521 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  ( y 
\  z )  \/  n  e.  ( z 
\  y ) )  <-> 
( ( n  e.  y  /\  -.  n  e.  z )  \/  (
n  e.  z  /\  -.  n  e.  y
) ) )
76 elun 3509 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  ( ( y 
\  z )  u.  ( z  \  y
) )  <->  ( n  e.  ( y  \  z
)  \/  n  e.  ( z  \  y
) ) )
77 xor 886 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( n  e.  y  <-> 
n  e.  z )  <-> 
( ( n  e.  y  /\  -.  n  e.  z )  \/  (
n  e.  z  /\  -.  n  e.  y
) ) )
7875, 76, 773bitr4ri 278 . . . . . . . . . . . . . . . 16  |-  ( -.  ( n  e.  y  <-> 
n  e.  z )  <-> 
n  e.  ( ( y  \  z )  u.  ( z  \ 
y ) ) )
7978con1bii 331 . . . . . . . . . . . . . . 15  |-  ( -.  n  e.  ( ( y  \  z )  u.  ( z  \ 
y ) )  <->  ( n  e.  y  <->  n  e.  z
) )
8079imbi2i 312 . . . . . . . . . . . . . 14  |-  ( ( -.  m  <_  n  ->  -.  n  e.  ( ( y  \  z
)  u.  ( z 
\  y ) ) )  <->  ( -.  m  <_  n  ->  ( n  e.  y  <->  n  e.  z
) ) )
8172, 80bitri 249 . . . . . . . . . . . . 13  |-  ( ( n  e.  ( ( y  \  z )  u.  ( z  \ 
y ) )  ->  m  <_  n )  <->  ( -.  m  <_  n  ->  (
n  e.  y  <->  n  e.  z ) ) )
8281albii 1610 . . . . . . . . . . . 12  |-  ( A. n ( n  e.  ( ( y  \ 
z )  u.  (
z  \  y )
)  ->  m  <_  n )  <->  A. n ( -.  m  <_  n  ->  ( n  e.  y  <->  n  e.  z ) ) )
8371, 82bitri 249 . . . . . . . . . . 11  |-  ( A. n  e.  ( (
y  \  z )  u.  ( z  \  y
) ) m  <_  n 
<-> 
A. n ( -.  m  <_  n  ->  ( n  e.  y  <->  n  e.  z ) ) )
84 alral 2786 . . . . . . . . . . . 12  |-  ( A. n ( -.  m  <_  n  ->  ( n  e.  y  <->  n  e.  z
) )  ->  A. n  e.  NN  ( -.  m  <_  n  ->  ( n  e.  y  <->  n  e.  z
) ) )
85 nnre 10341 . . . . . . . . . . . . . . 15  |-  ( n  e.  NN  ->  n  e.  RR )
86 nnre 10341 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN  ->  m  e.  RR )
87 ltnle 9466 . . . . . . . . . . . . . . 15  |-  ( ( n  e.  RR  /\  m  e.  RR )  ->  ( n  <  m  <->  -.  m  <_  n )
)
8885, 86, 87syl2anr 478 . . . . . . . . . . . . . 14  |-  ( ( m  e.  NN  /\  n  e.  NN )  ->  ( n  <  m  <->  -.  m  <_  n )
)
8988imbi1d 317 . . . . . . . . . . . . 13  |-  ( ( m  e.  NN  /\  n  e.  NN )  ->  ( ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) )  <->  ( -.  m  <_  n  ->  (
n  e.  y  <->  n  e.  z ) ) ) )
9089ralbidva 2743 . . . . . . . . . . . 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
) ) ) )
9184, 90syl5ibr 221 . . . . . . . . . . 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
) ) ) )
9283, 91syl5bi 217 . . . . . . . . . 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 ) ) ) )
9370, 92syl 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 ) ) ) )
9493reximdva 2840 . . . . . . . 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 ) ) ) )
9569, 94syld 44 . . . . . . 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
) ) ) )
96 rexun 3548 . . . . . . 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 ) ) ) )
9795, 96syl6ib 226 . . . . . 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 ) ) ) ) )
98 simpll 753 . . . . . . . . . 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 )
99 simplr 754 . . . . . . . . . 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 )
100 simprl 755 . . . . . . . . . 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 ) )
101 simprr 756 . . . . . . . . . 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 ) ) )
102 biid 236 . . . . . . . . . 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 ) )
1036, 98, 99, 100, 101, 102rpnnen2lem11 13519 . . . . . . . . 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 )
)
104103rexlimdvaa 2854 . . . . . . . 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 )
) )
105 simplr 754 . . . . . . . . . 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 )
106 simpll 753 . . . . . . . . . 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 )
107 simprl 755 . . . . . . . . . 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 ) )
108 simprr 756 . . . . . . . . . . 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 ) ) )
109 bicom 200 . . . . . . . . . . . . 13  |-  ( ( n  e.  z  <->  n  e.  y )  <->  ( n  e.  y  <->  n  e.  z
) )
110109imbi2i 312 . . . . . . . . . . . 12  |-  ( ( n  <  m  -> 
( n  e.  z  <-> 
n  e.  y ) )  <->  ( n  < 
m  ->  ( n  e.  y  <->  n  e.  z
) ) )
111110ralbii 2751 . . . . . . . . . . 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
) ) )
112108, 111sylibr 212 . . . . . . . . . 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 ) ) )
113 eqcom 2445 . . . . . . . . . 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 ) )
1146, 105, 106, 107, 112, 113rpnnen2lem11 13519 . . . . . . . . 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 )
)
115114rexlimdvaa 2854 . . . . . . . 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 )
) )
116104, 115jaod 380 . . . . . . 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 )
) )
1172, 52, 116syl2an 477 . . . . . 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
) ) )
11897, 117syld 44 . . . . 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 )
) )
119118necon4ad 2684 . . . 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 ) )
120 fveq2 5703 . . . . . 6  |-  ( y  =  z  ->  ( F `  y )  =  ( F `  z ) )
121120fveq1d 5705 . . . . 5  |-  ( y  =  z  ->  (
( F `  y
) `  k )  =  ( ( F `
 z ) `  k ) )
122121sumeq2sdv 13193 . . . 4  |-  ( y  =  z  ->  sum_ k  e.  NN  ( ( F `
 y ) `  k )  =  sum_ k  e.  NN  (
( F `  z
) `  k )
)
123119, 122impbid1 203 . . 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 ) )
12451, 123dom2 7364 . 2  |-  ( ( 0 [,] 1 )  e.  _V  ->  ~P NN 
~<_  ( 0 [,] 1
) )
1251, 124ax-mp 5 1  |-  ~P NN  ~<_  ( 0 [,] 1
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369   A.wal 1367    = wceq 1369    e. wcel 1756    =/= wne 2618   A.wral 2727   E.wrex 2728   _Vcvv 2984    \ cdif 3337    u. cun 3338    C_ wss 3340   (/)c0 3649   ifcif 3803   ~Pcpw 3872   class class class wbr 4304    e. cmpt 4362   dom cdm 4852   -->wf 5426   ` cfv 5430  (class class class)co 6103    ~<_ cdom 7320   CCcc 9292   RRcr 9293   0cc0 9294   1c1 9295    + caddc 9297    < clt 9430    <_ cle 9431    / cdiv 10005   NNcn 10334   2c2 10383   3c3 10384   ZZ>=cuz 10873   [,]cicc 11315    seqcseq 11818   ^cexp 11877    ~~> cli 12974   sum_csu 13175
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4415  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384  ax-inf2 7859  ax-cnex 9350  ax-resscn 9351  ax-1cn 9352  ax-icn 9353  ax-addcl 9354  ax-addrcl 9355  ax-mulcl 9356  ax-mulrcl 9357  ax-mulcom 9358  ax-addass 9359  ax-mulass 9360  ax-distr 9361  ax-i2m1 9362  ax-1ne0 9363  ax-1rid 9364  ax-rnegex 9365  ax-rrecex 9366  ax-cnre 9367  ax-pre-lttri 9368  ax-pre-lttrn 9369  ax-pre-ltadd 9370  ax-pre-mulgt0 9371  ax-pre-sup 9372
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-nel 2621  df-ral 2732  df-rex 2733  df-reu 2734  df-rmo 2735  df-rab 2736  df-v 2986  df-sbc 3199  df-csb 3301  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-pss 3356  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-tp 3894  df-op 3896  df-uni 4104  df-int 4141  df-iun 4185  df-br 4305  df-opab 4363  df-mpt 4364  df-tr 4398  df-eprel 4644  df-id 4648  df-po 4653  df-so 4654  df-fr 4691  df-se 4692  df-we 4693  df-ord 4734  df-on 4735  df-lim 4736  df-suc 4737  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-f1 5435  df-fo 5436  df-f1o 5437  df-fv 5438  df-isom 5439  df-riota 6064  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-om 6489  df-1st 6589  df-2nd 6590  df-recs 6844  df-rdg 6878  df-1o 6932  df-oadd 6936  df-er 7113  df-pm 7229  df-en 7323  df-dom 7324  df-sdom 7325  df-fin 7326  df-sup 7703  df-oi 7736  df-card 8121  df-pnf 9432  df-mnf 9433  df-xr 9434  df-ltxr 9435  df-le 9436  df-sub 9609  df-neg 9610  df-div 10006  df-nn 10335  df-2 10392  df-3 10393  df-n0 10592  df-z 10659  df-uz 10874  df-rp 11004  df-ico 11318  df-icc 11319  df-fz 11450  df-fzo 11561  df-fl 11654  df-seq 11819  df-exp 11878  df-hash 12116  df-cj 12600  df-re 12601  df-im 12602  df-sqr 12736  df-abs 12737  df-limsup 12961  df-clim 12978  df-rlim 12979  df-sum 13176
This theorem is referenced by:  rpnnen  13521  opnreen  20420
  Copyright terms: Public domain W3C validator