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	ffvelcdmd	|- ( ( 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	mullidd	|- ( ps -> ( 1 x. T ) = T )
320	319	eqcomd	|- ( ps -> T = ( 1 x. T ) )
321	320	ad2antrr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T = ( 1 x. T ) )
322		simpr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> j < k )
323		zltlem1	|- ( ( j e. ZZ /\ k e. ZZ ) -> ( j < k <-> j <_ ( k - 1 ) ) )
324	323	ad2antlr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( j < k <-> j <_ ( k - 1 ) ) )
325	322 324	mpbid	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> j <_ ( k - 1 ) )
326	284	ad2antlr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> j e. RR )
327		peano2rem	|- ( k e. RR -> ( k - 1 ) e. RR )
328	295 327	syl	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k - 1 ) e. RR )
329	328	adantr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( k - 1 ) e. RR )
330		1re	|- 1 e. RR
331		resubcl	|- ( ( 1 e. RR /\ j e. RR ) -> ( 1 - j ) e. RR )
332	330 326 331	sylancr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( 1 - j ) e. RR )
333		simpr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> j <_ ( k - 1 ) )
334	326 329 332 333	leadd1dd	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( j + ( 1 - j ) ) <_ ( ( k - 1 ) + ( 1 - j ) ) )
335		zcn	|- ( j e. ZZ -> j e. CC )
336	335	adantr	|- ( ( j e. ZZ /\ k e. ZZ ) -> j e. CC )
337		1cnd	|- ( ( j e. ZZ /\ k e. ZZ ) -> 1 e. CC )
338	336 337	pncan3d	|- ( ( j e. ZZ /\ k e. ZZ ) -> ( j + ( 1 - j ) ) = 1 )
339	338	ad2antlr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( j + ( 1 - j ) ) = 1 )
340		zcn	|- ( k e. ZZ -> k e. CC )
341	340	adantl	|- ( ( j e. ZZ /\ k e. ZZ ) -> k e. CC )
342	341 337 336	npncand	|- ( ( j e. ZZ /\ k e. ZZ ) -> ( ( k - 1 ) + ( 1 - j ) ) = ( k - j ) )
343	342	ad2antlr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( ( k - 1 ) + ( 1 - j ) ) = ( k - j ) )
344	334 339 343	3brtr3d	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> 1 <_ ( k - j ) )
345	325 344	syldan	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> 1 <_ ( k - j ) )
346	330	a1i	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> 1 e. RR )
347	297	adantr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( k - j ) e. RR )
348	1 2	posdifd	|- ( ph -> ( B < C <-> 0 < ( C - B ) ) )
349	3 348	mpbid	|- ( ph -> 0 < ( C - B ) )
350	349 4	breqtrrdi	|- ( ph -> 0 < T )
351	292 350	elrpd	|- ( ph -> T e. RR+ )
352	268 351	syl	|- ( ps -> T e. RR+ )
353	352	ad2antrr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T e. RR+ )
354	346 347 353	lemul1d	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( 1 <_ ( k - j ) <-> ( 1 x. T ) <_ ( ( k - j ) x. T ) ) )
355	345 354	mpbid	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( 1 x. T ) <_ ( ( k - j ) x. T ) )
356	321 355	eqbrtrd	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T <_ ( ( k - j ) x. T ) )
357	302 309	resubcld	|- ( ps -> ( b - a ) e. RR )
358	301	simp3d	|- ( ps -> a < b )
359	309 302	posdifd	|- ( ps -> ( a < b <-> 0 < ( b - a ) ) )
360	358 359	mpbid	|- ( ps -> 0 < ( b - a ) )
361	357 360	elrpd	|- ( ps -> ( b - a ) e. RR+ )
362	361	adantr	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( b - a ) e. RR+ )
363	299 362	ltaddrp2d	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) < ( ( b - a ) + ( ( k - j ) x. T ) ) )
364	302	recnd	|- ( ps -> b e. CC )
365	364	adantr	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> b e. CC )
366	306	recnd	|- ( ( ps /\ k e. ZZ ) -> ( k x. T ) e. CC )
367	366	adantrl	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k x. T ) e. CC )
368	309	recnd	|- ( ps -> a e. CC )
369	368	adantr	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> a e. CC )
370	313	recnd	|- ( ( ps /\ j e. ZZ ) -> ( j x. T ) e. CC )
371	370	adantrr	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j x. T ) e. CC )
372	365 367 369 371	addsub4d	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) = ( ( b - a ) + ( ( k x. T ) - ( j x. T ) ) ) )
373	340	ad2antll	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> k e. CC )
374	335	ad2antrl	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> j e. CC )
375	318	adantr	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> T e. CC )
376	373 374 375	subdird	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) = ( ( k x. T ) - ( j x. T ) ) )
377	376	eqcomd	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k x. T ) - ( j x. T ) ) = ( ( k - j ) x. T ) )
378	377	oveq2d	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b - a ) + ( ( k x. T ) - ( j x. T ) ) ) = ( ( b - a ) + ( ( k - j ) x. T ) ) )
379	372 378	eqtr2d	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b - a ) + ( ( k - j ) x. T ) ) = ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
380	363 379	breqtrd	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
381	380	adantr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( ( k - j ) x. T ) < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
382	294 300 317 356 381	lelttrd	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
383	294 317	ltnled	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( T < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <-> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T ) )
384	382 383	mpbid	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
385	290 384	syldan	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
386	385	3adantl3	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ -. k <_ j ) -> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
387	281 386	condan	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> k <_ j )
388	190 193	sselid	|- ( ph -> inf ( R , RR , < ) e. RR )
389	12 388	eqeltrid	|- ( ph -> E e. RR )
390	268 389	syl	|- ( ps -> E e. RR )
391	390	3ad2ant1	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E e. RR )
392	391	ad2antrr	|- ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> E e. RR )
393	293	3ad2ant1	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> T e. RR )
394	393	ad2antrr	|- ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> T e. RR )
395	284 287	resubcld	|- ( ( j e. ZZ /\ k e. ZZ ) -> ( j - k ) e. RR )
396	395	adantl	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j - k ) e. RR )
397	396 298	remulcld	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( j - k ) x. T ) e. RR )
398	397	3adant3	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( j - k ) x. T ) e. RR )
399	398	ad2antrr	|- ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( ( j - k ) x. T ) e. RR )
400		id	|- ( ph -> ph )
401	7 8	jca	|- ( ph -> ( B e. A /\ C e. A ) )
402	400 401 3	3jca	|- ( ph -> ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) )
403		eleq1	|- ( d = C -> ( d e. A <-> C e. A ) )
404	403	anbi2d	|- ( d = C -> ( ( B e. A /\ d e. A ) <-> ( B e. A /\ C e. A ) ) )
405		breq2	|- ( d = C -> ( B < d <-> B < C ) )
406	404 405	3anbi23d	|- ( d = C -> ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) <-> ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) ) )
407		oveq1	|- ( d = C -> ( d - B ) = ( C - B ) )
408	407	breq2d	|- ( d = C -> ( E <_ ( d - B ) <-> E <_ ( C - B ) ) )
409	406 408	imbi12d	|- ( d = C -> ( ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> E <_ ( d - B ) ) <-> ( ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) -> E <_ ( C - B ) ) ) )
410		simp2l	|- ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> B e. A )
411		eleq1	|- ( c = B -> ( c e. A <-> B e. A ) )
412	411	anbi1d	|- ( c = B -> ( ( c e. A /\ d e. A ) <-> ( B e. A /\ d e. A ) ) )
413		breq1	|- ( c = B -> ( c < d <-> B < d ) )
414	412 413	3anbi23d	|- ( c = B -> ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) <-> ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) ) )
415		oveq2	|- ( c = B -> ( d - c ) = ( d - B ) )
416	415	breq2d	|- ( c = B -> ( E <_ ( d - c ) <-> E <_ ( d - B ) ) )
417	414 416	imbi12d	|- ( c = B -> ( ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E <_ ( d - c ) ) <-> ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> E <_ ( d - B ) ) ) )
418	190	a1i	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> R C_ RR )
419		0re	|- 0 e. RR
420	11	eleq2i	|- ( y e. R <-> y e. ran ( D |` I ) )
421	420	bilani	|- ( ( ph /\ y e. R ) -> y e. ran ( D |` I ) )
422	67	adantr	|- ( ( ph /\ y e. R ) -> ( D |` I ) Fn I )
423		fvelrnb	|- ( ( D |` I ) Fn I -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) )
424	422 423	syl	|- ( ( ph /\ y e. R ) -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) )
425	421 424	mpbid	|- ( ( ph /\ y e. R ) -> E. x e. I ( ( D |` I ) ` x ) = y )
426	127	rpge0d	|- ( ( ph /\ x e. I ) -> 0 <_ ( ( D |` I ) ` x ) )
427	426	3adant3	|- ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> 0 <_ ( ( D |` I ) ` x ) )
428		simp3	|- ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> ( ( D |` I ) ` x ) = y )
429	427 428	breqtrd	|- ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> 0 <_ y )
430	429	3exp	|- ( ph -> ( x e. I -> ( ( ( D |` I ) ` x ) = y -> 0 <_ y ) ) )
431	430	adantr	|- ( ( ph /\ y e. R ) -> ( x e. I -> ( ( ( D |` I ) ` x ) = y -> 0 <_ y ) ) )
432	431	rexlimdv	|- ( ( ph /\ y e. R ) -> ( E. x e. I ( ( D |` I ) ` x ) = y -> 0 <_ y ) )
433	425 432	mpd	|- ( ( ph /\ y e. R ) -> 0 <_ y )
434	433	ralrimiva	|- ( ph -> A. y e. R 0 <_ y )
435		breq1	|- ( x = 0 -> ( x <_ y <-> 0 <_ y ) )
436	435	ralbidv	|- ( x = 0 -> ( A. y e. R x <_ y <-> A. y e. R 0 <_ y ) )
437	436	rspcev	|- ( ( 0 e. RR /\ A. y e. R 0 <_ y ) -> E. x e. RR A. y e. R x <_ y )
438	419 434 437	sylancr	|- ( ph -> E. x e. RR A. y e. R x <_ y )
439	438	3ad2ant1	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E. x e. RR A. y e. R x <_ y )
440		pm3.22	|- ( ( c e. A /\ d e. A ) -> ( d e. A /\ c e. A ) )
441		opelxp	|- ( <. d , c >. e. ( A X. A ) <-> ( d e. A /\ c e. A ) )
442	440 441	sylibr	|- ( ( c e. A /\ d e. A ) -> <. d , c >. e. ( A X. A ) )
443	442	3ad2ant2	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. ( A X. A ) )
444	5 58	sstrd	|- ( ph -> A C_ RR )
445	444	sselda	|- ( ( ph /\ c e. A ) -> c e. RR )
446	445	adantrr	|- ( ( ph /\ ( c e. A /\ d e. A ) ) -> c e. RR )
447	446	3adant3	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c e. RR )
448		simp3	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c < d )
449	447 448	gtned	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> d =/= c )
450	449	neneqd	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> -. d = c )
451		df-br	|- ( d _I c <-> <. d , c >. e. _I )
452		vex	|- c e. _V
453	452	ideq	|- ( d _I c <-> d = c )
454	451 453	bitr3i	|- ( <. d , c >. e. _I <-> d = c )
455	450 454	sylnibr	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> -. <. d , c >. e. _I )
456	443 455	eldifd	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. ( ( A X. A ) \ _I ) )
457	456 10	eleqtrrdi	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. I )
458	447 448	ltned	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c =/= d )
459	146	3ad2ant1	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( D |` I ) = ( ( abs o. - ) |` I ) )
460	459	fveq1d	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( D |` I ) ` <. d , c >. ) = ( ( ( abs o. - ) |` I ) ` <. d , c >. ) )
461	442	3ad2ant2	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. ( A X. A ) )
462		necom	|- ( c =/= d <-> d =/= c )
463	462	biimpi	|- ( c =/= d -> d =/= c )
464	463	neneqd	|- ( c =/= d -> -. d = c )
465	464	3ad2ant3	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> -. d = c )
466	465 454	sylnibr	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> -. <. d , c >. e. _I )
467	461 466	eldifd	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. ( ( A X. A ) \ _I ) )
468	467 10	eleqtrrdi	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. I )
469		fvres	|- ( <. d , c >. e. I -> ( ( ( abs o. - ) |` I ) ` <. d , c >. ) = ( ( abs o. - ) ` <. d , c >. ) )
470	468 469	syl	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( ( abs o. - ) |` I ) ` <. d , c >. ) = ( ( abs o. - ) ` <. d , c >. ) )
471		simp1	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ph )
472	471 468	jca	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ph /\ <. d , c >. e. I ) )
473		eleq1	|- ( x = <. d , c >. -> ( x e. I <-> <. d , c >. e. I ) )
474	473	anbi2d	|- ( x = <. d , c >. -> ( ( ph /\ x e. I ) <-> ( ph /\ <. d , c >. e. I ) ) )
475		eleq1	|- ( x = <. d , c >. -> ( x e. dom - <-> <. d , c >. e. dom - ) )
476	474 475	imbi12d	|- ( x = <. d , c >. -> ( ( ( ph /\ x e. I ) -> x e. dom - ) <-> ( ( ph /\ <. d , c >. e. I ) -> <. d , c >. e. dom - ) ) )
477	476 76	vtoclg	|- ( <. d , c >. e. I -> ( ( ph /\ <. d , c >. e. I ) -> <. d , c >. e. dom - ) )
478	468 472 477	sylc	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. dom - )
479		fvco	|- ( ( Fun - /\ <. d , c >. e. dom - ) -> ( ( abs o. - ) ` <. d , c >. ) = ( abs ` ( - ` <. d , c >. ) ) )
480	73 478 479	sylancr	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( abs o. - ) ` <. d , c >. ) = ( abs ` ( - ` <. d , c >. ) ) )
481		df-ov	|- ( d - c ) = ( - ` <. d , c >. )
482	481	eqcomi	|- ( - ` <. d , c >. ) = ( d - c )
483	482	fveq2i	|- ( abs ` ( - ` <. d , c >. ) ) = ( abs ` ( d - c ) )
484	480 483	eqtrdi	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( abs o. - ) ` <. d , c >. ) = ( abs ` ( d - c ) ) )
485	460 470 484	3eqtrd	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( D |` I ) ` <. d , c >. ) = ( abs ` ( d - c ) ) )
486	458 485	syld3an3	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( ( D |` I ) ` <. d , c >. ) = ( abs ` ( d - c ) ) )
487	444	sselda	|- ( ( ph /\ d e. A ) -> d e. RR )
488	487	adantrl	|- ( ( ph /\ ( c e. A /\ d e. A ) ) -> d e. RR )
489	488	3adant3	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> d e. RR )
490	447 489 448	ltled	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c <_ d )
491	447 489 490	abssubge0d	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( abs ` ( d - c ) ) = ( d - c ) )
492	486 491	eqtrd	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( ( D |` I ) ` <. d , c >. ) = ( d - c ) )
493		fveq2	|- ( x = <. d , c >. -> ( ( D |` I ) ` x ) = ( ( D |` I ) ` <. d , c >. ) )
494	493	eqeq1d	|- ( x = <. d , c >. -> ( ( ( D |` I ) ` x ) = ( d - c ) <-> ( ( D |` I ) ` <. d , c >. ) = ( d - c ) ) )
495	494	rspcev	|- ( ( <. d , c >. e. I /\ ( ( D |` I ) ` <. d , c >. ) = ( d - c ) ) -> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) )
496	457 492 495	syl2anc	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) )
497	488 446	resubcld	|- ( ( ph /\ ( c e. A /\ d e. A ) ) -> ( d - c ) e. RR )
498		elex	|- ( ( d - c ) e. RR -> ( d - c ) e. _V )
499	497 498	syl	|- ( ( ph /\ ( c e. A /\ d e. A ) ) -> ( d - c ) e. _V )
500	499	3adant3	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( d - c ) e. _V )
501		simp1	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ph )
502		eleq1	|- ( y = ( d - c ) -> ( y e. ran ( D |` I ) <-> ( d - c ) e. ran ( D |` I ) ) )
503		eqeq2	|- ( y = ( d - c ) -> ( ( ( D |` I ) ` x ) = y <-> ( ( D |` I ) ` x ) = ( d - c ) ) )
504	503	rexbidv	|- ( y = ( d - c ) -> ( E. x e. I ( ( D |` I ) ` x ) = y <-> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) ) )
505	502 504	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 ) ) ) )
506	505	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 ) ) ) ) )
507	67 423	syl	|- ( ph -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) )
508	506 507	vtoclg	|- ( ( d - c ) e. _V -> ( ph -> ( ( d - c ) e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) ) ) )
509	500 501 508	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 ) ) )
510	496 509	mpbird	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( d - c ) e. ran ( D |` I ) )
511	510 11	eleqtrrdi	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( d - c ) e. R )
512		infrelb	|- ( ( R C_ RR /\ E. x e. RR A. y e. R x <_ y /\ ( d - c ) e. R ) -> inf ( R , RR , < ) <_ ( d - c ) )
513	418 439 511 512	syl3anc	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> inf ( R , RR , < ) <_ ( d - c ) )
514	12 513	eqbrtrid	|- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E <_ ( d - c ) )
515	417 514	vtoclg	|- ( B e. A -> ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> E <_ ( d - B ) ) )
516	410 515	mpcom	|- ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> E <_ ( d - B ) )
517	409 516	vtoclg	|- ( C e. A -> ( ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) -> E <_ ( C - B ) ) )
518	8 402 517	sylc	|- ( ph -> E <_ ( C - B ) )
519	518 4	breqtrrdi	|- ( ph -> E <_ T )
520	268 519	syl	|- ( ps -> E <_ T )
521	520	3ad2ant1	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ T )
522	521	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 )
523	364	adantr	|- ( ( ps /\ k e. ZZ ) -> b e. CC )
524	523 366	pncan2d	|- ( ( ps /\ k e. ZZ ) -> ( ( b + ( k x. T ) ) - b ) = ( k x. T ) )
525	524	oveq1d	|- ( ( ps /\ k e. ZZ ) -> ( ( ( b + ( k x. T ) ) - b ) / T ) = ( ( k x. T ) / T ) )
526	340	adantl	|- ( ( ps /\ k e. ZZ ) -> k e. CC )
527	318	adantr	|- ( ( ps /\ k e. ZZ ) -> T e. CC )
528	419	a1i	|- ( ph -> 0 e. RR )
529	528 350	gtned	|- ( ph -> T =/= 0 )
530	268 529	syl	|- ( ps -> T =/= 0 )
531	530	adantr	|- ( ( ps /\ k e. ZZ ) -> T =/= 0 )
532	526 527 531	divcan4d	|- ( ( ps /\ k e. ZZ ) -> ( ( k x. T ) / T ) = k )
533	525 532	eqtr2d	|- ( ( ps /\ k e. ZZ ) -> k = ( ( ( b + ( k x. T ) ) - b ) / T ) )
534	533	adantrl	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> k = ( ( ( b + ( k x. T ) ) - b ) / T ) )
535	534	adantr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> k = ( ( ( b + ( k x. T ) ) - b ) / T ) )
536		oveq1	|- ( ( a + ( j x. T ) ) = ( b + ( k x. T ) ) -> ( ( a + ( j x. T ) ) - b ) = ( ( b + ( k x. T ) ) - b ) )
537	536	oveq1d	|- ( ( a + ( j x. T ) ) = ( b + ( k x. T ) ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) = ( ( ( b + ( k x. T ) ) - b ) / T ) )
538	537	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 ) )
539	368	adantr	|- ( ( ps /\ j e. ZZ ) -> a e. CC )
540	364	adantr	|- ( ( ps /\ j e. ZZ ) -> b e. CC )
541	539 370 540	addsubd	|- ( ( ps /\ j e. ZZ ) -> ( ( a + ( j x. T ) ) - b ) = ( ( a - b ) + ( j x. T ) ) )
542	539 540	subcld	|- ( ( ps /\ j e. ZZ ) -> ( a - b ) e. CC )
543	542 370	addcomd	|- ( ( ps /\ j e. ZZ ) -> ( ( a - b ) + ( j x. T ) ) = ( ( j x. T ) + ( a - b ) ) )
544	541 543	eqtrd	|- ( ( ps /\ j e. ZZ ) -> ( ( a + ( j x. T ) ) - b ) = ( ( j x. T ) + ( a - b ) ) )
545	544	oveq1d	|- ( ( ps /\ j e. ZZ ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) = ( ( ( j x. T ) + ( a - b ) ) / T ) )
546	318	adantr	|- ( ( ps /\ j e. ZZ ) -> T e. CC )
547	530	adantr	|- ( ( ps /\ j e. ZZ ) -> T =/= 0 )
548	370 542 546 547	divdird	|- ( ( ps /\ j e. ZZ ) -> ( ( ( j x. T ) + ( a - b ) ) / T ) = ( ( ( j x. T ) / T ) + ( ( a - b ) / T ) ) )
549	335	adantl	|- ( ( ps /\ j e. ZZ ) -> j e. CC )
550	549 546 547	divcan4d	|- ( ( ps /\ j e. ZZ ) -> ( ( j x. T ) / T ) = j )
551	550	oveq1d	|- ( ( ps /\ j e. ZZ ) -> ( ( ( j x. T ) / T ) + ( ( a - b ) / T ) ) = ( j + ( ( a - b ) / T ) ) )
552	545 548 551	3eqtrd	|- ( ( ps /\ j e. ZZ ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) = ( j + ( ( a - b ) / T ) ) )
553	552	adantrr	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) = ( j + ( ( a - b ) / T ) ) )
554	553	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 ) ) )
555	535 538 554	3eqtr2d	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> k = ( j + ( ( a - b ) / T ) ) )
556	309 302	resubcld	|- ( ps -> ( a - b ) e. RR )
557	309 302	sublt0d	|- ( ps -> ( ( a - b ) < 0 <-> a < b ) )
558	358 557	mpbird	|- ( ps -> ( a - b ) < 0 )
559	556 352 558	divlt0gt0d	|- ( ps -> ( ( a - b ) / T ) < 0 )
560	559	adantr	|- ( ( ps /\ j e. ZZ ) -> ( ( a - b ) / T ) < 0 )
561	335	subidd	|- ( j e. ZZ -> ( j - j ) = 0 )
562	561	eqcomd	|- ( j e. ZZ -> 0 = ( j - j ) )
563	562	adantl	|- ( ( ps /\ j e. ZZ ) -> 0 = ( j - j ) )
564	560 563	breqtrd	|- ( ( ps /\ j e. ZZ ) -> ( ( a - b ) / T ) < ( j - j ) )
565	556 293 530	redivcld	|- ( ps -> ( ( a - b ) / T ) e. RR )
566	565	adantr	|- ( ( ps /\ j e. ZZ ) -> ( ( a - b ) / T ) e. RR )
567	311 566 311	ltaddsub2d	|- ( ( ps /\ j e. ZZ ) -> ( ( j + ( ( a - b ) / T ) ) < j <-> ( ( a - b ) / T ) < ( j - j ) ) )
568	564 567	mpbird	|- ( ( ps /\ j e. ZZ ) -> ( j + ( ( a - b ) / T ) ) < j )
569	568	adantrr	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j + ( ( a - b ) / T ) ) < j )
570	569	adantr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> ( j + ( ( a - b ) / T ) ) < j )
571	555 570	eqbrtrd	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> k < j )
572	320	ad2antrr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> T = ( 1 x. T ) )
573		simpr	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> k < j )
574		simplr	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> k e. ZZ )
575		simpll	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> j e. ZZ )
576		zltp1le	|- ( ( k e. ZZ /\ j e. ZZ ) -> ( k < j <-> ( k + 1 ) <_ j ) )
577	574 575 576	syl2anc	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> ( k < j <-> ( k + 1 ) <_ j ) )
578	573 577	mpbid	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> ( k + 1 ) <_ j )
579	286	ad2antlr	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> k e. RR )
580	330	a1i	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> 1 e. RR )
581	283	ad2antrr	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> j e. RR )
582	579 580 581	leaddsub2d	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> ( ( k + 1 ) <_ j <-> 1 <_ ( j - k ) ) )
583	578 582	mpbid	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> 1 <_ ( j - k ) )
584	583	adantll	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> 1 <_ ( j - k ) )
585	330	a1i	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> 1 e. RR )
586	395	ad2antlr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> ( j - k ) e. RR )
587	352	ad2antrr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> T e. RR+ )
588	585 586 587	lemul1d	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> ( 1 <_ ( j - k ) <-> ( 1 x. T ) <_ ( ( j - k ) x. T ) ) )
589	584 588	mpbid	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> ( 1 x. T ) <_ ( ( j - k ) x. T ) )
590	572 589	eqbrtrd	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k < j ) -> T <_ ( ( j - k ) x. T ) )
591	571 590	syldan	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> T <_ ( ( j - k ) x. T ) )
592	591	adantlr	|- ( ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k <_ j ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> T <_ ( ( j - k ) x. T ) )
593	592	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 ) )
594	392 394 399 522 593	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 ) )
595		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 ) ) ) )
596	595	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 ) ) )
597	596	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 ) ) )
598	268 444	syl	|- ( ps -> A C_ RR )
599	598	sselda	|- ( ( ps /\ ( b + ( k x. T ) ) e. A ) -> ( b + ( k x. T ) ) e. RR )
600	599	adantrl	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( b + ( k x. T ) ) e. RR )
601	600	recnd	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( b + ( k x. T ) ) e. CC )
602	601	subidd	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( b + ( k x. T ) ) - ( b + ( k x. T ) ) ) = 0 )
603	602	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 ) ) )
604	603	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 ) ) )
605	597 604	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 ) ) )
606	605	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 ) ) )
607	606	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 ) ) )
608	374 373	subcld	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j - k ) e. CC )
609	608 375	mulcld	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( j - k ) x. T ) e. CC )
610	609	addlidd	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( 0 + ( ( j - k ) x. T ) ) = ( ( j - k ) x. T ) )
611	610	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 ) )
612	611	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 ) )
613	607 612	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 ) ) )
614	594 613	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 ) ) )
615	614	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 ) ) )
616	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 )
617	598	sselda	|- ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> ( a + ( j x. T ) ) e. RR )
618	617	adantrr	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) e. RR )
619	600 618	resubcld	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) e. RR )
620	619	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 )
621	620	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 )
622	620 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 )
623	622	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 )
624	268	adantr	|- ( ( ps /\ k <_ j ) -> ph )
625	624	3ad2antl1	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> ph )
626	625	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 )
627		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 ) )
628	627	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 ) )
629		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 ) ) )
630	618	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 )
631	600	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 )
632	630 631	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 ) ) ) )
633	629 632	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 ) ) )
634		eqcom	|- ( ( a + ( j x. T ) ) = ( b + ( k x. T ) ) <-> ( b + ( k x. T ) ) = ( a + ( j x. T ) ) )
635	634	notbii	|- ( -. ( a + ( j x. T ) ) = ( b + ( k x. T ) ) <-> -. ( b + ( k x. T ) ) = ( a + ( j x. T ) ) )
636	635	bilani	|- ( ( ( ( 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 ) ) )
637		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 ) ) ) )
638	633 636 637	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 ) ) ) )
639	631 630	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 ) ) ) ) )
640	638 639	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 ) ) )
641	640	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 ) ) )
642	641	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 ) ) )
643	618	adantr	|- ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> ( a + ( j x. T ) ) e. RR )
644	643	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 )
645	644	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 )
646	600	adantr	|- ( ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k <_ j ) -> ( b + ( k x. T ) ) e. RR )
647	646	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 )
648	647	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 )
649	645 648	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 ) ) ) )
650	642 649	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 ) ) )
651		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 )
652		eleq1	|- ( c = ( a + ( j x. T ) ) -> ( c e. A <-> ( a + ( j x. T ) ) e. A ) )
653	652	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 ) ) )
654		breq1	|- ( c = ( a + ( j x. T ) ) -> ( c < ( b + ( k x. T ) ) <-> ( a + ( j x. T ) ) < ( b + ( k x. T ) ) ) )
655	653 654	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 ) ) ) ) )
656		oveq2	|- ( c = ( a + ( j x. T ) ) -> ( ( b + ( k x. T ) ) - c ) = ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
657	656	breq2d	|- ( c = ( a + ( j x. T ) ) -> ( E <_ ( ( b + ( k x. T ) ) - c ) <-> E <_ ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) ) )
658	655 657	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 ) ) ) ) ) )
659		simp2r	|- ( ( ph /\ ( c e. A /\ ( b + ( k x. T ) ) e. A ) /\ c < ( b + ( k x. T ) ) ) -> ( b + ( k x. T ) ) e. A )
660		eleq1	|- ( d = ( b + ( k x. T ) ) -> ( d e. A <-> ( b + ( k x. T ) ) e. A ) )
661	660	anbi2d	|- ( d = ( b + ( k x. T ) ) -> ( ( c e. A /\ d e. A ) <-> ( c e. A /\ ( b + ( k x. T ) ) e. A ) ) )
662		breq2	|- ( d = ( b + ( k x. T ) ) -> ( c < d <-> c < ( b + ( k x. T ) ) ) )
663	661 662	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 ) ) ) ) )
664		oveq1	|- ( d = ( b + ( k x. T ) ) -> ( d - c ) = ( ( b + ( k x. T ) ) - c ) )
665	664	breq2d	|- ( d = ( b + ( k x. T ) ) -> ( E <_ ( d - c ) <-> E <_ ( ( b + ( k x. T ) ) - c ) ) )
666	663 665	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 ) ) ) )
667	666 514	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 ) ) )
668	659 667	mpcom	|- ( ( ph /\ ( c e. A /\ ( b + ( k x. T ) ) e. A ) /\ c < ( b + ( k x. T ) ) ) -> E <_ ( ( b + ( k x. T ) ) - c ) )
669	658 668	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 ) ) ) ) )
670	651 669	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 ) ) ) )
671	626 628 650 670	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 ) ) ) )
672	395	ad2antlr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k <_ j ) -> ( j - k ) e. RR )
673	293	ad2antrr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k <_ j ) -> T e. RR )
674		simpr	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k <_ j ) -> k <_ j )
675	283	ad2antrr	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k <_ j ) -> j e. RR )
676	286	ad2antlr	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k <_ j ) -> k e. RR )
677	675 676	subge0d	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k <_ j ) -> ( 0 <_ ( j - k ) <-> k <_ j ) )
678	674 677	mpbird	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k <_ j ) -> 0 <_ ( j - k ) )
679	678	adantll	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k <_ j ) -> 0 <_ ( j - k ) )
680	352	rpge0d	|- ( ps -> 0 <_ T )
681	680	ad2antrr	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k <_ j ) -> 0 <_ T )
682	672 673 679 681	mulge0d	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k <_ j ) -> 0 <_ ( ( j - k ) x. T ) )
683	682	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 ) )
684	620	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 )
685	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 )
686	684 685	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 ) ) ) )
687	683 686	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 ) ) )
688	687	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 ) ) )
689	616 621 623 671 688	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 ) ) )
690	615 689	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 ) ) )
691	372 378	eqtrd	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) = ( ( b - a ) + ( ( k - j ) x. T ) ) )
692	691	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 ) ) )
693	365 369	subcld	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( b - a ) e. CC )
694	373 374	subcld	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k - j ) e. CC )
695	694 375	mulcld	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) e. CC )
696	693 695 609	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 ) ) ) )
697	341 336 336 341	subadd4b	|- ( ( j e. ZZ /\ k e. ZZ ) -> ( ( k - j ) + ( j - k ) ) = ( ( k - k ) + ( j - j ) ) )
698	697	adantl	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) + ( j - k ) ) = ( ( k - k ) + ( j - j ) ) )
699	698	oveq1d	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( k - j ) + ( j - k ) ) x. T ) = ( ( ( k - k ) + ( j - j ) ) x. T ) )
700	694 608 375	adddird	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( k - j ) + ( j - k ) ) x. T ) = ( ( ( k - j ) x. T ) + ( ( j - k ) x. T ) ) )
701	340	subidd	|- ( k e. ZZ -> ( k - k ) = 0 )
702	701	adantl	|- ( ( j e. ZZ /\ k e. ZZ ) -> ( k - k ) = 0 )
703	561	adantr	|- ( ( j e. ZZ /\ k e. ZZ ) -> ( j - j ) = 0 )
704	702 703	oveq12d	|- ( ( j e. ZZ /\ k e. ZZ ) -> ( ( k - k ) + ( j - j ) ) = ( 0 + 0 ) )
705		00id	|- ( 0 + 0 ) = 0
706	704 705	eqtrdi	|- ( ( j e. ZZ /\ k e. ZZ ) -> ( ( k - k ) + ( j - j ) ) = 0 )
707	706	oveq1d	|- ( ( j e. ZZ /\ k e. ZZ ) -> ( ( ( k - k ) + ( j - j ) ) x. T ) = ( 0 x. T ) )
708	707	adantl	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( k - k ) + ( j - j ) ) x. T ) = ( 0 x. T ) )
709	699 700 708	3eqtr3d	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( k - j ) x. T ) + ( ( j - k ) x. T ) ) = ( 0 x. T ) )
710	709	oveq2d	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b - a ) + ( ( ( k - j ) x. T ) + ( ( j - k ) x. T ) ) ) = ( ( b - a ) + ( 0 x. T ) ) )
711	318	mul02d	|- ( ps -> ( 0 x. T ) = 0 )
712	711	oveq2d	|- ( ps -> ( ( b - a ) + ( 0 x. T ) ) = ( ( b - a ) + 0 ) )
713	364 368	subcld	|- ( ps -> ( b - a ) e. CC )
714	713	addridd	|- ( ps -> ( ( b - a ) + 0 ) = ( b - a ) )
715	712 714	eqtrd	|- ( ps -> ( ( b - a ) + ( 0 x. T ) ) = ( b - a ) )
716	715	adantr	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b - a ) + ( 0 x. T ) ) = ( b - a ) )
717	710 716	eqtrd	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b - a ) + ( ( ( k - j ) x. T ) + ( ( j - k ) x. T ) ) ) = ( b - a ) )
718	692 696 717	3eqtrd	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) = ( b - a ) )
719	718	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 ) )
720	719	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 ) )
721	690 720	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 ) )
722		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 ) ) )
723		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 ) ) )
724	600	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 )
725	724	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 )
726	618	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 )
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 ) ) ) -> ( a + ( j x. T ) ) e. RR )
728	725 727	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 ) ) ) )
729	723 728	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 ) ) )
730	729	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 ) ) )
731	534	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 ) )
732	731	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 ) )
733	599	3adant2	|- ( ( ps /\ k e. ZZ /\ ( b + ( k x. T ) ) e. A ) -> ( b + ( k x. T ) ) e. RR )
734	302	3ad2ant1	|- ( ( ps /\ k e. ZZ /\ ( b + ( k x. T ) ) e. A ) -> b e. RR )
735	733 734	resubcld	|- ( ( ps /\ k e. ZZ /\ ( b + ( k x. T ) ) e. A ) -> ( ( b + ( k x. T ) ) - b ) e. RR )
736	293	3ad2ant1	|- ( ( ps /\ k e. ZZ /\ ( b + ( k x. T ) ) e. A ) -> T e. RR )
737	530	3ad2ant1	|- ( ( ps /\ k e. ZZ /\ ( b + ( k x. T ) ) e. A ) -> T =/= 0 )
738	735 736 737	redivcld	|- ( ( ps /\ k e. ZZ /\ ( b + ( k x. T ) ) e. A ) -> ( ( ( b + ( k x. T ) ) - b ) / T ) e. RR )
739	738	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 )
740	739	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 )
741	740	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 )
742	617	3adant2	|- ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> ( a + ( j x. T ) ) e. RR )
743	302	3ad2ant1	|- ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> b e. RR )
744	742 743	resubcld	|- ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> ( ( a + ( j x. T ) ) - b ) e. RR )
745	293	3ad2ant1	|- ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> T e. RR )
746	530	3ad2ant1	|- ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> T =/= 0 )
747	744 745 746	redivcld	|- ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) e. RR )
748	747	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 )
749	748	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 )
750	749	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 )
751	284	3ad2ant2	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> j 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 ) ) ) -> j e. RR )
753	724	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 )
754	302	3ad2ant1	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> b e. RR )
755	754	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 )
756	753 755	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 )
757	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 ) ) ) -> ( a + ( j x. T ) ) e. RR )
758	757 755	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 )
759	352	3ad2ant1	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> T e. RR+ )
760	759	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+ )
761	600	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 )
762	618	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 )
763	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 )
764		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 ) ) )
765	761 762 763 764	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 ) )
766	765	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 ) )
767	756 758 760 766	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 ) )
768	553 569	eqbrtrd	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) < j )
769	768	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 )
770	769	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 )
771	741 750 752 767 770	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 )
772	732 771	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 )
773	772	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 )
774	730 773	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 )
775	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 )
776	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 )
777	622	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 )
778	521	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 )
779		peano2rem	|- ( j e. RR -> ( j - 1 ) e. RR )
780	751 779	syl	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( j - 1 ) e. RR )
781	287	3ad2ant2	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> k e. RR )
782	780 781	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 )
783	782 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 )
784	783	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 )
785	751	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 )
786	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 )
787	785 786	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 )
788	286	ad2antlr	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> k e. RR )
789	788	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 )
790	787 789	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 )
791	680	adantr	|- ( ( ps /\ k < ( j - 1 ) ) -> 0 <_ T )
792	791	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 )
793	283	ad2antrr	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> j e. RR )
794	330	a1i	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> 1 e. RR )
795	793 794	resubcld	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> ( j - 1 ) e. RR )
796		simpr	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> k < ( j - 1 ) )
797		simplr	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> k e. ZZ )
798		simpll	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> j e. ZZ )
799		1zzd	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> 1 e. ZZ )
800	798 799	zsubcld	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> ( j - 1 ) e. ZZ )
801		zltlem1	|- ( ( k e. ZZ /\ ( j - 1 ) e. ZZ ) -> ( k < ( j - 1 ) <-> k <_ ( ( j - 1 ) - 1 ) ) )
802	797 800 801	syl2anc	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> ( k < ( j - 1 ) <-> k <_ ( ( j - 1 ) - 1 ) ) )
803	796 802	mpbid	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> k <_ ( ( j - 1 ) - 1 ) )
804	788 795 794 803	lesubd	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < ( j - 1 ) ) -> 1 <_ ( ( j - 1 ) - k ) )
805	804	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 ) )
806	776 790 792 805	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 ) )
807	336 337 341	sub32d	|- ( ( j e. ZZ /\ k e. ZZ ) -> ( ( j - 1 ) - k ) = ( ( j - k ) - 1 ) )
808	807	oveq1d	|- ( ( j e. ZZ /\ k e. ZZ ) -> ( ( ( j - 1 ) - k ) x. T ) = ( ( ( j - k ) - 1 ) x. T ) )
809	808	adantl	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( j - 1 ) - k ) x. T ) = ( ( ( j - k ) - 1 ) x. T ) )
810		1cnd	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> 1 e. CC )
811	608 810 375	subdird	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( j - k ) - 1 ) x. T ) = ( ( ( j - k ) x. T ) - ( 1 x. T ) ) )
812	319	oveq2d	|- ( ps -> ( ( ( j - k ) x. T ) - ( 1 x. T ) ) = ( ( ( j - k ) x. T ) - T ) )
813	812	adantr	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( j - k ) x. T ) - ( 1 x. T ) ) = ( ( ( j - k ) x. T ) - T ) )
814	809 811 813	3eqtrd	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( ( j - 1 ) - k ) x. T ) = ( ( ( j - k ) x. T ) - T ) )
815	814	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 ) )
816	726 724	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 )
817	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 ) )
818	817 4	breqtrrdi	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( a + ( j x. T ) ) - ( b + ( k x. T ) ) ) <_ T )
819	818	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 )
820	816 393 398 819	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 ) ) ) ) )
821	815 820	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 ) ) ) ) )
822	609	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 )
823	726	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 )
824	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. CC )
825	822 823 824	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 ) ) ) ) )
826	620	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 )
827	822 826	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 ) ) )
828	825 827	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 ) ) )
829	821 828	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 ) ) )
830	829	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 ) ) )
831	776 784 777 806 830	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 ) ) )
832	775 776 777 778 831	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 ) ) )
833	719	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 ) )
834	832 833	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 ) )
835	834	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 ) )
836	835	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 ) )
837		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 ) ) )
838		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 ) )
839		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 )
840		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 ) )
841	580 581 579 583	lesubd	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j ) -> k <_ ( j - 1 ) )
842	841	3adant3	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j /\ -. k < ( j - 1 ) ) -> k <_ ( j - 1 ) )
843		simpr	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ -. k < ( j - 1 ) ) -> -. k < ( j - 1 ) )
844	284 779	syl	|- ( ( j e. ZZ /\ k e. ZZ ) -> ( j - 1 ) e. RR )
845	844	adantr	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ -. k < ( j - 1 ) ) -> ( j - 1 ) e. RR )
846	286	ad2antlr	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ -. k < ( j - 1 ) ) -> k e. RR )
847	845 846	lenltd	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ -. k < ( j - 1 ) ) -> ( ( j - 1 ) <_ k <-> -. k < ( j - 1 ) ) )
848	843 847	mpbird	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ -. k < ( j - 1 ) ) -> ( j - 1 ) <_ k )
849	848	3adant2	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j /\ -. k < ( j - 1 ) ) -> ( j - 1 ) <_ k )
850	579	3adant3	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j /\ -. k < ( j - 1 ) ) -> k e. RR )
851	844	3ad2ant1	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j /\ -. k < ( j - 1 ) ) -> ( j - 1 ) e. RR )
852	850 851	letri3d	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j /\ -. k < ( j - 1 ) ) -> ( k = ( j - 1 ) <-> ( k <_ ( j - 1 ) /\ ( j - 1 ) <_ k ) ) )
853	842 849 852	mpbir2and	|- ( ( ( j e. ZZ /\ k e. ZZ ) /\ k < j /\ -. k < ( j - 1 ) ) -> k = ( j - 1 ) )
854	838 839 840 853	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 ) )
855	854	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 ) )
856		simpl1	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) /\ k = ( j - 1 ) ) -> ps )
857		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 )
858		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 )
859		oveq1	|- ( k = ( j - 1 ) -> ( k x. T ) = ( ( j - 1 ) x. T ) )
860	859	oveq2d	|- ( k = ( j - 1 ) -> ( b + ( k x. T ) ) = ( b + ( ( j - 1 ) x. T ) ) )
861	860	eqcomd	|- ( k = ( j - 1 ) -> ( b + ( ( j - 1 ) x. T ) ) = ( b + ( k x. T ) ) )
862	861	adantl	|- ( ( ( b + ( k x. T ) ) e. A /\ k = ( j - 1 ) ) -> ( b + ( ( j - 1 ) x. T ) ) = ( b + ( k x. T ) ) )
863		simpl	|- ( ( ( b + ( k x. T ) ) e. A /\ k = ( j - 1 ) ) -> ( b + ( k x. T ) ) e. A )
864	862 863	eqeltrd	|- ( ( ( b + ( k x. T ) ) e. A /\ k = ( j - 1 ) ) -> ( b + ( ( j - 1 ) x. T ) ) e. A )
865	864	adantll	|- ( ( ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) /\ k = ( j - 1 ) ) -> ( b + ( ( j - 1 ) x. T ) ) e. A )
866	865	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 )
867	858 866	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 ) )
868		id	|- ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) )
869	868	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 ) )
870	742	adantr	|- ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( a + ( j x. T ) ) e. RR )
871	271	3ad2ant1	|- ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> C e. RR )
872	871	adantr	|- ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> C e. RR )
873	269	adantr	|- ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> B e. RR )
874	271	adantr	|- ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> C e. RR )
875		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 ) ) )
876	873 874 875	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 ) ) )
877	276 876	mpbid	|- ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> ( ( a + ( j x. T ) ) e. RR /\ B <_ ( a + ( j x. T ) ) /\ ( a + ( j x. T ) ) <_ C ) )
878	877	simp3d	|- ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> ( a + ( j x. T ) ) <_ C )
879	878	3adant2	|- ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> ( a + ( j x. T ) ) <_ C )
880	879	adantr	|- ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( a + ( j x. T ) ) <_ C )
881		nne	|- ( -. C =/= ( a + ( j x. T ) ) <-> C = ( a + ( j x. T ) ) )
882	539 370	pncand	|- ( ( ps /\ j e. ZZ ) -> ( ( a + ( j x. T ) ) - ( j x. T ) ) = a )
883	882	eqcomd	|- ( ( ps /\ j e. ZZ ) -> a = ( ( a + ( j x. T ) ) - ( j x. T ) ) )
884	883	adantr	|- ( ( ( ps /\ j e. ZZ ) /\ C = ( a + ( j x. T ) ) ) -> a = ( ( a + ( j x. T ) ) - ( j x. T ) ) )
885		oveq1	|- ( C = ( a + ( j x. T ) ) -> ( C - ( j x. T ) ) = ( ( a + ( j x. T ) ) - ( j x. T ) ) )
886	885	eqcomd	|- ( C = ( a + ( j x. T ) ) -> ( ( a + ( j x. T ) ) - ( j x. T ) ) = ( C - ( j x. T ) ) )
887	886	adantl	|- ( ( ( ps /\ j e. ZZ ) /\ C = ( a + ( j x. T ) ) ) -> ( ( a + ( j x. T ) ) - ( j x. T ) ) = ( C - ( j x. T ) ) )
888	4	oveq2i	|- ( B + T ) = ( B + ( C - B ) )
889	268 161	syl	|- ( ps -> B e. CC )
890	268 162	syl	|- ( ps -> C e. CC )
891	889 890	pncan3d	|- ( ps -> ( B + ( C - B ) ) = C )
892	888 891	eqtr2id	|- ( ps -> C = ( B + T ) )
893	892	oveq1d	|- ( ps -> ( C - ( j x. T ) ) = ( ( B + T ) - ( j x. T ) ) )
894	893	adantr	|- ( ( ps /\ j e. ZZ ) -> ( C - ( j x. T ) ) = ( ( B + T ) - ( j x. T ) ) )
895	889	adantr	|- ( ( ps /\ j e. ZZ ) -> B e. CC )
896	895 370 546	subsub3d	|- ( ( ps /\ j e. ZZ ) -> ( B - ( ( j x. T ) - T ) ) = ( ( B + T ) - ( j x. T ) ) )
897	549 546	mulsubfacd	|- ( ( ps /\ j e. ZZ ) -> ( ( j x. T ) - T ) = ( ( j - 1 ) x. T ) )
898	897	oveq2d	|- ( ( ps /\ j e. ZZ ) -> ( B - ( ( j x. T ) - T ) ) = ( B - ( ( j - 1 ) x. T ) ) )
899	894 896 898	3eqtr2d	|- ( ( ps /\ j e. ZZ ) -> ( C - ( j x. T ) ) = ( B - ( ( j - 1 ) x. T ) ) )
900	899	adantr	|- ( ( ( ps /\ j e. ZZ ) /\ C = ( a + ( j x. T ) ) ) -> ( C - ( j x. T ) ) = ( B - ( ( j - 1 ) x. T ) ) )
901	884 887 900	3eqtrd	|- ( ( ( ps /\ j e. ZZ ) /\ C = ( a + ( j x. T ) ) ) -> a = ( B - ( ( j - 1 ) x. T ) ) )
902	901	3adantl3	|- ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ C = ( a + ( j x. T ) ) ) -> a = ( B - ( ( j - 1 ) x. T ) ) )
903	902	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 ) ) )
904		oveq1	|- ( ( b + ( ( j - 1 ) x. T ) ) = B -> ( ( b + ( ( j - 1 ) x. T ) ) - ( ( j - 1 ) x. T ) ) = ( B - ( ( j - 1 ) x. T ) ) )
905	904	eqcomd	|- ( ( b + ( ( j - 1 ) x. T ) ) = B -> ( B - ( ( j - 1 ) x. T ) ) = ( ( b + ( ( j - 1 ) x. T ) ) - ( ( j - 1 ) x. T ) ) )
906	905	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 ) ) )
907	364	ad2antrr	|- ( ( ( ps /\ j e. ZZ ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> b e. CC )
908		1cnd	|- ( ( ps /\ j e. ZZ ) -> 1 e. CC )
909	549 908	subcld	|- ( ( ps /\ j e. ZZ ) -> ( j - 1 ) e. CC )
910	909 546	mulcld	|- ( ( ps /\ j e. ZZ ) -> ( ( j - 1 ) x. T ) e. CC )
911	910	adantr	|- ( ( ( ps /\ j e. ZZ ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( ( j - 1 ) x. T ) e. CC )
912	907 911	pncand	|- ( ( ( ps /\ j e. ZZ ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( ( b + ( ( j - 1 ) x. T ) ) - ( ( j - 1 ) x. T ) ) = b )
913	912	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 )
914	913	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 )
915	903 906 914	3eqtrd	|- ( ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) /\ C = ( a + ( j x. T ) ) ) -> a = b )
916	881 915	sylan2b	|- ( ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) /\ -. C =/= ( a + ( j x. T ) ) ) -> a = b )
917	309 358	ltned	|- ( ps -> a =/= b )
918	917	neneqd	|- ( ps -> -. a = b )
919	918	3ad2ant1	|- ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) -> -. a = b )
920	919	ad2antrr	|- ( ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) /\ -. C =/= ( a + ( j x. T ) ) ) -> -. a = b )
921	916 920	condan	|- ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> C =/= ( a + ( j x. T ) ) )
922	870 872 880 921	leneltd	|- ( ( ( ps /\ j e. ZZ /\ ( a + ( j x. T ) ) e. A ) /\ ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( a + ( j x. T ) ) < C )
923	869 922	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 )
924	268	ad2antrr	|- ( ( ( ps /\ ( a + ( j x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < C ) -> ph )
925		simplr	|- ( ( ( ps /\ ( a + ( j x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < C ) -> ( a + ( j x. T ) ) e. A )
926	924 8	syl	|- ( ( ( ps /\ ( a + ( j x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < C ) -> C e. A )
927		simpr	|- ( ( ( ps /\ ( a + ( j x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < C ) -> ( a + ( j x. T ) ) < C )
928		simp2l	|- ( ( ph /\ ( ( a + ( j x. T ) ) e. A /\ C e. A ) /\ ( a + ( j x. T ) ) < C ) -> ( a + ( j x. T ) ) e. A )
929	652	anbi1d	|- ( c = ( a + ( j x. T ) ) -> ( ( c e. A /\ C e. A ) <-> ( ( a + ( j x. T ) ) e. A /\ C e. A ) ) )
930		breq1	|- ( c = ( a + ( j x. T ) ) -> ( c < C <-> ( a + ( j x. T ) ) < C ) )
931	929 930	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 ) ) )
932		oveq2	|- ( c = ( a + ( j x. T ) ) -> ( C - c ) = ( C - ( a + ( j x. T ) ) ) )
933	932	breq2d	|- ( c = ( a + ( j x. T ) ) -> ( E <_ ( C - c ) <-> E <_ ( C - ( a + ( j x. T ) ) ) ) )
934	931 933	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 ) ) ) ) ) )
935		simp2r	|- ( ( ph /\ ( c e. A /\ C e. A ) /\ c < C ) -> C e. A )
936	403	anbi2d	|- ( d = C -> ( ( c e. A /\ d e. A ) <-> ( c e. A /\ C e. A ) ) )
937		breq2	|- ( d = C -> ( c < d <-> c < C ) )
938	936 937	3anbi23d	|- ( d = C -> ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) <-> ( ph /\ ( c e. A /\ C e. A ) /\ c < C ) ) )
939		oveq1	|- ( d = C -> ( d - c ) = ( C - c ) )
940	939	breq2d	|- ( d = C -> ( E <_ ( d - c ) <-> E <_ ( C - c ) ) )
941	938 940	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 ) ) ) )
942	941 514	vtoclg	|- ( C e. A -> ( ( ph /\ ( c e. A /\ C e. A ) /\ c < C ) -> E <_ ( C - c ) ) )
943	935 942	mpcom	|- ( ( ph /\ ( c e. A /\ C e. A ) /\ c < C ) -> E <_ ( C - c ) )
944	934 943	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 ) ) ) ) )
945	928 944	mpcom	|- ( ( ph /\ ( ( a + ( j x. T ) ) e. A /\ C e. A ) /\ ( a + ( j x. T ) ) < C ) -> E <_ ( C - ( a + ( j x. T ) ) ) )
946	924 925 926 927 945	syl121anc	|- ( ( ( ps /\ ( a + ( j x. T ) ) e. A ) /\ ( a + ( j x. T ) ) < C ) -> E <_ ( C - ( a + ( j x. T ) ) ) )
947	946	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 ) ) ) )
948	947	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 ) ) ) )
949	948	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 ) ) ) )
950	890	adantr	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> C e. CC )
951	598	sselda	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( b + ( ( j - 1 ) x. T ) ) e. RR )
952	951	recnd	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( b + ( ( j - 1 ) x. T ) ) e. CC )
953	950 952	npcand	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( ( C - ( b + ( ( j - 1 ) x. T ) ) ) + ( b + ( ( j - 1 ) x. T ) ) ) = C )
954	953	eqcomd	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> C = ( ( C - ( b + ( ( j - 1 ) x. T ) ) ) + ( b + ( ( j - 1 ) x. T ) ) ) )
955	954	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 ) ) ) )
956	955	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 ) ) ) )
957	956	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 ) ) ) )
958	957	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 ) ) ) )
959		oveq2	|- ( ( b + ( ( j - 1 ) x. T ) ) = B -> ( C - ( b + ( ( j - 1 ) x. T ) ) ) = ( C - B ) )
960	959	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 ) ) ) )
961	960	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 ) ) ) )
962	961	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 ) ) ) )
963	4	eqcomi	|- ( C - B ) = T
964	963	oveq1i	|- ( ( C - B ) + ( b + ( ( j - 1 ) x. T ) ) ) = ( T + ( b + ( ( j - 1 ) x. T ) ) )
965	964	a1i	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( ( C - B ) + ( b + ( ( j - 1 ) x. T ) ) ) = ( T + ( b + ( ( j - 1 ) x. T ) ) ) )
966	318	adantr	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> T e. CC )
967	966 952	addcomd	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( T + ( b + ( ( j - 1 ) x. T ) ) ) = ( ( b + ( ( j - 1 ) x. T ) ) + T ) )
968	965 967	eqtrd	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( ( C - B ) + ( b + ( ( j - 1 ) x. T ) ) ) = ( ( b + ( ( j - 1 ) x. T ) ) + T ) )
969	968	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 ) ) ) )
970	969	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 ) ) ) )
971	970	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 ) ) ) )
972	971	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 ) ) ) )
973	952	adantrl	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( b + ( ( j - 1 ) x. T ) ) e. CC )
974	973	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 )
975	974	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 )
976	318	3ad2ant1	|- ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> 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 ) -> T e. CC )
978	617	adantrr	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) e. RR )
979	978	recnd	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) e. CC )
980	979	3adant2	|- ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) e. CC )
981	980	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 )
982	975 977 981	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 ) )
983	972 982	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 ) )
984	958 962 983	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 ) )
985	984	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 ) )
986	949 985	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 ) )
987	923 986	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 ) )
988		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 )
989		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 )
990		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 )
991	269	3ad2ant1	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> B e. RR )
992	951	3adant3	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( b + ( ( j - 1 ) x. T ) ) e. RR )
993	273	sselda	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> ( b + ( ( j - 1 ) x. T ) ) e. ( B [,] C ) )
994	269	adantr	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> B e. RR )
995	271	adantr	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> C e. RR )
996		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 ) ) )
997	994 995 996	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 ) ) )
998	993 997	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 ) )
999	998	simp2d	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) -> B <_ ( b + ( ( j - 1 ) x. T ) ) )
1000	999	3adant3	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> B <_ ( b + ( ( j - 1 ) x. T ) ) )
1001		neqne	|- ( -. ( b + ( ( j - 1 ) x. T ) ) = B -> ( b + ( ( j - 1 ) x. T ) ) =/= B )
1002	1001	3ad2ant3	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> ( b + ( ( j - 1 ) x. T ) ) =/= B )
1003	991 992 1000 1002	leneltd	|- ( ( ps /\ ( b + ( ( j - 1 ) x. T ) ) e. A /\ -. ( b + ( ( j - 1 ) x. T ) ) = B ) -> B < ( b + ( ( j - 1 ) x. T ) ) )
1004	988 989 990 1003	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 ) ) )
1005	390	3ad2ant1	|- ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> E e. RR )
1006	1005	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 )
1007	951	adantrl	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( b + ( ( j - 1 ) x. T ) ) e. RR )
1008	1007	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 )
1009	269	3ad2ant1	|- ( ( ps /\ j e. ZZ /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> B e. RR )
1010	1008 1009	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 )
1011	1010	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 )
1012	1007 978	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 )
1013	293	adantr	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> T e. RR )
1014	1012 1013	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 )
1015	1014	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 )
1016	1015	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 )
1017	268	adantr	|- ( ( ps /\ B < ( b + ( ( j - 1 ) x. T ) ) ) -> ph )
1018	1017	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 )
1019	1018 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 )
1020		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 )
1021		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 ) ) )
1022		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 )
1023		eleq1	|- ( d = ( b + ( ( j - 1 ) x. T ) ) -> ( d e. A <-> ( b + ( ( j - 1 ) x. T ) ) e. A ) )
1024	1023	anbi2d	|- ( d = ( b + ( ( j - 1 ) x. T ) ) -> ( ( B e. A /\ d e. A ) <-> ( B e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) )
1025		breq2	|- ( d = ( b + ( ( j - 1 ) x. T ) ) -> ( B < d <-> B < ( b + ( ( j - 1 ) x. T ) ) ) )
1026	1024 1025	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 ) ) ) ) )
1027		oveq1	|- ( d = ( b + ( ( j - 1 ) x. T ) ) -> ( d - B ) = ( ( b + ( ( j - 1 ) x. T ) ) - B ) )
1028	1027	breq2d	|- ( d = ( b + ( ( j - 1 ) x. T ) ) -> ( E <_ ( d - B ) <-> E <_ ( ( b + ( ( j - 1 ) x. T ) ) - B ) ) )
1029	1026 1028	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 ) ) ) )
1030	1029 516	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 ) ) )
1031	1022 1030	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 ) )
1032	1018 1019 1020 1021 1031	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 ) )
1033	269	adantr	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> B e. RR )
1034	978 1033	resubcld	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( a + ( j x. T ) ) - B ) e. RR )
1035	963 1013	eqeltrid	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( C - B ) e. RR )
1036	271	adantr	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> C e. RR )
1037	878	adantrr	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) <_ C )
1038	978 1036 1033 1037	lesub1dd	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> ( ( a + ( j x. T ) ) - B ) <_ ( C - B ) )
1039	1034 1035 1012 1038	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 ) ) )
1040	973 979	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 ) ) )
1041	1040	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 ) ) ) )
1042	1041	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 ) )
1043	1012	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 )
1044	889	adantr	|- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( ( j - 1 ) x. T ) ) e. A ) ) -> B e. CC )
1045	1043 979 1044	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 ) ) )
1046	1042 1045	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 ) ) )
1047	4	oveq2i	|- ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) = ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + ( C - B ) )
1048	1047	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 ) ) )
1049	1039 1046 1048	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 ) )
1050	1049	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 ) )
1051	1050	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 ) )
1052	1006 1011 1016 1032 1051	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 ) )
1053	1004 1052	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 ) )
1054	987 1053	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 ) )
1055	856 857 867 1054	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 ) )
1056	718	eqcomd	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( b - a ) = ( ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) + ( ( j - k ) x. T ) ) )
1057	1056	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 ) ) )
1058	860	oveq1d	|- ( k = ( j - 1 ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) = ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) )
1059	1058	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 ) ) ) )
1060		oveq2	|- ( k = ( j - 1 ) -> ( j - k ) = ( j - ( j - 1 ) ) )
1061	1060	oveq1d	|- ( k = ( j - 1 ) -> ( ( j - k ) x. T ) = ( ( j - ( j - 1 ) ) x. T ) )
1062	1061	adantl	|- ( ( ( ps /\ j e. ZZ ) /\ k = ( j - 1 ) ) -> ( ( j - k ) x. T ) = ( ( j - ( j - 1 ) ) x. T ) )
1063		1cnd	|- ( j e. ZZ -> 1 e. CC )
1064	335 1063	nncand	|- ( j e. ZZ -> ( j - ( j - 1 ) ) = 1 )
1065	1064	oveq1d	|- ( j e. ZZ -> ( ( j - ( j - 1 ) ) x. T ) = ( 1 x. T ) )
1066	1065	ad2antlr	|- ( ( ( ps /\ j e. ZZ ) /\ k = ( j - 1 ) ) -> ( ( j - ( j - 1 ) ) x. T ) = ( 1 x. T ) )
1067	319	ad2antrr	|- ( ( ( ps /\ j e. ZZ ) /\ k = ( j - 1 ) ) -> ( 1 x. T ) = T )
1068	1062 1066 1067	3eqtrd	|- ( ( ( ps /\ j e. ZZ ) /\ k = ( j - 1 ) ) -> ( ( j - k ) x. T ) = T )
1069	1059 1068	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 ) )
1070	1069	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 ) )
1071	1057 1070	eqtr2d	|- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ k = ( j - 1 ) ) -> ( ( ( b + ( ( j - 1 ) x. T ) ) - ( a + ( j x. T ) ) ) + T ) = ( b - a ) )
1072	1071	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 ) )
1073	1055 1072	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 ) )
1074	837 855 1073	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 ) )
1075	836 1074	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 ) )
1076	722 774 730 1075	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 ) )
1077	721 1076	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 ) )
1078	387 1077	mpdan	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ ( b - a ) )
1079	309 302 358	ltled	|- ( ps -> a <_ b )
1080	309 302 1079	abssuble0d	|- ( ps -> ( abs ` ( a - b ) ) = ( b - a ) )
1081	1080	eqcomd	|- ( ps -> ( b - a ) = ( abs ` ( a - b ) ) )
1082	1081	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 ) ) )
1083	1078 1082	breqtrd	|- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ ( abs ` ( a - b ) ) )
1084	1083	3exp	|- ( ps -> ( ( j e. ZZ /\ k e. ZZ ) -> ( ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) -> E <_ ( abs ` ( a - b ) ) ) ) )
1085	1084	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 ) ) ) )
1086	265 1085	mpd	|- ( ps -> E <_ ( abs ` ( a - b ) ) )
1087	18 1086	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 ) ) )
1088	264 1087	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 ) ) )
1089	251 1088	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 ) ) )
1090	231 237 238 1089	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 ) ) )
1091		simpr	|- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> -. y < z )
1092		simpl3	|- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> y =/= z )
1093		simpl1	|- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> y e. RR )
1094		simpl2	|- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> z e. RR )
1095	1093 1094	lttri2d	|- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> ( y =/= z <-> ( y < z \/ z < y ) ) )
1096	1092 1095	mpbid	|- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> ( y < z \/ z < y ) )
1097	1096	ord	|- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> ( -. y < z -> z < y ) )
1098	1091 1097	mpd	|- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ -. y < z ) -> z < y )
1099	1098	adantll	|- ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ -. y < z ) -> z < y )
1100	1099	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 )
1101		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 )
1102		simplr	|- ( ( ( y e. RR /\ z e. RR ) /\ z < y ) -> z e. RR )
1103		simpll	|- ( ( ( y e. RR /\ z e. RR ) /\ z < y ) -> y e. RR )
1104		simpr	|- ( ( ( y e. RR /\ z e. RR ) /\ z < y ) -> z < y )
1105	1102 1103 1104	3jca	|- ( ( ( y e. RR /\ z e. RR ) /\ z < y ) -> ( z e. RR /\ y e. RR /\ z < y ) )
1106	1105	adantll	|- ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ z < y ) -> ( z e. RR /\ y e. RR /\ z < y ) )
1107	1106	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 ) )
1108		oveq1	|- ( j = i -> ( j x. T ) = ( i x. T ) )
1109	1108	oveq2d	|- ( j = i -> ( y + ( j x. T ) ) = ( y + ( i x. T ) ) )
1110	1109	eleq1d	|- ( j = i -> ( ( y + ( j x. T ) ) e. A <-> ( y + ( i x. T ) ) e. A ) )
1111	1110	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 ) ) )
1112		oveq1	|- ( k = l -> ( k x. T ) = ( l x. T ) )
1113	1112	oveq2d	|- ( k = l -> ( z + ( k x. T ) ) = ( z + ( l x. T ) ) )
1114	1113	eleq1d	|- ( k = l -> ( ( z + ( k x. T ) ) e. A <-> ( z + ( l x. T ) ) e. A ) )
1115	1114	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 ) ) )
1116	1111 1115	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 ) )
1117		oveq1	|- ( i = k -> ( i x. T ) = ( k x. T ) )
1118	1117	oveq2d	|- ( i = k -> ( y + ( i x. T ) ) = ( y + ( k x. T ) ) )
1119	1118	eleq1d	|- ( i = k -> ( ( y + ( i x. T ) ) e. A <-> ( y + ( k x. T ) ) e. A ) )
1120	1119	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 ) ) )
1121		oveq1	|- ( l = j -> ( l x. T ) = ( j x. T ) )
1122	1121	oveq2d	|- ( l = j -> ( z + ( l x. T ) ) = ( z + ( j x. T ) ) )
1123	1122	eleq1d	|- ( l = j -> ( ( z + ( l x. T ) ) e. A <-> ( z + ( j x. T ) ) e. A ) )
1124	1123	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 ) ) )
1125	1120 1124	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 ) )
1126		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 ) )
1127		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 ) )
1128	1127	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 ) )
1129	1125 1126 1128	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 ) )
1130	1116 1129	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 ) )
1131	1130	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 ) )
1132		eleq1	|- ( b = y -> ( b e. RR <-> y e. RR ) )
1133		breq2	|- ( b = y -> ( z < b <-> z < y ) )
1134	1132 1133	3anbi23d	|- ( b = y -> ( ( z e. RR /\ b e. RR /\ z < b ) <-> ( z e. RR /\ y e. RR /\ z < y ) ) )
1135	1134	anbi2d	|- ( b = y -> ( ( ph /\ ( z e. RR /\ b e. RR /\ z < b ) ) <-> ( ph /\ ( z e. RR /\ y e. RR /\ z < y ) ) ) )
1136		oveq1	|- ( b = y -> ( b + ( k x. T ) ) = ( y + ( k x. T ) ) )
1137	1136	eleq1d	|- ( b = y -> ( ( b + ( k x. T ) ) e. A <-> ( y + ( k x. T ) ) e. A ) )
1138	1137	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 ) ) )
1139	1138	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 ) ) )
1140	1135 1139	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 ) ) ) )
1141		oveq2	|- ( b = y -> ( z - b ) = ( z - y ) )
1142	1141	fveq2d	|- ( b = y -> ( abs ` ( z - b ) ) = ( abs ` ( z - y ) ) )
1143	1142	breq2d	|- ( b = y -> ( E <_ ( abs ` ( z - b ) ) <-> E <_ ( abs ` ( z - y ) ) ) )
1144	1140 1143	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 ) ) ) ) )
1145		eleq1	|- ( a = z -> ( a e. RR <-> z e. RR ) )
1146		breq1	|- ( a = z -> ( a < b <-> z < b ) )
1147	1145 1146	3anbi13d	|- ( a = z -> ( ( a e. RR /\ b e. RR /\ a < b ) <-> ( z e. RR /\ b e. RR /\ z < b ) ) )
1148	1147	anbi2d	|- ( a = z -> ( ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) <-> ( ph /\ ( z e. RR /\ b e. RR /\ z < b ) ) ) )
1149		oveq1	|- ( a = z -> ( a + ( j x. T ) ) = ( z + ( j x. T ) ) )
1150	1149	eleq1d	|- ( a = z -> ( ( a + ( j x. T ) ) e. A <-> ( z + ( j x. T ) ) e. A ) )
1151	1150	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 ) ) )
1152	1151	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 ) ) )
1153	1148 1152	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 ) ) ) )
1154		oveq1	|- ( a = z -> ( a - b ) = ( z - b ) )
1155	1154	fveq2d	|- ( a = z -> ( abs ` ( a - b ) ) = ( abs ` ( z - b ) ) )
1156	1155	breq2d	|- ( a = z -> ( E <_ ( abs ` ( a - b ) ) <-> E <_ ( abs ` ( z - b ) ) ) )
1157	1153 1156	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 ) ) ) ) )
1158	1157 1087	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 ) ) )
1159	1144 1158	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 ) ) )
1160	1101 1107 1131 1159	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 ) ) )
1161		recn	|- ( z e. RR -> z e. CC )
1162	1161	adantl	|- ( ( y e. RR /\ z e. RR ) -> z e. CC )
1163		recn	|- ( y e. RR -> y e. CC )
1164	1163	adantr	|- ( ( y e. RR /\ z e. RR ) -> y e. CC )
1165	1162 1164	abssubd	|- ( ( y e. RR /\ z e. RR ) -> ( abs ` ( z - y ) ) = ( abs ` ( y - z ) ) )
1166	1165	adantl	|- ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> ( abs ` ( z - y ) ) = ( abs ` ( y - z ) ) )
1167	1166	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 ) ) )
1168	1160 1167	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 ) ) )
1169	1168	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 ) ) ) )
1170	1169	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 ) ) ) )
1171	1170	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 ) ) ) )
1172	1100 1171	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 ) ) )
1173	1090 1172	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 ) ) )
1174	198 206 230 1173	syl21anc	|- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> E <_ ( abs ` ( y - z ) ) )
1175	389	ad2antrr	|- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> E e. RR )
1176	200 203	resubcld	|- ( ( ph /\ ( y e. H /\ z e. H ) ) -> ( y - z ) e. RR )
1177	1176	recnd	|- ( ( ph /\ ( y e. H /\ z e. H ) ) -> ( y - z ) e. CC )
1178	1177	abscld	|- ( ( ph /\ ( y e. H /\ z e. H ) ) -> ( abs ` ( y - z ) ) e. RR )
1179	1178	adantr	|- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> ( abs ` ( y - z ) ) e. RR )
1180	1175 1179	lenltd	|- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> ( E <_ ( abs ` ( y - z ) ) <-> -. ( abs ` ( y - z ) ) < E ) )
1181	1174 1180	mpbid	|- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> -. ( abs ` ( y - z ) ) < E )
1182		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 ) )
1183	1181 1182	mpbir	|- ( ( ph /\ ( y e. H /\ z e. H ) ) -> -. ( y =/= z /\ ( abs ` ( y - z ) ) < E ) )
1184	1183	ralrimivva	|- ( ph -> A. y e. H A. z e. H -. ( y =/= z /\ ( abs ` ( y - z ) ) < E ) )
1185		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 ) )
1186	1184 1185	sylib	|- ( ph -> -. E. y e. H E. z e. H ( y =/= z /\ ( abs ` ( y - z ) ) < E ) )
1187	1186	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 ) )
1188	197 1187	pm2.65da	|- ( ( ph /\ x e. U. K ) -> -. x e. ( ( limPt ` J ) ` H ) )
1189	1188	intnanrd	|- ( ( ph /\ x e. U. K ) -> -. ( x e. ( ( limPt ` J ) ` H ) /\ x e. ( X [,] Y ) ) )
1190		elin	|- ( x e. ( ( ( limPt ` J ) ` H ) i^i ( X [,] Y ) ) <-> ( x e. ( ( limPt ` J ) ` H ) /\ x e. ( X [,] Y ) ) )
1191	1189 1190	sylnibr	|- ( ( ph /\ x e. U. K ) -> -. x e. ( ( ( limPt ` J ) ` H ) i^i ( X [,] Y ) ) )
1192	26	a1i	|- ( ( ph /\ x e. U. K ) -> J e. Top )
1193	27	adantr	|- ( ( ph /\ x e. U. K ) -> ( X [,] Y ) C_ RR )
1194	24	adantr	|- ( ( ph /\ x e. U. K ) -> H C_ ( X [,] Y ) )
1195	30 16	restlp	|- ( ( J e. Top /\ ( X [,] Y ) C_ RR /\ H C_ ( X [,] Y ) ) -> ( ( limPt ` K ) ` H ) = ( ( ( limPt ` J ) ` H ) i^i ( X [,] Y ) ) )
1196	1192 1193 1194 1195	syl3anc	|- ( ( ph /\ x e. U. K ) -> ( ( limPt ` K ) ` H ) = ( ( ( limPt ` J ) ` H ) i^i ( X [,] Y ) ) )
1197	1191 1196	neleqtrrd	|- ( ( ph /\ x e. U. K ) -> -. x e. ( ( limPt ` K ) ` H ) )
1198	1197	nrexdv	|- ( ph -> -. E. x e. U. K x e. ( ( limPt ` K ) ` H ) )
1199	1198	adantr	|- ( ( ph /\ -. H e. Fin ) -> -. E. x e. U. K x e. ( ( limPt ` K ) ` H ) )
1200	41 1199	condan	|- ( ph -> H e. Fin )