Metamath Proof Explorer

Theorem mbfi1fseqlem4

Description: Lemma for mbfi1fseq . This lemma is not as interesting as it is long - it is simply checking that G is in fact a sequence of simple functions, by verifying that its range is in ( 0 ... n 2 ^ n ) / ( 2 ^ n ) (which is to say, the numbers from 0 to n in increments of 1 / ( 2 ^ n ) ), and also that the preimage of each point k is measurable, because it is equal to ( -u n , n ) i^i (`' F " ( k [,) k + 1 / ( 2 ^ n ) ) ) for k < n and ( -u n , n ) i^i ( ``' F " ( k [,) +oo ) ) for k = n ` . (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 mbfi1fseqlem4 
|- ( ph -> G : NN --> dom S.1 )

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 reex 
 |-  RR e. _V
6 5 mptex 
 |-  ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) e. _V
7 6 4 fnmpti 
 |-  G Fn NN
8 7 a1i 
 |-  ( ph -> G Fn NN )
9 1 2 3 4 mbfi1fseqlem3 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) : RR --> ran ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) )
10 elfznn0 
 |-  ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) -> m e. NN0 )
11 10 nn0red 
 |-  ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) -> m e. RR )
12 2nn 
 |-  2 e. NN
13 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
14 nnexpcl 
 |-  ( ( 2 e. NN /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
15 12 13 14 sylancr 
 |-  ( n e. NN -> ( 2 ^ n ) e. NN )
16 15 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 2 ^ n ) e. NN )
17 nndivre 
 |-  ( ( m e. RR /\ ( 2 ^ n ) e. NN ) -> ( m / ( 2 ^ n ) ) e. RR )
18 11 16 17 syl2anr 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) ) -> ( m / ( 2 ^ n ) ) e. RR )
19 18 fmpttd 
 |-  ( ( ph /\ n e. NN ) -> ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) : ( 0 ... ( n x. ( 2 ^ n ) ) ) --> RR )
20 19 frnd 
 |-  ( ( ph /\ n e. NN ) -> ran ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) C_ RR )
21 9 20 fssd 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) : RR --> RR )
22 fzfid 
 |-  ( ( ph /\ n e. NN ) -> ( 0 ... ( n x. ( 2 ^ n ) ) ) e. Fin )
23 19 ffnd 
 |-  ( ( ph /\ n e. NN ) -> ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) Fn ( 0 ... ( n x. ( 2 ^ n ) ) ) )
24 dffn4 
 |-  ( ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) Fn ( 0 ... ( n x. ( 2 ^ n ) ) ) <-> ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) : ( 0 ... ( n x. ( 2 ^ n ) ) ) -onto-> ran ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) )
25 23 24 sylib 
 |-  ( ( ph /\ n e. NN ) -> ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) : ( 0 ... ( n x. ( 2 ^ n ) ) ) -onto-> ran ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) )
26 fofi 
 |-  ( ( ( 0 ... ( n x. ( 2 ^ n ) ) ) e. Fin /\ ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) : ( 0 ... ( n x. ( 2 ^ n ) ) ) -onto-> ran ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) ) -> ran ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) e. Fin )
27 22 25 26 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ran ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) e. Fin )
28 9 frnd 
 |-  ( ( ph /\ n e. NN ) -> ran ( G ` n ) C_ ran ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) )
29 27 28 ssfid 
 |-  ( ( ph /\ n e. NN ) -> ran ( G ` n ) e. Fin )
30 1 2 3 4 mbfi1fseqlem2 
 |-  ( n e. NN -> ( G ` n ) = ( x e. RR |-> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) ) )
31 30 fveq1d 
 |-  ( n e. NN -> ( ( G ` n ) ` x ) = ( ( x e. RR |-> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) ) ` x ) )
32 31 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( G ` n ) ` x ) = ( ( x e. RR |-> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) ) ` x ) )
33 simpr 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> x e. RR )
34 ovex 
 |-  ( n J x ) e. _V
35 vex 
 |-  n e. _V
36 34 35 ifex 
 |-  if ( ( n J x ) <_ n , ( n J x ) , n ) e. _V
37 c0ex 
 |-  0 e. _V
38 36 37 ifex 
 |-  if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) e. _V
39 eqid 
 |-  ( x e. RR |-> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) ) = ( x e. RR |-> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) )
40 39 fvmpt2 
 |-  ( ( x e. RR /\ if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) e. _V ) -> ( ( x e. RR |-> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) ) ` x ) = if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) )
41 33 38 40 sylancl 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( x e. RR |-> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) ) ` x ) = if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) )
42 32 41 eqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( G ` n ) ` x ) = if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) )
43 42 adantlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( G ` n ) ` x ) = if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) )
44 43 eqeq1d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( ( G ` n ) ` x ) = k <-> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) = k ) )
45 eldifsni 
 |-  ( k e. ( ran ( G ` n ) \ { 0 } ) -> k =/= 0 )
46 45 ad2antlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> k =/= 0 )
47 neeq1 
 |-  ( if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) = k -> ( if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) =/= 0 <-> k =/= 0 ) )
48 46 47 syl5ibrcom 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) = k -> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) =/= 0 ) )
49 iffalse 
 |-  ( -. x e. ( -u n [,] n ) -> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) = 0 )
50 49 necon1ai 
 |-  ( if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) =/= 0 -> x e. ( -u n [,] n ) )
51 48 50 syl6 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) = k -> x e. ( -u n [,] n ) ) )
52 51 pm4.71rd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) = k <-> ( x e. ( -u n [,] n ) /\ if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) = k ) ) )
53 iftrue 
 |-  ( x e. ( -u n [,] n ) -> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) = if ( ( n J x ) <_ n , ( n J x ) , n ) )
54 53 eqeq1d 
 |-  ( x e. ( -u n [,] n ) -> ( if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) = k <-> if ( ( n J x ) <_ n , ( n J x ) , n ) = k ) )
55 simpllr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> n e. NN )
56 55 nnred 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> n e. RR )
57 56 adantr 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> n e. RR )
58 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
59 simpr 
 |-  ( ( m e. NN /\ y e. RR ) -> y e. RR )
60 ffvelrn 
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ y e. RR ) -> ( F ` y ) e. ( 0 [,) +oo ) )
61 2 59 60 syl2an 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( F ` y ) e. ( 0 [,) +oo ) )
62 58 61 sseldi 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( F ` y ) e. RR )
63 nnnn0 
 |-  ( m e. NN -> m e. NN0 )
64 nnexpcl 
 |-  ( ( 2 e. NN /\ m e. NN0 ) -> ( 2 ^ m ) e. NN )
65 12 63 64 sylancr 
 |-  ( m e. NN -> ( 2 ^ m ) e. NN )
66 65 ad2antrl 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( 2 ^ m ) e. NN )
67 66 nnred 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( 2 ^ m ) e. RR )
68 62 67 remulcld 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( ( F ` y ) x. ( 2 ^ m ) ) e. RR )
69 reflcl 
 |-  ( ( ( F ` y ) x. ( 2 ^ m ) ) e. RR -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) e. RR )
70 68 69 syl 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) e. RR )
71 70 66 nndivred 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. RR )
72 71 ralrimivva 
 |-  ( ph -> A. m e. NN A. y e. RR ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. RR )
73 3 fmpo 
 |-  ( A. m e. NN A. y e. RR ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. RR <-> J : ( NN X. RR ) --> RR )
74 72 73 sylib 
 |-  ( ph -> J : ( NN X. RR ) --> RR )
75 fovrn 
 |-  ( ( J : ( NN X. RR ) --> RR /\ n e. NN /\ x e. RR ) -> ( n J x ) e. RR )
76 74 75 syl3an1 
 |-  ( ( ph /\ n e. NN /\ x e. RR ) -> ( n J x ) e. RR )
77 76 3expa 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( n J x ) e. RR )
78 77 adantlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( n J x ) e. RR )
79 78 adantr 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> ( n J x ) e. RR )
80 lemin 
 |-  ( ( n e. RR /\ ( n J x ) e. RR /\ n e. RR ) -> ( n <_ if ( ( n J x ) <_ n , ( n J x ) , n ) <-> ( n <_ ( n J x ) /\ n <_ n ) ) )
81 57 79 57 80 syl3anc 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> ( n <_ if ( ( n J x ) <_ n , ( n J x ) , n ) <-> ( n <_ ( n J x ) /\ n <_ n ) ) )
82 79 57 ifcld 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> if ( ( n J x ) <_ n , ( n J x ) , n ) e. RR )
83 82 57 letri3d 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> ( if ( ( n J x ) <_ n , ( n J x ) , n ) = n <-> ( if ( ( n J x ) <_ n , ( n J x ) , n ) <_ n /\ n <_ if ( ( n J x ) <_ n , ( n J x ) , n ) ) ) )
84 simpr 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> k = n )
85 84 eqeq2d 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> ( if ( ( n J x ) <_ n , ( n J x ) , n ) = k <-> if ( ( n J x ) <_ n , ( n J x ) , n ) = n ) )
86 min2 
 |-  ( ( ( n J x ) e. RR /\ n e. RR ) -> if ( ( n J x ) <_ n , ( n J x ) , n ) <_ n )
87 79 57 86 syl2anc 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> if ( ( n J x ) <_ n , ( n J x ) , n ) <_ n )
88 87 biantrurd 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> ( n <_ if ( ( n J x ) <_ n , ( n J x ) , n ) <-> ( if ( ( n J x ) <_ n , ( n J x ) , n ) <_ n /\ n <_ if ( ( n J x ) <_ n , ( n J x ) , n ) ) ) )
89 83 85 88 3bitr4d 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> ( if ( ( n J x ) <_ n , ( n J x ) , n ) = k <-> n <_ if ( ( n J x ) <_ n , ( n J x ) , n ) ) )
90 57 leidd 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> n <_ n )
91 90 biantrud 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> ( n <_ ( n J x ) <-> ( n <_ ( n J x ) /\ n <_ n ) ) )
92 81 89 91 3bitr4d 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> ( if ( ( n J x ) <_ n , ( n J x ) , n ) = k <-> n <_ ( n J x ) ) )
93 breq1 
 |-  ( k = n -> ( k <_ ( F ` x ) <-> n <_ ( F ` x ) ) )
94 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> F : RR --> ( 0 [,) +oo ) )
95 94 ffvelrnda 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
96 elrege0 
 |-  ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
97 95 96 sylib 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
98 97 simpld 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( F ` x ) e. RR )
99 98 adantlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( F ` x ) e. RR )
100 55 15 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( 2 ^ n ) e. NN )
101 100 nnred 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( 2 ^ n ) e. RR )
102 99 101 remulcld 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( F ` x ) x. ( 2 ^ n ) ) e. RR )
103 reflcl 
 |-  ( ( ( F ` x ) x. ( 2 ^ n ) ) e. RR -> ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) e. RR )
104 102 103 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) e. RR )
105 100 nngt0d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> 0 < ( 2 ^ n ) )
106 lemuldiv 
 |-  ( ( n e. RR /\ ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) e. RR /\ ( ( 2 ^ n ) e. RR /\ 0 < ( 2 ^ n ) ) ) -> ( ( n x. ( 2 ^ n ) ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) <-> n <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) / ( 2 ^ n ) ) ) )
107 56 104 101 105 106 syl112anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( n x. ( 2 ^ n ) ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) <-> n <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) / ( 2 ^ n ) ) ) )
108 lemul1 
 |-  ( ( n e. RR /\ ( F ` x ) e. RR /\ ( ( 2 ^ n ) e. RR /\ 0 < ( 2 ^ n ) ) ) -> ( n <_ ( F ` x ) <-> ( n x. ( 2 ^ n ) ) <_ ( ( F ` x ) x. ( 2 ^ n ) ) ) )
109 56 99 101 105 108 syl112anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( n <_ ( F ` x ) <-> ( n x. ( 2 ^ n ) ) <_ ( ( F ` x ) x. ( 2 ^ n ) ) ) )
110 nnmulcl 
 |-  ( ( n e. NN /\ ( 2 ^ n ) e. NN ) -> ( n x. ( 2 ^ n ) ) e. NN )
111 55 15 110 syl2anc2 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( n x. ( 2 ^ n ) ) e. NN )
112 111 nnzd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( n x. ( 2 ^ n ) ) e. ZZ )
113 flge 
 |-  ( ( ( ( F ` x ) x. ( 2 ^ n ) ) e. RR /\ ( n x. ( 2 ^ n ) ) e. ZZ ) -> ( ( n x. ( 2 ^ n ) ) <_ ( ( F ` x ) x. ( 2 ^ n ) ) <-> ( n x. ( 2 ^ n ) ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) ) )
114 102 112 113 syl2anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( n x. ( 2 ^ n ) ) <_ ( ( F ` x ) x. ( 2 ^ n ) ) <-> ( n x. ( 2 ^ n ) ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) ) )
115 109 114 bitrd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( n <_ ( F ` x ) <-> ( n x. ( 2 ^ n ) ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) ) )
116 simpr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> x e. RR )
117 simpr 
 |-  ( ( m = n /\ y = x ) -> y = x )
118 117 fveq2d 
 |-  ( ( m = n /\ y = x ) -> ( F ` y ) = ( F ` x ) )
119 simpl 
 |-  ( ( m = n /\ y = x ) -> m = n )
120 119 oveq2d 
 |-  ( ( m = n /\ y = x ) -> ( 2 ^ m ) = ( 2 ^ n ) )
121 118 120 oveq12d 
 |-  ( ( m = n /\ y = x ) -> ( ( F ` y ) x. ( 2 ^ m ) ) = ( ( F ` x ) x. ( 2 ^ n ) ) )
122 121 fveq2d 
 |-  ( ( m = n /\ y = x ) -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) = ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) )
123 122 120 oveq12d 
 |-  ( ( m = n /\ y = x ) -> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) / ( 2 ^ n ) ) )
124 ovex 
 |-  ( ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) / ( 2 ^ n ) ) e. _V
125 123 3 124 ovmpoa 
 |-  ( ( n e. NN /\ x e. RR ) -> ( n J x ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) / ( 2 ^ n ) ) )
126 55 116 125 syl2anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( n J x ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) / ( 2 ^ n ) ) )
127 126 breq2d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( n <_ ( n J x ) <-> n <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) / ( 2 ^ n ) ) ) )
128 107 115 127 3bitr4d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( n <_ ( F ` x ) <-> n <_ ( n J x ) ) )
129 93 128 sylan9bbr 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> ( k <_ ( F ` x ) <-> n <_ ( n J x ) ) )
130 116 adantr 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> x e. RR )
131 iftrue 
 |-  ( k = n -> if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) = RR )
132 131 adantl 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) = RR )
133 130 132 eleqtrrd 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> x e. if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) )
134 133 biantrurd 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> ( k <_ ( F ` x ) <-> ( x e. if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) /\ k <_ ( F ` x ) ) ) )
135 92 129 134 3bitr2d 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k = n ) -> ( if ( ( n J x ) <_ n , ( n J x ) , n ) = k <-> ( x e. if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) /\ k <_ ( F ` x ) ) ) )
136 28 ssdifssd 
 |-  ( ( ph /\ n e. NN ) -> ( ran ( G ` n ) \ { 0 } ) C_ ran ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) )
137 136 sselda 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> k e. ran ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) )
138 eqid 
 |-  ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) = ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) )
139 138 rnmpt 
 |-  ran ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) = { k | E. m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) k = ( m / ( 2 ^ n ) ) }
140 139 abeq2i 
 |-  ( k e. ran ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) <-> E. m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) k = ( m / ( 2 ^ n ) ) )
141 elfzelz 
 |-  ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) -> m e. ZZ )
142 141 adantl 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) ) -> m e. ZZ )
143 142 zcnd 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) ) -> m e. CC )
144 15 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) ) -> ( 2 ^ n ) e. NN )
145 144 nncnd 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) ) -> ( 2 ^ n ) e. CC )
146 144 nnne0d 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) ) -> ( 2 ^ n ) =/= 0 )
147 143 145 146 divcan1d 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) ) -> ( ( m / ( 2 ^ n ) ) x. ( 2 ^ n ) ) = m )
148 147 142 eqeltrd 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) ) -> ( ( m / ( 2 ^ n ) ) x. ( 2 ^ n ) ) e. ZZ )
149 oveq1 
 |-  ( k = ( m / ( 2 ^ n ) ) -> ( k x. ( 2 ^ n ) ) = ( ( m / ( 2 ^ n ) ) x. ( 2 ^ n ) ) )
150 149 eleq1d 
 |-  ( k = ( m / ( 2 ^ n ) ) -> ( ( k x. ( 2 ^ n ) ) e. ZZ <-> ( ( m / ( 2 ^ n ) ) x. ( 2 ^ n ) ) e. ZZ ) )
151 148 150 syl5ibrcom 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) ) -> ( k = ( m / ( 2 ^ n ) ) -> ( k x. ( 2 ^ n ) ) e. ZZ ) )
152 151 rexlimdva 
 |-  ( ( ph /\ n e. NN ) -> ( E. m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) k = ( m / ( 2 ^ n ) ) -> ( k x. ( 2 ^ n ) ) e. ZZ ) )
153 140 152 syl5bi 
 |-  ( ( ph /\ n e. NN ) -> ( k e. ran ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) -> ( k x. ( 2 ^ n ) ) e. ZZ ) )
154 153 imp 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ran ( m e. ( 0 ... ( n x. ( 2 ^ n ) ) ) |-> ( m / ( 2 ^ n ) ) ) ) -> ( k x. ( 2 ^ n ) ) e. ZZ )
155 137 154 syldan 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( k x. ( 2 ^ n ) ) e. ZZ )
156 155 adantr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( k x. ( 2 ^ n ) ) e. ZZ )
157 flbi 
 |-  ( ( ( ( F ` x ) x. ( 2 ^ n ) ) e. RR /\ ( k x. ( 2 ^ n ) ) e. ZZ ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) = ( k x. ( 2 ^ n ) ) <-> ( ( k x. ( 2 ^ n ) ) <_ ( ( F ` x ) x. ( 2 ^ n ) ) /\ ( ( F ` x ) x. ( 2 ^ n ) ) < ( ( k x. ( 2 ^ n ) ) + 1 ) ) ) )
158 102 156 157 syl2anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) = ( k x. ( 2 ^ n ) ) <-> ( ( k x. ( 2 ^ n ) ) <_ ( ( F ` x ) x. ( 2 ^ n ) ) /\ ( ( F ` x ) x. ( 2 ^ n ) ) < ( ( k x. ( 2 ^ n ) ) + 1 ) ) ) )
159 158 adantr 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k =/= n ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) = ( k x. ( 2 ^ n ) ) <-> ( ( k x. ( 2 ^ n ) ) <_ ( ( F ` x ) x. ( 2 ^ n ) ) /\ ( ( F ` x ) x. ( 2 ^ n ) ) < ( ( k x. ( 2 ^ n ) ) + 1 ) ) ) )
160 neeq1 
 |-  ( if ( ( n J x ) <_ n , ( n J x ) , n ) = k -> ( if ( ( n J x ) <_ n , ( n J x ) , n ) =/= n <-> k =/= n ) )
161 160 biimparc 
 |-  ( ( k =/= n /\ if ( ( n J x ) <_ n , ( n J x ) , n ) = k ) -> if ( ( n J x ) <_ n , ( n J x ) , n ) =/= n )
162 iffalse 
 |-  ( -. ( n J x ) <_ n -> if ( ( n J x ) <_ n , ( n J x ) , n ) = n )
163 162 necon1ai 
 |-  ( if ( ( n J x ) <_ n , ( n J x ) , n ) =/= n -> ( n J x ) <_ n )
164 161 163 syl 
 |-  ( ( k =/= n /\ if ( ( n J x ) <_ n , ( n J x ) , n ) = k ) -> ( n J x ) <_ n )
165 164 iftrued 
 |-  ( ( k =/= n /\ if ( ( n J x ) <_ n , ( n J x ) , n ) = k ) -> if ( ( n J x ) <_ n , ( n J x ) , n ) = ( n J x ) )
166 simpr 
 |-  ( ( k =/= n /\ if ( ( n J x ) <_ n , ( n J x ) , n ) = k ) -> if ( ( n J x ) <_ n , ( n J x ) , n ) = k )
167 165 166 eqtr3d 
 |-  ( ( k =/= n /\ if ( ( n J x ) <_ n , ( n J x ) , n ) = k ) -> ( n J x ) = k )
168 167 164 eqbrtrrd 
 |-  ( ( k =/= n /\ if ( ( n J x ) <_ n , ( n J x ) , n ) = k ) -> k <_ n )
169 168 167 jca 
 |-  ( ( k =/= n /\ if ( ( n J x ) <_ n , ( n J x ) , n ) = k ) -> ( k <_ n /\ ( n J x ) = k ) )
170 169 ex 
 |-  ( k =/= n -> ( if ( ( n J x ) <_ n , ( n J x ) , n ) = k -> ( k <_ n /\ ( n J x ) = k ) ) )
171 breq1 
 |-  ( ( n J x ) = k -> ( ( n J x ) <_ n <-> k <_ n ) )
172 171 biimparc 
 |-  ( ( k <_ n /\ ( n J x ) = k ) -> ( n J x ) <_ n )
173 172 iftrued 
 |-  ( ( k <_ n /\ ( n J x ) = k ) -> if ( ( n J x ) <_ n , ( n J x ) , n ) = ( n J x ) )
174 simpr 
 |-  ( ( k <_ n /\ ( n J x ) = k ) -> ( n J x ) = k )
175 173 174 eqtrd 
 |-  ( ( k <_ n /\ ( n J x ) = k ) -> if ( ( n J x ) <_ n , ( n J x ) , n ) = k )
176 170 175 impbid1 
 |-  ( k =/= n -> ( if ( ( n J x ) <_ n , ( n J x ) , n ) = k <-> ( k <_ n /\ ( n J x ) = k ) ) )
177 176 adantl 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k =/= n ) -> ( if ( ( n J x ) <_ n , ( n J x ) , n ) = k <-> ( k <_ n /\ ( n J x ) = k ) ) )
178 eldifi 
 |-  ( k e. ( ran ( G ` n ) \ { 0 } ) -> k e. ran ( G ` n ) )
179 nnre 
 |-  ( n e. NN -> n e. RR )
180 179 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> n e. RR )
181 77 180 86 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> if ( ( n J x ) <_ n , ( n J x ) , n ) <_ n )
182 13 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> n e. NN0 )
183 182 nn0ge0d 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> 0 <_ n )
184 breq1 
 |-  ( if ( ( n J x ) <_ n , ( n J x ) , n ) = if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) -> ( if ( ( n J x ) <_ n , ( n J x ) , n ) <_ n <-> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) <_ n ) )
185 breq1 
 |-  ( 0 = if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) -> ( 0 <_ n <-> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) <_ n ) )
186 184 185 ifboth 
 |-  ( ( if ( ( n J x ) <_ n , ( n J x ) , n ) <_ n /\ 0 <_ n ) -> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) <_ n )
187 181 183 186 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) <_ n )
188 42 187 eqbrtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( G ` n ) ` x ) <_ n )
189 188 ralrimiva 
 |-  ( ( ph /\ n e. NN ) -> A. x e. RR ( ( G ` n ) ` x ) <_ n )
190 9 ffnd 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) Fn RR )
191 breq1 
 |-  ( k = ( ( G ` n ) ` x ) -> ( k <_ n <-> ( ( G ` n ) ` x ) <_ n ) )
192 191 ralrn 
 |-  ( ( G ` n ) Fn RR -> ( A. k e. ran ( G ` n ) k <_ n <-> A. x e. RR ( ( G ` n ) ` x ) <_ n ) )
193 190 192 syl 
 |-  ( ( ph /\ n e. NN ) -> ( A. k e. ran ( G ` n ) k <_ n <-> A. x e. RR ( ( G ` n ) ` x ) <_ n ) )
194 189 193 mpbird 
 |-  ( ( ph /\ n e. NN ) -> A. k e. ran ( G ` n ) k <_ n )
195 194 r19.21bi 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ran ( G ` n ) ) -> k <_ n )
196 178 195 sylan2 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> k <_ n )
197 196 ad2antrr 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k =/= n ) -> k <_ n )
198 197 biantrurd 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k =/= n ) -> ( ( n J x ) = k <-> ( k <_ n /\ ( n J x ) = k ) ) )
199 126 eqeq1d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( n J x ) = k <-> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) / ( 2 ^ n ) ) = k ) )
200 104 recnd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) e. CC )
201 28 20 sstrd 
 |-  ( ( ph /\ n e. NN ) -> ran ( G ` n ) C_ RR )
202 201 ssdifssd 
 |-  ( ( ph /\ n e. NN ) -> ( ran ( G ` n ) \ { 0 } ) C_ RR )
203 202 sselda 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> k e. RR )
204 203 adantr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> k e. RR )
205 204 recnd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> k e. CC )
206 100 nncnd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( 2 ^ n ) e. CC )
207 100 nnne0d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( 2 ^ n ) =/= 0 )
208 200 205 206 207 divmul3d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) / ( 2 ^ n ) ) = k <-> ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) = ( k x. ( 2 ^ n ) ) ) )
209 199 208 bitrd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( n J x ) = k <-> ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) = ( k x. ( 2 ^ n ) ) ) )
210 209 adantr 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k =/= n ) -> ( ( n J x ) = k <-> ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) = ( k x. ( 2 ^ n ) ) ) )
211 177 198 210 3bitr2d 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k =/= n ) -> ( if ( ( n J x ) <_ n , ( n J x ) , n ) = k <-> ( |_ ` ( ( F ` x ) x. ( 2 ^ n ) ) ) = ( k x. ( 2 ^ n ) ) ) )
212 ifnefalse 
 |-  ( k =/= n -> if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) = ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) )
213 212 eleq2d 
 |-  ( k =/= n -> ( x e. if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) <-> x e. ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) )
214 100 nnrecred 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( 1 / ( 2 ^ n ) ) e. RR )
215 204 214 readdcld 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( k + ( 1 / ( 2 ^ n ) ) ) e. RR )
216 215 rexrd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( k + ( 1 / ( 2 ^ n ) ) ) e. RR* )
217 elioomnf 
 |-  ( ( k + ( 1 / ( 2 ^ n ) ) ) e. RR* -> ( ( F ` x ) e. ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) <-> ( ( F ` x ) e. RR /\ ( F ` x ) < ( k + ( 1 / ( 2 ^ n ) ) ) ) ) )
218 216 217 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( F ` x ) e. ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) <-> ( ( F ` x ) e. RR /\ ( F ` x ) < ( k + ( 1 / ( 2 ^ n ) ) ) ) ) )
219 94 ad2antrr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> F : RR --> ( 0 [,) +oo ) )
220 219 ffnd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> F Fn RR )
221 elpreima 
 |-  ( F Fn RR -> ( x e. ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) <-> ( x e. RR /\ ( F ` x ) e. ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) )
222 220 221 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( x e. ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) <-> ( x e. RR /\ ( F ` x ) e. ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) )
223 116 222 mpbirand 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( x e. ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) <-> ( F ` x ) e. ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) )
224 99 biantrurd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( F ` x ) < ( k + ( 1 / ( 2 ^ n ) ) ) <-> ( ( F ` x ) e. RR /\ ( F ` x ) < ( k + ( 1 / ( 2 ^ n ) ) ) ) ) )
225 218 223 224 3bitr4d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( x e. ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) <-> ( F ` x ) < ( k + ( 1 / ( 2 ^ n ) ) ) ) )
226 ltmul1 
 |-  ( ( ( F ` x ) e. RR /\ ( k + ( 1 / ( 2 ^ n ) ) ) e. RR /\ ( ( 2 ^ n ) e. RR /\ 0 < ( 2 ^ n ) ) ) -> ( ( F ` x ) < ( k + ( 1 / ( 2 ^ n ) ) ) <-> ( ( F ` x ) x. ( 2 ^ n ) ) < ( ( k + ( 1 / ( 2 ^ n ) ) ) x. ( 2 ^ n ) ) ) )
227 99 215 101 105 226 syl112anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( F ` x ) < ( k + ( 1 / ( 2 ^ n ) ) ) <-> ( ( F ` x ) x. ( 2 ^ n ) ) < ( ( k + ( 1 / ( 2 ^ n ) ) ) x. ( 2 ^ n ) ) ) )
228 214 recnd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( 1 / ( 2 ^ n ) ) e. CC )
229 206 207 recid2d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( 1 / ( 2 ^ n ) ) x. ( 2 ^ n ) ) = 1 )
230 229 oveq2d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( k x. ( 2 ^ n ) ) + ( ( 1 / ( 2 ^ n ) ) x. ( 2 ^ n ) ) ) = ( ( k x. ( 2 ^ n ) ) + 1 ) )
231 205 206 228 230 joinlmuladdmuld 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( k + ( 1 / ( 2 ^ n ) ) ) x. ( 2 ^ n ) ) = ( ( k x. ( 2 ^ n ) ) + 1 ) )
232 231 breq2d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( ( F ` x ) x. ( 2 ^ n ) ) < ( ( k + ( 1 / ( 2 ^ n ) ) ) x. ( 2 ^ n ) ) <-> ( ( F ` x ) x. ( 2 ^ n ) ) < ( ( k x. ( 2 ^ n ) ) + 1 ) ) )
233 225 227 232 3bitrd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( x e. ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) <-> ( ( F ` x ) x. ( 2 ^ n ) ) < ( ( k x. ( 2 ^ n ) ) + 1 ) ) )
234 213 233 sylan9bbr 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k =/= n ) -> ( x e. if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) <-> ( ( F ` x ) x. ( 2 ^ n ) ) < ( ( k x. ( 2 ^ n ) ) + 1 ) ) )
235 lemul1 
 |-  ( ( k e. RR /\ ( F ` x ) e. RR /\ ( ( 2 ^ n ) e. RR /\ 0 < ( 2 ^ n ) ) ) -> ( k <_ ( F ` x ) <-> ( k x. ( 2 ^ n ) ) <_ ( ( F ` x ) x. ( 2 ^ n ) ) ) )
236 204 99 101 105 235 syl112anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( k <_ ( F ` x ) <-> ( k x. ( 2 ^ n ) ) <_ ( ( F ` x ) x. ( 2 ^ n ) ) ) )
237 236 adantr 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k =/= n ) -> ( k <_ ( F ` x ) <-> ( k x. ( 2 ^ n ) ) <_ ( ( F ` x ) x. ( 2 ^ n ) ) ) )
238 234 237 anbi12d 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k =/= n ) -> ( ( x e. if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) /\ k <_ ( F ` x ) ) <-> ( ( ( F ` x ) x. ( 2 ^ n ) ) < ( ( k x. ( 2 ^ n ) ) + 1 ) /\ ( k x. ( 2 ^ n ) ) <_ ( ( F ` x ) x. ( 2 ^ n ) ) ) ) )
239 238 biancomd 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k =/= n ) -> ( ( x e. if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) /\ k <_ ( F ` x ) ) <-> ( ( k x. ( 2 ^ n ) ) <_ ( ( F ` x ) x. ( 2 ^ n ) ) /\ ( ( F ` x ) x. ( 2 ^ n ) ) < ( ( k x. ( 2 ^ n ) ) + 1 ) ) ) )
240 159 211 239 3bitr4d 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ k =/= n ) -> ( if ( ( n J x ) <_ n , ( n J x ) , n ) = k <-> ( x e. if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) /\ k <_ ( F ` x ) ) ) )
241 135 240 pm2.61dane 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( if ( ( n J x ) <_ n , ( n J x ) , n ) = k <-> ( x e. if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) /\ k <_ ( F ` x ) ) ) )
242 eldif 
 |-  ( x e. ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) <-> ( x e. if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) /\ -. x e. ( `' F " ( -oo (,) k ) ) ) )
243 204 rexrd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> k e. RR* )
244 elioomnf 
 |-  ( k e. RR* -> ( ( F ` x ) e. ( -oo (,) k ) <-> ( ( F ` x ) e. RR /\ ( F ` x ) < k ) ) )
245 243 244 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( F ` x ) e. ( -oo (,) k ) <-> ( ( F ` x ) e. RR /\ ( F ` x ) < k ) ) )
246 elpreima 
 |-  ( F Fn RR -> ( x e. ( `' F " ( -oo (,) k ) ) <-> ( x e. RR /\ ( F ` x ) e. ( -oo (,) k ) ) ) )
247 220 246 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( x e. ( `' F " ( -oo (,) k ) ) <-> ( x e. RR /\ ( F ` x ) e. ( -oo (,) k ) ) ) )
248 116 247 mpbirand 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( x e. ( `' F " ( -oo (,) k ) ) <-> ( F ` x ) e. ( -oo (,) k ) ) )
249 99 biantrurd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( F ` x ) < k <-> ( ( F ` x ) e. RR /\ ( F ` x ) < k ) ) )
250 245 248 249 3bitr4d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( x e. ( `' F " ( -oo (,) k ) ) <-> ( F ` x ) < k ) )
251 250 notbid 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( -. x e. ( `' F " ( -oo (,) k ) ) <-> -. ( F ` x ) < k ) )
252 204 99 lenltd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( k <_ ( F ` x ) <-> -. ( F ` x ) < k ) )
253 251 252 bitr4d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( -. x e. ( `' F " ( -oo (,) k ) ) <-> k <_ ( F ` x ) ) )
254 253 anbi2d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( x e. if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) /\ -. x e. ( `' F " ( -oo (,) k ) ) ) <-> ( x e. if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) /\ k <_ ( F ` x ) ) ) )
255 242 254 syl5bb 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( x e. ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) <-> ( x e. if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) /\ k <_ ( F ` x ) ) ) )
256 241 255 bitr4d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( if ( ( n J x ) <_ n , ( n J x ) , n ) = k <-> x e. ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) )
257 54 256 sylan9bbr 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) /\ x e. ( -u n [,] n ) ) -> ( if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) = k <-> x e. ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) )
258 257 pm5.32da 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( x e. ( -u n [,] n ) /\ if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) = k ) <-> ( x e. ( -u n [,] n ) /\ x e. ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) ) )
259 44 52 258 3bitrd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( ( G ` n ) ` x ) = k <-> ( x e. ( -u n [,] n ) /\ x e. ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) ) )
260 259 pm5.32da 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( ( x e. RR /\ ( ( G ` n ) ` x ) = k ) <-> ( x e. RR /\ ( x e. ( -u n [,] n ) /\ x e. ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) ) ) )
261 21 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( G ` n ) : RR --> RR )
262 261 ffnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( G ` n ) Fn RR )
263 fniniseg 
 |-  ( ( G ` n ) Fn RR -> ( x e. ( `' ( G ` n ) " { k } ) <-> ( x e. RR /\ ( ( G ` n ) ` x ) = k ) ) )
264 262 263 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( x e. ( `' ( G ` n ) " { k } ) <-> ( x e. RR /\ ( ( G ` n ) ` x ) = k ) ) )
265 elin 
 |-  ( x e. ( ( -u n [,] n ) i^i ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) <-> ( x e. ( -u n [,] n ) /\ x e. ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) )
266 179 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> n e. RR )
267 266 renegcld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> -u n e. RR )
268 iccmbl 
 |-  ( ( -u n e. RR /\ n e. RR ) -> ( -u n [,] n ) e. dom vol )
269 267 266 268 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( -u n [,] n ) e. dom vol )
270 mblss 
 |-  ( ( -u n [,] n ) e. dom vol -> ( -u n [,] n ) C_ RR )
271 269 270 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( -u n [,] n ) C_ RR )
272 271 sseld 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( x e. ( -u n [,] n ) -> x e. RR ) )
273 272 adantrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( ( x e. ( -u n [,] n ) /\ x e. ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) -> x e. RR ) )
274 273 pm4.71rd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( ( x e. ( -u n [,] n ) /\ x e. ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) <-> ( x e. RR /\ ( x e. ( -u n [,] n ) /\ x e. ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) ) ) )
275 265 274 syl5bb 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( x e. ( ( -u n [,] n ) i^i ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) <-> ( x e. RR /\ ( x e. ( -u n [,] n ) /\ x e. ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) ) ) )
276 260 264 275 3bitr4d 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( x e. ( `' ( G ` n ) " { k } ) <-> x e. ( ( -u n [,] n ) i^i ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) ) )
277 276 eqrdv 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( `' ( G ` n ) " { k } ) = ( ( -u n [,] n ) i^i ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) )
278 rembl 
 |-  RR e. dom vol
279 fss 
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : RR --> RR )
280 2 58 279 sylancl 
 |-  ( ph -> F : RR --> RR )
281 mbfima 
 |-  ( ( F e. MblFn /\ F : RR --> RR ) -> ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) e. dom vol )
282 1 280 281 syl2anc 
 |-  ( ph -> ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) e. dom vol )
283 ifcl 
 |-  ( ( RR e. dom vol /\ ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) e. dom vol ) -> if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) e. dom vol )
284 278 282 283 sylancr 
 |-  ( ph -> if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) e. dom vol )
285 mbfima 
 |-  ( ( F e. MblFn /\ F : RR --> RR ) -> ( `' F " ( -oo (,) k ) ) e. dom vol )
286 1 280 285 syl2anc 
 |-  ( ph -> ( `' F " ( -oo (,) k ) ) e. dom vol )
287 difmbl 
 |-  ( ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) e. dom vol /\ ( `' F " ( -oo (,) k ) ) e. dom vol ) -> ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) e. dom vol )
288 284 286 287 syl2anc 
 |-  ( ph -> ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) e. dom vol )
289 288 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) e. dom vol )
290 inmbl 
 |-  ( ( ( -u n [,] n ) e. dom vol /\ ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) e. dom vol ) -> ( ( -u n [,] n ) i^i ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) e. dom vol )
291 269 289 290 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( ( -u n [,] n ) i^i ( if ( k = n , RR , ( `' F " ( -oo (,) ( k + ( 1 / ( 2 ^ n ) ) ) ) ) ) \ ( `' F " ( -oo (,) k ) ) ) ) e. dom vol )
292 277 291 eqeltrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( `' ( G ` n ) " { k } ) e. dom vol )
293 mblvol 
 |-  ( ( `' ( G ` n ) " { k } ) e. dom vol -> ( vol ` ( `' ( G ` n ) " { k } ) ) = ( vol* ` ( `' ( G ` n ) " { k } ) ) )
294 292 293 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( vol ` ( `' ( G ` n ) " { k } ) ) = ( vol* ` ( `' ( G ` n ) " { k } ) ) )
295 190 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( G ` n ) Fn RR )
296 295 263 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( x e. ( `' ( G ` n ) " { k } ) <-> ( x e. RR /\ ( ( G ` n ) ` x ) = k ) ) )
297 77 180 ifcld 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> if ( ( n J x ) <_ n , ( n J x ) , n ) e. RR )
298 0re 
 |-  0 e. RR
299 ifcl 
 |-  ( ( if ( ( n J x ) <_ n , ( n J x ) , n ) e. RR /\ 0 e. RR ) -> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) e. RR )
300 297 298 299 sylancl 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) e. RR )
301 39 fvmpt2 
 |-  ( ( x e. RR /\ if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) e. RR ) -> ( ( x e. RR |-> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) ) ` x ) = if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) )
302 33 300 301 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( x e. RR |-> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) ) ` x ) = if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) )
303 32 302 eqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( G ` n ) ` x ) = if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) )
304 303 adantlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( G ` n ) ` x ) = if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) )
305 304 eqeq1d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( ( G ` n ) ` x ) = k <-> if ( x e. ( -u n [,] n ) , if ( ( n J x ) <_ n , ( n J x ) , n ) , 0 ) = k ) )
306 305 51 sylbid 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) /\ x e. RR ) -> ( ( ( G ` n ) ` x ) = k -> x e. ( -u n [,] n ) ) )
307 306 expimpd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( ( x e. RR /\ ( ( G ` n ) ` x ) = k ) -> x e. ( -u n [,] n ) ) )
308 296 307 sylbid 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( x e. ( `' ( G ` n ) " { k } ) -> x e. ( -u n [,] n ) ) )
309 308 ssrdv 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( `' ( G ` n ) " { k } ) C_ ( -u n [,] n ) )
310 iccssre 
 |-  ( ( -u n e. RR /\ n e. RR ) -> ( -u n [,] n ) C_ RR )
311 267 266 310 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( -u n [,] n ) C_ RR )
312 mblvol 
 |-  ( ( -u n [,] n ) e. dom vol -> ( vol ` ( -u n [,] n ) ) = ( vol* ` ( -u n [,] n ) ) )
313 269 312 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( vol ` ( -u n [,] n ) ) = ( vol* ` ( -u n [,] n ) ) )
314 iccvolcl 
 |-  ( ( -u n e. RR /\ n e. RR ) -> ( vol ` ( -u n [,] n ) ) e. RR )
315 267 266 314 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( vol ` ( -u n [,] n ) ) e. RR )
316 313 315 eqeltrrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( vol* ` ( -u n [,] n ) ) e. RR )
317 ovolsscl 
 |-  ( ( ( `' ( G ` n ) " { k } ) C_ ( -u n [,] n ) /\ ( -u n [,] n ) C_ RR /\ ( vol* ` ( -u n [,] n ) ) e. RR ) -> ( vol* ` ( `' ( G ` n ) " { k } ) ) e. RR )
318 309 311 316 317 syl3anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( vol* ` ( `' ( G ` n ) " { k } ) ) e. RR )
319 294 318 eqeltrd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ran ( G ` n ) \ { 0 } ) ) -> ( vol ` ( `' ( G ` n ) " { k } ) ) e. RR )
320 21 29 292 319 i1fd 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) e. dom S.1 )
321 320 ralrimiva 
 |-  ( ph -> A. n e. NN ( G ` n ) e. dom S.1 )
322 ffnfv 
 |-  ( G : NN --> dom S.1 <-> ( G Fn NN /\ A. n e. NN ( G ` n ) e. dom S.1 ) )
323 8 321 322 sylanbrc 
 |-  ( ph -> G : NN --> dom S.1 )