Metamath Proof Explorer

Theorem dvfsumlem3

Description: Lemma for dvfsumrlim . (Contributed by Mario Carneiro, 17-May-2016)

Ref Expression
Hypotheses dvfsum.s 
|- S = ( T (,) +oo )
dvfsum.z 
|- Z = ( ZZ>= ` M )
dvfsum.m 
|- ( ph -> M e. ZZ )
dvfsum.d 
|- ( ph -> D e. RR )
dvfsum.md 
|- ( ph -> M <_ ( D + 1 ) )
dvfsum.t 
|- ( ph -> T e. RR )
dvfsum.a 
|- ( ( ph /\ x e. S ) -> A e. RR )
dvfsum.b1 
|- ( ( ph /\ x e. S ) -> B e. V )
dvfsum.b2 
|- ( ( ph /\ x e. Z ) -> B e. RR )
dvfsum.b3 
|- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
dvfsum.c 
|- ( x = k -> B = C )
dvfsum.u 
|- ( ph -> U e. RR* )
dvfsum.l 
|- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B )
dvfsum.h 
|- H = ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) )
dvfsumlem1.1 
|- ( ph -> X e. S )
dvfsumlem1.2 
|- ( ph -> Y e. S )
dvfsumlem1.3 
|- ( ph -> D <_ X )
dvfsumlem1.4 
|- ( ph -> X <_ Y )
dvfsumlem1.5 
|- ( ph -> Y <_ U )
Assertion dvfsumlem3 
|- ( ph -> ( ( H ` Y ) <_ ( H ` X ) /\ ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) ) )

Proof

Step Hyp Ref Expression
1 dvfsum.s 
 |-  S = ( T (,) +oo )
2 dvfsum.z 
 |-  Z = ( ZZ>= ` M )
3 dvfsum.m 
 |-  ( ph -> M e. ZZ )
4 dvfsum.d 
 |-  ( ph -> D e. RR )
5 dvfsum.md 
 |-  ( ph -> M <_ ( D + 1 ) )
6 dvfsum.t 
 |-  ( ph -> T e. RR )
7 dvfsum.a 
 |-  ( ( ph /\ x e. S ) -> A e. RR )
8 dvfsum.b1 
 |-  ( ( ph /\ x e. S ) -> B e. V )
9 dvfsum.b2 
 |-  ( ( ph /\ x e. Z ) -> B e. RR )
10 dvfsum.b3 
 |-  ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
11 dvfsum.c 
 |-  ( x = k -> B = C )
12 dvfsum.u 
 |-  ( ph -> U e. RR* )
13 dvfsum.l 
 |-  ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B )
14 dvfsum.h 
 |-  H = ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) )
15 dvfsumlem1.1 
 |-  ( ph -> X e. S )
16 dvfsumlem1.2 
 |-  ( ph -> Y e. S )
17 dvfsumlem1.3 
 |-  ( ph -> D <_ X )
18 dvfsumlem1.4 
 |-  ( ph -> X <_ Y )
19 dvfsumlem1.5 
 |-  ( ph -> Y <_ U )
20 ioossre 
 |-  ( T (,) +oo ) C_ RR
21 1 20 eqsstri 
 |-  S C_ RR
22 21 16 sselid 
 |-  ( ph -> Y e. RR )
23 21 15 sselid 
 |-  ( ph -> X e. RR )
24 reflcl 
 |-  ( X e. RR -> ( |_ ` X ) e. RR )
25 peano2re 
 |-  ( ( |_ ` X ) e. RR -> ( ( |_ ` X ) + 1 ) e. RR )
26 23 24 25 3syl 
 |-  ( ph -> ( ( |_ ` X ) + 1 ) e. RR )
27 3 adantr 
 |-  ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) -> M e. ZZ )
28 4 adantr 
 |-  ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) -> D e. RR )
29 5 adantr 
 |-  ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) -> M <_ ( D + 1 ) )
30 6 adantr 
 |-  ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) -> T e. RR )
31 7 adantlr 
 |-  ( ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) /\ x e. S ) -> A e. RR )
32 8 adantlr 
 |-  ( ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) /\ x e. S ) -> B e. V )
33 9 adantlr 
 |-  ( ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) /\ x e. Z ) -> B e. RR )
34 10 adantr 
 |-  ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
35 12 adantr 
 |-  ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) -> U e. RR* )
36 13 3adant1r 
 |-  ( ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B )
37 15 adantr 
 |-  ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) -> X e. S )
38 16 adantr 
 |-  ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) -> Y e. S )
39 17 adantr 
 |-  ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) -> D <_ X )
40 18 adantr 
 |-  ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) -> X <_ Y )
41 19 adantr 
 |-  ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) -> Y <_ U )
42 simpr 
 |-  ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) -> Y <_ ( ( |_ ` X ) + 1 ) )
43 1 2 27 28 29 30 31 32 33 34 11 35 36 14 37 38 39 40 41 42 dvfsumlem2 
 |-  ( ( ph /\ Y <_ ( ( |_ ` X ) + 1 ) ) -> ( ( H ` Y ) <_ ( H ` X ) /\ ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) ) )
44 21 a1i 
 |-  ( ph -> S C_ RR )
45 44 sselda 
 |-  ( ( ph /\ x e. S ) -> x e. RR )
46 reflcl 
 |-  ( x e. RR -> ( |_ ` x ) e. RR )
47 45 46 syl 
 |-  ( ( ph /\ x e. S ) -> ( |_ ` x ) e. RR )
48 45 47 resubcld 
 |-  ( ( ph /\ x e. S ) -> ( x - ( |_ ` x ) ) e. RR )
49 44 7 8 10 dvmptrecl 
 |-  ( ( ph /\ x e. S ) -> B e. RR )
50 48 49 remulcld 
 |-  ( ( ph /\ x e. S ) -> ( ( x - ( |_ ` x ) ) x. B ) e. RR )
51 fzfid 
 |-  ( ( ph /\ x e. S ) -> ( M ... ( |_ ` x ) ) e. Fin )
52 9 ralrimiva 
 |-  ( ph -> A. x e. Z B e. RR )
53 52 adantr 
 |-  ( ( ph /\ x e. S ) -> A. x e. Z B e. RR )
54 elfzuz 
 |-  ( k e. ( M ... ( |_ ` x ) ) -> k e. ( ZZ>= ` M ) )
55 54 2 eleqtrrdi 
 |-  ( k e. ( M ... ( |_ ` x ) ) -> k e. Z )
56 11 eleq1d 
 |-  ( x = k -> ( B e. RR <-> C e. RR ) )
57 56 rspccva 
 |-  ( ( A. x e. Z B e. RR /\ k e. Z ) -> C e. RR )
58 53 55 57 syl2an 
 |-  ( ( ( ph /\ x e. S ) /\ k e. ( M ... ( |_ ` x ) ) ) -> C e. RR )
59 51 58 fsumrecl 
 |-  ( ( ph /\ x e. S ) -> sum_ k e. ( M ... ( |_ ` x ) ) C e. RR )
60 59 7 resubcld 
 |-  ( ( ph /\ x e. S ) -> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) e. RR )
61 50 60 readdcld 
 |-  ( ( ph /\ x e. S ) -> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) e. RR )
62 61 14 fmptd 
 |-  ( ph -> H : S --> RR )
63 62 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> H : S --> RR )
64 16 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> Y e. S )
65 63 64 ffvelrnd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( H ` Y ) e. RR )
66 22 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> Y e. RR )
67 reflcl 
 |-  ( Y e. RR -> ( |_ ` Y ) e. RR )
68 66 67 syl 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( |_ ` Y ) e. RR )
69 6 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> T e. RR )
70 23 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> X e. RR )
71 70 24 25 3syl 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( |_ ` X ) + 1 ) e. RR )
72 15 1 eleqtrdi 
 |-  ( ph -> X e. ( T (,) +oo ) )
73 6 rexrd 
 |-  ( ph -> T e. RR* )
74 elioopnf 
 |-  ( T e. RR* -> ( X e. ( T (,) +oo ) <-> ( X e. RR /\ T < X ) ) )
75 73 74 syl 
 |-  ( ph -> ( X e. ( T (,) +oo ) <-> ( X e. RR /\ T < X ) ) )
76 72 75 mpbid 
 |-  ( ph -> ( X e. RR /\ T < X ) )
77 76 simprd 
 |-  ( ph -> T < X )
78 fllep1 
 |-  ( X e. RR -> X <_ ( ( |_ ` X ) + 1 ) )
79 23 78 syl 
 |-  ( ph -> X <_ ( ( |_ ` X ) + 1 ) )
80 6 23 26 77 79 ltletrd 
 |-  ( ph -> T < ( ( |_ ` X ) + 1 ) )
81 80 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> T < ( ( |_ ` X ) + 1 ) )
82 simpr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( |_ ` X ) + 1 ) <_ Y )
83 70 flcld 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( |_ ` X ) e. ZZ )
84 83 peano2zd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( |_ ` X ) + 1 ) e. ZZ )
85 flge 
 |-  ( ( Y e. RR /\ ( ( |_ ` X ) + 1 ) e. ZZ ) -> ( ( ( |_ ` X ) + 1 ) <_ Y <-> ( ( |_ ` X ) + 1 ) <_ ( |_ ` Y ) ) )
86 66 84 85 syl2anc 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( ( |_ ` X ) + 1 ) <_ Y <-> ( ( |_ ` X ) + 1 ) <_ ( |_ ` Y ) ) )
87 82 86 mpbid 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( |_ ` X ) + 1 ) <_ ( |_ ` Y ) )
88 69 71 68 81 87 ltletrd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> T < ( |_ ` Y ) )
89 73 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> T e. RR* )
90 elioopnf 
 |-  ( T e. RR* -> ( ( |_ ` Y ) e. ( T (,) +oo ) <-> ( ( |_ ` Y ) e. RR /\ T < ( |_ ` Y ) ) ) )
91 89 90 syl 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( |_ ` Y ) e. ( T (,) +oo ) <-> ( ( |_ ` Y ) e. RR /\ T < ( |_ ` Y ) ) ) )
92 68 88 91 mpbir2and 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( |_ ` Y ) e. ( T (,) +oo ) )
93 92 1 eleqtrrdi 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( |_ ` Y ) e. S )
94 63 93 ffvelrnd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( H ` ( |_ ` Y ) ) e. RR )
95 15 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> X e. S )
96 63 95 ffvelrnd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( H ` X ) e. RR )
97 3 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> M e. ZZ )
98 4 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> D e. RR )
99 5 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> M <_ ( D + 1 ) )
100 7 adantlr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ x e. S ) -> A e. RR )
101 8 adantlr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ x e. S ) -> B e. V )
102 9 adantlr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ x e. Z ) -> B e. RR )
103 10 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
104 12 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> U e. RR* )
105 13 3adant1r 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B )
106 17 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> D <_ X )
107 70 78 syl 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> X <_ ( ( |_ ` X ) + 1 ) )
108 98 70 71 106 107 letrd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> D <_ ( ( |_ ` X ) + 1 ) )
109 98 71 68 108 87 letrd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> D <_ ( |_ ` Y ) )
110 flle 
 |-  ( Y e. RR -> ( |_ ` Y ) <_ Y )
111 66 110 syl 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( |_ ` Y ) <_ Y )
112 19 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> Y <_ U )
113 fllep1 
 |-  ( Y e. RR -> Y <_ ( ( |_ ` Y ) + 1 ) )
114 66 113 syl 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> Y <_ ( ( |_ ` Y ) + 1 ) )
115 flidm 
 |-  ( Y e. RR -> ( |_ ` ( |_ ` Y ) ) = ( |_ ` Y ) )
116 66 115 syl 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( |_ ` ( |_ ` Y ) ) = ( |_ ` Y ) )
117 116 oveq1d 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( |_ ` ( |_ ` Y ) ) + 1 ) = ( ( |_ ` Y ) + 1 ) )
118 114 117 breqtrrd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> Y <_ ( ( |_ ` ( |_ ` Y ) ) + 1 ) )
119 1 2 97 98 99 69 100 101 102 103 11 104 105 14 93 64 109 111 112 118 dvfsumlem2 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( H ` Y ) <_ ( H ` ( |_ ` Y ) ) /\ ( ( H ` ( |_ ` Y ) ) - [_ ( |_ ` Y ) / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) ) )
120 119 simpld 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( H ` Y ) <_ ( H ` ( |_ ` Y ) ) )
121 elioopnf 
 |-  ( T e. RR* -> ( ( ( |_ ` X ) + 1 ) e. ( T (,) +oo ) <-> ( ( ( |_ ` X ) + 1 ) e. RR /\ T < ( ( |_ ` X ) + 1 ) ) ) )
122 73 121 syl 
 |-  ( ph -> ( ( ( |_ ` X ) + 1 ) e. ( T (,) +oo ) <-> ( ( ( |_ ` X ) + 1 ) e. RR /\ T < ( ( |_ ` X ) + 1 ) ) ) )
123 26 80 122 mpbir2and 
 |-  ( ph -> ( ( |_ ` X ) + 1 ) e. ( T (,) +oo ) )
124 123 1 eleqtrrdi 
 |-  ( ph -> ( ( |_ ` X ) + 1 ) e. S )
125 124 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( |_ ` X ) + 1 ) e. S )
126 63 125 ffvelrnd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( H ` ( ( |_ ` X ) + 1 ) ) e. RR )
127 66 flcld 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( |_ ` Y ) e. ZZ )
128 eluz2 
 |-  ( ( |_ ` Y ) e. ( ZZ>= ` ( ( |_ ` X ) + 1 ) ) <-> ( ( ( |_ ` X ) + 1 ) e. ZZ /\ ( |_ ` Y ) e. ZZ /\ ( ( |_ ` X ) + 1 ) <_ ( |_ ` Y ) ) )
129 84 127 87 128 syl3anbrc 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( |_ ` Y ) e. ( ZZ>= ` ( ( |_ ` X ) + 1 ) ) )
130 63 adantr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> H : S --> RR )
131 elfzelz 
 |-  ( m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) -> m e. ZZ )
132 131 adantl 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> m e. ZZ )
133 132 zred 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> m e. RR )
134 69 adantr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> T e. RR )
135 71 adantr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> ( ( |_ ` X ) + 1 ) e. RR )
136 80 ad2antrr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> T < ( ( |_ ` X ) + 1 ) )
137 elfzle1 
 |-  ( m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) -> ( ( |_ ` X ) + 1 ) <_ m )
138 137 adantl 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> ( ( |_ ` X ) + 1 ) <_ m )
139 134 135 133 136 138 ltletrd 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> T < m )
140 73 ad2antrr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> T e. RR* )
141 elioopnf 
 |-  ( T e. RR* -> ( m e. ( T (,) +oo ) <-> ( m e. RR /\ T < m ) ) )
142 140 141 syl 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> ( m e. ( T (,) +oo ) <-> ( m e. RR /\ T < m ) ) )
143 133 139 142 mpbir2and 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> m e. ( T (,) +oo ) )
144 143 1 eleqtrrdi 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> m e. S )
145 130 144 ffvelrnd 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> ( H ` m ) e. RR )
146 97 adantr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> M e. ZZ )
147 98 adantr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> D e. RR )
148 5 ad2antrr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> M <_ ( D + 1 ) )
149 69 adantr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> T e. RR )
150 100 adantlr 
 |-  ( ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) /\ x e. S ) -> A e. RR )
151 101 adantlr 
 |-  ( ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) /\ x e. S ) -> B e. V )
152 102 adantlr 
 |-  ( ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) /\ x e. Z ) -> B e. RR )
153 103 adantr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
154 104 adantr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> U e. RR* )
155 105 3adant1r 
 |-  ( ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B )
156 elfzelz 
 |-  ( m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) -> m e. ZZ )
157 156 adantl 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> m e. ZZ )
158 157 zred 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> m e. RR )
159 71 adantr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( ( |_ ` X ) + 1 ) e. RR )
160 80 ad2antrr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> T < ( ( |_ ` X ) + 1 ) )
161 elfzle1 
 |-  ( m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) -> ( ( |_ ` X ) + 1 ) <_ m )
162 161 adantl 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( ( |_ ` X ) + 1 ) <_ m )
163 149 159 158 160 162 ltletrd 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> T < m )
164 149 rexrd 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> T e. RR* )
165 164 141 syl 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( m e. ( T (,) +oo ) <-> ( m e. RR /\ T < m ) ) )
166 158 163 165 mpbir2and 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> m e. ( T (,) +oo ) )
167 166 1 eleqtrrdi 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> m e. S )
168 peano2re 
 |-  ( m e. RR -> ( m + 1 ) e. RR )
169 158 168 syl 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( m + 1 ) e. RR )
170 158 lep1d 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> m <_ ( m + 1 ) )
171 149 158 169 163 170 ltletrd 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> T < ( m + 1 ) )
172 elioopnf 
 |-  ( T e. RR* -> ( ( m + 1 ) e. ( T (,) +oo ) <-> ( ( m + 1 ) e. RR /\ T < ( m + 1 ) ) ) )
173 164 172 syl 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( ( m + 1 ) e. ( T (,) +oo ) <-> ( ( m + 1 ) e. RR /\ T < ( m + 1 ) ) ) )
174 169 171 173 mpbir2and 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( m + 1 ) e. ( T (,) +oo ) )
175 174 1 eleqtrrdi 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( m + 1 ) e. S )
176 108 adantr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> D <_ ( ( |_ ` X ) + 1 ) )
177 147 159 158 176 162 letrd 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> D <_ m )
178 169 rexrd 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( m + 1 ) e. RR* )
179 68 rexrd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( |_ ` Y ) e. RR* )
180 179 adantr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( |_ ` Y ) e. RR* )
181 elfzle2 
 |-  ( m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) -> m <_ ( ( |_ ` Y ) - 1 ) )
182 181 adantl 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> m <_ ( ( |_ ` Y ) - 1 ) )
183 1red 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> 1 e. RR )
184 66 adantr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> Y e. RR )
185 184 67 syl 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( |_ ` Y ) e. RR )
186 leaddsub 
 |-  ( ( m e. RR /\ 1 e. RR /\ ( |_ ` Y ) e. RR ) -> ( ( m + 1 ) <_ ( |_ ` Y ) <-> m <_ ( ( |_ ` Y ) - 1 ) ) )
187 158 183 185 186 syl3anc 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( ( m + 1 ) <_ ( |_ ` Y ) <-> m <_ ( ( |_ ` Y ) - 1 ) ) )
188 182 187 mpbird 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( m + 1 ) <_ ( |_ ` Y ) )
189 66 rexrd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> Y e. RR* )
190 179 189 104 111 112 xrletrd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( |_ ` Y ) <_ U )
191 190 adantr 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( |_ ` Y ) <_ U )
192 178 180 154 188 191 xrletrd 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( m + 1 ) <_ U )
193 flid 
 |-  ( m e. ZZ -> ( |_ ` m ) = m )
194 157 193 syl 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( |_ ` m ) = m )
195 194 eqcomd 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> m = ( |_ ` m ) )
196 195 oveq1d 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( m + 1 ) = ( ( |_ ` m ) + 1 ) )
197 169 196 eqled 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( m + 1 ) <_ ( ( |_ ` m ) + 1 ) )
198 1 2 146 147 148 149 150 151 152 153 11 154 155 14 167 175 177 170 192 197 dvfsumlem2 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( ( H ` ( m + 1 ) ) <_ ( H ` m ) /\ ( ( H ` m ) - [_ m / x ]_ B ) <_ ( ( H ` ( m + 1 ) ) - [_ ( m + 1 ) / x ]_ B ) ) )
199 198 simpld 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( H ` ( m + 1 ) ) <_ ( H ` m ) )
200 129 145 199 monoord2 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( H ` ( |_ ` Y ) ) <_ ( H ` ( ( |_ ` X ) + 1 ) ) )
201 71 rexrd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( |_ ` X ) + 1 ) e. RR* )
202 201 179 104 87 190 xrletrd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( |_ ` X ) + 1 ) <_ U )
203 71 leidd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( |_ ` X ) + 1 ) <_ ( ( |_ ` X ) + 1 ) )
204 1 2 97 98 99 69 100 101 102 103 11 104 105 14 95 125 106 107 202 203 dvfsumlem2 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( H ` ( ( |_ ` X ) + 1 ) ) <_ ( H ` X ) /\ ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` ( ( |_ ` X ) + 1 ) ) - [_ ( ( |_ ` X ) + 1 ) / x ]_ B ) ) )
205 204 simpld 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( H ` ( ( |_ ` X ) + 1 ) ) <_ ( H ` X ) )
206 94 126 96 200 205 letrd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( H ` ( |_ ` Y ) ) <_ ( H ` X ) )
207 65 94 96 120 206 letrd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( H ` Y ) <_ ( H ` X ) )
208 csbeq1 
 |-  ( m = X -> [_ m / x ]_ B = [_ X / x ]_ B )
209 208 eleq1d 
 |-  ( m = X -> ( [_ m / x ]_ B e. RR <-> [_ X / x ]_ B e. RR ) )
210 49 ralrimiva 
 |-  ( ph -> A. x e. S B e. RR )
211 210 adantr 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> A. x e. S B e. RR )
212 nfcsb1v 
 |-  F/_ x [_ m / x ]_ B
213 212 nfel1 
 |-  F/ x [_ m / x ]_ B e. RR
214 csbeq1a 
 |-  ( x = m -> B = [_ m / x ]_ B )
215 214 eleq1d 
 |-  ( x = m -> ( B e. RR <-> [_ m / x ]_ B e. RR ) )
216 213 215 rspc 
 |-  ( m e. S -> ( A. x e. S B e. RR -> [_ m / x ]_ B e. RR ) )
217 211 216 mpan9 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. S ) -> [_ m / x ]_ B e. RR )
218 217 ralrimiva 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> A. m e. S [_ m / x ]_ B e. RR )
219 209 218 95 rspcdva 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> [_ X / x ]_ B e. RR )
220 96 219 resubcld 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( H ` X ) - [_ X / x ]_ B ) e. RR )
221 csbeq1 
 |-  ( m = ( |_ ` Y ) -> [_ m / x ]_ B = [_ ( |_ ` Y ) / x ]_ B )
222 221 eleq1d 
 |-  ( m = ( |_ ` Y ) -> ( [_ m / x ]_ B e. RR <-> [_ ( |_ ` Y ) / x ]_ B e. RR ) )
223 222 218 93 rspcdva 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> [_ ( |_ ` Y ) / x ]_ B e. RR )
224 94 223 resubcld 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( H ` ( |_ ` Y ) ) - [_ ( |_ ` Y ) / x ]_ B ) e. RR )
225 csbeq1 
 |-  ( m = Y -> [_ m / x ]_ B = [_ Y / x ]_ B )
226 225 eleq1d 
 |-  ( m = Y -> ( [_ m / x ]_ B e. RR <-> [_ Y / x ]_ B e. RR ) )
227 226 218 64 rspcdva 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> [_ Y / x ]_ B e. RR )
228 65 227 resubcld 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( H ` Y ) - [_ Y / x ]_ B ) e. RR )
229 csbeq1 
 |-  ( m = ( ( |_ ` X ) + 1 ) -> [_ m / x ]_ B = [_ ( ( |_ ` X ) + 1 ) / x ]_ B )
230 229 eleq1d 
 |-  ( m = ( ( |_ ` X ) + 1 ) -> ( [_ m / x ]_ B e. RR <-> [_ ( ( |_ ` X ) + 1 ) / x ]_ B e. RR ) )
231 230 218 125 rspcdva 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> [_ ( ( |_ ` X ) + 1 ) / x ]_ B e. RR )
232 126 231 resubcld 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( H ` ( ( |_ ` X ) + 1 ) ) - [_ ( ( |_ ` X ) + 1 ) / x ]_ B ) e. RR )
233 204 simprd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` ( ( |_ ` X ) + 1 ) ) - [_ ( ( |_ ` X ) + 1 ) / x ]_ B ) )
234 fveq2 
 |-  ( y = m -> ( H ` y ) = ( H ` m ) )
235 csbeq1 
 |-  ( y = m -> [_ y / x ]_ B = [_ m / x ]_ B )
236 234 235 oveq12d 
 |-  ( y = m -> ( ( H ` y ) - [_ y / x ]_ B ) = ( ( H ` m ) - [_ m / x ]_ B ) )
237 eqid 
 |-  ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) ) = ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) )
238 ovex 
 |-  ( ( H ` y ) - [_ y / x ]_ B ) e. _V
239 236 237 238 fvmpt3i 
 |-  ( m e. _V -> ( ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) ) ` m ) = ( ( H ` m ) - [_ m / x ]_ B ) )
240 239 elv 
 |-  ( ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) ) ` m ) = ( ( H ` m ) - [_ m / x ]_ B )
241 144 217 syldan 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> [_ m / x ]_ B e. RR )
242 145 241 resubcld 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> ( ( H ` m ) - [_ m / x ]_ B ) e. RR )
243 240 242 eqeltrid 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( |_ ` Y ) ) ) -> ( ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) ) ` m ) e. RR )
244 198 simprd 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( ( H ` m ) - [_ m / x ]_ B ) <_ ( ( H ` ( m + 1 ) ) - [_ ( m + 1 ) / x ]_ B ) )
245 ovex 
 |-  ( m + 1 ) e. _V
246 fveq2 
 |-  ( y = ( m + 1 ) -> ( H ` y ) = ( H ` ( m + 1 ) ) )
247 csbeq1 
 |-  ( y = ( m + 1 ) -> [_ y / x ]_ B = [_ ( m + 1 ) / x ]_ B )
248 246 247 oveq12d 
 |-  ( y = ( m + 1 ) -> ( ( H ` y ) - [_ y / x ]_ B ) = ( ( H ` ( m + 1 ) ) - [_ ( m + 1 ) / x ]_ B ) )
249 248 237 238 fvmpt3i 
 |-  ( ( m + 1 ) e. _V -> ( ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) ) ` ( m + 1 ) ) = ( ( H ` ( m + 1 ) ) - [_ ( m + 1 ) / x ]_ B ) )
250 245 249 ax-mp 
 |-  ( ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) ) ` ( m + 1 ) ) = ( ( H ` ( m + 1 ) ) - [_ ( m + 1 ) / x ]_ B )
251 244 240 250 3brtr4g 
 |-  ( ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) /\ m e. ( ( ( |_ ` X ) + 1 ) ... ( ( |_ ` Y ) - 1 ) ) ) -> ( ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) ) ` m ) <_ ( ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) ) ` ( m + 1 ) ) )
252 129 243 251 monoord 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) ) ` ( ( |_ ` X ) + 1 ) ) <_ ( ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) ) ` ( |_ ` Y ) ) )
253 ovex 
 |-  ( ( |_ ` X ) + 1 ) e. _V
254 fveq2 
 |-  ( y = ( ( |_ ` X ) + 1 ) -> ( H ` y ) = ( H ` ( ( |_ ` X ) + 1 ) ) )
255 csbeq1 
 |-  ( y = ( ( |_ ` X ) + 1 ) -> [_ y / x ]_ B = [_ ( ( |_ ` X ) + 1 ) / x ]_ B )
256 254 255 oveq12d 
 |-  ( y = ( ( |_ ` X ) + 1 ) -> ( ( H ` y ) - [_ y / x ]_ B ) = ( ( H ` ( ( |_ ` X ) + 1 ) ) - [_ ( ( |_ ` X ) + 1 ) / x ]_ B ) )
257 256 237 238 fvmpt3i 
 |-  ( ( ( |_ ` X ) + 1 ) e. _V -> ( ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) ) ` ( ( |_ ` X ) + 1 ) ) = ( ( H ` ( ( |_ ` X ) + 1 ) ) - [_ ( ( |_ ` X ) + 1 ) / x ]_ B ) )
258 253 257 ax-mp 
 |-  ( ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) ) ` ( ( |_ ` X ) + 1 ) ) = ( ( H ` ( ( |_ ` X ) + 1 ) ) - [_ ( ( |_ ` X ) + 1 ) / x ]_ B )
259 fvex 
 |-  ( |_ ` Y ) e. _V
260 fveq2 
 |-  ( y = ( |_ ` Y ) -> ( H ` y ) = ( H ` ( |_ ` Y ) ) )
261 csbeq1 
 |-  ( y = ( |_ ` Y ) -> [_ y / x ]_ B = [_ ( |_ ` Y ) / x ]_ B )
262 260 261 oveq12d 
 |-  ( y = ( |_ ` Y ) -> ( ( H ` y ) - [_ y / x ]_ B ) = ( ( H ` ( |_ ` Y ) ) - [_ ( |_ ` Y ) / x ]_ B ) )
263 262 237 238 fvmpt3i 
 |-  ( ( |_ ` Y ) e. _V -> ( ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) ) ` ( |_ ` Y ) ) = ( ( H ` ( |_ ` Y ) ) - [_ ( |_ ` Y ) / x ]_ B ) )
264 259 263 ax-mp 
 |-  ( ( y e. _V |-> ( ( H ` y ) - [_ y / x ]_ B ) ) ` ( |_ ` Y ) ) = ( ( H ` ( |_ ` Y ) ) - [_ ( |_ ` Y ) / x ]_ B )
265 252 258 264 3brtr3g 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( H ` ( ( |_ ` X ) + 1 ) ) - [_ ( ( |_ ` X ) + 1 ) / x ]_ B ) <_ ( ( H ` ( |_ ` Y ) ) - [_ ( |_ ` Y ) / x ]_ B ) )
266 220 232 224 233 265 letrd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` ( |_ ` Y ) ) - [_ ( |_ ` Y ) / x ]_ B ) )
267 119 simprd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( H ` ( |_ ` Y ) ) - [_ ( |_ ` Y ) / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) )
268 220 224 228 266 267 letrd 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) )
269 207 268 jca 
 |-  ( ( ph /\ ( ( |_ ` X ) + 1 ) <_ Y ) -> ( ( H ` Y ) <_ ( H ` X ) /\ ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) ) )
270 22 26 43 269 lecasei 
 |-  ( ph -> ( ( H ` Y ) <_ ( H ` X ) /\ ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) ) )