Theorem fourierdlem42 31820

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

Hypotheses

Ref	Expression
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 = sup ( 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

Ref	Expression
fourierdlem42	|- ( ph -> H e. Fin )

Distinct variable groups:   A, a, b, j, k, x   x, B   x, C   x, D   E, a, b, j, k   H, a, b, x   x, I   J, a, b   K, a, b, x   x, R   T, a, b, j, k, x   x, X   x, Y   ph, a, b, x   ps, j, k

Allowed substitution hints:   ph( j, k)   ps( x, a, b)   B( j, k, a, b)   C( j, k, a, b)   D( j, k, a, b)   R( j, k, a, b)   E( x)   H( j, k)   I( j, k, a, b)   J( x, j, k)   K( j, k)   X( j, k, a, b)   Y( j, k, a, b)

Proof of Theorem fourierdlem42

Dummy variables c d i l y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem42.x	. . . . 5 |- ( ph -> X e. RR )
2		fourierdlem42.y	. . . . 5 |- ( ph -> Y e. RR )
3		fourierdlem42.j	. . . . . 6 |- J = ( topGen ` ran (,) )
4		fourierdlem42.k	. . . . . 6 |- K = ( J ↾t ( X [,] Y ) )
5	3, 4	icccmp 21307	. . . . 5 |- ( ( X e. RR /\ Y e. RR ) -> K e. Comp )
6	1, 2, 5	syl2anc 661	. . . 4 |- ( ph -> K e. Comp )
7	6	adantr 465	. . 3 |- ( ( ph /\ -. H e. Fin ) -> K e. Comp )
8		fourierdlem42.h	. . . . . 6 |- H = { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A }
9		ssrab2 3570	. . . . . . 7 |- { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } C_ ( X [,] Y )
10	9	a1i 11	. . . . . 6 |- ( ph -> { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } C_ ( X [,] Y ) )
11	8, 10	syl5eqss 3533	. . . . 5 |- ( ph -> H C_ ( X [,] Y ) )
12		retop 21245	. . . . . . . 8 |- ( topGen ` ran (,) ) e. Top
13	3, 12	eqeltri 2527	. . . . . . 7 |- J e. Top
14	1, 2	iccssred 31475	. . . . . . 7 |- ( ph -> ( X [,] Y ) C_ RR )
15		uniretop 21246	. . . . . . . . 9 |- RR = U. ( topGen ` ran (,) )
16	3	unieqi 4243	. . . . . . . . 9 |- U. J = U. ( topGen ` ran (,) )
17	15, 16	eqtr4i 2475	. . . . . . . 8 |- RR = U. J
18	17	restuni 19640	. . . . . . 7 |- ( ( J e. Top /\ ( X [,] Y ) C_ RR ) -> ( X [,] Y ) = U. ( J ↾t ( X [,] Y ) ) )
19	13, 14, 18	sylancr 663	. . . . . 6 |- ( ph -> ( X [,] Y ) = U. ( J ↾t ( X [,] Y ) ) )
20	4	unieqi 4243	. . . . . . 7 |- U. K = U. ( J ↾t ( X [,] Y ) )
21	20	eqcomi 2456	. . . . . 6 |- U. ( J ↾t ( X [,] Y ) ) = U. K
22	19, 21	syl6eq 2500	. . . . 5 |- ( ph -> ( X [,] Y ) = U. K )
23	11, 22	sseqtrd 3525	. . . 4 |- ( ph -> H C_ U. K )
24	23	adantr 465	. . 3 |- ( ( ph /\ -. H e. Fin ) -> H C_ U. K )
25		simpr 461	. . 3 |- ( ( ph /\ -. H e. Fin ) -> -. H e. Fin )
26		eqid 2443	. . . 4 |- U. K = U. K
27	26	bwth 19887	. . 3 |- ( ( K e. Comp /\ H C_ U. K /\ -. H e. Fin ) -> E. x e. U. K x e. ( ( limPt ` K ) ` H ) )
28	7, 24, 25, 27	syl3anc 1229	. 2 |- ( ( ph /\ -. H e. Fin ) -> E. x e. U. K x e. ( ( limPt ` K ) ` H ) )
29	11, 14	sstrd 3499	. . . . . . . . . 10 |- ( ph -> H C_ RR )
30	29	ad2antrr 725	. . . . . . . . 9 |- ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> H C_ RR )
31		ne0i 3776	. . . . . . . . . 10 |- ( x e. ( ( limPt ` J ) ` H ) -> ( ( limPt ` J ) ` H ) =/= (/) )
32	31	adantl 466	. . . . . . . . 9 |- ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> ( ( limPt ` J ) ` H ) =/= (/) )
33		fourierdlem42.e	. . . . . . . . . . 11 |- E = sup ( R , RR , `' < )
34		fourierdlem42.r	. . . . . . . . . . . . 13 |- R = ran ( D |` I )
35		absf 13151	. . . . . . . . . . . . . . . . . 18 |- abs : CC --> RR
36		ffn 5721	. . . . . . . . . . . . . . . . . 18 |- ( abs : CC --> RR -> abs Fn CC )
37	35, 36	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- abs Fn CC
38		subf 9827	. . . . . . . . . . . . . . . . . 18 |- - : ( CC X. CC ) --> CC
39		ffn 5721	. . . . . . . . . . . . . . . . . 18 |- ( - : ( CC X. CC ) --> CC -> - Fn ( CC X. CC ) )
40	38, 39	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- - Fn ( CC X. CC )
41		frn 5727	. . . . . . . . . . . . . . . . . 18 |- ( - : ( CC X. CC ) --> CC -> ran - C_ CC )
42	38, 41	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ran - C_ CC
43		fnco 5679	. . . . . . . . . . . . . . . . 17 |- ( ( abs Fn CC /\ - Fn ( CC X. CC ) /\ ran - C_ CC ) -> ( abs o. - ) Fn ( CC X. CC ) )
44	37, 40, 42, 43	mp3an 1325	. . . . . . . . . . . . . . . 16 |- ( abs o. - ) Fn ( CC X. CC )
45		fourierdlem42.d	. . . . . . . . . . . . . . . . 17 |- D = ( abs o. - )
46	45	fneq1i 5665	. . . . . . . . . . . . . . . 16 |- ( D Fn ( CC X. CC ) <-> ( abs o. - ) Fn ( CC X. CC ) )
47	44, 46	mpbir 209	. . . . . . . . . . . . . . 15 |- D Fn ( CC X. CC )
48		fourierdlem42.i	. . . . . . . . . . . . . . . 16 |- I = ( ( A X. A ) \ _I )
49		fourierdlem42.a	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A C_ ( B [,] C ) )
50		fourierdlem42.b	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> B e. RR )
51		fourierdlem42.c	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> C e. RR )
52	50, 51	iccssred 31475	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( B [,] C ) C_ RR )
53		ax-resscn 9552	. . . . . . . . . . . . . . . . . . . 20 |- RR C_ CC
54	52, 53	syl6ss 3501	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( B [,] C ) C_ CC )
55	49, 54	sstrd 3499	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A C_ CC )
56		xpss12 5098	. . . . . . . . . . . . . . . . . 18 |- ( ( A C_ CC /\ A C_ CC ) -> ( A X. A ) C_ ( CC X. CC ) )
57	55, 55, 56	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( A X. A ) C_ ( CC X. CC ) )
58	57	ssdifssd 3627	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( A X. A ) \ _I ) C_ ( CC X. CC ) )
59	48, 58	syl5eqss 3533	. . . . . . . . . . . . . . 15 |- ( ph -> I C_ ( CC X. CC ) )
60		fnssres 5684	. . . . . . . . . . . . . . 15 |- ( ( D Fn ( CC X. CC ) /\ I C_ ( CC X. CC ) ) -> ( D |` I ) Fn I )
61	47, 59, 60	sylancr 663	. . . . . . . . . . . . . 14 |- ( ph -> ( D |` I ) Fn I )
62		fvres 5870	. . . . . . . . . . . . . . . . . . 19 |- ( x e. I -> ( ( D |` I ) ` x ) = ( D ` x ) )
63	62	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) = ( D ` x ) )
64	45	fveq1i 5857	. . . . . . . . . . . . . . . . . . 19 |- ( D ` x ) = ( ( abs o. - ) ` x )
65	64	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. I ) -> ( D ` x ) = ( ( abs o. - ) ` x ) )
66		ffun 5723	. . . . . . . . . . . . . . . . . . . 20 |- ( - : ( CC X. CC ) --> CC -> Fun - )
67	38, 66	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- Fun -
68	59	sselda 3489	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. I ) -> x e. ( CC X. CC ) )
69	38	fdmi 5726	. . . . . . . . . . . . . . . . . . . 20 |- dom - = ( CC X. CC )
70	68, 69	syl6eleqr 2542	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. I ) -> x e. dom - )
71		fvco 5934	. . . . . . . . . . . . . . . . . . 19 |- ( ( Fun - /\ x e. dom - ) -> ( ( abs o. - ) ` x ) = ( abs ` ( - ` x ) ) )
72	67, 70, 71	sylancr 663	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. I ) -> ( ( abs o. - ) ` x ) = ( abs ` ( - ` x ) ) )
73	63, 65, 72	3eqtrd 2488	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) = ( abs ` ( - ` x ) ) )
74	38	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. I ) -> - : ( CC X. CC ) --> CC )
75	74, 68	ffvelrnd 6017	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. I ) -> ( - ` x ) e. CC )
76	75	abscld 13248	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. I ) -> ( abs ` ( - ` x ) ) e. RR )
77	73, 76	eqeltrd 2531	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) e. RR )
78		elxp2 5007	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( CC X. CC ) <-> E. y e. CC E. z e. CC x = <. y , z >. )
79	68, 78	sylib 196	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. I ) -> E. y e. CC E. z e. CC x = <. y , z >. )
80		fveq2 5856	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = <. y , z >. -> ( - ` x ) = ( - ` <. y , z >. ) )
81	80	3ad2ant3 1020	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( - ` x ) = ( - ` <. y , z >. ) )
82		df-ov 6284	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y - z ) = ( - ` <. y , z >. )
83		simp1l 1021	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ph )
84		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. I /\ x = <. y , z >. ) -> x = <. y , z >. )
85		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. I /\ x = <. y , z >. ) -> x e. I )
86	84, 85	eqeltrrd 2532	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( x e. I /\ x = <. y , z >. ) -> <. y , z >. e. I )
87	86	adantll 713	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ x e. I ) /\ x = <. y , z >. ) -> <. y , z >. e. I )
88	87	3adant2 1016	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> <. y , z >. e. I )
89	55	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ <. y , z >. e. I ) -> A C_ CC )
90	48	eleq2i 2521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( <. y , z >. e. I <-> <. y , z >. e. ( ( A X. A ) \ _I ) )
91		eldif 3471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( <. y , z >. e. ( ( A X. A ) \ _I ) <-> ( <. y , z >. e. ( A X. A ) /\ -. <. y , z >. e. _I ) )
92	90, 91	sylbb 197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( <. y , z >. e. I -> ( <. y , z >. e. ( A X. A ) /\ -. <. y , z >. e. _I ) )
93	92	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( <. y , z >. e. I -> <. y , z >. e. ( A X. A ) )
94		opelxp 5019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( <. y , z >. e. ( A X. A ) <-> ( y e. A /\ z e. A ) )
95	93, 94	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( <. y , z >. e. I -> ( y e. A /\ z e. A ) )
96	95	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ <. y , z >. e. I ) -> ( y e. A /\ z e. A ) )
97	96	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ <. y , z >. e. I ) -> y e. A )
98	89, 97	sseldd 3490	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ <. y , z >. e. I ) -> y e. CC )
99	96	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ <. y , z >. e. I ) -> z e. A )
100	89, 99	sseldd 3490	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ <. y , z >. e. I ) -> z e. CC )
101	92	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( <. y , z >. e. I -> -. <. y , z >. e. _I )
102		df-br 4438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( y _I z <-> <. y , z >. e. _I )
103	101, 102	sylnibr 305	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( <. y , z >. e. I -> -. y _I z )
104		vex 3098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- z e. _V
105	104	ideq 5145	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( y _I z <-> y = z )
106	103, 105	sylnib 304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( <. y , z >. e. I -> -. y = z )
107	106	neqned 2646	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( <. y , z >. e. I -> y =/= z )
108	107	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ <. y , z >. e. I ) -> y =/= z )
109	98, 100, 108	subne0d 9945	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ <. y , z >. e. I ) -> ( y - z ) =/= 0 )
110	83, 88, 109	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( y - z ) =/= 0 )
111	82, 110	syl5eqner 2744	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( - ` <. y , z >. ) =/= 0 )
112	81, 111	eqnetrd 2736	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( - ` x ) =/= 0 )
113	112	3exp 1196	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. I ) -> ( ( y e. CC /\ z e. CC ) -> ( x = <. y , z >. -> ( - ` x ) =/= 0 ) ) )
114	113	rexlimdvv 2941	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. I ) -> ( E. y e. CC E. z e. CC x = <. y , z >. -> ( - ` x ) =/= 0 ) )
115	79, 114	mpd 15	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. I ) -> ( - ` x ) =/= 0 )
116		absgt0 13138	. . . . . . . . . . . . . . . . . . 19 |- ( ( - ` x ) e. CC -> ( ( - ` x ) =/= 0 <-> 0 < ( abs ` ( - ` x ) ) ) )
117	75, 116	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. I ) -> ( ( - ` x ) =/= 0 <-> 0 < ( abs ` ( - ` x ) ) ) )
118	115, 117	mpbid 210	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. I ) -> 0 < ( abs ` ( - ` x ) ) )
119	73	eqcomd 2451	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. I ) -> ( abs ` ( - ` x ) ) = ( ( D |` I ) ` x ) )
120	118, 119	breqtrd 4461	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. I ) -> 0 < ( ( D |` I ) ` x ) )
121	77, 120	elrpd 11264	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) e. RR+ )
122	121	ralrimiva 2857	. . . . . . . . . . . . . 14 |- ( ph -> A. x e. I ( ( D |` I ) ` x ) e. RR+ )
123		fnfvrnss 6044	. . . . . . . . . . . . . 14 |- ( ( ( D |` I ) Fn I /\ A. x e. I ( ( D |` I ) ` x ) e. RR+ ) -> ran ( D |` I ) C_ RR+ )
124	61, 122, 123	syl2anc 661	. . . . . . . . . . . . 13 |- ( ph -> ran ( D |` I ) C_ RR+ )
125	34, 124	syl5eqss 3533	. . . . . . . . . . . 12 |- ( ph -> R C_ RR+ )
126		ltso 9668	. . . . . . . . . . . . . . 15 |- < Or RR
127	126	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> < Or RR )
128		cnvso 5536	. . . . . . . . . . . . . 14 |- ( < Or RR <-> `' < Or RR )
129	127, 128	sylib 196	. . . . . . . . . . . . 13 |- ( ph -> `' < Or RR )
130		fourierdlem42.af	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A e. Fin )
131		xpfi 7793	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. Fin /\ A e. Fin ) -> ( A X. A ) e. Fin )
132	130, 130, 131	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( A X. A ) e. Fin )
133		diffi 7753	. . . . . . . . . . . . . . . . . 18 |- ( ( A X. A ) e. Fin -> ( ( A X. A ) \ _I ) e. Fin )
134	132, 133	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( A X. A ) \ _I ) e. Fin )
135	48, 134	syl5eqel 2535	. . . . . . . . . . . . . . . 16 |- ( ph -> I e. Fin )
136		fnfi 7800	. . . . . . . . . . . . . . . 16 |- ( ( ( D |` I ) Fn I /\ I e. Fin ) -> ( D |` I ) e. Fin )
137	61, 135, 136	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ph -> ( D |` I ) e. Fin )
138		rnfi 7807	. . . . . . . . . . . . . . 15 |- ( ( D |` I ) e. Fin -> ran ( D |` I ) e. Fin )
139	137, 138	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ran ( D |` I ) e. Fin )
140	34, 139	syl5eqel 2535	. . . . . . . . . . . . 13 |- ( ph -> R e. Fin )
141	34	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> R = ran ( D |` I ) )
142	45	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> D = ( abs o. - ) )
143	142	reseq1d 5262	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( D |` I ) = ( ( abs o. - ) |` I ) )
144	143	fveq1d 5858	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( D |` I ) ` <. B , C >. ) = ( ( ( abs o. - ) |` I ) ` <. B , C >. ) )
145		fourierdlem42.ba	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> B e. A )
146		fourierdlem42.ca	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> C e. A )
147		opelxp 5019	. . . . . . . . . . . . . . . . . . . . 21 |- ( <. B , C >. e. ( A X. A ) <-> ( B e. A /\ C e. A ) )
148	145, 146, 147	sylanbrc 664	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> <. B , C >. e. ( A X. A ) )
149		fourierdlem42.bc	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> B < C )
150	50, 149	ltned 9724	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> B =/= C )
151	150	neneqd 2645	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> -. B = C )
152		ideqg 5144	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( C e. A -> ( B _I C <-> B = C ) )
153	146, 152	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( B _I C <-> B = C ) )
154	151, 153	mtbird 301	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> -. B _I C )
155		df-br 4438	. . . . . . . . . . . . . . . . . . . . 21 |- ( B _I C <-> <. B , C >. e. _I )
156	154, 155	sylnib 304	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> -. <. B , C >. e. _I )
157	148, 156	eldifd 3472	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> <. B , C >. e. ( ( A X. A ) \ _I ) )
158	157, 48	syl6eleqr 2542	. . . . . . . . . . . . . . . . . 18 |- ( ph -> <. B , C >. e. I )
159		fvres 5870	. . . . . . . . . . . . . . . . . 18 |- ( <. B , C >. e. I -> ( ( ( abs o. - ) |` I ) ` <. B , C >. ) = ( ( abs o. - ) ` <. B , C >. ) )
160	158, 159	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( abs o. - ) |` I ) ` <. B , C >. ) = ( ( abs o. - ) ` <. B , C >. ) )
161	50	recnd 9625	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> B e. CC )
162	51	recnd 9625	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> C e. CC )
163		opelxp 5019	. . . . . . . . . . . . . . . . . . . . 21 |- ( <. B , C >. e. ( CC X. CC ) <-> ( B e. CC /\ C e. CC ) )
164	161, 162, 163	sylanbrc 664	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> <. B , C >. e. ( CC X. CC ) )
165	164, 69	syl6eleqr 2542	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> <. B , C >. e. dom - )
166		fvco 5934	. . . . . . . . . . . . . . . . . . 19 |- ( ( Fun - /\ <. B , C >. e. dom - ) -> ( ( abs o. - ) ` <. B , C >. ) = ( abs ` ( - ` <. B , C >. ) ) )
167	67, 165, 166	sylancr 663	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( abs o. - ) ` <. B , C >. ) = ( abs ` ( - ` <. B , C >. ) ) )
168		df-ov 6284	. . . . . . . . . . . . . . . . . . . . 21 |- ( B - C ) = ( - ` <. B , C >. )
169	168	eqcomi 2456	. . . . . . . . . . . . . . . . . . . 20 |- ( - ` <. B , C >. ) = ( B - C )
170	169	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( - ` <. B , C >. ) = ( B - C ) )
171	170	fveq2d 5860	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( abs ` ( - ` <. B , C >. ) ) = ( abs ` ( B - C ) ) )
172	167, 171	eqtrd 2484	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( abs o. - ) ` <. B , C >. ) = ( abs ` ( B - C ) ) )
173	144, 160, 172	3eqtrrd 2489	. . . . . . . . . . . . . . . 16 |- ( ph -> ( abs ` ( B - C ) ) = ( ( D |` I ) ` <. B , C >. ) )
174		fnfvelrn 6013	. . . . . . . . . . . . . . . . 17 |- ( ( ( D |` I ) Fn I /\ <. B , C >. e. I ) -> ( ( D |` I ) ` <. B , C >. ) e. ran ( D |` I ) )
175	61, 158, 174	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( D |` I ) ` <. B , C >. ) e. ran ( D |` I ) )
176	173, 175	eqeltrd 2531	. . . . . . . . . . . . . . 15 |- ( ph -> ( abs ` ( B - C ) ) e. ran ( D |` I ) )
177		ne0i 3776	. . . . . . . . . . . . . . 15 |- ( ( abs ` ( B - C ) ) e. ran ( D |` I ) -> ran ( D |` I ) =/= (/) )
178	176, 177	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ran ( D |` I ) =/= (/) )
179	141, 178	eqnetrd 2736	. . . . . . . . . . . . 13 |- ( ph -> R =/= (/) )
180		resss 5287	. . . . . . . . . . . . . . . . 17 |- ( D |` I ) C_ D
181		rnss 5221	. . . . . . . . . . . . . . . . 17 |- ( ( D |` I ) C_ D -> ran ( D |` I ) C_ ran D )
182	180, 181	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ran ( D |` I ) C_ ran D
183	45	rneqi 5219	. . . . . . . . . . . . . . . . 17 |- ran D = ran ( abs o. - )
184		rncoss 5253	. . . . . . . . . . . . . . . . . 18 |- ran ( abs o. - ) C_ ran abs
185		frn 5727	. . . . . . . . . . . . . . . . . . 19 |- ( abs : CC --> RR -> ran abs C_ RR )
186	35, 185	ax-mp 5	. . . . . . . . . . . . . . . . . 18 |- ran abs C_ RR
187	184, 186	sstri 3498	. . . . . . . . . . . . . . . . 17 |- ran ( abs o. - ) C_ RR
188	183, 187	eqsstri 3519	. . . . . . . . . . . . . . . 16 |- ran D C_ RR
189	182, 188	sstri 3498	. . . . . . . . . . . . . . 15 |- ran ( D |` I ) C_ RR
190	34, 189	eqsstri 3519	. . . . . . . . . . . . . 14 |- R C_ RR
191	190	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> R C_ RR )
192		fisupcl 7930	. . . . . . . . . . . . 13 |- ( ( `' < Or RR /\ ( R e. Fin /\ R =/= (/) /\ R C_ RR ) ) -> sup ( R , RR , `' < ) e. R )
193	129, 140, 179, 191, 192	syl13anc 1231	. . . . . . . . . . . 12 |- ( ph -> sup ( R , RR , `' < ) e. R )
194	125, 193	sseldd 3490	. . . . . . . . . . 11 |- ( ph -> sup ( R , RR , `' < ) e. RR+ )
195	33, 194	syl5eqel 2535	. . . . . . . . . 10 |- ( ph -> E e. RR+ )
196	195	ad2antrr 725	. . . . . . . . 9 |- ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> E e. RR+ )
197	3, 30, 32, 196	lptre2pt 31554	. . . . . . . 8 |- ( ( ( 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 753	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> ph )
199	29	sselda 3489	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. H ) -> y e. RR )
200	199	adantrr 716	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. H /\ z e. H ) ) -> y e. RR )
201	200	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> y e. RR )
202	29	sselda 3489	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. H ) -> z e. RR )
203	202	adantrl 715	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. H /\ z e. H ) ) -> z e. RR )
204	203	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> z e. RR )
205		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> y =/= z )
206	201, 204, 205	3jca 1177	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> ( y e. RR /\ z e. RR /\ y =/= z ) )
207	8	eleq2i 2521	. . . . . . . . . . . . . . . . . . 19 |- ( y e. H <-> y e. { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } )
208		oveq1 6288	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> ( x + ( k x. T ) ) = ( y + ( k x. T ) ) )
209	208	eleq1d 2512	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( ( x + ( k x. T ) ) e. A <-> ( y + ( k x. T ) ) e. A ) )
210	209	rexbidv 2954	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = y -> ( E. k e. ZZ ( x + ( k x. T ) ) e. A <-> E. k e. ZZ ( y + ( k x. T ) ) e. A ) )
211		oveq1 6288	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = j -> ( k x. T ) = ( j x. T ) )
212	211	oveq2d 6297	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k = j -> ( y + ( k x. T ) ) = ( y + ( j x. T ) ) )
213	212	eleq1d 2512	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k = j -> ( ( y + ( k x. T ) ) e. A <-> ( y + ( j x. T ) ) e. A ) )
214	213	cbvrexv 3071	. . . . . . . . . . . . . . . . . . . . 21 |- ( E. k e. ZZ ( y + ( k x. T ) ) e. A <-> E. j e. ZZ ( y + ( j x. T ) ) e. A )
215	210, 214	syl6bb 261	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 3243	. . . . . . . . . . . . . . . . . . 19 |- ( 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 197	. . . . . . . . . . . . . . . . . 18 |- ( y e. H -> ( y e. ( X [,] Y ) /\ E. j e. ZZ ( y + ( j x. T ) ) e. A ) )
218	217	simprd 463	. . . . . . . . . . . . . . . . 17 |- ( y e. H -> E. j e. ZZ ( y + ( j x. T ) ) e. A )
219	218	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( y e. H /\ z e. H ) -> E. j e. ZZ ( y + ( j x. T ) ) e. A )
220	8	eleq2i 2521	. . . . . . . . . . . . . . . . . . 19 |- ( z e. H <-> z e. { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } )
221		oveq1 6288	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( x + ( k x. T ) ) = ( z + ( k x. T ) ) )
222	221	eleq1d 2512	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = z -> ( ( x + ( k x. T ) ) e. A <-> ( z + ( k x. T ) ) e. A ) )
223	222	rexbidv 2954	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 3243	. . . . . . . . . . . . . . . . . . 19 |- ( 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 197	. . . . . . . . . . . . . . . . . 18 |- ( z e. H -> ( z e. ( X [,] Y ) /\ E. k e. ZZ ( z + ( k x. T ) ) e. A ) )
226	225	simprd 463	. . . . . . . . . . . . . . . . 17 |- ( z e. H -> E. k e. ZZ ( z + ( k x. T ) ) e. A )
227	226	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( y e. H /\ z e. H ) -> E. k e. ZZ ( z + ( k x. T ) ) e. A )
228		reeanv 3011	. . . . . . . . . . . . . . . 16 |- ( 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 664	. . . . . . . . . . . . . . 15 |- ( ( 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 726	. . . . . . . . . . . . . 14 |- ( ( ( 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 759	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 1000	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> y e. RR )
233		simpl2 1001	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> z e. RR )
234		simpr 461	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> y < z )
235	232, 233, 234	3jca 1177	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> ( y e. RR /\ z e. RR /\ y < z ) )
236	235	adantll 713	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ y < z ) -> ( y e. RR /\ z e. RR /\ y < z ) )
237	236	adantlr 714	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 755	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 2515	. . . . . . . . . . . . . . . . . . . . 21 |- ( b = z -> ( b e. RR <-> z e. RR ) )
240		breq2 4441	. . . . . . . . . . . . . . . . . . . . 21 |- ( b = z -> ( y < b <-> y < z ) )
241	239, 240	3anbi23d 1303	. . . . . . . . . . . . . . . . . . . 20 |- ( b = z -> ( ( y e. RR /\ b e. RR /\ y < b ) <-> ( y e. RR /\ z e. RR /\ y < z ) ) )
242	241	anbi2d 703	. . . . . . . . . . . . . . . . . . 19 |- ( b = z -> ( ( ph /\ ( y e. RR /\ b e. RR /\ y < b ) ) <-> ( ph /\ ( y e. RR /\ z e. RR /\ y < z ) ) ) )
243		oveq1 6288	. . . . . . . . . . . . . . . . . . . . . 22 |- ( b = z -> ( b + ( k x. T ) ) = ( z + ( k x. T ) ) )
244	243	eleq1d 2512	. . . . . . . . . . . . . . . . . . . . 21 |- ( b = z -> ( ( b + ( k x. T ) ) e. A <-> ( z + ( k x. T ) ) e. A ) )
245	244	anbi2d 703	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 2961	. . . . . . . . . . . . . . . . . . 19 |- ( 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 710	. . . . . . . . . . . . . . . . . 18 |- ( 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 6289	. . . . . . . . . . . . . . . . . . . 20 |- ( b = z -> ( y - b ) = ( y - z ) )
249	248	fveq2d 5860	. . . . . . . . . . . . . . . . . . 19 |- ( b = z -> ( abs ` ( y - b ) ) = ( abs ` ( y - z ) ) )
250	249	breq2d 4449	. . . . . . . . . . . . . . . . . 18 |- ( b = z -> ( E <_ ( abs ` ( y - b ) ) <-> E <_ ( abs ` ( y - z ) ) ) )
251	247, 250	imbi12d 320	. . . . . . . . . . . . . . . . 17 |- ( 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 2515	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = y -> ( a e. RR <-> y e. RR ) )
253		breq1 4440	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = y -> ( a < b <-> y < b ) )
254	252, 253	3anbi13d 1302	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = y -> ( ( a e. RR /\ b e. RR /\ a < b ) <-> ( y e. RR /\ b e. RR /\ y < b ) ) )
255	254	anbi2d 703	. . . . . . . . . . . . . . . . . . . 20 |- ( a = y -> ( ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) <-> ( ph /\ ( y e. RR /\ b e. RR /\ y < b ) ) ) )
256		oveq1 6288	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = y -> ( a + ( j x. T ) ) = ( y + ( j x. T ) ) )
257	256	eleq1d 2512	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = y -> ( ( a + ( j x. T ) ) e. A <-> ( y + ( j x. T ) ) e. A ) )
258	257	anbi1d 704	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 2961	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 710	. . . . . . . . . . . . . . . . . . 19 |- ( 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 6288	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = y -> ( a - b ) = ( y - b ) )
262	261	fveq2d 5860	. . . . . . . . . . . . . . . . . . . 20 |- ( a = y -> ( abs ` ( a - b ) ) = ( abs ` ( y - b ) ) )
263	262	breq2d 4449	. . . . . . . . . . . . . . . . . . 19 |- ( a = y -> ( E <_ ( abs ` ( a - b ) ) <-> E <_ ( abs ` ( y - b ) ) ) )
264	260, 263	imbi12d 320	. . . . . . . . . . . . . . . . . 18 |- ( 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		fourierdlem42.15	. . . . . . . . . . . . . . . . . . 19 |- ( 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 ) ) )
266	265	simprbi 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ps -> E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) )
267	265	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( 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 ) ) )
268	267	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ps -> ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) )
269	268	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ps -> ph )
270	269, 50	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ps -> B e. RR )
271	270	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> B e. RR )
272	269, 51	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ps -> C e. RR )
273	272	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> C e. RR )
274	269, 49	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ps -> A C_ ( B [,] C ) )
275	274	sselda 3489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ps /\ ( b + ( k x. T ) ) e. A ) -> ( b + ( k x. T ) ) e. ( B [,] C ) )
276	275	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( b + ( k x. T ) ) e. ( B [,] C ) )
277	274	sselda 3489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> ( a + ( j x. T ) ) e. ( B [,] C ) )
278	277	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) e. ( B [,] C ) )
279	271, 273, 276, 278	iccsuble 31495	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ ( C - B ) )
280		fourierdlem42.t	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- T = ( C - B )
281	279, 280	syl6breqr 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
282	281	3adant2 1016	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 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 )
283	282	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 )
284		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> -. k <_ j )
285		zre 10875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( j e. ZZ -> j e. RR )
286	285	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( j e. ZZ /\ k e. ZZ ) -> j e. RR )
287	286	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> j e. RR )
288		zre 10875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( k e. ZZ -> k e. RR )
289	288	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( j e. ZZ /\ k e. ZZ ) -> k e. RR )
290	289	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> k e. RR )
291	287, 290	ltnled 9735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> ( j < k <-> -. k <_ j ) )
292	284, 291	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> j < k )
293	51, 50	resubcld 9994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ph -> ( C - B ) e. RR )
294	280, 293	syl5eqel 2535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ph -> T e. RR )
295	269, 294	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ps -> T e. RR )
296	295	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T e. RR )
297	289	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> k e. RR )
298	286	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> j e. RR )
299	297, 298	resubcld 9994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k - j ) e. RR )
300	295	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> T e. RR )
301	299, 300	remulcld 9627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) e. RR )
302	301	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( ( k - j ) x. T ) e. RR )
303	268	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ps -> ( a e. RR /\ b e. RR /\ a < b ) )
304	303	simp2d 1010	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ps -> b e. RR )
305	304	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> b e. RR )
306	288	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ k e. ZZ ) -> k e. RR )
307	295	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ k e. ZZ ) -> T e. RR )
308	306, 307	remulcld 9627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ k e. ZZ ) -> ( k x. T ) e. RR )
309	308	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k x. T ) e. RR )
310	305, 309	readdcld 9626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( b + ( k x. T ) ) e. RR )
311	303	simp1d 1009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ps -> a e. RR )
312	311	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> a e. RR )
313	285	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ j e. ZZ ) -> j e. RR )
314	295	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ j e. ZZ ) -> T e. RR )
315	313, 314	remulcld 9627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ j e. ZZ ) -> ( j x. T ) e. RR )
316	315	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j x. T ) e. RR )
317	312, 316	readdcld 9626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( a + ( j x. T ) ) e. RR )
318	310, 317	resubcld 9994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) e. RR )
319	318	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) e. RR )
320	295	recnd 9625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ps -> T e. CC )
321	320	mulid2d 9617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ps -> ( 1 x. T ) = T )
322	321	eqcomd 2451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ps -> T = ( 1 x. T ) )
323	322	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T = ( 1 x. T ) )
324		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> j < k )
325		zltlem1 10923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( j e. ZZ /\ k e. ZZ ) -> ( j < k <-> j <_ ( k - 1 ) ) )
326	325	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( j < k <-> j <_ ( k - 1 ) ) )
327	324, 326	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> j <_ ( k - 1 ) )
328	286	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> j e. RR )
329		peano2rem 9891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( k e. RR -> ( k - 1 ) e. RR )
330	297, 329	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k - 1 ) e. RR )
331	330	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( k - 1 ) e. RR )
332		1re 9598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- 1 e. RR
333		resubcl 9888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( 1 e. RR /\ j e. RR ) -> ( 1 - j ) e. RR )
334	332, 328, 333	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( 1 - j ) e. RR )
335		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> j <_ ( k - 1 ) )
336	328, 331, 334, 335	leadd1dd 10173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( j + ( 1 - j ) ) <_ ( ( k - 1 ) + ( 1 - j ) ) )
337		zcn 10876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( j e. ZZ -> j e. CC )
338	337	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( j e. ZZ /\ k e. ZZ ) -> j e. CC )
339		1cnd 9615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( j e. ZZ /\ k e. ZZ ) -> 1 e. CC )
340	338, 339	pncan3d 9939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( j e. ZZ /\ k e. ZZ ) -> ( j + ( 1 - j ) ) = 1 )
341	340	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( j + ( 1 - j ) ) = 1 )
342		zcn 10876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( k e. ZZ -> k e. CC )
343	342	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( j e. ZZ /\ k e. ZZ ) -> k e. CC )
344	343, 339, 338	npncand 9960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( j e. ZZ /\ k e. ZZ ) -> ( ( k - 1 ) + ( 1 - j ) ) = ( k - j ) )
345	344	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( ( k - 1 ) + ( 1 - j ) ) = ( k - j ) )
346	336, 341, 345	3brtr3d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> 1 <_ ( k - j ) )
347	327, 346	syldan 470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> 1 <_ ( k - j ) )
348	332	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> 1 e. RR )
349	299	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( k - j ) e. RR )
350	50, 51	posdifd 10146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ph -> ( B < C <-> 0 < ( C - B ) ) )
351	149, 350	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ph -> 0 < ( C - B ) )
352	351, 280	syl6breqr 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> 0 < T )
353	294, 352	elrpd 11264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> T e. RR+ )
354	269, 353	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ps -> T e. RR+ )
355	354	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T e. RR+ )
356	348, 349, 355	lemul1d 11305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( 1 <_ ( k - j ) <-> ( 1 x. T ) <_ ( ( k - j ) x. T ) ) )
357	347, 356	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( 1 x. T ) <_ ( ( k - j ) x. T ) )
358	323, 357	eqbrtrd 4457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T <_ ( ( k - j ) x. T ) )
359	304, 311	resubcld 9994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ps -> ( b - a ) e. RR )
360	303	simp3d 1011	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ps -> a < b )
361	311, 304	posdifd 10146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ps -> ( a < b <-> 0 < ( b - a ) ) )
362	360, 361	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ps -> 0 < ( b - a ) )
363	359, 362	elrpd 11264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ps -> ( b - a ) e. RR+ )
364	363	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( b - a ) e. RR+ )
365	301, 364	ltaddrp2d 11296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) < ( ( b - a ) + ( ( k - j ) x. T ) ) )
366	304	recnd 9625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ps -> b e. CC )
367	366	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> b e. CC )
368	308	recnd 9625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ k e. ZZ ) -> ( k x. T ) e. CC )
369	368	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k x. T ) e. CC )
370	311	recnd 9625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ps -> a e. CC )
371	370	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> a e. CC )
372	315	recnd 9625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ j e. ZZ ) -> ( j x. T ) e. CC )
373	372	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j x. T ) e. CC )
374	367, 369, 371, 373	addsub4d 9983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) = ( ( b - a ) + ( ( k x. T ) - ( j x. T ) ) ) )
375	342	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> k e. CC )
376	337	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> j e. CC )
377	320	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> T e. CC )
378	375, 376, 377	subdird 10020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) = ( ( k x. T ) - ( j x. T ) ) )
379	378	eqcomd 2451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k x. T ) - ( j x. T ) ) = ( ( k - j ) x. T ) )
380	379	oveq2d 6297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b - a ) + ( ( k x. T ) - ( j x. T ) ) ) = ( ( b - a ) + ( ( k - j ) x. T ) ) )
381	374, 380	eqtr2d 2485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b - a ) + ( ( k - j ) x. T ) ) = ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
382	365, 381	breqtrd 4461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
383	382	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( ( k - j ) x. T ) < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
384	296, 302, 319, 358, 383	lelttrd 9743	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
385	296, 319	ltnled 9735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( 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 ) )
386	384, 385	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
387	292, 386	syldan 470	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
388	387	3adantl3 1155	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 )
389	283, 388	condan 794	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> k <_ j )
390	190, 193	sseldi 3487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> sup ( R , RR , `' < ) e. RR )
391	33, 390	syl5eqel 2535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> E e. RR )
392	269, 391	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ps -> E e. RR )
393	392	3ad2ant1 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E e. RR )
394	393	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( 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 )
395	295	3ad2ant1 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> T e. RR )
396	395	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( 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 )
397	286, 289	resubcld 9994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( j e. ZZ /\ k e. ZZ ) -> ( j - k ) e. RR )
398	397	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j - k ) e. RR )
399	398, 300	remulcld 9627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( j - k ) x. T ) e. RR )
400	399	3adant3 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( 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 )
401	400	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( 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 )
402		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ph -> ph )
403	145, 146	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ph -> ( B e. A /\ C e. A ) )
404	402, 403, 149	3jca 1177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) )
405		eleq1 2515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( d = C -> ( d e. A <-> C e. A ) )
406	405	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( d = C -> ( ( B e. A /\ d e. A ) <-> ( B e. A /\ C e. A ) ) )
407		breq2 4441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( d = C -> ( B < d <-> B < C ) )
408	406, 407	3anbi23d 1303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( d = C -> ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) <-> ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) ) )
409		oveq1 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( d = C -> ( d - B ) = ( C - B ) )
410	409	breq2d 4449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( d = C -> ( E <_ ( d - B ) <-> E <_ ( C - B ) ) )
411	408, 410	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( 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 ) ) ) )
412		simp2l 1023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> B e. A )
413		eleq1 2515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( c = B -> ( c e. A <-> B e. A ) )
414	413	anbi1d 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( c = B -> ( ( c e. A /\ d e. A ) <-> ( B e. A /\ d e. A ) ) )
415		breq1 4440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( c = B -> ( c < d <-> B < d ) )
416	414, 415	3anbi23d 1303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( c = B -> ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) <-> ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) ) )
417		oveq2 6289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( c = B -> ( d - c ) = ( d - B ) )
418	417	breq2d 4449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( c = B -> ( E <_ ( d - c ) <-> E <_ ( d - B ) ) )
419	416, 418	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( 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 ) ) ) )
420	190	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> R C_ RR )
421		0re 9599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- 0 e. RR
422	34	eleq2i 2521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( y e. R <-> y e. ran ( D |` I ) )
423	422	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( y e. R -> y e. ran ( D |` I ) )
424	423	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ y e. R ) -> y e. ran ( D |` I ) )
425	61	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ y e. R ) -> ( D |` I ) Fn I )
426		fvelrnb 5905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( D |` I ) Fn I -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) )
427	425, 426	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ y e. R ) -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) )
428	424, 427	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ y e. R ) -> E. x e. I ( ( D |` I ) ` x ) = y )
429	121	rpge0d 11270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ x e. I ) -> 0 <_ ( ( D |` I ) ` x ) )
430	429	3adant3 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> 0 <_ ( ( D |` I ) ` x ) )
431		simp3 999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> ( ( D |` I ) ` x ) = y )
432	430, 431	breqtrd 4461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> 0 <_ y )
433	432	3exp 1196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ph -> ( x e. I -> ( ( ( D |` I ) ` x ) = y -> 0 <_ y ) ) )
434	433	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ y e. R ) -> ( x e. I -> ( ( ( D |` I ) ` x ) = y -> 0 <_ y ) ) )
435	434	rexlimdv 2933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ y e. R ) -> ( E. x e. I ( ( D |` I ) ` x ) = y -> 0 <_ y ) )
436	428, 435	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ y e. R ) -> 0 <_ y )
437	436	ralrimiva 2857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ph -> A. y e. R 0 <_ y )
438		breq1 4440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( x = 0 -> ( x <_ y <-> 0 <_ y ) )
439	438	ralbidv 2882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( x = 0 -> ( A. y e. R x <_ y <-> A. y e. R 0 <_ y ) )
440	439	rspcev 3196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( 0 e. RR /\ A. y e. R 0 <_ y ) -> E. x e. RR A. y e. R x <_ y )
441	421, 437, 440	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ph -> E. x e. RR A. y e. R x <_ y )
442	441	3ad2ant1 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E. x e. RR A. y e. R x <_ y )
443		pm3.22 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( c e. A /\ d e. A ) -> ( d e. A /\ c e. A ) )
444		opelxp 5019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( <. d , c >. e. ( A X. A ) <-> ( d e. A /\ c e. A ) )
445	443, 444	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( c e. A /\ d e. A ) -> <. d , c >. e. ( A X. A ) )
446	445	3ad2ant2 1019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. ( A X. A ) )
447	49, 52	sstrd 3499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( ph -> A C_ RR )
448	447	sselda 3489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ph /\ c e. A ) -> c e. RR )
449	448	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ ( c e. A /\ d e. A ) ) -> c e. RR )
450	449	3adant3 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c e. RR )
451		simp3 999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c < d )
452	450, 451	gtned 9723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> d =/= c )
453	452	neneqd 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> -. d = c )
454		df-br 4438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( d _I c <-> <. d , c >. e. _I )
455		vex 3098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- c e. _V
456	455	ideq 5145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( d _I c <-> d = c )
457	454, 456	bitr3i 251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( <. d , c >. e. _I <-> d = c )
458	453, 457	sylnibr 305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> -. <. d , c >. e. _I )
459	446, 458	eldifd 3472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. ( ( A X. A ) \ _I ) )
460	459, 48	syl6eleqr 2542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. I )
461	450, 451	ltned 9724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c =/= d )
462	143	3ad2ant1 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( D |` I ) = ( ( abs o. - ) |` I ) )
463	462	fveq1d 5858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( D |` I ) ` <. d , c >. ) = ( ( ( abs o. - ) |` I ) ` <. d , c >. ) )
464	445	3ad2ant2 1019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. ( A X. A ) )
465		necom 2712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ( c =/= d <-> d =/= c )
466	465	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ( c =/= d -> d =/= c )
467	466	neneqd 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( c =/= d -> -. d = c )
468	467	3ad2ant3 1020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> -. d = c )
469	468, 457	sylnibr 305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> -. <. d , c >. e. _I )
470	464, 469	eldifd 3472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. ( ( A X. A ) \ _I ) )
471	470, 48	syl6eleqr 2542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. I )
472		fvres 5870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( <. d , c >. e. I -> ( ( ( abs o. - ) |` I ) ` <. d , c >. ) = ( ( abs o. - ) ` <. d , c >. ) )
473	471, 472	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( ( abs o. - ) |` I ) ` <. d , c >. ) = ( ( abs o. - ) ` <. d , c >. ) )
474		simp1 997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ph )
475	474, 471	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ph /\ <. d , c >. e. I ) )
476		eleq1 2515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ( x = <. d , c >. -> ( x e. I <-> <. d , c >. e. I ) )
477	476	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( x = <. d , c >. -> ( ( ph /\ x e. I ) <-> ( ph /\ <. d , c >. e. I ) ) )
478		eleq1 2515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( x = <. d , c >. -> ( x e. dom - <-> <. d , c >. e. dom - ) )
479	477, 478	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( x = <. d , c >. -> ( ( ( ph /\ x e. I ) -> x e. dom - ) <-> ( ( ph /\ <. d , c >. e. I ) -> <. d , c >. e. dom - ) ) )
480	479, 70	vtoclg 3153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( <. d , c >. e. I -> ( ( ph /\ <. d , c >. e. I ) -> <. d , c >. e. dom - ) )
481	471, 475, 480	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. dom - )
482		fvco 5934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( Fun - /\ <. d , c >. e. dom - ) -> ( ( abs o. - ) ` <. d , c >. ) = ( abs ` ( - ` <. d , c >. ) ) )
483	67, 481, 482	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( abs o. - ) ` <. d , c >. ) = ( abs ` ( - ` <. d , c >. ) ) )
484		df-ov 6284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( d - c ) = ( - ` <. d , c >. )
485	484	eqcomi 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( - ` <. d , c >. ) = ( d - c )
486	485	fveq2i 5859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( abs ` ( - ` <. d , c >. ) ) = ( abs ` ( d - c ) )
487	483, 486	syl6eq 2500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( abs o. - ) ` <. d , c >. ) = ( abs ` ( d - c ) ) )
488	463, 473, 487	3eqtrd 2488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( D |` I ) ` <. d , c >. ) = ( abs ` ( d - c ) ) )
489	461, 488	syld3an3 1274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( ( D |` I ) ` <. d , c >. ) = ( abs ` ( d - c ) ) )
490	447	sselda 3489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ d e. A ) -> d e. RR )
491	490	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ ( c e. A /\ d e. A ) ) -> d e. RR )
492	491	3adant3 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> d e. RR )
493	450, 492, 451	ltled 9736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c <_ d )
494	450, 492, 493	abssubge0d 13244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( abs ` ( d - c ) ) = ( d - c ) )
495	489, 494	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( ( D |` I ) ` <. d , c >. ) = ( d - c ) )
496		fveq2 5856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( x = <. d , c >. -> ( ( D |` I ) ` x ) = ( ( D |` I ) ` <. d , c >. ) )
497	496	eqeq1d 2445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( x = <. d , c >. -> ( ( ( D |` I ) ` x ) = ( d - c ) <-> ( ( D |` I ) ` <. d , c >. ) = ( d - c ) ) )
498	497	rspcev 3196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( <. d , c >. e. I /\ ( ( D |` I ) ` <. d , c >. ) = ( d - c ) ) -> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) )
499	460, 495, 498	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) )
500	491, 449	resubcld 9994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) ) -> ( d - c ) e. RR )
501		elex 3104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( d - c ) e. RR -> ( d - c ) e. _V )
502	500, 501	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ ( c e. A /\ d e. A ) ) -> ( d - c ) e. _V )
503	502	3adant3 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( d - c ) e. _V )
504		simp1 997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ph )
505		eleq1 2515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( y = ( d - c ) -> ( y e. ran ( D |` I ) <-> ( d - c ) e. ran ( D |` I ) ) )
506		eqeq2 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( y = ( d - c ) -> ( ( ( D |` I ) ` x ) = y <-> ( ( D |` I ) ` x ) = ( d - c ) ) )
507	506	rexbidv 2954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( y = ( d - c ) -> ( E. x e. I ( ( D |` I ) ` x ) = y <-> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) ) )
508	505, 507	bibi12d 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( 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 ) ) ) )
509	508	imbi2d 316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( 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 ) ) ) ) )
510	61, 426	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ph -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) )
511	509, 510	vtoclg 3153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( d - c ) e. _V -> ( ph -> ( ( d - c ) e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) ) ) )
512	503, 504, 511	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( ( d - c ) e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) ) )
513	499, 512	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( d - c ) e. ran ( D |` I ) )
514	513, 34	syl6eleqr 2542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( d - c ) e. R )
515		infmrlb 10531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( R C_ RR /\ E. x e. RR A. y e. R x <_ y /\ ( d - c ) e. R ) -> sup ( R , RR , `' < ) <_ ( d - c ) )
516	420, 442, 514, 515	syl3anc 1229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> sup ( R , RR , `' < ) <_ ( d - c ) )
517	33, 516	syl5eqbr 4470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E <_ ( d - c ) )
518	419, 517	vtoclg 3153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( B e. A -> ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> E <_ ( d - B ) ) )
519	412, 518	mpcom 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> E <_ ( d - B ) )
520	411, 519	vtoclg 3153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( C e. A -> ( ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) -> E <_ ( C - B ) ) )
521	146, 404, 520	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> E <_ ( C - B ) )
522	521, 280	syl6breqr 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> E <_ T )
523	269, 522	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ps -> E <_ T )
524	523	3ad2ant1 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ T )
525	524	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( 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 )
526	366	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ps /\ k e. ZZ ) -> b e. CC )
527	526, 368	pncan2d 9938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ps /\ k e. ZZ ) -> ( ( b + ( k x. T ) ) - b ) = ( k x. T ) )
528	527	oveq1d 6296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ps /\ k e. ZZ ) -> ( ( ( b + ( k x. T ) ) - b ) / T ) = ( ( k x. T ) / T ) )
529	342	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ps /\ k e. ZZ ) -> k e. CC )
530	320	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ps /\ k e. ZZ ) -> T e. CC )
531	421	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ph -> 0 e. RR )
532	531, 352	gtned 9723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ph -> T =/= 0 )
533	269, 532	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ps -> T =/= 0 )
534	533	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ps /\ k e. ZZ ) -> T =/= 0 )
535	529, 530, 534	divcan4d 10333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ps /\ k e. ZZ ) -> ( ( k x. T ) / T ) = k )
536	528, 535	eqtr2d 2485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ps /\ k e. ZZ ) -> k = ( ( ( b + ( k x. T ) ) - b ) / T ) )
537	536	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> k = ( ( ( b + ( k x. T ) ) - b ) / T ) )
538	537	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> k = ( ( ( b + ( k x. T ) ) - b ) / T ) )
539		oveq1 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( a + ( j x. T ) ) = ( b + ( k x. T ) ) -> ( ( a + ( j x. T ) ) - b ) = ( ( b + ( k x. T ) ) - b ) )
540	539	oveq1d 6296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( a + ( j x. T ) ) = ( b + ( k x. T ) ) -> ( ( ( a + ( j x. T ) ) - b