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	sseldi	|- ( 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 )