Metamath Proof Explorer


Theorem fourierdlem42

Description: The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 29-Sep-2020)

Ref Expression
Hypotheses fourierdlem42.b
|- ( ph -> B e. RR )
fourierdlem42.c
|- ( ph -> C e. RR )
fourierdlem42.bc
|- ( ph -> B < C )
fourierdlem42.t
|- T = ( C - B )
fourierdlem42.a
|- ( ph -> A C_ ( B [,] C ) )
fourierdlem42.af
|- ( ph -> A e. Fin )
fourierdlem42.ba
|- ( ph -> B e. A )
fourierdlem42.ca
|- ( ph -> C e. A )
fourierdlem42.d
|- D = ( abs o. - )
fourierdlem42.i
|- I = ( ( A X. A ) \ _I )
fourierdlem42.r
|- R = ran ( D |` I )
fourierdlem42.e
|- E = inf ( R , RR , < )
fourierdlem42.x
|- ( ph -> X e. RR )
fourierdlem42.y
|- ( ph -> Y e. RR )
fourierdlem42.j
|- J = ( topGen ` ran (,) )
fourierdlem42.k
|- K = ( J |`t ( X [,] Y ) )
fourierdlem42.h
|- H = { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A }
fourierdlem42.15
|- ( ps <-> ( ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) )
Assertion fourierdlem42
|- ( ph -> H e. Fin )

Proof

Step Hyp Ref Expression
1 fourierdlem42.b
 |-  ( ph -> B e. RR )
2 fourierdlem42.c
 |-  ( ph -> C e. RR )
3 fourierdlem42.bc
 |-  ( ph -> B < C )
4 fourierdlem42.t
 |-  T = ( C - B )
5 fourierdlem42.a
 |-  ( ph -> A C_ ( B [,] C ) )
6 fourierdlem42.af
 |-  ( ph -> A e. Fin )
7 fourierdlem42.ba
 |-  ( ph -> B e. A )
8 fourierdlem42.ca
 |-  ( ph -> C e. A )
9 fourierdlem42.d
 |-  D = ( abs o. - )
10 fourierdlem42.i
 |-  I = ( ( A X. A ) \ _I )
11 fourierdlem42.r
 |-  R = ran ( D |` I )
12 fourierdlem42.e
 |-  E = inf ( R , RR , < )
13 fourierdlem42.x
 |-  ( ph -> X e. RR )
14 fourierdlem42.y
 |-  ( ph -> Y e. RR )
15 fourierdlem42.j
 |-  J = ( topGen ` ran (,) )
16 fourierdlem42.k
 |-  K = ( J |`t ( X [,] Y ) )
17 fourierdlem42.h
 |-  H = { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A }
18 fourierdlem42.15
 |-  ( ps <-> ( ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) )
19 15 16 icccmp
 |-  ( ( X e. RR /\ Y e. RR ) -> K e. Comp )
20 13 14 19 syl2anc
 |-  ( ph -> K e. Comp )
21 20 adantr
 |-  ( ( ph /\ -. H e. Fin ) -> K e. Comp )
22 ssrab2
 |-  { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } C_ ( X [,] Y )
23 22 a1i
 |-  ( ph -> { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } C_ ( X [,] Y ) )
24 17 23 eqsstrid
 |-  ( ph -> H C_ ( X [,] Y ) )
25 retop
 |-  ( topGen ` ran (,) ) e. Top
26 15 25 eqeltri
 |-  J e. Top
27 13 14 iccssred
 |-  ( ph -> ( X [,] Y ) C_ RR )
28 uniretop
 |-  RR = U. ( topGen ` ran (,) )
29 15 unieqi
 |-  U. J = U. ( topGen ` ran (,) )
30 28 29 eqtr4i
 |-  RR = U. J
31 30 restuni
 |-  ( ( J e. Top /\ ( X [,] Y ) C_ RR ) -> ( X [,] Y ) = U. ( J |`t ( X [,] Y ) ) )
32 26 27 31 sylancr
 |-  ( ph -> ( X [,] Y ) = U. ( J |`t ( X [,] Y ) ) )
33 16 unieqi
 |-  U. K = U. ( J |`t ( X [,] Y ) )
34 33 eqcomi
 |-  U. ( J |`t ( X [,] Y ) ) = U. K
35 32 34 eqtrdi
 |-  ( ph -> ( X [,] Y ) = U. K )
36 24 35 sseqtrd
 |-  ( ph -> H C_ U. K )
37 36 adantr
 |-  ( ( ph /\ -. H e. Fin ) -> H C_ U. K )
38 simpr
 |-  ( ( ph /\ -. H e. Fin ) -> -. H e. Fin )
39 eqid
 |-  U. K = U. K
40 39 bwth
 |-  ( ( K e. Comp /\ H C_ U. K /\ -. H e. Fin ) -> E. x e. U. K x e. ( ( limPt ` K ) ` H ) )
41 21 37 38 40 syl3anc
 |-  ( ( ph /\ -. H e. Fin ) -> E. x e. U. K x e. ( ( limPt ` K ) ` H ) )
42 24 27 sstrd
 |-  ( ph -> H C_ RR )
43 42 ad2antrr
 |-  ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> H C_ RR )
44 ne0i
 |-  ( x e. ( ( limPt ` J ) ` H ) -> ( ( limPt ` J ) ` H ) =/= (/) )
45 44 adantl
 |-  ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> ( ( limPt ` J ) ` H ) =/= (/) )
46 absf
 |-  abs : CC --> RR
47 ffn
 |-  ( abs : CC --> RR -> abs Fn CC )
48 46 47 ax-mp
 |-  abs Fn CC
49 subf
 |-  - : ( CC X. CC ) --> CC
50 ffn
 |-  ( - : ( CC X. CC ) --> CC -> - Fn ( CC X. CC ) )
51 49 50 ax-mp
 |-  - Fn ( CC X. CC )
52 frn
 |-  ( - : ( CC X. CC ) --> CC -> ran - C_ CC )
53 49 52 ax-mp
 |-  ran - C_ CC
54 fnco
 |-  ( ( abs Fn CC /\ - Fn ( CC X. CC ) /\ ran - C_ CC ) -> ( abs o. - ) Fn ( CC X. CC ) )
55 48 51 53 54 mp3an
 |-  ( abs o. - ) Fn ( CC X. CC )
56 9 fneq1i
 |-  ( D Fn ( CC X. CC ) <-> ( abs o. - ) Fn ( CC X. CC ) )
57 55 56 mpbir
 |-  D Fn ( CC X. CC )
58 1 2 iccssred
 |-  ( ph -> ( B [,] C ) C_ RR )
59 ax-resscn
 |-  RR C_ CC
60 58 59 sstrdi
 |-  ( ph -> ( B [,] C ) C_ CC )
61 5 60 sstrd
 |-  ( ph -> A C_ CC )
62 xpss12
 |-  ( ( A C_ CC /\ A C_ CC ) -> ( A X. A ) C_ ( CC X. CC ) )
63 61 61 62 syl2anc
 |-  ( ph -> ( A X. A ) C_ ( CC X. CC ) )
64 63 ssdifssd
 |-  ( ph -> ( ( A X. A ) \ _I ) C_ ( CC X. CC ) )
65 10 64 eqsstrid
 |-  ( ph -> I C_ ( CC X. CC ) )
66 fnssres
 |-  ( ( D Fn ( CC X. CC ) /\ I C_ ( CC X. CC ) ) -> ( D |` I ) Fn I )
67 57 65 66 sylancr
 |-  ( ph -> ( D |` I ) Fn I )
68 fvres
 |-  ( x e. I -> ( ( D |` I ) ` x ) = ( D ` x ) )
69 68 adantl
 |-  ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) = ( D ` x ) )
70 9 fveq1i
 |-  ( D ` x ) = ( ( abs o. - ) ` x )
71 70 a1i
 |-  ( ( ph /\ x e. I ) -> ( D ` x ) = ( ( abs o. - ) ` x ) )
72 ffun
 |-  ( - : ( CC X. CC ) --> CC -> Fun - )
73 49 72 ax-mp
 |-  Fun -
74 65 sselda
 |-  ( ( ph /\ x e. I ) -> x e. ( CC X. CC ) )
75 49 fdmi
 |-  dom - = ( CC X. CC )
76 74 75 eleqtrrdi
 |-  ( ( ph /\ x e. I ) -> x e. dom - )
77 fvco
 |-  ( ( Fun - /\ x e. dom - ) -> ( ( abs o. - ) ` x ) = ( abs ` ( - ` x ) ) )
78 73 76 77 sylancr
 |-  ( ( ph /\ x e. I ) -> ( ( abs o. - ) ` x ) = ( abs ` ( - ` x ) ) )
79 69 71 78 3eqtrd
 |-  ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) = ( abs ` ( - ` x ) ) )
80 49 a1i
 |-  ( ( ph /\ x e. I ) -> - : ( CC X. CC ) --> CC )
81 80 74 ffvelrnd
 |-  ( ( ph /\ x e. I ) -> ( - ` x ) e. CC )
82 81 abscld
 |-  ( ( ph /\ x e. I ) -> ( abs ` ( - ` x ) ) e. RR )
83 79 82 eqeltrd
 |-  ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) e. RR )
84 elxp2
 |-  ( x e. ( CC X. CC ) <-> E. y e. CC E. z e. CC x = <. y , z >. )
85 74 84 sylib
 |-  ( ( ph /\ x e. I ) -> E. y e. CC E. z e. CC x = <. y , z >. )
86 fveq2
 |-  ( x = <. y , z >. -> ( - ` x ) = ( - ` <. y , z >. ) )
87 86 3ad2ant3
 |-  ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( - ` x ) = ( - ` <. y , z >. ) )
88 df-ov
 |-  ( y - z ) = ( - ` <. y , z >. )
89 simp1l
 |-  ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ph )
90 simpr
 |-  ( ( x e. I /\ x = <. y , z >. ) -> x = <. y , z >. )
91 simpl
 |-  ( ( x e. I /\ x = <. y , z >. ) -> x e. I )
92 90 91 eqeltrrd
 |-  ( ( x e. I /\ x = <. y , z >. ) -> <. y , z >. e. I )
93 92 adantll
 |-  ( ( ( ph /\ x e. I ) /\ x = <. y , z >. ) -> <. y , z >. e. I )
94 93 3adant2
 |-  ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> <. y , z >. e. I )
95 61 adantr
 |-  ( ( ph /\ <. y , z >. e. I ) -> A C_ CC )
96 10 eleq2i
 |-  ( <. y , z >. e. I <-> <. y , z >. e. ( ( A X. A ) \ _I ) )
97 eldif
 |-  ( <. y , z >. e. ( ( A X. A ) \ _I ) <-> ( <. y , z >. e. ( A X. A ) /\ -. <. y , z >. e. _I ) )
98 96 97 sylbb
 |-  ( <. y , z >. e. I -> ( <. y , z >. e. ( A X. A ) /\ -. <. y , z >. e. _I ) )
99 98 simpld
 |-  ( <. y , z >. e. I -> <. y , z >. e. ( A X. A ) )
100 opelxp
 |-  ( <. y , z >. e. ( A X. A ) <-> ( y e. A /\ z e. A ) )
101 99 100 sylib
 |-  ( <. y , z >. e. I -> ( y e. A /\ z e. A ) )
102 101 adantl
 |-  ( ( ph /\ <. y , z >. e. I ) -> ( y e. A /\ z e. A ) )
103 102 simpld
 |-  ( ( ph /\ <. y , z >. e. I ) -> y e. A )
104 95 103 sseldd
 |-  ( ( ph /\ <. y , z >. e. I ) -> y e. CC )
105 102 simprd
 |-  ( ( ph /\ <. y , z >. e. I ) -> z e. A )
106 95 105 sseldd
 |-  ( ( ph /\ <. y , z >. e. I ) -> z e. CC )
107 98 simprd
 |-  ( <. y , z >. e. I -> -. <. y , z >. e. _I )
108 df-br
 |-  ( y _I z <-> <. y , z >. e. _I )
109 107 108 sylnibr
 |-  ( <. y , z >. e. I -> -. y _I z )
110 vex
 |-  z e. _V
111 110 ideq
 |-  ( y _I z <-> y = z )
112 109 111 sylnib
 |-  ( <. y , z >. e. I -> -. y = z )
113 112 neqned
 |-  ( <. y , z >. e. I -> y =/= z )
114 113 adantl
 |-  ( ( ph /\ <. y , z >. e. I ) -> y =/= z )
115 104 106 114 subne0d
 |-  ( ( ph /\ <. y , z >. e. I ) -> ( y - z ) =/= 0 )
116 89 94 115 syl2anc
 |-  ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( y - z ) =/= 0 )
117 88 116 eqnetrrid
 |-  ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( - ` <. y , z >. ) =/= 0 )
118 87 117 eqnetrd
 |-  ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( - ` x ) =/= 0 )
119 118 3exp
 |-  ( ( ph /\ x e. I ) -> ( ( y e. CC /\ z e. CC ) -> ( x = <. y , z >. -> ( - ` x ) =/= 0 ) ) )
120 119 rexlimdvv
 |-  ( ( ph /\ x e. I ) -> ( E. y e. CC E. z e. CC x = <. y , z >. -> ( - ` x ) =/= 0 ) )
121 85 120 mpd
 |-  ( ( ph /\ x e. I ) -> ( - ` x ) =/= 0 )
122 absgt0
 |-  ( ( - ` x ) e. CC -> ( ( - ` x ) =/= 0 <-> 0 < ( abs ` ( - ` x ) ) ) )
123 81 122 syl
 |-  ( ( ph /\ x e. I ) -> ( ( - ` x ) =/= 0 <-> 0 < ( abs ` ( - ` x ) ) ) )
124 121 123 mpbid
 |-  ( ( ph /\ x e. I ) -> 0 < ( abs ` ( - ` x ) ) )
125 79 eqcomd
 |-  ( ( ph /\ x e. I ) -> ( abs ` ( - ` x ) ) = ( ( D |` I ) ` x ) )
126 124 125 breqtrd
 |-  ( ( ph /\ x e. I ) -> 0 < ( ( D |` I ) ` x ) )
127 83 126 elrpd
 |-  ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) e. RR+ )
128 127 ralrimiva
 |-  ( ph -> A. x e. I ( ( D |` I ) ` x ) e. RR+ )
129 fnfvrnss
 |-  ( ( ( D |` I ) Fn I /\ A. x e. I ( ( D |` I ) ` x ) e. RR+ ) -> ran ( D |` I ) C_ RR+ )
130 67 128 129 syl2anc
 |-  ( ph -> ran ( D |` I ) C_ RR+ )
131 11 130 eqsstrid
 |-  ( ph -> R C_ RR+ )
132 ltso
 |-  < Or RR
133 132 a1i
 |-  ( ph -> < Or RR )
134 xpfi
 |-  ( ( A e. Fin /\ A e. Fin ) -> ( A X. A ) e. Fin )
135 6 6 134 syl2anc
 |-  ( ph -> ( A X. A ) e. Fin )
136 diffi
 |-  ( ( A X. A ) e. Fin -> ( ( A X. A ) \ _I ) e. Fin )
137 135 136 syl
 |-  ( ph -> ( ( A X. A ) \ _I ) e. Fin )
138 10 137 eqeltrid
 |-  ( ph -> I e. Fin )
139 fnfi
 |-  ( ( ( D |` I ) Fn I /\ I e. Fin ) -> ( D |` I ) e. Fin )
140 67 138 139 syl2anc
 |-  ( ph -> ( D |` I ) e. Fin )
141 rnfi
 |-  ( ( D |` I ) e. Fin -> ran ( D |` I ) e. Fin )
142 140 141 syl
 |-  ( ph -> ran ( D |` I ) e. Fin )
143 11 142 eqeltrid
 |-  ( ph -> R e. Fin )
144 11 a1i
 |-  ( ph -> R = ran ( D |` I ) )
145 9 a1i
 |-  ( ph -> D = ( abs o. - ) )
146 145 reseq1d
 |-  ( ph -> ( D |` I ) = ( ( abs o. - ) |` I ) )
147 146 fveq1d
 |-  ( ph -> ( ( D |` I ) ` <. B , C >. ) = ( ( ( abs o. - ) |` I ) ` <. B , C >. ) )
148 opelxp
 |-  ( <. B , C >. e. ( A X. A ) <-> ( B e. A /\ C e. A ) )
149 7 8 148 sylanbrc
 |-  ( ph -> <. B , C >. e. ( A X. A ) )
150 1 3 ltned
 |-  ( ph -> B =/= C )
151 150 neneqd
 |-  ( ph -> -. B = C )
152 ideqg
 |-  ( C e. A -> ( B _I C <-> B = C ) )
153 8 152 syl
 |-  ( ph -> ( B _I C <-> B = C ) )
154 151 153 mtbird
 |-  ( ph -> -. B _I C )
155 df-br
 |-  ( B _I C <-> <. B , C >. e. _I )
156 154 155 sylnib
 |-  ( ph -> -. <. B , C >. e. _I )
157 149 156 eldifd
 |-  ( ph -> <. B , C >. e. ( ( A X. A ) \ _I ) )
158 157 10 eleqtrrdi
 |-  ( ph -> <. B , C >. e. I )
159 fvres
 |-  ( <. B , C >. e. I -> ( ( ( abs o. - ) |` I ) ` <. B , C >. ) = ( ( abs o. - ) ` <. B , C >. ) )
160 158 159 syl
 |-  ( ph -> ( ( ( abs o. - ) |` I ) ` <. B , C >. ) = ( ( abs o. - ) ` <. B , C >. ) )
161 1 recnd
 |-  ( ph -> B e. CC )
162 2 recnd
 |-  ( ph -> C e. CC )
163 opelxp
 |-  ( <. B , C >. e. ( CC X. CC ) <-> ( B e. CC /\ C e. CC ) )
164 161 162 163 sylanbrc
 |-  ( ph -> <. B , C >. e. ( CC X. CC ) )
165 164 75 eleqtrrdi
 |-  ( ph -> <. B , C >. e. dom - )
166 fvco
 |-  ( ( Fun - /\ <. B , C >. e. dom - ) -> ( ( abs o. - ) ` <. B , C >. ) = ( abs ` ( - ` <. B , C >. ) ) )
167 73 165 166 sylancr
 |-  ( ph -> ( ( abs o. - ) ` <. B , C >. ) = ( abs ` ( - ` <. B , C >. ) ) )
168 df-ov
 |-  ( B - C ) = ( - ` <. B , C >. )
169 168 eqcomi
 |-  ( - ` <. B , C >. ) = ( B - C )
170 169 a1i
 |-  ( ph -> ( - ` <. B , C >. ) = ( B - C ) )
171 170 fveq2d
 |-  ( ph -> ( abs ` ( - ` <. B , C >. ) ) = ( abs ` ( B - C ) ) )
172 167 171 eqtrd
 |-  ( ph -> ( ( abs o. - ) ` <. B , C >. ) = ( abs ` ( B - C ) ) )
173 147 160 172 3eqtrrd
 |-  ( ph -> ( abs ` ( B - C ) ) = ( ( D |` I ) ` <. B , C >. ) )
174 fnfvelrn
 |-  ( ( ( D |` I ) Fn I /\ <. B , C >. e. I ) -> ( ( D |` I ) ` <. B , C >. ) e. ran ( D |` I ) )
175 67 158 174 syl2anc
 |-  ( ph -> ( ( D |` I ) ` <. B , C >. ) e. ran ( D |` I ) )
176 173 175 eqeltrd
 |-  ( ph -> ( abs ` ( B - C ) ) e. ran ( D |` I ) )
177 ne0i
 |-  ( ( abs ` ( B - C ) ) e. ran ( D |` I ) -> ran ( D |` I ) =/= (/) )
178 176 177 syl
 |-  ( ph -> ran ( D |` I ) =/= (/) )
179 144 178 eqnetrd
 |-  ( ph -> R =/= (/) )
180 resss
 |-  ( D |` I ) C_ D
181 rnss
 |-  ( ( D |` I ) C_ D -> ran ( D |` I ) C_ ran D )
182 180 181 ax-mp
 |-  ran ( D |` I ) C_ ran D
183 9 rneqi
 |-  ran D = ran ( abs o. - )
184 rncoss
 |-  ran ( abs o. - ) C_ ran abs
185 frn
 |-  ( abs : CC --> RR -> ran abs C_ RR )
186 46 185 ax-mp
 |-  ran abs C_ RR
187 184 186 sstri
 |-  ran ( abs o. - ) C_ RR
188 183 187 eqsstri
 |-  ran D C_ RR
189 182 188 sstri
 |-  ran ( D |` I ) C_ RR
190 11 189 eqsstri
 |-  R C_ RR
191 190 a1i
 |-  ( ph -> R C_ RR )
192 fiinfcl
 |-  ( ( < Or RR /\ ( R e. Fin /\ R =/= (/) /\ R C_ RR ) ) -> inf ( R , RR , < ) e. R )
193 133 143 179 191 192 syl13anc
 |-  ( ph -> inf ( R , RR , < ) e. R )
194 131 193 sseldd
 |-  ( ph -> inf ( R , RR , < ) e. RR+ )
195 12 194 eqeltrid
 |-  ( ph -> E e. RR+ )
196 195 ad2antrr
 |-  ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> E e. RR+ )
197 15 43 45 196 lptre2pt
 |-  ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> E. y e. H E. z e. H ( y =/= z /\ ( abs ` ( y - z ) ) < E ) )
198 simpll
 |-  ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> ph )
199 42 sselda
 |-  ( ( ph /\ y e. H ) -> y e. RR )
200 199 adantrr
 |-  ( ( ph /\ ( y e. H /\ z e. H ) ) -> y e. RR )
201 200 adantr
 |-  ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> y e. RR )
202 42 sselda
 |-  ( ( ph /\ z e. H ) -> z e. RR )
203 202 adantrl
 |-  ( ( ph /\ ( y e. H /\ z e. H ) ) -> z e. RR )
204 203 adantr
 |-  ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> z e. RR )
205 simpr
 |-  ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> y =/= z )
206 201 204 205 3jca
 |-  ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> ( y e. RR /\ z e. RR /\ y =/= z ) )
207 17 eleq2i
 |-  ( y e. H <-> y e. { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } )
208 oveq1
 |-  ( x = y -> ( x + ( k x. T ) ) = ( y + ( k x. T ) ) )
209 208 eleq1d
 |-  ( x = y -> ( ( x + ( k x. T ) ) e. A <-> ( y + ( k x. T ) ) e. A ) )
210 209 rexbidv
 |-  ( x = y -> ( E. k e. ZZ ( x + ( k x. T ) ) e. A <-> E. k e. ZZ ( y + ( k x. T ) ) e. A ) )
211 oveq1
 |-  ( k = j -> ( k x. T ) = ( j x. T ) )
212 211 oveq2d
 |-  ( k = j -> ( y + ( k x. T ) ) = ( y + ( j x. T ) ) )
213 212 eleq1d
 |-  ( k = j -> ( ( y + ( k x. T ) ) e. A <-> ( y + ( j x. T ) ) e. A ) )
214 213 cbvrexvw
 |-  ( E. k e. ZZ ( y + ( k x. T ) ) e. A <-> E. j e. ZZ ( y + ( j x. T ) ) e. A )
215 210 214 bitrdi
 |-  ( x = y -> ( E. k e. ZZ ( x + ( k x. T ) ) e. A <-> E. j e. ZZ ( y + ( j x. T ) ) e. A ) )
216 215 elrab
 |-  ( y e. { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } <-> ( y e. ( X [,] Y ) /\ E. j e. ZZ ( y + ( j x. T ) ) e. A ) )
217 207 216 sylbb
 |-  ( y e. H -> ( y e. ( X [,] Y ) /\ E. j e. ZZ ( y + ( j x. T ) ) e. A ) )
218 217 simprd
 |-  ( y e. H -> E. j e. ZZ ( y + ( j x. T ) ) e. A )
219 218 adantr
 |-  ( ( y e. H /\ z e. H ) -> E. j e. ZZ ( y + ( j x. T ) ) e. A )
220 17 eleq2i
 |-  ( z e. H <-> z e. { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } )
221 oveq1
 |-  ( x = z -> ( x + ( k x. T ) ) = ( z + ( k x. T ) ) )
222 221 eleq1d
 |-  ( x = z -> ( ( x + ( k x. T ) ) e. A <-> ( z + ( k x. T ) ) e. A ) )
223 222 rexbidv
 |-  ( x = z -> ( E. k e. ZZ ( x + ( k x. T ) ) e. A <-> E. k e. ZZ ( z + ( k x. T ) ) e. A ) )
224 223 elrab
 |-  ( z e. { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } <-> ( z e. ( X [,] Y ) /\ E. k e. ZZ ( z + ( k x. T ) ) e. A ) )
225 220 224 sylbb
 |-  ( z e. H -> ( z e. ( X [,] Y ) /\ E. k e. ZZ ( z + ( k x. T ) ) e. A ) )
226 225 simprd
 |-  ( z e. H -> E. k e. ZZ ( z + ( k x. T ) ) e. A )
227 226 adantl
 |-  ( ( y e. H /\ z e. H ) -> E. k e. ZZ ( z + ( k x. T ) ) e. A )
228 reeanv
 |-  ( E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) <-> ( E. j e. ZZ ( y + ( j x. T ) ) e. A /\ E. k e. ZZ ( z + ( k x. T ) ) e. A ) )
229 219 227 228 sylanbrc
 |-  ( ( y e. H /\ z e. H ) -> E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) )
230 229 ad2antlr
 |-  ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) )
231 simplll
 |-  ( ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) /\ y < z ) -> ph )
232 simpl1
 |-  ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> y e. RR )
233 simpl2
 |-  ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> z e. RR )
234 simpr
 |-  ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> y < z )
235 232 233 234 3jca
 |-  ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> ( y e. RR /\ z e. RR /\ y < z ) )
236 235 adantll
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ y < z ) -> ( y e. RR /\ z e. RR /\ y < z ) )
237 236 adantlr
 |-  ( ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) /\ y < z ) -> ( y e. RR /\ z e. RR /\ y < z ) )
238 simplr
 |-  ( ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) /\ y < z ) -> E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) )
239 eleq1
 |-  ( b = z -> ( b e. RR <-> z e. RR ) )
240 breq2
 |-  ( b = z -> ( y < b <-> y < z ) )
241 239 240 3anbi23d
 |-  ( b = z -> ( ( y e. RR /\ b e. RR /\ y < b ) <-> ( y e. RR /\ z e. RR /\ y < z ) ) )
242 241 anbi2d
 |-  ( b = z -> ( ( ph /\ ( y e. RR /\ b e. RR /\ y < b ) ) <-> ( ph /\ ( y e. RR /\ z e. RR /\ y < z ) ) ) )
243 oveq1
 |-  ( b = z -> ( b + ( k x. T ) ) = ( z + ( k x. T ) ) )
244 243 eleq1d
 |-  ( b = z -> ( ( b + ( k x. T ) ) e. A <-> ( z + ( k x. T ) ) e. A ) )
245 244 anbi2d
 |-  ( b = z -> ( ( ( y + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) <-> ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) )
246 245 2rexbidv
 |-  ( b = z -> ( E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) <-> E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) )
247 242 246 anbi12d
 |-  ( b = z -> ( ( ( ph /\ ( y e. RR /\ b e. RR /\ y < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) <-> ( ( ph /\ ( y e. RR /\ z e. RR /\ y < z ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) ) )
248 oveq2
 |-  ( b = z -> ( y - b ) = ( y - z ) )
249 248 fveq2d
 |-  ( b = z -> ( abs ` ( y - b ) ) = ( abs ` ( y - z ) ) )
250 249 breq2d
 |-  ( b = z -> ( E <_ ( abs ` ( y - b ) ) <-> E <_ ( abs ` ( y - z ) ) ) )
251 247 250 imbi12d
 |-  ( b = z -> ( ( ( ( ph /\ ( y e. RR /\ b e. RR /\ y < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( y - b ) ) ) <-> ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y < z ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( y - z ) ) ) ) )
252 eleq1
 |-  ( a = y -> ( a e. RR <-> y e. RR ) )
253 breq1
 |-  ( a = y -> ( a < b <-> y < b ) )
254 252 253 3anbi13d
 |-  ( a = y -> ( ( a e. RR /\ b e. RR /\ a < b ) <-> ( y e. RR /\ b e. RR /\ y < b ) ) )
255 254 anbi2d
 |-  ( a = y -> ( ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) <-> ( ph /\ ( y e. RR /\ b e. RR /\ y < b ) ) ) )
256 oveq1
 |-  ( a = y -> ( a + ( j x. T ) ) = ( y + ( j x. T ) ) )
257 256 eleq1d
 |-  ( a = y -> ( ( a + ( j x. T ) ) e. A <-> ( y + ( j x. T ) ) e. A ) )
258 257 anbi1d
 |-  ( a = y -> ( ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) <-> ( ( y + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) )
259 258 2rexbidv
 |-  ( a = y -> ( E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) <-> E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) )
260 255 259 anbi12d
 |-  ( a = y -> ( ( ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) <-> ( ( ph /\ ( y e. RR /\ b e. RR /\ y < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) ) )
261 oveq1
 |-  ( a = y -> ( a - b ) = ( y - b ) )
262 261 fveq2d
 |-  ( a = y -> ( abs ` ( a - b ) ) = ( abs ` ( y - b ) ) )
263 262 breq2d
 |-  ( a = y -> ( E <_ ( abs ` ( a - b ) ) <-> E <_ ( abs ` ( y - b ) ) ) )
264 260 263 imbi12d
 |-  ( a = y -> ( ( ( ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( a - b ) ) ) <-> ( ( ( ph /\ ( y e. RR /\ b e. RR /\ y < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( y - b ) ) ) ) )
265 18 simprbi
 |-  ( ps -> E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) )
266 18 biimpi
 |-  ( ps -> ( ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) )
267 266 simpld
 |-  ( ps -> ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) )
268 267 simpld
 |-  ( ps -> ph )
269 268 1 syl
 |-  ( ps -> B e. RR )
270 269 adantr
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> B e. RR )
271 268 2 syl
 |-  ( ps -> C e. RR )
272 271 adantr
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> C e. RR )
273 268 5 syl
 |-  ( ps -> A C_ ( B [,] C ) )
274 273 sselda
 |-  ( ( ps /\ ( b + ( k x. T ) ) e. A ) -> ( b + ( k x. T ) ) e. ( B [,] C ) )
275 274 adantrl
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( b + ( k x. T ) ) e. ( B [,] C ) )
276 273 sselda
 |-  ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> ( a + ( j x. T ) ) e. ( B [,] C ) )
277 276 adantrr
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) e. ( B [,] C ) )
278 270 272 275 277 iccsuble
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ ( C - B ) )
279 278 4 breqtrrdi
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
280 279 3adant2
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
281 280 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ -. k <_ j ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
282 simpr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> -. k <_ j )
283 zre
 |-  ( j e. ZZ -> j e. RR )
284 283 adantr
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> j e. RR )
285 284 ad2antlr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> j e. RR )
286 zre
 |-  ( k e. ZZ -> k e. RR )
287 286 adantl
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> k e. RR )
288 287 ad2antlr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> k e. RR )
289 285 288 ltnled
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> ( j < k <-> -. k <_ j ) )
290 282 289 mpbird
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> j < k )
291 2 1 resubcld
 |-  ( ph -> ( C - B ) e. RR )
292 4 291 eqeltrid
 |-  ( ph -> T e. RR )
293 268 292 syl
 |-  ( ps -> T e. RR )
294 293 ad2antrr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T e. RR )
295 287 adantl
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> k e. RR )
296 284 adantl
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> j e. RR )
297 295 296 resubcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k - j ) e. RR )
298 293 adantr
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> T e. RR )
299 297 298 remulcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) e. RR )
300 299 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( ( k - j ) x. T ) e. RR )
301 267 simprd
 |-  ( ps -> ( a e. RR /\ b e. RR /\ a < b ) )
302 301 simp2d
 |-  ( ps -> b e. RR )
303 302 adantr
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> b e. RR )
304 286 adantl
 |-  ( ( ps /\ k e. ZZ ) -> k e. RR )
305 293 adantr
 |-  ( ( ps /\ k e. ZZ ) -> T e. RR )
306 304 305 remulcld
 |-  ( ( ps /\ k e. ZZ ) -> ( k x. T ) e. RR )
307 306 adantrl
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k x. T ) e. RR )
308 303 307 readdcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( b + ( k x. T ) ) e. RR )
309 301 simp1d
 |-  ( ps -> a e. RR )
310 309 adantr
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> a e. RR )
311 283 adantl
 |-  ( ( ps /\ j e. ZZ ) -> j e. RR )
312 293 adantr
 |-  ( ( ps /\ j e. ZZ ) -> T e. RR )
313 311 312 remulcld
 |-  ( ( ps /\ j e. ZZ ) -> ( j x. T ) e. RR )
314 313 adantrr
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j x. T ) e. RR )
315 310 314 readdcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( a + ( j x. T ) ) e. RR )
316 308 315 resubcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) e. RR )
317 316 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) e. RR )
318 293 recnd
 |-  ( ps -> T e. CC )
319 318 mulid2d
 |-  ( ps -> ( 1 x. T ) = T )
320 319 eqcomd
 |-  ( ps -> T = ( 1 x. T ) )
321 320 ad2antrr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T = ( 1 x. T ) )
322 simpr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> j < k )
323 zltlem1
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( j < k <-> j <_ ( k - 1 ) ) )
324 323 ad2antlr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( j < k <-> j <_ ( k - 1 ) ) )
325 322 324 mpbid
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> j <_ ( k - 1 ) )
326 284 ad2antlr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> j e. RR )
327 peano2rem
 |-  ( k e. RR -> ( k - 1 ) e. RR )
328 295 327 syl
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k - 1 ) e. RR )
329 328 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( k - 1 ) e. RR )
330 1re
 |-  1 e. RR
331 resubcl
 |-  ( ( 1 e. RR /\ j e. RR ) -> ( 1 - j ) e. RR )
332 330 326 331 sylancr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( 1 - j ) e. RR )
333 simpr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> j <_ ( k - 1 ) )
334 326 329 332 333 leadd1dd
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( j + ( 1 - j ) ) <_ ( ( k - 1 ) + ( 1 - j ) ) )
335 zcn
 |-  ( j e. ZZ -> j e. CC )
336 335 adantr
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> j e. CC )
337 1cnd
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> 1 e. CC )
338 336 337 pncan3d
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( j + ( 1 - j ) ) = 1 )
339 338 ad2antlr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( j + ( 1 - j ) ) = 1 )
340 zcn
 |-  ( k e. ZZ -> k e. CC )
341 340 adantl
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> k e. CC )
342 341 337 336 npncand
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( ( k - 1 ) + ( 1 - j ) ) = ( k - j ) )
343 342 ad2antlr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( ( k - 1 ) + ( 1 - j ) ) = ( k - j ) )
344 334 339 343 3brtr3d
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> 1 <_ ( k - j ) )
345 325 344 syldan
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> 1 <_ ( k - j ) )
346 330 a1i
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> 1 e. RR )
347 297 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( k - j ) e. RR )
348 1 2 posdifd
 |-  ( ph -> ( B < C <-> 0 < ( C - B ) ) )
349 3 348 mpbid
 |-  ( ph -> 0 < ( C - B ) )
350 349 4 breqtrrdi
 |-  ( ph -> 0 < T )
351 292 350 elrpd
 |-  ( ph -> T e. RR+ )
352 268 351 syl
 |-  ( ps -> T e. RR+ )
353 352 ad2antrr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T e. RR+ )
354 346 347 353 lemul1d
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( 1 <_ ( k - j ) <-> ( 1 x. T ) <_ ( ( k - j ) x. T ) ) )
355 345 354 mpbid
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( 1 x. T ) <_ ( ( k - j ) x. T ) )
356 321 355 eqbrtrd
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T <_ ( ( k - j ) x. T ) )
357 302 309 resubcld
 |-  ( ps -> ( b - a ) e. RR )
358 301 simp3d
 |-  ( ps -> a < b )
359 309 302 posdifd
 |-  ( ps -> ( a < b <-> 0 < ( b - a ) ) )
360 358 359 mpbid
 |-  ( ps -> 0 < ( b - a ) )
361 357 360 elrpd
 |-  ( ps -> ( b - a ) e. RR+ )
362 361 adantr
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( b - a ) e. RR+ )
363 299 362 ltaddrp2d
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) < ( ( b - a ) + ( ( k - j ) x. T ) ) )
364 302 recnd
 |-  ( ps -> b e. CC )
365 364 adantr
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> b e. CC )
366 306 recnd
 |-  ( ( ps /\ k e. ZZ ) -> ( k x. T ) e. CC )
367 366 adantrl
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k x. T ) e. CC )
368 309 recnd
 |-  ( ps -> a e. CC )
369 368 adantr
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> a e. CC )
370 313 recnd
 |-  ( ( ps /\ j e. ZZ ) -> ( j x. T ) e. CC )
371 370 adantrr
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j x. T ) e. CC )
372 365 367 369 371 addsub4d
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) = ( ( b - a ) + ( ( k x. T ) - ( j x. T ) ) ) )
373 340 ad2antll
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> k e. CC )
374 335 ad2antrl
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> j e. CC )
375 318 adantr
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> T e. CC )
376 373 374 375 subdird
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) = ( ( k x. T ) - ( j x. T ) ) )
377 376 eqcomd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k x. T ) - ( j x. T ) ) = ( ( k - j ) x. T ) )
378 377 oveq2d
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b - a ) + ( ( k x. T ) - ( j x. T ) ) ) = ( ( b - a ) + ( ( k - j ) x. T ) ) )
379 372 378 eqtr2d
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b - a ) + ( ( k - j ) x. T ) ) = ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
380 363 379 breqtrd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
381 380 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( ( k - j ) x. T ) < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
382 294 300 317 356 381 lelttrd
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
383 294 317 ltnled
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( T < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <-> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T ) )
384 382 383 mpbid
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
385 290 384 syldan
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
386 385 3adantl3
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ -. k <_ j ) -> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
387 281 386 condan
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> k <_ j )
388 190 193 sselid
 |-  ( ph -> inf ( R , RR , < ) e. RR )
389 12 388 eqeltrid
 |-  ( ph -> E e. RR )
390 268 389 syl
 |-  ( ps -> E e. RR )
391 390 3ad2ant1
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E e. RR )
392 391 ad2antrr
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> E e. RR )
393 293 3ad2ant1
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> T e. RR )
394 393 ad2antrr
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> T e. RR )
395 284 287 resubcld
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( j - k ) e. RR )
396 395 adantl
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j - k ) e. RR )
397 396 298 remulcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( j - k ) x. T ) e. RR )
398 397 3adant3
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( j - k ) x. T ) e. RR )
399 398 ad2antrr
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( j - k ) x. T ) e. RR )
400 id
 |-  ( ph -> ph )
401 7 8 jca
 |-  ( ph -> ( B e. A /\ C e. A ) )
402 400 401 3 3jca
 |-  ( ph -> ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) )
403 eleq1
 |-  ( d = C -> ( d e. A <-> C e. A ) )
404 403 anbi2d
 |-  ( d = C -> ( ( B e. A /\ d e. A ) <-> ( B e. A /\ C e. A ) ) )
405 breq2
 |-  ( d = C -> ( B < d <-> B < C ) )
406 404 405 3anbi23d
 |-  ( d = C -> ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) <-> ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) ) )
407 oveq1
 |-  ( d = C -> ( d - B ) = ( C - B ) )
408 407 breq2d
 |-  ( d = C -> ( E <_ ( d - B ) <-> E <_ ( C - B ) ) )
409 406 408 imbi12d
 |-  ( d = C -> ( ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> E <_ ( d - B ) ) <-> ( ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) -> E <_ ( C - B ) ) ) )
410 simp2l
 |-  ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> B e. A )
411 eleq1
 |-  ( c = B -> ( c e. A <-> B e. A ) )
412 411 anbi1d
 |-  ( c = B -> ( ( c e. A /\ d e. A ) <-> ( B e. A /\ d e. A ) ) )
413 breq1
 |-  ( c = B -> ( c < d <-> B < d ) )
414 412 413 3anbi23d
 |-  ( c = B -> ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) <-> ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) ) )
415 oveq2
 |-  ( c = B -> ( d - c ) = ( d - B ) )
416 415 breq2d
 |-  ( c = B -> ( E <_ ( d - c ) <-> E <_ ( d - B ) ) )
417 414 416 imbi12d
 |-  ( c = B -> ( ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E <_ ( d - c ) ) <-> ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> E <_ ( d - B ) ) ) )
418 190 a1i
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> R C_ RR )
419 0re
 |-  0 e. RR
420 11 eleq2i
 |-  ( y e. R <-> y e. ran ( D |` I ) )
421 420 biimpi
 |-  ( y e. R -> y e. ran ( D |` I ) )
422 421 adantl
 |-  ( ( ph /\ y e. R ) -> y e. ran ( D |` I ) )
423 67 adantr
 |-  ( ( ph /\ y e. R ) -> ( D |` I ) Fn I )
424 fvelrnb
 |-  ( ( D |` I ) Fn I -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) )
425 423 424 syl
 |-  ( ( ph /\ y e. R ) -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) )
426 422 425 mpbid
 |-  ( ( ph /\ y e. R ) -> E. x e. I ( ( D |` I ) ` x ) = y )
427 127 rpge0d
 |-  ( ( ph /\ x e. I ) -> 0 <_ ( ( D |` I ) ` x ) )
428 427 3adant3
 |-  ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> 0 <_ ( ( D |` I ) ` x ) )
429 simp3
 |-  ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> ( ( D |` I ) ` x ) = y )
430 428 429 breqtrd
 |-  ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> 0 <_ y )
431 430 3exp
 |-  ( ph -> ( x e. I -> ( ( ( D |` I ) ` x ) = y -> 0 <_ y ) ) )
432 431 adantr
 |-  ( ( ph /\ y e. R ) -> ( x e. I -> ( ( ( D |` I ) ` x ) = y -> 0 <_ y ) ) )
433 432 rexlimdv
 |-  ( ( ph /\ y e. R ) -> ( E. x e. I ( ( D |` I ) ` x ) = y -> 0 <_ y ) )
434 426 433 mpd
 |-  ( ( ph /\ y e. R ) -> 0 <_ y )
435 434 ralrimiva
 |-  ( ph -> A. y e. R 0 <_ y )
436 breq1
 |-  ( x = 0 -> ( x <_ y <-> 0 <_ y ) )
437 436 ralbidv
 |-  ( x = 0 -> ( A. y e. R x <_ y <-> A. y e. R 0 <_ y ) )
438 437 rspcev
 |-  ( ( 0 e. RR /\ A. y e. R 0 <_ y ) -> E. x e. RR A. y e. R x <_ y )
439 419 435 438 sylancr
 |-  ( ph -> E. x e. RR A. y e. R x <_ y )
440 439 3ad2ant1
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E. x e. RR A. y e. R x <_ y )
441 pm3.22
 |-  ( ( c e. A /\ d e. A ) -> ( d e. A /\ c e. A ) )
442 opelxp
 |-  ( <. d , c >. e. ( A X. A ) <-> ( d e. A /\ c e. A ) )
443 441 442 sylibr
 |-  ( ( c e. A /\ d e. A ) -> <. d , c >. e. ( A X. A ) )
444 443 3ad2ant2
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. ( A X. A ) )
445 5 58 sstrd
 |-  ( ph -> A C_ RR )
446 445 sselda
 |-  ( ( ph /\ c e. A ) -> c e. RR )
447 446 adantrr
 |-  ( ( ph /\ ( c e. A /\ d e. A ) ) -> c e. RR )
448 447 3adant3
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c e. RR )
449 simp3
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c < d )
450 448 449 gtned
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> d =/= c )
451 450 neneqd
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> -. d = c )
452 df-br
 |-  ( d _I c <-> <. d , c >. e. _I )
453 vex
 |-  c e. _V
454 453 ideq
 |-  ( d _I c <-> d = c )
455 452 454 bitr3i
 |-  ( <. d , c >. e. _I <-> d = c )
456 451 455 sylnibr
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> -. <. d , c >. e. _I )
457 444 456 eldifd
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. ( ( A X. A ) \ _I ) )
458 457 10 eleqtrrdi
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. I )
459 448 449 ltned
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c =/= d )
460 146 3ad2ant1
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( D |` I ) = ( ( abs o. - ) |` I ) )
461 460 fveq1d
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( D |` I ) ` <. d , c >. ) = ( ( ( abs o. - ) |` I ) ` <. d , c >. ) )
462 443 3ad2ant2
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. ( A X. A ) )
463 necom
 |-  ( c =/= d <-> d =/= c )
464 463 biimpi
 |-  ( c =/= d -> d =/= c )
465 464 neneqd
 |-  ( c =/= d -> -. d = c )
466 465 3ad2ant3
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> -. d = c )
467 466 455 sylnibr
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> -. <. d , c >. e. _I )
468 462 467 eldifd
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. ( ( A X. A ) \ _I ) )
469 468 10 eleqtrrdi
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. I )
470 fvres
 |-  ( <. d , c >. e. I -> ( ( ( abs o. - ) |` I ) ` <. d , c >. ) = ( ( abs o. - ) ` <. d , c >. ) )
471 469 470 syl
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( ( abs o. - ) |` I ) ` <. d , c >. ) = ( ( abs o. - ) ` <. d , c >. ) )
472 simp1
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ph )
473 472 469 jca
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ph /\ <. d , c >. e. I ) )
474 eleq1
 |-  ( x = <. d , c >. -> ( x e. I <-> <. d , c >. e. I ) )
475 474 anbi2d
 |-  ( x = <. d , c >. -> ( ( ph /\ x e. I ) <-> ( ph /\ <. d , c >. e. I ) ) )
476 eleq1
 |-  ( x = <. d , c >. -> ( x e. dom - <-> <. d , c >. e. dom - ) )
477 475 476 imbi12d
 |-  ( x = <. d , c >. -> ( ( ( ph /\ x e. I ) -> x e. dom - ) <-> ( ( ph /\ <. d , c >. e. I ) -> <. d , c >. e. dom - ) ) )
478 477 76 vtoclg
 |-  ( <. d , c >. e. I -> ( ( ph /\ <. d , c >. e. I ) -> <. d , c >. e. dom - ) )
479 469 473 478 sylc
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. dom - )
480 fvco
 |-  ( ( Fun - /\ <. d , c >. e. dom - ) -> ( ( abs o. - ) ` <. d , c >. ) = ( abs ` ( - ` <. d , c >. ) ) )
481 73 479 480 sylancr
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( abs o. - ) ` <. d , c >. ) = ( abs ` ( - ` <. d , c >. ) ) )
482 df-ov
 |-  ( d - c ) = ( - ` <. d , c >. )
483 482 eqcomi
 |-  ( - ` <. d , c >. ) = ( d - c )
484 483 fveq2i
 |-  ( abs ` ( - ` <. d , c >. ) ) = ( abs ` ( d - c ) )
485 481 484 eqtrdi
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( abs o. - ) ` <. d , c >. ) = ( abs ` ( d - c ) ) )
486 461 471 485 3eqtrd
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( D |` I ) ` <. d , c >. ) = ( abs ` ( d - c ) ) )
487 459 486 syld3an3
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( ( D |` I ) ` <. d , c >. ) = ( abs ` ( d - c ) ) )
488 445 sselda
 |-  ( ( ph /\ d e. A ) -> d e. RR )
489 488 adantrl
 |-  ( ( ph /\ ( c e. A /\ d e. A ) ) -> d e. RR )
490 489 3adant3
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> d e. RR )
491 448 490 449 ltled
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c <_ d )
492 448 490 491 abssubge0d
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( abs ` ( d - c ) ) = ( d - c ) )
493 487 492 eqtrd
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( ( D |` I ) ` <. d , c >. ) = ( d - c ) )
494 fveq2
 |-  ( x = <. d , c >. -> ( ( D |` I ) ` x ) = ( ( D |` I ) ` <. d , c >. ) )
495 494 eqeq1d
 |-  ( x = <. d , c >. -> ( ( ( D |` I ) ` x ) = ( d - c ) <-> ( ( D |` I ) ` <. d , c >. ) = ( d - c ) ) )
496 495 rspcev
 |-  ( ( <. d , c >. e. I /\ ( ( D |` I ) ` <. d , c >. ) = ( d - c ) ) -> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) )
497 458 493 496 syl2anc
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) )
498 489 447 resubcld
 |-  ( ( ph /\ ( c e. A /\ d e. A ) ) -> ( d - c ) e. RR )
499 elex
 |-  ( ( d - c ) e. RR -> ( d - c ) e. _V )
500 498 499 syl
 |-  ( ( ph /\ ( c e. A /\ d e. A ) ) -> ( d - c ) e. _V )
501 500 3adant3
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( d - c ) e. _V )
502 simp1
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ph )
503 eleq1
 |-  ( y = ( d - c ) -> ( y e. ran ( D |` I ) <-> ( d - c ) e. ran ( D |` I ) ) )
504 eqeq2
 |-  ( y = ( d - c ) -> ( ( ( D |` I ) ` x ) = y <-> ( ( D |` I ) ` x ) = ( d - c ) ) )
505 504 rexbidv
 |-  ( y = ( d - c ) -> ( E. x e. I ( ( D |` I ) ` x ) = y <-> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) ) )
506 503 505 bibi12d
 |-  ( y = ( d - c ) -> ( ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) <-> ( ( d - c ) e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) ) ) )
507 506 imbi2d
 |-  ( y = ( d - c ) -> ( ( ph -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) ) <-> ( ph -> ( ( d - c ) e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) ) ) ) )
508 67 424 syl
 |-  ( ph -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) )
509 507 508 vtoclg
 |-  ( ( d - c ) e. _V -> ( ph -> ( ( d - c ) e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) ) ) )
510 501 502 509 sylc
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( ( d - c ) e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) ) )
511 497 510 mpbird
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( d - c ) e. ran ( D |` I ) )
512 511 11 eleqtrrdi
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( d - c ) e. R )
513 infrelb
 |-  ( ( R C_ RR /\ E. x e. RR A. y e. R x <_ y /\ ( d - c ) e. R ) -> inf ( R , RR , < ) <_ ( d - c ) )
514 418 440 512 513 syl3anc
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> inf ( R , RR , < ) <_ ( d - c ) )
515 12 514 eqbrtrid
 |-  ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E <_ ( d - c ) )
516 417 515 vtoclg
 |-  ( B e. A -> ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> E <_ ( d - B ) ) )
517 410 516 mpcom
 |-  ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> E <_ ( d - B ) )
518 409 517 vtoclg
 |-  ( C e. A -> ( ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) -> E <_ ( C - B ) ) )
519 8 402 518 sylc
 |-  ( ph -> E <_ ( C - B ) )
520 519 4 breqtrrdi
 |-  ( ph -> E <_ T )
521 268 520 syl
 |-  ( ps -> E <_ T )
522 521 3ad2ant1
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ T )
523 522 ad2antrr
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> E <_ T )
524 364 adantr
 |-  ( ( ps /\ k e. ZZ ) -> b e. CC )
525 524 366 pncan2d
 |-  ( ( ps /\ k e. ZZ ) -> ( ( b + ( k x. T ) ) - b ) = ( k x. T ) )
526 525 oveq1d
 |-  ( ( ps /\ k e. ZZ ) -> ( ( ( b + ( k x. T ) ) - b ) / T ) = ( ( k x. T ) / T ) )
527 340 adantl
 |-  ( ( ps /\ k e. ZZ ) -> k e. CC )
528 318 adantr
 |-  ( ( ps /\ k e. ZZ ) -> T e. CC )
529 419 a1i
 |-  ( ph -> 0 e. RR )
530 529 350 gtned
 |-  ( ph -> T =/= 0 )
531 268 530 syl
 |-  ( ps -> T =/= 0 )
532 531 adantr
 |-  ( ( ps /\ k e. ZZ ) -> T =/= 0 )
533 527 528 532 divcan4d
 |-  ( ( ps /\ k e. ZZ ) -> ( ( k x. T ) / T ) = k )
534 526 533 eqtr2d
 |-  ( ( ps /\ k e. ZZ ) -> k = ( ( ( b + ( k x. T ) ) - b ) / T ) )
535 534 adantrl
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> k = ( ( ( b + ( k x. T ) ) - b ) / T ) )
536 535 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> k = ( ( ( b + ( k x. T ) ) - b ) / T ) )
537 oveq1
 |-  ( ( a + ( j x. T ) ) = ( b + ( k x. T ) ) -> ( ( a + ( j x. T ) ) - b ) = ( ( b + ( k x. T ) ) - b ) )
538 537 oveq1d
 |-  ( ( a + ( j x. T ) ) = ( b + ( k x. T ) ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) = ( ( ( b + ( k x. T ) ) - b ) / T ) )
539 538 adantl
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) = ( ( ( b + ( k x. T ) ) - b ) / T ) )
540 368 adantr
 |-  ( ( ps /\ j e. ZZ ) -> a e. CC )
541 364 adantr
 |-  ( ( ps /\ j e. ZZ ) -> b e. CC )
542 540 370 541 addsubd
 |-  ( ( ps /\ j e. ZZ ) -> ( ( a + ( j x. T ) ) - b ) = ( ( a - b ) + ( j x. T ) ) )
543 540 541 subcld
 |-  ( ( ps /\ j e. ZZ ) -> ( a - b ) e. CC )
544 543 370 addcomd
 |-  ( ( ps /\ j e. ZZ ) -> ( ( a - b ) + ( j x. T ) ) = ( ( j x. T ) + ( a - b ) ) )
545 542 544 eqtrd
 |-  ( ( ps /\ j e. ZZ ) -> ( ( a + ( j x. T ) ) - b ) = ( ( j x. T ) + ( a - b ) ) )
546 545 oveq1d
 |-  ( ( ps /\ j e. ZZ ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) = ( ( ( j x. T ) + ( a - b ) ) / T ) )
547 318 adantr
 |-  ( ( ps /\ j e. ZZ ) -> T e. CC )
548 531 adantr
 |-  ( ( ps /\ j e. ZZ ) -> T =/= 0 )
549 370 543 547 548 divdird
 |-  ( ( ps /\ j e. ZZ ) -> ( ( ( j x. T ) + ( a - b ) ) / T ) = ( ( ( j x. T ) / T ) + ( ( a - b ) / T ) ) )
550 335 adantl
 |-  ( ( ps /\ j e. ZZ ) -> j e. CC )
551 550 547 548 divcan4d
 |-  ( ( ps /\ j e. ZZ ) -> ( ( j x. T ) / T ) = j )
552 551 oveq1d
 |-  ( ( ps /\ j e. ZZ ) -> ( ( ( j x. T ) / T ) + ( ( a - b ) / T ) ) = ( j + ( ( a - b ) / T ) ) )
553 546 549 552 3eqtrd
 |-  ( ( ps /\ j e. ZZ ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) = ( j + ( ( a - b ) / T ) ) )
554 553 adantrr
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) = ( j + ( ( a - b ) / T ) ) )
555 554 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) = ( j + ( ( a - b ) / T ) ) )
556 536 539 555 3eqtr2d
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> k = ( j + ( ( a - b ) / T ) ) )
557 309 302 resubcld
 |-  ( ps -> ( a - b ) e. RR )
558 309 302 sublt0d
 |-  ( ps -> ( ( a - b ) < 0 <-> a < b ) )
559 358 558 mpbird
 |-  ( ps -> ( a - b ) < 0 )
560 557 352 559 divlt0gt0d
 |-  ( ps -> ( ( a - b ) / T ) < 0 )
561 560 adantr
 |-  ( ( ps /\ j e. ZZ ) -> ( ( a - b ) / T ) < 0 )
562 335 subidd
 |-  ( j e. ZZ -> ( j - j ) = 0 )
563 562 eqcomd
 |-  ( j e. ZZ -> 0 = ( j - j ) )
564 563 adantl
 |-  ( ( ps /\ j e. ZZ ) -> 0 = ( j - j ) )
565 561 564 breqtrd
 |-  ( ( ps /\ j e. ZZ ) -> ( ( a - b ) / T ) < ( j - j ) )
566 557 293 531 redivcld
 |-  ( ps -> ( ( a - b ) / T ) e. RR )
567 566 adantr
 |-  ( ( ps /\ j e. ZZ ) -> ( ( a - b ) / T ) e. RR )
568 311 567 311 ltaddsub2d
 |-  ( ( ps /\ j e. ZZ ) -> ( ( j + ( ( a - b ) / T ) ) < j <-> ( ( a - b ) / T ) < ( j - j ) ) )
569 565 568 mpbird
 |-  ( ( ps /\ j e. ZZ ) -> ( j + ( ( a - b ) / T ) ) < j )
570 569 adantrr
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j + ( ( a - b ) / T ) ) < j )
571 570 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( j + ( ( a - b ) / T ) ) < j )
572 556 571 eqbrtrd
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> k < j )
573 320 ad2antrr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> T = ( 1 x. T ) )
574 simpr
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> k < j )
575 simplr
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> k e. ZZ )
576 simpll
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> j e. ZZ )
577 zltp1le
 |-  ( ( k e. ZZ /\ j e. ZZ ) -> ( k < j <-> ( k + 1 ) <_ j ) )
578 575 576 577 syl2anc
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> ( k < j <-> ( k + 1 ) <_ j ) )
579 574 578 mpbid
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> ( k + 1 ) <_ j )
580 286 ad2antlr
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> k e. RR )
581 330 a1i
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> 1 e. RR )
582 283 ad2antrr
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> j e. RR )
583 580 581 582 leaddsub2d
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> ( ( k + 1 ) <_ j <-> 1 <_ ( j - k ) ) )
584 579 583 mpbid
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> 1 <_ ( j - k ) )
585 584 adantll
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> 1 <_ ( j - k ) )
586 330 a1i
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> 1 e. RR )
587 395 ad2antlr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> ( j - k ) e. RR )
588 352 ad2antrr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> T e. RR+ )
589 586 587 588 lemul1d
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> ( 1 <_ ( j - k ) <-> ( 1 x. T ) <_ ( ( j - k ) x. T ) ) )
590 585 589 mpbid
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> ( 1 x. T ) <_ ( ( j - k ) x. T ) )
591 573 590 eqbrtrd
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> T <_ ( ( j - k ) x. T ) )
592 572 591 syldan
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> T <_ ( ( j - k ) x. T ) )
593 592 adantlr
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> T <_ ( ( j - k ) x. T ) )
594 593 3adantll3
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> T <_ ( ( j - k ) x. T ) )
595 392 394 399 523 594 letrd
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> E <_ ( ( j - k ) x. T ) )
596 oveq2
 |-  ( ( a + ( j x. T ) ) = ( b + ( k x. T ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) = ( ( b + ( k x. T ) ) - ( b + ( k x. T ) ) ) )
597 596 oveq1d
 |-  ( ( a + ( j x. T ) ) = ( b + ( k x. T ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) = ( ( ( b + ( k x. T ) ) - ( b + ( k x. T ) ) ) + ( ( j - k ) x. T ) ) )
598 597 adantl
 |-  ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) = ( ( ( b + ( k x. T ) ) - ( b + ( k x. T ) ) ) + ( ( j - k ) x. T ) ) )
599 268 445 syl
 |-  ( ps -> A C_ RR )
600 599 sselda
 |-  ( ( ps /\ ( b + ( k x. T ) ) e. A ) -> ( b + ( k x. T ) ) e. RR )
601 600 adantrl
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( b + ( k x. T ) ) e. RR )
602 601 recnd
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( b + ( k x. T ) ) e. CC )
603 602 subidd
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( b + ( k x. T ) ) - ( b + ( k x. T ) ) ) = 0 )
604 603 oveq1d
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( b + ( k x. T ) ) - ( b + ( k x. T ) ) ) + ( ( j - k ) x. T ) ) = ( 0 + ( ( j - k ) x. T ) ) )
605 604 adantr
 |-  ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( ( b + ( k x. T ) ) - ( b + ( k x. T ) ) ) + ( ( j - k ) x. T ) ) = ( 0 + ( ( j - k ) x. T ) ) )
606 598 605 eqtrd
 |-  ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) = ( 0 + ( ( j - k ) x. T ) ) )
607 606 3adantl2
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) = ( 0 + ( ( j - k ) x. T ) ) )
608 607 adantlr
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) = ( 0 + ( ( j - k ) x. T ) ) )
609 374 373 subcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j - k ) e. CC )
610 609 375 mulcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( j - k ) x. T ) e. CC )
611 610 addid2d
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( 0 + ( ( j - k ) x. T ) ) = ( ( j - k ) x. T ) )
612 611 3adant3
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( 0 + ( ( j - k ) x. T ) ) = ( ( j - k ) x. T ) )
613 612 ad2antrr
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( 0 + ( ( j - k ) x. T ) ) = ( ( j - k ) x. T ) )
614 608 613 eqtr2d
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( j - k ) x. T ) = ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
615 595 614 breqtrd
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> E <_ ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
616 615 adantlr
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> E <_ ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
617 391 ad3antrrr
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> E e. RR )
618 599 sselda
 |-  ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> ( a + ( j x. T ) ) e. RR )
619 618 adantrr
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) e. RR )
620 601 619 resubcld
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) e. RR )
621 620 3adant2
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) e. RR )
622 621 ad3antrrr
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) e. RR )
623 621 398 readdcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) e. RR )
624 623 ad3antrrr
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) e. RR )
625 268 adantr
 |-  ( ( ps /\ k <_ j ) -> ph )
626 625 3ad2antl1
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> ph )
627 626 ad2antrr
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ph )
628 simpl3
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) )
629 628 ad2antrr
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) )
630 simplr
 |-  ( ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) )
631 619 ad2antrr
 |-  ( ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( a + ( j x. T ) ) e. RR )
632 601 ad2antrr
 |-  ( ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( b + ( k x. T ) ) e. RR )
633 631 632 lenltd
 |-  ( ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) <-> -. ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) )
634 630 633 mpbid
 |-  ( ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> -. ( b + ( k x. T ) ) < ( a + ( j x. T ) ) )
635 eqcom
 |-  ( ( a + ( j x. T ) ) = ( b + ( k x. T ) ) <-> ( b + ( k x. T ) ) = ( a + ( j x. T ) ) )
636 635 notbii
 |-  ( -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) <-> -. ( b + ( k x. T ) ) = ( a + ( j x. T ) ) )
637 636 biimpi
 |-  ( -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) -> -. ( b + ( k x. T ) ) = ( a + ( j x. T ) ) )
638 637 adantl
 |-  ( ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> -. ( b + ( k x. T ) ) = ( a + ( j x. T ) ) )
639 ioran
 |-  ( -. ( ( b + ( k x. T ) ) < ( a + ( j x. T ) ) \/ ( b + ( k x. T ) ) = ( a + ( j x. T ) ) ) <-> ( -. ( b + ( k x. T ) ) < ( a + ( j x. T ) ) /\ -. ( b + ( k x. T ) ) = ( a + ( j x. T ) ) ) )
640 634 638 639 sylanbrc
 |-  ( ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> -. ( ( b + ( k x. T ) ) < ( a + ( j x. T ) ) \/ ( b + ( k x. T ) ) = ( a + ( j x. T ) ) ) )
641 632 631 leloed
 |-  ( ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( b + ( k x. T ) ) <_ ( a + ( j x. T ) ) <-> ( ( b + ( k x. T ) ) < ( a + ( j x. T ) ) \/ ( b + ( k x. T ) ) = ( a + ( j x. T ) ) ) ) )
642 640 641 mtbird
 |-  ( ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> -. ( b + ( k x. T ) ) <_ ( a + ( j x. T ) ) )
643 642 3adantll2
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> -. ( b + ( k x. T ) ) <_ ( a + ( j x. T ) ) )
644 643 adantllr
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> -. ( b + ( k x. T ) ) <_ ( a + ( j x. T ) ) )
645 619 adantr
 |-  ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> ( a + ( j x. T ) ) e. RR )
646 645 3adantl2
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> ( a + ( j x. T ) ) e. RR )
647 646 ad2antrr
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( a + ( j x. T ) ) e. RR )
648 601 adantr
 |-  ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> ( b + ( k x. T ) ) e. RR )
649 648 3adantl2
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> ( b + ( k x. T ) ) e. RR )
650 649 ad2antrr
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( b + ( k x. T ) ) e. RR )
651 647 650 ltnled
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( a + ( j x. T ) ) < ( b + ( k x. T ) ) <-> -. ( b + ( k x. T ) ) <_ ( a + ( j x. T ) ) ) )
652 644 651 mpbird
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( a + ( j x. T ) ) < ( b + ( k x. T ) ) )
653 simp2l
 |-  ( ( ph /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < ( b + ( k x. T ) ) ) -> ( a + ( j x. T ) ) e. A )
654 eleq1
 |-  ( c = ( a + ( j x. T ) ) -> ( c e. A <-> ( a + ( j x. T ) ) e. A ) )
655 654 anbi1d
 |-  ( c = ( a + ( j x. T ) ) -> ( ( c e. A /\ ( b + ( k x. T ) ) e. A ) <-> ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) )
656 breq1
 |-  ( c = ( a + ( j x. T ) ) -> ( c < ( b + ( k x. T ) ) <-> ( a + ( j x. T ) ) < ( b + ( k x. T ) ) ) )
657 655 656 3anbi23d
 |-  ( c = ( a + ( j x. T ) ) -> ( ( ph /\ ( c e. A /\ ( b + ( k x. T ) ) e. A ) /\ c < ( b + ( k x. T ) ) ) <-> ( ph /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < ( b + ( k x. T ) ) ) ) )
658 oveq2
 |-  ( c = ( a + ( j x. T ) ) -> ( ( b + ( k x. T ) ) - c ) = ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
659 658 breq2d
 |-  ( c = ( a + ( j x. T ) ) -> ( E <_ ( ( b + ( k x. T ) ) - c ) <-> E <_ ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) ) )
660 657 659 imbi12d
 |-  ( c = ( a + ( j x. T ) ) -> ( ( ( ph /\ ( c e. A /\ ( b + ( k x. T ) ) e. A ) /\ c < ( b + ( k x. T ) ) ) -> E <_ ( ( b + ( k x. T ) ) - c ) ) <-> ( ( ph /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < ( b + ( k x. T ) ) ) -> E <_ ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) ) ) )
661 simp2r
 |-  ( ( ph /\ ( c e. A /\ ( b + ( k x. T ) ) e. A ) /\ c < ( b + ( k x. T ) ) ) -> ( b + ( k x. T ) ) e. A )
662 eleq1
 |-  ( d = ( b + ( k x. T ) ) -> ( d e. A <-> ( b + ( k x. T ) ) e. A ) )
663 662 anbi2d
 |-  ( d = ( b + ( k x. T ) ) -> ( ( c e. A /\ d e. A ) <-> ( c e. A /\ ( b + ( k x. T ) ) e. A ) ) )
664 breq2
 |-  ( d = ( b + ( k x. T ) ) -> ( c < d <-> c < ( b + ( k x. T ) ) ) )
665 663 664 3anbi23d
 |-  ( d = ( b + ( k x. T ) ) -> ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) <-> ( ph /\ ( c e. A /\ ( b + ( k x. T ) ) e. A ) /\ c < ( b + ( k x. T ) ) ) ) )
666 oveq1
 |-  ( d = ( b + ( k x. T ) ) -> ( d - c ) = ( ( b + ( k x. T ) ) - c ) )
667 666 breq2d
 |-  ( d = ( b + ( k x. T ) ) -> ( E <_ ( d - c ) <-> E <_ ( ( b + ( k x. T ) ) - c ) ) )
668 665 667 imbi12d
 |-  ( d = ( b + ( k x. T ) ) -> ( ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E <_ ( d - c ) ) <-> ( ( ph /\ ( c e. A /\ ( b + ( k x. T ) ) e. A ) /\ c < ( b + ( k x. T ) ) ) -> E <_ ( ( b + ( k x. T ) ) - c ) ) ) )
669 668 515 vtoclg
 |-  ( ( b + ( k x. T ) ) e. A -> ( ( ph /\ ( c e. A /\ ( b + ( k x. T ) ) e. A ) /\ c < ( b + ( k x. T ) ) ) -> E <_ ( ( b + ( k x. T ) ) - c ) ) )
670 661 669 mpcom
 |-  ( ( ph /\ ( c e. A /\ ( b + ( k x. T ) ) e. A ) /\ c < ( b + ( k x. T ) ) ) -> E <_ ( ( b + ( k x. T ) ) - c ) )
671 660 670 vtoclg
 |-  ( ( a + ( j x. T ) ) e. A -> ( ( ph /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < ( b + ( k x. T ) ) ) -> E <_ ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) ) )
672 653 671 mpcom
 |-  ( ( ph /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < ( b + ( k x. T ) ) ) -> E <_ ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
673 627 629 652 672 syl3anc
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> E <_ ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
674 395 ad2antlr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k <_ j ) -> ( j - k ) e. RR )
675 293 ad2antrr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k <_ j ) -> T e. RR )
676 simpr
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k <_ j ) -> k <_ j )
677 283 ad2antrr
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k <_ j ) -> j e. RR )
678 286 ad2antlr
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k <_ j ) -> k e. RR )
679 677 678 subge0d
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k <_ j ) -> ( 0 <_ ( j - k ) <-> k <_ j ) )
680 676 679 mpbird
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k <_ j ) -> 0 <_ ( j - k ) )
681 680 adantll
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k <_ j ) -> 0 <_ ( j - k ) )
682 352 rpge0d
 |-  ( ps -> 0 <_ T )
683 682 ad2antrr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k <_ j ) -> 0 <_ T )
684 674 675 681 683 mulge0d
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k <_ j ) -> 0 <_ ( ( j - k ) x. T ) )
685 684 3adantl3
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> 0 <_ ( ( j - k ) x. T ) )
686 621 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) e. RR )
687 398 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> ( ( j - k ) x. T ) e. RR )
688 686 687 addge01d
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> ( 0 <_ ( ( j - k ) x. T ) <-> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) ) )
689 685 688 mpbid
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
690 689 ad2antrr
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
691 617 622 624 673 690 letrd
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) /\ -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> E <_ ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
692 616 691 pm2.61dan
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) -> E <_ ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
693 372 378 eqtrd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) = ( ( b - a ) + ( ( k - j ) x. T ) ) )
694 693 oveq1d
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) = ( ( ( b - a ) + ( ( k - j ) x. T ) ) + ( ( j - k ) x. T ) ) )
695 365 369 subcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( b - a ) e. CC )
696 373 374 subcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k - j ) e. CC )
697 696 375 mulcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) e. CC )
698 695 697 610 addassd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( b - a ) + ( ( k - j ) x. T ) ) + ( ( j - k ) x. T ) ) = ( ( b - a ) + ( ( ( k - j ) x. T ) + ( ( j - k ) x. T ) ) ) )
699 341 336 336 341 subadd4b
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( ( k - j ) + ( j - k ) ) = ( ( k - k ) + ( j - j ) ) )
700 699 adantl
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) + ( j - k ) ) = ( ( k - k ) + ( j - j ) ) )
701 700 oveq1d
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( k - j ) + ( j - k ) ) x. T ) = ( ( ( k - k ) + ( j - j ) ) x. T ) )
702 696 609 375 adddird
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( k - j ) + ( j - k ) ) x. T ) = ( ( ( k - j ) x. T ) + ( ( j - k ) x. T ) ) )
703 340 subidd
 |-  ( k e. ZZ -> ( k - k ) = 0 )
704 703 adantl
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( k - k ) = 0 )
705 562 adantr
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( j - j ) = 0 )
706 704 705 oveq12d
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( ( k - k ) + ( j - j ) ) = ( 0 + 0 ) )
707 00id
 |-  ( 0 + 0 ) = 0
708 706 707 eqtrdi
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( ( k - k ) + ( j - j ) ) = 0 )
709 708 oveq1d
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( ( ( k - k ) + ( j - j ) ) x. T ) = ( 0 x. T ) )
710 709 adantl
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( k - k ) + ( j - j ) ) x. T ) = ( 0 x. T ) )
711 701 702 710 3eqtr3d
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( k - j ) x. T ) + ( ( j - k ) x. T ) ) = ( 0 x. T ) )
712 711 oveq2d
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b - a ) + ( ( ( k - j ) x. T ) + ( ( j - k ) x. T ) ) ) = ( ( b - a ) + ( 0 x. T ) ) )
713 318 mul02d
 |-  ( ps -> ( 0 x. T ) = 0 )
714 713 oveq2d
 |-  ( ps -> ( ( b - a ) + ( 0 x. T ) ) = ( ( b - a ) + 0 ) )
715 364 368 subcld
 |-  ( ps -> ( b - a ) e. CC )
716 715 addid1d
 |-  ( ps -> ( ( b - a ) + 0 ) = ( b - a ) )
717 714 716 eqtrd
 |-  ( ps -> ( ( b - a ) + ( 0 x. T ) ) = ( b - a ) )
718 717 adantr
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b - a ) + ( 0 x. T ) ) = ( b - a ) )
719 712 718 eqtrd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b - a ) + ( ( ( k - j ) x. T ) + ( ( j - k ) x. T ) ) ) = ( b - a ) )
720 694 698 719 3eqtrd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) = ( b - a ) )
721 720 3adant3
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) = ( b - a ) )
722 721 ad2antrr
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) = ( b - a ) )
723 692 722 breqtrd
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) -> E <_ ( b - a ) )
724 simpll
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ -. ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) -> ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) )
725 simpr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ -. ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) -> -. ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) )
726 601 3adant2
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( b + ( k x. T ) ) e. RR )
727 726 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ -. ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) -> ( b + ( k x. T ) ) e. RR )
728 619 3adant2
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) e. RR )
729 728 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ -. ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) -> ( a + ( j x. T ) ) e. RR )
730 727 729 ltnled
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ -. ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) -> ( ( b + ( k x. T ) ) < ( a + ( j x. T ) ) <-> -. ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) )
731 725 730 mpbird
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ -. ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) -> ( b + ( k x. T ) ) < ( a + ( j x. T ) ) )
732 731 adantlr
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ -. ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) -> ( b + ( k x. T ) ) < ( a + ( j x. T ) ) )
733 535 3adant3
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> k = ( ( ( b + ( k x. T ) ) - b ) / T ) )
734 733 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> k = ( ( ( b + ( k x. T ) ) - b ) / T ) )
735 600 3adant2
 |-  ( ( ps /\ k e. ZZ /\ ( b + ( k x. T ) ) e. A ) -> ( b + ( k x. T ) ) e. RR )
736 302 3ad2ant1
 |-  ( ( ps /\ k e. ZZ /\ ( b + ( k x. T ) ) e. A ) -> b e. RR )
737 735 736 resubcld
 |-  ( ( ps /\ k e. ZZ /\ ( b + ( k x. T ) ) e. A ) -> ( ( b + ( k x. T ) ) - b ) e. RR )
738 293 3ad2ant1
 |-  ( ( ps /\ k e. ZZ /\ ( b + ( k x. T ) ) e. A ) -> T e. RR )
739 531 3ad2ant1
 |-  ( ( ps /\ k e. ZZ /\ ( b + ( k x. T ) ) e. A ) -> T =/= 0 )
740 737 738 739 redivcld
 |-  ( ( ps /\ k e. ZZ /\ ( b + ( k x. T ) ) e. A ) -> ( ( ( b + ( k x. T ) ) - b ) / T ) e. RR )
741 740 3adant3l
 |-  ( ( ps /\ k e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( b + ( k x. T ) ) - b ) / T ) e. RR )
742 741 3adant2l
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( b + ( k x. T ) ) - b ) / T ) e. RR )
743 742 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> ( ( ( b + ( k x. T ) ) - b ) / T ) e. RR )
744 618 3adant2
 |-  ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> ( a + ( j x. T ) ) e. RR )
745 302 3ad2ant1
 |-  ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> b e. RR )
746 744 745 resubcld
 |-  ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> ( ( a + ( j x. T ) ) - b ) e. RR )
747 293 3ad2ant1
 |-  ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> T e. RR )
748 531 3ad2ant1
 |-  ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> T =/= 0 )
749 746 747 748 redivcld
 |-  ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) e. RR )
750 749 3adant3r
 |-  ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) e. RR )
751 750 3adant2r
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) e. RR )
752 751 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) e. RR )
753 284 3ad2ant2
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> j e. RR )
754 753 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> j e. RR )
755 726 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> ( b + ( k x. T ) ) e. RR )
756 302 3ad2ant1
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> b e. RR )
757 756 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> b e. RR )
758 755 757 resubcld
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> ( ( b + ( k x. T ) ) - b ) e. RR )
759 728 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> ( a + ( j x. T ) ) e. RR )
760 759 757 resubcld
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> ( ( a + ( j x. T ) ) - b ) e. RR )
761 352 3ad2ant1
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> T e. RR+ )
762 761 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> T e. RR+ )
763 601 adantr
 |-  ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> ( b + ( k x. T ) ) e. RR )
764 619 adantr
 |-  ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> ( a + ( j x. T ) ) e. RR )
765 302 ad2antrr
 |-  ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> b e. RR )
766 simpr
 |-  ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> ( b + ( k x. T ) ) < ( a + ( j x. T ) ) )
767 763 764 765 766 ltsub1dd
 |-  ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> ( ( b + ( k x. T ) ) - b ) < ( ( a + ( j x. T ) ) - b ) )
768 767 3adantl2
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> ( ( b + ( k x. T ) ) - b ) < ( ( a + ( j x. T ) ) - b ) )
769 758 760 762 768 ltdiv1dd
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> ( ( ( b + ( k x. T ) ) - b ) / T ) < ( ( ( a + ( j x. T ) ) - b ) / T ) )
770 554 570 eqbrtrd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) < j )
771 770 3adant3
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) < j )
772 771 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) < j )
773 743 752 754 769 772 lttrd
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> ( ( ( b + ( k x. T ) ) - b ) / T ) < j )
774 734 773 eqbrtrd
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> k < j )
775 774 adantlr
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> k < j )
776 732 775 syldan
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ -. ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) -> k < j )
777 391 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> E e. RR )
778 393 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> T e. RR )
779 623 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) e. RR )
780 522 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> E <_ T )
781 peano2rem
 |-  ( j e. RR -> ( j - 1 ) e. RR )
782 753 781 syl
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( j - 1 ) e. RR )
783 287 3ad2ant2
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> k e. RR )
784 782 783 resubcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( j - 1 ) - k ) e. RR )
785 784 393 remulcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( j - 1 ) - k ) x. T ) e. RR )
786 785 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> ( ( ( j - 1 ) - k ) x. T ) e. RR )
787 753 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> j e. RR )
788 330 a1i
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> 1 e. RR )
789 787 788 resubcld
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> ( j - 1 ) e. RR )
790 286 ad2antlr
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> k e. RR )
791 790 3ad2antl2
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> k e. RR )
792 789 791 resubcld
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> ( ( j - 1 ) - k ) e. RR )
793 682 adantr
 |-  ( ( ps /\ k < ( j - 1 ) ) -> 0 <_ T )
794 793 3ad2antl1
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> 0 <_ T )
795 283 ad2antrr
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> j e. RR )
796 330 a1i
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> 1 e. RR )
797 795 796 resubcld
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> ( j - 1 ) e. RR )
798 simpr
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> k < ( j - 1 ) )
799 simplr
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> k e. ZZ )
800 simpll
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> j e. ZZ )
801 1zzd
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> 1 e. ZZ )
802 800 801 zsubcld
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> ( j - 1 ) e. ZZ )
803 zltlem1
 |-  ( ( k e. ZZ /\ ( j - 1 ) e. ZZ ) -> ( k < ( j - 1 ) <-> k <_ ( ( j - 1 ) - 1 ) ) )
804 799 802 803 syl2anc
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> ( k < ( j - 1 ) <-> k <_ ( ( j - 1 ) - 1 ) ) )
805 798 804 mpbid
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> k <_ ( ( j - 1 ) - 1 ) )
806 790 797 796 805 lesubd
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> 1 <_ ( ( j - 1 ) - k ) )
807 806 3ad2antl2
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> 1 <_ ( ( j - 1 ) - k ) )
808 778 792 794 807 lemulge12d
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> T <_ ( ( ( j - 1 ) - k ) x. T ) )
809 336 337 341 sub32d
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( ( j - 1 ) - k ) = ( ( j - k ) - 1 ) )
810 809 oveq1d
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( ( ( j - 1 ) - k ) x. T ) = ( ( ( j - k ) - 1 ) x. T ) )
811 810 adantl
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( j - 1 ) - k ) x. T ) = ( ( ( j - k ) - 1 ) x. T ) )
812 1cnd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> 1 e. CC )
813 609 812 375 subdird
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( j - k ) - 1 ) x. T ) = ( ( ( j - k ) x. T ) - ( 1 x. T ) ) )
814 319 oveq2d
 |-  ( ps -> ( ( ( j - k ) x. T ) - ( 1 x. T ) ) = ( ( ( j - k ) x. T ) - T ) )
815 814 adantr
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( j - k ) x. T ) - ( 1 x. T ) ) = ( ( ( j - k ) x. T ) - T ) )
816 811 813 815 3eqtrd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( j - 1 ) - k ) x. T ) = ( ( ( j - k ) x. T ) - T ) )
817 816 3adant3
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( j - 1 ) - k ) x. T ) = ( ( ( j - k ) x. T ) - T ) )
818 728 726 resubcld
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( a + ( j x. T ) ) - ( b + ( k x. T ) ) ) e. RR )
819 270 272 277 275 iccsuble
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( a + ( j x. T ) ) - ( b + ( k x. T ) ) ) <_ ( C - B ) )
820 819 4 breqtrrdi
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( a + ( j x. T ) ) - ( b + ( k x. T ) ) ) <_ T )
821 820 3adant2
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( a + ( j x. T ) ) - ( b + ( k x. T ) ) ) <_ T )
822 818 393 398 821 lesub2dd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( j - k ) x. T ) - T ) <_ ( ( ( j - k ) x. T ) - ( ( a + ( j x. T ) ) - ( b + ( k x. T ) ) ) ) )
823 817 822 eqbrtrd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( j - 1 ) - k ) x. T ) <_ ( ( ( j - k ) x. T ) - ( ( a + ( j x. T ) ) - ( b + ( k x. T ) ) ) ) )
824 610 3adant3
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( j - k ) x. T ) e. CC )
825 728 recnd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) e. CC )
826 602 3adant2
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( b + ( k x. T ) ) e. CC )
827 824 825 826 subsub2d
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( j - k ) x. T ) - ( ( a + ( j x. T ) ) - ( b + ( k x. T ) ) ) ) = ( ( ( j - k ) x. T ) + ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) ) )
828 621 recnd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) e. CC )
829 824 828 addcomd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( j - k ) x. T ) + ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) ) = ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
830 827 829 eqtrd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( j - k ) x. T ) - ( ( a + ( j x. T ) ) - ( b + ( k x. T ) ) ) ) = ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
831 823 830 breqtrd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( ( j - 1 ) - k ) x. T ) <_ ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
832 831 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> ( ( ( j - 1 ) - k ) x. T ) <_ ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
833 778 786 779 808 832 letrd
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> T <_ ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
834 777 778 779 780 833 letrd
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> E <_ ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
835 721 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) = ( b - a ) )
836 834 835 breqtrd
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < ( j - 1 ) ) -> E <_ ( b - a ) )
837 836 adantlr
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < j ) /\ k < ( j - 1 ) ) -> E <_ ( b - a ) )
838 837 adantlr
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < j ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) /\ k < ( j - 1 ) ) -> E <_ ( b - a ) )
839 simplll
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < j ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) /\ -. k < ( j - 1 ) ) -> ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) )
840 simpll2
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < j ) /\ -. k < ( j - 1 ) ) -> ( j e. ZZ /\ k e. ZZ ) )
841 simplr
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < j ) /\ -. k < ( j - 1 ) ) -> k < j )
842 simpr
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < j ) /\ -. k < ( j - 1 ) ) -> -. k < ( j - 1 ) )
843 581 582 580 584 lesubd
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> k <_ ( j - 1 ) )
844 843 3adant3
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j /\ -. k < ( j - 1 ) ) -> k <_ ( j - 1 ) )
845 simpr
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ -. k < ( j - 1 ) ) -> -. k < ( j - 1 ) )
846 284 781 syl
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( j - 1 ) e. RR )
847 846 adantr
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ -. k < ( j - 1 ) ) -> ( j - 1 ) e. RR )
848 286 ad2antlr
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ -. k < ( j - 1 ) ) -> k e. RR )
849 847 848 lenltd
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ -. k < ( j - 1 ) ) -> ( ( j - 1 ) <_ k <-> -. k < ( j - 1 ) ) )
850 845 849 mpbird
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ -. k < ( j - 1 ) ) -> ( j - 1 ) <_ k )
851 850 3adant2
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j /\ -. k < ( j - 1 ) ) -> ( j - 1 ) <_ k )
852 580 3adant3
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j /\ -. k < ( j - 1 ) ) -> k e. RR )
853 846 3ad2ant1
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j /\ -. k < ( j - 1 ) ) -> ( j - 1 ) e. RR )
854 852 853 letri3d
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j /\ -. k < ( j - 1 ) ) -> ( k = ( j - 1 ) <-> ( k <_ ( j - 1 ) /\ ( j - 1 ) <_ k ) ) )
855 844 851 854 mpbir2and
 |-  ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j /\ -. k < ( j - 1 ) ) -> k = ( j - 1 ) )
856 840 841 842 855 syl3anc
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < j ) /\ -. k < ( j - 1 ) ) -> k = ( j - 1 ) )
857 856 adantlr
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < j ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) /\ -. k < ( j - 1 ) ) -> k = ( j - 1 ) )
858 simpl1
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k = ( j - 1 ) ) -> ps )
859 simpl2l
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k = ( j - 1 ) ) -> j e. ZZ )
860 simpl3l
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k = ( j - 1 ) ) -> ( a + ( j x. T ) ) e. A )
861 oveq1
 |-  ( k = ( j - 1 ) -> ( k x. T ) = ( ( j - 1 ) x. T ) )
862 861 oveq2d
 |-  ( k = ( j - 1 ) -> ( b + ( k x. T ) ) = ( b + ( ( j - 1 ) x. T ) ) )
863 862 eqcomd
 |-  ( k = ( j - 1 ) -> ( b + ( ( j - 1 ) x. T ) ) = ( b + ( k x. T ) ) )
864 863 adantl
 |-  ( ( ( b + ( k x. T ) ) e. A /\ k = ( j - 1 ) ) -> ( b + ( ( j - 1 ) x. T ) ) = ( b + ( k x. T ) ) )
865 simpl
 |-  ( ( ( b + ( k x. T ) ) e. A /\ k = ( j - 1 ) ) -> ( b + ( k x. T ) ) e. A )
866 864 865 eqeltrd
 |-  ( ( ( b + ( k x. T ) ) e. A /\ k = ( j - 1 ) ) -> ( b + ( ( j - 1 ) x. T ) ) e. A )
867 866 adantll
 |-  ( ( ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) /\ k = ( j - 1 ) ) -> ( b + ( ( j - 1 ) x. T ) ) e. A )
868 867 3ad2antl3
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k = ( j - 1 ) ) -> ( b + ( ( j - 1 ) x. T ) ) e. A )
869 860 868 jca
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k = ( j - 1 ) ) -> ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) )
870 id
 |-  ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) )
871 870 3adant3r
 |-  ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) )
872 744 adantr
 |-  ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( a + ( j x. T ) ) e. RR )
873 271 3ad2ant1
 |-  ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> C e. RR )
874 873 adantr
 |-  ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> C e. RR )
875 269 adantr
 |-  ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> B e. RR )
876 271 adantr
 |-  ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> C e. RR )
877 elicc2
 |-  ( ( B e. RR /\ C e. RR ) -> ( ( a + ( j x. T ) ) e. ( B [,] C ) <-> ( ( a + ( j x. T ) ) e. RR /\ B <_ ( a + ( j x. T ) ) /\ ( a + ( j x. T ) ) <_ C ) ) )
878 875 876 877 syl2anc
 |-  ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> ( ( a + ( j x. T ) ) e. ( B [,] C ) <-> ( ( a + ( j x. T ) ) e. RR /\ B <_ ( a + ( j x. T ) ) /\ ( a + ( j x. T ) ) <_ C ) ) )
879 276 878 mpbid
 |-  ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> ( ( a + ( j x. T ) ) e. RR /\ B <_ ( a + ( j x. T ) ) /\ ( a + ( j x. T ) ) <_ C ) )
880 879 simp3d
 |-  ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> ( a + ( j x. T ) ) <_ C )
881 880 3adant2
 |-  ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> ( a + ( j x. T ) ) <_ C )
882 881 adantr
 |-  ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( a + ( j x. T ) ) <_ C )
883 nne
 |-  ( -. C =/= ( a + ( j x. T ) ) <-> C = ( a + ( j x. T ) ) )
884 540 370 pncand
 |-  ( ( ps /\ j e. ZZ ) -> ( ( a + ( j x. T ) ) - ( j x. T ) ) = a )
885 884 eqcomd
 |-  ( ( ps /\ j e. ZZ ) -> a = ( ( a + ( j x. T ) ) - ( j x. T ) ) )
886 885 adantr
 |-  ( ( ( ps /\ j e. ZZ ) /\ C = ( a + ( j x. T ) ) ) -> a = ( ( a + ( j x. T ) ) - ( j x. T ) ) )
887 oveq1
 |-  ( C = ( a + ( j x. T ) ) -> ( C - ( j x. T ) ) = ( ( a + ( j x. T ) ) - ( j x. T ) ) )
888 887 eqcomd
 |-  ( C = ( a + ( j x. T ) ) -> ( ( a + ( j x. T ) ) - ( j x. T ) ) = ( C - ( j x. T ) ) )
889 888 adantl
 |-  ( ( ( ps /\ j e. ZZ ) /\ C = ( a + ( j x. T ) ) ) -> ( ( a + ( j x. T ) ) - ( j x. T ) ) = ( C - ( j x. T ) ) )
890 4 oveq2i
 |-  ( B + T ) = ( B + ( C - B ) )
891 268 161 syl
 |-  ( ps -> B e. CC )
892 268 162 syl
 |-  ( ps -> C e. CC )
893 891 892 pncan3d
 |-  ( ps -> ( B + ( C - B ) ) = C )
894 890 893 eqtr2id
 |-  ( ps -> C = ( B + T ) )
895 894 oveq1d
 |-  ( ps -> ( C - ( j x. T ) ) = ( ( B + T ) - ( j x. T ) ) )
896 895 adantr
 |-  ( ( ps /\ j e. ZZ ) -> ( C - ( j x. T ) ) = ( ( B + T ) - ( j x. T ) ) )
897 891 adantr
 |-  ( ( ps /\ j e. ZZ ) -> B e. CC )
898 897 370 547 subsub3d
 |-  ( ( ps /\ j e. ZZ ) -> ( B - ( ( j x. T ) - T ) ) = ( ( B + T ) - ( j x. T ) ) )
899 550 547 mulsubfacd
 |-  ( ( ps /\ j e. ZZ ) -> ( ( j x. T ) - T ) = ( ( j - 1 ) x. T ) )
900 899 oveq2d
 |-  ( ( ps /\ j e. ZZ ) -> ( B - ( ( j x. T ) - T ) ) = ( B - ( ( j - 1 ) x. T ) ) )
901 896 898 900 3eqtr2d
 |-  ( ( ps /\ j e. ZZ ) -> ( C - ( j x. T ) ) = ( B - ( ( j - 1 ) x. T ) ) )
902 901 adantr
 |-  ( ( ( ps /\ j e. ZZ ) /\ C = ( a + ( j x. T ) ) ) -> ( C - ( j x. T ) ) = ( B - ( ( j - 1 ) x. T ) ) )
903 886 889 902 3eqtrd
 |-  ( ( ( ps /\ j e. ZZ ) /\ C = ( a + ( j x. T ) ) ) -> a = ( B - ( ( j - 1 ) x. T ) ) )
904 903 3adantl3
 |-  ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ C = ( a + ( j x. T ) ) ) -> a = ( B - ( ( j - 1 ) x. T ) ) )
905 904 adantlr
 |-  ( ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) /\ C = ( a + ( j x. T ) ) ) -> a = ( B - ( ( j - 1 ) x. T ) ) )
906 oveq1
 |-  ( ( b + ( ( j - 1 ) x. T ) ) = B -> ( ( b + ( ( j - 1 ) x. T ) ) - ( ( j - 1 ) x. T ) ) = ( B - ( ( j - 1 ) x. T ) ) )
907 906 eqcomd
 |-  ( ( b + ( ( j - 1 ) x. T ) ) = B -> ( B - ( ( j - 1 ) x. T ) ) = ( ( b + ( ( j - 1 ) x. T ) ) - ( ( j - 1 ) x. T ) ) )
908 907 ad2antlr
 |-  ( ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) /\ C = ( a + ( j x. T ) ) ) -> ( B - ( ( j - 1 ) x. T ) ) = ( ( b + ( ( j - 1 ) x. T ) ) - ( ( j - 1 ) x. T ) ) )
909 364 ad2antrr
 |-  ( ( ( ps /\ j e. ZZ ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> b e. CC )
910 1cnd
 |-  ( ( ps /\ j e. ZZ ) -> 1 e. CC )
911 550 910 subcld
 |-  ( ( ps /\ j e. ZZ ) -> ( j - 1 ) e. CC )
912 911 547 mulcld
 |-  ( ( ps /\ j e. ZZ ) -> ( ( j - 1 ) x. T ) e. CC )
913 912 adantr
 |-  ( ( ( ps /\ j e. ZZ ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( ( j - 1 ) x. T ) e. CC )
914 909 913 pncand
 |-  ( ( ( ps /\ j e. ZZ ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( ( b + ( ( j - 1 ) x. T ) ) - ( ( j - 1 ) x. T ) ) = b )
915 914 3adantl3
 |-  ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( ( b + ( ( j - 1 ) x. T ) ) - ( ( j - 1 ) x. T ) ) = b )
916 915 adantr
 |-  ( ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) /\ C = ( a + ( j x. T ) ) ) -> ( ( b + ( ( j - 1 ) x. T ) ) - ( ( j - 1 ) x. T ) ) = b )
917 905 908 916 3eqtrd
 |-  ( ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) /\ C = ( a + ( j x. T ) ) ) -> a = b )
918 883 917 sylan2b
 |-  ( ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) /\ -. C =/= ( a + ( j x. T ) ) ) -> a = b )
919 309 358 ltned
 |-  ( ps -> a =/= b )
920 919 neneqd
 |-  ( ps -> -. a = b )
921 920 3ad2ant1
 |-  ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> -. a = b )
922 921 ad2antrr
 |-  ( ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) /\ -. C =/= ( a + ( j x. T ) ) ) -> -. a = b )
923 918 922 condan
 |-  ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> C =/= ( a + ( j x. T ) ) )
924 872 874 882 923 leneltd
 |-  ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( a + ( j x. T ) ) < C )
925 871 924 sylan
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( a + ( j x. T ) ) < C )
926 268 ad2antrr
 |-  ( ( ( ps /\ ( a + ( j x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < C ) -> ph )
927 simplr
 |-  ( ( ( ps /\ ( a + ( j x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < C ) -> ( a + ( j x. T ) ) e. A )
928 926 8 syl
 |-  ( ( ( ps /\ ( a + ( j x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < C ) -> C e. A )
929 simpr
 |-  ( ( ( ps /\ ( a + ( j x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < C ) -> ( a + ( j x. T ) ) < C )
930 simp2l
 |-  ( ( ph /\ ( ( a + ( j x. T ) ) e. A /\ C e. A ) /\ ( a + ( j x. T ) ) < C ) -> ( a + ( j x. T ) ) e. A )
931 654 anbi1d
 |-  ( c = ( a + ( j x. T ) ) -> ( ( c e. A /\ C e. A ) <-> ( ( a + ( j x. T ) ) e. A /\ C e. A ) ) )
932 breq1
 |-  ( c = ( a + ( j x. T ) ) -> ( c < C <-> ( a + ( j x. T ) ) < C ) )
933 931 932 3anbi23d
 |-  ( c = ( a + ( j x. T ) ) -> ( ( ph /\ ( c e. A /\ C e. A ) /\ c < C ) <-> ( ph /\ ( ( a + ( j x. T ) ) e. A /\ C e. A ) /\ ( a + ( j x. T ) ) < C ) ) )
934 oveq2
 |-  ( c = ( a + ( j x. T ) ) -> ( C - c ) = ( C - ( a + ( j x. T ) ) ) )
935 934 breq2d
 |-  ( c = ( a + ( j x. T ) ) -> ( E <_ ( C - c ) <-> E <_ ( C - ( a + ( j x. T ) ) ) ) )
936 933 935 imbi12d
 |-  ( c = ( a + ( j x. T ) ) -> ( ( ( ph /\ ( c e. A /\ C e. A ) /\ c < C ) -> E <_ ( C - c ) ) <-> ( ( ph /\ ( ( a + ( j x. T ) ) e. A /\ C e. A ) /\ ( a + ( j x. T ) ) < C ) -> E <_ ( C - ( a + ( j x. T ) ) ) ) ) )
937 simp2r
 |-  ( ( ph /\ ( c e. A /\ C e. A ) /\ c < C ) -> C e. A )
938 403 anbi2d
 |-  ( d = C -> ( ( c e. A /\ d e. A ) <-> ( c e. A /\ C e. A ) ) )
939 breq2
 |-  ( d = C -> ( c < d <-> c < C ) )
940 938 939 3anbi23d
 |-  ( d = C -> ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) <-> ( ph /\ ( c e. A /\ C e. A ) /\ c < C ) ) )
941 oveq1
 |-  ( d = C -> ( d - c ) = ( C - c ) )
942 941 breq2d
 |-  ( d = C -> ( E <_ ( d - c ) <-> E <_ ( C - c ) ) )
943 940 942 imbi12d
 |-  ( d = C -> ( ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E <_ ( d - c ) ) <-> ( ( ph /\ ( c e. A /\ C e. A ) /\ c < C ) -> E <_ ( C - c ) ) ) )
944 943 515 vtoclg
 |-  ( C e. A -> ( ( ph /\ ( c e. A /\ C e. A ) /\ c < C ) -> E <_ ( C - c ) ) )
945 937 944 mpcom
 |-  ( ( ph /\ ( c e. A /\ C e. A ) /\ c < C ) -> E <_ ( C - c ) )
946 936 945 vtoclg
 |-  ( ( a + ( j x. T ) ) e. A -> ( ( ph /\ ( ( a + ( j x. T ) ) e. A /\ C e. A ) /\ ( a + ( j x. T ) ) < C ) -> E <_ ( C - ( a + ( j x. T ) ) ) ) )
947 930 946 mpcom
 |-  ( ( ph /\ ( ( a + ( j x. T ) ) e. A /\ C e. A ) /\ ( a + ( j x. T ) ) < C ) -> E <_ ( C - ( a + ( j x. T ) ) ) )
948 926 927 928 929 947 syl121anc
 |-  ( ( ( ps /\ ( a + ( j x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < C ) -> E <_ ( C - ( a + ( j x. T ) ) ) )
949 948 adantlrr
 |-  ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) < C ) -> E <_ ( C - ( a + ( j x. T ) ) ) )
950 949 3adantl2
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( a + ( j x. T ) ) < C ) -> E <_ ( C - ( a + ( j x. T ) ) ) )
951 950 adantlr
 |-  ( ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) /\ ( a + ( j x. T ) ) < C ) -> E <_ ( C - ( a + ( j x. T ) ) ) )
952 892 adantr
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> C e. CC )
953 599 sselda
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( b + ( ( j - 1 ) x. T ) ) e. RR )
954 953 recnd
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( b + ( ( j - 1 ) x. T ) ) e. CC )
955 952 954 npcand
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( ( C - ( b + ( ( j - 1 ) x. T ) ) ) + ( b + ( ( j - 1 ) x. T ) ) ) = C )
956 955 eqcomd
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> C = ( ( C - ( b + ( ( j - 1 ) x. T ) ) ) + ( b + ( ( j - 1 ) x. T ) ) ) )
957 956 oveq1d
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( C - ( a + ( j x. T ) ) ) = ( ( ( C - ( b + ( ( j - 1 ) x. T ) ) ) + ( b + ( ( j - 1 ) x. T ) ) ) - ( a + ( j x. T ) ) ) )
958 957 adantrl
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( C - ( a + ( j x. T ) ) ) = ( ( ( C - ( b + ( ( j - 1 ) x. T ) ) ) + ( b + ( ( j - 1 ) x. T ) ) ) - ( a + ( j x. T ) ) ) )
959 958 3adant2
 |-  ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( C - ( a + ( j x. T ) ) ) = ( ( ( C - ( b + ( ( j - 1 ) x. T ) ) ) + ( b + ( ( j - 1 ) x. T ) ) ) - ( a + ( j x. T ) ) ) )
960 959 adantr
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( C - ( a + ( j x. T ) ) ) = ( ( ( C - ( b + ( ( j - 1 ) x. T ) ) ) + ( b + ( ( j - 1 ) x. T ) ) ) - ( a + ( j x. T ) ) ) )
961 oveq2
 |-  ( ( b + ( ( j - 1 ) x. T ) ) = B -> ( C - ( b + ( ( j - 1 ) x. T ) ) ) = ( C - B ) )
962 961 oveq1d
 |-  ( ( b + ( ( j - 1 ) x. T ) ) = B -> ( ( C - ( b + ( ( j - 1 ) x. T ) ) ) + ( b + ( ( j - 1 ) x. T ) ) ) = ( ( C - B ) + ( b + ( ( j - 1 ) x. T ) ) ) )
963 962 oveq1d
 |-  ( ( b + ( ( j - 1 ) x. T ) ) = B -> ( ( ( C - ( b + ( ( j - 1 ) x. T ) ) ) + ( b + ( ( j - 1 ) x. T ) ) ) - ( a + ( j x. T ) ) ) = ( ( ( C - B ) + ( b + ( ( j - 1 ) x. T ) ) ) - ( a + ( j x. T ) ) ) )
964 963 adantl
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( ( ( C - ( b + ( ( j - 1 ) x. T ) ) ) + ( b + ( ( j - 1 ) x. T ) ) ) - ( a + ( j x. T ) ) ) = ( ( ( C - B ) + ( b + ( ( j - 1 ) x. T ) ) ) - ( a + ( j x. T ) ) ) )
965 4 eqcomi
 |-  ( C - B ) = T
966 965 oveq1i
 |-  ( ( C - B ) + ( b + ( ( j - 1 ) x. T ) ) ) = ( T + ( b + ( ( j - 1 ) x. T ) ) )
967 966 a1i
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( ( C - B ) + ( b + ( ( j - 1 ) x. T ) ) ) = ( T + ( b + ( ( j - 1 ) x. T ) ) ) )
968 318 adantr
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> T e. CC )
969 968 954 addcomd
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( T + ( b + ( ( j - 1 ) x. T ) ) ) = ( ( b + ( ( j - 1 ) x. T ) ) + T ) )
970 967 969 eqtrd
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( ( C - B ) + ( b + ( ( j - 1 ) x. T ) ) ) = ( ( b + ( ( j - 1 ) x. T ) ) + T ) )
971 970 oveq1d
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( ( ( C - B ) + ( b + ( ( j - 1 ) x. T ) ) ) - ( a + ( j x. T ) ) ) = ( ( ( b + ( ( j - 1 ) x. T ) ) + T ) - ( a + ( j x. T ) ) ) )
972 971 adantrl
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( ( C - B ) + ( b + ( ( j - 1 ) x. T ) ) ) - ( a + ( j x. T ) ) ) = ( ( ( b + ( ( j - 1 ) x. T ) ) + T ) - ( a + ( j x. T ) ) ) )
973 972 3adant2
 |-  ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( ( C - B ) + ( b + ( ( j - 1 ) x. T ) ) ) - ( a + ( j x. T ) ) ) = ( ( ( b + ( ( j - 1 ) x. T ) ) + T ) - ( a + ( j x. T ) ) ) )
974 973 adantr
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( ( ( C - B ) + ( b + ( ( j - 1 ) x. T ) ) ) - ( a + ( j x. T ) ) ) = ( ( ( b + ( ( j - 1 ) x. T ) ) + T ) - ( a + ( j x. T ) ) ) )
975 954 adantrl
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( b + ( ( j - 1 ) x. T ) ) e. CC )
976 975 3adant2
 |-  ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( b + ( ( j - 1 ) x. T ) ) e. CC )
977 976 adantr
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( b + ( ( j - 1 ) x. T ) ) e. CC )
978 318 3ad2ant1
 |-  ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> T e. CC )
979 978 adantr
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> T e. CC )
980 618 adantrr
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) e. RR )
981 980 recnd
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) e. CC )
982 981 3adant2
 |-  ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) e. CC )
983 982 adantr
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( a + ( j x. T ) ) e. CC )
984 977 979 983 addsubd
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( ( ( b + ( ( j - 1 ) x. T ) ) + T ) - ( a + ( j x. T ) ) ) = ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
985 974 984 eqtrd
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( ( ( C - B ) + ( b + ( ( j - 1 ) x. T ) ) ) - ( a + ( j x. T ) ) ) = ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
986 960 964 985 3eqtrd
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( C - ( a + ( j x. T ) ) ) = ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
987 986 adantr
 |-  ( ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) /\ ( a + ( j x. T ) ) < C ) -> ( C - ( a + ( j x. T ) ) ) = ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
988 951 987 breqtrd
 |-  ( ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) /\ ( a + ( j x. T ) ) < C ) -> E <_ ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
989 925 988 mpdan
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> E <_ ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
990 simpl1
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> ps )
991 simpl3r
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( b + ( ( j - 1 ) x. T ) ) e. A )
992 simpr
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> -. ( b + ( ( j - 1 ) x. T ) ) = B )
993 269 3ad2ant1
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> B e. RR )
994 953 3adant3
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( b + ( ( j - 1 ) x. T ) ) e. RR )
995 273 sselda
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( b + ( ( j - 1 ) x. T ) ) e. ( B [,] C ) )
996 269 adantr
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> B e. RR )
997 271 adantr
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> C e. RR )
998 elicc2
 |-  ( ( B e. RR /\ C e. RR ) -> ( ( b + ( ( j - 1 ) x. T ) ) e. ( B [,] C ) <-> ( ( b + ( ( j - 1 ) x. T ) ) e. RR /\ B <_ ( b + ( ( j - 1 ) x. T ) ) /\ ( b + ( ( j - 1 ) x. T ) ) <_ C ) ) )
999 996 997 998 syl2anc
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( ( b + ( ( j - 1 ) x. T ) ) e. ( B [,] C ) <-> ( ( b + ( ( j - 1 ) x. T ) ) e. RR /\ B <_ ( b + ( ( j - 1 ) x. T ) ) /\ ( b + ( ( j - 1 ) x. T ) ) <_ C ) ) )
1000 995 999 mpbid
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( ( b + ( ( j - 1 ) x. T ) ) e. RR /\ B <_ ( b + ( ( j - 1 ) x. T ) ) /\ ( b + ( ( j - 1 ) x. T ) ) <_ C ) )
1001 1000 simp2d
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> B <_ ( b + ( ( j - 1 ) x. T ) ) )
1002 1001 3adant3
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> B <_ ( b + ( ( j - 1 ) x. T ) ) )
1003 neqne
 |-  ( -. ( b + ( ( j - 1 ) x. T ) ) = B -> ( b + ( ( j - 1 ) x. T ) ) =/= B )
1004 1003 3ad2ant3
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( b + ( ( j - 1 ) x. T ) ) =/= B )
1005 993 994 1002 1004 leneltd
 |-  ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> B < ( b + ( ( j - 1 ) x. T ) ) )
1006 990 991 992 1005 syl3anc
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> B < ( b + ( ( j - 1 ) x. T ) ) )
1007 390 3ad2ant1
 |-  ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> E e. RR )
1008 1007 adantr
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> E e. RR )
1009 953 adantrl
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( b + ( ( j - 1 ) x. T ) ) e. RR )
1010 1009 3adant2
 |-  ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( b + ( ( j - 1 ) x. T ) ) e. RR )
1011 269 3ad2ant1
 |-  ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> B e. RR )
1012 1010 1011 resubcld
 |-  ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( b + ( ( j - 1 ) x. T ) ) - B ) e. RR )
1013 1012 adantr
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> ( ( b + ( ( j - 1 ) x. T ) ) - B ) e. RR )
1014 1009 980 resubcld
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) e. RR )
1015 293 adantr
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> T e. RR )
1016 1014 1015 readdcld
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) e. RR )
1017 1016 3adant2
 |-  ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) e. RR )
1018 1017 adantr
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) e. RR )
1019 268 adantr
 |-  ( ( ps /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> ph )
1020 1019 3ad2antl1
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> ph )
1021 1020 7 syl
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> B e. A )
1022 simpl3r
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> ( b + ( ( j - 1 ) x. T ) ) e. A )
1023 simpr
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> B < ( b + ( ( j - 1 ) x. T ) ) )
1024 simp2r
 |-  ( ( ph /\ ( B e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> ( b + ( ( j - 1 ) x. T ) ) e. A )
1025 eleq1
 |-  ( d = ( b + ( ( j - 1 ) x. T ) ) -> ( d e. A <-> ( b + ( ( j - 1 ) x. T ) ) e. A ) )
1026 1025 anbi2d
 |-  ( d = ( b + ( ( j - 1 ) x. T ) ) -> ( ( B e. A /\ d e. A ) <-> ( B e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) )
1027 breq2
 |-  ( d = ( b + ( ( j - 1 ) x. T ) ) -> ( B < d <-> B < ( b + ( ( j - 1 ) x. T ) ) ) )
1028 1026 1027 3anbi23d
 |-  ( d = ( b + ( ( j - 1 ) x. T ) ) -> ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) <-> ( ph /\ ( B e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) ) )
1029 oveq1
 |-  ( d = ( b + ( ( j - 1 ) x. T ) ) -> ( d - B ) = ( ( b + ( ( j - 1 ) x. T ) ) - B ) )
1030 1029 breq2d
 |-  ( d = ( b + ( ( j - 1 ) x. T ) ) -> ( E <_ ( d - B ) <-> E <_ ( ( b + ( ( j - 1 ) x. T ) ) - B ) ) )
1031 1028 1030 imbi12d
 |-  ( d = ( b + ( ( j - 1 ) x. T ) ) -> ( ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> E <_ ( d - B ) ) <-> ( ( ph /\ ( B e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> E <_ ( ( b + ( ( j - 1 ) x. T ) ) - B ) ) ) )
1032 1031 517 vtoclg
 |-  ( ( b + ( ( j - 1 ) x. T ) ) e. A -> ( ( ph /\ ( B e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> E <_ ( ( b + ( ( j - 1 ) x. T ) ) - B ) ) )
1033 1024 1032 mpcom
 |-  ( ( ph /\ ( B e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> E <_ ( ( b + ( ( j - 1 ) x. T ) ) - B ) )
1034 1020 1021 1022 1023 1033 syl121anc
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> E <_ ( ( b + ( ( j - 1 ) x. T ) ) - B ) )
1035 269 adantr
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> B e. RR )
1036 980 1035 resubcld
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( a + ( j x. T ) ) - B ) e. RR )
1037 965 1015 eqeltrid
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( C - B ) e. RR )
1038 271 adantr
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> C e. RR )
1039 880 adantrr
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) <_ C )
1040 980 1038 1035 1039 lesub1dd
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( a + ( j x. T ) ) - B ) <_ ( C - B ) )
1041 1036 1037 1014 1040 leadd2dd
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + ( ( a + ( j x. T ) ) - B ) ) <_ ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + ( C - B ) ) )
1042 975 981 npcand
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + ( a + ( j x. T ) ) ) = ( b + ( ( j - 1 ) x. T ) ) )
1043 1042 eqcomd
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( b + ( ( j - 1 ) x. T ) ) = ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + ( a + ( j x. T ) ) ) )
1044 1043 oveq1d
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( b + ( ( j - 1 ) x. T ) ) - B ) = ( ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + ( a + ( j x. T ) ) ) - B ) )
1045 1014 recnd
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) e. CC )
1046 891 adantr
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> B e. CC )
1047 1045 981 1046 addsubassd
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + ( a + ( j x. T ) ) ) - B ) = ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + ( ( a + ( j x. T ) ) - B ) ) )
1048 1044 1047 eqtrd
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( b + ( ( j - 1 ) x. T ) ) - B ) = ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + ( ( a + ( j x. T ) ) - B ) ) )
1049 4 oveq2i
 |-  ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) = ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + ( C - B ) )
1050 1049 a1i
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) = ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + ( C - B ) ) )
1051 1041 1048 1050 3brtr4d
 |-  ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( b + ( ( j - 1 ) x. T ) ) - B ) <_ ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
1052 1051 3adant2
 |-  ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( b + ( ( j - 1 ) x. T ) ) - B ) <_ ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
1053 1052 adantr
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> ( ( b + ( ( j - 1 ) x. T ) ) - B ) <_ ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
1054 1008 1013 1018 1034 1053 letrd
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> E <_ ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
1055 1006 1054 syldan
 |-  ( ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> E <_ ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
1056 989 1055 pm2.61dan
 |-  ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> E <_ ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
1057 858 859 869 1056 syl3anc
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k = ( j - 1 ) ) -> E <_ ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
1058 720 eqcomd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( b - a ) = ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
1059 1058 adantr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k = ( j - 1 ) ) -> ( b - a ) = ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
1060 862 oveq1d
 |-  ( k = ( j - 1 ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) = ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) )
1061 1060 adantl
 |-  ( ( ( ps /\ j e. ZZ ) /\ k = ( j - 1 ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) = ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) )
1062 oveq2
 |-  ( k = ( j - 1 ) -> ( j - k ) = ( j - ( j - 1 ) ) )
1063 1062 oveq1d
 |-  ( k = ( j - 1 ) -> ( ( j - k ) x. T ) = ( ( j - ( j - 1 ) ) x. T ) )
1064 1063 adantl
 |-  ( ( ( ps /\ j e. ZZ ) /\ k = ( j - 1 ) ) -> ( ( j - k ) x. T ) = ( ( j - ( j - 1 ) ) x. T ) )
1065 1cnd
 |-  ( j e. ZZ -> 1 e. CC )
1066 335 1065 nncand
 |-  ( j e. ZZ -> ( j - ( j - 1 ) ) = 1 )
1067 1066 oveq1d
 |-  ( j e. ZZ -> ( ( j - ( j - 1 ) ) x. T ) = ( 1 x. T ) )
1068 1067 ad2antlr
 |-  ( ( ( ps /\ j e. ZZ ) /\ k = ( j - 1 ) ) -> ( ( j - ( j - 1 ) ) x. T ) = ( 1 x. T ) )
1069 319 ad2antrr
 |-  ( ( ( ps /\ j e. ZZ ) /\ k = ( j - 1 ) ) -> ( 1 x. T ) = T )
1070 1064 1068 1069 3eqtrd
 |-  ( ( ( ps /\ j e. ZZ ) /\ k = ( j - 1 ) ) -> ( ( j - k ) x. T ) = T )
1071 1061 1070 oveq12d
 |-  ( ( ( ps /\ j e. ZZ ) /\ k = ( j - 1 ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) = ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
1072 1071 adantlrr
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k = ( j - 1 ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) = ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) )
1073 1059 1072 eqtr2d
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k = ( j - 1 ) ) -> ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) = ( b - a ) )
1074 1073 3adantl3
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k = ( j - 1 ) ) -> ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) = ( b - a ) )
1075 1057 1074 breqtrd
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k = ( j - 1 ) ) -> E <_ ( b - a ) )
1076 839 857 1075 syl2anc
 |-  ( ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < j ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) /\ -. k < ( j - 1 ) ) -> E <_ ( b - a ) )
1077 838 1076 pm2.61dan
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k < j ) /\ ( b + ( k x. T ) ) < ( a + ( j x. T ) ) ) -> E <_ ( b - a ) )
1078 724 776 732 1077 syl21anc
 |-  ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ -. ( a + ( j x. T ) ) <_ ( b + ( k x. T ) ) ) -> E <_ ( b - a ) )
1079 723 1078 pm2.61dan
 |-  ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> E <_ ( b - a ) )
1080 387 1079 mpdan
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ ( b - a ) )
1081 309 302 358 ltled
 |-  ( ps -> a <_ b )
1082 309 302 1081 abssuble0d
 |-  ( ps -> ( abs ` ( a - b ) ) = ( b - a ) )
1083 1082 eqcomd
 |-  ( ps -> ( b - a ) = ( abs ` ( a - b ) ) )
1084 1083 3ad2ant1
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( b - a ) = ( abs ` ( a - b ) ) )
1085 1080 1084 breqtrd
 |-  ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( a - b ) ) )
1086 1085 3exp
 |-  ( ps -> ( ( j e. ZZ /\ k e. ZZ ) -> ( ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) -> E <_ ( abs ` ( a - b ) ) ) ) )
1087 1086 rexlimdvv
 |-  ( ps -> ( E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) -> E <_ ( abs ` ( a - b ) ) ) )
1088 265 1087 mpd
 |-  ( ps -> E <_ ( abs ` ( a - b ) ) )
1089 18 1088 sylbir
 |-  ( ( ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( a - b ) ) )
1090 264 1089 chvarvv
 |-  ( ( ( ph /\ ( y e. RR /\ b e. RR /\ y < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( y - b ) ) )
1091 251 1090 chvarvv
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y < z ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( y - z ) ) )
1092 231 237 238 1091 syl21anc
 |-  ( ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) /\ y < z ) -> E <_ ( abs ` ( y - z ) ) )
1093 simpr
 |-  ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> -. y < z )
1094 simpl3
 |-  ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> y =/= z )
1095 simpl1
 |-  ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> y e. RR )
1096 simpl2
 |-  ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> z e. RR )
1097 1095 1096 lttri2d
 |-  ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> ( y =/= z <-> ( y < z \/ z < y ) ) )
1098 1094 1097 mpbid
 |-  ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> ( y < z \/ z < y ) )
1099 1098 ord
 |-  ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> ( -. y < z -> z < y ) )
1100 1093 1099 mpd
 |-  ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> z < y )
1101 1100 adantll
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ -. y < z ) -> z < y )
1102 1101 adantlr
 |-  ( ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) /\ -. y < z ) -> z < y )
1103 simplll
 |-  ( ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) /\ z < y ) -> ph )
1104 simplr
 |-  ( ( ( y e. RR /\ z e. RR ) /\ z < y ) -> z e. RR )
1105 simpll
 |-  ( ( ( y e. RR /\ z e. RR ) /\ z < y ) -> y e. RR )
1106 simpr
 |-  ( ( ( y e. RR /\ z e. RR ) /\ z < y ) -> z < y )
1107 1104 1105 1106 3jca
 |-  ( ( ( y e. RR /\ z e. RR ) /\ z < y ) -> ( z e. RR /\ y e. RR /\ z < y ) )
1108 1107 adantll
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ z < y ) -> ( z e. RR /\ y e. RR /\ z < y ) )
1109 1108 adantlr
 |-  ( ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) /\ z < y ) -> ( z e. RR /\ y e. RR /\ z < y ) )
1110 oveq1
 |-  ( j = i -> ( j x. T ) = ( i x. T ) )
1111 1110 oveq2d
 |-  ( j = i -> ( y + ( j x. T ) ) = ( y + ( i x. T ) ) )
1112 1111 eleq1d
 |-  ( j = i -> ( ( y + ( j x. T ) ) e. A <-> ( y + ( i x. T ) ) e. A ) )
1113 1112 anbi1d
 |-  ( j = i -> ( ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) <-> ( ( y + ( i x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) )
1114 oveq1
 |-  ( k = l -> ( k x. T ) = ( l x. T ) )
1115 1114 oveq2d
 |-  ( k = l -> ( z + ( k x. T ) ) = ( z + ( l x. T ) ) )
1116 1115 eleq1d
 |-  ( k = l -> ( ( z + ( k x. T ) ) e. A <-> ( z + ( l x. T ) ) e. A ) )
1117 1116 anbi2d
 |-  ( k = l -> ( ( ( y + ( i x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) <-> ( ( y + ( i x. T ) ) e. A /\ ( z + ( l x. T ) ) e. A ) ) )
1118 1113 1117 cbvrex2vw
 |-  ( E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) <-> E. i e. ZZ E. l e. ZZ ( ( y + ( i x. T ) ) e. A /\ ( z + ( l x. T ) ) e. A ) )
1119 oveq1
 |-  ( i = k -> ( i x. T ) = ( k x. T ) )
1120 1119 oveq2d
 |-  ( i = k -> ( y + ( i x. T ) ) = ( y + ( k x. T ) ) )
1121 1120 eleq1d
 |-  ( i = k -> ( ( y + ( i x. T ) ) e. A <-> ( y + ( k x. T ) ) e. A ) )
1122 1121 anbi1d
 |-  ( i = k -> ( ( ( y + ( i x. T ) ) e. A /\ ( z + ( l x. T ) ) e. A ) <-> ( ( y + ( k x. T ) ) e. A /\ ( z + ( l x. T ) ) e. A ) ) )
1123 oveq1
 |-  ( l = j -> ( l x. T ) = ( j x. T ) )
1124 1123 oveq2d
 |-  ( l = j -> ( z + ( l x. T ) ) = ( z + ( j x. T ) ) )
1125 1124 eleq1d
 |-  ( l = j -> ( ( z + ( l x. T ) ) e. A <-> ( z + ( j x. T ) ) e. A ) )
1126 1125 anbi2d
 |-  ( l = j -> ( ( ( y + ( k x. T ) ) e. A /\ ( z + ( l x. T ) ) e. A ) <-> ( ( y + ( k x. T ) ) e. A /\ ( z + ( j x. T ) ) e. A ) ) )
1127 1122 1126 cbvrex2vw
 |-  ( E. i e. ZZ E. l e. ZZ ( ( y + ( i x. T ) ) e. A /\ ( z + ( l x. T ) ) e. A ) <-> E. k e. ZZ E. j e. ZZ ( ( y + ( k x. T ) ) e. A /\ ( z + ( j x. T ) ) e. A ) )
1128 rexcom
 |-  ( E. k e. ZZ E. j e. ZZ ( ( y + ( k x. T ) ) e. A /\ ( z + ( j x. T ) ) e. A ) <-> E. j e. ZZ E. k e. ZZ ( ( y + ( k x. T ) ) e. A /\ ( z + ( j x. T ) ) e. A ) )
1129 ancom
 |-  ( ( ( y + ( k x. T ) ) e. A /\ ( z + ( j x. T ) ) e. A ) <-> ( ( z + ( j x. T ) ) e. A /\ ( y + ( k x. T ) ) e. A ) )
1130 1129 2rexbii
 |-  ( E. j e. ZZ E. k e. ZZ ( ( y + ( k x. T ) ) e. A /\ ( z + ( j x. T ) ) e. A ) <-> E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( y + ( k x. T ) ) e. A ) )
1131 1127 1128 1130 3bitri
 |-  ( E. i e. ZZ E. l e. ZZ ( ( y + ( i x. T ) ) e. A /\ ( z + ( l x. T ) ) e. A ) <-> E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( y + ( k x. T ) ) e. A ) )
1132 1118 1131 sylbb
 |-  ( E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) -> E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( y + ( k x. T ) ) e. A ) )
1133 1132 ad2antlr
 |-  ( ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) /\ z < y ) -> E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( y + ( k x. T ) ) e. A ) )
1134 eleq1
 |-  ( b = y -> ( b e. RR <-> y e. RR ) )
1135 breq2
 |-  ( b = y -> ( z < b <-> z < y ) )
1136 1134 1135 3anbi23d
 |-  ( b = y -> ( ( z e. RR /\ b e. RR /\ z < b ) <-> ( z e. RR /\ y e. RR /\ z < y ) ) )
1137 1136 anbi2d
 |-  ( b = y -> ( ( ph /\ ( z e. RR /\ b e. RR /\ z < b ) ) <-> ( ph /\ ( z e. RR /\ y e. RR /\ z < y ) ) ) )
1138 oveq1
 |-  ( b = y -> ( b + ( k x. T ) ) = ( y + ( k x. T ) ) )
1139 1138 eleq1d
 |-  ( b = y -> ( ( b + ( k x. T ) ) e. A <-> ( y + ( k x. T ) ) e. A ) )
1140 1139 anbi2d
 |-  ( b = y -> ( ( ( z + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) <-> ( ( z + ( j x. T ) ) e. A /\ ( y + ( k x. T ) ) e. A ) ) )
1141 1140 2rexbidv
 |-  ( b = y -> ( E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) <-> E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( y + ( k x. T ) ) e. A ) ) )
1142 1137 1141 anbi12d
 |-  ( b = y -> ( ( ( ph /\ ( z e. RR /\ b e. RR /\ z < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) <-> ( ( ph /\ ( z e. RR /\ y e. RR /\ z < y ) ) /\ E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( y + ( k x. T ) ) e. A ) ) ) )
1143 oveq2
 |-  ( b = y -> ( z - b ) = ( z - y ) )
1144 1143 fveq2d
 |-  ( b = y -> ( abs ` ( z - b ) ) = ( abs ` ( z - y ) ) )
1145 1144 breq2d
 |-  ( b = y -> ( E <_ ( abs ` ( z - b ) ) <-> E <_ ( abs ` ( z - y ) ) ) )
1146 1142 1145 imbi12d
 |-  ( b = y -> ( ( ( ( ph /\ ( z e. RR /\ b e. RR /\ z < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( z - b ) ) ) <-> ( ( ( ph /\ ( z e. RR /\ y e. RR /\ z < y ) ) /\ E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( y + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( z - y ) ) ) ) )
1147 eleq1
 |-  ( a = z -> ( a e. RR <-> z e. RR ) )
1148 breq1
 |-  ( a = z -> ( a < b <-> z < b ) )
1149 1147 1148 3anbi13d
 |-  ( a = z -> ( ( a e. RR /\ b e. RR /\ a < b ) <-> ( z e. RR /\ b e. RR /\ z < b ) ) )
1150 1149 anbi2d
 |-  ( a = z -> ( ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) <-> ( ph /\ ( z e. RR /\ b e. RR /\ z < b ) ) ) )
1151 oveq1
 |-  ( a = z -> ( a + ( j x. T ) ) = ( z + ( j x. T ) ) )
1152 1151 eleq1d
 |-  ( a = z -> ( ( a + ( j x. T ) ) e. A <-> ( z + ( j x. T ) ) e. A ) )
1153 1152 anbi1d
 |-  ( a = z -> ( ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) <-> ( ( z + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) )
1154 1153 2rexbidv
 |-  ( a = z -> ( E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) <-> E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) )
1155 1150 1154 anbi12d
 |-  ( a = z -> ( ( ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) <-> ( ( ph /\ ( z e. RR /\ b e. RR /\ z < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) ) )
1156 oveq1
 |-  ( a = z -> ( a - b ) = ( z - b ) )
1157 1156 fveq2d
 |-  ( a = z -> ( abs ` ( a - b ) ) = ( abs ` ( z - b ) ) )
1158 1157 breq2d
 |-  ( a = z -> ( E <_ ( abs ` ( a - b ) ) <-> E <_ ( abs ` ( z - b ) ) ) )
1159 1155 1158 imbi12d
 |-  ( a = z -> ( ( ( ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( a - b ) ) ) <-> ( ( ( ph /\ ( z e. RR /\ b e. RR /\ z < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( z - b ) ) ) ) )
1160 1159 1089 chvarvv
 |-  ( ( ( ph /\ ( z e. RR /\ b e. RR /\ z < b ) ) /\ E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( z - b ) ) )
1161 1146 1160 chvarvv
 |-  ( ( ( ph /\ ( z e. RR /\ y e. RR /\ z < y ) ) /\ E. j e. ZZ E. k e. ZZ ( ( z + ( j x. T ) ) e. A /\ ( y + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( z - y ) ) )
1162 1103 1109 1133 1161 syl21anc
 |-  ( ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) /\ z < y ) -> E <_ ( abs ` ( z - y ) ) )
1163 recn
 |-  ( z e. RR -> z e. CC )
1164 1163 adantl
 |-  ( ( y e. RR /\ z e. RR ) -> z e. CC )
1165 recn
 |-  ( y e. RR -> y e. CC )
1166 1165 adantr
 |-  ( ( y e. RR /\ z e. RR ) -> y e. CC )
1167 1164 1166 abssubd
 |-  ( ( y e. RR /\ z e. RR ) -> ( abs ` ( z - y ) ) = ( abs ` ( y - z ) ) )
1168 1167 adantl
 |-  ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> ( abs ` ( z - y ) ) = ( abs ` ( y - z ) ) )
1169 1168 ad2antrr
 |-  ( ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) /\ z < y ) -> ( abs ` ( z - y ) ) = ( abs ` ( y - z ) ) )
1170 1162 1169 breqtrd
 |-  ( ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) /\ z < y ) -> E <_ ( abs ` ( y - z ) ) )
1171 1170 ex
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) -> ( z < y -> E <_ ( abs ` ( y - z ) ) ) )
1172 1171 3adantlr3
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) -> ( z < y -> E <_ ( abs ` ( y - z ) ) ) )
1173 1172 adantr
 |-  ( ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) /\ -. y < z ) -> ( z < y -> E <_ ( abs ` ( y - z ) ) ) )
1174 1102 1173 mpd
 |-  ( ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) /\ -. y < z ) -> E <_ ( abs ` ( y - z ) ) )
1175 1092 1174 pm2.61dan
 |-  ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ E. j e. ZZ E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( y - z ) ) )
1176 198 206 230 1175 syl21anc
 |-  ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> E <_ ( abs ` ( y - z ) ) )
1177 389 ad2antrr
 |-  ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> E e. RR )
1178 200 203 resubcld
 |-  ( ( ph /\ ( y e. H /\ z e. H ) ) -> ( y - z ) e. RR )
1179 1178 recnd
 |-  ( ( ph /\ ( y e. H /\ z e. H ) ) -> ( y - z ) e. CC )
1180 1179 abscld
 |-  ( ( ph /\ ( y e. H /\ z e. H ) ) -> ( abs ` ( y - z ) ) e. RR )
1181 1180 adantr
 |-  ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> ( abs ` ( y - z ) ) e. RR )
1182 1177 1181 lenltd
 |-  ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> ( E <_ ( abs ` ( y - z ) ) <-> -. ( abs ` ( y - z ) ) < E ) )
1183 1176 1182 mpbid
 |-  ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> -. ( abs ` ( y - z ) ) < E )
1184 nan
 |-  ( ( ( ph /\ ( y e. H /\ z e. H ) ) -> -. ( y =/= z /\ ( abs ` ( y - z ) ) < E ) ) <-> ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> -. ( abs ` ( y - z ) ) < E ) )
1185 1183 1184 mpbir
 |-  ( ( ph /\ ( y e. H /\ z e. H ) ) -> -. ( y =/= z /\ ( abs ` ( y - z ) ) < E ) )
1186 1185 ralrimivva
 |-  ( ph -> A. y e. H A. z e. H -. ( y =/= z /\ ( abs ` ( y - z ) ) < E ) )
1187 ralnex2
 |-  ( A. y e. H A. z e. H -. ( y =/= z /\ ( abs ` ( y - z ) ) < E ) <-> -. E. y e. H E. z e. H ( y =/= z /\ ( abs ` ( y - z ) ) < E ) )
1188 1186 1187 sylib
 |-  ( ph -> -. E. y e. H E. z e. H ( y =/= z /\ ( abs ` ( y - z ) ) < E ) )
1189 1188 ad2antrr
 |-  ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> -. E. y e. H E. z e. H ( y =/= z /\ ( abs ` ( y - z ) ) < E ) )
1190 197 1189 pm2.65da
 |-  ( ( ph /\ x e. U. K ) -> -. x e. ( ( limPt ` J ) ` H ) )
1191 1190 intnanrd
 |-  ( ( ph /\ x e. U. K ) -> -. ( x e. ( ( limPt ` J ) ` H ) /\ x e. ( X [,] Y ) ) )
1192 elin
 |-  ( x e. ( ( ( limPt ` J ) ` H ) i^i ( X [,] Y ) ) <-> ( x e. ( ( limPt ` J ) ` H ) /\ x e. ( X [,] Y ) ) )
1193 1191 1192 sylnibr
 |-  ( ( ph /\ x e. U. K ) -> -. x e. ( ( ( limPt ` J ) ` H ) i^i ( X [,] Y ) ) )
1194 26 a1i
 |-  ( ( ph /\ x e. U. K ) -> J e. Top )
1195 27 adantr
 |-  ( ( ph /\ x e. U. K ) -> ( X [,] Y ) C_ RR )
1196 24 adantr
 |-  ( ( ph /\ x e. U. K ) -> H C_ ( X [,] Y ) )
1197 30 16 restlp
 |-  ( ( J e. Top /\ ( X [,] Y ) C_ RR /\ H C_ ( X [,] Y ) ) -> ( ( limPt ` K ) ` H ) = ( ( ( limPt ` J ) ` H ) i^i ( X [,] Y ) ) )
1198 1194 1195 1196 1197 syl3anc
 |-  ( ( ph /\ x e. U. K ) -> ( ( limPt ` K ) ` H ) = ( ( ( limPt ` J ) ` H ) i^i ( X [,] Y ) ) )
1199 1193 1198 neleqtrrd
 |-  ( ( ph /\ x e. U. K ) -> -. x e. ( ( limPt ` K ) ` H ) )
1200 1199 nrexdv
 |-  ( ph -> -. E. x e. U. K x e. ( ( limPt ` K ) ` H ) )
1201 1200 adantr
 |-  ( ( ph /\ -. H e. Fin ) -> -. E. x e. U. K x e. ( ( limPt ` K ) ` H ) )
1202 41 1201 condan
 |-  ( ph -> H e. Fin )