Metamath Proof Explorer

Theorem rpnnen2lem4

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

Ref Expression
Hypothesis rpnnen2.1 
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
Assertion rpnnen2lem4 
|- ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> ( 0 <_ ( ( F ` A ) ` k ) /\ ( ( F ` A ) ` k ) <_ ( ( 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 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
3 0re 
 |-  0 e. RR
4 1re 
 |-  1 e. RR
5 3nn 
 |-  3 e. NN
6 nndivre 
 |-  ( ( 1 e. RR /\ 3 e. NN ) -> ( 1 / 3 ) e. RR )
7 4 5 6 mp2an 
 |-  ( 1 / 3 ) e. RR
8 3re 
 |-  3 e. RR
9 3pos 
 |-  0 < 3
10 8 9 recgt0ii 
 |-  0 < ( 1 / 3 )
11 3 7 10 ltleii 
 |-  0 <_ ( 1 / 3 )
12 expge0 
 |-  ( ( ( 1 / 3 ) e. RR /\ k e. NN0 /\ 0 <_ ( 1 / 3 ) ) -> 0 <_ ( ( 1 / 3 ) ^ k ) )
13 7 12 mp3an1 
 |-  ( ( k e. NN0 /\ 0 <_ ( 1 / 3 ) ) -> 0 <_ ( ( 1 / 3 ) ^ k ) )
14 2 11 13 sylancl 
 |-  ( k e. NN -> 0 <_ ( ( 1 / 3 ) ^ k ) )
15 14 3ad2ant3 
 |-  ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> 0 <_ ( ( 1 / 3 ) ^ k ) )
16 0le0 
 |-  0 <_ 0
17 breq2 
 |-  ( ( ( 1 / 3 ) ^ k ) = if ( k e. A , ( ( 1 / 3 ) ^ k ) , 0 ) -> ( 0 <_ ( ( 1 / 3 ) ^ k ) <-> 0 <_ if ( k e. A , ( ( 1 / 3 ) ^ k ) , 0 ) ) )
18 breq2 
 |-  ( 0 = if ( k e. A , ( ( 1 / 3 ) ^ k ) , 0 ) -> ( 0 <_ 0 <-> 0 <_ if ( k e. A , ( ( 1 / 3 ) ^ k ) , 0 ) ) )
19 17 18 ifboth 
 |-  ( ( 0 <_ ( ( 1 / 3 ) ^ k ) /\ 0 <_ 0 ) -> 0 <_ if ( k e. A , ( ( 1 / 3 ) ^ k ) , 0 ) )
20 15 16 19 sylancl 
 |-  ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> 0 <_ if ( k e. A , ( ( 1 / 3 ) ^ k ) , 0 ) )
21 sstr 
 |-  ( ( A C_ B /\ B C_ NN ) -> A C_ NN )
22 1 rpnnen2lem1 
 |-  ( ( A C_ NN /\ k e. NN ) -> ( ( F ` A ) ` k ) = if ( k e. A , ( ( 1 / 3 ) ^ k ) , 0 ) )
23 21 22 stoic3 
 |-  ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> ( ( F ` A ) ` k ) = if ( k e. A , ( ( 1 / 3 ) ^ k ) , 0 ) )
24 20 23 breqtrrd 
 |-  ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> 0 <_ ( ( F ` A ) ` k ) )
25 reexpcl 
 |-  ( ( ( 1 / 3 ) e. RR /\ k e. NN0 ) -> ( ( 1 / 3 ) ^ k ) e. RR )
26 7 2 25 sylancr 
 |-  ( k e. NN -> ( ( 1 / 3 ) ^ k ) e. RR )
27 26 3ad2ant3 
 |-  ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> ( ( 1 / 3 ) ^ k ) e. RR )
28 0red 
 |-  ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> 0 e. RR )
29 simp1 
 |-  ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> A C_ B )
30 29 sseld 
 |-  ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> ( k e. A -> k e. B ) )
31 ifle 
 |-  ( ( ( ( ( 1 / 3 ) ^ k ) e. RR /\ 0 e. RR /\ 0 <_ ( ( 1 / 3 ) ^ k ) ) /\ ( k e. A -> k e. B ) ) -> if ( k e. A , ( ( 1 / 3 ) ^ k ) , 0 ) <_ if ( k e. B , ( ( 1 / 3 ) ^ k ) , 0 ) )
32 27 28 15 30 31 syl31anc 
 |-  ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> if ( k e. A , ( ( 1 / 3 ) ^ k ) , 0 ) <_ if ( k e. B , ( ( 1 / 3 ) ^ k ) , 0 ) )
33 1 rpnnen2lem1 
 |-  ( ( B C_ NN /\ k e. NN ) -> ( ( F ` B ) ` k ) = if ( k e. B , ( ( 1 / 3 ) ^ k ) , 0 ) )
34 33 3adant1 
 |-  ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> ( ( F ` B ) ` k ) = if ( k e. B , ( ( 1 / 3 ) ^ k ) , 0 ) )
35 32 23 34 3brtr4d 
 |-  ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> ( ( F ` A ) ` k ) <_ ( ( F ` B ) ` k ) )
36 24 35 jca 
 |-  ( ( A C_ B /\ B C_ NN /\ k e. NN ) -> ( 0 <_ ( ( F ` A ) ` k ) /\ ( ( F ` A ) ` k ) <_ ( ( F ` B ) ` k ) ) )