Metamath Proof Explorer

Theorem rpnnen2lem12

Description: Lemma for rpnnen2 . (Contributed by Mario Carneiro, 13-May-2013)

Ref Expression
Hypothesis rpnnen2.1 
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
Assertion rpnnen2lem12 
|- ~P NN ~<_ ( 0 [,] 1 )

Proof

Step Hyp Ref Expression
1 rpnnen2.1 
 |-  F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
2 ovex 
 |-  ( 0 [,] 1 ) e. _V
3 elpwi 
 |-  ( y e. ~P NN -> y C_ NN )
4 nnuz 
 |-  NN = ( ZZ>= ` 1 )
5 4 sumeq1i 
 |-  sum_ k e. NN ( ( F ` y ) ` k ) = sum_ k e. ( ZZ>= ` 1 ) ( ( F ` y ) ` k )
6 1nn 
 |-  1 e. NN
7 1 rpnnen2lem6 
 |-  ( ( y C_ NN /\ 1 e. NN ) -> sum_ k e. ( ZZ>= ` 1 ) ( ( F ` y ) ` k ) e. RR )
8 6 7 mpan2 
 |-  ( y C_ NN -> sum_ k e. ( ZZ>= ` 1 ) ( ( F ` y ) ` k ) e. RR )
9 5 8 eqeltrid 
 |-  ( y C_ NN -> sum_ k e. NN ( ( F ` y ) ` k ) e. RR )
10 3 9 syl 
 |-  ( y e. ~P NN -> sum_ k e. NN ( ( F ` y ) ` k ) e. RR )
11 1zzd 
 |-  ( y e. ~P NN -> 1 e. ZZ )
12 eqidd 
 |-  ( ( y e. ~P NN /\ k e. NN ) -> ( ( F ` y ) ` k ) = ( ( F ` y ) ` k ) )
13 1 rpnnen2lem2 
 |-  ( y C_ NN -> ( F ` y ) : NN --> RR )
14 3 13 syl 
 |-  ( y e. ~P NN -> ( F ` y ) : NN --> RR )
15 14 ffvelcdmda 
 |-  ( ( y e. ~P NN /\ k e. NN ) -> ( ( F ` y ) ` k ) e. RR )
16 1 rpnnen2lem5 
 |-  ( ( y C_ NN /\ 1 e. NN ) -> seq 1 ( + , ( F ` y ) ) e. dom ~~> )
17 3 6 16 sylancl 
 |-  ( y e. ~P NN -> seq 1 ( + , ( F ` y ) ) e. dom ~~> )
18 ssid 
 |-  NN C_ NN
19 1 rpnnen2lem4 
 |-  ( ( y C_ NN /\ NN C_ NN /\ k e. NN ) -> ( 0 <_ ( ( F ` y ) ` k ) /\ ( ( F ` y ) ` k ) <_ ( ( F ` NN ) ` k ) ) )
20 18 19 mp3an2 
 |-  ( ( y C_ NN /\ k e. NN ) -> ( 0 <_ ( ( F ` y ) ` k ) /\ ( ( F ` y ) ` k ) <_ ( ( F ` NN ) ` k ) ) )
21 20 simpld 
 |-  ( ( y C_ NN /\ k e. NN ) -> 0 <_ ( ( F ` y ) ` k ) )
22 3 21 sylan 
 |-  ( ( y e. ~P NN /\ k e. NN ) -> 0 <_ ( ( F ` y ) ` k ) )
23 4 11 12 15 17 22 isumge0 
 |-  ( y e. ~P NN -> 0 <_ sum_ k e. NN ( ( F ` y ) ` k ) )
24 halfre 
 |-  ( 1 / 2 ) e. RR
25 24 a1i 
 |-  ( y e. ~P NN -> ( 1 / 2 ) e. RR )
26 1re 
 |-  1 e. RR
27 26 a1i 
 |-  ( y e. ~P NN -> 1 e. RR )
28 1 rpnnen2lem7 
 |-  ( ( 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 ) )
29 18 6 28 mp3an23 
 |-  ( y C_ NN -> sum_ k e. ( ZZ>= ` 1 ) ( ( F ` y ) ` k ) <_ sum_ k e. ( ZZ>= ` 1 ) ( ( F ` NN ) ` k ) )
30 3 29 syl 
 |-  ( y e. ~P NN -> sum_ k e. ( ZZ>= ` 1 ) ( ( F ` y ) ` k ) <_ sum_ k e. ( ZZ>= ` 1 ) ( ( F ` NN ) ` k ) )
31 eqid 
 |-  ( ZZ>= ` 1 ) = ( ZZ>= ` 1 )
32 eqidd 
 |-  ( ( y e. ~P NN /\ k e. ( ZZ>= ` 1 ) ) -> ( ( F ` NN ) ` k ) = ( ( F ` NN ) ` k ) )
33 elnnuz 
 |-  ( k e. NN <-> k e. ( ZZ>= ` 1 ) )
34 1 rpnnen2lem2 
 |-  ( NN C_ NN -> ( F ` NN ) : NN --> RR )
35 18 34 ax-mp 
 |-  ( F ` NN ) : NN --> RR
36 35 ffvelcdmi 
 |-  ( k e. NN -> ( ( F ` NN ) ` k ) e. RR )
37 36 recnd 
 |-  ( k e. NN -> ( ( F ` NN ) ` k ) e. CC )
38 33 37 sylbir 
 |-  ( k e. ( ZZ>= ` 1 ) -> ( ( F ` NN ) ` k ) e. CC )
39 38 adantl 
 |-  ( ( y e. ~P NN /\ k e. ( ZZ>= ` 1 ) ) -> ( ( F ` NN ) ` k ) e. CC )
40 1 rpnnen2lem3 
 |-  seq 1 ( + , ( F ` NN ) ) ~~> ( 1 / 2 )
41 40 a1i 
 |-  ( y e. ~P NN -> seq 1 ( + , ( F ` NN ) ) ~~> ( 1 / 2 ) )
42 31 11 32 39 41 isumclim 
 |-  ( y e. ~P NN -> sum_ k e. ( ZZ>= ` 1 ) ( ( F ` NN ) ` k ) = ( 1 / 2 ) )
43 30 42 breqtrd 
 |-  ( y e. ~P NN -> sum_ k e. ( ZZ>= ` 1 ) ( ( F ` y ) ` k ) <_ ( 1 / 2 ) )
44 5 43 eqbrtrid 
 |-  ( y e. ~P NN -> sum_ k e. NN ( ( F ` y ) ` k ) <_ ( 1 / 2 ) )
45 halflt1 
 |-  ( 1 / 2 ) < 1
46 24 26 45 ltleii 
 |-  ( 1 / 2 ) <_ 1
47 46 a1i 
 |-  ( y e. ~P NN -> ( 1 / 2 ) <_ 1 )
48 10 25 27 44 47 letrd 
 |-  ( y e. ~P NN -> sum_ k e. NN ( ( F ` y ) ` k ) <_ 1 )
49 elicc01 
 |-  ( 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 ) )
50 10 23 48 49 syl3anbrc 
 |-  ( y e. ~P NN -> sum_ k e. NN ( ( F ` y ) ` k ) e. ( 0 [,] 1 ) )
51 elpwi 
 |-  ( z e. ~P NN -> z C_ NN )
52 ssdifss 
 |-  ( y C_ NN -> ( y \ z ) C_ NN )
53 ssdifss 
 |-  ( z C_ NN -> ( z \ y ) C_ NN )
54 unss 
 |-  ( ( ( y \ z ) C_ NN /\ ( z \ y ) C_ NN ) <-> ( ( y \ z ) u. ( z \ y ) ) C_ NN )
55 54 biimpi 
 |-  ( ( ( y \ z ) C_ NN /\ ( z \ y ) C_ NN ) -> ( ( y \ z ) u. ( z \ y ) ) C_ NN )
56 52 53 55 syl2an 
 |-  ( ( y C_ NN /\ z C_ NN ) -> ( ( y \ z ) u. ( z \ y ) ) C_ NN )
57 3 51 56 syl2an 
 |-  ( ( y e. ~P NN /\ z e. ~P NN ) -> ( ( y \ z ) u. ( z \ y ) ) C_ NN )
58 eqss 
 |-  ( y = z <-> ( y C_ z /\ z C_ y ) )
59 ssdif0 
 |-  ( y C_ z <-> ( y \ z ) = (/) )
60 ssdif0 
 |-  ( z C_ y <-> ( z \ y ) = (/) )
61 59 60 anbi12i 
 |-  ( ( y C_ z /\ z C_ y ) <-> ( ( y \ z ) = (/) /\ ( z \ y ) = (/) ) )
62 un00 
 |-  ( ( ( y \ z ) = (/) /\ ( z \ y ) = (/) ) <-> ( ( y \ z ) u. ( z \ y ) ) = (/) )
63 58 61 62 3bitri 
 |-  ( y = z <-> ( ( y \ z ) u. ( z \ y ) ) = (/) )
64 63 necon3bii 
 |-  ( y =/= z <-> ( ( y \ z ) u. ( z \ y ) ) =/= (/) )
65 64 biimpi 
 |-  ( y =/= z -> ( ( y \ z ) u. ( z \ y ) ) =/= (/) )
66 nnwo 
 |-  ( ( ( ( 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 )
67 57 65 66 syl2an 
 |-  ( ( ( 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 )
68 67 ex 
 |-  ( ( 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 ) )
69 57 sselda 
 |-  ( ( ( y e. ~P NN /\ z e. ~P NN ) /\ m e. ( ( y \ z ) u. ( z \ y ) ) ) -> m e. NN )
70 df-ral 
 |-  ( A. n e. ( ( y \ z ) u. ( z \ y ) ) m <_ n <-> A. n ( n e. ( ( y \ z ) u. ( z \ y ) ) -> m <_ n ) )
71 con34b 
 |-  ( ( n e. ( ( y \ z ) u. ( z \ y ) ) -> m <_ n ) <-> ( -. m <_ n -> -. n e. ( ( y \ z ) u. ( z \ y ) ) ) )
72 eldif 
 |-  ( n e. ( y \ z ) <-> ( n e. y /\ -. n e. z ) )
73 eldif 
 |-  ( n e. ( z \ y ) <-> ( n e. z /\ -. n e. y ) )
74 72 73 orbi12i 
 |-  ( ( n e. ( y \ z ) \/ n e. ( z \ y ) ) <-> ( ( n e. y /\ -. n e. z ) \/ ( n e. z /\ -. n e. y ) ) )
75 elun 
 |-  ( n e. ( ( y \ z ) u. ( z \ y ) ) <-> ( n e. ( y \ z ) \/ n e. ( z \ y ) ) )
76 xor 
 |-  ( -. ( n e. y <-> n e. z ) <-> ( ( n e. y /\ -. n e. z ) \/ ( n e. z /\ -. n e. y ) ) )
77 74 75 76 3bitr4ri 
 |-  ( -. ( n e. y <-> n e. z ) <-> n e. ( ( y \ z ) u. ( z \ y ) ) )
78 77 con1bii 
 |-  ( -. n e. ( ( y \ z ) u. ( z \ y ) ) <-> ( n e. y <-> n e. z ) )
79 78 imbi2i 
 |-  ( ( -. m <_ n -> -. n e. ( ( y \ z ) u. ( z \ y ) ) ) <-> ( -. m <_ n -> ( n e. y <-> n e. z ) ) )
80 71 79 bitri 
 |-  ( ( n e. ( ( y \ z ) u. ( z \ y ) ) -> m <_ n ) <-> ( -. m <_ n -> ( n e. y <-> n e. z ) ) )
81 80 albii 
 |-  ( A. n ( n e. ( ( y \ z ) u. ( z \ y ) ) -> m <_ n ) <-> A. n ( -. m <_ n -> ( n e. y <-> n e. z ) ) )
82 70 81 bitri 
 |-  ( A. n e. ( ( y \ z ) u. ( z \ y ) ) m <_ n <-> A. n ( -. m <_ n -> ( n e. y <-> n e. z ) ) )
83 alral 
 |-  ( A. n ( -. m <_ n -> ( n e. y <-> n e. z ) ) -> A. n e. NN ( -. m <_ n -> ( n e. y <-> n e. z ) ) )
84 nnre 
 |-  ( n e. NN -> n e. RR )
85 nnre 
 |-  ( m e. NN -> m e. RR )
86 ltnle 
 |-  ( ( n e. RR /\ m e. RR ) -> ( n < m <-> -. m <_ n ) )
87 84 85 86 syl2anr 
 |-  ( ( m e. NN /\ n e. NN ) -> ( n < m <-> -. m <_ n ) )
88 87 imbi1d 
 |-  ( ( m e. NN /\ n e. NN ) -> ( ( n < m -> ( n e. y <-> n e. z ) ) <-> ( -. m <_ n -> ( n e. y <-> n e. z ) ) ) )
89 88 ralbidva 
 |-  ( 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 ) ) ) )
90 83 89 imbitrrid 
 |-  ( 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 ) ) ) )
91 82 90 biimtrid 
 |-  ( 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 ) ) ) )
92 69 91 syl 
 |-  ( ( ( 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 ) ) ) )
93 92 reximdva 
 |-  ( ( 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 ) ) ) )
94 68 93 syld 
 |-  ( ( 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 ) ) ) )
95 rexun 
 |-  ( 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 ) ) ) )
96 94 95 imbitrdi 
 |-  ( ( 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 ) ) ) ) )
97 simpll 
 |-  ( ( ( 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 )
98 simplr 
 |-  ( ( ( 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 )
99 simprl 
 |-  ( ( ( 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 ) )
100 simprr 
 |-  ( ( ( 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 ) ) )
101 biid 
 |-  ( 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 ) )
102 1 97 98 99 100 101 rpnnen2lem11 
 |-  ( ( ( 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 ) )
103 102 rexlimdvaa 
 |-  ( ( 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 ) ) )
104 simplr 
 |-  ( ( ( 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 )
105 simpll 
 |-  ( ( ( 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 )
106 simprl 
 |-  ( ( ( 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 ) )
107 simprr 
 |-  ( ( ( 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 ) ) )
108 bicom 
 |-  ( ( n e. z <-> n e. y ) <-> ( n e. y <-> n e. z ) )
109 108 imbi2i 
 |-  ( ( n < m -> ( n e. z <-> n e. y ) ) <-> ( n < m -> ( n e. y <-> n e. z ) ) )
110 109 ralbii 
 |-  ( A. n e. NN ( n < m -> ( n e. z <-> n e. y ) ) <-> A. n e. NN ( n < m -> ( n e. y <-> n e. z ) ) )
111 107 110 sylibr 
 |-  ( ( ( 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 ) ) )
112 eqcom 
 |-  ( 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 ) )
113 1 104 105 106 111 112 rpnnen2lem11 
 |-  ( ( ( 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 ) )
114 113 rexlimdvaa 
 |-  ( ( 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 ) ) )
115 103 114 jaod 
 |-  ( ( 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 ) ) )
116 3 51 115 syl2an 
 |-  ( ( 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 ) ) )
117 96 116 syld 
 |-  ( ( y e. ~P NN /\ z e. ~P NN ) -> ( y =/= z -> -. sum_ k e. NN ( ( F ` y ) ` k ) = sum_ k e. NN ( ( F ` z ) ` k ) ) )
118 117 necon4ad 
 |-  ( ( y e. ~P NN /\ z e. ~P NN ) -> ( sum_ k e. NN ( ( F ` y ) ` k ) = sum_ k e. NN ( ( F ` z ) ` k ) -> y = z ) )
119 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
120 119 fveq1d 
 |-  ( y = z -> ( ( F ` y ) ` k ) = ( ( F ` z ) ` k ) )
121 120 sumeq2sdv 
 |-  ( y = z -> sum_ k e. NN ( ( F ` y ) ` k ) = sum_ k e. NN ( ( F ` z ) ` k ) )
122 118 121 impbid1 
 |-  ( ( y e. ~P NN /\ z e. ~P NN ) -> ( sum_ k e. NN ( ( F ` y ) ` k ) = sum_ k e. NN ( ( F ` z ) ` k ) <-> y = z ) )
123 50 122 dom2 
 |-  ( ( 0 [,] 1 ) e. _V -> ~P NN ~<_ ( 0 [,] 1 ) )
124 2 123 ax-mp 
 |-  ~P NN ~<_ ( 0 [,] 1 )