Metamath Proof Explorer

Theorem mbfi1fseqlem5

Description: Lemma for mbfi1fseq . Verify that G describes an increasing sequence of positive functions. (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 mbfi1fseqlem5 
|- ( ( ph /\ A e. NN ) -> ( 0p oR <_ ( G ` A ) /\ ( G ` A ) oR <_ ( G ` ( A + 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 2 adantr 
 |-  ( ( ph /\ A e. NN ) -> F : RR --> ( 0 [,) +oo ) )
6 5 ffvelcdmda 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
7 elrege0 
 |-  ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
8 6 7 sylib 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
9 8 simpld 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( F ` x ) e. RR )
10 2nn 
 |-  2 e. NN
11 nnnn0 
 |-  ( A e. NN -> A e. NN0 )
12 nnexpcl 
 |-  ( ( 2 e. NN /\ A e. NN0 ) -> ( 2 ^ A ) e. NN )
13 10 11 12 sylancr 
 |-  ( A e. NN -> ( 2 ^ A ) e. NN )
14 13 ad2antlr 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 2 ^ A ) e. NN )
15 14 nnred 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 2 ^ A ) e. RR )
16 9 15 remulcld 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( F ` x ) x. ( 2 ^ A ) ) e. RR )
17 14 nnnn0d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 2 ^ A ) e. NN0 )
18 17 nn0ge0d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 <_ ( 2 ^ A ) )
19 mulge0 
 |-  ( ( ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) /\ ( ( 2 ^ A ) e. RR /\ 0 <_ ( 2 ^ A ) ) ) -> 0 <_ ( ( F ` x ) x. ( 2 ^ A ) ) )
20 8 15 18 19 syl12anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 <_ ( ( F ` x ) x. ( 2 ^ A ) ) )
21 flge0nn0 
 |-  ( ( ( ( F ` x ) x. ( 2 ^ A ) ) e. RR /\ 0 <_ ( ( F ` x ) x. ( 2 ^ A ) ) ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) e. NN0 )
22 16 20 21 syl2anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) e. NN0 )
23 22 nn0red 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) e. RR )
24 22 nn0ge0d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) )
25 14 nngt0d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 < ( 2 ^ A ) )
26 divge0 
 |-  ( ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) e. RR /\ 0 <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) ) /\ ( ( 2 ^ A ) e. RR /\ 0 < ( 2 ^ A ) ) ) -> 0 <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) )
27 23 24 15 25 26 syl22anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) )
28 simpr 
 |-  ( ( m = A /\ y = x ) -> y = x )
29 28 fveq2d 
 |-  ( ( m = A /\ y = x ) -> ( F ` y ) = ( F ` x ) )
30 simpl 
 |-  ( ( m = A /\ y = x ) -> m = A )
31 30 oveq2d 
 |-  ( ( m = A /\ y = x ) -> ( 2 ^ m ) = ( 2 ^ A ) )
32 29 31 oveq12d 
 |-  ( ( m = A /\ y = x ) -> ( ( F ` y ) x. ( 2 ^ m ) ) = ( ( F ` x ) x. ( 2 ^ A ) ) )
33 32 fveq2d 
 |-  ( ( m = A /\ y = x ) -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) = ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) )
34 33 31 oveq12d 
 |-  ( ( m = A /\ y = x ) -> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) )
35 ovex 
 |-  ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) e. _V
36 34 3 35 ovmpoa 
 |-  ( ( A e. NN /\ x e. RR ) -> ( A J x ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) )
37 36 adantll 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( A J x ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) )
38 27 37 breqtrrd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 <_ ( A J x ) )
39 11 nn0ge0d 
 |-  ( A e. NN -> 0 <_ A )
40 39 ad2antlr 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 <_ A )
41 breq2 
 |-  ( ( A J x ) = if ( ( A J x ) <_ A , ( A J x ) , A ) -> ( 0 <_ ( A J x ) <-> 0 <_ if ( ( A J x ) <_ A , ( A J x ) , A ) ) )
42 breq2 
 |-  ( A = if ( ( A J x ) <_ A , ( A J x ) , A ) -> ( 0 <_ A <-> 0 <_ if ( ( A J x ) <_ A , ( A J x ) , A ) ) )
43 41 42 ifboth 
 |-  ( ( 0 <_ ( A J x ) /\ 0 <_ A ) -> 0 <_ if ( ( A J x ) <_ A , ( A J x ) , A ) )
44 38 40 43 syl2anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 <_ if ( ( A J x ) <_ A , ( A J x ) , A ) )
45 0le0 
 |-  0 <_ 0
46 breq2 
 |-  ( if ( ( A J x ) <_ A , ( A J x ) , A ) = if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) -> ( 0 <_ if ( ( A J x ) <_ A , ( A J x ) , A ) <-> 0 <_ if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) )
47 breq2 
 |-  ( 0 = if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) -> ( 0 <_ 0 <-> 0 <_ if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) )
48 46 47 ifboth 
 |-  ( ( 0 <_ if ( ( A J x ) <_ A , ( A J x ) , A ) /\ 0 <_ 0 ) -> 0 <_ if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) )
49 44 45 48 sylancl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 <_ if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) )
50 49 ralrimiva 
 |-  ( ( ph /\ A e. NN ) -> A. x e. RR 0 <_ if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) )
51 0re 
 |-  0 e. RR
52 fnconstg 
 |-  ( 0 e. RR -> ( CC X. { 0 } ) Fn CC )
53 51 52 ax-mp 
 |-  ( CC X. { 0 } ) Fn CC
54 df-0p 
 |-  0p = ( CC X. { 0 } )
55 54 fneq1i 
 |-  ( 0p Fn CC <-> ( CC X. { 0 } ) Fn CC )
56 53 55 mpbir 
 |-  0p Fn CC
57 56 a1i 
 |-  ( ( ph /\ A e. NN ) -> 0p Fn CC )
58 1 2 3 4 mbfi1fseqlem4 
 |-  ( ph -> G : NN --> dom S.1 )
59 58 ffvelcdmda 
 |-  ( ( ph /\ A e. NN ) -> ( G ` A ) e. dom S.1 )
60 i1ff 
 |-  ( ( G ` A ) e. dom S.1 -> ( G ` A ) : RR --> RR )
61 ffn 
 |-  ( ( G ` A ) : RR --> RR -> ( G ` A ) Fn RR )
62 59 60 61 3syl 
 |-  ( ( ph /\ A e. NN ) -> ( G ` A ) Fn RR )
63 cnex 
 |-  CC e. _V
64 63 a1i 
 |-  ( ( ph /\ A e. NN ) -> CC e. _V )
65 reex 
 |-  RR e. _V
66 65 a1i 
 |-  ( ( ph /\ A e. NN ) -> RR e. _V )
67 ax-resscn 
 |-  RR C_ CC
68 sseqin2 
 |-  ( RR C_ CC <-> ( CC i^i RR ) = RR )
69 67 68 mpbi 
 |-  ( CC i^i RR ) = RR
70 0pval 
 |-  ( x e. CC -> ( 0p ` x ) = 0 )
71 70 adantl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. CC ) -> ( 0p ` x ) = 0 )
72 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 ) ) )
73 72 fveq1d 
 |-  ( A e. NN -> ( ( G ` A ) ` x ) = ( ( x e. RR |-> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) ` x ) )
74 73 ad2antlr 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( G ` A ) ` x ) = ( ( x e. RR |-> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) ` x ) )
75 simpr 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> x e. RR )
76 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
77 simpr 
 |-  ( ( m e. NN /\ y e. RR ) -> y e. RR )
78 ffvelcdm 
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ y e. RR ) -> ( F ` y ) e. ( 0 [,) +oo ) )
79 2 77 78 syl2an 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( F ` y ) e. ( 0 [,) +oo ) )
80 76 79 sselid 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( F ` y ) e. RR )
81 nnnn0 
 |-  ( m e. NN -> m e. NN0 )
82 nnexpcl 
 |-  ( ( 2 e. NN /\ m e. NN0 ) -> ( 2 ^ m ) e. NN )
83 10 81 82 sylancr 
 |-  ( m e. NN -> ( 2 ^ m ) e. NN )
84 83 ad2antrl 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( 2 ^ m ) e. NN )
85 84 nnred 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( 2 ^ m ) e. RR )
86 80 85 remulcld 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( ( F ` y ) x. ( 2 ^ m ) ) e. RR )
87 reflcl 
 |-  ( ( ( F ` y ) x. ( 2 ^ m ) ) e. RR -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) e. RR )
88 86 87 syl 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) e. RR )
89 88 84 nndivred 
 |-  ( ( ph /\ ( m e. NN /\ y e. RR ) ) -> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. RR )
90 89 ralrimivva 
 |-  ( ph -> A. m e. NN A. y e. RR ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. RR )
91 3 fmpo 
 |-  ( A. m e. NN A. y e. RR ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) e. RR <-> J : ( NN X. RR ) --> RR )
92 90 91 sylib 
 |-  ( ph -> J : ( NN X. RR ) --> RR )
93 fovcdm 
 |-  ( ( J : ( NN X. RR ) --> RR /\ A e. NN /\ x e. RR ) -> ( A J x ) e. RR )
94 92 93 syl3an1 
 |-  ( ( ph /\ A e. NN /\ x e. RR ) -> ( A J x ) e. RR )
95 94 3expa 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( A J x ) e. RR )
96 nnre 
 |-  ( A e. NN -> A e. RR )
97 96 ad2antlr 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> A e. RR )
98 95 97 ifcld 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> if ( ( A J x ) <_ A , ( A J x ) , A ) e. RR )
99 ifcl 
 |-  ( ( if ( ( A J x ) <_ A , ( A J x ) , A ) e. RR /\ 0 e. RR ) -> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) e. RR )
100 98 51 99 sylancl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) e. RR )
101 eqid 
 |-  ( x e. RR |-> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) = ( x e. RR |-> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) )
102 101 fvmpt2 
 |-  ( ( x e. RR /\ if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) e. RR ) -> ( ( x e. RR |-> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) ` x ) = if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) )
103 75 100 102 syl2anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( x e. RR |-> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) ` x ) = if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) )
104 74 103 eqtrd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( G ` A ) ` x ) = if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) )
105 57 62 64 66 69 71 104 ofrfval 
 |-  ( ( ph /\ A e. NN ) -> ( 0p oR <_ ( G ` A ) <-> A. x e. RR 0 <_ if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) )
106 50 105 mpbird 
 |-  ( ( ph /\ A e. NN ) -> 0p oR <_ ( G ` A ) )
107 1 2 3 mbfi1fseqlem1 
 |-  ( ph -> J : ( NN X. RR ) --> ( 0 [,) +oo ) )
108 107 ad2antrr 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> J : ( NN X. RR ) --> ( 0 [,) +oo ) )
109 peano2nn 
 |-  ( A e. NN -> ( A + 1 ) e. NN )
110 109 ad2antlr 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( A + 1 ) e. NN )
111 108 110 75 fovcdmd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( A + 1 ) J x ) e. ( 0 [,) +oo ) )
112 elrege0 
 |-  ( ( ( A + 1 ) J x ) e. ( 0 [,) +oo ) <-> ( ( ( A + 1 ) J x ) e. RR /\ 0 <_ ( ( A + 1 ) J x ) ) )
113 111 112 sylib 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( ( A + 1 ) J x ) e. RR /\ 0 <_ ( ( A + 1 ) J x ) ) )
114 113 simpld 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( A + 1 ) J x ) e. RR )
115 min1 
 |-  ( ( ( A J x ) e. RR /\ A e. RR ) -> if ( ( A J x ) <_ A , ( A J x ) , A ) <_ ( A J x ) )
116 95 97 115 syl2anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> if ( ( A J x ) <_ A , ( A J x ) , A ) <_ ( A J x ) )
117 2cn 
 |-  2 e. CC
118 11 ad2antlr 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> A e. NN0 )
119 expp1 
 |-  ( ( 2 e. CC /\ A e. NN0 ) -> ( 2 ^ ( A + 1 ) ) = ( ( 2 ^ A ) x. 2 ) )
120 117 118 119 sylancr 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 2 ^ ( A + 1 ) ) = ( ( 2 ^ A ) x. 2 ) )
121 120 oveq2d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) x. ( 2 ^ ( A + 1 ) ) ) = ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) x. ( ( 2 ^ A ) x. 2 ) ) )
122 37 95 eqeltrrd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) e. RR )
123 122 recnd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) e. CC )
124 15 recnd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 2 ^ A ) e. CC )
125 2cnd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 2 e. CC )
126 123 124 125 mulassd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) x. ( 2 ^ A ) ) x. 2 ) = ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) x. ( ( 2 ^ A ) x. 2 ) ) )
127 23 recnd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) e. CC )
128 14 nnne0d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 2 ^ A ) =/= 0 )
129 127 124 128 divcan1d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) x. ( 2 ^ A ) ) = ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) )
130 129 oveq1d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) x. ( 2 ^ A ) ) x. 2 ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) x. 2 ) )
131 121 126 130 3eqtr2d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) x. ( 2 ^ ( A + 1 ) ) ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) x. 2 ) )
132 flle 
 |-  ( ( ( F ` x ) x. ( 2 ^ A ) ) e. RR -> ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) <_ ( ( F ` x ) x. ( 2 ^ A ) ) )
133 16 132 syl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) <_ ( ( F ` x ) x. ( 2 ^ A ) ) )
134 2re 
 |-  2 e. RR
135 2pos 
 |-  0 < 2
136 134 135 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
137 136 a1i 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 2 e. RR /\ 0 < 2 ) )
138 lemul1 
 |-  ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) e. RR /\ ( ( F ` x ) x. ( 2 ^ A ) ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) <_ ( ( F ` x ) x. ( 2 ^ A ) ) <-> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) x. 2 ) <_ ( ( ( F ` x ) x. ( 2 ^ A ) ) x. 2 ) ) )
139 23 16 137 138 syl3anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) <_ ( ( F ` x ) x. ( 2 ^ A ) ) <-> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) x. 2 ) <_ ( ( ( F ` x ) x. ( 2 ^ A ) ) x. 2 ) ) )
140 133 139 mpbid 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) x. 2 ) <_ ( ( ( F ` x ) x. ( 2 ^ A ) ) x. 2 ) )
141 120 oveq2d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) = ( ( F ` x ) x. ( ( 2 ^ A ) x. 2 ) ) )
142 9 recnd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( F ` x ) e. CC )
143 142 124 125 mulassd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( ( F ` x ) x. ( 2 ^ A ) ) x. 2 ) = ( ( F ` x ) x. ( ( 2 ^ A ) x. 2 ) ) )
144 141 143 eqtr4d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) = ( ( ( F ` x ) x. ( 2 ^ A ) ) x. 2 ) )
145 140 144 breqtrrd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) x. 2 ) <_ ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) )
146 110 nnnn0d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( A + 1 ) e. NN0 )
147 nnexpcl 
 |-  ( ( 2 e. NN /\ ( A + 1 ) e. NN0 ) -> ( 2 ^ ( A + 1 ) ) e. NN )
148 10 146 147 sylancr 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 2 ^ ( A + 1 ) ) e. NN )
149 148 nnred 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( 2 ^ ( A + 1 ) ) e. RR )
150 9 149 remulcld 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) e. RR )
151 16 flcld 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) e. ZZ )
152 2z 
 |-  2 e. ZZ
153 zmulcl 
 |-  ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) e. ZZ /\ 2 e. ZZ ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) x. 2 ) e. ZZ )
154 151 152 153 sylancl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) x. 2 ) e. ZZ )
155 flge 
 |-  ( ( ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) e. RR /\ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) x. 2 ) e. ZZ ) -> ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) x. 2 ) <_ ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) <-> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) x. 2 ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) ) )
156 150 154 155 syl2anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) x. 2 ) <_ ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) <-> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) x. 2 ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) ) )
157 145 156 mpbid 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) x. 2 ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) )
158 131 157 eqbrtrd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) x. ( 2 ^ ( A + 1 ) ) ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) )
159 reflcl 
 |-  ( ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) e. RR -> ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) e. RR )
160 150 159 syl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) e. RR )
161 148 nngt0d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 < ( 2 ^ ( A + 1 ) ) )
162 lemuldiv 
 |-  ( ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) e. RR /\ ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) e. RR /\ ( ( 2 ^ ( A + 1 ) ) e. RR /\ 0 < ( 2 ^ ( A + 1 ) ) ) ) -> ( ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) x. ( 2 ^ ( A + 1 ) ) ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) <-> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) / ( 2 ^ ( A + 1 ) ) ) ) )
163 122 160 149 161 162 syl112anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) x. ( 2 ^ ( A + 1 ) ) ) <_ ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) <-> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) / ( 2 ^ ( A + 1 ) ) ) ) )
164 158 163 mpbid 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( |_ ` ( ( F ` x ) x. ( 2 ^ A ) ) ) / ( 2 ^ A ) ) <_ ( ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) / ( 2 ^ ( A + 1 ) ) ) )
165 simpr 
 |-  ( ( m = ( A + 1 ) /\ y = x ) -> y = x )
166 165 fveq2d 
 |-  ( ( m = ( A + 1 ) /\ y = x ) -> ( F ` y ) = ( F ` x ) )
167 simpl 
 |-  ( ( m = ( A + 1 ) /\ y = x ) -> m = ( A + 1 ) )
168 167 oveq2d 
 |-  ( ( m = ( A + 1 ) /\ y = x ) -> ( 2 ^ m ) = ( 2 ^ ( A + 1 ) ) )
169 166 168 oveq12d 
 |-  ( ( m = ( A + 1 ) /\ y = x ) -> ( ( F ` y ) x. ( 2 ^ m ) ) = ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) )
170 169 fveq2d 
 |-  ( ( m = ( A + 1 ) /\ y = x ) -> ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) = ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) )
171 170 168 oveq12d 
 |-  ( ( m = ( A + 1 ) /\ y = x ) -> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) / ( 2 ^ ( A + 1 ) ) ) )
172 ovex 
 |-  ( ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) / ( 2 ^ ( A + 1 ) ) ) e. _V
173 171 3 172 ovmpoa 
 |-  ( ( ( A + 1 ) e. NN /\ x e. RR ) -> ( ( A + 1 ) J x ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) / ( 2 ^ ( A + 1 ) ) ) )
174 110 75 173 syl2anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( A + 1 ) J x ) = ( ( |_ ` ( ( F ` x ) x. ( 2 ^ ( A + 1 ) ) ) ) / ( 2 ^ ( A + 1 ) ) ) )
175 164 37 174 3brtr4d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( A J x ) <_ ( ( A + 1 ) J x ) )
176 98 95 114 116 175 letrd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> if ( ( A J x ) <_ A , ( A J x ) , A ) <_ ( ( A + 1 ) J x ) )
177 110 nnred 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( A + 1 ) e. RR )
178 min2 
 |-  ( ( ( A J x ) e. RR /\ A e. RR ) -> if ( ( A J x ) <_ A , ( A J x ) , A ) <_ A )
179 95 97 178 syl2anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> if ( ( A J x ) <_ A , ( A J x ) , A ) <_ A )
180 97 lep1d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> A <_ ( A + 1 ) )
181 98 97 177 179 180 letrd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> if ( ( A J x ) <_ A , ( A J x ) , A ) <_ ( A + 1 ) )
182 breq2 
 |-  ( ( ( A + 1 ) J x ) = if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) -> ( if ( ( A J x ) <_ A , ( A J x ) , A ) <_ ( ( A + 1 ) J x ) <-> if ( ( A J x ) <_ A , ( A J x ) , A ) <_ if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) ) )
183 breq2 
 |-  ( ( A + 1 ) = if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) -> ( if ( ( A J x ) <_ A , ( A J x ) , A ) <_ ( A + 1 ) <-> if ( ( A J x ) <_ A , ( A J x ) , A ) <_ if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) ) )
184 182 183 ifboth 
 |-  ( ( if ( ( A J x ) <_ A , ( A J x ) , A ) <_ ( ( A + 1 ) J x ) /\ if ( ( A J x ) <_ A , ( A J x ) , A ) <_ ( A + 1 ) ) -> if ( ( A J x ) <_ A , ( A J x ) , A ) <_ if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) )
185 176 181 184 syl2anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> if ( ( A J x ) <_ A , ( A J x ) , A ) <_ if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) )
186 185 adantr 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ x e. ( -u A [,] A ) ) -> if ( ( A J x ) <_ A , ( A J x ) , A ) <_ if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) )
187 iftrue 
 |-  ( x e. ( -u A [,] A ) -> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) = if ( ( A J x ) <_ A , ( A J x ) , A ) )
188 187 adantl 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ x e. ( -u A [,] A ) ) -> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) = if ( ( A J x ) <_ A , ( A J x ) , A ) )
189 177 renegcld 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> -u ( A + 1 ) e. RR )
190 97 177 lenegd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( A <_ ( A + 1 ) <-> -u ( A + 1 ) <_ -u A ) )
191 180 190 mpbid 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> -u ( A + 1 ) <_ -u A )
192 iccss 
 |-  ( ( ( -u ( A + 1 ) e. RR /\ ( A + 1 ) e. RR ) /\ ( -u ( A + 1 ) <_ -u A /\ A <_ ( A + 1 ) ) ) -> ( -u A [,] A ) C_ ( -u ( A + 1 ) [,] ( A + 1 ) ) )
193 189 177 191 180 192 syl22anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( -u A [,] A ) C_ ( -u ( A + 1 ) [,] ( A + 1 ) ) )
194 193 sselda 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ x e. ( -u A [,] A ) ) -> x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) )
195 194 iftrued 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ x e. ( -u A [,] A ) ) -> if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) = if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) )
196 186 188 195 3brtr4d 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ x e. ( -u A [,] A ) ) -> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) <_ if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) )
197 iffalse 
 |-  ( -. x e. ( -u A [,] A ) -> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) = 0 )
198 197 adantl 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ -. x e. ( -u A [,] A ) ) -> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) = 0 )
199 113 simprd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 <_ ( ( A + 1 ) J x ) )
200 146 nn0ge0d 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 <_ ( A + 1 ) )
201 breq2 
 |-  ( ( ( A + 1 ) J x ) = if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) -> ( 0 <_ ( ( A + 1 ) J x ) <-> 0 <_ if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) ) )
202 breq2 
 |-  ( ( A + 1 ) = if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) -> ( 0 <_ ( A + 1 ) <-> 0 <_ if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) ) )
203 201 202 ifboth 
 |-  ( ( 0 <_ ( ( A + 1 ) J x ) /\ 0 <_ ( A + 1 ) ) -> 0 <_ if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) )
204 199 200 203 syl2anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 <_ if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) )
205 breq2 
 |-  ( if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) = if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) -> ( 0 <_ if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) <-> 0 <_ if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) ) )
206 breq2 
 |-  ( 0 = if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) -> ( 0 <_ 0 <-> 0 <_ if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) ) )
207 205 206 ifboth 
 |-  ( ( 0 <_ if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) /\ 0 <_ 0 ) -> 0 <_ if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) )
208 204 45 207 sylancl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> 0 <_ if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) )
209 208 adantr 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ -. x e. ( -u A [,] A ) ) -> 0 <_ if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) )
210 198 209 eqbrtrd 
 |-  ( ( ( ( ph /\ A e. NN ) /\ x e. RR ) /\ -. x e. ( -u A [,] A ) ) -> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) <_ if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) )
211 196 210 pm2.61dan 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) <_ if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) )
212 211 ralrimiva 
 |-  ( ( ph /\ A e. NN ) -> A. x e. RR if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) <_ if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) )
213 ffvelcdm 
 |-  ( ( G : NN --> dom S.1 /\ ( A + 1 ) e. NN ) -> ( G ` ( A + 1 ) ) e. dom S.1 )
214 58 109 213 syl2an 
 |-  ( ( ph /\ A e. NN ) -> ( G ` ( A + 1 ) ) e. dom S.1 )
215 i1ff 
 |-  ( ( G ` ( A + 1 ) ) e. dom S.1 -> ( G ` ( A + 1 ) ) : RR --> RR )
216 ffn 
 |-  ( ( G ` ( A + 1 ) ) : RR --> RR -> ( G ` ( A + 1 ) ) Fn RR )
217 214 215 216 3syl 
 |-  ( ( ph /\ A e. NN ) -> ( G ` ( A + 1 ) ) Fn RR )
218 inidm 
 |-  ( RR i^i RR ) = RR
219 1 2 3 4 mbfi1fseqlem2 
 |-  ( ( A + 1 ) e. NN -> ( G ` ( A + 1 ) ) = ( x e. RR |-> if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) ) )
220 219 fveq1d 
 |-  ( ( A + 1 ) e. NN -> ( ( G ` ( A + 1 ) ) ` x ) = ( ( x e. RR |-> if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) ) ` x ) )
221 110 220 syl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( G ` ( A + 1 ) ) ` x ) = ( ( x e. RR |-> if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) ) ` x ) )
222 114 177 ifcld 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) e. RR )
223 ifcl 
 |-  ( ( if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) e. RR /\ 0 e. RR ) -> if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) e. RR )
224 222 51 223 sylancl 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) e. RR )
225 eqid 
 |-  ( x e. RR |-> if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) ) = ( x e. RR |-> if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) )
226 225 fvmpt2 
 |-  ( ( x e. RR /\ if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) e. RR ) -> ( ( x e. RR |-> if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) ) ` x ) = if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) )
227 75 224 226 syl2anc 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( x e. RR |-> if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) ) ` x ) = if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) )
228 221 227 eqtrd 
 |-  ( ( ( ph /\ A e. NN ) /\ x e. RR ) -> ( ( G ` ( A + 1 ) ) ` x ) = if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) )
229 62 217 66 66 218 104 228 ofrfval 
 |-  ( ( ph /\ A e. NN ) -> ( ( G ` A ) oR <_ ( G ` ( A + 1 ) ) <-> A. x e. RR if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) <_ if ( x e. ( -u ( A + 1 ) [,] ( A + 1 ) ) , if ( ( ( A + 1 ) J x ) <_ ( A + 1 ) , ( ( A + 1 ) J x ) , ( A + 1 ) ) , 0 ) ) )
230 212 229 mpbird 
 |-  ( ( ph /\ A e. NN ) -> ( G ` A ) oR <_ ( G ` ( A + 1 ) ) )
231 106 230 jca 
 |-  ( ( ph /\ A e. NN ) -> ( 0p oR <_ ( G ` A ) /\ ( G ` A ) oR <_ ( G ` ( A + 1 ) ) ) )