Metamath Proof Explorer

Theorem rpnnen2lem7

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

Ref Expression
Hypothesis rpnnen2.1 
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
Assertion rpnnen2lem7 
|- ( ( A C_ B /\ B C_ NN /\ M e. NN ) -> sum_ k e. ( ZZ>= ` M ) ( ( F ` A ) ` k ) <_ sum_ k e. ( ZZ>= ` M ) ( ( F ` B ) ` k ) )

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 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
3 simp3 
 |-  ( ( A C_ B /\ B C_ NN /\ M e. NN ) -> M e. NN )
4 3 nnzd 
 |-  ( ( A C_ B /\ B C_ NN /\ M e. NN ) -> M e. ZZ )
5 eqidd 
 |-  ( ( ( A C_ B /\ B C_ NN /\ M e. NN ) /\ k e. ( ZZ>= ` M ) ) -> ( ( F ` A ) ` k ) = ( ( F ` A ) ` k ) )
6 eluznn 
 |-  ( ( M e. NN /\ k e. ( ZZ>= ` M ) ) -> k e. NN )
7 3 6 sylan 
 |-  ( ( ( A C_ B /\ B C_ NN /\ M e. NN ) /\ k e. ( ZZ>= ` M ) ) -> k e. NN )
8 sstr 
 |-  ( ( A C_ B /\ B C_ NN ) -> A C_ NN )
9 8 3adant3 
 |-  ( ( A C_ B /\ B C_ NN /\ M e. NN ) -> A C_ NN )
10 1 rpnnen2lem2 
 |-  ( A C_ NN -> ( F ` A ) : NN --> RR )
11 9 10 syl 
 |-  ( ( A C_ B /\ B C_ NN /\ M e. NN ) -> ( F ` A ) : NN --> RR )
12 11 ffvelrnda 
 |-  ( ( ( A C_ B /\ B C_ NN /\ M e. NN ) /\ k e. NN ) -> ( ( F ` A ) ` k ) e. RR )
13 7 12 syldan 
 |-  ( ( ( A C_ B /\ B C_ NN /\ M e. NN ) /\ k e. ( ZZ>= ` M ) ) -> ( ( F ` A ) ` k ) e. RR )
14 eqidd 
 |-  ( ( ( A C_ B /\ B C_ NN /\ M e. NN ) /\ k e. ( ZZ>= ` M ) ) -> ( ( F ` B ) ` k ) = ( ( F ` B ) ` k ) )
15 1 rpnnen2lem2 
 |-  ( B C_ NN -> ( F ` B ) : NN --> RR )
16 15 3ad2ant2 
 |-  ( ( A C_ B /\ B C_ NN /\ M e. NN ) -> ( F ` B ) : NN --> RR )
17 16 ffvelrnda 
 |-  ( ( ( A C_ B /\ B C_ NN /\ M e. NN ) /\ k e. NN ) -> ( ( F ` B ) ` k ) e. RR )
18 7 17 syldan 
 |-  ( ( ( A C_ B /\ B C_ NN /\ M e. NN ) /\ k e. ( ZZ>= ` M ) ) -> ( ( F ` B ) ` k ) e. RR )
19 1 rpnnen2lem4 
 |-  ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> ( 0 <_ ( ( F ` A ) ` k ) /\ ( ( F ` A ) ` k ) <_ ( ( F ` B ) ` k ) ) )
20 19 simprd 
 |-  ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> ( ( F ` A ) ` k ) <_ ( ( F ` B ) ` k ) )
21 20 3expa 
 |-  ( ( ( A C_ B /\ B C_ NN ) /\ k e. NN ) -> ( ( F ` A ) ` k ) <_ ( ( F ` B ) ` k ) )
22 21 3adantl3 
 |-  ( ( ( A C_ B /\ B C_ NN /\ M e. NN ) /\ k e. NN ) -> ( ( F ` A ) ` k ) <_ ( ( F ` B ) ` k ) )
23 7 22 syldan 
 |-  ( ( ( A C_ B /\ B C_ NN /\ M e. NN ) /\ k e. ( ZZ>= ` M ) ) -> ( ( F ` A ) ` k ) <_ ( ( F ` B ) ` k ) )
24 1 rpnnen2lem5 
 |-  ( ( A C_ NN /\ M e. NN ) -> seq M ( + , ( F ` A ) ) e. dom ~~> )
25 8 24 stoic3 
 |-  ( ( A C_ B /\ B C_ NN /\ M e. NN ) -> seq M ( + , ( F ` A ) ) e. dom ~~> )
26 1 rpnnen2lem5 
 |-  ( ( B C_ NN /\ M e. NN ) -> seq M ( + , ( F ` B ) ) e. dom ~~> )
27 26 3adant1 
 |-  ( ( A C_ B /\ B C_ NN /\ M e. NN ) -> seq M ( + , ( F ` B ) ) e. dom ~~> )
28 2 4 5 13 14 18 23 25 27 isumle 
 |-  ( ( A C_ B /\ B C_ NN /\ M e. NN ) -> sum_ k e. ( ZZ>= ` M ) ( ( F ` A ) ` k ) <_ sum_ k e. ( ZZ>= ` M ) ( ( F ` B ) ` k ) )