Theorem fourierdlem42 38124

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

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 = 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

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 21921	. . . . 5 |- ( ( X e. RR /\ Y e. RR ) -> K e. Comp )
6	1, 2, 5	syl2anc 673	. . . 4 |- ( ph -> K e. Comp )
7	6	adantr 472	. . 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 3500	. . . . . . 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 3462	. . . . 5 |- ( ph -> H C_ ( X [,] Y ) )
12		retop 21860	. . . . . . . 8 |- ( topGen ` ran (,) ) e. Top
13	3, 12	eqeltri 2545	. . . . . . 7 |- J e. Top
14	1, 2	iccssred 37698	. . . . . . 7 |- ( ph -> ( X [,] Y ) C_ RR )
15		uniretop 21861	. . . . . . . . 9 |- RR = U. ( topGen ` ran (,) )
16	3	unieqi 4199	. . . . . . . . 9 |- U. J = U. ( topGen ` ran (,) )
17	15, 16	eqtr4i 2496	. . . . . . . 8 |- RR = U. J
18	17	restuni 20255	. . . . . . 7 |- ( ( J e. Top /\ ( X [,] Y ) C_ RR ) -> ( X [,] Y ) = U. ( J ↾t ( X [,] Y ) ) )
19	13, 14, 18	sylancr 676	. . . . . 6 |- ( ph -> ( X [,] Y ) = U. ( J ↾t ( X [,] Y ) ) )
20	4	unieqi 4199	. . . . . . 7 |- U. K = U. ( J ↾t ( X [,] Y ) )
21	20	eqcomi 2480	. . . . . 6 |- U. ( J ↾t ( X [,] Y ) ) = U. K
22	19, 21	syl6eq 2521	. . . . 5 |- ( ph -> ( X [,] Y ) = U. K )
23	11, 22	sseqtrd 3454	. . . 4 |- ( ph -> H C_ U. K )
24	23	adantr 472	. . 3 |- ( ( ph /\ -. H e. Fin ) -> H C_ U. K )
25		simpr 468	. . 3 |- ( ( ph /\ -. H e. Fin ) -> -. H e. Fin )
26		eqid 2471	. . . 4 |- U. K = U. K
27	26	bwth 20502	. . 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 1292	. 2 |- ( ( ph /\ -. H e. Fin ) -> E. x e. U. K x e. ( ( limPt ` K ) ` H ) )
29	11, 14	sstrd 3428	. . . . . . . . . 10 |- ( ph -> H C_ RR )
30	29	ad2antrr 740	. . . . . . . . 9 |- ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> H C_ RR )
31		ne0i 3728	. . . . . . . . . 10 |- ( x e. ( ( limPt ` J ) ` H ) -> ( ( limPt ` J ) ` H ) =/= (/) )
32	31	adantl 473	. . . . . . . . 9 |- ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> ( ( limPt ` J ) ` H ) =/= (/) )
33		fourierdlem42.e	. . . . . . . . . . 11 |- E = inf ( R , RR , < )
34		fourierdlem42.r	. . . . . . . . . . . . 13 |- R = ran ( D |` I )
35		absf 13477	. . . . . . . . . . . . . . . . . 18 |- abs : CC --> RR
36		ffn 5739	. . . . . . . . . . . . . . . . . 18 |- ( abs : CC --> RR -> abs Fn CC )
37	35, 36	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- abs Fn CC
38		subf 9897	. . . . . . . . . . . . . . . . . 18 |- - : ( CC X. CC ) --> CC
39		ffn 5739	. . . . . . . . . . . . . . . . . 18 |- ( - : ( CC X. CC ) --> CC -> - Fn ( CC X. CC ) )
40	38, 39	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- - Fn ( CC X. CC )
41		frn 5747	. . . . . . . . . . . . . . . . . 18 |- ( - : ( CC X. CC ) --> CC -> ran - C_ CC )
42	38, 41	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ran - C_ CC
43		fnco 5694	. . . . . . . . . . . . . . . . 17 |- ( ( abs Fn CC /\ - Fn ( CC X. CC ) /\ ran - C_ CC ) -> ( abs o. - ) Fn ( CC X. CC ) )
44	37, 40, 42, 43	mp3an 1390	. . . . . . . . . . . . . . . 16 |- ( abs o. - ) Fn ( CC X. CC )
45		fourierdlem42.d	. . . . . . . . . . . . . . . . 17 |- D = ( abs o. - )
46	45	fneq1i 5680	. . . . . . . . . . . . . . . 16 |- ( D Fn ( CC X. CC ) <-> ( abs o. - ) Fn ( CC X. CC ) )
47	44, 46	mpbir 214	. . . . . . . . . . . . . . 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 37698	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( B [,] C ) C_ RR )
53		ax-resscn 9614	. . . . . . . . . . . . . . . . . . . 20 |- RR C_ CC
54	52, 53	syl6ss 3430	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( B [,] C ) C_ CC )
55	49, 54	sstrd 3428	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A C_ CC )
56		xpss12 4945	. . . . . . . . . . . . . . . . . 18 |- ( ( A C_ CC /\ A C_ CC ) -> ( A X. A ) C_ ( CC X. CC ) )
57	55, 55, 56	syl2anc 673	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( A X. A ) C_ ( CC X. CC ) )
58	57	ssdifssd 3560	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( A X. A ) \ _I ) C_ ( CC X. CC ) )
59	48, 58	syl5eqss 3462	. . . . . . . . . . . . . . 15 |- ( ph -> I C_ ( CC X. CC ) )
60		fnssres 5699	. . . . . . . . . . . . . . 15 |- ( ( D Fn ( CC X. CC ) /\ I C_ ( CC X. CC ) ) -> ( D |` I ) Fn I )
61	47, 59, 60	sylancr 676	. . . . . . . . . . . . . 14 |- ( ph -> ( D |` I ) Fn I )
62		fvres 5893	. . . . . . . . . . . . . . . . . . 19 |- ( x e. I -> ( ( D |` I ) ` x ) = ( D ` x ) )
63	62	adantl 473	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) = ( D ` x ) )
64	45	fveq1i 5880	. . . . . . . . . . . . . . . . . . 19 |- ( D ` x ) = ( ( abs o. - ) ` x )
65	64	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. I ) -> ( D ` x ) = ( ( abs o. - ) ` x ) )
66		ffun 5742	. . . . . . . . . . . . . . . . . . . 20 |- ( - : ( CC X. CC ) --> CC -> Fun - )
67	38, 66	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- Fun -
68	59	sselda 3418	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. I ) -> x e. ( CC X. CC ) )
69	38	fdmi 5746	. . . . . . . . . . . . . . . . . . . 20 |- dom - = ( CC X. CC )
70	68, 69	syl6eleqr 2560	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. I ) -> x e. dom - )
71		fvco 5956	. . . . . . . . . . . . . . . . . . 19 |- ( ( Fun - /\ x e. dom - ) -> ( ( abs o. - ) ` x ) = ( abs ` ( - ` x ) ) )
72	67, 70, 71	sylancr 676	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. I ) -> ( ( abs o. - ) ` x ) = ( abs ` ( - ` x ) ) )
73	63, 65, 72	3eqtrd 2509	. . . . . . . . . . . . . . . . 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 6038	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. I ) -> ( - ` x ) e. CC )
76	75	abscld 13575	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. I ) -> ( abs ` ( - ` x ) ) e. RR )
77	73, 76	eqeltrd 2549	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) e. RR )
78		elxp2 4857	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( CC X. CC ) <-> E. y e. CC E. z e. CC x = <. y , z >. )
79	68, 78	sylib 201	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. I ) -> E. y e. CC E. z e. CC x = <. y , z >. )
80		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = <. y , z >. -> ( - ` x ) = ( - ` <. y , z >. ) )
81	80	3ad2ant3 1053	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( - ` x ) = ( - ` <. y , z >. ) )
82		df-ov 6311	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y - z ) = ( - ` <. y , z >. )
83		simp1l 1054	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ph )
84		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. I /\ x = <. y , z >. ) -> x = <. y , z >. )
85		simpl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. I /\ x = <. y , z >. ) -> x e. I )
86	84, 85	eqeltrrd 2550	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( x e. I /\ x = <. y , z >. ) -> <. y , z >. e. I )
87	86	adantll 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ x e. I ) /\ x = <. y , z >. ) -> <. y , z >. e. I )
88	87	3adant2 1049	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> <. y , z >. e. I )
89	55	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ <. y , z >. e. I ) -> A C_ CC )
90	48	eleq2i 2541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( <. y , z >. e. I <-> <. y , z >. e. ( ( A X. A ) \ _I ) )
91		eldif 3400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( <. y , z >. e. ( ( A X. A ) \ _I ) <-> ( <. y , z >. e. ( A X. A ) /\ -. <. y , z >. e. _I ) )
92	90, 91	sylbb 202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( <. y , z >. e. I -> ( <. y , z >. e. ( A X. A ) /\ -. <. y , z >. e. _I ) )
93	92	simpld 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( <. y , z >. e. I -> <. y , z >. e. ( A X. A ) )
94		opelxp 4869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( <. y , z >. e. ( A X. A ) <-> ( y e. A /\ z e. A ) )
95	93, 94	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( <. y , z >. e. I -> ( y e. A /\ z e. A ) )
96	95	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ <. y , z >. e. I ) -> ( y e. A /\ z e. A ) )
97	96	simpld 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ <. y , z >. e. I ) -> y e. A )
98	89, 97	sseldd 3419	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ <. y , z >. e. I ) -> y e. CC )
99	96	simprd 470	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ <. y , z >. e. I ) -> z e. A )
100	89, 99	sseldd 3419	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ <. y , z >. e. I ) -> z e. CC )
101	92	simprd 470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( <. y , z >. e. I -> -. <. y , z >. e. _I )
102		df-br 4396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( y _I z <-> <. y , z >. e. _I )
103	101, 102	sylnibr 312	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( <. y , z >. e. I -> -. y _I z )
104		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- z e. _V
105	104	ideq 4992	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( y _I z <-> y = z )
106	103, 105	sylnib 311	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( <. y , z >. e. I -> -. y = z )
107	106	neqned 2650	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( <. y , z >. e. I -> y =/= z )
108	107	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ <. y , z >. e. I ) -> y =/= z )
109	98, 100, 108	subne0d 10014	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ <. y , z >. e. I ) -> ( y - z ) =/= 0 )
110	83, 88, 109	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( y - z ) =/= 0 )
111	82, 110	syl5eqner 2718	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( - ` <. y , z >. ) =/= 0 )
112	81, 111	eqnetrd 2710	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( - ` x ) =/= 0 )
113	112	3exp 1230	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. I ) -> ( ( y e. CC /\ z e. CC ) -> ( x = <. y , z >. -> ( - ` x ) =/= 0 ) ) )
114	113	rexlimdvv 2877	. . . . . . . . . . . . . . . . . . 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 13464	. . . . . . . . . . . . . . . . . . 19 |- ( ( - ` x ) e. CC -> ( ( - ` x ) =/= 0 <-> 0 < ( abs ` ( - ` x ) ) ) )
117	75, 116	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. I ) -> ( ( - ` x ) =/= 0 <-> 0 < ( abs ` ( - ` x ) ) ) )
118	115, 117	mpbid 215	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. I ) -> 0 < ( abs ` ( - ` x ) ) )
119	73	eqcomd 2477	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. I ) -> ( abs ` ( - ` x ) ) = ( ( D |` I ) ` x ) )
120	118, 119	breqtrd 4420	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. I ) -> 0 < ( ( D |` I ) ` x ) )
121	77, 120	elrpd 11361	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) e. RR+ )
122	121	ralrimiva 2809	. . . . . . . . . . . . . 14 |- ( ph -> A. x e. I ( ( D |` I ) ` x ) e. RR+ )
123		fnfvrnss 6066	. . . . . . . . . . . . . 14 |- ( ( ( D |` I ) Fn I /\ A. x e. I ( ( D |` I ) ` x ) e. RR+ ) -> ran ( D |` I ) C_ RR+ )
124	61, 122, 123	syl2anc 673	. . . . . . . . . . . . 13 |- ( ph -> ran ( D |` I ) C_ RR+ )
125	34, 124	syl5eqss 3462	. . . . . . . . . . . 12 |- ( ph -> R C_ RR+ )
126		ltso 9732	. . . . . . . . . . . . . 14 |- < Or RR
127	126	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> < Or RR )
128		fourierdlem42.af	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A e. Fin )
129		xpfi 7860	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. Fin /\ A e. Fin ) -> ( A X. A ) e. Fin )
130	128, 128, 129	syl2anc 673	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( A X. A ) e. Fin )
131		diffi 7821	. . . . . . . . . . . . . . . . . 18 |- ( ( A X. A ) e. Fin -> ( ( A X. A ) \ _I ) e. Fin )
132	130, 131	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( A X. A ) \ _I ) e. Fin )
133	48, 132	syl5eqel 2553	. . . . . . . . . . . . . . . 16 |- ( ph -> I e. Fin )
134		fnfi 7867	. . . . . . . . . . . . . . . 16 |- ( ( ( D |` I ) Fn I /\ I e. Fin ) -> ( D |` I ) e. Fin )
135	61, 133, 134	syl2anc 673	. . . . . . . . . . . . . . 15 |- ( ph -> ( D |` I ) e. Fin )
136		rnfi 7875	. . . . . . . . . . . . . . 15 |- ( ( D |` I ) e. Fin -> ran ( D |` I ) e. Fin )
137	135, 136	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ran ( D |` I ) e. Fin )
138	34, 137	syl5eqel 2553	. . . . . . . . . . . . 13 |- ( ph -> R e. Fin )
139	34	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> R = ran ( D |` I ) )
140	45	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> D = ( abs o. - ) )
141	140	reseq1d 5110	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( D |` I ) = ( ( abs o. - ) |` I ) )
142	141	fveq1d 5881	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( D |` I ) ` <. B , C >. ) = ( ( ( abs o. - ) |` I ) ` <. B , C >. ) )
143		fourierdlem42.ba	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> B e. A )
144		fourierdlem42.ca	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> C e. A )
145		opelxp 4869	. . . . . . . . . . . . . . . . . . . . 21 |- ( <. B , C >. e. ( A X. A ) <-> ( B e. A /\ C e. A ) )
146	143, 144, 145	sylanbrc 677	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> <. B , C >. e. ( A X. A ) )
147		fourierdlem42.bc	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> B < C )
148	50, 147	ltned 9788	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> B =/= C )
149	148	neneqd 2648	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> -. B = C )
150		ideqg 4991	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( C e. A -> ( B _I C <-> B = C ) )
151	144, 150	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( B _I C <-> B = C ) )
152	149, 151	mtbird 308	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> -. B _I C )
153		df-br 4396	. . . . . . . . . . . . . . . . . . . . 21 |- ( B _I C <-> <. B , C >. e. _I )
154	152, 153	sylnib 311	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> -. <. B , C >. e. _I )
155	146, 154	eldifd 3401	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> <. B , C >. e. ( ( A X. A ) \ _I ) )
156	155, 48	syl6eleqr 2560	. . . . . . . . . . . . . . . . . 18 |- ( ph -> <. B , C >. e. I )
157		fvres 5893	. . . . . . . . . . . . . . . . . 18 |- ( <. B , C >. e. I -> ( ( ( abs o. - ) |` I ) ` <. B , C >. ) = ( ( abs o. - ) ` <. B , C >. ) )
158	156, 157	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( abs o. - ) |` I ) ` <. B , C >. ) = ( ( abs o. - ) ` <. B , C >. ) )
159	50	recnd 9687	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> B e. CC )
160	51	recnd 9687	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> C e. CC )
161		opelxp 4869	. . . . . . . . . . . . . . . . . . . . 21 |- ( <. B , C >. e. ( CC X. CC ) <-> ( B e. CC /\ C e. CC ) )
162	159, 160, 161	sylanbrc 677	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> <. B , C >. e. ( CC X. CC ) )
163	162, 69	syl6eleqr 2560	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> <. B , C >. e. dom - )
164		fvco 5956	. . . . . . . . . . . . . . . . . . 19 |- ( ( Fun - /\ <. B , C >. e. dom - ) -> ( ( abs o. - ) ` <. B , C >. ) = ( abs ` ( - ` <. B , C >. ) ) )
165	67, 163, 164	sylancr 676	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( abs o. - ) ` <. B , C >. ) = ( abs ` ( - ` <. B , C >. ) ) )
166		df-ov 6311	. . . . . . . . . . . . . . . . . . . . 21 |- ( B - C ) = ( - ` <. B , C >. )
167	166	eqcomi 2480	. . . . . . . . . . . . . . . . . . . 20 |- ( - ` <. B , C >. ) = ( B - C )
168	167	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( - ` <. B , C >. ) = ( B - C ) )
169	168	fveq2d 5883	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( abs ` ( - ` <. B , C >. ) ) = ( abs ` ( B - C ) ) )
170	165, 169	eqtrd 2505	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( abs o. - ) ` <. B , C >. ) = ( abs ` ( B - C ) ) )
171	142, 158, 170	3eqtrrd 2510	. . . . . . . . . . . . . . . 16 |- ( ph -> ( abs ` ( B - C ) ) = ( ( D |` I ) ` <. B , C >. ) )
172		fnfvelrn 6034	. . . . . . . . . . . . . . . . 17 |- ( ( ( D |` I ) Fn I /\ <. B , C >. e. I ) -> ( ( D |` I ) ` <. B , C >. ) e. ran ( D |` I ) )
173	61, 156, 172	syl2anc 673	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( D |` I ) ` <. B , C >. ) e. ran ( D |` I ) )
174	171, 173	eqeltrd 2549	. . . . . . . . . . . . . . 15 |- ( ph -> ( abs ` ( B - C ) ) e. ran ( D |` I ) )
175		ne0i 3728	. . . . . . . . . . . . . . 15 |- ( ( abs ` ( B - C ) ) e. ran ( D |` I ) -> ran ( D |` I ) =/= (/) )
176	174, 175	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ran ( D |` I ) =/= (/) )
177	139, 176	eqnetrd 2710	. . . . . . . . . . . . 13 |- ( ph -> R =/= (/) )
178		resss 5134	. . . . . . . . . . . . . . . . 17 |- ( D |` I ) C_ D
179		rnss 5069	. . . . . . . . . . . . . . . . 17 |- ( ( D |` I ) C_ D -> ran ( D |` I ) C_ ran D )
180	178, 179	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ran ( D |` I ) C_ ran D
181	45	rneqi 5067	. . . . . . . . . . . . . . . . 17 |- ran D = ran ( abs o. - )
182		rncoss 5101	. . . . . . . . . . . . . . . . . 18 |- ran ( abs o. - ) C_ ran abs
183		frn 5747	. . . . . . . . . . . . . . . . . . 19 |- ( abs : CC --> RR -> ran abs C_ RR )
184	35, 183	ax-mp 5	. . . . . . . . . . . . . . . . . 18 |- ran abs C_ RR
185	182, 184	sstri 3427	. . . . . . . . . . . . . . . . 17 |- ran ( abs o. - ) C_ RR
186	181, 185	eqsstri 3448	. . . . . . . . . . . . . . . 16 |- ran D C_ RR
187	180, 186	sstri 3427	. . . . . . . . . . . . . . 15 |- ran ( D |` I ) C_ RR
188	34, 187	eqsstri 3448	. . . . . . . . . . . . . 14 |- R C_ RR
189	188	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> R C_ RR )
190		fiinfcl 8035	. . . . . . . . . . . . 13 |- ( ( < Or RR /\ ( R e. Fin /\ R =/= (/) /\ R C_ RR ) ) -> inf ( R , RR , < ) e. R )
191	127, 138, 177, 189, 190	syl13anc 1294	. . . . . . . . . . . 12 |- ( ph -> inf ( R , RR , < ) e. R )
192	125, 191	sseldd 3419	. . . . . . . . . . 11 |- ( ph -> inf ( R , RR , < ) e. RR+ )
193	33, 192	syl5eqel 2553	. . . . . . . . . 10 |- ( ph -> E e. RR+ )
194	193	ad2antrr 740	. . . . . . . . 9 |- ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> E e. RR+ )
195	3, 30, 32, 194	lptre2pt 37817	. . . . . . . 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 ) )
196		simpll 768	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> ph )
197	29	sselda 3418	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. H ) -> y e. RR )
198	197	adantrr 731	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. H /\ z e. H ) ) -> y e. RR )
199	198	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> y e. RR )
200	29	sselda 3418	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. H ) -> z e. RR )
201	200	adantrl 730	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( y e. H /\ z e. H ) ) -> z e. RR )
202	201	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> z e. RR )
203		simpr 468	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> y =/= z )
204	199, 202, 203	3jca 1210	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> ( y e. RR /\ z e. RR /\ y =/= z ) )
205	8	eleq2i 2541	. . . . . . . . . . . . . . . . . . 19 |- ( y e. H <-> y e. { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } )
206		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> ( x + ( k x. T ) ) = ( y + ( k x. T ) ) )
207	206	eleq1d 2533	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( ( x + ( k x. T ) ) e. A <-> ( y + ( k x. T ) ) e. A ) )
208	207	rexbidv 2892	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = y -> ( E. k e. ZZ ( x + ( k x. T ) ) e. A <-> E. k e. ZZ ( y + ( k x. T ) ) e. A ) )
209		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = j -> ( k x. T ) = ( j x. T ) )
210	209	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k = j -> ( y + ( k x. T ) ) = ( y + ( j x. T ) ) )
211	210	eleq1d 2533	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k = j -> ( ( y + ( k x. T ) ) e. A <-> ( y + ( j x. T ) ) e. A ) )
212	211	cbvrexv 3006	. . . . . . . . . . . . . . . . . . . . 21 |- ( E. k e. ZZ ( y + ( k x. T ) ) e. A <-> E. j e. ZZ ( y + ( j x. T ) ) e. A )
213	208, 212	syl6bb 269	. . . . . . . . . . . . . . . . . . . 20 |- ( x = y -> ( E. k e. ZZ ( x + ( k x. T ) ) e. A <-> E. j e. ZZ ( y + ( j x. T ) ) e. A ) )
214	213	elrab 3184	. . . . . . . . . . . . . . . . . . 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 ) )
215	205, 214	sylbb 202	. . . . . . . . . . . . . . . . . 18 |- ( y e. H -> ( y e. ( X [,] Y ) /\ E. j e. ZZ ( y + ( j x. T ) ) e. A ) )
216	215	simprd 470	. . . . . . . . . . . . . . . . 17 |- ( y e. H -> E. j e. ZZ ( y + ( j x. T ) ) e. A )
217	216	adantr 472	. . . . . . . . . . . . . . . 16 |- ( ( y e. H /\ z e. H ) -> E. j e. ZZ ( y + ( j x. T ) ) e. A )
218	8	eleq2i 2541	. . . . . . . . . . . . . . . . . . 19 |- ( z e. H <-> z e. { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } )
219		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( x + ( k x. T ) ) = ( z + ( k x. T ) ) )
220	219	eleq1d 2533	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = z -> ( ( x + ( k x. T ) ) e. A <-> ( z + ( k x. T ) ) e. A ) )
221	220	rexbidv 2892	. . . . . . . . . . . . . . . . . . . 20 |- ( x = z -> ( E. k e. ZZ ( x + ( k x. T ) ) e. A <-> E. k e. ZZ ( z + ( k x. T ) ) e. A ) )
222	221	elrab 3184	. . . . . . . . . . . . . . . . . . 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 ) )
223	218, 222	sylbb 202	. . . . . . . . . . . . . . . . . 18 |- ( z e. H -> ( z e. ( X [,] Y ) /\ E. k e. ZZ ( z + ( k x. T ) ) e. A ) )
224	223	simprd 470	. . . . . . . . . . . . . . . . 17 |- ( z e. H -> E. k e. ZZ ( z + ( k x. T ) ) e. A )
225	224	adantl 473	. . . . . . . . . . . . . . . 16 |- ( ( y e. H /\ z e. H ) -> E. k e. ZZ ( z + ( k x. T ) ) e. A )
226		reeanv 2944	. . . . . . . . . . . . . . . 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 ) )
227	217, 225, 226	sylanbrc 677	. . . . . . . . . . . . . . 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 ) )
228	227	ad2antlr 741	. . . . . . . . . . . . . 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 ) )
229		simplll 776	. . . . . . . . . . . . . . . 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 )
230		simpl1 1033	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> y e. RR )
231		simpl2 1034	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> z e. RR )
232		simpr 468	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> y < z )
233	230, 231, 232	3jca 1210	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> ( y e. RR /\ z e. RR /\ y < z ) )
234	233	adantll 728	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ y < z ) -> ( y e. RR /\ z e. RR /\ y < z ) )
235	234	adantlr 729	. . . . . . . . . . . . . . . 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 ) )
236		simplr 770	. . . . . . . . . . . . . . . 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 ) )
237		eleq1 2537	. . . . . . . . . . . . . . . . . . . . 21 |- ( b = z -> ( b e. RR <-> z e. RR ) )
238		breq2 4399	. . . . . . . . . . . . . . . . . . . . 21 |- ( b = z -> ( y < b <-> y < z ) )
239	237, 238	3anbi23d 1368	. . . . . . . . . . . . . . . . . . . 20 |- ( b = z -> ( ( y e. RR /\ b e. RR /\ y < b ) <-> ( y e. RR /\ z e. RR /\ y < z ) ) )
240	239	anbi2d 718	. . . . . . . . . . . . . . . . . . 19 |- ( b = z -> ( ( ph /\ ( y e. RR /\ b e. RR /\ y < b ) ) <-> ( ph /\ ( y e. RR /\ z e. RR /\ y < z ) ) ) )
241		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . 22 |- ( b = z -> ( b + ( k x. T ) ) = ( z + ( k x. T ) ) )
242	241	eleq1d 2533	. . . . . . . . . . . . . . . . . . . . 21 |- ( b = z -> ( ( b + ( k x. T ) ) e. A <-> ( z + ( k x. T ) ) e. A ) )
243	242	anbi2d 718	. . . . . . . . . . . . . . . . . . . 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 ) ) )
244	243	2rexbidv 2897	. . . . . . . . . . . . . . . . . . 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 ) ) )
245	240, 244	anbi12d 725	. . . . . . . . . . . . . . . . . 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 ) ) ) )
246		oveq2 6316	. . . . . . . . . . . . . . . . . . . 20 |- ( b = z -> ( y - b ) = ( y - z ) )
247	246	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 |- ( b = z -> ( abs ` ( y - b ) ) = ( abs ` ( y - z ) ) )
248	247	breq2d 4407	. . . . . . . . . . . . . . . . . 18 |- ( b = z -> ( E <_ ( abs ` ( y - b ) ) <-> E <_ ( abs ` ( y - z ) ) ) )
249	245, 248	imbi12d 327	. . . . . . . . . . . . . . . . 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 ) ) ) ) )
250		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = y -> ( a e. RR <-> y e. RR ) )
251		breq1 4398	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = y -> ( a < b <-> y < b ) )
252	250, 251	3anbi13d 1367	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = y -> ( ( a e. RR /\ b e. RR /\ a < b ) <-> ( y e. RR /\ b e. RR /\ y < b ) ) )
253	252	anbi2d 718	. . . . . . . . . . . . . . . . . . . 20 |- ( a = y -> ( ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) <-> ( ph /\ ( y e. RR /\ b e. RR /\ y < b ) ) ) )
254		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = y -> ( a + ( j x. T ) ) = ( y + ( j x. T ) ) )
255	254	eleq1d 2533	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = y -> ( ( a + ( j x. T ) ) e. A <-> ( y + ( j x. T ) ) e. A ) )
256	255	anbi1d 719	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
257	256	2rexbidv 2897	. . . . . . . . . . . . . . . . . . . 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 ) ) )
258	253, 257	anbi12d 725	. . . . . . . . . . . . . . . . . . 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 ) ) ) )
259		oveq1 6315	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = y -> ( a - b ) = ( y - b ) )
260	259	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20 |- ( a = y -> ( abs ` ( a - b ) ) = ( abs ` ( y - b ) ) )
261	260	breq2d 4407	. . . . . . . . . . . . . . . . . . 19 |- ( a = y -> ( E <_ ( abs ` ( a - b ) ) <-> E <_ ( abs ` ( y - b ) ) ) )
262	258, 261	imbi12d 327	. . . . . . . . . . . . . . . . . 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 ) ) ) ) )
263		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 ) ) )
264	263	simprbi 471	. . . . . . . . . . . . . . . . . . . 20 |- ( ps -> E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) )
265	263	biimpi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
266	265	simpld 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ps -> ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) )
267	266	simpld 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ps -> ph )
268	267, 50	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ps -> B e. RR )
269	268	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> B e. RR )
270	267, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ps -> C e. RR )
271	270	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> C e. RR )
272	267, 49	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ps -> A C_ ( B [,] C ) )
273	272	sselda 3418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ps /\ ( b + ( k x. T ) ) e. A ) -> ( b + ( k x. T ) ) e. ( B [,] C ) )
274	273	adantrl 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( b + ( k x. T ) ) e. ( B [,] C ) )
275	272	sselda 3418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> ( a + ( j x. T ) ) e. ( B [,] C ) )
276	275	adantrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) e. ( B [,] C ) )
277	269, 271, 274, 276	iccsuble 37716	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ ( C - B ) )
278		fourierdlem42.t	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- T = ( C - B )
279	277, 278	syl6breqr 4436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( 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 1049	. . . . . . . . . . . . . . . . . . . . . . . . . 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 )
281	280	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 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 )
282		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> -. k <_ j )
283		zre 10965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( j e. ZZ -> j e. RR )
284	283	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( j e. ZZ /\ k e. ZZ ) -> j e. RR )
285	284	ad2antlr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> j e. RR )
286		zre 10965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( k e. ZZ -> k e. RR )
287	286	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( j e. ZZ /\ k e. ZZ ) -> k e. RR )
288	287	ad2antlr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> k e. RR )
289	285, 288	ltnled 9799	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> ( j < k <-> -. k <_ j ) )
290	282, 289	mpbird 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> j < k )
291	51, 50	resubcld 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ph -> ( C - B ) e. RR )
292	278, 291	syl5eqel 2553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ph -> T e. RR )
293	267, 292	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ps -> T e. RR )
294	293	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T e. RR )
295	287	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> k e. RR )
296	284	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> j e. RR )
297	295, 296	resubcld 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k - j ) e. RR )
298	293	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> T e. RR )
299	297, 298	remulcld 9689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) e. RR )
300	299	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( ( k - j ) x. T ) e. RR )
301	266	simprd 470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ps -> ( a e. RR /\ b e. RR /\ a < b ) )
302	301	simp2d 1043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ps -> b e. RR )
303	302	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> b e. RR )
304	286	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ k e. ZZ ) -> k e. RR )
305	293	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ k e. ZZ ) -> T e. RR )
306	304, 305	remulcld 9689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ k e. ZZ ) -> ( k x. T ) e. RR )
307	306	adantrl 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k x. T ) e. RR )
308	303, 307	readdcld 9688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( b + ( k x. T ) ) e. RR )
309	301	simp1d 1042	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ps -> a e. RR )
310	309	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> a e. RR )
311	283	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ j e. ZZ ) -> j e. RR )
312	293	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ j e. ZZ ) -> T e. RR )
313	311, 312	remulcld 9689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ j e. ZZ ) -> ( j x. T ) e. RR )
314	313	adantrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j x. T ) e. RR )
315	310, 314	readdcld 9688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( a + ( j x. T ) ) e. RR )
316	308, 315	resubcld 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) e. RR )
317	316	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) e. RR )
318	293	recnd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ps -> T e. CC )
319	318	mulid2d 9679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ps -> ( 1 x. T ) = T )
320	319	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ps -> T = ( 1 x. T ) )
321	320	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T = ( 1 x. T ) )
322		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> j < k )
323		zltlem1 11013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( j e. ZZ /\ k e. ZZ ) -> ( j < k <-> j <_ ( k - 1 ) ) )
324	323	ad2antlr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( j < k <-> j <_ ( k - 1 ) ) )
325	322, 324	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> j <_ ( k - 1 ) )
326	284	ad2antlr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> j e. RR )
327		peano2rem 9961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( k e. RR -> ( k - 1 ) e. RR )
328	295, 327	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k - 1 ) e. RR )
329	328	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( k - 1 ) e. RR )
330		1re 9660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- 1 e. RR
331		resubcl 9958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( 1 e. RR /\ j e. RR ) -> ( 1 - j ) e. RR )
332	330, 326, 331	sylancr 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( 1 - j ) e. RR )
333		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> j <_ ( k - 1 ) )
334	326, 329, 332, 333	leadd1dd 10248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( j + ( 1 - j ) ) <_ ( ( k - 1 ) + ( 1 - j ) ) )
335		zcn 10966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( j e. ZZ -> j e. CC )
336	335	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( j e. ZZ /\ k e. ZZ ) -> j e. CC )
337		1cnd 9677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( j e. ZZ /\ k e. ZZ ) -> 1 e. CC )
338	336, 337	pncan3d 10008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( j e. ZZ /\ k e. ZZ ) -> ( j + ( 1 - j ) ) = 1 )
339	338	ad2antlr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( j + ( 1 - j ) ) = 1 )
340		zcn 10966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( k e. ZZ -> k e. CC )
341	340	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( j e. ZZ /\ k e. ZZ ) -> k e. CC )
342	341, 337, 336	npncand 10029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( j e. ZZ /\ k e. ZZ ) -> ( ( k - 1 ) + ( 1 - j ) ) = ( k - j ) )
343	342	ad2antlr 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( ( k - 1 ) + ( 1 - j ) ) = ( k - j ) )
344	334, 339, 343	3brtr3d 4425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> 1 <_ ( k - j ) )
345	325, 344	syldan 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> 1 <_ ( k - j ) )
346	330	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> 1 e. RR )
347	297	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( k - j ) e. RR )
348	50, 51	posdifd 10221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ph -> ( B < C <-> 0 < ( C - B ) ) )
349	147, 348	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ph -> 0 < ( C - B ) )
350	349, 278	syl6breqr 4436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> 0 < T )
351	292, 350	elrpd 11361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> T e. RR+ )
352	267, 351	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ps -> T e. RR+ )
353	352	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T e. RR+ )
354	346, 347, 353	lemul1d 11404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( 1 <_ ( k - j ) <-> ( 1 x. T ) <_ ( ( k - j ) x. T ) ) )
355	345, 354	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( 1 x. T ) <_ ( ( k - j ) x. T ) )
356	321, 355	eqbrtrd 4416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T <_ ( ( k - j ) x. T ) )
357	302, 309	resubcld 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ps -> ( b - a ) e. RR )
358	301	simp3d 1044	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ps -> a < b )
359	309, 302	posdifd 10221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ps -> ( a < b <-> 0 < ( b - a ) ) )
360	358, 359	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ps -> 0 < ( b - a ) )
361	357, 360	elrpd 11361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ps -> ( b - a ) e. RR+ )
362	361	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( b - a ) e. RR+ )
363	299, 362	ltaddrp2d 11395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) < ( ( b - a ) + ( ( k - j ) x. T ) ) )
364	302	recnd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ps -> b e. CC )
365	364	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> b e. CC )
366	306	recnd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ k e. ZZ ) -> ( k x. T ) e. CC )
367	366	adantrl 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k x. T ) e. CC )
368	309	recnd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ps -> a e. CC )
369	368	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> a e. CC )
370	313	recnd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ j e. ZZ ) -> ( j x. T ) e. CC )
371	370	adantrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j x. T ) e. CC )
372	365, 367, 369, 371	addsub4d 10052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( 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 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> k e. CC )
374	335	ad2antrl 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> j e. CC )
375	318	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> T e. CC )
376	373, 374, 375	subdird 10096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) = ( ( k x. T ) - ( j x. T ) ) )
377	376	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k x. T ) - ( j x. T ) ) = ( ( k - j ) x. T ) )
378	377	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( 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 2506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( 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 4420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
381	380	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( 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 9810	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
383	294, 317	ltnled 9799	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
384	382, 383	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
385	290, 384	syldan 478	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
386	385	3adantl3 1188	. . . . . . . . . . . . . . . . . . . . . . . . 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 )
387	281, 386	condan 811	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> k <_ j )
388	188, 191	sseldi 3416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> inf ( R , RR , < ) e. RR )
389	33, 388	syl5eqel 2553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> E e. RR )
390	267, 389	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ps -> E e. RR )
391	390	3ad2ant1 1051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( 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 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
393	293	3ad2ant1 1051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( 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 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
395	284, 287	resubcld 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( j e. ZZ /\ k e. ZZ ) -> ( j - k ) e. RR )
396	395	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j - k ) e. RR )
397	396, 298	remulcld 9689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( j - k ) x. T ) e. RR )
398	397	3adant3 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
399	398	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
400		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ph -> ph )
401	143, 144	jca 541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ph -> ( B e. A /\ C e. A ) )
402	400, 401, 147	3jca 1210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) )
403		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( d = C -> ( d e. A <-> C e. A ) )
404	403	anbi2d 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( d = C -> ( ( B e. A /\ d e. A ) <-> ( B e. A /\ C e. A ) ) )
405		breq2 4399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( d = C -> ( B < d <-> B < C ) )
406	404, 405	3anbi23d 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( d = C -> ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) <-> ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) ) )
407		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( d = C -> ( d - B ) = ( C - B ) )
408	407	breq2d 4407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( d = C -> ( E <_ ( d - B ) <-> E <_ ( C - B ) ) )
409	406, 408	imbi12d 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
410		simp2l 1056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> B e. A )
411		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( c = B -> ( c e. A <-> B e. A ) )
412	411	anbi1d 719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( c = B -> ( ( c e. A /\ d e. A ) <-> ( B e. A /\ d e. A ) ) )
413		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( c = B -> ( c < d <-> B < d ) )
414	412, 413	3anbi23d 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( c = B -> ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) <-> ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) ) )
415		oveq2 6316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( c = B -> ( d - c ) = ( d - B ) )
416	415	breq2d 4407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( c = B -> ( E <_ ( d - c ) <-> E <_ ( d - B ) ) )
417	414, 416	imbi12d 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
418	188	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> R C_ RR )
419		0re 9661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- 0 e. RR
420	34	eleq2i 2541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( y e. R <-> y e. ran ( D |` I ) )
421	420	biimpi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( y e. R -> y e. ran ( D |` I ) )
422	421	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ y e. R ) -> y e. ran ( D |` I ) )
423	61	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ y e. R ) -> ( D |` I ) Fn I )
424		fvelrnb 5926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( D |` I ) Fn I -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) )
425	423, 424	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ y e. R ) -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) )
426	422, 425	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ y e. R ) -> E. x e. I ( ( D |` I ) ` x ) = y )
427	121	rpge0d 11368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ x e. I ) -> 0 <_ ( ( D |` I ) ` x ) )
428	427	3adant3 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> 0 <_ ( ( D |` I ) ` x ) )
429		simp3 1032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> ( ( D |` I ) ` x ) = y )
430	428, 429	breqtrd 4420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> 0 <_ y )
431	430	3exp 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ph -> ( x e. I -> ( ( ( D |` I ) ` x ) = y -> 0 <_ y ) ) )
432	431	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ y e. R ) -> ( x e. I -> ( ( ( D |` I ) ` x ) = y -> 0 <_ y ) ) )
433	432	rexlimdv 2870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ y e. R ) -> ( E. x e. I ( ( D |` I ) ` x ) = y -> 0 <_ y ) )
434	426, 433	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ y e. R ) -> 0 <_ y )
435	434	ralrimiva 2809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ph -> A. y e. R 0 <_ y )
436		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( x = 0 -> ( x <_ y <-> 0 <_ y ) )
437	436	ralbidv 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( x = 0 -> ( A. y e. R x <_ y <-> A. y e. R 0 <_ y ) )
438	437	rspcev 3136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( 0 e. RR /\ A. y e. R 0 <_ y ) -> E. x e. RR A. y e. R x <_ y )
439	419, 435, 438	sylancr 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ph -> E. x e. RR A. y e. R x <_ y )
440	439	3ad2ant1 1051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E. x e. RR A. y e. R x <_ y )
441		pm3.22 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( c e. A /\ d e. A ) -> ( d e. A /\ c e. A ) )
442		opelxp 4869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( <. d , c >. e. ( A X. A ) <-> ( d e. A /\ c e. A ) )
443	441, 442	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( c e. A /\ d e. A ) -> <. d , c >. e. ( A X. A ) )
444	443	3ad2ant2 1052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. ( A X. A ) )
445	49, 52	sstrd 3428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( ph -> A C_ RR )
446	445	sselda 3418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ph /\ c e. A ) -> c e. RR )
447	446	adantrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ ( c e. A /\ d e. A ) ) -> c e. RR )
448	447	3adant3 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c e. RR )
449		simp3 1032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c < d )
450	448, 449	gtned 9787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> d =/= c )
451	450	neneqd 2648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> -. d = c )
452		df-br 4396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( d _I c <-> <. d , c >. e. _I )
453		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- c e. _V
454	453	ideq 4992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( d _I c <-> d = c )
455	452, 454	bitr3i 259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( <. d , c >. e. _I <-> d = c )
456	451, 455	sylnibr 312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> -. <. d , c >. e. _I )
457	444, 456	eldifd 3401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. ( ( A X. A ) \ _I ) )
458	457, 48	syl6eleqr 2560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. I )
459	448, 449	ltned 9788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c =/= d )
460	141	3ad2ant1 1051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( D |` I ) = ( ( abs o. - ) |` I ) )
461	460	fveq1d 5881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( D |` I ) ` <. d , c >. ) = ( ( ( abs o. - ) |` I ) ` <. d , c >. ) )
462	443	3ad2ant2 1052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. ( A X. A ) )
463		necom 2696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ( c =/= d <-> d =/= c )
464	463	biimpi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ( c =/= d -> d =/= c )
465	464	neneqd 2648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( c =/= d -> -. d = c )
466	465	3ad2ant3 1053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> -. d = c )
467	466, 455	sylnibr 312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> -. <. d , c >. e. _I )
468	462, 467	eldifd 3401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. ( ( A X. A ) \ _I ) )
469	468, 48	syl6eleqr 2560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. I )
470		fvres 5893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( <. d , c >. e. I -> ( ( ( abs o. - ) |` I ) ` <. d , c >. ) = ( ( abs o. - ) ` <. d , c >. ) )
471	469, 470	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( ( abs o. - ) |` I ) ` <. d , c >. ) = ( ( abs o. - ) ` <. d , c >. ) )
472		simp1 1030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ph )
473	472, 469	jca 541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ph /\ <. d , c >. e. I ) )
474		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ( x = <. d , c >. -> ( x e. I <-> <. d , c >. e. I ) )
475	474	anbi2d 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( x = <. d , c >. -> ( ( ph /\ x e. I ) <-> ( ph /\ <. d , c >. e. I ) ) )
476		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( x = <. d , c >. -> ( x e. dom - <-> <. d , c >. e. dom - ) )
477	475, 476	imbi12d 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( x = <. d , c >. -> ( ( ( ph /\ x e. I ) -> x e. dom - ) <-> ( ( ph /\ <. d , c >. e. I ) -> <. d , c >. e. dom - ) ) )
478	477, 70	vtoclg 3093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( <. d , c >. e. I -> ( ( ph /\ <. d , c >. e. I ) -> <. d , c >. e. dom - ) )
479	469, 473, 478	sylc 61	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. dom - )
480		fvco 5956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( Fun - /\ <. d , c >. e. dom - ) -> ( ( abs o. - ) ` <. d , c >. ) = ( abs ` ( - ` <. d , c >. ) ) )
481	67, 479, 480	sylancr 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( abs o. - ) ` <. d , c >. ) = ( abs ` ( - ` <. d , c >. ) ) )
482		df-ov 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( d - c ) = ( - ` <. d , c >. )
483	482	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( - ` <. d , c >. ) = ( d - c )
484	483	fveq2i 5882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( abs ` ( - ` <. d , c >. ) ) = ( abs ` ( d - c ) )
485	481, 484	syl6eq 2521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( abs o. - ) ` <. d , c >. ) = ( abs ` ( d - c ) ) )
486	461, 471, 485	3eqtrd 2509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( D |` I ) ` <. d , c >. ) = ( abs ` ( d - c ) ) )
487	459, 486	syld3an3 1337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( ( D |` I ) ` <. d , c >. ) = ( abs ` ( d - c ) ) )
488	445	sselda 3418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ d e. A ) -> d e. RR )
489	488	adantrl 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ ( c e. A /\ d e. A ) ) -> d e. RR )
490	489	3adant3 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> d e. RR )
491	448, 490, 449	ltled 9800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c <_ d )
492	448, 490, 491	abssubge0d 13570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( abs ` ( d - c ) ) = ( d - c ) )
493	487, 492	eqtrd 2505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( ( D |` I ) ` <. d , c >. ) = ( d - c ) )
494		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( x = <. d , c >. -> ( ( D |` I ) ` x ) = ( ( D |` I ) ` <. d , c >. ) )
495	494	eqeq1d 2473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( x = <. d , c >. -> ( ( ( D |` I ) ` x ) = ( d - c ) <-> ( ( D |` I ) ` <. d , c >. ) = ( d - c ) ) )
496	495	rspcev 3136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( <. d , c >. e. I /\ ( ( D |` I ) ` <. d , c >. ) = ( d - c ) ) -> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) )
497	458, 493, 496	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) )
498	489, 447	resubcld 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) ) -> ( d - c ) e. RR )
499		elex 3040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( d - c ) e. RR -> ( d - c ) e. _V )
500	498, 499	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ph /\ ( c e. A /\ d e. A ) ) -> ( d - c ) e. _V )
501	500	3adant3 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( d - c ) e. _V )
502		simp1 1030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ph )
503		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( y = ( d - c ) -> ( y e. ran ( D |` I ) <-> ( d - c ) e. ran ( D |` I ) ) )
504		eqeq2 2482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( y = ( d - c ) -> ( ( ( D |` I ) ` x ) = y <-> ( ( D |` I ) ` x ) = ( d - c ) ) )
505	504	rexbidv 2892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( y = ( d - c ) -> ( E. x e. I ( ( D |` I ) ` x ) = y <-> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) ) )
506	503, 505	bibi12d 328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
507	506	imbi2d 323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
508	61, 424	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ph -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) )
509	507, 508	vtoclg 3093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( d - c ) e. _V -> ( ph -> ( ( d - c ) e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = ( d - c ) ) ) )
510	501, 502, 509	sylc 61	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
511	497, 510	mpbird 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( d - c ) e. ran ( D |` I ) )
512	511, 34	syl6eleqr 2560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( d - c ) e. R )
513		infrelb 10618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( R C_ RR /\ E. x e. RR A. y e. R x <_ y /\ ( d - c ) e. R ) -> inf ( R , RR , < ) <_ ( d - c ) )
514	418, 440, 512, 513	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> inf ( R , RR , < ) <_ ( d - c ) )
515	33, 514	syl5eqbr 4429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E <_ ( d - c ) )
516	417, 515	vtoclg 3093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( B e. A -> ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> E <_ ( d - B ) ) )
517	410, 516	mpcom 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> E <_ ( d - B ) )
518	409, 517	vtoclg 3093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( C e. A -> ( ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) -> E <_ ( C - B ) ) )
519	144, 402, 518	sylc 61	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> E <_ ( C - B ) )
520	519, 278	syl6breqr 4436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> E <_ T )
521	267, 520	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ps -> E <_ T )
522	521	3ad2ant1 1051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E <_ T )
523	522	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
524	364	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ps /\ k e. ZZ ) -> b e. CC )
525	524, 366	pncan2d 10007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ps /\ k e. ZZ ) -> ( ( b + ( k x. T ) ) - b ) = ( k x. T ) )
526	525	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ps /\ k e. ZZ ) -> ( ( ( b + ( k x. T ) ) - b ) / T ) = ( ( k x. T ) / T ) )
527	340	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ps /\ k e. ZZ ) -> k e. CC )
528	318	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ps /\ k e. ZZ ) -> T e. CC )
529	419	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ph -> 0 e. RR )
530	529, 350	gtned 9787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ph -> T =/= 0 )
531	267, 530	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ps -> T =/= 0 )
532	531	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ps /\ k e. ZZ ) -> T =/= 0 )
533	527, 528, 532	divcan4d 10411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ps /\ k e. ZZ ) -> ( ( k x. T ) / T ) = k )
534	526, 533	eqtr2d 2506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ps /\ k e. ZZ ) -> k = ( ( ( b + ( k x. T ) ) - b ) / T ) )
535	534	adantrl 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> k = ( ( ( b + ( k x. T ) ) - b ) / T ) )
536	535	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a + ( j x. T ) ) = ( b + ( k x. T ) ) ) -> k = ( ( ( b + ( k x. T ) ) - b ) / T ) )
537		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( a + ( j x. T ) ) = ( b + ( k x. T ) ) -> ( ( a + ( j x. T ) ) - b ) = ( ( b + ( k x. T ) ) - b ) )
538	537	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( a + ( j x. T ) ) = ( b + ( k x. T ) ) -> ( ( ( a + ( j x. T ) ) - b ) / T ) = ( ( ( b + ( k x. T ) ) - b ) / T ) )
539	538	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ ( a