Metamath Proof Explorer

Theorem mbfi1fseqlem1

Description: Lemma for mbfi1fseq . (Contributed by Mario Carneiro, 16-Aug-2014)

Ref Expression
Hypotheses mbfi1fseq.1 
|- ( ph -> F e. MblFn )
mbfi1fseq.2 
|- ( ph -> F : RR --> ( 0 [,) +oo ) )
mbfi1fseq.3 
|- J = ( m e. NN , y e. RR |-> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) )
Assertion mbfi1fseqlem1 
|- ( ph -> J : ( NN X. RR ) --> ( 0 [,) +oo ) )

Proof

Step Hyp Ref Expression
1 mbfi1fseq.1 
 |-  ( ph -> F e. MblFn )
2 mbfi1fseq.2 
 |-  ( ph -> F : RR --> ( 0 [,) +oo ) )
3 mbfi1fseq.3 
 |-  J = ( m e. NN , y e. RR |-> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) )
4 simpr 
 |-  ( ( m e. NN /\ y e. RR ) -> y e. RR )
5 ffvelrn 
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ y e. RR ) -> ( F ` y ) e. ( 0 [,) +oo ) )
6 2 4 5 syl2an 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( F ` y ) e. ( 0 [,) +oo ) )
7 elrege0 
 |-  ( ( F ` y ) e. ( 0 [,) +oo ) <-> ( ( F ` y ) e. RR /\ 0 <_ ( F ` y ) ) )
8 6 7 sylib 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( ( F ` y ) e. RR /\ 0 <_ ( F ` y ) ) )
9 8 simpld 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( F ` y ) e. RR )
10 2nn 
 |-  2 e. NN
11 nnnn0 
 |-  ( m e. NN -> m e. NN0 )
12 nnexpcl 
 |-  ( ( 2 e. NN /\ m e. NN0 ) -> ( 2 ^ m ) e. NN )
13 10 11 12 sylancr 
 |-  ( m e. NN -> ( 2 ^ m ) e. NN )
14 13 ad2antrl 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( 2 ^ m ) e. NN )
15 14 nnred 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( 2 ^ m ) e. RR )
16 9 15 remulcld 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( ( F ` y ) x. ( 2 ^ m ) ) e. RR )
17 reflcl 
 |-  ( ( ( F ` y ) x. ( 2 ^ m ) ) e. RR -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) e. RR )
18 16 17 syl 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) e. RR )
19 18 14 nndivred 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. RR )
20 14 nnnn0d 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( 2 ^ m ) e. NN0 )
21 20 nn0ge0d 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> 0 <_ ( 2 ^ m ) )
22 mulge0 
 |-  ( ( ( ( F ` y ) e. RR /\ 0 <_ ( F ` y ) ) /\ ( ( 2 ^ m ) e. RR /\ 0 <_ ( 2 ^ m ) ) ) -> 0 <_ ( ( F ` y ) x. ( 2 ^ m ) ) )
23 8 15 21 22 syl12anc 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> 0 <_ ( ( F ` y ) x. ( 2 ^ m ) ) )
24 flge0nn0 
 |-  ( ( ( ( F ` y ) x. ( 2 ^ m ) ) e. RR /\ 0 <_ ( ( F ` y ) x. ( 2 ^ m ) ) ) -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) e. NN0 )
25 16 23 24 syl2anc 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) e. NN0 )
26 25 nn0ge0d 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> 0 <_ ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) )
27 14 nngt0d 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> 0 < ( 2 ^ m ) )
28 divge0 
 |-  ( ( ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) e. RR /\ 0 <_ ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) ) /\ ( ( 2 ^ m ) e. RR /\ 0 < ( 2 ^ m ) ) ) -> 0 <_ ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) )
29 18 26 15 27 28 syl22anc 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> 0 <_ ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) )
30 elrege0 
 |-  ( ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. ( 0 [,) +oo ) <-> ( ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. RR /\ 0 <_ ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) ) )
31 19 29 30 sylanbrc 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. ( 0 [,) +oo ) )
32 31 ralrimivva 
 |-  ( ph -> A. m e. NN A. y e. RR ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. ( 0 [,) +oo ) )
33 3 fmpo 
 |-  ( A. m e. NN A. y e. RR ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. ( 0 [,) +oo ) <-> J : ( NN X. RR ) --> ( 0 [,) +oo ) )
34 32 33 sylib 
 |-  ( ph -> J : ( NN X. RR ) --> ( 0 [,) +oo ) )