Metamath Proof Explorer

Theorem mbfi1fseqlem3

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 ) ) )
mbfi1fseq.4 
|- G = ( m e. NN |-> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) )
Assertion mbfi1fseqlem3 
|- ( ( ph /\ A e. NN ) -> ( G ` A ) : RR --> ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )

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 mbfi1fseq.4 
 |-  G = ( m e. NN |-> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) )
5 1 2 3 4 mbfi1fseqlem2 
 |-  ( A e. NN -> ( G ` A ) = ( x e. RR |-> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) )
6 5 adantl 
 |-  ( ( ph /\ A e. NN ) -> ( G ` A ) = ( x e. RR |-> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) )
7 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
8 simpr 
 |-  ( ( m e. NN /\ y e. RR ) -> y e. RR )
9 ffvelrn 
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ y e. RR ) -> ( F ` y ) e. ( 0 [,) +oo ) )
10 2 8 9 syl2an 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( F ` y ) e. ( 0 [,) +oo ) )
11 7 10 sseldi 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( F ` y ) e. RR )
12 2nn 
 |-  2 e. NN
13 nnnn0 
 |-  ( m e. NN -> m e. NN0 )
14 nnexpcl 
 |-  ( ( 2 e. NN /\ m e. NN0 ) -> ( 2 ^ m ) e. NN )
15 12 13 14 sylancr 
 |-  ( m e. NN -> ( 2 ^ m ) e. NN )
16 15 ad2antrl 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( 2 ^ m ) e. NN )
17 16 nnred 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( 2 ^ m ) e. RR )
18 11 17 remulcld 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( ( F ` y ) x. ( 2 ^ m ) ) e. RR )
19 reflcl 
 |-  ( ( ( F ` y ) x. ( 2 ^ m ) ) e. RR -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) e. RR )
20 18 19 syl 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) e. RR )
21 20 16 nndivred 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. RR )
22 21 ralrimivva 
 |-  ( ph -> A. m e. NN A. y e. RR ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. RR )
23 3 fmpo 
 |-  ( A. m e. NN A. y e. RR ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. RR <-> J : ( NN X. RR ) --> RR )
24 22 23 sylib 
 |-  ( ph -> J : ( NN X. RR ) --> RR )
25 fovrn 
 |-  ( ( J : ( NN X. RR ) --> RR /\ A e. NN /\ x e. RR ) -> ( A J x ) e. RR )
26 24 25 syl3an1 
 |-  ( ( ph /\ A e. NN /\ x e. RR ) -> ( A J x ) e. RR )
27 26 3expa 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( A J x ) e. RR )
28 nnre 
 |-  ( A e. NN -> A e. RR )
29 28 ad2antlr 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> A e. RR )
30 nnnn0 
 |-  ( A e. NN -> A e. NN0 )
31 nnexpcl 
 |-  ( ( 2 e. NN /\ A e. NN0 ) -> ( 2 ^ A ) e. NN )
32 12 30 31 sylancr 
 |-  ( A e. NN -> ( 2 ^ A ) e. NN )
33 32 ad2antlr 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 2 ^ A ) e. NN )
34 nnre 
 |-  ( ( 2 ^ A ) e. NN -> ( 2 ^ A ) e. RR )
35 nngt0 
 |-  ( ( 2 ^ A ) e. NN -> 0 < ( 2 ^ A ) )
36 34 35 jca 
 |-  ( ( 2 ^ A ) e. NN -> ( ( 2 ^ A ) e. RR /\ 0 < ( 2 ^ A ) ) )
37 33 36 syl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( 2 ^ A ) e. RR /\ 0 < ( 2 ^ A ) ) )
38 lemul1 
 |-  ( ( ( A J x ) e. RR /\ A e. RR /\ ( ( 2 ^ A ) e. RR /\ 0 < ( 2 ^ A ) ) ) -> ( ( A J x ) <_ A <-> ( ( A J x ) x. ( 2 ^ A ) ) <_ ( A x. ( 2 ^ A ) ) ) )
39 27 29 37 38 syl3anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( A J x ) <_ A <-> ( ( A J x ) x. ( 2 ^ A ) ) <_ ( A x. ( 2 ^ A ) ) ) )
40 39 biimpa 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( ( A J x ) x. ( 2 ^ A ) ) <_ ( A x. ( 2 ^ A ) ) )
41 simpr 
 |-  ( ( m = A /\ y = x ) -> y = x )
42 41 fveq2d 
 |-  ( ( m = A /\ y = x ) -> ( F ` y ) = ( F ` x ) )
43 simpl 
 |-  ( ( m = A /\ y = x ) -> m = A )
44 43 oveq2d 
 |-  ( ( m = A /\ y = x ) -> ( 2 ^ m ) = ( 2 ^ A ) )
45 42 44 oveq12d 
 |-  ( ( m = A /\ y = x ) -> ( ( F ` y ) x. ( 2 ^ m ) ) = ( ( F ` x ) x. ( 2 ^ A ) ) )
46 45 fveq2d 
 |-  ( ( m = A /\ y = x ) -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) = ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) )
47 46 44 oveq12d 
 |-  ( ( m = A /\ y = x ) -> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) )
48 ovex 
 |-  ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) e. _V
49 47 3 48 ovmpoa 
 |-  ( ( A e. NN /\ x e. RR ) -> ( A J x ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) )
50 49 ad4ant23 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( A J x ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) )
51 50 oveq1d 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( ( A J x ) x. ( 2 ^ A ) ) = ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) x. ( 2 ^ A ) ) )
52 2 adantr 
 |-  ( ( ph /\ A e. NN ) -> F : RR --> ( 0 [,) +oo ) )
53 52 ffvelrnda 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
54 elrege0 
 |-  ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
55 53 54 sylib 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
56 55 simpld 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( F ` x ) e. RR )
57 33 nnred 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 2 ^ A ) e. RR )
58 56 57 remulcld 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( F ` x ) x. ( 2 ^ A ) ) e. RR )
59 33 nnnn0d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 2 ^ A ) e. NN0 )
60 59 nn0ge0d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 <_ ( 2 ^ A ) )
61 mulge0 
 |-  ( ( ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) /\ ( ( 2 ^ A ) e. RR /\ 0 <_ ( 2 ^ A ) ) ) -> 0 <_ ( ( F ` x ) x. ( 2 ^ A ) ) )
62 55 57 60 61 syl12anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 <_ ( ( F ` x ) x. ( 2 ^ A ) ) )
63 flge0nn0 
 |-  ( ( ( ( F ` x ) x. ( 2 ^ A ) ) e. RR /\ 0 <_ ( ( F ` x ) x. ( 2 ^ A ) ) ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) e. NN0 )
64 58 62 63 syl2anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) e. NN0 )
65 64 adantr 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) e. NN0 )
66 65 nn0cnd 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) e. CC )
67 33 adantr 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( 2 ^ A ) e. NN )
68 67 nncnd 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( 2 ^ A ) e. CC )
69 67 nnne0d 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( 2 ^ A ) =/= 0 )
70 66 68 69 divcan1d 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) x. ( 2 ^ A ) ) = ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) )
71 51 70 eqtrd 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( ( A J x ) x. ( 2 ^ A ) ) = ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) )
72 71 65 eqeltrd 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( ( A J x ) x. ( 2 ^ A ) ) e. NN0 )
73 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
74 72 73 eleqtrdi 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( ( A J x ) x. ( 2 ^ A ) ) e. ( ZZ>= ` 0 ) )
75 nnmulcl 
 |-  ( ( A e. NN /\ ( 2 ^ A ) e. NN ) -> ( A x. ( 2 ^ A ) ) e. NN )
76 32 75 mpdan 
 |-  ( A e. NN -> ( A x. ( 2 ^ A ) ) e. NN )
77 76 ad2antlr 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( A x. ( 2 ^ A ) ) e. NN )
78 77 adantr 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( A x. ( 2 ^ A ) ) e. NN )
79 78 nnzd 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( A x. ( 2 ^ A ) ) e. ZZ )
80 elfz5 
 |-  ( ( ( ( A J x ) x. ( 2 ^ A ) ) e. ( ZZ>= ` 0 ) /\ ( A x. ( 2 ^ A ) ) e. ZZ ) -> ( ( ( A J x ) x. ( 2 ^ A ) ) e. ( 0 ... ( A x. ( 2 ^ A ) ) ) <-> ( ( A J x ) x. ( 2 ^ A ) ) <_ ( A x. ( 2 ^ A ) ) ) )
81 74 79 80 syl2anc 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( ( ( A J x ) x. ( 2 ^ A ) ) e. ( 0 ... ( A x. ( 2 ^ A ) ) ) <-> ( ( A J x ) x. ( 2 ^ A ) ) <_ ( A x. ( 2 ^ A ) ) ) )
82 40 81 mpbird 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( ( A J x ) x. ( 2 ^ A ) ) e. ( 0 ... ( A x. ( 2 ^ A ) ) ) )
83 oveq1 
 |-  ( m = ( ( A J x ) x. ( 2 ^ A ) ) -> ( m / ( 2 ^ A ) ) = ( ( ( A J x ) x. ( 2 ^ A ) ) / ( 2 ^ A ) ) )
84 eqid 
 |-  ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) = ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) )
85 ovex 
 |-  ( ( ( A J x ) x. ( 2 ^ A ) ) / ( 2 ^ A ) ) e. _V
86 83 84 85 fvmpt 
 |-  ( ( ( A J x ) x. ( 2 ^ A ) ) e. ( 0 ... ( A x. ( 2 ^ A ) ) ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` ( ( A J x ) x. ( 2 ^ A ) ) ) = ( ( ( A J x ) x. ( 2 ^ A ) ) / ( 2 ^ A ) ) )
87 82 86 syl 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` ( ( A J x ) x. ( 2 ^ A ) ) ) = ( ( ( A J x ) x. ( 2 ^ A ) ) / ( 2 ^ A ) ) )
88 27 adantr 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( A J x ) e. RR )
89 88 recnd 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( A J x ) e. CC )
90 89 68 69 divcan4d 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( ( ( A J x ) x. ( 2 ^ A ) ) / ( 2 ^ A ) ) = ( A J x ) )
91 87 90 eqtrd 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` ( ( A J x ) x. ( 2 ^ A ) ) ) = ( A J x ) )
92 elfznn0 
 |-  ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) -> m e. NN0 )
93 92 nn0red 
 |-  ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) -> m e. RR )
94 32 adantl 
 |-  ( ( ph /\ A e. NN ) -> ( 2 ^ A ) e. NN )
95 nndivre 
 |-  ( ( m e. RR /\ ( 2 ^ A ) e. NN ) -> ( m / ( 2 ^ A ) ) e. RR )
96 93 94 95 syl2anr 
 |-  ( ( ( ph /\ A e. NN ) /\ m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) ) -> ( m / ( 2 ^ A ) ) e. RR )
97 96 fmpttd 
 |-  ( ( ph /\ A e. NN ) -> ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) : ( 0 ... ( A x. ( 2 ^ A ) ) ) --> RR )
98 97 ffnd 
 |-  ( ( ph /\ A e. NN ) -> ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) Fn ( 0 ... ( A x. ( 2 ^ A ) ) ) )
99 98 adantr 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) Fn ( 0 ... ( A x. ( 2 ^ A ) ) ) )
100 99 adantr 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) Fn ( 0 ... ( A x. ( 2 ^ A ) ) ) )
101 fnfvelrn 
 |-  ( ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) Fn ( 0 ... ( A x. ( 2 ^ A ) ) ) /\ ( ( A J x ) x. ( 2 ^ A ) ) e. ( 0 ... ( A x. ( 2 ^ A ) ) ) ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` ( ( A J x ) x. ( 2 ^ A ) ) ) e. ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )
102 100 82 101 syl2anc 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` ( ( A J x ) x. ( 2 ^ A ) ) ) e. ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )
103 91 102 eqeltrrd 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ ( A J x ) <_ A ) -> ( A J x ) e. ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )
104 77 nnnn0d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( A x. ( 2 ^ A ) ) e. NN0 )
105 104 73 eleqtrdi 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( A x. ( 2 ^ A ) ) e. ( ZZ>= ` 0 ) )
106 eluzfz2 
 |-  ( ( A x. ( 2 ^ A ) ) e. ( ZZ>= ` 0 ) -> ( A x. ( 2 ^ A ) ) e. ( 0 ... ( A x. ( 2 ^ A ) ) ) )
107 105 106 syl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( A x. ( 2 ^ A ) ) e. ( 0 ... ( A x. ( 2 ^ A ) ) ) )
108 oveq1 
 |-  ( m = ( A x. ( 2 ^ A ) ) -> ( m / ( 2 ^ A ) ) = ( ( A x. ( 2 ^ A ) ) / ( 2 ^ A ) ) )
109 ovex 
 |-  ( ( A x. ( 2 ^ A ) ) / ( 2 ^ A ) ) e. _V
110 108 84 109 fvmpt 
 |-  ( ( A x. ( 2 ^ A ) ) e. ( 0 ... ( A x. ( 2 ^ A ) ) ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` ( A x. ( 2 ^ A ) ) ) = ( ( A x. ( 2 ^ A ) ) / ( 2 ^ A ) ) )
111 107 110 syl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` ( A x. ( 2 ^ A ) ) ) = ( ( A x. ( 2 ^ A ) ) / ( 2 ^ A ) ) )
112 29 recnd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> A e. CC )
113 33 nncnd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 2 ^ A ) e. CC )
114 33 nnne0d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 2 ^ A ) =/= 0 )
115 112 113 114 divcan4d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( A x. ( 2 ^ A ) ) / ( 2 ^ A ) ) = A )
116 111 115 eqtrd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` ( A x. ( 2 ^ A ) ) ) = A )
117 fnfvelrn 
 |-  ( ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) Fn ( 0 ... ( A x. ( 2 ^ A ) ) ) /\ ( A x. ( 2 ^ A ) ) e. ( 0 ... ( A x. ( 2 ^ A ) ) ) ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` ( A x. ( 2 ^ A ) ) ) e. ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )
118 99 107 117 syl2anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` ( A x. ( 2 ^ A ) ) ) e. ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )
119 116 118 eqeltrrd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> A e. ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )
120 119 adantr 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ -. ( A J x ) <_ A ) -> A e. ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )
121 103 120 ifclda 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> if ( ( A J x ) <_ A , ( A J x ) , A ) e. ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )
122 eluzfz1 
 |-  ( ( A x. ( 2 ^ A ) ) e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... ( A x. ( 2 ^ A ) ) ) )
123 105 122 syl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 e. ( 0 ... ( A x. ( 2 ^ A ) ) ) )
124 oveq1 
 |-  ( m = 0 -> ( m / ( 2 ^ A ) ) = ( 0 / ( 2 ^ A ) ) )
125 ovex 
 |-  ( 0 / ( 2 ^ A ) ) e. _V
126 124 84 125 fvmpt 
 |-  ( 0 e. ( 0 ... ( A x. ( 2 ^ A ) ) ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` 0 ) = ( 0 / ( 2 ^ A ) ) )
127 123 126 syl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` 0 ) = ( 0 / ( 2 ^ A ) ) )
128 nncn 
 |-  ( ( 2 ^ A ) e. NN -> ( 2 ^ A ) e. CC )
129 nnne0 
 |-  ( ( 2 ^ A ) e. NN -> ( 2 ^ A ) =/= 0 )
130 128 129 div0d 
 |-  ( ( 2 ^ A ) e. NN -> ( 0 / ( 2 ^ A ) ) = 0 )
131 33 130 syl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 0 / ( 2 ^ A ) ) = 0 )
132 127 131 eqtrd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` 0 ) = 0 )
133 fnfvelrn 
 |-  ( ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) Fn ( 0 ... ( A x. ( 2 ^ A ) ) ) /\ 0 e. ( 0 ... ( A x. ( 2 ^ A ) ) ) ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` 0 ) e. ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )
134 99 123 133 syl2anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) ` 0 ) e. ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )
135 132 134 eqeltrrd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 e. ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )
136 121 135 ifcld 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) e. ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )
137 6 136 fmpt3d 
 |-  ( ( ph /\ A e. NN ) -> ( G ` A ) : RR --> ran ( m e. ( 0 ... ( A x. ( 2 ^ A ) ) ) |-> ( m / ( 2 ^ A ) ) ) )