Metamath Proof Explorer

Theorem rpnnen2lem11

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

Ref Expression
Hypotheses rpnnen2.1 
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
rpnnen2.2 
|- ( ph -> A C_ NN )
rpnnen2.3 
|- ( ph -> B C_ NN )
rpnnen2.4 
|- ( ph -> m e. ( A \ B ) )
rpnnen2.5 
|- ( ph -> A. n e. NN ( n < m -> ( n e. A <-> n e. B ) ) )
rpnnen2.6 
|- ( ps <-> sum_ k e. NN ( ( F ` A ) ` k ) = sum_ k e. NN ( ( F ` B ) ` k ) )
Assertion rpnnen2lem11 
|- ( ph -> -. ps )

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 rpnnen2.2 
 |-  ( ph -> A C_ NN )
3 rpnnen2.3 
 |-  ( ph -> B C_ NN )
4 rpnnen2.4 
 |-  ( ph -> m e. ( A \ B ) )
5 rpnnen2.5 
 |-  ( ph -> A. n e. NN ( n < m -> ( n e. A <-> n e. B ) ) )
6 rpnnen2.6 
 |-  ( ps <-> sum_ k e. NN ( ( F ` A ) ` k ) = sum_ k e. NN ( ( F ` B ) ` k ) )
7 eldifi 
 |-  ( m e. ( A \ B ) -> m e. A )
8 ssel2 
 |-  ( ( A C_ NN /\ m e. A ) -> m e. NN )
9 7 8 sylan2 
 |-  ( ( A C_ NN /\ m e. ( A \ B ) ) -> m e. NN )
10 2 4 9 syl2anc 
 |-  ( ph -> m e. NN )
11 1 rpnnen2lem6 
 |-  ( ( B C_ NN /\ m e. NN ) -> sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) e. RR )
12 3 10 11 syl2anc 
 |-  ( ph -> sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) e. RR )
13 3nn 
 |-  3 e. NN
14 nnrecre 
 |-  ( 3 e. NN -> ( 1 / 3 ) e. RR )
15 13 14 ax-mp 
 |-  ( 1 / 3 ) e. RR
16 10 nnnn0d 
 |-  ( ph -> m e. NN0 )
17 reexpcl 
 |-  ( ( ( 1 / 3 ) e. RR /\ m e. NN0 ) -> ( ( 1 / 3 ) ^ m ) e. RR )
18 15 16 17 sylancr 
 |-  ( ph -> ( ( 1 / 3 ) ^ m ) e. RR )
19 1 rpnnen2lem6 
 |-  ( ( A C_ NN /\ m e. NN ) -> sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) e. RR )
20 2 10 19 syl2anc 
 |-  ( ph -> sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) e. RR )
21 nnrp 
 |-  ( 3 e. NN -> 3 e. RR+ )
22 rpreccl 
 |-  ( 3 e. RR+ -> ( 1 / 3 ) e. RR+ )
23 13 21 22 mp2b 
 |-  ( 1 / 3 ) e. RR+
24 10 nnzd 
 |-  ( ph -> m e. ZZ )
25 rpexpcl 
 |-  ( ( ( 1 / 3 ) e. RR+ /\ m e. ZZ ) -> ( ( 1 / 3 ) ^ m ) e. RR+ )
26 23 24 25 sylancr 
 |-  ( ph -> ( ( 1 / 3 ) ^ m ) e. RR+ )
27 26 rpred 
 |-  ( ph -> ( ( 1 / 3 ) ^ m ) e. RR )
28 27 rehalfcld 
 |-  ( ph -> ( ( ( 1 / 3 ) ^ m ) / 2 ) e. RR )
29 4 snssd 
 |-  ( ph -> { m } C_ ( A \ B ) )
30 2 ssdifd 
 |-  ( ph -> ( A \ B ) C_ ( NN \ B ) )
31 29 30 sstrd 
 |-  ( ph -> { m } C_ ( NN \ B ) )
32 10 snssd 
 |-  ( ph -> { m } C_ NN )
33 ssconb 
 |-  ( ( B C_ NN /\ { m } C_ NN ) -> ( B C_ ( NN \ { m } ) <-> { m } C_ ( NN \ B ) ) )
34 3 32 33 syl2anc 
 |-  ( ph -> ( B C_ ( NN \ { m } ) <-> { m } C_ ( NN \ B ) ) )
35 31 34 mpbird 
 |-  ( ph -> B C_ ( NN \ { m } ) )
36 difssd 
 |-  ( ph -> ( NN \ { m } ) C_ NN )
37 1 rpnnen2lem7 
 |-  ( ( B C_ ( NN \ { m } ) /\ ( NN \ { m } ) C_ NN /\ m e. NN ) -> sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) <_ sum_ k e. ( ZZ>= ` m ) ( ( F ` ( NN \ { m } ) ) ` k ) )
38 35 36 10 37 syl3anc 
 |-  ( ph -> sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) <_ sum_ k e. ( ZZ>= ` m ) ( ( F ` ( NN \ { m } ) ) ` k ) )
39 1 rpnnen2lem9 
 |-  ( m e. NN -> sum_ k e. ( ZZ>= ` m ) ( ( F ` ( NN \ { m } ) ) ` k ) = ( 0 + ( ( ( 1 / 3 ) ^ ( m + 1 ) ) / ( 1 - ( 1 / 3 ) ) ) ) )
40 10 39 syl 
 |-  ( ph -> sum_ k e. ( ZZ>= ` m ) ( ( F ` ( NN \ { m } ) ) ` k ) = ( 0 + ( ( ( 1 / 3 ) ^ ( m + 1 ) ) / ( 1 - ( 1 / 3 ) ) ) ) )
41 15 recni 
 |-  ( 1 / 3 ) e. CC
42 expp1 
 |-  ( ( ( 1 / 3 ) e. CC /\ m e. NN0 ) -> ( ( 1 / 3 ) ^ ( m + 1 ) ) = ( ( ( 1 / 3 ) ^ m ) x. ( 1 / 3 ) ) )
43 41 16 42 sylancr 
 |-  ( ph -> ( ( 1 / 3 ) ^ ( m + 1 ) ) = ( ( ( 1 / 3 ) ^ m ) x. ( 1 / 3 ) ) )
44 27 recnd 
 |-  ( ph -> ( ( 1 / 3 ) ^ m ) e. CC )
45 3cn 
 |-  3 e. CC
46 3ne0 
 |-  3 =/= 0
47 divrec 
 |-  ( ( ( ( 1 / 3 ) ^ m ) e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( ( ( 1 / 3 ) ^ m ) / 3 ) = ( ( ( 1 / 3 ) ^ m ) x. ( 1 / 3 ) ) )
48 45 46 47 mp3an23 
 |-  ( ( ( 1 / 3 ) ^ m ) e. CC -> ( ( ( 1 / 3 ) ^ m ) / 3 ) = ( ( ( 1 / 3 ) ^ m ) x. ( 1 / 3 ) ) )
49 44 48 syl 
 |-  ( ph -> ( ( ( 1 / 3 ) ^ m ) / 3 ) = ( ( ( 1 / 3 ) ^ m ) x. ( 1 / 3 ) ) )
50 43 49 eqtr4d 
 |-  ( ph -> ( ( 1 / 3 ) ^ ( m + 1 ) ) = ( ( ( 1 / 3 ) ^ m ) / 3 ) )
51 50 oveq1d 
 |-  ( ph -> ( ( ( 1 / 3 ) ^ ( m + 1 ) ) / ( 1 - ( 1 / 3 ) ) ) = ( ( ( ( 1 / 3 ) ^ m ) / 3 ) / ( 1 - ( 1 / 3 ) ) ) )
52 ax-1cn 
 |-  1 e. CC
53 45 46 pm3.2i 
 |-  ( 3 e. CC /\ 3 =/= 0 )
54 divsubdir 
 |-  ( ( 3 e. CC /\ 1 e. CC /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( 3 - 1 ) / 3 ) = ( ( 3 / 3 ) - ( 1 / 3 ) ) )
55 45 52 53 54 mp3an 
 |-  ( ( 3 - 1 ) / 3 ) = ( ( 3 / 3 ) - ( 1 / 3 ) )
56 3m1e2 
 |-  ( 3 - 1 ) = 2
57 56 oveq1i 
 |-  ( ( 3 - 1 ) / 3 ) = ( 2 / 3 )
58 45 46 dividi 
 |-  ( 3 / 3 ) = 1
59 58 oveq1i 
 |-  ( ( 3 / 3 ) - ( 1 / 3 ) ) = ( 1 - ( 1 / 3 ) )
60 55 57 59 3eqtr3ri 
 |-  ( 1 - ( 1 / 3 ) ) = ( 2 / 3 )
61 60 oveq2i 
 |-  ( ( ( ( 1 / 3 ) ^ m ) / 3 ) / ( 1 - ( 1 / 3 ) ) ) = ( ( ( ( 1 / 3 ) ^ m ) / 3 ) / ( 2 / 3 ) )
62 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
63 divcan7 
 |-  ( ( ( ( 1 / 3 ) ^ m ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( ( ( 1 / 3 ) ^ m ) / 3 ) / ( 2 / 3 ) ) = ( ( ( 1 / 3 ) ^ m ) / 2 ) )
64 62 53 63 mp3an23 
 |-  ( ( ( 1 / 3 ) ^ m ) e. CC -> ( ( ( ( 1 / 3 ) ^ m ) / 3 ) / ( 2 / 3 ) ) = ( ( ( 1 / 3 ) ^ m ) / 2 ) )
65 44 64 syl 
 |-  ( ph -> ( ( ( ( 1 / 3 ) ^ m ) / 3 ) / ( 2 / 3 ) ) = ( ( ( 1 / 3 ) ^ m ) / 2 ) )
66 61 65 syl5eq 
 |-  ( ph -> ( ( ( ( 1 / 3 ) ^ m ) / 3 ) / ( 1 - ( 1 / 3 ) ) ) = ( ( ( 1 / 3 ) ^ m ) / 2 ) )
67 51 66 eqtrd 
 |-  ( ph -> ( ( ( 1 / 3 ) ^ ( m + 1 ) ) / ( 1 - ( 1 / 3 ) ) ) = ( ( ( 1 / 3 ) ^ m ) / 2 ) )
68 67 oveq2d 
 |-  ( ph -> ( 0 + ( ( ( 1 / 3 ) ^ ( m + 1 ) ) / ( 1 - ( 1 / 3 ) ) ) ) = ( 0 + ( ( ( 1 / 3 ) ^ m ) / 2 ) ) )
69 28 recnd 
 |-  ( ph -> ( ( ( 1 / 3 ) ^ m ) / 2 ) e. CC )
70 69 addid2d 
 |-  ( ph -> ( 0 + ( ( ( 1 / 3 ) ^ m ) / 2 ) ) = ( ( ( 1 / 3 ) ^ m ) / 2 ) )
71 40 68 70 3eqtrd 
 |-  ( ph -> sum_ k e. ( ZZ>= ` m ) ( ( F ` ( NN \ { m } ) ) ` k ) = ( ( ( 1 / 3 ) ^ m ) / 2 ) )
72 38 71 breqtrd 
 |-  ( ph -> sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) <_ ( ( ( 1 / 3 ) ^ m ) / 2 ) )
73 rphalflt 
 |-  ( ( ( 1 / 3 ) ^ m ) e. RR+ -> ( ( ( 1 / 3 ) ^ m ) / 2 ) < ( ( 1 / 3 ) ^ m ) )
74 26 73 syl 
 |-  ( ph -> ( ( ( 1 / 3 ) ^ m ) / 2 ) < ( ( 1 / 3 ) ^ m ) )
75 12 28 27 72 74 lelttrd 
 |-  ( ph -> sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) < ( ( 1 / 3 ) ^ m ) )
76 eluznn 
 |-  ( ( m e. NN /\ k e. ( ZZ>= ` m ) ) -> k e. NN )
77 10 76 sylan 
 |-  ( ( ph /\ k e. ( ZZ>= ` m ) ) -> k e. NN )
78 1 rpnnen2lem1 
 |-  ( ( { m } C_ NN /\ k e. NN ) -> ( ( F ` { m } ) ` k ) = if ( k e. { m } , ( ( 1 / 3 ) ^ k ) , 0 ) )
79 32 77 78 syl2an2r 
 |-  ( ( ph /\ k e. ( ZZ>= ` m ) ) -> ( ( F ` { m } ) ` k ) = if ( k e. { m } , ( ( 1 / 3 ) ^ k ) , 0 ) )
80 79 sumeq2dv 
 |-  ( ph -> sum_ k e. ( ZZ>= ` m ) ( ( F ` { m } ) ` k ) = sum_ k e. ( ZZ>= ` m ) if ( k e. { m } , ( ( 1 / 3 ) ^ k ) , 0 ) )
81 uzid 
 |-  ( m e. ZZ -> m e. ( ZZ>= ` m ) )
82 24 81 syl 
 |-  ( ph -> m e. ( ZZ>= ` m ) )
83 82 snssd 
 |-  ( ph -> { m } C_ ( ZZ>= ` m ) )
84 vex 
 |-  m e. _V
85 oveq2 
 |-  ( k = m -> ( ( 1 / 3 ) ^ k ) = ( ( 1 / 3 ) ^ m ) )
86 85 eleq1d 
 |-  ( k = m -> ( ( ( 1 / 3 ) ^ k ) e. CC <-> ( ( 1 / 3 ) ^ m ) e. CC ) )
87 84 86 ralsn 
 |-  ( A. k e. { m } ( ( 1 / 3 ) ^ k ) e. CC <-> ( ( 1 / 3 ) ^ m ) e. CC )
88 44 87 sylibr 
 |-  ( ph -> A. k e. { m } ( ( 1 / 3 ) ^ k ) e. CC )
89 ssidd 
 |-  ( ph -> ( ZZ>= ` m ) C_ ( ZZ>= ` m ) )
90 89 orcd 
 |-  ( ph -> ( ( ZZ>= ` m ) C_ ( ZZ>= ` m ) \/ ( ZZ>= ` m ) e. Fin ) )
91 sumss2 
 |-  ( ( ( { m } C_ ( ZZ>= ` m ) /\ A. k e. { m } ( ( 1 / 3 ) ^ k ) e. CC ) /\ ( ( ZZ>= ` m ) C_ ( ZZ>= ` m ) \/ ( ZZ>= ` m ) e. Fin ) ) -> sum_ k e. { m } ( ( 1 / 3 ) ^ k ) = sum_ k e. ( ZZ>= ` m ) if ( k e. { m } , ( ( 1 / 3 ) ^ k ) , 0 ) )
92 83 88 90 91 syl21anc 
 |-  ( ph -> sum_ k e. { m } ( ( 1 / 3 ) ^ k ) = sum_ k e. ( ZZ>= ` m ) if ( k e. { m } , ( ( 1 / 3 ) ^ k ) , 0 ) )
93 85 sumsn 
 |-  ( ( m e. NN /\ ( ( 1 / 3 ) ^ m ) e. CC ) -> sum_ k e. { m } ( ( 1 / 3 ) ^ k ) = ( ( 1 / 3 ) ^ m ) )
94 10 44 93 syl2anc 
 |-  ( ph -> sum_ k e. { m } ( ( 1 / 3 ) ^ k ) = ( ( 1 / 3 ) ^ m ) )
95 80 92 94 3eqtr2d 
 |-  ( ph -> sum_ k e. ( ZZ>= ` m ) ( ( F ` { m } ) ` k ) = ( ( 1 / 3 ) ^ m ) )
96 4 7 syl 
 |-  ( ph -> m e. A )
97 96 snssd 
 |-  ( ph -> { m } C_ A )
98 1 rpnnen2lem7 
 |-  ( ( { m } C_ A /\ A C_ NN /\ m e. NN ) -> sum_ k e. ( ZZ>= ` m ) ( ( F ` { m } ) ` k ) <_ sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) )
99 97 2 10 98 syl3anc 
 |-  ( ph -> sum_ k e. ( ZZ>= ` m ) ( ( F ` { m } ) ` k ) <_ sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) )
100 95 99 eqbrtrrd 
 |-  ( ph -> ( ( 1 / 3 ) ^ m ) <_ sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) )
101 12 18 20 75 100 ltletrd 
 |-  ( ph -> sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) < sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) )
102 12 101 gtned 
 |-  ( ph -> sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) =/= sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) )
103 1 2 3 4 5 6 rpnnen2lem10 
 |-  ( ( ph /\ ps ) -> sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) = sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) )
104 103 ex 
 |-  ( ph -> ( ps -> sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) = sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) ) )
105 104 necon3ad 
 |-  ( ph -> ( sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) =/= sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) -> -. ps ) )
106 102 105 mpd 
 |-  ( ph -> -. ps )