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 ) )