Theorem fourierdlem41 40365

Description: Lemma used to prove that every real is a limit point for the domain of the derivative of the periodic function to be approximated. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem41.a	|- ( ph -> A e. RR )
fourierdlem41.b	|- ( ph -> B e. RR )
fourierdlem41.altb	|- ( ph -> A < B )
fourierdlem41.t	|- T = ( B - A )
fourierdlem41.dper	|- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D )
fourierdlem41.x	|- ( ph -> X e. RR )
fourierdlem41.z	|- Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
fourierdlem41.e	|- E = ( x e. RR |-> ( x + ( Z ` x ) ) )
fourierdlem41.p	|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem41.m	|- ( ph -> M e. NN )
fourierdlem41.q	|- ( ph -> Q e. ( P ` M ) )
fourierdlem41.qssd	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )

Assertion

Ref	Expression
fourierdlem41	|- ( ph -> ( E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) /\ E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) ) )

Distinct variable groups:   x, k   A, m, p   x, A   B, i, k   B, m, p, i   x, B, y, k   D, i, k, y   x, D   i, E, k, y   i, M, k   m, M, p   y, M   Q, i, k   Q, p   y, Q   T, k, x, y   i, X, k   x, X, y   k, Z, x, y   ph, i, k   ph, x, y

Allowed substitution hints:   ph( m, p)   A( y, i, k)   D( m, p)   P( x, y, i, k, m, p)   Q( x, m)   T( i, m, p)   E( x, m, p)   M( x)   X( m, p)   Z( i, m, p)

Proof of Theorem fourierdlem41

Dummy variable j is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 477	. . . . . 6 |- ( ( ph /\ ( E ` X ) e. ran Q ) -> ( E ` X ) e. ran Q )
2		fourierdlem41.q	. . . . . . . . . . 11 |- ( ph -> Q e. ( P ` M ) )
3		fourierdlem41.m	. . . . . . . . . . . 12 |- ( ph -> M e. NN )
4		fourierdlem41.p	. . . . . . . . . . . . 13 |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
5	4	fourierdlem2 40326	. . . . . . . . . . . 12 |- ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
6	3, 5	syl 17	. . . . . . . . . . 11 |- ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
7	2, 6	mpbid 222	. . . . . . . . . 10 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
8	7	simpld 475	. . . . . . . . 9 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
9		elmapi 7879	. . . . . . . . 9 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
10		ffn 6045	. . . . . . . . 9 |- ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
11	8, 9, 10	3syl 18	. . . . . . . 8 |- ( ph -> Q Fn ( 0 ... M ) )
12	11	adantr 481	. . . . . . 7 |- ( ( ph /\ ( E ` X ) e. ran Q ) -> Q Fn ( 0 ... M ) )
13		fvelrnb 6243	. . . . . . 7 |- ( Q Fn ( 0 ... M ) -> ( ( E ` X ) e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) ) )
14	12, 13	syl 17	. . . . . 6 |- ( ( ph /\ ( E ` X ) e. ran Q ) -> ( ( E ` X ) e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) ) )
15	1, 14	mpbid 222	. . . . 5 |- ( ( ph /\ ( E ` X ) e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) )
16		0zd 11389	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 e. ZZ )
17		elfzelz 12342	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> j e. ZZ )
18	17	3ad2ant2 1083	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ZZ )
19		1zzd 11408	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 e. ZZ )
20	18, 19	zsubcld 11487	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ZZ )
21		simpll 790	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. 0 < j ) -> ph )
22		elfzle1 12344	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( 0 ... M ) -> 0 <_ j )
23	22	anim1i 592	. . . . . . . . . . . . . . . . . 18 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> ( 0 <_ j /\ -. 0 < j ) )
24		0red 10041	. . . . . . . . . . . . . . . . . . 19 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> 0 e. RR )
25	17	zred 11482	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. ( 0 ... M ) -> j e. RR )
26	25	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> j e. RR )
27	24, 26	eqleltd 10181	. . . . . . . . . . . . . . . . . 18 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> ( 0 = j <-> ( 0 <_ j /\ -. 0 < j ) ) )
28	23, 27	mpbird 247	. . . . . . . . . . . . . . . . 17 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> 0 = j )
29	28	eqcomd 2628	. . . . . . . . . . . . . . . 16 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> j = 0 )
30	29	adantll 750	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. 0 < j ) -> j = 0 )
31		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( j = 0 -> ( Q ` j ) = ( Q ` 0 ) )
32	7	simprld 795	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
33	32	simpld 475	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Q ` 0 ) = A )
34	31, 33	sylan9eqr 2678	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j = 0 ) -> ( Q ` j ) = A )
35	21, 30, 34	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. 0 < j ) -> ( Q ` j ) = A )
36	35	3adantl3 1219	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> ( Q ` j ) = A )
37		simpr 477	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
38		fourierdlem41.a	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A e. RR )
39	38	rexrd 10089	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> A e. RR* )
40		fourierdlem41.b	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> B e. RR )
41	40	rexrd 10089	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> B e. RR* )
42		fourierdlem41.altb	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> A < B )
43		fourierdlem41.t	. . . . . . . . . . . . . . . . . . . . . . 23 |- T = ( B - A )
44		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
45	38, 40, 42, 43, 44	fourierdlem4 40328	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) : RR --> ( A (,] B ) )
46		fourierdlem41.e	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- E = ( x e. RR |-> ( x + ( Z ` x ) ) )
47	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> E = ( x e. RR |-> ( x + ( Z ` x ) ) ) )
48		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ x e. RR ) -> x e. RR )
49	40	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ x e. RR ) -> B e. RR )
50	49, 48	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ x e. RR ) -> ( B - x ) e. RR )
51	40, 38	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> ( B - A ) e. RR )
52	43, 51	syl5eqel 2705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ph -> T e. RR )
53	52	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ x e. RR ) -> T e. RR )
54		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> 0 e. RR )
55	38, 40	posdifd 10614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
56	42, 55	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> 0 < ( B - A ) )
57	43	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( B - A ) = T
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> ( B - A ) = T )
59	56, 58	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> 0 < T )
60	54, 59	gtned 10172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ph -> T =/= 0 )
61	60	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ x e. RR ) -> T =/= 0 )
62	50, 53, 61	redivcld 10853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ x e. RR ) -> ( ( B - x ) / T ) e. RR )
63	62	flcld 12599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ x e. RR ) -> ( |_ ` ( ( B - x ) / T ) ) e. ZZ )
64	63	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ x e. RR ) -> ( |_ ` ( ( B - x ) / T ) ) e. RR )
65	64, 53	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ x e. RR ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. RR )
66		fourierdlem41.z	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
67	66	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. RR /\ ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. RR ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
68	48, 65, 67	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ x e. RR ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
69	68	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ x e. RR ) -> ( x + ( Z ` x ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
70	69	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( x e. RR |-> ( x + ( Z ` x ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
71	47, 70	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
72	71	feq1d 6030	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( E : RR --> ( A (,] B ) <-> ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) : RR --> ( A (,] B ) ) )
73	45, 72	mpbird 247	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> E : RR --> ( A (,] B ) )
74		fourierdlem41.x	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> X e. RR )
75	73, 74	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( E ` X ) e. ( A (,] B ) )
76		iocgtlb 39724	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. RR* /\ B e. RR* /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
77	39, 41, 75, 76	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A < ( E ` X ) )
78	38, 77	gtned 10172	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( E ` X ) =/= A )
79	78	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) =/= A )
80	37, 79	eqnetrd 2861	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) =/= A )
81	80	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> ( Q ` j ) =/= A )
82	81	3adantl2 1218	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> ( Q ` j ) =/= A )
83	82	neneqd 2799	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> -. ( Q ` j ) = A )
84	36, 83	condan 835	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 < j )
85		zltlem1 11430	. . . . . . . . . . . . 13 |- ( ( 0 e. ZZ /\ j e. ZZ ) -> ( 0 < j <-> 0 <_ ( j - 1 ) ) )
86	16, 18, 85	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 < j <-> 0 <_ ( j - 1 ) ) )
87	84, 86	mpbid 222	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ ( j - 1 ) )
88		eluz2 11693	. . . . . . . . . . 11 |- ( ( j - 1 ) e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ ( j - 1 ) e. ZZ /\ 0 <_ ( j - 1 ) ) )
89	16, 20, 87, 88	syl3anbrc 1246	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( ZZ>= ` 0 ) )
90		elfzel2 12340	. . . . . . . . . . 11 |- ( j e. ( 0 ... M ) -> M e. ZZ )
91	90	3ad2ant2 1083	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> M e. ZZ )
92		1red 10055	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> 1 e. RR )
93	25, 92	resubcld 10458	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> ( j - 1 ) e. RR )
94	90	zred 11482	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> M e. RR )
95	25	ltm1d 10956	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> ( j - 1 ) < j )
96		elfzle2 12345	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> j <_ M )
97	93, 25, 94, 95, 96	ltletrd 10197	. . . . . . . . . . 11 |- ( j e. ( 0 ... M ) -> ( j - 1 ) < M )
98	97	3ad2ant2 1083	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) < M )
99		elfzo2 12473	. . . . . . . . . 10 |- ( ( j - 1 ) e. ( 0..^ M ) <-> ( ( j - 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( j - 1 ) < M ) )
100	89, 91, 98, 99	syl3anbrc 1246	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0..^ M ) )
101	8, 9	syl 17	. . . . . . . . . . . . 13 |- ( ph -> Q : ( 0 ... M ) --> RR )
102	101	3ad2ant1 1082	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> Q : ( 0 ... M ) --> RR )
103	16, 91, 20	3jca 1242	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) )
104	93, 94, 97	ltled 10185	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... M ) -> ( j - 1 ) <_ M )
105	104	3ad2ant2 1083	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) <_ M )
106	103, 87, 105	jca32 558	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) /\ ( 0 <_ ( j - 1 ) /\ ( j - 1 ) <_ M ) ) )
107		elfz2 12333	. . . . . . . . . . . . 13 |- ( ( j - 1 ) e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) /\ ( 0 <_ ( j - 1 ) /\ ( j - 1 ) <_ M ) ) )
108	106, 107	sylibr 224	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ... M ) )
109	102, 108	ffvelrnd 6360	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR )
110	109	rexrd 10089	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR* )
111	25	recnd 10068	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... M ) -> j e. CC )
112		1cnd 10056	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... M ) -> 1 e. CC )
113	111, 112	npcand 10396	. . . . . . . . . . . . . 14 |- ( j e. ( 0 ... M ) -> ( ( j - 1 ) + 1 ) = j )
114	113	fveq2d 6195	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
115	114	adantl 482	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
116	101	ffvelrnda 6359	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR )
117	116	rexrd 10089	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
118	115, 117	eqeltrd 2701	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) e. RR* )
119	118	3adant3 1081	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) e. RR* )
120		id 22	. . . . . . . . . . . . . . . 16 |- ( x = X -> x = X )
121		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( x = X -> ( Z ` x ) = ( Z ` X ) )
122	120, 121	oveq12d 6668	. . . . . . . . . . . . . . 15 |- ( x = X -> ( x + ( Z ` x ) ) = ( X + ( Z ` X ) ) )
123	122	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ph /\ x = X ) -> ( x + ( Z ` x ) ) = ( X + ( Z ` X ) ) )
124	66	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
125		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = X -> ( B - x ) = ( B - X ) )
126	125	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20 |- ( x = X -> ( ( B - x ) / T ) = ( ( B - X ) / T ) )
127	126	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( x = X -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - X ) / T ) ) )
128	127	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( x = X -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
129	128	adantl 482	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x = X ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
130	40, 74	resubcld 10458	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( B - X ) e. RR )
131	130, 52, 60	redivcld 10853	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( B - X ) / T ) e. RR )
132	131	flcld 12599	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
133	132	zred 11482	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. RR )
134	133, 52	remulcld 10070	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
135	124, 129, 74, 134	fvmptd 6288	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Z ` X ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
136	135, 134	eqeltrd 2701	. . . . . . . . . . . . . . 15 |- ( ph -> ( Z ` X ) e. RR )
137	74, 136	readdcld 10069	. . . . . . . . . . . . . 14 |- ( ph -> ( X + ( Z ` X ) ) e. RR )
138	47, 123, 74, 137	fvmptd 6288	. . . . . . . . . . . . 13 |- ( ph -> ( E ` X ) = ( X + ( Z ` X ) ) )
139	138, 137	eqeltrd 2701	. . . . . . . . . . . 12 |- ( ph -> ( E ` X ) e. RR )
140	139	rexrd 10089	. . . . . . . . . . 11 |- ( ph -> ( E ` X ) e. RR* )
141	140	3ad2ant1 1082	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. RR* )
142		simp1 1061	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ph )
143		ovex 6678	. . . . . . . . . . . . . 14 |- ( j - 1 ) e. _V
144		eleq1 2689	. . . . . . . . . . . . . . . 16 |- ( i = ( j - 1 ) -> ( i e. ( 0..^ M ) <-> ( j - 1 ) e. ( 0..^ M ) ) )
145	144	anbi2d 740	. . . . . . . . . . . . . . 15 |- ( i = ( j - 1 ) -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) ) )
146		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( i = ( j - 1 ) -> ( Q ` i ) = ( Q ` ( j - 1 ) ) )
147		oveq1 6657	. . . . . . . . . . . . . . . . 17 |- ( i = ( j - 1 ) -> ( i + 1 ) = ( ( j - 1 ) + 1 ) )
148	147	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( i = ( j - 1 ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
149	146, 148	breq12d 4666	. . . . . . . . . . . . . . 15 |- ( i = ( j - 1 ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) )
150	145, 149	imbi12d 334	. . . . . . . . . . . . . 14 |- ( i = ( j - 1 ) -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) ) )
151	7	simprrd 797	. . . . . . . . . . . . . . 15 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
152	151	r19.21bi 2932	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
153	143, 150, 152	vtocl 3259	. . . . . . . . . . . . 13 |- ( ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
154	142, 100, 153	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
155	114	3ad2ant2 1083	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
156	154, 155	breqtrd 4679	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` j ) )
157		simp3 1063	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
158	156, 157	breqtrd 4679	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( E ` X ) )
159	139	leidd 10594	. . . . . . . . . . . . . 14 |- ( ph -> ( E ` X ) <_ ( E ` X ) )
160	159	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( E ` X ) )
161	37	eqcomd 2628	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) = ( Q ` j ) )
162	160, 161	breqtrd 4679	. . . . . . . . . . . 12 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
163	162	3adant2 1080	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
164	113	eqcomd 2628	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> j = ( ( j - 1 ) + 1 ) )
165	164	fveq2d 6195	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
166	165	3ad2ant2 1083	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
167	163, 166	breqtrd 4679	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` ( ( j - 1 ) + 1 ) ) )
168	110, 119, 141, 158, 167	eliocd 39730	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
169	146, 148	oveq12d 6668	. . . . . . . . . . 11 |- ( i = ( j - 1 ) -> ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
170	169	eleq2d 2687	. . . . . . . . . 10 |- ( i = ( j - 1 ) -> ( ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) <-> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) ) )
171	170	rspcev 3309	. . . . . . . . 9 |- ( ( ( j - 1 ) e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
172	100, 168, 171	syl2anc 693	. . . . . . . 8 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
173	172	3exp 1264	. . . . . . 7 |- ( ph -> ( j e. ( 0 ... M ) -> ( ( Q ` j ) = ( E ` X ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) ) )
174	173	adantr 481	. . . . . 6 |- ( ( ph /\ ( E ` X ) e. ran Q ) -> ( j e. ( 0 ... M ) -> ( ( Q ` j ) = ( E ` X ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) ) )
175	174	rexlimdv 3030	. . . . 5 |- ( ( ph /\ ( E ` X ) e. ran Q ) -> ( E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
176	15, 175	mpd 15	. . . 4 |- ( ( ph /\ ( E ` X ) e. ran Q ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
177	3	adantr 481	. . . . . 6 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> M e. NN )
178	101	adantr 481	. . . . . 6 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> Q : ( 0 ... M ) --> RR )
179		iocssicc 12261	. . . . . . . 8 |- ( ( Q ` 0 ) (,] ( Q ` M ) ) C_ ( ( Q ` 0 ) [,] ( Q ` M ) )
180	32	simprd 479	. . . . . . . . . 10 |- ( ph -> ( Q ` M ) = B )
181	33, 180	oveq12d 6668	. . . . . . . . 9 |- ( ph -> ( ( Q ` 0 ) (,] ( Q ` M ) ) = ( A (,] B ) )
182	75, 181	eleqtrrd 2704	. . . . . . . 8 |- ( ph -> ( E ` X ) e. ( ( Q ` 0 ) (,] ( Q ` M ) ) )
183	179, 182	sseldi 3601	. . . . . . 7 |- ( ph -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
184	183	adantr 481	. . . . . 6 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
185		simpr 477	. . . . . 6 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> -. ( E ` X ) e. ran Q )
186		fveq2 6191	. . . . . . . . 9 |- ( k = j -> ( Q ` k ) = ( Q ` j ) )
187	186	breq1d 4663	. . . . . . . 8 |- ( k = j -> ( ( Q ` k ) < ( E ` X ) <-> ( Q ` j ) < ( E ` X ) ) )
188	187	cbvrabv 3199	. . . . . . 7 |- { k e. ( 0..^ M ) | ( Q ` k ) < ( E ` X ) } = { j e. ( 0..^ M ) | ( Q ` j ) < ( E ` X ) }
189	188	supeq1i 8353	. . . . . 6 |- sup ( { k e. ( 0..^ M ) | ( Q ` k ) < ( E ` X ) } , RR , < ) = sup ( { j e. ( 0..^ M ) | ( Q ` j ) < ( E ` X ) } , RR , < )
190	177, 178, 184, 185, 189	fourierdlem25 40349	. . . . 5 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
191		ioossioc 39713	. . . . . . . 8 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) )
192	191	a1i 11	. . . . . . 7 |- ( ( ( ph /\ -. ( E ` X ) e. ran Q ) /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
193	192	sseld 3602	. . . . . 6 |- ( ( ( ph /\ -. ( E ` X ) e. ran Q ) /\ i e. ( 0..^ M ) ) -> ( ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
194	193	reximdva 3017	. . . . 5 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> ( E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) )
195	190, 194	mpd 15	. . . 4 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
196	176, 195	pm2.61dan 832	. . 3 |- ( ph -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
197	101	adantr 481	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
198		elfzofz 12485	. . . . . . . . . 10 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
199	198	adantl 482	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
200	197, 199	ffvelrnd 6360	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
201	200	3adant3 1081	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
202	136	3ad2ant1 1082	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Z ` X ) e. RR )
203	201, 202	resubcld 10458	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR )
204	139	3ad2ant1 1082	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR )
205	201	rexrd 10089	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
206		fzofzp1 12565	. . . . . . . . . . . . 13 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
207	206	adantl 482	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
208	197, 207	ffvelrnd 6360	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
209	208	rexrd 10089	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
210	209	3adant3 1081	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
211		simp3 1063	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
212		iocgtlb 39724	. . . . . . . . 9 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
213	205, 210, 211, 212	syl3anc 1326	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
214	201, 204, 202, 213	ltsub1dd 10639	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < ( ( E ` X ) - ( Z ` X ) ) )
215	138	oveq1d 6665	. . . . . . . . 9 |- ( ph -> ( ( E ` X ) - ( Z ` X ) ) = ( ( X + ( Z ` X ) ) - ( Z ` X ) ) )
216	74	recnd 10068	. . . . . . . . . 10 |- ( ph -> X e. CC )
217	136	recnd 10068	. . . . . . . . . 10 |- ( ph -> ( Z ` X ) e. CC )
218	216, 217	pncand 10393	. . . . . . . . 9 |- ( ph -> ( ( X + ( Z ` X ) ) - ( Z ` X ) ) = X )
219	215, 218	eqtrd 2656	. . . . . . . 8 |- ( ph -> ( ( E ` X ) - ( Z ` X ) ) = X )
220	219	3ad2ant1 1082	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( E ` X ) - ( Z ` X ) ) = X )
221	214, 220	breqtrd 4679	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < X )
222		elioore 12205	. . . . . . . . . . 11 |- ( y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) -> y e. RR )
223	135	oveq2d 6666	. . . . . . . . . . . . . 14 |- ( ph -> ( y + ( Z ` X ) ) = ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
224	133	recnd 10068	. . . . . . . . . . . . . . 15 |- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. CC )
225	52	recnd 10068	. . . . . . . . . . . . . . 15 |- ( ph -> T e. CC )
226	224, 225	mulneg1d 10483	. . . . . . . . . . . . . 14 |- ( ph -> ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
227	223, 226	oveq12d 6668	. . . . . . . . . . . . 13 |- ( ph -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
228	227	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
229		simpr 477	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. RR ) -> y e. RR )
230	134	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. RR ) -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
231	229, 230	readdcld 10069	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. RR ) -> ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. RR )
232	231	recnd 10068	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. CC )
233	230	recnd 10068	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. CC )
234	232, 233	negsubd 10398	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
235	229	recnd 10068	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> y e. CC )
236	235, 233	pncand 10393	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = y )
237	228, 234, 236	3eqtrrd 2661	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> y = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
238	222, 237	sylan2 491	. . . . . . . . . 10 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
239	238	3ad2antl1 1223	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
240		simpl1 1064	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ph )
241		fourierdlem41.qssd	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
242	241	3adant3 1081	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
243	242	adantr 481	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
244	205	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) e. RR* )
245	210	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
246	222	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. RR )
247	136	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. RR )
248	246, 247	readdcld 10069	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. RR )
249	248	3ad2antl1 1223	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. RR )
250	136	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Z ` X ) e. RR )
251	200, 250	resubcld 10458	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR )
252	251	rexrd 10089	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
253	252	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
254	74	rexrd 10089	. . . . . . . . . . . . . . . 16 |- ( ph -> X e. RR* )
255	254	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> X e. RR* )
256		simpr 477	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
257		ioogtlb 39717	. . . . . . . . . . . . . . 15 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < y )
258	253, 255, 256, 257	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < y )
259	200	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) e. RR )
260	136	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. RR )
261	222	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. RR )
262	259, 260, 261	ltsubaddd 10623	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) < y <-> ( Q ` i ) < ( y + ( Z ` X ) ) ) )
263	258, 262	mpbid 222	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) < ( y + ( Z ` X ) ) )
264	263	3adantl3 1219	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) < ( y + ( Z ` X ) ) )
265	240, 139	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( E ` X ) e. RR )
266	208	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` ( i + 1 ) ) e. RR )
267	266	3adantl3 1219	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` ( i + 1 ) ) e. RR )
268	74	ad2antrr 762	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> X e. RR )
269		iooltub 39735	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y < X )
270	253, 255, 256, 269	syl3anc 1326	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y < X )
271	261, 268, 260, 270	ltadd1dd 10638	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( X + ( Z ` X ) ) )
272	138	eqcomd 2628	. . . . . . . . . . . . . . . 16 |- ( ph -> ( X + ( Z ` X ) ) = ( E ` X ) )
273	272	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( X + ( Z ` X ) ) = ( E ` X ) )
274	271, 273	breqtrd 4679	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( E ` X ) )
275	274	3adantl3 1219	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( E ` X ) )
276		iocleub 39725	. . . . . . . . . . . . . . 15 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
277	205, 210, 211, 276	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
278	277	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
279	249, 265, 267, 275, 278	ltletrd 10197	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( Q ` ( i + 1 ) ) )
280	244, 245, 249, 264, 279	eliood 39720	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
281	243, 280	sseldd 3604	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. D )
282	240, 131	syl 17	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( B - X ) / T ) e. RR )
283	282	flcld 12599	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
284	283	znegcld 11484	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
285		negex 10279	. . . . . . . . . . 11 |- -u ( |_ ` ( ( B - X ) / T ) ) e. _V
286		eleq1 2689	. . . . . . . . . . . . 13 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( k e. ZZ <-> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
287	286	3anbi3d 1405	. . . . . . . . . . . 12 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) ) )
288		oveq1 6657	. . . . . . . . . . . . . 14 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( k x. T ) = ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) )
289	288	oveq2d 6666	. . . . . . . . . . . . 13 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
290	289	eleq1d 2686	. . . . . . . . . . . 12 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D <-> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D ) )
291	287, 290	imbi12d 334	. . . . . . . . . . 11 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) <-> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D ) ) )
292		ovex 6678	. . . . . . . . . . . 12 |- ( y + ( Z ` X ) ) e. _V
293		eleq1 2689	. . . . . . . . . . . . . 14 |- ( x = ( y + ( Z ` X ) ) -> ( x e. D <-> ( y + ( Z ` X ) ) e. D ) )
294	293	3anbi2d 1404	. . . . . . . . . . . . 13 |- ( x = ( y + ( Z ` X ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) ) )
295		oveq1 6657	. . . . . . . . . . . . . 14 |- ( x = ( y + ( Z ` X ) ) -> ( x + ( k x. T ) ) = ( ( y + ( Z ` X ) ) + ( k x. T ) ) )
296	295	eleq1d 2686	. . . . . . . . . . . . 13 |- ( x = ( y + ( Z ` X ) ) -> ( ( x + ( k x. T ) ) e. D <-> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) )
297	294, 296	imbi12d 334	. . . . . . . . . . . 12 |- ( x = ( y + ( Z ` X ) ) -> ( ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D ) <-> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) ) )
298		fourierdlem41.dper	. . . . . . . . . . . 12 |- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D )
299	292, 297, 298	vtocl 3259	. . . . . . . . . . 11 |- ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D )
300	285, 291, 299	vtocl 3259	. . . . . . . . . 10 |- ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D )
301	240, 281, 284, 300	syl3anc 1326	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D )
302	239, 301	eqeltrd 2701	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. D )
303	302	ralrimiva 2966	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> A. y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) y e. D )
304		dfss3 3592	. . . . . . 7 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D <-> A. y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) y e. D )
305	303, 304	sylibr 224	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D )
306		breq1 4656	. . . . . . . 8 |- ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( y < X <-> ( ( Q ` i ) - ( Z ` X ) ) < X ) )
307		oveq1 6657	. . . . . . . . 9 |- ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( y (,) X ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
308	307	sseq1d 3632	. . . . . . . 8 |- ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( ( y (,) X ) C_ D <-> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D ) )
309	306, 308	anbi12d 747	. . . . . . 7 |- ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( ( y < X /\ ( y (,) X ) C_ D ) <-> ( ( ( Q ` i ) - ( Z ` X ) ) < X /\ ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D ) ) )
310	309	rspcev 3309	. . . . . 6 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR /\ ( ( ( Q ` i ) - ( Z ` X ) ) < X /\ ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D ) ) -> E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) )
311	203, 221, 305, 310	syl12anc 1324	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) )
312	311	3exp 1264	. . . 4 |- ( ph -> ( i e. ( 0..^ M ) -> ( ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) -> E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) ) ) )
313	312	rexlimdv 3030	. . 3 |- ( ph -> ( E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) -> E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) ) )
314	196, 313	mpd 15	. 2 |- ( ph -> E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) )
315		0zd 11389	. . . . . . . . . 10 |- ( ph -> 0 e. ZZ )
316	3	nnzd 11481	. . . . . . . . . 10 |- ( ph -> M e. ZZ )
317		1zzd 11408	. . . . . . . . . 10 |- ( ph -> 1 e. ZZ )
318	315, 316, 317	3jca 1242	. . . . . . . . 9 |- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) )
319		0le1 10551	. . . . . . . . . 10 |- 0 <_ 1
320	319	a1i 11	. . . . . . . . 9 |- ( ph -> 0 <_ 1 )
321	3	nnge1d 11063	. . . . . . . . 9 |- ( ph -> 1 <_ M )
322	318, 320, 321	jca32 558	. . . . . . . 8 |- ( ph -> ( ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) /\ ( 0 <_ 1 /\ 1 <_ M ) ) )
323		elfz2 12333	. . . . . . . 8 |- ( 1 e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) /\ ( 0 <_ 1 /\ 1 <_ M ) ) )
324	322, 323	sylibr 224	. . . . . . 7 |- ( ph -> 1 e. ( 0 ... M ) )
325	101, 324	ffvelrnd 6360	. . . . . 6 |- ( ph -> ( Q ` 1 ) e. RR )
326	136, 52	resubcld 10458	. . . . . 6 |- ( ph -> ( ( Z ` X ) - T ) e. RR )
327	325, 326	resubcld 10458	. . . . 5 |- ( ph -> ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR )
328	327	adantr 481	. . . 4 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR )
329	38	recnd 10068	. . . . . . . . . 10 |- ( ph -> A e. CC )
330	329, 225	pncand 10393	. . . . . . . . 9 |- ( ph -> ( ( A + T ) - T ) = A )
331	330	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( A + T ) - T ) = A )
332	43	oveq2i 6661	. . . . . . . . . . 11 |- ( A + T ) = ( A + ( B - A ) )
333	332	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ ( E ` X ) = B ) -> ( A + T ) = ( A + ( B - A ) ) )
334	40	recnd 10068	. . . . . . . . . . . 12 |- ( ph -> B e. CC )
335	329, 334	pncan3d 10395	. . . . . . . . . . 11 |- ( ph -> ( A + ( B - A ) ) = B )
336	335	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( E ` X ) = B ) -> ( A + ( B - A ) ) = B )
337		id 22	. . . . . . . . . . . 12 |- ( ( E ` X ) = B -> ( E ` X ) = B )
338	337	eqcomd 2628	. . . . . . . . . . 11 |- ( ( E ` X ) = B -> B = ( E ` X ) )
339	338	adantl 482	. . . . . . . . . 10 |- ( ( ph /\ ( E ` X ) = B ) -> B = ( E ` X ) )
340	333, 336, 339	3eqtrrd 2661	. . . . . . . . 9 |- ( ( ph /\ ( E ` X ) = B ) -> ( E ` X ) = ( A + T ) )
341	340	oveq1d 6665	. . . . . . . 8 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( E ` X ) - T ) = ( ( A + T ) - T ) )
342	33	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( E ` X ) = B ) -> ( Q ` 0 ) = A )
343	331, 341, 342	3eqtr4rd 2667	. . . . . . 7 |- ( ( ph /\ ( E ` X ) = B ) -> ( Q ` 0 ) = ( ( E ` X ) - T ) )
344	343	oveq1d 6665	. . . . . 6 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) = ( ( ( E ` X ) - T ) - ( ( Z ` X ) - T ) ) )
345	139	recnd 10068	. . . . . . . 8 |- ( ph -> ( E ` X ) e. CC )
346	345, 217, 225	nnncan2d 10427	. . . . . . 7 |- ( ph -> ( ( ( E ` X ) - T ) - ( ( Z ` X ) - T ) ) = ( ( E ` X ) - ( Z ` X ) ) )
347	346	adantr 481	. . . . . 6 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( ( E ` X ) - T ) - ( ( Z ` X ) - T ) ) = ( ( E ` X ) - ( Z ` X ) ) )
348	219	adantr 481	. . . . . 6 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( E ` X ) - ( Z ` X ) ) = X )
349	344, 347, 348	3eqtrrd 2661	. . . . 5 |- ( ( ph /\ ( E ` X ) = B ) -> X = ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) )
350	33, 38	eqeltrd 2701	. . . . . . 7 |- ( ph -> ( Q ` 0 ) e. RR )
351	3	nngt0d 11064	. . . . . . . . . 10 |- ( ph -> 0 < M )
352		fzolb 12476	. . . . . . . . . 10 |- ( 0 e. ( 0..^ M ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
353	315, 316, 351, 352	syl3anbrc 1246	. . . . . . . . 9 |- ( ph -> 0 e. ( 0..^ M ) )
354		0re 10040	. . . . . . . . . 10 |- 0 e. RR
355		eleq1 2689	. . . . . . . . . . . . 13 |- ( i = 0 -> ( i e. ( 0..^ M ) <-> 0 e. ( 0..^ M ) ) )
356	355	anbi2d 740	. . . . . . . . . . . 12 |- ( i = 0 -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ 0 e. ( 0..^ M ) ) ) )
357		fveq2 6191	. . . . . . . . . . . . 13 |- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
358		oveq1 6657	. . . . . . . . . . . . . 14 |- ( i = 0 -> ( i + 1 ) = ( 0 + 1 ) )
359	358	fveq2d 6195	. . . . . . . . . . . . 13 |- ( i = 0 -> ( Q ` ( i + 1 ) ) = ( Q ` ( 0 + 1 ) ) )
360	357, 359	breq12d 4666	. . . . . . . . . . . 12 |- ( i = 0 -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
361	356, 360	imbi12d 334	. . . . . . . . . . 11 |- ( i = 0 -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ 0 e. ( 0..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) ) )
362	361, 152	vtoclg 3266	. . . . . . . . . 10 |- ( 0 e. RR -> ( ( ph /\ 0 e. ( 0..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
363	354, 362	ax-mp 5	. . . . . . . . 9 |- ( ( ph /\ 0 e. ( 0..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
364	353, 363	mpdan 702	. . . . . . . 8 |- ( ph -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
365		0p1e1 11132	. . . . . . . . . 10 |- ( 0 + 1 ) = 1
366	365	fveq2i 6194	. . . . . . . . 9 |- ( Q ` ( 0 + 1 ) ) = ( Q ` 1 )
367	366	a1i 11	. . . . . . . 8 |- ( ph -> ( Q ` ( 0 + 1 ) ) = ( Q ` 1 ) )
368	364, 367	breqtrd 4679	. . . . . . 7 |- ( ph -> ( Q ` 0 ) < ( Q ` 1 ) )
369	350, 325, 326, 368	ltsub1dd 10639	. . . . . 6 |- ( ph -> ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
370	369	adantr 481	. . . . 5 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
371	349, 370	eqbrtrd 4675	. . . 4 |- ( ( ph /\ ( E ` X ) = B ) -> X < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
372		elioore 12205	. . . . . . . . 9 |- ( y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) -> y e. RR )
373	135	eqcomd 2628	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) = ( Z ` X ) )
374	373	negeqd 10275	. . . . . . . . . . . . . . 15 |- ( ph -> -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( Z ` X ) )
375	226, 374	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( ph -> ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( Z ` X ) )
376	225	mulid2d 10058	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 x. T ) = T )
377	375, 376	oveq12d 6668	. . . . . . . . . . . . 13 |- ( ph -> ( ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) + ( 1 x. T ) ) = ( -u ( Z ` X ) + T ) )
378	224	negcld 10379	. . . . . . . . . . . . . 14 |- ( ph -> -u ( |_ ` ( ( B - X ) / T ) ) e. CC )
379		1cnd 10056	. . . . . . . . . . . . . 14 |- ( ph -> 1 e. CC )
380	378, 379, 225	adddird 10065	. . . . . . . . . . . . 13 |- ( ph -> ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) = ( ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) + ( 1 x. T ) ) )
381	217, 225	negsubdid 10407	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( Z ` X ) - T ) = ( -u ( Z ` X ) + T ) )
382	377, 380, 381	3eqtr4d 2666	. . . . . . . . . . . 12 |- ( ph -> ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) = -u ( ( Z ` X ) - T ) )
383	382	oveq2d 6666	. . . . . . . . . . 11 |- ( ph -> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) = ( ( y + ( ( Z ` X ) - T ) ) + -u ( ( Z ` X ) - T ) ) )
384	383	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ y e. RR ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) = ( ( y + ( ( Z ` X ) - T ) ) + -u ( ( Z ` X ) - T ) ) )
385	326	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> ( ( Z ` X ) - T ) e. RR )
386	229, 385	readdcld 10069	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( y + ( ( Z ` X ) - T ) ) e. RR )
387	386	recnd 10068	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( y + ( ( Z ` X ) - T ) ) e. CC )
388	385	recnd 10068	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( ( Z ` X ) - T ) e. CC )
389	387, 388	negsubd 10398	. . . . . . . . . 10 |- ( ( ph /\ y e. RR ) -> ( ( y + ( ( Z ` X ) - T ) ) + -u ( ( Z ` X ) - T ) ) = ( ( y + ( ( Z ` X ) - T ) ) - ( ( Z ` X ) - T ) ) )
390	235, 388	pncand 10393	. . . . . . . . . 10 |- ( ( ph /\ y e. RR ) -> ( ( y + ( ( Z ` X ) - T ) ) - ( ( Z ` X ) - T ) ) = y )
391	384, 389, 390	3eqtrrd 2661	. . . . . . . . 9 |- ( ( ph /\ y e. RR ) -> y = ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) )
392	372, 391	sylan2 491	. . . . . . . 8 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y = ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) )
393	392	adantlr 751	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y = ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) )
394		simpll 790	. . . . . . . 8 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ph )
395	367	eqcomd 2628	. . . . . . . . . . . 12 |- ( ph -> ( Q ` 1 ) = ( Q ` ( 0 + 1 ) ) )
396	395	oveq2d 6666	. . . . . . . . . . 11 |- ( ph -> ( ( Q ` 0 ) (,) ( Q ` 1 ) ) = ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) )
397	357, 359	oveq12d 6668	. . . . . . . . . . . . . . . 16 |- ( i = 0 -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) )
398	397	sseq1d 3632	. . . . . . . . . . . . . . 15 |- ( i = 0 -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D <-> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D ) )
399	356, 398	imbi12d 334	. . . . . . . . . . . . . 14 |- ( i = 0 -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D ) <-> ( ( ph /\ 0 e. ( 0..^ M ) ) -> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D ) ) )
400	399, 241	vtoclg 3266	. . . . . . . . . . . . 13 |- ( 0 e. RR -> ( ( ph /\ 0 e. ( 0..^ M ) ) -> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D ) )
401	354, 400	ax-mp 5	. . . . . . . . . . . 12 |- ( ( ph /\ 0 e. ( 0..^ M ) ) -> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D )
402	353, 401	mpdan 702	. . . . . . . . . . 11 |- ( ph -> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D )
403	396, 402	eqsstrd 3639	. . . . . . . . . 10 |- ( ph -> ( ( Q ` 0 ) (,) ( Q ` 1 ) ) C_ D )
404	403	ad2antrr 762	. . . . . . . . 9 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( ( Q ` 0 ) (,) ( Q ` 1 ) ) C_ D )
405	33, 39	eqeltrd 2701	. . . . . . . . . . 11 |- ( ph -> ( Q ` 0 ) e. RR* )
406	405	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 0 ) e. RR* )
407	325	rexrd 10089	. . . . . . . . . . 11 |- ( ph -> ( Q ` 1 ) e. RR* )
408	407	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 1 ) e. RR* )
409	372, 386	sylan2 491	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) e. RR )
410	409	adantlr 751	. . . . . . . . . 10 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) e. RR )
411	345, 216, 217	subaddd 10410	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( E ` X ) - X ) = ( Z ` X ) <-> ( X + ( Z ` X ) ) = ( E ` X ) ) )
412	272, 411	mpbird 247	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( E ` X ) - X ) = ( Z ` X ) )
413		oveq1 6657	. . . . . . . . . . . . . . . 16 |- ( ( E ` X ) = B -> ( ( E ` X ) - X ) = ( B - X ) )
414	412, 413	sylan9req 2677	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( E ` X ) = B ) -> ( Z ` X ) = ( B - X ) )
415	414	oveq1d 6665	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( Z ` X ) - T ) = ( ( B - X ) - T ) )
416	415	oveq2d 6666	. . . . . . . . . . . . 13 |- ( ( ph /\ ( E ` X ) = B ) -> ( X + ( ( Z ` X ) - T ) ) = ( X + ( ( B - X ) - T ) ) )
417	130	recnd 10068	. . . . . . . . . . . . . . . 16 |- ( ph -> ( B - X ) e. CC )
418	216, 417, 225	addsubassd 10412	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( X + ( B - X ) ) - T ) = ( X + ( ( B - X ) - T ) ) )
419	418	eqcomd 2628	. . . . . . . . . . . . . 14 |- ( ph -> ( X + ( ( B - X ) - T ) ) = ( ( X + ( B - X ) ) - T ) )
420	419	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( E ` X ) = B ) -> ( X + ( ( B - X ) - T ) ) = ( ( X + ( B - X ) ) - T ) )
421	334, 225, 329	subsub23d 39499	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B - T ) = A <-> ( B - A ) = T ) )
422	58, 421	mpbird 247	. . . . . . . . . . . . . . 15 |- ( ph -> ( B - T ) = A )
423	216, 334	pncan3d 10395	. . . . . . . . . . . . . . . 16 |- ( ph -> ( X + ( B - X ) ) = B )
424	423	oveq1d 6665	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( X + ( B - X ) ) - T ) = ( B - T ) )
425	422, 424, 33	3eqtr4d 2666	. . . . . . . . . . . . . 14 |- ( ph -> ( ( X + ( B - X ) ) - T ) = ( Q ` 0 ) )
426	425	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( X + ( B - X ) ) - T ) = ( Q ` 0 ) )
427	416, 420, 426	3eqtrrd 2661	. . . . . . . . . . . 12 |- ( ( ph /\ ( E ` X ) = B ) -> ( Q ` 0 ) = ( X + ( ( Z ` X ) - T ) ) )
428	427	adantr 481	. . . . . . . . . . 11 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 0 ) = ( X + ( ( Z ` X ) - T ) ) )
429	74	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> X e. RR )
430	372	adantl 482	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y e. RR )
431	326	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( ( Z ` X ) - T ) e. RR )
432	254	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> X e. RR* )
433	327	rexrd 10089	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR* )
434	433	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR* )
435		simpr 477	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) )
436		ioogtlb 39717	. . . . . . . . . . . . . 14 |- ( ( X e. RR* /\ ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR* /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> X < y )
437	432, 434, 435, 436	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> X < y )
438	429, 430, 431, 437	ltadd1dd 10638	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( X + ( ( Z ` X ) - T ) ) < ( y + ( ( Z ` X ) - T ) ) )
439	438	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( X + ( ( Z ` X ) - T ) ) < ( y + ( ( Z ` X ) - T ) ) )
440	428, 439	eqbrtrd 4675	. . . . . . . . . 10 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 0 ) < ( y + ( ( Z ` X ) - T ) ) )
441		iooltub 39735	. . . . . . . . . . . . 13 |- ( ( X e. RR* /\ ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR* /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
442	432, 434, 435, 441	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
443	325	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 1 ) e. RR )
444	430, 431, 443	ltaddsubd 10627	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( ( y + ( ( Z ` X ) - T ) ) < ( Q ` 1 ) <-> y < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) )
445	442, 444	mpbird 247	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) < ( Q ` 1 ) )
446	445	adantlr 751	. . . . . . . . . 10 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) < ( Q ` 1 ) )
447	406, 408, 410, 440, 446	eliood 39720	. . . . . . . . 9 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) e. ( ( Q ` 0 ) (,) ( Q ` 1 ) ) )
448	404, 447	sseldd 3604	. . . . . . . 8 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) e. D )
449	132	znegcld 11484	. . . . . . . . . 10 |- ( ph -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
450	449	peano2zd 11485	. . . . . . . . 9 |- ( ph -> ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) e. ZZ )
451	450	ad2antrr 762	. . . . . . . 8 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) e. ZZ )
452		ovex 6678	. . . . . . . . 9 |- ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) e. _V
453		eleq1 2689	. . . . . . . . . . 11 |- ( k = ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) -> ( k e. ZZ <-> ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) e. ZZ ) )
454	453	3anbi3d 1405	. . . . . . . . . 10 |- ( k = ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) -> ( ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) e. ZZ ) ) )
455		oveq1 6657	. . . . . . . . . . . 12 |- ( k = ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) -> ( k x. T ) = ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) )
456	455	oveq2d 6666	. . . . . . . . . . 11 |- ( k = ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( k x. T ) ) = ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) )
457	456	eleq1d 2686	. . . . . . . . . 10 |- ( k = ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) -> ( ( ( y + ( ( Z ` X ) - T ) ) + ( k x. T ) ) e. D <-> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) e. D ) )
458	454, 457	imbi12d 334	. . . . . . . . 9 |- ( k = ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) -> ( ( ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ k e. ZZ ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( k x. T ) ) e. D ) <-> ( ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) e. ZZ ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) e. D ) ) )
459		ovex 6678	. . . . . . . . . 10 |- ( y + ( ( Z ` X ) - T ) ) e. _V
460		eleq1 2689	. . . . . . . . . . . 12 |- ( x = ( y + ( ( Z ` X ) - T ) ) -> ( x e. D <-> ( y + ( ( Z ` X ) - T ) ) e. D ) )
461	460	3anbi2d 1404	. . . . . . . . . . 11 |- ( x = ( y + ( ( Z ` X ) - T ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ k e. ZZ ) ) )
462		oveq1 6657	. . . . . . . . . . . 12 |- ( x = ( y + ( ( Z ` X ) - T ) ) -> ( x + ( k x. T ) ) = ( ( y + ( ( Z ` X ) - T ) ) + ( k x. T ) ) )
463	462	eleq1d 2686	. . . . . . . . . . 11 |- ( x = ( y + ( ( Z ` X ) - T ) ) -> ( ( x + ( k x. T ) ) e. D <-> ( ( y + ( ( Z ` X ) - T ) ) + ( k x. T ) ) e. D ) )
464	461, 463	imbi12d 334	. . . . . . . . . 10 |- ( x = ( y + ( ( Z ` X ) - T ) ) -> ( ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D ) <-> ( ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ k e. ZZ ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( k x. T ) ) e. D ) ) )
465	459, 464, 298	vtocl 3259	. . . . . . . . 9 |- ( ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ k e. ZZ ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( k x. T ) ) e. D )
466	452, 458, 465	vtocl 3259	. . . . . . . 8 |- ( ( ph /\ ( y + ( ( Z ` X ) - T ) ) e. D /\ ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) e. ZZ ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) e. D )
467	394, 448, 451, 466	syl3anc 1326	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) e. D )
468	393, 467	eqeltrd 2701	. . . . . 6 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y e. D )
469	468	ralrimiva 2966	. . . . 5 |- ( ( ph /\ ( E ` X ) = B ) -> A. y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) y e. D )
470		dfss3 3592	. . . . 5 |- ( ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) C_ D <-> A. y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) y e. D )
471	469, 470	sylibr 224	. . . 4 |- ( ( ph /\ ( E ` X ) = B ) -> ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) C_ D )
472		breq2 4657	. . . . . 6 |- ( y = ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) -> ( X < y <-> X < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) )
473		oveq2 6658	. . . . . . 7 |- ( y = ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) -> ( X (,) y ) = ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) )
474	473	sseq1d 3632	. . . . . 6 |- ( y = ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) -> ( ( X (,) y ) C_ D <-> ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) C_ D ) )
475	472, 474	anbi12d 747	. . . . 5 |- ( y = ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) -> ( ( X < y /\ ( X (,) y ) C_ D ) <-> ( X < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) /\ ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) C_ D ) ) )
476	475	rspcev 3309	. . . 4 |- ( ( ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR /\ ( X < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) /\ ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) C_ D ) ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) )
477	328, 371, 471, 476	syl12anc 1324	. . 3 |- ( ( ph /\ ( E ` X ) = B ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) )
478	15	adantlr 751	. . . . . 6 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) )
479		simp2 1062	. . . . . . . . . . 11 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ( 0 ... M ) )
480	25	3ad2ant2 1083	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. RR )
481	94	3ad2ant2 1083	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> M e. RR )
482	96	3ad2ant2 1083	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> j <_ M )
483		id 22	. . . . . . . . . . . . . . . . . 18 |- ( ( Q ` j ) = ( E ` X ) -> ( Q ` j ) = ( E ` X ) )
484	483	eqcomd 2628	. . . . . . . . . . . . . . . . 17 |- ( ( Q ` j ) = ( E ` X ) -> ( E ` X ) = ( Q ` j ) )
485	484	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( Q ` j ) = ( E ` X ) /\ M = j ) -> ( E ` X ) = ( Q ` j ) )
486	485	3ad2antl3 1225	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ M = j ) -> ( E ` X ) = ( Q ` j ) )
487		fveq2 6191	. . . . . . . . . . . . . . . . 17 |- ( M = j -> ( Q ` M ) = ( Q ` j ) )
488	487	eqcomd 2628	. . . . . . . . . . . . . . . 16 |- ( M = j -> ( Q ` j ) = ( Q ` M ) )
489	488	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ M = j ) -> ( Q ` j ) = ( Q ` M ) )
490	180	ad2antrr 762	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ M = j ) -> ( Q ` M ) = B )
491	490	3ad2antl1 1223	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ M = j ) -> ( Q ` M ) = B )
492	486, 489, 491	3eqtrd 2660	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ M = j ) -> ( E ` X ) = B )
493		neneq 2800	. . . . . . . . . . . . . . . 16 |- ( ( E ` X ) =/= B -> -. ( E ` X ) = B )
494	493	ad2antlr 763	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ M = j ) -> -. ( E ` X ) = B )
495	494	3ad2antl1 1223	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ M = j ) -> -. ( E ` X ) = B )
496	492, 495	pm2.65da 600	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> -. M = j )
497	496	neqned 2801	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> M =/= j )
498	480, 481, 482, 497	leneltd 10191	. . . . . . . . . . 11 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> j < M )
499		elfzfzo 39488	. . . . . . . . . . 11 |- ( j e. ( 0..^ M ) <-> ( j e. ( 0 ... M ) /\ j < M ) )
500	479, 498, 499	sylanbrc 698	. . . . . . . . . 10 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ( 0..^ M ) )
501	117	adantlr 751	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
502	501	3adant3 1081	. . . . . . . . . . 11 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) e. RR* )
503		simp1l 1085	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ph )
504	101	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
505		fzofzp1 12565	. . . . . . . . . . . . . . 15 |- ( j e. ( 0..^ M ) -> ( j + 1 ) e. ( 0 ... M ) )
506	505	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( j + 1 ) e. ( 0 ... M ) )
507	504, 506	ffvelrnd 6360	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( Q ` ( j + 1 ) ) e. RR )
508	507	rexrd 10089	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( Q ` ( j + 1 ) ) e. RR* )
509	503, 500, 508	syl2anc 693	. . . . . . . . . . 11 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j + 1 ) ) e. RR* )
510	141	3adant1r 1319	. . . . . . . . . . 11 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. RR* )
511	37, 160	eqbrtrd 4675	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) <_ ( E ` X ) )
512	511	adantlr 751	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) <_ ( E ` X ) )
513	512	3adant2 1080	. . . . . . . . . . 11 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) <_ ( E ` X ) )
514	484	3ad2ant3 1084	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) = ( Q ` j ) )
515		eleq1 2689	. . . . . . . . . . . . . . . 16 |- ( i = j -> ( i e. ( 0..^ M ) <-> j e. ( 0..^ M ) ) )
516	515	anbi2d 740	. . . . . . . . . . . . . . 15 |- ( i = j -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ j e. ( 0..^ M ) ) ) )
517		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( i = j -> ( Q ` i ) = ( Q ` j ) )
518		oveq1 6657	. . . . . . . . . . . . . . . . 17 |- ( i = j -> ( i + 1 ) = ( j + 1 ) )
519	518	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( i = j -> ( Q ` ( i + 1 ) ) = ( Q ` ( j + 1 ) ) )
520	517, 519	breq12d 4666	. . . . . . . . . . . . . . 15 |- ( i = j -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` j ) < ( Q ` ( j + 1 ) ) ) )
521	516, 520	imbi12d 334	. . . . . . . . . . . . . 14 |- ( i = j -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ j e. ( 0..^ M ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) ) ) )
522	521, 152	chvarv 2263	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) )
523	503, 500, 522	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) )
524	514, 523	eqbrtrd 4675	. . . . . . . . . . 11 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) < ( Q ` ( j + 1 ) ) )
525	502, 509, 510, 513, 524	elicod 12224	. . . . . . . . . 10 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` j ) [,) ( Q ` ( j + 1 ) ) ) )
526	517, 519	oveq12d 6668	. . . . . . . . . . . 12 |- ( i = j -> ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` j ) [,) ( Q ` ( j + 1 ) ) ) )
527	526	eleq2d 2687	. . . . . . . . . . 11 |- ( i = j -> ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) <-> ( E ` X ) e. ( ( Q ` j ) [,) ( Q ` ( j + 1 ) ) ) ) )
528	527	rspcev 3309	. . . . . . . . . 10 |- ( ( j e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` j ) [,) ( Q ` ( j + 1 ) ) ) ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
529	500, 525, 528	syl2anc 693	. . . . . . . . 9 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
530	529	3exp 1264	. . . . . . . 8 |- ( ( ph /\ ( E ` X ) =/= B ) -> ( j e. ( 0 ... M ) -> ( ( Q ` j ) = ( E ` X ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) ) )
531	530	adantr 481	. . . . . . 7 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) e. ran Q ) -> ( j e. ( 0 ... M ) -> ( ( Q ` j ) = ( E ` X ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) ) )
532	531	rexlimdv 3030	. . . . . 6 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) e. ran Q ) -> ( E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) )
533	478, 532	mpd 15	. . . . 5 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ ( E ` X ) e. ran Q ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
534		ioossico 12262	. . . . . . . . . . 11 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) )
535		simpr 477	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
536	534, 535	sseldi 3601	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
537	536	ex 450	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) )
538	537	adantlr 751	. . . . . . . 8 |- ( ( ( ph /\ -. ( E ` X ) e. ran Q ) /\ i e. ( 0..^ M ) ) -> ( ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) )
539	538	reximdva 3017	. . . . . . 7 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> ( E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) )
540	190, 539	mpd 15	. . . . . 6 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
541	540	adantlr 751	. . . . 5 |- ( ( ( ph /\ ( E ` X ) =/= B ) /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
542	533, 541	pm2.61dan 832	. . . 4 |- ( ( ph /\ ( E ` X ) =/= B ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
543	208, 250	resubcld 10458	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR )
544	543	3adant3 1081	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR )
545	219	eqcomd 2628	. . . . . . . . . 10 |- ( ph -> X = ( ( E ` X ) - ( Z ` X ) ) )
546	545	3ad2ant1 1082	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> X = ( ( E ` X ) - ( Z ` X ) ) )
547	139	3ad2ant1 1082	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR )
548	208	3adant3 1081	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
549	136	3ad2ant1 1082	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Z ` X ) e. RR )
550	200	rexrd 10089	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
551	550	3adant3 1081	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
552	209	3adant3 1081	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
553		simp3 1063	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
554		icoltub 39732	. . . . . . . . . . 11 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) < ( Q ` ( i + 1 ) ) )
555	551, 552, 553, 554	syl3anc 1326	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) < ( Q ` ( i + 1 ) ) )
556	547, 548, 549, 555	ltsub1dd 10639	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( ( E ` X ) - ( Z ` X ) ) < ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) )
557	546, 556	eqbrtrd 4675	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> X < ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) )
558		elioore 12205	. . . . . . . . . . . . 13 |- ( y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) -> y e. RR )
559	558, 237	sylan2 491	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
560	559	3ad2antl1 1223	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
561		simpl1 1064	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ph )
562	241	3adant3 1081	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
563	562	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
564	551	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( Q ` i ) e. RR* )
565	552	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
566	558	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y e. RR )
567	136	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( Z ` X ) e. RR )
568	566, 567	readdcld 10069	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( y + ( Z ` X ) ) e. RR )
569	568	3ad2antl1 1223	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( y + ( Z ` X ) ) e. RR )
570	200	3adant3 1081	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
571	570	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( Q ` i ) e. RR )
572	561, 139	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( E ` X ) e. RR )
573		icogelb 12225	. . . . . . . . . . . . . . . . 17 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) <_ ( E ` X ) )
574	551, 552, 553, 573	syl3anc 1326	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) <_ ( E ` X ) )
575	574	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( Q ` i ) <_ ( E ` X ) )
576	138	ad2antrr 762	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( E ` X ) = ( X + ( Z ` X ) ) )
577	74	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> X e. RR )
578	558	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y e. RR )
579	136	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( Z ` X ) e. RR )
580	254	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> X e. RR* )
581	543	rexrd 10089	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR* )
582	581	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR* )
583		simpr 477	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) )
584		ioogtlb 39717	. . . . . . . . . . . . . . . . . . 19 |- ( ( X e. RR* /\ ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR* /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> X < y )
585	580, 582, 583, 584	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> X < y )
586	577, 578, 579, 585	ltadd1dd 10638	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( X + ( Z ` X ) ) < ( y + ( Z ` X ) ) )
587	576, 586	eqbrtrd 4675	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( E ` X ) < ( y + ( Z ` X ) ) )
588	587	3adantl3 1219	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( E ` X ) < ( y + ( Z ` X ) ) )
589	571, 572, 569, 575, 588	lelttrd 10195	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( Q ` i ) < ( y + ( Z ` X ) ) )
590	543	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR )
591		iooltub 39735	. . . . . . . . . . . . . . . . . 18 |- ( ( X e. RR* /\ ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR* /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y < ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) )
592	580, 582, 583, 591	syl3anc 1326	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y < ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) )
593	578, 590, 579, 592	ltadd1dd 10638	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( y + ( Z ` X ) ) < ( ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) + ( Z ` X ) ) )
594	208	recnd 10068	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
595	217	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Z ` X ) e. CC )
596	594, 595	npcand 10396	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) + ( Z ` X ) ) = ( Q ` ( i + 1 ) ) )
597	596	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) + ( Z ` X ) ) = ( Q ` ( i + 1 ) ) )
598	593, 597	breqtrd 4679	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( y + ( Z ` X ) ) < ( Q ` ( i + 1 ) ) )
599	598	3adantl3 1219	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( y + ( Z ` X ) ) < ( Q ` ( i + 1 ) ) )
600	564, 565, 569, 589, 599	eliood 39720	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( y + ( Z ` X ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
601	563, 600	sseldd 3604	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( y + ( Z ` X ) ) e. D )
602	561, 449	syl 17	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
603	561, 601, 602, 300	syl3anc 1326	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D )
604	560, 603	eqeltrd 2701	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) ) -> y e. D )
605	604	ralrimiva 2966	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> A. y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) y e. D )
606		dfss3 3592	. . . . . . . . 9 |- ( ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) C_ D <-> A. y e. ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) y e. D )
607	605, 606	sylibr 224	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) C_ D )
608		breq2 4657	. . . . . . . . . 10 |- ( y = ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) -> ( X < y <-> X < ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) )
609		oveq2 6658	. . . . . . . . . . 11 |- ( y = ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) -> ( X (,) y ) = ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) )
610	609	sseq1d 3632	. . . . . . . . . 10 |- ( y = ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) -> ( ( X (,) y ) C_ D <-> ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) C_ D ) )
611	608, 610	anbi12d 747	. . . . . . . . 9 |- ( y = ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) -> ( ( X < y /\ ( X (,) y ) C_ D ) <-> ( X < ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) /\ ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) C_ D ) ) )
612	611	rspcev 3309	. . . . . . . 8 |- ( ( ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) e. RR /\ ( X < ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) /\ ( X (,) ( ( Q ` ( i + 1 ) ) - ( Z ` X ) ) ) C_ D ) ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) )
613	544, 557, 607, 612	syl12anc 1324	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) )
614	613	3exp 1264	. . . . . 6 |- ( ph -> ( i e. ( 0..^ M ) -> ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) ) ) )
615	614	adantr 481	. . . . 5 |- ( ( ph /\ ( E ` X ) =/= B ) -> ( i e. ( 0..^ M ) -> ( ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) ) ) )
616	615	rexlimdv 3030	. . . 4 |- ( ( ph /\ ( E ` X ) =/= B ) -> ( E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) ) )
617	542, 616	mpd 15	. . 3 |- ( ( ph /\ ( E ` X ) =/= B ) -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) )
618	477, 617	pm2.61dane 2881	. 2 |- ( ph -> E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) )
619	314, 618	jca 554	1 |- ( ph -> ( E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) /\ E. y e. RR ( X < y /\ ( X (,) y ) C_ D ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   C_ wss 3574   class class class wbr 4653   |-> cmpt 4729   ran crn 5115   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   supcsup 8346   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   -ucneg 10267   / cdiv 10684   NNcn 11020   ZZcz 11377   ZZ>=cuz 11687   (,)cioo 12175   (,]cioc 12176   [,)cico 12177   [,]cicc 12178   ...cfz 12326  ..^cfzo 12465   |_cfl 12591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-ioo 12179  df-ioc 12180  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593

This theorem is referenced by:  fourierdlem113  40436