Theorem fourierdlem42 31772

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 21198	. . . . 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 3590	. . . . . . 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 3553	. . . . 5 |- ( ph -> H C_ ( X [,] Y ) )
12		retop 21136	. . . . . . . . . 10 |- ( topGen ` ran (,) ) e. Top
13	3, 12	eqeltri 2551	. . . . . . . . 9 |- J e. Top
14	13	a1i 11	. . . . . . . 8 |- ( ph -> J e. Top )
15	1, 2	iccssred 31426	. . . . . . . 8 |- ( ph -> ( X [,] Y ) C_ RR )
16		uniretop 21137	. . . . . . . . . 10 |- RR = U. ( topGen ` ran (,) )
17	3	unieqi 4260	. . . . . . . . . . 11 |- U. J = U. ( topGen ` ran (,) )
18	17	eqcomi 2480	. . . . . . . . . 10 |- U. ( topGen ` ran (,) ) = U. J
19	16, 18	eqtri 2496	. . . . . . . . 9 |- RR = U. J
20	19	restuni 19531	. . . . . . . 8 |- ( ( J e. Top /\ ( X [,] Y ) C_ RR ) -> ( X [,] Y ) = U. ( J ↾t ( X [,] Y ) ) )
21	14, 15, 20	syl2anc 661	. . . . . . 7 |- ( ph -> ( X [,] Y ) = U. ( J ↾t ( X [,] Y ) ) )
22	4	unieqi 4260	. . . . . . . . 9 |- U. K = U. ( J ↾t ( X [,] Y ) )
23	22	eqcomi 2480	. . . . . . . 8 |- U. ( J ↾t ( X [,] Y ) ) = U. K
24	23	a1i 11	. . . . . . 7 |- ( ph -> U. ( J ↾t ( X [,] Y ) ) = U. K )
25	21, 24	eqtrd 2508	. . . . . 6 |- ( ph -> ( X [,] Y ) = U. K )
26		eqid 2467	. . . . . . 7 |- U. K = U. K
27	26	a1i 11	. . . . . 6 |- ( ph -> U. K = U. K )
28	25, 27	eqtrd 2508	. . . . 5 |- ( ph -> ( X [,] Y ) = U. K )
29	11, 28	sseqtrd 3545	. . . 4 |- ( ph -> H C_ U. K )
30	29	adantr 465	. . 3 |- ( ( ph /\ -. H e. Fin ) -> H C_ U. K )
31		simpr 461	. . 3 |- ( ( ph /\ -. H e. Fin ) -> -. H e. Fin )
32	26	bwth 19778	. . 3 |- ( ( K e. Comp /\ H C_ U. K /\ -. H e. Fin ) -> E. x e. U. K x e. ( ( limPt ` K ) ` H ) )
33	7, 30, 31, 32	syl3anc 1228	. 2 |- ( ( ph /\ -. H e. Fin ) -> E. x e. U. K x e. ( ( limPt ` K ) ` H ) )
34	11, 15	sstrd 3519	. . . . . . . . . . . 12 |- ( ph -> H C_ RR )
35	34	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ x e. U. K ) -> H C_ RR )
36	35	adantr 465	. . . . . . . . . 10 |- ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> H C_ RR )
37		ne0i 3796	. . . . . . . . . . 11 |- ( x e. ( ( limPt ` J ) ` H ) -> ( ( limPt ` J ) ` H ) =/= (/) )
38	37	adantl 466	. . . . . . . . . 10 |- ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> ( ( limPt ` J ) ` H ) =/= (/) )
39		fourierdlem42.e	. . . . . . . . . . . . 13 |- E = sup ( R , RR , `' < )
40		fourierdlem42.r	. . . . . . . . . . . . . . 15 |- R = ran ( D |` I )
41		absf 13150	. . . . . . . . . . . . . . . . . . . . 21 |- abs : CC --> RR
42		ffn 5737	. . . . . . . . . . . . . . . . . . . . 21 |- ( abs : CC --> RR -> abs Fn CC )
43	41, 42	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- abs Fn CC
44		subf 9834	. . . . . . . . . . . . . . . . . . . . 21 |- - : ( CC X. CC ) --> CC
45		ffn 5737	. . . . . . . . . . . . . . . . . . . . 21 |- ( - : ( CC X. CC ) --> CC -> - Fn ( CC X. CC ) )
46	44, 45	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- - Fn ( CC X. CC )
47		frn 5743	. . . . . . . . . . . . . . . . . . . . 21 |- ( - : ( CC X. CC ) --> CC -> ran - C_ CC )
48	44, 47	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- ran - C_ CC
49		fnco 5695	. . . . . . . . . . . . . . . . . . . 20 |- ( ( abs Fn CC /\ - Fn ( CC X. CC ) /\ ran - C_ CC ) -> ( abs o. - ) Fn ( CC X. CC ) )
50	43, 46, 48, 49	mp3an 1324	. . . . . . . . . . . . . . . . . . 19 |- ( abs o. - ) Fn ( CC X. CC )
51		fourierdlem42.d	. . . . . . . . . . . . . . . . . . . 20 |- D = ( abs o. - )
52	51	fneq1i 5681	. . . . . . . . . . . . . . . . . . 19 |- ( D Fn ( CC X. CC ) <-> ( abs o. - ) Fn ( CC X. CC ) )
53	50, 52	mpbir 209	. . . . . . . . . . . . . . . . . 18 |- D Fn ( CC X. CC )
54	53	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> D Fn ( CC X. CC ) )
55		fourierdlem42.i	. . . . . . . . . . . . . . . . . 18 |- I = ( ( A X. A ) \ _I )
56		fourierdlem42.a	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> A C_ ( B [,] C ) )
57		fourierdlem42.b	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> B e. RR )
58		fourierdlem42.c	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> C e. RR )
59	57, 58	iccssred 31426	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( B [,] C ) C_ RR )
60		ax-resscn 9561	. . . . . . . . . . . . . . . . . . . . . . 23 |- RR C_ CC
61	60	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> RR C_ CC )
62	59, 61	sstrd 3519	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( B [,] C ) C_ CC )
63	56, 62	sstrd 3519	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> A C_ CC )
64		xpss12 5114	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A C_ CC /\ A C_ CC ) -> ( A X. A ) C_ ( CC X. CC ) )
65	63, 63, 64	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( A X. A ) C_ ( CC X. CC ) )
66		ssdifss 3640	. . . . . . . . . . . . . . . . . . 19 |- ( ( A X. A ) C_ ( CC X. CC ) -> ( ( A X. A ) \ _I ) C_ ( CC X. CC ) )
67	65, 66	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( A X. A ) \ _I ) C_ ( CC X. CC ) )
68	55, 67	syl5eqss 3553	. . . . . . . . . . . . . . . . 17 |- ( ph -> I C_ ( CC X. CC ) )
69		fnssres 5700	. . . . . . . . . . . . . . . . 17 |- ( ( D Fn ( CC X. CC ) /\ I C_ ( CC X. CC ) ) -> ( D |` I ) Fn I )
70	54, 68, 69	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ph -> ( D |` I ) Fn I )
71		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. I ) -> x e. I )
72		fvres 5886	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. I -> ( ( D |` I ) ` x ) = ( D ` x ) )
73	71, 72	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) = ( D ` x ) )
74	51	fveq1i 5873	. . . . . . . . . . . . . . . . . . . . . 22 |- ( D ` x ) = ( ( abs o. - ) ` x )
75	74	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. I ) -> ( D ` x ) = ( ( abs o. - ) ` x ) )
76		ffun 5739	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( - : ( CC X. CC ) --> CC -> Fun - )
77	44, 76	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 |- Fun -
78	77	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. I ) -> Fun - )
79	68	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ x e. I ) -> I C_ ( CC X. CC ) )
80	79, 71	sseldd 3510	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. I ) -> x e. ( CC X. CC ) )
81	44	fdmi 5742	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- dom - = ( CC X. CC )
82	81	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( CC X. CC ) = dom -
83	82	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. I ) -> ( CC X. CC ) = dom - )
84	80, 83	eleqtrd 2557	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. I ) -> x e. dom - )
85		fvco 5950	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( Fun - /\ x e. dom - ) -> ( ( abs o. - ) ` x ) = ( abs ` ( - ` x ) ) )
86	78, 84, 85	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. I ) -> ( ( abs o. - ) ` x ) = ( abs ` ( - ` x ) ) )
87	73, 75, 86	3eqtrd 2512	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) = ( abs ` ( - ` x ) ) )
88	41	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. I ) -> abs : CC --> RR )
89	44	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. I ) -> - : ( CC X. CC ) --> CC )
90	89, 80	ffvelrnd 6033	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. I ) -> ( - ` x ) e. CC )
91	88, 90	ffvelrnd 6033	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. I ) -> ( abs ` ( - ` x ) ) e. RR )
92	87, 91	eqeltrd 2555	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) e. RR )
93		elxp2 5023	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. ( CC X. CC ) <-> E. y e. CC E. z e. CC x = <. y , z >. )
94	80, 93	sylib 196	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. I ) -> E. y e. CC E. z e. CC x = <. y , z >. )
95		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x = <. y , z >. -> ( - ` x ) = ( - ` <. y , z >. ) )
96	95	3ad2ant3 1019	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( - ` x ) = ( - ` <. y , z >. ) )
97		df-ov 6298	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y - z ) = ( - ` <. y , z >. )
98		simp1l 1020	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ph )
99		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( x e. I /\ x = <. y , z >. ) -> x = <. y , z >. )
100	99	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( x e. I /\ x = <. y , z >. ) -> <. y , z >. = x )
101		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( x e. I /\ x = <. y , z >. ) -> x e. I )
102	100, 101	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( x e. I /\ x = <. y , z >. ) -> <. y , z >. e. I )
103	102	adantll 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ x e. I ) /\ x = <. y , z >. ) -> <. y , z >. e. I )
104	103	3adant2 1015	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> <. y , z >. e. I )
105	63	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ <. y , z >. e. I ) -> A C_ CC )
106	55	eleq2i 2545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( <. y , z >. e. I <-> <. y , z >. e. ( ( A X. A ) \ _I ) )
107	106	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( <. y , z >. e. I -> <. y , z >. e. ( ( A X. A ) \ _I ) )
108		eldif 3491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( <. y , z >. e. ( ( A X. A ) \ _I ) <-> ( <. y , z >. e. ( A X. A ) /\ -. <. y , z >. e. _I ) )
109	107, 108	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( <. y , z >. e. I -> ( <. y , z >. e. ( A X. A ) /\ -. <. y , z >. e. _I ) )
110	109	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( <. y , z >. e. I -> <. y , z >. e. ( A X. A ) )
111		opelxp 5035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( <. y , z >. e. ( A X. A ) <-> ( y e. A /\ z e. A ) )
112	110, 111	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( <. y , z >. e. I -> ( y e. A /\ z e. A ) )
113	112	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ <. y , z >. e. I ) -> ( y e. A /\ z e. A ) )
114	113	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ <. y , z >. e. I ) -> y e. A )
115	105, 114	sseldd 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ <. y , z >. e. I ) -> y e. CC )
116	113	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ <. y , z >. e. I ) -> z e. A )
117	105, 116	sseldd 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ <. y , z >. e. I ) -> z e. CC )
118	109	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( <. y , z >. e. I -> -. <. y , z >. e. _I )
119		df-br 4454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( y _I z <-> <. y , z >. e. _I )
120	118, 119	sylnibr 305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( <. y , z >. e. I -> -. y _I z )
121		vex 3121	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- z e. _V
122		ideqg 5160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( z e. _V -> ( y _I z <-> y = z ) )
123	121, 122	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( y _I z <-> y = z )
124	120, 123	sylnib 304	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( <. y , z >. e. I -> -. y = z )
125	124	neqned 2670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( <. y , z >. e. I -> y =/= z )
126	125	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ <. y , z >. e. I ) -> y =/= z )
127	115, 117, 126	subne0d 9951	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ <. y , z >. e. I ) -> ( y - z ) =/= 0 )
128	98, 104, 127	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( y - z ) =/= 0 )
129	97, 128	syl5eqner 2768	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( - ` <. y , z >. ) =/= 0 )
130	96, 129	eqnetrd 2760	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. I ) /\ ( y e. CC /\ z e. CC ) /\ x = <. y , z >. ) -> ( - ` x ) =/= 0 )
131	130	3exp 1195	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. I ) -> ( ( y e. CC /\ z e. CC ) -> ( x = <. y , z >. -> ( - ` x ) =/= 0 ) ) )
132	131	rexlimdvv 2965	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. I ) -> ( E. y e. CC E. z e. CC x = <. y , z >. -> ( - ` x ) =/= 0 ) )
133	94, 132	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. I ) -> ( - ` x ) =/= 0 )
134		absgt0 13137	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( - ` x ) e. CC -> ( ( - ` x ) =/= 0 <-> 0 < ( abs ` ( - ` x ) ) ) )
135	90, 134	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. I ) -> ( ( - ` x ) =/= 0 <-> 0 < ( abs ` ( - ` x ) ) ) )
136	133, 135	mpbid 210	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. I ) -> 0 < ( abs ` ( - ` x ) ) )
137	87	eqcomd 2475	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. I ) -> ( abs ` ( - ` x ) ) = ( ( D |` I ) ` x ) )
138	136, 137	breqtrd 4477	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. I ) -> 0 < ( ( D |` I ) ` x ) )
139	92, 138	jca 532	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. I ) -> ( ( ( D |` I ) ` x ) e. RR /\ 0 < ( ( D |` I ) ` x ) ) )
140		elrp 11234	. . . . . . . . . . . . . . . . . 18 |- ( ( ( D |` I ) ` x ) e. RR+ <-> ( ( ( D |` I ) ` x ) e. RR /\ 0 < ( ( D |` I ) ` x ) ) )
141	139, 140	sylibr 212	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. I ) -> ( ( D |` I ) ` x ) e. RR+ )
142	141	ralrimiva 2881	. . . . . . . . . . . . . . . 16 |- ( ph -> A. x e. I ( ( D |` I ) ` x ) e. RR+ )
143		fnfvrnss 6060	. . . . . . . . . . . . . . . 16 |- ( ( ( D |` I ) Fn I /\ A. x e. I ( ( D |` I ) ` x ) e. RR+ ) -> ran ( D |` I ) C_ RR+ )
144	70, 142, 143	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ph -> ran ( D |` I ) C_ RR+ )
145	40, 144	syl5eqss 3553	. . . . . . . . . . . . . 14 |- ( ph -> R C_ RR+ )
146		ltso 9677	. . . . . . . . . . . . . . . . 17 |- < Or RR
147	146	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> < Or RR )
148		cnvso 5552	. . . . . . . . . . . . . . . 16 |- ( < Or RR <-> `' < Or RR )
149	147, 148	sylib 196	. . . . . . . . . . . . . . 15 |- ( ph -> `' < Or RR )
150		fneq1 5675	. . . . . . . . . . . . . . . . . . . . . 22 |- ( D = ( abs o. - ) -> ( D Fn ( CC X. CC ) <-> ( abs o. - ) Fn ( CC X. CC ) ) )
151	51, 150	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 |- ( D Fn ( CC X. CC ) <-> ( abs o. - ) Fn ( CC X. CC ) )
152	50, 151	mpbir 209	. . . . . . . . . . . . . . . . . . . 20 |- D Fn ( CC X. CC )
153	152	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> D Fn ( CC X. CC ) )
154	153, 68, 69	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( D |` I ) Fn I )
155		fourierdlem42.af	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> A e. Fin )
156		xpfi 7803	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. Fin /\ A e. Fin ) -> ( A X. A ) e. Fin )
157	155, 155, 156	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( A X. A ) e. Fin )
158		diffi 7763	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A X. A ) e. Fin -> ( ( A X. A ) \ _I ) e. Fin )
159	157, 158	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( A X. A ) \ _I ) e. Fin )
160	55, 159	syl5eqel 2559	. . . . . . . . . . . . . . . . . 18 |- ( ph -> I e. Fin )
161		fnfi 7810	. . . . . . . . . . . . . . . . . 18 |- ( ( ( D |` I ) Fn I /\ I e. Fin ) -> ( D |` I ) e. Fin )
162	154, 160, 161	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( D |` I ) e. Fin )
163		rnfi 7817	. . . . . . . . . . . . . . . . 17 |- ( ( D |` I ) e. Fin -> ran ( D |` I ) e. Fin )
164	162, 163	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ran ( D |` I ) e. Fin )
165	40, 164	syl5eqel 2559	. . . . . . . . . . . . . . 15 |- ( ph -> R e. Fin )
166	40	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> R = ran ( D |` I ) )
167	51	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> D = ( abs o. - ) )
168	167	reseq1d 5278	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( D |` I ) = ( ( abs o. - ) |` I ) )
169	168	fveq1d 5874	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( D |` I ) ` <. B , C >. ) = ( ( ( abs o. - ) |` I ) ` <. B , C >. ) )
170		fourierdlem42.ba	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> B e. A )
171		fourierdlem42.ca	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> C e. A )
172	170, 171	jca 532	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( B e. A /\ C e. A ) )
173		opelxp 5035	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( <. B , C >. e. ( A X. A ) <-> ( B e. A /\ C e. A ) )
174	172, 173	sylibr 212	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> <. B , C >. e. ( A X. A ) )
175		fourierdlem42.bc	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> B < C )
176	57, 175	ltned 9732	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> B =/= C )
177	176	neneqd 2669	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> -. B = C )
178		ideqg 5160	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( C e. A -> ( B _I C <-> B = C ) )
179	171, 178	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( B _I C <-> B = C ) )
180	177, 179	mtbird 301	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> -. B _I C )
181		df-br 4454	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( B _I C <-> <. B , C >. e. _I )
182	180, 181	sylnib 304	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> -. <. B , C >. e. _I )
183	174, 182	eldifd 3492	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> <. B , C >. e. ( ( A X. A ) \ _I ) )
184	183, 55	syl6eleqr 2566	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> <. B , C >. e. I )
185		fvres 5886	. . . . . . . . . . . . . . . . . . . 20 |- ( <. B , C >. e. I -> ( ( ( abs o. - ) |` I ) ` <. B , C >. ) = ( ( abs o. - ) ` <. B , C >. ) )
186	184, 185	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( ( abs o. - ) |` I ) ` <. B , C >. ) = ( ( abs o. - ) ` <. B , C >. ) )
187	77	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> Fun - )
188	63, 170	sseldd 3510	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> B e. CC )
189	63, 171	sseldd 3510	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> C e. CC )
190	188, 189	jca 532	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( B e. CC /\ C e. CC ) )
191		opelxp 5035	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( <. B , C >. e. ( CC X. CC ) <-> ( B e. CC /\ C e. CC ) )
192	190, 191	sylibr 212	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> <. B , C >. e. ( CC X. CC ) )
193	192, 81	syl6eleqr 2566	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> <. B , C >. e. dom - )
194		fvco 5950	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( Fun - /\ <. B , C >. e. dom - ) -> ( ( abs o. - ) ` <. B , C >. ) = ( abs ` ( - ` <. B , C >. ) ) )
195	187, 193, 194	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( abs o. - ) ` <. B , C >. ) = ( abs ` ( - ` <. B , C >. ) ) )
196		df-ov 6298	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( B - C ) = ( - ` <. B , C >. )
197	196	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . 22 |- ( - ` <. B , C >. ) = ( B - C )
198	197	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( - ` <. B , C >. ) = ( B - C ) )
199	198	fveq2d 5876	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( abs ` ( - ` <. B , C >. ) ) = ( abs ` ( B - C ) ) )
200	195, 199	eqtrd 2508	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( abs o. - ) ` <. B , C >. ) = ( abs ` ( B - C ) ) )
201	169, 186, 200	3eqtrrd 2513	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( abs ` ( B - C ) ) = ( ( D |` I ) ` <. B , C >. ) )
202		fnfvelrn 6029	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( D |` I ) Fn I /\ <. B , C >. e. I ) -> ( ( D |` I ) ` <. B , C >. ) e. ran ( D |` I ) )
203	154, 184, 202	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( D |` I ) ` <. B , C >. ) e. ran ( D |` I ) )
204	201, 203	eqeltrd 2555	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( abs ` ( B - C ) ) e. ran ( D |` I ) )
205		ne0i 3796	. . . . . . . . . . . . . . . . 17 |- ( ( abs ` ( B - C ) ) e. ran ( D |` I ) -> ran ( D |` I ) =/= (/) )
206	204, 205	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ran ( D |` I ) =/= (/) )
207	166, 206	eqnetrd 2760	. . . . . . . . . . . . . . 15 |- ( ph -> R =/= (/) )
208		resss 5303	. . . . . . . . . . . . . . . . . . 19 |- ( D |` I ) C_ D
209		rnss 5237	. . . . . . . . . . . . . . . . . . 19 |- ( ( D |` I ) C_ D -> ran ( D |` I ) C_ ran D )
210	208, 209	ax-mp 5	. . . . . . . . . . . . . . . . . 18 |- ran ( D |` I ) C_ ran D
211	51	rneqi 5235	. . . . . . . . . . . . . . . . . . 19 |- ran D = ran ( abs o. - )
212		rncoss 5269	. . . . . . . . . . . . . . . . . . . 20 |- ran ( abs o. - ) C_ ran abs
213		frn 5743	. . . . . . . . . . . . . . . . . . . . 21 |- ( abs : CC --> RR -> ran abs C_ RR )
214	41, 213	mp1i 12	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( abs : CC --> RR -> ran abs C_ RR ) -> ran abs C_ RR )
215	213, 214	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- ran abs C_ RR
216	212, 215	sstri 3518	. . . . . . . . . . . . . . . . . . 19 |- ran ( abs o. - ) C_ RR
217	211, 216	eqsstri 3539	. . . . . . . . . . . . . . . . . 18 |- ran D C_ RR
218	210, 217	sstri 3518	. . . . . . . . . . . . . . . . 17 |- ran ( D |` I ) C_ RR
219	40, 218	eqsstri 3539	. . . . . . . . . . . . . . . 16 |- R C_ RR
220	219	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> R C_ RR )
221		fisupcl 7939	. . . . . . . . . . . . . . 15 |- ( ( `' < Or RR /\ ( R e. Fin /\ R =/= (/) /\ R C_ RR ) ) -> sup ( R , RR , `' < ) e. R )
222	149, 165, 207, 220, 221	syl13anc 1230	. . . . . . . . . . . . . 14 |- ( ph -> sup ( R , RR , `' < ) e. R )
223	145, 222	sseldd 3510	. . . . . . . . . . . . 13 |- ( ph -> sup ( R , RR , `' < ) e. RR+ )
224	39, 223	syl5eqel 2559	. . . . . . . . . . . 12 |- ( ph -> E e. RR+ )
225	224	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ x e. U. K ) -> E e. RR+ )
226	225	adantr 465	. . . . . . . . . 10 |- ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> E e. RR+ )
227	3, 36, 38, 226	lptre2pt 31505	. . . . . . . . 9 |- ( ( ( ph /\ x e. U. K ) /\ x e. ( ( limPt ` J ) ` H ) ) -> E. y e. H E. z e. H ( y =/= z /\ ( abs ` ( y - z ) ) < E ) )
228		id 22	. . . . . . . . . . . . . . . . 17 |- ( ph -> ph )
229	228	ad2antrr 725	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> ph )
230	34	sselda 3509	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. H ) -> y e. RR )
231	230	adantrr 716	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. H /\ z e. H ) ) -> y e. RR )
232	231	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> y e. RR )
233	34	sselda 3509	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. H ) -> z e. RR )
234	233	adantrl 715	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( y e. H /\ z e. H ) ) -> z e. RR )
235	234	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> z e. RR )
236		simpr 461	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> y =/= z )
237	232, 235, 236	3jca 1176	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> ( y e. RR /\ z e. RR /\ y =/= z ) )
238	229, 237	jca 532	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( y e. H /\ z e. H ) ) /\ y =/= z ) -> ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) )
239	8	eleq2i 2545	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. H <-> y e. { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } )
240	239	biimpi 194	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. H -> y e. { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } )
241		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = y -> ( x + ( k x. T ) ) = ( y + ( k x. T ) ) )
242	241	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = y -> ( ( x + ( k x. T ) ) e. A <-> ( y + ( k x. T ) ) e. A ) )
243	242	rexbidv 2978	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> ( E. k e. ZZ ( x + ( k x. T ) ) e. A <-> E. k e. ZZ ( y + ( k x. T ) ) e. A ) )
244		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = j -> ( k x. T ) = ( j x. T ) )
245	244	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = j -> ( y + ( k x. T ) ) = ( y + ( j x. T ) ) )
246	245	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = j -> ( ( y + ( k x. T ) ) e. A <-> ( y + ( j x. T ) ) e. A ) )
247	246	cbvrexv 3094	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( E. k e. ZZ ( y + ( k x. T ) ) e. A <-> E. j e. ZZ ( y + ( j x. T ) ) e. A )
248	243, 247	syl6bb 261	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( E. k e. ZZ ( x + ( k x. T ) ) e. A <-> E. j e. ZZ ( y + ( j x. T ) ) e. A ) )
249	248	elrab 3266	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) )
250	240, 249	sylib 196	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. H -> ( y e. ( X [,] Y ) /\ E. j e. ZZ ( y + ( j x. T ) ) e. A ) )
251	250	simprd 463	. . . . . . . . . . . . . . . . . . 19 |- ( y e. H -> E. j e. ZZ ( y + ( j x. T ) ) e. A )
252	251	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. H /\ z e. H ) -> E. j e. ZZ ( y + ( j x. T ) ) e. A )
253	8	eleq2i 2545	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z e. H <-> z e. { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } )
254	253	biimpi 194	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. H -> z e. { x e. ( X [,] Y ) | E. k e. ZZ ( x + ( k x. T ) ) e. A } )
255		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = z -> ( x + ( k x. T ) ) = ( z + ( k x. T ) ) )
256	255	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = z -> ( ( x + ( k x. T ) ) e. A <-> ( z + ( k x. T ) ) e. A ) )
257	256	rexbidv 2978	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = z -> ( E. k e. ZZ ( x + ( k x. T ) ) e. A <-> E. k e. ZZ ( z + ( k x. T ) ) e. A ) )
258	257	elrab 3266	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) )
259	254, 258	sylib 196	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. H -> ( z e. ( X [,] Y ) /\ E. k e. ZZ ( z + ( k x. T ) ) e. A ) )
260	259	simprd 463	. . . . . . . . . . . . . . . . . . 19 |- ( z e. H -> E. k e. ZZ ( z + ( k x. T ) ) e. A )
261	260	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. H /\ z e. H ) -> E. k e. ZZ ( z + ( k x. T ) ) e. A )
262	252, 261	jca 532	. . . . . . . . . . . . . . . . 17 |- ( ( y e. H /\ z e. H ) -> ( E. j e. ZZ ( y + ( j x. T ) ) e. A /\ E. k e. ZZ ( z + ( k x. T ) ) e. A ) )
263		reeanv 3034	. . . . . . . . . . . . . . . . 17 |- ( 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 ) )
264	262, 263	sylibr 212	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) )
265	264	ad2antlr 726	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) )
266	228	ad3antrrr 729	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
267		simpl1 999	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> y e. RR )
268		simpl2 1000	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> z e. RR )
269		simpr 461	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> y < z )
270	267, 268, 269	3jca 1176	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( y e. RR /\ z e. RR /\ y =/= z ) /\ y < z ) -> ( y e. RR /\ z e. RR /\ y < z ) )
271	270	adantll 713	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( y e. RR /\ z e. RR /\ y =/= z ) ) /\ y < z ) -> ( y e. RR /\ z e. RR /\ y < z ) )
272	271	adantlr 714	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 ) )
273		simplr 754	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 ) )
274		nfv 1683	. . . . . . . . . . . . . . . . . 18 |- F/ 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 ) ) )
275		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . 22 |- ( b = z -> ( b e. RR <-> z e. RR ) )
276		breq2 4457	. . . . . . . . . . . . . . . . . . . . . 22 |- ( b = z -> ( y < b <-> y < z ) )
277	275, 276	3anbi23d 1302	. . . . . . . . . . . . . . . . . . . . 21 |- ( b = z -> ( ( y e. RR /\ b e. RR /\ y < b ) <-> ( y e. RR /\ z e. RR /\ y < z ) ) )
278	277	anbi2d 703	. . . . . . . . . . . . . . . . . . . 20 |- ( b = z -> ( ( ph /\ ( y e. RR /\ b e. RR /\ y < b ) ) <-> ( ph /\ ( y e. RR /\ z e. RR /\ y < z ) ) ) )
279		nfv 1683	. . . . . . . . . . . . . . . . . . . . 21 |- F/ j b = z
280		nfv 1683	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ k b = z
281		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( b = z -> ( b + ( k x. T ) ) = ( z + ( k x. T ) ) )
282	281	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( b = z -> ( ( b + ( k x. T ) ) e. A <-> ( z + ( k x. T ) ) e. A ) )
283	282	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 ) ) )
284	280, 283	rexbid 2977	. . . . . . . . . . . . . . . . . . . . 21 |- ( b = z -> ( E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) <-> E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( z + ( k x. T ) ) e. A ) ) )
285	279, 284	rexbid 2977	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) )
286	278, 285	anbi12d 710	. . . . . . . . . . . . . . . . . . 19 |- ( 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 ) ) ) )
287		oveq2 6303	. . . . . . . . . . . . . . . . . . . . 21 |- ( b = z -> ( y - b ) = ( y - z ) )
288	287	fveq2d 5876	. . . . . . . . . . . . . . . . . . . 20 |- ( b = z -> ( abs ` ( y - b ) ) = ( abs ` ( y - z ) ) )
289	288	breq2d 4465	. . . . . . . . . . . . . . . . . . 19 |- ( b = z -> ( E <_ ( abs ` ( y - b ) ) <-> E <_ ( abs ` ( y - z ) ) ) )
290	286, 289	imbi12d 320	. . . . . . . . . . . . . . . . . 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 ) ) -> 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 ) ) ) ) )
291		nfv 1683	. . . . . . . . . . . . . . . . . . 19 |- F/ 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 ) ) -> E <_ ( abs ` ( y - b ) ) )
292		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = y -> ( a e. RR <-> y e. RR ) )
293		breq1 4456	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = y -> ( a < b <-> y < b ) )
294	292, 293	3anbi13d 1301	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = y -> ( ( a e. RR /\ b e. RR /\ a < b ) <-> ( y e. RR /\ b e. RR /\ y < b ) ) )
295	294	anbi2d 703	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = y -> ( ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) <-> ( ph /\ ( y e. RR /\ b e. RR /\ y < b ) ) ) )
296		nfv 1683	. . . . . . . . . . . . . . . . . . . . . 22 |- F/ j a = y
297		nfv 1683	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/ k a = y
298		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( a = y -> ( a + ( j x. T ) ) = ( y + ( j x. T ) ) )
299	298	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( a = y -> ( ( a + ( j x. T ) ) e. A <-> ( y + ( j x. T ) ) e. A ) )
300	299	anbi1d 704	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 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 ) ) )
301	297, 300	rexbid 2977	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = y -> ( E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) <-> E. k e. ZZ ( ( y + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) )
302	296, 301	rexbid 2977	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) ) )
303	295, 302	anbi12d 710	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) ) )
304		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = y -> ( a - b ) = ( y - b ) )
305	304	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = y -> ( abs ` ( a - b ) ) = ( abs ` ( y - b ) ) )
306	305	breq2d 4465	. . . . . . . . . . . . . . . . . . . 20 |- ( a = y -> ( E <_ ( abs ` ( a - b ) ) <-> E <_ ( abs ` ( y - b ) ) ) )
307	303, 306	imbi12d 320	. . . . . . . . . . . . . . . . . . 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 ) ) -> 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 ) ) ) ) )
308		fourierdlem42.15	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) ) )
309	308	biimpri 206	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) ) -> ps )
310	308	simprbi 464	. . . . . . . . . . . . . . . . . . . . 21 |- ( ps -> E. j e. ZZ E. k e. ZZ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) )
311	308	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 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 ) ) )
312	311	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ps -> ( ph /\ ( a e. RR /\ b e. RR /\ a < b ) ) )
313	312	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ps -> ph )
314	313, 57	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ps -> B e. RR )
315	314	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> B e. RR )
316	313, 58	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ps -> C e. RR )
317	316	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> C e. RR )
318	313, 56	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ps -> A C_ ( B [,] C ) )
319	318	sselda 3509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( b + ( k x. T ) ) e. A ) -> ( b + ( k x. T ) ) e. ( B [,] C ) )
320	319	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( b + ( k x. T ) ) e. ( B [,] C ) )
321	318	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> A C_ ( B [,] C ) )
322		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> ( a + ( j x. T ) ) e. A )
323	321, 322	sseldd 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ps /\ ( a + ( j x. T ) ) e. A ) -> ( a + ( j x. T ) ) e. ( B [,] C ) )
324	323	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( a + ( j x. T ) ) e. ( B [,] C ) )
325	315, 317, 320, 324	iccsuble 31446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ ( C - B ) )
326		fourierdlem42.t	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- T = ( C - B )
327	326	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( C - B ) = T
328	327	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( C - B ) = T )
329	325, 328	breqtrd 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ps /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
330	329	3adant2 1015	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( 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 )
331	330	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( 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 )
332		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> -. k <_ j )
333		zre 10880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( j e. ZZ -> j e. RR )
334	333	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( j e. ZZ /\ k e. ZZ ) -> j e. RR )
335	334	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> j e. RR )
336		zre 10880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( k e. ZZ -> k e. RR )
337	336	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( j e. ZZ /\ k e. ZZ ) -> k e. RR )
338	337	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> k e. RR )
339	335, 338	ltnled 9743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> ( j < k <-> -. k <_ j ) )
340	332, 339	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> j < k )
341	58, 57	resubcld 9999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ph -> ( C - B ) e. RR )
342	326, 341	syl5eqel 2559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> T e. RR )
343	313, 342	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ps -> T e. RR )
344	343	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> T e. RR )
345	344	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T e. RR )
346	337	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> k e. RR )
347	334	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> j e. RR )
348	346, 347	resubcld 9999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k - j ) e. RR )
349	348, 344	remulcld 9636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) e. RR )
350	349	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( ( k - j ) x. T ) e. RR )
351	312	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ps -> ( a e. RR /\ b e. RR /\ a < b ) )
352	351	simp2d 1009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ps -> b e. RR )
353	352	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> b e. RR )
354	336	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ps /\ k e. ZZ ) -> k e. RR )
355	343	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ps /\ k e. ZZ ) -> T e. RR )
356	354, 355	remulcld 9636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ps /\ k e. ZZ ) -> ( k x. T ) e. RR )
357	356	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k x. T ) e. RR )
358	353, 357	readdcld 9635	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( b + ( k x. T ) ) e. RR )
359	351	simp1d 1008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ps -> a e. RR )
360	359	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> a e. RR )
361	333	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ps /\ j e. ZZ ) -> j e. RR )
362	343	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ps /\ j e. ZZ ) -> T e. RR )
363	361, 362	remulcld 9636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ps /\ j e. ZZ ) -> ( j x. T ) e. RR )
364	363	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j x. T ) e. RR )
365	360, 364	readdcld 9635	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( a + ( j x. T ) ) e. RR )
366	358, 365	resubcld 9999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) e. RR )
367	366	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) e. RR )
368	343	recnd 9634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ps -> T e. CC )
369	368	mulid2d 9626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ps -> ( 1 x. T ) = T )
370	369	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ps -> T = ( 1 x. T ) )
371	370	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T = ( 1 x. T ) )
372		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> j < k )
373		simplrl 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> j e. ZZ )
374		simplrr 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> k e. ZZ )
375		zltlem1 10927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( j e. ZZ /\ k e. ZZ ) -> ( j < k <-> j <_ ( k - 1 ) ) )
376	373, 374, 375	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( j < k <-> j <_ ( k - 1 ) ) )
377	372, 376	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> j <_ ( k - 1 ) )
378		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> j <_ ( k - 1 ) )
379	347	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> j e. RR )
380		peano2rem 9898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( k e. RR -> ( k - 1 ) e. RR )
381	346, 380	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k - 1 ) e. RR )
382	381	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( k - 1 ) e. RR )
383		1re 9607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- 1 e. RR
384	383	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> 1 e. RR )
385	384, 379	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( 1 e. RR /\ j e. RR ) )
386		resubcl 9895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( 1 e. RR /\ j e. RR ) -> ( 1 - j ) e. RR )
387	385, 386	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( 1 - j ) e. RR )
388	379, 382, 387	leadd1d 10158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( j <_ ( k - 1 ) <-> ( j + ( 1 - j ) ) <_ ( ( k - 1 ) + ( 1 - j ) ) ) )
389	378, 388	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( j + ( 1 - j ) ) <_ ( ( k - 1 ) + ( 1 - j ) ) )
390	333	recnd 9634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( j e. ZZ -> j e. CC )
391	390	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( j e. ZZ /\ k e. ZZ ) -> j e. CC )
392		ax-1cn 9562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- 1 e. CC
393	392	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( j e. ZZ /\ k e. ZZ ) -> 1 e. CC )
394	391, 393	pncan3d 9945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( j e. ZZ /\ k e. ZZ ) -> ( j + ( 1 - j ) ) = 1 )
395	394	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( j + ( 1 - j ) ) = 1 )
396	336	recnd 9634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( k e. ZZ -> k e. CC )
397	396	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( j e. ZZ /\ k e. ZZ ) -> k e. CC )
398	397, 393, 391	npncand 9966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( j e. ZZ /\ k e. ZZ ) -> ( ( k - 1 ) + ( 1 - j ) ) = ( k - j ) )
399	398	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( ( k - 1 ) + ( 1 - j ) ) = ( k - j ) )
400	395, 399	breq12d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> ( ( j + ( 1 - j ) ) <_ ( ( k - 1 ) + ( 1 - j ) ) <-> 1 <_ ( k - j ) ) )
401	389, 400	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j <_ ( k - 1 ) ) -> 1 <_ ( k - j ) )
402	401	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j <_ ( k - 1 ) -> 1 <_ ( k - j ) ) )
403	402	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( j <_ ( k - 1 ) -> 1 <_ ( k - j ) ) )
404	377, 403	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> 1 <_ ( k - j ) )
405	383	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> 1 e. RR )
406	348	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( k - j ) e. RR )
407	57, 58	posdifd 10151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ph -> ( B < C <-> 0 < ( C - B ) ) )
408	175, 407	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ph -> 0 < ( C - B ) )
409	327	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ph -> ( C - B ) = T )
410	408, 409	breqtrd 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ph -> 0 < T )
411	342, 410	elrpd 11266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ph -> T e. RR+ )
412	313, 411	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ps -> T e. RR+ )
413	412	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T e. RR+ )
414	405, 406, 413	lemul1d 11307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( 1 <_ ( k - j ) <-> ( 1 x. T ) <_ ( ( k - j ) x. T ) ) )
415	404, 414	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( 1 x. T ) <_ ( ( k - j ) x. T ) )
416	371, 415	eqbrtrd 4473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T <_ ( ( k - j ) x. T ) )
417	352, 359	resubcld 9999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ps -> ( b - a ) e. RR )
418	351	simp3d 1010	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ps -> a < b )
419	359, 352	posdifd 10151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ps -> ( a < b <-> 0 < ( b - a ) ) )
420	418, 419	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ps -> 0 < ( b - a ) )
421	417, 420	elrpd 11266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ps -> ( b - a ) e. RR+ )
422	421	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( b - a ) e. RR+ )
423	349, 422	ltaddrp2d 11298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) < ( ( b - a ) + ( ( k - j ) x. T ) ) )
424	352	recnd 9634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ps -> b e. CC )
425	424	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> b e. CC )
426	356	recnd 9634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ps /\ k e. ZZ ) -> ( k x. T ) e. CC )
427	426	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( k x. T ) e. CC )
428	359	recnd 9634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ps -> a e. CC )
429	428	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> a e. CC )
430	363	recnd 9634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ps /\ j e. ZZ ) -> ( j x. T ) e. CC )
431	430	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j x. T ) e. CC )
432	425, 427, 429, 431	addsub4d 9989	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) = ( ( b - a ) + ( ( k x. T ) - ( j x. T ) ) ) )
433	396	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> k e. CC )
434	390	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> j e. CC )
435	368	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> T e. CC )
436	433, 434, 435	subdird 10025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) = ( ( k x. T ) - ( j x. T ) ) )
437	436	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k x. T ) - ( j x. T ) ) = ( ( k - j ) x. T ) )
438	437	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b - a ) + ( ( k x. T ) - ( j x. T ) ) ) = ( ( b - a ) + ( ( k - j ) x. T ) ) )
439	432, 438	eqtr2d 2509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( b - a ) + ( ( k - j ) x. T ) ) = ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
440	423, 439	breqtrd 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( k - j ) x. T ) < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
441	440	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> ( ( k - j ) x. T ) < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
442	345, 350, 367, 416, 441	lelttrd 9751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> T < ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) )
443	345, 367	ltnled 9743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( 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 ) )
444	442, 443	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ j < k ) -> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
445	444	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j < k -> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T ) )
446	445	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> ( j < k -> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T ) )
447	340, 446	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) /\ -. k <_ j ) -> -. ( ( b + ( k x. T ) ) - ( a + ( j x. T ) ) ) <_ T )
448	447	3adantl3 1154	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( 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 )
449	331, 448	condan 792	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> k <_ j )
450	220, 222	sseldd 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ph -> sup ( R , RR , `' < ) e. RR )
451	39, 450	syl5eqel 2559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> E e. RR )
452	313, 451	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ps -> E e. RR )
453	452	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> E e. RR )
454	453	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( 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 )
455	344	3adant3 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) /\ ( ( a + ( j x. T ) ) e. A /\ ( b + ( k x. T ) ) e. A ) ) -> T e. RR )
456	455	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( 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 )
457	334, 337	resubcld 9999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( j e. ZZ /\ k e. ZZ ) -> ( j - k ) e. RR )
458	457	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( j - k ) e. RR )
459	458, 344	remulcld 9636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ps /\ ( j e. ZZ /\ k e. ZZ ) ) -> ( ( j - k ) x. T ) e. RR )
460	459	3adant3 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( 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 )
461	460	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( 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 )
462	228, 172, 175	3jca 1176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ph -> ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) )
463		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( d = C -> ( d e. A <-> C e. A ) )
464	463	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( d = C -> ( ( B e. A /\ d e. A ) <-> ( B e. A /\ C e. A ) ) )
465		breq2 4457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( d = C -> ( B < d <-> B < C ) )
466	464, 465	3anbi23d 1302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( d = C -> ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) <-> ( ph /\ ( B e. A /\ C e. A ) /\ B < C ) ) )
467		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( d = C -> ( d - B ) = ( C - B ) )
468	467	breq2d 4465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( d = C -> ( E <_ ( d - B ) <-> E <_ ( C - B ) ) )
469	466, 468	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( 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 ) ) ) )
470	170	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) -> B e. A )
471		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( c = B -> ( c e. A <-> B e. A ) )
472	471	anbi1d 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( c = B -> ( ( c e. A /\ d e. A ) <-> ( B e. A /\ d e. A ) ) )
473		breq1 4456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( c = B -> ( c < d <-> B < d ) )
474	472, 473	3anbi23d 1302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( c = B -> ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) <-> ( ph /\ ( B e. A /\ d e. A ) /\ B < d ) ) )
475		oveq2 6303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( c = B -> ( d - c ) = ( d - B ) )
476	475	breq2d 4465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( c = B -> ( E <_ ( d - c ) <-> E <_ ( d - B ) ) )
477	474, 476	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( 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 ) ) ) )
478	39	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E = sup ( R , RR , `' < ) )
479	219	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> R C_ RR )
480		0re 9608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- 0 e. RR
481	480	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ph -> 0 e. RR )
482	40	eleq2i 2545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( y e. R <-> y e. ran ( D |` I ) )
483	482	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( y e. R -> y e. ran ( D |` I ) )
484	483	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ y e. R ) -> y e. ran ( D |` I ) )
485	70	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ y e. R ) -> ( D |` I ) Fn I )
486		fvelrnb 5921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( D |` I ) Fn I -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) )
487	485, 486	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ y e. R ) -> ( y e. ran ( D |` I ) <-> E. x e. I ( ( D |` I ) ` x ) = y ) )
488	484, 487	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ y e. R ) -> E. x e. I ( ( D |` I ) ` x ) = y )
489	141	rpge0d 11272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( ( ph /\ x e. I ) -> 0 <_ ( ( D |` I ) ` x ) )
490	489	3adant3 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> 0 <_ ( ( D |` I ) ` x ) )
491		simp3 998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> ( ( D |` I ) ` x ) = y )
492	490, 491	breqtrd 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ x e. I /\ ( ( D |` I ) ` x ) = y ) -> 0 <_ y )
493	492	3exp 1195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ph -> ( x e. I -> ( ( ( D |` I ) ` x ) = y -> 0 <_ y ) ) )
494	493	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ y e. R ) -> ( x e. I -> ( ( ( D |` I ) ` x ) = y -> 0 <_ y ) ) )
495	494	rexlimdv 2957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ y e. R ) -> ( E. x e. I ( ( D |` I ) ` x ) = y -> 0 <_ y ) )
496	488, 495	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ y e. R ) -> 0 <_ y )
497	496	ralrimiva 2881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ph -> A. y e. R 0 <_ y )
498		breq1 4456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( x = 0 -> ( x <_ y <-> 0 <_ y ) )
499	498	ralbidv 2906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( x = 0 -> ( A. y e. R x <_ y <-> A. y e. R 0 <_ y ) )
500	499	rspcev 3219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( 0 e. RR /\ A. y e. R 0 <_ y ) -> E. x e. RR A. y e. R x <_ y )
501	481, 497, 500	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ph -> E. x e. RR A. y e. R x <_ y )
502	501	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> E. x e. RR A. y e. R x <_ y )
503		pm3.22 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( c e. A /\ d e. A ) -> ( d e. A /\ c e. A ) )
504		opelxp 5035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( <. d , c >. e. ( A X. A ) <-> ( d e. A /\ c e. A ) )
505	503, 504	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( c e. A /\ d e. A ) -> <. d , c >. e. ( A X. A ) )
506	505	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. ( A X. A ) )
507	56, 59	sstrd 3519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- ( ph -> A C_ RR )
508	507	sselda 3509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ( ( ph /\ c e. A ) -> c e. RR )
509	508	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ( ( ph /\ ( c e. A /\ d e. A ) ) -> c e. RR )
510	509	3adant3 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c e. RR )
511		simp3 998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c < d )
512	510, 511	ltned 9732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> c =/= d )
513	512	necomd 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> d =/= c )
514	513	neneqd 2669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> -. d = c )
515		df-br 4454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( d _I c <-> <. d , c >. e. _I )
516		vex 3121	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- c e. _V
517		ideqg 5160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( c e. _V -> ( d _I c <-> d = c ) )
518	516, 517	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( d _I c <-> d = c )
519	515, 518	bitr3i 251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( <. d , c >. e. _I <-> d = c )
520	514, 519	sylnibr 305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> -. <. d , c >. e. _I )
521	506, 520	eldifd 3492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. ( ( A X. A ) \ _I ) )
522	521, 55	syl6eleqr 2566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> <. d , c >. e. I )
523		simp1 996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ph )
524		simp2 997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c < d ) -> ( c e. A /\ d e. A ) )
525	168	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( D |` I ) = ( ( abs o. - ) |` I ) )
526	525	fveq1d 5874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( D |` I ) ` <. d , c >. ) = ( ( ( abs o. - ) |` I ) ` <. d , c >. ) )
527	505	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. ( A X. A ) )
528		necom 2736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- ( c =/= d <-> d =/= c )
529	528	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- ( c =/= d -> d =/= c )
530	529	neneqd 2669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ( c =/= d -> -. d = c )
531	530	3ad2ant3 1019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> -. d = c )
532	531, 519	sylnibr 305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> -. <. d , c >. e. _I )
533	527, 532	eldifd 3492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. ( ( A X. A ) \ _I ) )
534	533, 55	syl6eleqr 2566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. I )
535		fvres 5886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( <. d , c >. e. I -> ( ( ( abs o. - ) |` I ) ` <. d , c >. ) = ( ( abs o. - ) ` <. d , c >. ) )
536	534, 535	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( ( abs o. - ) |` I ) ` <. d , c >. ) = ( ( abs o. - ) ` <. d , c >. ) )
537	77	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> Fun - )
538		simp1 996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ph )
539	538, 534	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ph /\ <. d , c >. e. I ) )
540		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- ( x = <. d , c >. -> ( x e. I <-> <. d , c >. e. I ) )
541	540	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ( x = <. d , c >. -> ( ( ph /\ x e. I ) <-> ( ph /\ <. d , c >. e. I ) ) )
542		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ( x = <. d , c >. -> ( x e. dom - <-> <. d , c >. e. dom - ) )
543	541, 542	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ( x = <. d , c >. -> ( ( ( ph /\ x e. I ) -> x e. dom - ) <-> ( ( ph /\ <. d , c >. e. I ) -> <. d , c >. e. dom - ) ) )
544	84	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ( x e. I -> ( ( ph /\ x e. I ) -> x e. dom - ) )
545	543, 544	vtoclga 3182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( <. d , c >. e. I -> ( ( ph /\ <. d , c >. e. I ) -> <. d , c >. e. dom - ) )
546	534, 539, 545	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> <. d , c >. e. dom - )
547		fvco 5950	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( Fun - /\ <. d , c >. e. dom - ) -> ( ( abs o. - ) ` <. d , c >. ) = ( abs ` ( - ` <. d , c >. ) ) )
548	537, 546, 547	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ ( c e. A /\ d e. A ) /\ c =/= d ) -> ( ( abs o. - ) ` <. d , c >. ) = ( abs ` ( - ` <. d , c >. ) ) )
549		df-ov 6298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ( d - c ) = ( - ` <. d , c >. )
550	549	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( - ` <. d , c >. ) = ( d - c )
551	550	fveq2i 5875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( abs ` ( - ` <. d , c >. ) ) = ( abs ` ( d - c ) )
552	551	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ph /\ ( c e. A /\ d e.