Theorem fourierdlem41 31771

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:   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 461	. . . . . 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 31732	. . . . . . . . . . . 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 16	. . . . . . . . . . 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 210	. . . . . . . . . 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 459	. . . . . . . . 9 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
9		elmapi 7452	. . . . . . . . 9 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
10		ffn 5737	. . . . . . . . 9 |- ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
11	8, 9, 10	3syl 20	. . . . . . . 8 |- ( ph -> Q Fn ( 0 ... M ) )
12	11	adantr 465	. . . . . . 7 |- ( ( ph /\ ( E ` X ) e. ran Q ) -> Q Fn ( 0 ... M ) )
13		fvelrnb 5921	. . . . . . 7 |- ( Q Fn ( 0 ... M ) -> ( ( E ` X ) e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) ) )
14	12, 13	syl 16	. . . . . 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 210	. . . . 5 |- ( ( ph /\ ( E ` X ) e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) )
16		0zd 10888	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 e. ZZ )
17		elfzelz 11700	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... M ) -> j e. ZZ )
18	17	3ad2ant2 1018	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ZZ )
19		1zzd 10907	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 e. ZZ )
20	18, 19	zsubcld 10983	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ZZ )
21		simpll 753	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. 0 < j ) -> ph )
22		elfzle1 11701	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. ( 0 ... M ) -> 0 <_ j )
23	22	anim1i 568	. . . . . . . . . . . . . . . . . . . 20 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> ( 0 <_ j /\ -. 0 < j ) )
24		0red 9609	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> 0 e. RR )
25	17	zred 10978	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j e. ( 0 ... M ) -> j e. RR )
26	25	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> j e. RR )
27	24, 26	eqleltd 9740	. . . . . . . . . . . . . . . . . . . 20 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> ( 0 = j <-> ( 0 <_ j /\ -. 0 < j ) ) )
28	23, 27	mpbird 232	. . . . . . . . . . . . . . . . . . 19 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> 0 = j )
29	28	eqcomd 2475	. . . . . . . . . . . . . . . . . 18 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> j = 0 )
30	29	adantll 713	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. 0 < j ) -> j = 0 )
31		fveq2 5872	. . . . . . . . . . . . . . . . . . 19 |- ( j = 0 -> ( Q ` j ) = ( Q ` 0 ) )
32	31	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j = 0 ) -> ( Q ` j ) = ( Q ` 0 ) )
33	7	simprld 31320	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
34	33	simpld 459	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( Q ` 0 ) = A )
35	34	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j = 0 ) -> ( Q ` 0 ) = A )
36		eqidd 2468	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j = 0 ) -> A = A )
37	32, 35, 36	3eqtrd 2512	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j = 0 ) -> ( Q ` j ) = A )
38	21, 30, 37	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. 0 < j ) -> ( Q ` j ) = A )
39	38	3adantl3 1154	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> ( Q ` j ) = A )
40		simpr 461	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
41		fourierdlem41.a	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> A e. RR )
42	41	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> A e. RR* )
43		fourierdlem41.b	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> B e. RR )
44	43	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> B e. RR* )
45		fourierdlem41.altb	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> A < B )
46		fourierdlem41.t	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- T = ( B - A )
47		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
48	41, 43, 45, 46, 47	fourierdlem4 31734	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) : RR --> ( A (,] B ) )
49		fourierdlem41.e	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- E = ( x e. RR |-> ( x + ( Z ` x ) ) )
50	49	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> E = ( x e. RR |-> ( x + ( Z ` x ) ) ) )
51		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ x e. RR ) -> x e. RR )
52	43	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ x e. RR ) -> B e. RR )
53	52, 51	resubcld 9999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ x e. RR ) -> ( B - x ) e. RR )
54	43, 41	resubcld 9999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> ( B - A ) e. RR )
55	46, 54	syl5eqel 2559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> T e. RR )
56	55	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ x e. RR ) -> T e. RR )
57		0red 9609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> 0 e. RR )
58	41, 43	posdifd 10151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
59	45, 58	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ph -> 0 < ( B - A ) )
60	46	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( B - A ) = T
61	60	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ph -> ( B - A ) = T )
62	59, 61	breqtrd 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> 0 < T )
63	57, 62	gtned 9731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> T =/= 0 )
64	63	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ x e. RR ) -> T =/= 0 )
65	53, 56, 64	redivcld 10384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ x e. RR ) -> ( ( B - x ) / T ) e. RR )
66	65	flcld 11915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ x e. RR ) -> ( |_ ` ( ( B - x ) / T ) ) e. ZZ )
67	66	zred 10978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ x e. RR ) -> ( |_ ` ( ( B - x ) / T ) ) e. RR )
68	67, 56	remulcld 9636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ x e. RR ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. RR )
69		fourierdlem41.z	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
70	69	fvmpt2 5964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( x e. RR /\ ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. RR ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
71	51, 68, 70	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ x e. RR ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
72	71	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ x e. RR ) -> ( x + ( Z ` x ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
73	72	mpteq2dva 4539	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( x e. RR |-> ( x + ( Z ` x ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
74	50, 73	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
75	74	feq1d 5723	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( E : RR --> ( A (,] B ) <-> ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) : RR --> ( A (,] B ) ) )
76	48, 75	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> E : RR --> ( A (,] B ) )
77		fourierdlem41.x	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> X e. RR )
78	76, 77	ffvelrnd 6033	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( E ` X ) e. ( A (,] B ) )
79		iocgtlb 31422	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A e. RR* /\ B e. RR* /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
80	42, 44, 78, 79	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> A < ( E ` X ) )
81	41, 80	gtned 9731	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( E ` X ) =/= A )
82	81	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) =/= A )
83	40, 82	eqnetrd 2760	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) =/= A )
84	83	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> ( Q ` j ) =/= A )
85	84	3adantl2 1153	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> ( Q ` j ) =/= A )
86	85	neneqd 2669	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> -. ( Q ` j ) = A )
87	39, 86	condan 792	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 < j )
88		zltlem1 10927	. . . . . . . . . . . . . . 15 |- ( ( 0 e. ZZ /\ j e. ZZ ) -> ( 0 < j <-> 0 <_ ( j - 1 ) ) )
89	16, 18, 88	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 < j <-> 0 <_ ( j - 1 ) ) )
90	87, 89	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ ( j - 1 ) )
91	16, 20, 90	3jca 1176	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 e. ZZ /\ ( j - 1 ) e. ZZ /\ 0 <_ ( j - 1 ) ) )
92		eluz2 11100	. . . . . . . . . . . 12 |- ( ( j - 1 ) e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ ( j - 1 ) e. ZZ /\ 0 <_ ( j - 1 ) ) )
93	91, 92	sylibr 212	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( ZZ>= ` 0 ) )
94		elfzel2 11698	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> M e. ZZ )
95	94	3ad2ant2 1018	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> M e. ZZ )
96		1red 9623	. . . . . . . . . . . . . 14 |- ( j e. ( 0 ... M ) -> 1 e. RR )
97	25, 96	resubcld 9999	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> ( j - 1 ) e. RR )
98	94	zred 10978	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> M e. RR )
99	25	ltm1d 10490	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> ( j - 1 ) < j )
100		elfzle2 11702	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> j <_ M )
101	97, 25, 98, 99, 100	ltletrd 9753	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> ( j - 1 ) < M )
102	101	3ad2ant2 1018	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) < M )
103	93, 95, 102	3jca 1176	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( ( j - 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( j - 1 ) < M ) )
104		elfzo2 11812	. . . . . . . . . 10 |- ( ( j - 1 ) e. ( 0..^ M ) <-> ( ( j - 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( j - 1 ) < M ) )
105	103, 104	sylibr 212	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0..^ M ) )
106	8, 9	syl 16	. . . . . . . . . . . . 13 |- ( ph -> Q : ( 0 ... M ) --> RR )
107	106	3ad2ant1 1017	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> Q : ( 0 ... M ) --> RR )
108	16, 95, 20	3jca 1176	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) )
109	97, 98, 101	ltled 9744	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... M ) -> ( j - 1 ) <_ M )
110	109	3ad2ant2 1018	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) <_ M )
111	108, 90, 110	jca32 535	. . . . . . . . . . . . 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 ) ) )
112		elfz2 11691	. . . . . . . . . . . . 13 |- ( ( j - 1 ) e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ ( j - 1 ) e. ZZ ) /\ ( 0 <_ ( j - 1 ) /\ ( j - 1 ) <_ M ) ) )
113	111, 112	sylibr 212	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ... M ) )
114	107, 113	ffvelrnd 6033	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR )
115	114	rexrd 9655	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR* )
116	25	recnd 9634	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... M ) -> j e. CC )
117		1cnd 9624	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... M ) -> 1 e. CC )
118	116, 117	npcand 9946	. . . . . . . . . . . . . 14 |- ( j e. ( 0 ... M ) -> ( ( j - 1 ) + 1 ) = j )
119	118	fveq2d 5876	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
120	119	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
121	106	ffvelrnda 6032	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR )
122	121	rexrd 9655	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
123	120, 122	eqeltrd 2555	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) e. RR* )
124	123	3adant3 1016	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) e. RR* )
125		id 22	. . . . . . . . . . . . . . . 16 |- ( x = X -> x = X )
126		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( x = X -> ( Z ` x ) = ( Z ` X ) )
127	125, 126	oveq12d 6313	. . . . . . . . . . . . . . 15 |- ( x = X -> ( x + ( Z ` x ) ) = ( X + ( Z ` X ) ) )
128	127	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ x = X ) -> ( x + ( Z ` x ) ) = ( X + ( Z ` X ) ) )
129	69	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> Z = ( x e. RR |-> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
130		oveq2 6303	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = X -> ( B - x ) = ( B - X ) )
131	130	oveq1d 6310	. . . . . . . . . . . . . . . . . . . 20 |- ( x = X -> ( ( B - x ) / T ) = ( ( B - X ) / T ) )
132	131	fveq2d 5876	. . . . . . . . . . . . . . . . . . 19 |- ( x = X -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - X ) / T ) ) )
133	132	oveq1d 6310	. . . . . . . . . . . . . . . . . 18 |- ( x = X -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
134	133	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x = X ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
135	43, 77	resubcld 9999	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( B - X ) e. RR )
136	135, 55, 63	redivcld 10384	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( B - X ) / T ) e. RR )
137	136	flcld 11915	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
138	137	zred 10978	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. RR )
139	138, 55	remulcld 9636	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
140	129, 134, 77, 139	fvmptd 5962	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Z ` X ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
141	140, 139	eqeltrd 2555	. . . . . . . . . . . . . . 15 |- ( ph -> ( Z ` X ) e. RR )
142	77, 141	readdcld 9635	. . . . . . . . . . . . . 14 |- ( ph -> ( X + ( Z ` X ) ) e. RR )
143	50, 128, 77, 142	fvmptd 5962	. . . . . . . . . . . . 13 |- ( ph -> ( E ` X ) = ( X + ( Z ` X ) ) )
144	143, 142	eqeltrd 2555	. . . . . . . . . . . 12 |- ( ph -> ( E ` X ) e. RR )
145	144	rexrd 9655	. . . . . . . . . . 11 |- ( ph -> ( E ` X ) e. RR* )
146	145	3ad2ant1 1017	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. RR* )
147		simp1 996	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ph )
148		ovex 6320	. . . . . . . . . . . . . 14 |- ( j - 1 ) e. _V
149		eleq1 2539	. . . . . . . . . . . . . . . . 17 |- ( i = ( j - 1 ) -> ( i e. ( 0..^ M ) <-> ( j - 1 ) e. ( 0..^ M ) ) )
150	149	anbi2d 703	. . . . . . . . . . . . . . . 16 |- ( i = ( j - 1 ) -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) ) )
151		fveq2 5872	. . . . . . . . . . . . . . . . 17 |- ( i = ( j - 1 ) -> ( Q ` i ) = ( Q ` ( j - 1 ) ) )
152		oveq1 6302	. . . . . . . . . . . . . . . . . 18 |- ( i = ( j - 1 ) -> ( i + 1 ) = ( ( j - 1 ) + 1 ) )
153	152	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( i = ( j - 1 ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
154	151, 153	breq12d 4466	. . . . . . . . . . . . . . . 16 |- ( i = ( j - 1 ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) )
155	150, 154	imbi12d 320	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) )
156	7	simprrd 31328	. . . . . . . . . . . . . . . 16 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
157	156	r19.21bi 2836	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
158	155, 157	vtoclg 3176	. . . . . . . . . . . . . 14 |- ( ( j - 1 ) e. _V -> ( ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) )
159	148, 158	ax-mp 5	. . . . . . . . . . . . 13 |- ( ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
160	147, 105, 159	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
161	119	3ad2ant2 1018	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
162	160, 161	breqtrd 4477	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` j ) )
163		simp3 998	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
164	162, 163	breqtrd 4477	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( E ` X ) )
165	144	leidd 10131	. . . . . . . . . . . . . 14 |- ( ph -> ( E ` X ) <_ ( E ` X ) )
166	165	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( E ` X ) )
167	40	eqcomd 2475	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) = ( Q ` j ) )
168	166, 167	breqtrd 4477	. . . . . . . . . . . 12 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
169	168	3adant2 1015	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
170	118	eqcomd 2475	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> j = ( ( j - 1 ) + 1 ) )
171	170	fveq2d 5876	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
172	171	3ad2ant2 1018	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
173	169, 172	breqtrd 4477	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` ( ( j - 1 ) + 1 ) ) )
174	115, 124, 146, 164, 173	eliocd 31430	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
175	151, 153	oveq12d 6313	. . . . . . . . . . 11 |- ( i = ( j - 1 ) -> ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
176	175	eleq2d 2537	. . . . . . . . . 10 |- ( i = ( j - 1 ) -> ( ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) <-> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) ) )
177	176	rspcev 3219	. . . . . . . . 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 ) ) ) )
178	105, 174, 177	syl2anc 661	. . . . . . . 8 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
179	178	3exp 1195	. . . . . . 7 |- ( ph -> ( j e. ( 0 ... M ) -> ( ( Q ` j ) = ( E ` X ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) ) )
180	179	adantr 465	. . . . . 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 ) ) ) ) ) )
181	180	rexlimdv 2957	. . . . 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 ) ) ) ) )
182	15, 181	mpd 15	. . . 4 |- ( ( ph /\ ( E ` X ) e. ran Q ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
183	3	adantr 465	. . . . . 6 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> M e. NN )
184	106	adantr 465	. . . . . 6 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> Q : ( 0 ... M ) --> RR )
185		iocssicc 11624	. . . . . . . 8 |- ( ( Q ` 0 ) (,] ( Q ` M ) ) C_ ( ( Q ` 0 ) [,] ( Q ` M ) )
186	33	simprd 463	. . . . . . . . . . 11 |- ( ph -> ( Q ` M ) = B )
187	34, 186	oveq12d 6313	. . . . . . . . . 10 |- ( ph -> ( ( Q ` 0 ) (,] ( Q ` M ) ) = ( A (,] B ) )
188	187	eqcomd 2475	. . . . . . . . 9 |- ( ph -> ( A (,] B ) = ( ( Q ` 0 ) (,] ( Q ` M ) ) )
189	78, 188	eleqtrd 2557	. . . . . . . 8 |- ( ph -> ( E ` X ) e. ( ( Q ` 0 ) (,] ( Q ` M ) ) )
190	185, 189	sseldi 3507	. . . . . . 7 |- ( ph -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
191	190	adantr 465	. . . . . 6 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
192		simpr 461	. . . . . 6 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> -. ( E ` X ) e. ran Q )
193		fveq2 5872	. . . . . . . . 9 |- ( k = j -> ( Q ` k ) = ( Q ` j ) )
194	193	breq1d 4463	. . . . . . . 8 |- ( k = j -> ( ( Q ` k ) < ( E ` X ) <-> ( Q ` j ) < ( E ` X ) ) )
195	194	cbvrabv 3117	. . . . . . 7 |- { k e. ( 0..^ M ) | ( Q ` k ) < ( E ` X ) } = { j e. ( 0..^ M ) | ( Q ` j ) < ( E ` X ) }
196	195	supeq1i 7919	. . . . . 6 |- sup ( { k e. ( 0..^ M ) | ( Q ` k ) < ( E ` X ) } , RR , < ) = sup ( { j e. ( 0..^ M ) | ( Q ` j ) < ( E ` X ) } , RR , < )
197	183, 184, 191, 192, 196	fourierdlem25 31755	. . . . 5 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
198		ioossioc 31411	. . . . . . . 8 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) )
199	198	a1i 11	. . . . . . 7 |- ( ( ( ph /\ -. ( E ` X ) e. ran Q ) /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
200	199	sseld 3508	. . . . . 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 ) ) ) ) )
201	200	reximdva 2942	. . . . 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 ) ) ) ) )
202	197, 201	mpd 15	. . . 4 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
203	182, 202	pm2.61dan 789	. . 3 |- ( ph -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
204	106	adantr 465	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
205		elfzofz 11823	. . . . . . . . . 10 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
206	205	adantl 466	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
207	204, 206	ffvelrnd 6033	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
208	207	3adant3 1016	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
209	141	3ad2ant1 1017	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Z ` X ) e. RR )
210	208, 209	resubcld 9999	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR )
211	144	3ad2ant1 1017	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR )
212	208	rexrd 9655	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
213		fzofzp1 11889	. . . . . . . . . . . . . 14 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
214	213	adantl 466	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
215	204, 214	ffvelrnd 6033	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
216	215	rexrd 9655	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
217	216	3adant3 1016	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
218		simp3 998	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
219		iocgtlb 31422	. . . . . . . . . 10 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
220	212, 217, 218, 219	syl3anc 1228	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
221	208, 211, 209, 220	ltsub1dd 10176	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < ( ( E ` X ) - ( Z ` X ) ) )
222	143	oveq1d 6310	. . . . . . . . . 10 |- ( ph -> ( ( E ` X ) - ( Z ` X ) ) = ( ( X + ( Z ` X ) ) - ( Z ` X ) ) )
223	77	recnd 9634	. . . . . . . . . . 11 |- ( ph -> X e. CC )
224	141	recnd 9634	. . . . . . . . . . 11 |- ( ph -> ( Z ` X ) e. CC )
225	223, 224	pncand 9943	. . . . . . . . . 10 |- ( ph -> ( ( X + ( Z ` X ) ) - ( Z ` X ) ) = X )
226	222, 225	eqtrd 2508	. . . . . . . . 9 |- ( ph -> ( ( E ` X ) - ( Z ` X ) ) = X )
227	226	3ad2ant1 1017	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( E ` X ) - ( Z ` X ) ) = X )
228	221, 227	breqtrd 4477	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < X )
229		simpl 457	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ph )
230		elioore 11571	. . . . . . . . . . . . 13 |- ( y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) -> y e. RR )
231	230	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. RR )
232	140	oveq2d 6311	. . . . . . . . . . . . . . 15 |- ( ph -> ( y + ( Z ` X ) ) = ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
233	138	recnd 9634	. . . . . . . . . . . . . . . 16 |- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. CC )
234	55	recnd 9634	. . . . . . . . . . . . . . . 16 |- ( ph -> T e. CC )
235	233, 234	mulneg1d 10021	. . . . . . . . . . . . . . 15 |- ( ph -> ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
236	232, 235	oveq12d 6313	. . . . . . . . . . . . . 14 |- ( ph -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = ( ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) + -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
237	236	adantr 465	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
238		simpr 461	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. RR ) -> y e. RR )
239	139	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. RR ) -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
240	238, 239	readdcld 9635	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. RR ) -> ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. RR )
241	240	recnd 9634	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. RR ) -> ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. CC )
242	239	recnd 9634	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. RR ) -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. CC )
243	241, 242	negsubd 9948	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
244	238	recnd 9634	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. RR ) -> y e. CC )
245	244, 242	pncand 9943	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> ( ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = y )
246	237, 243, 245	3eqtrrd 2513	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> y = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
247	229, 231, 246	syl2anc 661	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
248	247	3ad2antl1 1158	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
249		simpl1 999	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ph )
250		fourierdlem41.qssd	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
251	250	3adant3 1016	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
252	251	adantr 465	. . . . . . . . . . . 12 |- ( ( ( 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 )
253	212	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) e. RR* )
254	217	adantr 465	. . . . . . . . . . . . 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* )
255	141	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. RR )
256	231, 255	readdcld 9635	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. RR )
257	256	3ad2antl1 1158	. . . . . . . . . . . . 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. RR )
258	141	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Z ` X ) e. RR )
259	207, 258	resubcld 9999	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR )
260	259	rexrd 9655	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
261	260	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
262	77	rexrd 9655	. . . . . . . . . . . . . . . . 17 |- ( ph -> X e. RR* )
263	262	ad2antrr 725	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> X e. RR* )
264		simpr 461	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
265		ioogtlb 31415	. . . . . . . . . . . . . . . 16 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < y )
266	261, 263, 264, 265	syl3anc 1228	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < y )
267	207	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) e. RR )
268	255	adantlr 714	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. RR )
269	230	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. RR )
270	267, 268, 269	ltsubaddd 10160	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) < y <-> ( Q ` i ) < ( y + ( Z ` X ) ) ) )
271	266, 270	mpbid 210	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) < ( y + ( Z ` X ) ) )
272	271	3adantl3 1154	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
273	249, 144	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( E ` X ) e. RR )
274	215	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` ( i + 1 ) ) e. RR )
275	274	3adantl3 1154	. . . . . . . . . . . . . 14 |- ( ( ( 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 )
276	77	ad2antrr 725	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> X e. RR )
277		iooltub 31435	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) e. RR* /\ X e. RR* /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y < X )
278	261, 263, 264, 277	syl3anc 1228	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y < X )
279	269, 276, 268, 278	ltadd1dd 10175	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( X + ( Z ` X ) ) )
280	143	eqcomd 2475	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( X + ( Z ` X ) ) = ( E ` X ) )
281	280	ad2antrr 725	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( X + ( Z ` X ) ) = ( E ` X ) )
282	279, 281	breqtrd 4477	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( E ` X ) )
283	282	3adantl3 1154	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
284		iocleub 31423	. . . . . . . . . . . . . . . 16 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
285	212, 217, 218, 284	syl3anc 1228	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
286	285	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) )
287	257, 273, 275, 283, 286	ltletrd 9753	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
288	253, 254, 257, 272, 287	eliood 31418	. . . . . . . . . . . 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. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
289	252, 288	sseldd 3510	. . . . . . . . . . 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. D )
290	249, 136	syl 16	. . . . . . . . . . . . 13 |- ( ( ( 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 )
291	290	flcld 11915	. . . . . . . . . . . 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. ZZ )
292	291	znegcld 10980	. . . . . . . . . . 11 |- ( ( ( 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 )
293		negex 9830	. . . . . . . . . . . 12 |- -u ( |_ ` ( ( B - X ) / T ) ) e. _V
294		eleq1 2539	. . . . . . . . . . . . . . 15 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( k e. ZZ <-> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
295	294	3anbi3d 1305	. . . . . . . . . . . . . 14 |- ( 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 ) ) )
296		oveq1 6302	. . . . . . . . . . . . . . . 16 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( k x. T ) = ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) )
297	296	oveq2d 6311	. . . . . . . . . . . . . . 15 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
298	297	eleq1d 2536	. . . . . . . . . . . . . 14 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D <-> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D ) )
299	295, 298	imbi12d 320	. . . . . . . . . . . . 13 |- ( 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 ) ) )
300		ovex 6320	. . . . . . . . . . . . . 14 |- ( y + ( Z ` X ) ) e. _V
301		eleq1 2539	. . . . . . . . . . . . . . . . 17 |- ( x = ( y + ( Z ` X ) ) -> ( x e. D <-> ( y + ( Z ` X ) ) e. D ) )
302	301	3anbi2d 1304	. . . . . . . . . . . . . . . 16 |- ( x = ( y + ( Z ` X ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) ) )
303		oveq1 6302	. . . . . . . . . . . . . . . . 17 |- ( x = ( y + ( Z ` X ) ) -> ( x + ( k x. T ) ) = ( ( y + ( Z ` X ) ) + ( k x. T ) ) )
304	303	eleq1d 2536	. . . . . . . . . . . . . . . 16 |- ( x = ( y + ( Z ` X ) ) -> ( ( x + ( k x. T ) ) e. D <-> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) )
305	302, 304	imbi12d 320	. . . . . . . . . . . . . . 15 |- ( 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 ) ) )
306		fourierdlem41.dper	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. D /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. D )
307	305, 306	vtoclg 3176	. . . . . . . . . . . . . 14 |- ( ( y + ( Z ` X ) ) e. _V -> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) )
308	300, 307	ax-mp 5	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D )
309	299, 308	vtoclg 3176	. . . . . . . . . . . 12 |- ( -u ( |_ ` ( ( B - X ) / T ) ) e. _V -> ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D ) )
310	293, 309	ax-mp 5	. . . . . . . . . . 11 |- ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. D )
311	249, 289, 292, 310	syl3anc 1228	. . . . . . . . . 10 |- ( ( ( 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 )
312	248, 311	eqeltrd 2555	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. D )
313	312	ralrimiva 2881	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> A. y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) y e. D )
314		dfss3 3499	. . . . . . . 8 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D <-> A. y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) y e. D )
315	313, 314	sylibr 212	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D )
316	228, 315	jca 532	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) < X /\ ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D ) )
317		breq1 4456	. . . . . . . 8 |- ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( y < X <-> ( ( Q ` i ) - ( Z ` X ) ) < X ) )
318		oveq1 6302	. . . . . . . . 9 |- ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( y (,) X ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
319	318	sseq1d 3536	. . . . . . . 8 |- ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( ( y (,) X ) C_ D <-> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D ) )
320	317, 319	anbi12d 710	. . . . . . 7 |- ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( ( y < X /\ ( y (,) X ) C_ D ) <-> ( ( ( Q ` i ) - ( Z ` X ) ) < X /\ ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D ) ) )
321	320	rspcev 3219	. . . . . 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 ) )
322	210, 316, 321	syl2anc 661	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) )
323	322	3exp 1195	. . . 4 |- ( ph -> ( i e. ( 0..^ M ) -> ( ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) -> E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) ) ) )
324	323	rexlimdv 2957	. . 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 ) ) )
325	203, 324	mpd 15	. 2 |- ( ph -> E. y e. RR ( y < X /\ ( y (,) X ) C_ D ) )
326		0zd 10888	. . . . . . . . . 10 |- ( ph -> 0 e. ZZ )
327	3	nnzd 10977	. . . . . . . . . 10 |- ( ph -> M e. ZZ )
328		1zzd 10907	. . . . . . . . . 10 |- ( ph -> 1 e. ZZ )
329	326, 327, 328	3jca 1176	. . . . . . . . 9 |- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) )
330		0le1 10088	. . . . . . . . . 10 |- 0 <_ 1
331	330	a1i 11	. . . . . . . . 9 |- ( ph -> 0 <_ 1 )
332	3	nnge1d 10590	. . . . . . . . 9 |- ( ph -> 1 <_ M )
333	329, 331, 332	jca32 535	. . . . . . . 8 |- ( ph -> ( ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) /\ ( 0 <_ 1 /\ 1 <_ M ) ) )
334		elfz2 11691	. . . . . . . 8 |- ( 1 e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) /\ ( 0 <_ 1 /\ 1 <_ M ) ) )
335	333, 334	sylibr 212	. . . . . . 7 |- ( ph -> 1 e. ( 0 ... M ) )
336	106, 335	ffvelrnd 6033	. . . . . 6 |- ( ph -> ( Q ` 1 ) e. RR )
337	141, 55	resubcld 9999	. . . . . 6 |- ( ph -> ( ( Z ` X ) - T ) e. RR )
338	336, 337	resubcld 9999	. . . . 5 |- ( ph -> ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR )
339	338	adantr 465	. . . 4 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR )
340	34	adantr 465	. . . . . . . . 9 |- ( ( ph /\ ( E ` X ) = B ) -> ( Q ` 0 ) = A )
341	46	oveq2i 6306	. . . . . . . . . . . . 13 |- ( A + T ) = ( A + ( B - A ) )
342	341	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ ( E ` X ) = B ) -> ( A + T ) = ( A + ( B - A ) ) )
343	41	recnd 9634	. . . . . . . . . . . . . 14 |- ( ph -> A e. CC )
344	43	recnd 9634	. . . . . . . . . . . . . 14 |- ( ph -> B e. CC )
345	343, 344	pncan3d 9945	. . . . . . . . . . . . 13 |- ( ph -> ( A + ( B - A ) ) = B )
346	345	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( E ` X ) = B ) -> ( A + ( B - A ) ) = B )
347		id 22	. . . . . . . . . . . . . 14 |- ( ( E ` X ) = B -> ( E ` X ) = B )
348	347	eqcomd 2475	. . . . . . . . . . . . 13 |- ( ( E ` X ) = B -> B = ( E ` X ) )
349	348	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ ( E ` X ) = B ) -> B = ( E ` X ) )
350	342, 346, 349	3eqtrrd 2513	. . . . . . . . . . 11 |- ( ( ph /\ ( E ` X ) = B ) -> ( E ` X ) = ( A + T ) )
351	350	oveq1d 6310	. . . . . . . . . 10 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( E ` X ) - T ) = ( ( A + T ) - T ) )
352	343, 234	pncand 9943	. . . . . . . . . . 11 |- ( ph -> ( ( A + T ) - T ) = A )
353	352	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( A + T ) - T ) = A )
354	351, 353	eqtr2d 2509	. . . . . . . . 9 |- ( ( ph /\ ( E ` X ) = B ) -> A = ( ( E ` X ) - T ) )
355		eqidd 2468	. . . . . . . . 9 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( E ` X ) - T ) = ( ( E ` X ) - T ) )
356	340, 354, 355	3eqtrd 2512	. . . . . . . 8 |- ( ( ph /\ ( E ` X ) = B ) -> ( Q ` 0 ) = ( ( E ` X ) - T ) )
357	356	oveq1d 6310	. . . . . . 7 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) = ( ( ( E ` X ) - T ) - ( ( Z ` X ) - T ) ) )
358	144	recnd 9634	. . . . . . . . 9 |- ( ph -> ( E ` X ) e. CC )
359	358, 224, 234	nnncan2d 9977	. . . . . . . 8 |- ( ph -> ( ( ( E ` X ) - T ) - ( ( Z ` X ) - T ) ) = ( ( E ` X ) - ( Z ` X ) ) )
360	359	adantr 465	. . . . . . 7 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( ( E ` X ) - T ) - ( ( Z ` X ) - T ) ) = ( ( E ` X ) - ( Z ` X ) ) )
361	226	adantr 465	. . . . . . 7 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( E ` X ) - ( Z ` X ) ) = X )
362	357, 360, 361	3eqtrrd 2513	. . . . . 6 |- ( ( ph /\ ( E ` X ) = B ) -> X = ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) )
363	34, 41	eqeltrd 2555	. . . . . . . 8 |- ( ph -> ( Q ` 0 ) e. RR )
364		id 22	. . . . . . . . . 10 |- ( ph -> ph )
365	3	nngt0d 10591	. . . . . . . . . . . 12 |- ( ph -> 0 < M )
366	326, 327, 365	3jca 1176	. . . . . . . . . . 11 |- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
367		fzolb 11814	. . . . . . . . . . 11 |- ( 0 e. ( 0..^ M ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
368	366, 367	sylibr 212	. . . . . . . . . 10 |- ( ph -> 0 e. ( 0..^ M ) )
369		0re 9608	. . . . . . . . . . 11 |- 0 e. RR
370		eleq1 2539	. . . . . . . . . . . . . 14 |- ( i = 0 -> ( i e. ( 0..^ M ) <-> 0 e. ( 0..^ M ) ) )
371	370	anbi2d 703	. . . . . . . . . . . . 13 |- ( i = 0 -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ 0 e. ( 0..^ M ) ) ) )
372		fveq2 5872	. . . . . . . . . . . . . 14 |- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
373		oveq1 6302	. . . . . . . . . . . . . . 15 |- ( i = 0 -> ( i + 1 ) = ( 0 + 1 ) )
374	373	fveq2d 5876	. . . . . . . . . . . . . 14 |- ( i = 0 -> ( Q ` ( i + 1 ) ) = ( Q ` ( 0 + 1 ) ) )
375	372, 374	breq12d 4466	. . . . . . . . . . . . 13 |- ( i = 0 -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
376	371, 375	imbi12d 320	. . . . . . . . . . . 12 |- ( i = 0 -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ 0 e. ( 0..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) ) )
377	376, 157	vtoclg 3176	. . . . . . . . . . 11 |- ( 0 e. RR -> ( ( ph /\ 0 e. ( 0..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
378	369, 377	ax-mp 5	. . . . . . . . . 10 |- ( ( ph /\ 0 e. ( 0..^ M ) ) -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
379	364, 368, 378	syl2anc 661	. . . . . . . . 9 |- ( ph -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
380		0p1e1 10659	. . . . . . . . . . 11 |- ( 0 + 1 ) = 1
381	380	fveq2i 5875	. . . . . . . . . 10 |- ( Q ` ( 0 + 1 ) ) = ( Q ` 1 )
382	381	a1i 11	. . . . . . . . 9 |- ( ph -> ( Q ` ( 0 + 1 ) ) = ( Q ` 1 ) )
383	379, 382	breqtrd 4477	. . . . . . . 8 |- ( ph -> ( Q ` 0 ) < ( Q ` 1 ) )
384	363, 336, 337, 383	ltsub1dd 10176	. . . . . . 7 |- ( ph -> ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
385	384	adantr 465	. . . . . 6 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
386	362, 385	eqbrtrd 4473	. . . . 5 |- ( ( ph /\ ( E ` X ) = B ) -> X < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
387		simpl 457	. . . . . . . . . 10 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ph )
388		elioore 11571	. . . . . . . . . . 11 |- ( y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) -> y e. RR )
389	388	adantl 466	. . . . . . . . . 10 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y e. RR )
390	233	negcld 9929	. . . . . . . . . . . . . . 15 |- ( ph -> -u ( |_ ` ( ( B - X ) / T ) ) e. CC )
391		1cnd 9624	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. CC )
392	390, 391, 234	adddird 9633	. . . . . . . . . . . . . 14 |- ( ph -> ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) = ( ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) + ( 1 x. T ) ) )
393	140	eqcomd 2475	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) = ( Z ` X ) )
394	393	negeqd 9826	. . . . . . . . . . . . . . . 16 |- ( ph -> -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( Z ` X ) )
395	235, 394	eqtrd 2508	. . . . . . . . . . . . . . 15 |- ( ph -> ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( Z ` X ) )
396	234	mulid2d 9626	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 x. T ) = T )
397	395, 396	oveq12d 6313	. . . . . . . . . . . . . 14 |- ( ph -> ( ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) + ( 1 x. T ) ) = ( -u ( Z ` X ) + T ) )
398	224, 234	negsubdid 9957	. . . . . . . . . . . . . . 15 |- ( ph -> -u ( ( Z ` X ) - T ) = ( -u ( Z ` X ) + T ) )
399	398	eqcomd 2475	. . . . . . . . . . . . . 14 |- ( ph -> ( -u ( Z ` X ) + T ) = -u ( ( Z ` X ) - T ) )
400	392, 397, 399	3eqtrd 2512	. . . . . . . . . . . . 13 |- ( ph -> ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) = -u ( ( Z ` X ) - T ) )
401	400	oveq2d 6311	. . . . . . . . . . . 12 |- ( ph -> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) = ( ( y + ( ( Z ` X ) - T ) ) + -u ( ( Z ` X ) - T ) ) )
402	401	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) = ( ( y + ( ( Z ` X ) - T ) ) + -u ( ( Z ` X ) - T ) ) )
403	337	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. RR ) -> ( ( Z ` X ) - T ) e. RR )
404	238, 403	readdcld 9635	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> ( y + ( ( Z ` X ) - T ) ) e. RR )
405	404	recnd 9634	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( y + ( ( Z ` X ) - T ) ) e. CC )
406	403	recnd 9634	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( ( Z ` X ) - T ) e. CC )
407	405, 406	negsubd 9948	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( ( y + ( ( Z ` X ) - T ) ) + -u ( ( Z ` X ) - T ) ) = ( ( y + ( ( Z ` X ) - T ) ) - ( ( Z ` X ) - T ) ) )
408	244, 406	pncand 9943	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( ( y + ( ( Z ` X ) - T ) ) - ( ( Z ` X ) - T ) ) = y )
409	402, 407, 408	3eqtrrd 2513	. . . . . . . . . 10 |- ( ( ph /\ y e. RR ) -> y = ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) )
410	387, 389, 409	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y = ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) )
411	410	adantlr 714	. . . . . . . 8 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y = ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) )
412	364	ad2antrr 725	. . . . . . . . 9 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ph )
413	382	eqcomd 2475	. . . . . . . . . . . . 13 |- ( ph -> ( Q ` 1 ) = ( Q ` ( 0 + 1 ) ) )
414	413	oveq2d 6311	. . . . . . . . . . . 12 |- ( ph -> ( ( Q ` 0 ) (,) ( Q ` 1 ) ) = ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) )
415	372, 374	oveq12d 6313	. . . . . . . . . . . . . . . . 17 |- ( i = 0 -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) )
416	415	sseq1d 3536	. . . . . . . . . . . . . . . 16 |- ( i = 0 -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D <-> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D ) )
417	371, 416	imbi12d 320	. . . . . . . . . . . . . . 15 |- ( 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 ) ) )
418	417, 250	vtoclg 3176	. . . . . . . . . . . . . 14 |- ( 0 e. RR -> ( ( ph /\ 0 e. ( 0..^ M ) ) -> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D ) )
419	369, 418	ax-mp 5	. . . . . . . . . . . . 13 |- ( ( ph /\ 0 e. ( 0..^ M ) ) -> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D )
420	364, 368, 419	syl2anc 661	. . . . . . . . . . . 12 |- ( ph -> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D )
421	414, 420	eqsstrd 3543	. . . . . . . . . . 11 |- ( ph -> ( ( Q ` 0 ) (,) ( Q ` 1 ) ) C_ D )
422	421	ad2antrr 725	. . . . . . . . . 10 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( ( Q ` 0 ) (,) ( Q ` 1 ) ) C_ D )
423	34, 42	eqeltrd 2555	. . . . . . . . . . . 12 |- ( ph -> ( Q ` 0 ) e. RR* )
424	423	ad2antrr 725	. . . . . . . . . . 11 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 0 ) e. RR* )
425	336	rexrd 9655	. . . . . . . . . . . 12 |- ( ph -> ( Q ` 1 ) e. RR* )
426	425	ad2antrr 725	. . . . . . . . . . 11 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 1 ) e. RR* )
427	389, 404	syldan 470	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) e. RR )
428	427	adantlr 714	. . . . . . . . . . 11 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) e. RR )
429	358, 223, 224	subaddd 9960	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( ( E ` X ) - X ) = ( Z ` X ) <-> ( X + ( Z ` X ) ) = ( E ` X ) ) )
430	280, 429	mpbird 232	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( E ` X ) - X ) = ( Z ` X ) )
431	430	eqcomd 2475	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( Z ` X ) = ( ( E ` X ) - X ) )
432	431	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( E ` X ) = B ) -> ( Z ` X ) = ( ( E ` X ) - X ) )
433		oveq1 6302	. . . . . . . . . . . . . . . . . 18 |- ( ( E ` X ) = B ->