Theorem fourierdlem41 37298

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 459	. . . . . 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 37259	. . . . . . . . . . . 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 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 457	. . . . . . . . 9 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
9		elmapi 7478	. . . . . . . . 9 |- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
10		ffn 5714	. . . . . . . . 9 |- ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
11	8, 9, 10	3syl 18	. . . . . . . 8 |- ( ph -> Q Fn ( 0 ... M ) )
12	11	adantr 463	. . . . . . 7 |- ( ( ph /\ ( E ` X ) e. ran Q ) -> Q Fn ( 0 ... M ) )
13		fvelrnb 5896	. . . . . . 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 210	. . . . 5 |- ( ( ph /\ ( E ` X ) e. ran Q ) -> E. j e. ( 0 ... M ) ( Q ` j ) = ( E ` X ) )
16		0zd 10917	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 e. ZZ )
17		elfzelz 11742	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> j e. ZZ )
18	17	3ad2ant2 1019	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> j e. ZZ )
19		1zzd 10936	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 1 e. ZZ )
20	18, 19	zsubcld 11013	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ZZ )
21		simpll 752	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. 0 < j ) -> ph )
22		elfzle1 11743	. . . . . . . . . . . . . . . . . . 19 |- ( j e. ( 0 ... M ) -> 0 <_ j )
23	22	anim1i 566	. . . . . . . . . . . . . . . . . 18 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> ( 0 <_ j /\ -. 0 < j ) )
24		0red 9627	. . . . . . . . . . . . . . . . . . 19 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> 0 e. RR )
25	17	zred 11008	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. ( 0 ... M ) -> j e. RR )
26	25	adantr 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> j e. RR )
27	24, 26	eqleltd 9761	. . . . . . . . . . . . . . . . . 18 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> ( 0 = j <-> ( 0 <_ j /\ -. 0 < j ) ) )
28	23, 27	mpbird 232	. . . . . . . . . . . . . . . . 17 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> 0 = j )
29	28	eqcomd 2410	. . . . . . . . . . . . . . . 16 |- ( ( j e. ( 0 ... M ) /\ -. 0 < j ) -> j = 0 )
30	29	adantll 712	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. 0 < j ) -> j = 0 )
31		fveq2 5849	. . . . . . . . . . . . . . . 16 |- ( j = 0 -> ( Q ` j ) = ( Q ` 0 ) )
32	7	simprld 757	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
33	32	simpld 457	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Q ` 0 ) = A )
34	31, 33	sylan9eqr 2465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j = 0 ) -> ( Q ` j ) = A )
35	21, 30, 34	syl2anc 659	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... M ) ) /\ -. 0 < j ) -> ( Q ` j ) = A )
36	35	3adantl3 1155	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> ( Q ` j ) = A )
37		simpr 459	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
38		fourierdlem41.a	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A e. RR )
39	38	rexrd 9673	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> A e. RR* )
40		fourierdlem41.b	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> B e. RR )
41	40	rexrd 9673	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> B e. RR* )
42		fourierdlem41.altb	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> A < B )
43		fourierdlem41.t	. . . . . . . . . . . . . . . . . . . . . . 23 |- T = ( B - A )
44		eqid 2402	. . . . . . . . . . . . . . . . . . . . . . 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 37261	. . . . . . . . . . . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ x e. RR ) -> x e. RR )
49	40	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ x e. RR ) -> B e. RR )
50	49, 48	resubcld 10028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ x e. RR ) -> ( B - x ) e. RR )
51	40, 38	resubcld 10028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> ( B - A ) e. RR )
52	43, 51	syl5eqel 2494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ph -> T e. RR )
53	52	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ x e. RR ) -> T e. RR )
54		0red 9627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> 0 e. RR )
55	38, 40	posdifd 10179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
56	42, 55	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> 0 < ( B - A ) )
57	43	eqcomi 2415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( B - A ) = T
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> ( B - A ) = T )
59	56, 58	breqtrd 4419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> 0 < T )
60	54, 59	gtned 9752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ph -> T =/= 0 )
61	60	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ x e. RR ) -> T =/= 0 )
62	50, 53, 61	redivcld 10413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ x e. RR ) -> ( ( B - x ) / T ) e. RR )
63	62	flcld 11972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ x e. RR ) -> ( |_ ` ( ( B - x ) / T ) ) e. ZZ )
64	63	zred 11008	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ x e. RR ) -> ( |_ ` ( ( B - x ) / T ) ) e. RR )
65	64, 53	remulcld 9654	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5941	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. RR /\ ( ( |_ ` ( ( B - x ) / T ) ) x. T ) e. RR ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
68	48, 65, 67	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ x e. RR ) -> ( Z ` x ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
69	68	oveq2d 6294	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ x e. RR ) -> ( x + ( Z ` x ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
70	69	mpteq2dva 4481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( x e. RR |-> ( x + ( Z ` x ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
71	47, 70	eqtrd 2443	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) )
72	71	feq1d 5700	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( E : RR --> ( A (,] B ) <-> ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) : RR --> ( A (,] B ) ) )
73	45, 72	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> E : RR --> ( A (,] B ) )
74		fourierdlem41.x	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> X e. RR )
75	73, 74	ffvelrnd 6010	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( E ` X ) e. ( A (,] B ) )
76		iocgtlb 36904	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. RR* /\ B e. RR* /\ ( E ` X ) e. ( A (,] B ) ) -> A < ( E ` X ) )
77	39, 41, 75, 76	syl3anc 1230	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A < ( E ` X ) )
78	38, 77	gtned 9752	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( E ` X ) =/= A )
79	78	adantr 463	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) =/= A )
80	37, 79	eqnetrd 2696	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) =/= A )
81	80	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> ( Q ` j ) =/= A )
82	81	3adantl2 1154	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> ( Q ` j ) =/= A )
83	82	neneqd 2605	. . . . . . . . . . . . 13 |- ( ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) /\ -. 0 < j ) -> -. ( Q ` j ) = A )
84	36, 83	condan 795	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 < j )
85		zltlem1 10957	. . . . . . . . . . . . 13 |- ( ( 0 e. ZZ /\ j e. ZZ ) -> ( 0 < j <-> 0 <_ ( j - 1 ) ) )
86	16, 18, 85	syl2anc 659	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( 0 < j <-> 0 <_ ( j - 1 ) ) )
87	84, 86	mpbid 210	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> 0 <_ ( j - 1 ) )
88		eluz2 11133	. . . . . . . . . . 11 |- ( ( j - 1 ) e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ ( j - 1 ) e. ZZ /\ 0 <_ ( j - 1 ) ) )
89	16, 20, 87, 88	syl3anbrc 1181	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( ZZ>= ` 0 ) )
90		elfzel2 11740	. . . . . . . . . . 11 |- ( j e. ( 0 ... M ) -> M e. ZZ )
91	90	3ad2ant2 1019	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> M e. ZZ )
92		1red 9641	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> 1 e. RR )
93	25, 92	resubcld 10028	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> ( j - 1 ) e. RR )
94	90	zred 11008	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> M e. RR )
95	25	ltm1d 10518	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> ( j - 1 ) < j )
96		elfzle2 11744	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> j <_ M )
97	93, 25, 94, 95, 96	ltletrd 9776	. . . . . . . . . . 11 |- ( j e. ( 0 ... M ) -> ( j - 1 ) < M )
98	97	3ad2ant2 1019	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) < M )
99		elfzo2 11862	. . . . . . . . . 10 |- ( ( j - 1 ) e. ( 0..^ M ) <-> ( ( j - 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( j - 1 ) < M ) )
100	89, 91, 98, 99	syl3anbrc 1181	. . . . . . . . 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 1018	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> Q : ( 0 ... M ) --> RR )
103	16, 91, 20	3jca 1177	. . . . . . . . . . . . . 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 9765	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... M ) -> ( j - 1 ) <_ M )
105	104	3ad2ant2 1019	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) <_ M )
106	103, 87, 105	jca32 533	. . . . . . . . . . . . 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 11733	. . . . . . . . . . . . 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 212	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( j - 1 ) e. ( 0 ... M ) )
109	102, 108	ffvelrnd 6010	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR )
110	109	rexrd 9673	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) e. RR* )
111	25	recnd 9652	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... M ) -> j e. CC )
112		1cnd 9642	. . . . . . . . . . . . . . 15 |- ( j e. ( 0 ... M ) -> 1 e. CC )
113	111, 112	npcand 9971	. . . . . . . . . . . . . 14 |- ( j e. ( 0 ... M ) -> ( ( j - 1 ) + 1 ) = j )
114	113	fveq2d 5853	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
115	114	adantl 464	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
116	101	ffvelrnda 6009	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR )
117	116	rexrd 9673	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR* )
118	115, 117	eqeltrd 2490	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) e. RR* )
119	118	3adant3 1017	. . . . . . . . . 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 5849	. . . . . . . . . . . . . . . 16 |- ( x = X -> ( Z ` x ) = ( Z ` X ) )
122	120, 121	oveq12d 6296	. . . . . . . . . . . . . . 15 |- ( x = X -> ( x + ( Z ` x ) ) = ( X + ( Z ` X ) ) )
123	122	adantl 464	. . . . . . . . . . . . . 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 6286	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = X -> ( B - x ) = ( B - X ) )
126	125	oveq1d 6293	. . . . . . . . . . . . . . . . . . . 20 |- ( x = X -> ( ( B - x ) / T ) = ( ( B - X ) / T ) )
127	126	fveq2d 5853	. . . . . . . . . . . . . . . . . . 19 |- ( x = X -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - X ) / T ) ) )
128	127	oveq1d 6293	. . . . . . . . . . . . . . . . . 18 |- ( x = X -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
129	128	adantl 464	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x = X ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
130	40, 74	resubcld 10028	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( B - X ) e. RR )
131	130, 52, 60	redivcld 10413	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( B - X ) / T ) e. RR )
132	131	flcld 11972	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. ZZ )
133	132	zred 11008	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. RR )
134	133, 52	remulcld 9654	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
135	124, 129, 74, 134	fvmptd 5938	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Z ` X ) = ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
136	135, 134	eqeltrd 2490	. . . . . . . . . . . . . . 15 |- ( ph -> ( Z ` X ) e. RR )
137	74, 136	readdcld 9653	. . . . . . . . . . . . . 14 |- ( ph -> ( X + ( Z ` X ) ) e. RR )
138	47, 123, 74, 137	fvmptd 5938	. . . . . . . . . . . . 13 |- ( ph -> ( E ` X ) = ( X + ( Z ` X ) ) )
139	138, 137	eqeltrd 2490	. . . . . . . . . . . 12 |- ( ph -> ( E ` X ) e. RR )
140	139	rexrd 9673	. . . . . . . . . . 11 |- ( ph -> ( E ` X ) e. RR* )
141	140	3ad2ant1 1018	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. RR* )
142		simp1 997	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ph )
143		ovex 6306	. . . . . . . . . . . . . 14 |- ( j - 1 ) e. _V
144		eleq1 2474	. . . . . . . . . . . . . . . 16 |- ( i = ( j - 1 ) -> ( i e. ( 0..^ M ) <-> ( j - 1 ) e. ( 0..^ M ) ) )
145	144	anbi2d 702	. . . . . . . . . . . . . . 15 |- ( i = ( j - 1 ) -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) ) )
146		fveq2 5849	. . . . . . . . . . . . . . . 16 |- ( i = ( j - 1 ) -> ( Q ` i ) = ( Q ` ( j - 1 ) ) )
147		oveq1 6285	. . . . . . . . . . . . . . . . 17 |- ( i = ( j - 1 ) -> ( i + 1 ) = ( ( j - 1 ) + 1 ) )
148	147	fveq2d 5853	. . . . . . . . . . . . . . . 16 |- ( i = ( j - 1 ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
149	146, 148	breq12d 4408	. . . . . . . . . . . . . . 15 |- ( i = ( j - 1 ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) ) )
150	145, 149	imbi12d 318	. . . . . . . . . . . . . 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 759	. . . . . . . . . . . . . . 15 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
152	151	r19.21bi 2773	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
153	143, 150, 152	vtocl 3111	. . . . . . . . . . . . 13 |- ( ( ph /\ ( j - 1 ) e. ( 0..^ M ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
154	142, 100, 153	syl2anc 659	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` ( ( j - 1 ) + 1 ) ) )
155	114	3ad2ant2 1019	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( ( j - 1 ) + 1 ) ) = ( Q ` j ) )
156	154, 155	breqtrd 4419	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( Q ` j ) )
157		simp3 999	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( E ` X ) )
158	156, 157	breqtrd 4419	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` ( j - 1 ) ) < ( E ` X ) )
159	139	leidd 10159	. . . . . . . . . . . . . 14 |- ( ph -> ( E ` X ) <_ ( E ` X ) )
160	159	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( E ` X ) )
161	37	eqcomd 2410	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) = ( Q ` j ) )
162	160, 161	breqtrd 4419	. . . . . . . . . . . 12 |- ( ( ph /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
163	162	3adant2 1016	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` j ) )
164	113	eqcomd 2410	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... M ) -> j = ( ( j - 1 ) + 1 ) )
165	164	fveq2d 5853	. . . . . . . . . . . 12 |- ( j e. ( 0 ... M ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
166	165	3ad2ant2 1019	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( Q ` j ) = ( Q ` ( ( j - 1 ) + 1 ) ) )
167	163, 166	breqtrd 4419	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) <_ ( Q ` ( ( j - 1 ) + 1 ) ) )
168	110, 119, 141, 158, 167	eliocd 36911	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = ( E ` X ) ) -> ( E ` X ) e. ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
169	146, 148	oveq12d 6296	. . . . . . . . . . 11 |- ( i = ( j - 1 ) -> ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) = ( ( Q ` ( j - 1 ) ) (,] ( Q ` ( ( j - 1 ) + 1 ) ) ) )
170	169	eleq2d 2472	. . . . . . . . . 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 3160	. . . . . . . . 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 659	. . . . . . . 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 1196	. . . . . . 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 463	. . . . . 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 2894	. . . . 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 463	. . . . . 6 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> M e. NN )
178	101	adantr 463	. . . . . 6 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> Q : ( 0 ... M ) --> RR )
179		iocssicc 11666	. . . . . . . 8 |- ( ( Q ` 0 ) (,] ( Q ` M ) ) C_ ( ( Q ` 0 ) [,] ( Q ` M ) )
180	32	simprd 461	. . . . . . . . . 10 |- ( ph -> ( Q ` M ) = B )
181	33, 180	oveq12d 6296	. . . . . . . . 9 |- ( ph -> ( ( Q ` 0 ) (,] ( Q ` M ) ) = ( A (,] B ) )
182	75, 181	eleqtrrd 2493	. . . . . . . 8 |- ( ph -> ( E ` X ) e. ( ( Q ` 0 ) (,] ( Q ` M ) ) )
183	179, 182	sseldi 3440	. . . . . . 7 |- ( ph -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
184	183	adantr 463	. . . . . 6 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> ( E ` X ) e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
185		simpr 459	. . . . . 6 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> -. ( E ` X ) e. ran Q )
186		fveq2 5849	. . . . . . . . 9 |- ( k = j -> ( Q ` k ) = ( Q ` j ) )
187	186	breq1d 4405	. . . . . . . 8 |- ( k = j -> ( ( Q ` k ) < ( E ` X ) <-> ( Q ` j ) < ( E ` X ) ) )
188	187	cbvrabv 3058	. . . . . . 7 |- { k e. ( 0..^ M ) | ( Q ` k ) < ( E ` X ) } = { j e. ( 0..^ M ) | ( Q ` j ) < ( E ` X ) }
189	188	supeq1i 7940	. . . . . 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 37282	. . . . 5 |- ( ( ph /\ -. ( E ` X ) e. ran Q ) -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
191		ioossioc 36893	. . . . . . . 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 3441	. . . . . 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 2879	. . . . 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 792	. . 3 |- ( ph -> E. i e. ( 0..^ M ) ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
197	101	adantr 463	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
198		elfzofz 11874	. . . . . . . . . 10 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
199	198	adantl 464	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
200	197, 199	ffvelrnd 6010	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
201	200	3adant3 1017	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
202	136	3ad2ant1 1018	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Z ` X ) e. RR )
203	201, 202	resubcld 10028	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR )
204	139	3ad2ant1 1018	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. RR )
205	201	rexrd 9673	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
206		fzofzp1 11946	. . . . . . . . . . . . 13 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
207	206	adantl 464	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
208	197, 207	ffvelrnd 6010	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
209	208	rexrd 9673	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
210	209	3adant3 1017	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
211		simp3 999	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) )
212		iocgtlb 36904	. . . . . . . . 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 1230	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( E ` X ) )
214	201, 204, 202, 213	ltsub1dd 10204	. . . . . . 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 6293	. . . . . . . . 9 |- ( ph -> ( ( E ` X ) - ( Z ` X ) ) = ( ( X + ( Z ` X ) ) - ( Z ` X ) ) )
216	74	recnd 9652	. . . . . . . . . 10 |- ( ph -> X e. CC )
217	136	recnd 9652	. . . . . . . . . 10 |- ( ph -> ( Z ` X ) e. CC )
218	216, 217	pncand 9968	. . . . . . . . 9 |- ( ph -> ( ( X + ( Z ` X ) ) - ( Z ` X ) ) = X )
219	215, 218	eqtrd 2443	. . . . . . . 8 |- ( ph -> ( ( E ` X ) - ( Z ` X ) ) = X )
220	219	3ad2ant1 1018	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( E ` X ) - ( Z ` X ) ) = X )
221	214, 220	breqtrd 4419	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < X )
222		elioore 11612	. . . . . . . . . . 11 |- ( y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) -> y e. RR )
223	135	oveq2d 6294	. . . . . . . . . . . . . 14 |- ( ph -> ( y + ( Z ` X ) ) = ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
224	133	recnd 9652	. . . . . . . . . . . . . . 15 |- ( ph -> ( |_ ` ( ( B - X ) / T ) ) e. CC )
225	52	recnd 9652	. . . . . . . . . . . . . . 15 |- ( ph -> T e. CC )
226	224, 225	mulneg1d 10050	. . . . . . . . . . . . . 14 |- ( ph -> ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) )
227	223, 226	oveq12d 6296	. . . . . . . . . . . . 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 463	. . . . . . . . . . . 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 459	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. RR ) -> y e. RR )
230	134	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. RR ) -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. RR )
231	229, 230	readdcld 9653	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. RR ) -> ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. RR )
232	231	recnd 9652	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) e. CC )
233	230	recnd 9652	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) e. CC )
234	232, 233	negsubd 9973	. . . . . . . . . . . 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 9652	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> y e. CC )
236	235, 233	pncand 9968	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( ( y + ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) - ( ( |_ ` ( ( B - X ) / T ) ) x. T ) ) = y )
237	228, 234, 236	3eqtrrd 2448	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> y = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
238	222, 237	sylan2 472	. . . . . . . . . 10 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
239	238	3ad2antl1 1159	. . . . . . . . 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 1000	. . . . . . . . . 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 1017	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D )
243	242	adantr 463	. . . . . . . . . . 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 463	. . . . . . . . . . . 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 463	. . . . . . . . . . . 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 464	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. RR )
247	136	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. RR )
248	246, 247	readdcld 9653	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) e. RR )
249	248	3ad2antl1 1159	. . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Z ` X ) e. RR )
251	200, 250	resubcld 10028	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR )
252	251	rexrd 9673	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
253	252	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) e. RR* )
254	74	rexrd 9673	. . . . . . . . . . . . . . . 16 |- ( ph -> X e. RR* )
255	254	ad2antrr 724	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> X e. RR* )
256		simpr 459	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
257		ioogtlb 36897	. . . . . . . . . . . . . . 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 1230	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( ( Q ` i ) - ( Z ` X ) ) < y )
259	200	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) e. RR )
260	136	ad2antrr 724	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Z ` X ) e. RR )
261	222	adantl 464	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y e. RR )
262	259, 260, 261	ltsubaddd 10188	. . . . . . . . . . . . . 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 210	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` i ) < ( y + ( Z ` X ) ) )
264	263	3adantl3 1155	. . . . . . . . . . . 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 463	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( Q ` ( i + 1 ) ) e. RR )
267	266	3adantl3 1155	. . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> X e. RR )
269		iooltub 36916	. . . . . . . . . . . . . . . . 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 1230	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> y < X )
271	261, 268, 260, 270	ltadd1dd 10203	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( X + ( Z ` X ) ) )
272	138	eqcomd 2410	. . . . . . . . . . . . . . . 16 |- ( ph -> ( X + ( Z ` X ) ) = ( E ` X ) )
273	272	ad2antrr 724	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( X + ( Z ` X ) ) = ( E ` X ) )
274	271, 273	breqtrd 4419	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) ) -> ( y + ( Z ` X ) ) < ( E ` X ) )
275	274	3adantl3 1155	. . . . . . . . . . . . 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 36905	. . . . . . . . . . . . . . 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 1230	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( E ` X ) <_ ( Q ` ( i + 1 ) ) )
278	277	adantr 463	. . . . . . . . . . . . 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 9776	. . . . . . . . . . . 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 36900	. . . . . . . . . . 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 3443	. . . . . . . . . 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 11972	. . . . . . . . . . 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 11010	. . . . . . . . . 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 9854	. . . . . . . . . . 11 |- -u ( |_ ` ( ( B - X ) / T ) ) e. _V
286		eleq1 2474	. . . . . . . . . . . . 13 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( k e. ZZ <-> -u ( |_ ` ( ( B - X ) / T ) ) e. ZZ ) )
287	286	3anbi3d 1307	. . . . . . . . . . . 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 6285	. . . . . . . . . . . . . 14 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( k x. T ) = ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) )
289	288	oveq2d 6294	. . . . . . . . . . . . 13 |- ( k = -u ( |_ ` ( ( B - X ) / T ) ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) = ( ( y + ( Z ` X ) ) + ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) ) )
290	289	eleq1d 2471	. . . . . . . . . . . 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 318	. . . . . . . . . . 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 6306	. . . . . . . . . . . 12 |- ( y + ( Z ` X ) ) e. _V
293		eleq1 2474	. . . . . . . . . . . . . 14 |- ( x = ( y + ( Z ` X ) ) -> ( x e. D <-> ( y + ( Z ` X ) ) e. D ) )
294	293	3anbi2d 1306	. . . . . . . . . . . . 13 |- ( x = ( y + ( Z ` X ) ) -> ( ( ph /\ x e. D /\ k e. ZZ ) <-> ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) ) )
295		oveq1 6285	. . . . . . . . . . . . . 14 |- ( x = ( y + ( Z ` X ) ) -> ( x + ( k x. T ) ) = ( ( y + ( Z ` X ) ) + ( k x. T ) ) )
296	295	eleq1d 2471	. . . . . . . . . . . . 13 |- ( x = ( y + ( Z ` X ) ) -> ( ( x + ( k x. T ) ) e. D <-> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D ) )
297	294, 296	imbi12d 318	. . . . . . . . . . . 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 3111	. . . . . . . . . . 11 |- ( ( ph /\ ( y + ( Z ` X ) ) e. D /\ k e. ZZ ) -> ( ( y + ( Z ` X ) ) + ( k x. T ) ) e. D )
300	285, 291, 299	vtocl 3111	. . . . . . . . . 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 1230	. . . . . . . . 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 2490	. . . . . . . 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 2818	. . . . . . 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 3432	. . . . . . 7 |- ( ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D <-> A. y e. ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) y e. D )
305	303, 304	sylibr 212	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) /\ ( E ` X ) e. ( ( Q ` i ) (,] ( Q ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D )
306		breq1 4398	. . . . . . . 8 |- ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( y < X <-> ( ( Q ` i ) - ( Z ` X ) ) < X ) )
307		oveq1 6285	. . . . . . . . 9 |- ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( y (,) X ) = ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) )
308	307	sseq1d 3469	. . . . . . . 8 |- ( y = ( ( Q ` i ) - ( Z ` X ) ) -> ( ( y (,) X ) C_ D <-> ( ( ( Q ` i ) - ( Z ` X ) ) (,) X ) C_ D ) )
309	306, 308	anbi12d 709	. . . . . . 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 3160	. . . . . 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 1228	. . . . 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 1196	. . . 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 2894	. . 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 10917	. . . . . . . . . 10 |- ( ph -> 0 e. ZZ )
316	3	nnzd 11007	. . . . . . . . . 10 |- ( ph -> M e. ZZ )
317		1zzd 10936	. . . . . . . . . 10 |- ( ph -> 1 e. ZZ )
318	315, 316, 317	3jca 1177	. . . . . . . . 9 |- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) )
319		0le1 10116	. . . . . . . . . 10 |- 0 <_ 1
320	319	a1i 11	. . . . . . . . 9 |- ( ph -> 0 <_ 1 )
321	3	nnge1d 10619	. . . . . . . . 9 |- ( ph -> 1 <_ M )
322	318, 320, 321	jca32 533	. . . . . . . 8 |- ( ph -> ( ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) /\ ( 0 <_ 1 /\ 1 <_ M ) ) )
323		elfz2 11733	. . . . . . . 8 |- ( 1 e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ 1 e. ZZ ) /\ ( 0 <_ 1 /\ 1 <_ M ) ) )
324	322, 323	sylibr 212	. . . . . . 7 |- ( ph -> 1 e. ( 0 ... M ) )
325	101, 324	ffvelrnd 6010	. . . . . 6 |- ( ph -> ( Q ` 1 ) e. RR )
326	136, 52	resubcld 10028	. . . . . 6 |- ( ph -> ( ( Z ` X ) - T ) e. RR )
327	325, 326	resubcld 10028	. . . . 5 |- ( ph -> ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR )
328	327	adantr 463	. . . 4 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR )
329	38	recnd 9652	. . . . . . . . . 10 |- ( ph -> A e. CC )
330	329, 225	pncand 9968	. . . . . . . . 9 |- ( ph -> ( ( A + T ) - T ) = A )
331	330	adantr 463	. . . . . . . 8 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( A + T ) - T ) = A )
332	43	oveq2i 6289	. . . . . . . . . . 11 |- ( A + T ) = ( A + ( B - A ) )
333	332	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ ( E ` X ) = B ) -> ( A + T ) = ( A + ( B - A ) ) )
334	40	recnd 9652	. . . . . . . . . . . 12 |- ( ph -> B e. CC )
335	329, 334	pncan3d 9970	. . . . . . . . . . 11 |- ( ph -> ( A + ( B - A ) ) = B )
336	335	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ ( E ` X ) = B ) -> ( A + ( B - A ) ) = B )
337		id 22	. . . . . . . . . . . 12 |- ( ( E ` X ) = B -> ( E ` X ) = B )
338	337	eqcomd 2410	. . . . . . . . . . 11 |- ( ( E ` X ) = B -> B = ( E ` X ) )
339	338	adantl 464	. . . . . . . . . 10 |- ( ( ph /\ ( E ` X ) = B ) -> B = ( E ` X ) )
340	333, 336, 339	3eqtrrd 2448	. . . . . . . . 9 |- ( ( ph /\ ( E ` X ) = B ) -> ( E ` X ) = ( A + T ) )
341	340	oveq1d 6293	. . . . . . . 8 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( E ` X ) - T ) = ( ( A + T ) - T ) )
342	33	adantr 463	. . . . . . . 8 |- ( ( ph /\ ( E ` X ) = B ) -> ( Q ` 0 ) = A )
343	331, 341, 342	3eqtr4rd 2454	. . . . . . 7 |- ( ( ph /\ ( E ` X ) = B ) -> ( Q ` 0 ) = ( ( E ` X ) - T ) )
344	343	oveq1d 6293	. . . . . 6 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) = ( ( ( E ` X ) - T ) - ( ( Z ` X ) - T ) ) )
345	139	recnd 9652	. . . . . . . 8 |- ( ph -> ( E ` X ) e. CC )
346	345, 217, 225	nnncan2d 10002	. . . . . . 7 |- ( ph -> ( ( ( E ` X ) - T ) - ( ( Z ` X ) - T ) ) = ( ( E ` X ) - ( Z ` X ) ) )
347	346	adantr 463	. . . . . 6 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( ( E ` X ) - T ) - ( ( Z ` X ) - T ) ) = ( ( E ` X ) - ( Z ` X ) ) )
348	219	adantr 463	. . . . . 6 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( E ` X ) - ( Z ` X ) ) = X )
349	344, 347, 348	3eqtrrd 2448	. . . . 5 |- ( ( ph /\ ( E ` X ) = B ) -> X = ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) )
350	33, 38	eqeltrd 2490	. . . . . . 7 |- ( ph -> ( Q ` 0 ) e. RR )
351	3	nngt0d 10620	. . . . . . . . . 10 |- ( ph -> 0 < M )
352		fzolb 11865	. . . . . . . . . 10 |- ( 0 e. ( 0..^ M ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
353	315, 316, 351, 352	syl3anbrc 1181	. . . . . . . . 9 |- ( ph -> 0 e. ( 0..^ M ) )
354		0re 9626	. . . . . . . . . 10 |- 0 e. RR
355		eleq1 2474	. . . . . . . . . . . . 13 |- ( i = 0 -> ( i e. ( 0..^ M ) <-> 0 e. ( 0..^ M ) ) )
356	355	anbi2d 702	. . . . . . . . . . . 12 |- ( i = 0 -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ 0 e. ( 0..^ M ) ) ) )
357		fveq2 5849	. . . . . . . . . . . . 13 |- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
358		oveq1 6285	. . . . . . . . . . . . . 14 |- ( i = 0 -> ( i + 1 ) = ( 0 + 1 ) )
359	358	fveq2d 5853	. . . . . . . . . . . . 13 |- ( i = 0 -> ( Q ` ( i + 1 ) ) = ( Q ` ( 0 + 1 ) ) )
360	357, 359	breq12d 4408	. . . . . . . . . . . 12 |- ( i = 0 -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) ) )
361	356, 360	imbi12d 318	. . . . . . . . . . 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 3117	. . . . . . . . . 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 666	. . . . . . . 8 |- ( ph -> ( Q ` 0 ) < ( Q ` ( 0 + 1 ) ) )
365		0p1e1 10688	. . . . . . . . . 10 |- ( 0 + 1 ) = 1
366	365	fveq2i 5852	. . . . . . . . 9 |- ( Q ` ( 0 + 1 ) ) = ( Q ` 1 )
367	366	a1i 11	. . . . . . . 8 |- ( ph -> ( Q ` ( 0 + 1 ) ) = ( Q ` 1 ) )
368	364, 367	breqtrd 4419	. . . . . . 7 |- ( ph -> ( Q ` 0 ) < ( Q ` 1 ) )
369	350, 325, 326, 368	ltsub1dd 10204	. . . . . 6 |- ( ph -> ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
370	369	adantr 463	. . . . 5 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( Q ` 0 ) - ( ( Z ` X ) - T ) ) < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
371	349, 370	eqbrtrd 4415	. . . 4 |- ( ( ph /\ ( E ` X ) = B ) -> X < ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) )
372		elioore 11612	. . . . . . . . 9 |- ( y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) -> y e. RR )
373	135	eqcomd 2410	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( |_ ` ( ( B - X ) / T ) ) x. T ) = ( Z ` X ) )
374	373	negeqd 9850	. . . . . . . . . . . . . . 15 |- ( ph -> -u ( ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( Z ` X ) )
375	226, 374	eqtrd 2443	. . . . . . . . . . . . . 14 |- ( ph -> ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) = -u ( Z ` X ) )
376	225	mulid2d 9644	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 x. T ) = T )
377	375, 376	oveq12d 6296	. . . . . . . . . . . . 13 |- ( ph -> ( ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) + ( 1 x. T ) ) = ( -u ( Z ` X ) + T ) )
378	224	negcld 9954	. . . . . . . . . . . . . 14 |- ( ph -> -u ( |_ ` ( ( B - X ) / T ) ) e. CC )
379		1cnd 9642	. . . . . . . . . . . . . 14 |- ( ph -> 1 e. CC )
380	378, 379, 225	adddird 9651	. . . . . . . . . . . . 13 |- ( ph -> ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) = ( ( -u ( |_ ` ( ( B - X ) / T ) ) x. T ) + ( 1 x. T ) ) )
381	217, 225	negsubdid 9982	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( Z ` X ) - T ) = ( -u ( Z ` X ) + T ) )
382	377, 380, 381	3eqtr4d 2453	. . . . . . . . . . . 12 |- ( ph -> ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) = -u ( ( Z ` X ) - T ) )
383	382	oveq2d 6294	. . . . . . . . . . 11 |- ( ph -> ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) = ( ( y + ( ( Z ` X ) - T ) ) + -u ( ( Z ` X ) - T ) ) )
384	383	adantr 463	. . . . . . . . . 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 463	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> ( ( Z ` X ) - T ) e. RR )
386	229, 385	readdcld 9653	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( y + ( ( Z ` X ) - T ) ) e. RR )
387	386	recnd 9652	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( y + ( ( Z ` X ) - T ) ) e. CC )
388	385	recnd 9652	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( ( Z ` X ) - T ) e. CC )
389	387, 388	negsubd 9973	. . . . . . . . . 10 |- ( ( ph /\ y e. RR ) -> ( ( y + ( ( Z ` X ) - T ) ) + -u ( ( Z ` X ) - T ) ) = ( ( y + ( ( Z ` X ) - T ) ) - ( ( Z ` X ) - T ) ) )
390	235, 388	pncand 9968	. . . . . . . . . 10 |- ( ( ph /\ y e. RR ) -> ( ( y + ( ( Z ` X ) - T ) ) - ( ( Z ` X ) - T ) ) = y )
391	384, 389, 390	3eqtrrd 2448	. . . . . . . . 9 |- ( ( ph /\ y e. RR ) -> y = ( ( y + ( ( Z ` X ) - T ) ) + ( ( -u ( |_ ` ( ( B - X ) / T ) ) + 1 ) x. T ) ) )
392	372, 391	sylan2 472	. . . . . . . 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 713	. . . . . . 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 752	. . . . . . . 8 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ph )
395	367	eqcomd 2410	. . . . . . . . . . . 12 |- ( ph -> ( Q ` 1 ) = ( Q ` ( 0 + 1 ) ) )
396	395	oveq2d 6294	. . . . . . . . . . 11 |- ( ph -> ( ( Q ` 0 ) (,) ( Q ` 1 ) ) = ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) )
397	357, 359	oveq12d 6296	. . . . . . . . . . . . . . . 16 |- ( i = 0 -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) )
398	397	sseq1d 3469	. . . . . . . . . . . . . . 15 |- ( i = 0 -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ D <-> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D ) )
399	356, 398	imbi12d 318	. . . . . . . . . . . . . 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 3117	. . . . . . . . . . . . 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 666	. . . . . . . . . . 11 |- ( ph -> ( ( Q ` 0 ) (,) ( Q ` ( 0 + 1 ) ) ) C_ D )
403	396, 402	eqsstrd 3476	. . . . . . . . . 10 |- ( ph -> ( ( Q ` 0 ) (,) ( Q ` 1 ) ) C_ D )
404	403	ad2antrr 724	. . . . . . . . 9 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( ( Q ` 0 ) (,) ( Q ` 1 ) ) C_ D )
405	33, 39	eqeltrd 2490	. . . . . . . . . . 11 |- ( ph -> ( Q ` 0 ) e. RR* )
406	405	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 0 ) e. RR* )
407	325	rexrd 9673	. . . . . . . . . . 11 |- ( ph -> ( Q ` 1 ) e. RR* )
408	407	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 1 ) e. RR* )
409	372, 386	sylan2 472	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) e. RR )
410	409	adantlr 713	. . . . . . . . . 10 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( y + ( ( Z ` X ) - T ) ) e. RR )
411	345, 216, 217	subaddd 9985	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( E ` X ) - X ) = ( Z ` X ) <-> ( X + ( Z ` X ) ) = ( E ` X ) ) )
412	272, 411	mpbird 232	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( E ` X ) - X ) = ( Z ` X ) )
413		oveq1 6285	. . . . . . . . . . . . . . . 16 |- ( ( E ` X ) = B -> ( ( E ` X ) - X ) = ( B - X ) )
414	412, 413	sylan9req 2464	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( E ` X ) = B ) -> ( Z ` X ) = ( B - X ) )
415	414	oveq1d 6293	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( Z ` X ) - T ) = ( ( B - X ) - T ) )
416	415	oveq2d 6294	. . . . . . . . . . . . 13 |- ( ( ph /\ ( E ` X ) = B ) -> ( X + ( ( Z ` X ) - T ) ) = ( X + ( ( B - X ) - T ) ) )
417	130	recnd 9652	. . . . . . . . . . . . . . . 16 |- ( ph -> ( B - X ) e. CC )
418	216, 417, 225	addsubassd 9987	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( X + ( B - X ) ) - T ) = ( X + ( ( B - X ) - T ) ) )
419	418	eqcomd 2410	. . . . . . . . . . . . . 14 |- ( ph -> ( X + ( ( B - X ) - T ) ) = ( ( X + ( B - X ) ) - T ) )
420	419	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ ( E ` X ) = B ) -> ( X + ( ( B - X ) - T ) ) = ( ( X + ( B - X ) ) - T ) )
421	334, 225, 329	subsub23d 36847	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( B - T ) = A <-> ( B - A ) = T ) )
422	58, 421	mpbird 232	. . . . . . . . . . . . . . 15 |- ( ph -> ( B - T ) = A )
423	216, 334	pncan3d 9970	. . . . . . . . . . . . . . . 16 |- ( ph -> ( X + ( B - X ) ) = B )
424	423	oveq1d 6293	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( X + ( B - X ) ) - T ) = ( B - T ) )
425	422, 424, 33	3eqtr4d 2453	. . . . . . . . . . . . . 14 |- ( ph -> ( ( X + ( B - X ) ) - T ) = ( Q ` 0 ) )
426	425	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ ( E ` X ) = B ) -> ( ( X + ( B - X ) ) - T ) = ( Q ` 0 ) )
427	416, 420, 426	3eqtrrd 2448	. . . . . . . . . . . 12 |- ( ( ph /\ ( E ` X ) = B ) -> ( Q ` 0 ) = ( X + ( ( Z ` X ) - T ) ) )
428	427	adantr 463	. . . . . . . . . . 11 |- ( ( ( ph /\ ( E ` X ) = B ) /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( Q ` 0 ) = ( X + ( ( Z ` X ) - T ) ) )
429	74	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> X e. RR )
430	372	adantl 464	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> y e. RR )
431	326	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( ( Z ` X ) - T ) e. RR )
432	254	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> X e. RR* )
433	327	rexrd 9673	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR* )
434	433	adantr 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) ) ) -> ( ( Q ` 1 ) - ( ( Z ` X ) - T ) ) e. RR* )
435		simpr 459	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( X (,) ( ( Q ` 1 ) - ( ( Z