Theorem fourierdlem93 31823

Description: Integral by substitution (the domain is shifted by X) for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem93.1	|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` m ) = pi ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem93.2	|- H = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )
fourierdlem93.3	|- ( ph -> M e. NN )
fourierdlem93.4	|- ( ph -> Q e. ( P ` M ) )
fourierdlem93.5	|- ( ph -> X e. RR )
fourierdlem93.6	|- ( ph -> F : ( -u pi [,] pi ) --> CC )
fourierdlem93.7	|- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem93.8	|- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
fourierdlem93.9	|- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )

Assertion

Ref	Expression
fourierdlem93	|- ( ph -> S. ( -u pi [,] pi ) ( F ` t ) _d t = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + s ) ) _d s )

Distinct variable groups:   i, F, s, t   i, H, s, t   t, L   i, M, m, p   M, s, t   Q, i, p   Q, s, t   t, R   i, X, s, t   ph, i, s, t

Allowed substitution hints:   ph( m, p)   P( t, i, m, s, p)   Q( m)   R( i, m, s, p)   F( m, p)   H( m, p)   L( i, m, s, p)   X( m, p)

Proof of Theorem fourierdlem93

Dummy variables r x j are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem93.4	. . . . . . . . . . 11 |- ( ph -> Q e. ( P ` M ) )
2		fourierdlem93.3	. . . . . . . . . . . 12 |- ( ph -> M e. NN )
3		fourierdlem93.1	. . . . . . . . . . . . 13 |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u pi /\ ( p ` m ) = pi ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
4	3	fourierdlem2 31732	. . . . . . . . . . . 12 |- ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
5	2, 4	syl 16	. . . . . . . . . . 11 |- ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
6	1, 5	mpbid 210	. . . . . . . . . 10 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
7	6	simprd 463	. . . . . . . . 9 |- ( ph -> ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
8	7	simpld 459	. . . . . . . 8 |- ( ph -> ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) )
9	8	simpld 459	. . . . . . 7 |- ( ph -> ( Q ` 0 ) = -u pi )
10	8	simprd 463	. . . . . . 7 |- ( ph -> ( Q ` M ) = pi )
11	7	simprd 463	. . . . . . 7 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
12	9, 10, 11	3jca 1176	. . . . . 6 |- ( ph -> ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
13	12	simp1d 1008	. . . . 5 |- ( ph -> ( Q ` 0 ) = -u pi )
14	13	eqcomd 2475	. . . 4 |- ( ph -> -u pi = ( Q ` 0 ) )
15	12	simp2d 1009	. . . . 5 |- ( ph -> ( Q ` M ) = pi )
16	15	eqcomd 2475	. . . 4 |- ( ph -> pi = ( Q ` M ) )
17	14, 16	oveq12d 6313	. . 3 |- ( ph -> ( -u pi [,] pi ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
18		itgeq1 22047	. . 3 |- ( ( -u pi [,] pi ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) -> S. ( -u pi [,] pi ) ( F ` t ) _d t = S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( F ` t ) _d t )
19	17, 18	syl 16	. 2 |- ( ph -> S. ( -u pi [,] pi ) ( F ` t ) _d t = S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( F ` t ) _d t )
20		0z 10887	. . . 4 |- 0 e. ZZ
21	20	a1i 11	. . 3 |- ( ph -> 0 e. ZZ )
22		nnuz 11129	. . . . 5 |- NN = ( ZZ>= ` 1 )
23	2, 22	syl6eleq 2565	. . . 4 |- ( ph -> M e. ( ZZ>= ` 1 ) )
24		1e0p1 11016	. . . . . 6 |- 1 = ( 0 + 1 )
25	24	a1i 11	. . . . 5 |- ( ph -> 1 = ( 0 + 1 ) )
26	25	fveq2d 5876	. . . 4 |- ( ph -> ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) ) )
27	23, 26	eleqtrd 2557	. . 3 |- ( ph -> M e. ( ZZ>= ` ( 0 + 1 ) ) )
28	3, 2, 1	fourierdlem15 31745	. . . . 5 |- ( ph -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
29		pire 22718	. . . . . . . . 9 |- pi e. RR
30	29	renegcli 9892	. . . . . . . 8 |- -u pi e. RR
31	30, 29	pm3.2i 455	. . . . . . 7 |- ( -u pi e. RR /\ pi e. RR )
32		iccssre 11618	. . . . . . 7 |- ( ( -u pi e. RR /\ pi e. RR ) -> ( -u pi [,] pi ) C_ RR )
33	31, 32	ax-mp 5	. . . . . 6 |- ( -u pi [,] pi ) C_ RR
34	33	a1i 11	. . . . 5 |- ( ph -> ( -u pi [,] pi ) C_ RR )
35	28, 34	jca 532	. . . 4 |- ( ph -> ( Q : ( 0 ... M ) --> ( -u pi [,] pi ) /\ ( -u pi [,] pi ) C_ RR ) )
36		fss 5745	. . . 4 |- ( ( Q : ( 0 ... M ) --> ( -u pi [,] pi ) /\ ( -u pi [,] pi ) C_ RR ) -> Q : ( 0 ... M ) --> RR )
37	35, 36	syl 16	. . 3 |- ( ph -> Q : ( 0 ... M ) --> RR )
38	11	r19.21bi 2836	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
39		fourierdlem93.6	. . . . . 6 |- ( ph -> F : ( -u pi [,] pi ) --> CC )
40	39	adantr 465	. . . . 5 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> F : ( -u pi [,] pi ) --> CC )
41		simpr 461	. . . . . 6 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
42	17	eqcomd 2475	. . . . . . 7 |- ( ph -> ( ( Q ` 0 ) [,] ( Q ` M ) ) = ( -u pi [,] pi ) )
43	42	adantr 465	. . . . . 6 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( ( Q ` 0 ) [,] ( Q ` M ) ) = ( -u pi [,] pi ) )
44	41, 43	eleqtrd 2557	. . . . 5 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> t e. ( -u pi [,] pi ) )
45	40, 44	jca 532	. . . 4 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( F : ( -u pi [,] pi ) --> CC /\ t e. ( -u pi [,] pi ) ) )
46		ffvelrn 6030	. . . 4 |- ( ( F : ( -u pi [,] pi ) --> CC /\ t e. ( -u pi [,] pi ) ) -> ( F ` t ) e. CC )
47	45, 46	syl 16	. . 3 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( F ` t ) e. CC )
48		iooinlbub 31421	. . . . . . 7 |- ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) = (/)
49	48	a1i 11	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) = (/) )
50	49	fveq2d 5876	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( vol* ` ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) ) = ( vol* ` (/) ) )
51		ovol0 21772	. . . . . 6 |- ( vol* ` (/) ) = 0
52	51	a1i 11	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( vol* ` (/) ) = 0 )
53	50, 52	eqtrd 2508	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( vol* ` ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) ) = 0 )
54	37	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
55		elfzofz 11823	. . . . . . . . . . 11 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
56	55	adantl 466	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
57	54, 56	jca 532	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q : ( 0 ... M ) --> RR /\ i e. ( 0 ... M ) ) )
58		ffvelrn 6030	. . . . . . . . 9 |- ( ( Q : ( 0 ... M ) --> RR /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
59	57, 58	syl 16	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
60	59	rexrd 9655	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
61		fzofzp1 11889	. . . . . . . . . . 11 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
62	61	adantl 466	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
63	54, 62	jca 532	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q : ( 0 ... M ) --> RR /\ ( i + 1 ) e. ( 0 ... M ) ) )
64		ffvelrn 6030	. . . . . . . . 9 |- ( ( Q : ( 0 ... M ) --> RR /\ ( i + 1 ) e. ( 0 ... M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
65	63, 64	syl 16	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
66	65	rexrd 9655	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
67	59, 65, 38	ltled 9744	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) <_ ( Q ` ( i + 1 ) ) )
68	60, 66, 67	3jca 1176	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( Q ` i ) <_ ( Q ` ( i + 1 ) ) ) )
69		prunioo 11661	. . . . . 6 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( Q ` i ) <_ ( Q ` ( i + 1 ) ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) = ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
70	68, 69	syl 16	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) = ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
71	70	eqcomd 2475	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) )
72	39	ad2antrr 725	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> F : ( -u pi [,] pi ) --> CC )
73	30	rexri 9658	. . . . . . . 8 |- -u pi e. RR*
74	73	a1i 11	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> -u pi e. RR* )
75	29	rexri 9658	. . . . . . . 8 |- pi e. RR*
76	75	a1i 11	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> pi e. RR* )
77	28	ad2antrr 725	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
78		simplr 754	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0..^ M ) )
79		simpr 461	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
80	74, 76, 77, 78, 79	fourierdlem1 31731	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> t e. ( -u pi [,] pi ) )
81	72, 80	jca 532	. . . . 5 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F : ( -u pi [,] pi ) --> CC /\ t e. ( -u pi [,] pi ) ) )
82	81, 46	syl 16	. . . 4 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` t ) e. CC )
83	39	feqmptd 5927	. . . . . . . . . 10 |- ( ph -> F = ( t e. ( -u pi [,] pi ) |-> ( F ` t ) ) )
84	83	adantr 465	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F = ( t e. ( -u pi [,] pi ) |-> ( F ` t ) ) )
85	84	reseq1d 5278	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( t e. ( -u pi [,] pi ) |-> ( F ` t ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
86		ioossicc 11622	. . . . . . . . . . 11 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
87	86	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
88	80	ralrimiva 2881	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A. t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) t e. ( -u pi [,] pi ) )
89		dfss3 3499	. . . . . . . . . . 11 |- ( ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) <-> A. t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) t e. ( -u pi [,] pi ) )
90	88, 89	sylibr 212	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) )
91	87, 90	sstrd 3519	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) )
92		resmpt 5329	. . . . . . . . 9 |- ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) -> ( ( t e. ( -u pi [,] pi ) |-> ( F ` t ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) )
93	91, 92	syl 16	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( t e. ( -u pi [,] pi ) |-> ( F ` t ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) )
94		eqidd 2468	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) )
95	85, 93, 94	3eqtrd 2512	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) )
96	95	eqcomd 2475	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
97		fourierdlem93.7	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
98	96, 97	eqeltrd 2555	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
99		fourierdlem93.9	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
100	95	oveq1d 6310	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) lim CC ( Q ` ( i + 1 ) ) ) )
101	99, 100	eleqtrd 2557	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) lim CC ( Q ` ( i + 1 ) ) ) )
102		fourierdlem93.8	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
103	95	oveq1d 6310	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) lim CC ( Q ` i ) ) )
104	102, 103	eleqtrd 2557	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) lim CC ( Q ` i ) ) )
105	59, 65, 98, 101, 104	iblcncfioo 31619	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. L^1 )
106	59, 65	jca 532	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) e. RR /\ ( Q ` ( i + 1 ) ) e. RR ) )
107		prssg 4188	. . . . . . . 8 |- ( ( ( Q ` i ) e. RR /\ ( Q ` ( i + 1 ) ) e. RR ) -> ( ( ( Q ` i ) e. RR /\ ( Q ` ( i + 1 ) ) e. RR ) <-> { ( Q ` i ) , ( Q ` ( i + 1 ) ) } C_ RR ) )
108	106, 107	syl 16	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) e. RR /\ ( Q ` ( i + 1 ) ) e. RR ) <-> { ( Q ` i ) , ( Q ` ( i + 1 ) ) } C_ RR ) )
109	106, 108	mpbid 210	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> { ( Q ` i ) , ( Q ` ( i + 1 ) ) } C_ RR )
110		prfi 7807	. . . . . . . . 9 |- { ( Q ` i ) , ( Q ` ( i + 1 ) ) } e. Fin
111	110	a1i 11	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> { ( Q ` i ) , ( Q ` ( i + 1 ) ) } e. Fin )
112	111, 109	jca 532	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( { ( Q ` i ) , ( Q ` ( i + 1 ) ) } e. Fin /\ { ( Q ` i ) , ( Q ` ( i + 1 ) ) } C_ RR ) )
113		ovolfi 21773	. . . . . . 7 |- ( ( { ( Q ` i ) , ( Q ` ( i + 1 ) ) } e. Fin /\ { ( Q ` i ) , ( Q ` ( i + 1 ) ) } C_ RR ) -> ( vol* ` { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) = 0 )
114	112, 113	syl 16	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( vol* ` { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) = 0 )
115	39	ad2antrr 725	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) -> F : ( -u pi [,] pi ) --> CC )
116		simpl 457	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) -> ( ph /\ i e. ( 0..^ M ) ) )
117		lbicc2 11648	. . . . . . . . . . . . . . 15 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( Q ` i ) <_ ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
118	68, 117	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
119		ubicc2 11649	. . . . . . . . . . . . . . 15 |- ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( Q ` i ) <_ ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
120	68, 119	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
121	118, 120	jca 532	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) /\ ( Q ` ( i + 1 ) ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) )
122		prssi 4189	. . . . . . . . . . . . 13 |- ( ( ( Q ` i ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) /\ ( Q ` ( i + 1 ) ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> { ( Q ` i ) , ( Q ` ( i + 1 ) ) } C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
123	121, 122	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> { ( Q ` i ) , ( Q ` ( i + 1 ) ) } C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
124	123	sseld 3508	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. { ( Q ` i ) , ( Q ` ( i + 1 ) ) } -> t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) )
125	124	imp 429	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) -> t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
126	116, 125	jca 532	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) -> ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) )
127	126, 80	syl 16	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) -> t e. ( -u pi [,] pi ) )
128	115, 127	jca 532	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) -> ( F : ( -u pi [,] pi ) --> CC /\ t e. ( -u pi [,] pi ) ) )
129	128, 46	syl 16	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ) -> ( F ` t ) e. CC )
130	109, 114, 129	itgvol0 31609	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( t e. { ( Q ` i ) , ( Q ` ( i + 1 ) ) } |-> ( F ` t ) ) e. L^1 /\ S. { ( Q ` i ) , ( Q ` ( i + 1 ) ) } ( F ` t ) _d t = 0 ) )
131	130	simpld 459	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. { ( Q ` i ) , ( Q ` ( i + 1 ) ) } |-> ( F ` t ) ) e. L^1 )
132	53, 71, 82, 105, 131	iblsplit 31607	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. L^1 )
133	21, 27, 37, 38, 47, 132	itgspltprt 31620	. 2 |- ( ph -> S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( F ` t ) _d t = sum_ i e. ( 0..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` t ) _d t )
134		fvres 5886	. . . . . . . 8 |- ( t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) = ( F ` t ) )
135	134	eqcomd 2475	. . . . . . 7 |- ( t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -> ( F ` t ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) )
136	135	adantl 466	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` t ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) )
137	136	itgeq2dv 22056	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` t ) _d t = S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) _d t )
138		eqid 2467	. . . . . 6 |- ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) ) = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
139	39	adantr 465	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F : ( -u pi [,] pi ) --> CC )
140		fssres 5757	. . . . . . 7 |- ( ( F : ( -u pi [,] pi ) --> CC /\ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) ) -> ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) --> CC )
141	139, 90, 140	syl2anc 661	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) --> CC )
142		resabs1 5308	. . . . . . . 8 |- ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
143	87, 142	syl 16	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
144	143, 97	eqeltrd 2555	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
145	143	oveq1d 6310	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
146	145	eqcomd 2475	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) = ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
147	59, 65, 38, 141	limcicciooub 31502	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
148	146, 147	eqtrd 2508	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
149	99, 148	eleqtrd 2557	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
150	143	eqcomd 2475	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
151	150	oveq1d 6310	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) = ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
152	59, 65, 38, 141	limciccioolb 31486	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
153		eqidd 2468	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
154	151, 152, 153	3eqtrd 2512	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
155	102, 154	eleqtrd 2557	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
156		fourierdlem93.5	. . . . . . 7 |- ( ph -> X e. RR )
157	156	adantr 465	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> X e. RR )
158	138, 59, 65, 38, 141, 144, 149, 155, 157	fourierdlem82 31812	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) _d t = S. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) _d t )
159	157	adantr 465	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> X e. RR )
160	59	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( Q ` i ) e. RR )
161	160, 159	resubcld 9999	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( Q ` i ) - X ) e. RR )
162	65	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
163	162, 159	resubcld 9999	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( Q ` ( i + 1 ) ) - X ) e. RR )
164		simpr 461	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) )
165		eliccre 31427	. . . . . . . . . . 11 |- ( ( ( ( Q ` i ) - X ) e. RR /\ ( ( Q ` ( i + 1 ) ) - X ) e. RR /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t e. RR )
166	161, 163, 164, 165	syl3anc 1228	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t e. RR )
167	159, 166	readdcld 9635	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( X + t ) e. RR )
168		elicc2 11601	. . . . . . . . . . . . 13 |- ( ( ( ( Q ` i ) - X ) e. RR /\ ( ( Q ` ( i + 1 ) ) - X ) e. RR ) -> ( t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) <-> ( t e. RR /\ ( ( Q ` i ) - X ) <_ t /\ t <_ ( ( Q ` ( i + 1 ) ) - X ) ) ) )
169	161, 163, 168	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) <-> ( t e. RR /\ ( ( Q ` i ) - X ) <_ t /\ t <_ ( ( Q ` ( i + 1 ) ) - X ) ) ) )
170	164, 169	mpbid 210	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( t e. RR /\ ( ( Q ` i ) - X ) <_ t /\ t <_ ( ( Q ` ( i + 1 ) ) - X ) ) )
171	170	simp2d 1009	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( Q ` i ) - X ) <_ t )
172		lesubadd2 10037	. . . . . . . . . . 11 |- ( ( ( Q ` i ) e. RR /\ X e. RR /\ t e. RR ) -> ( ( ( Q ` i ) - X ) <_ t <-> ( Q ` i ) <_ ( X + t ) ) )
173	160, 159, 166, 172	syl3anc 1228	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( ( Q ` i ) - X ) <_ t <-> ( Q ` i ) <_ ( X + t ) ) )
174	171, 173	mpbid 210	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( Q ` i ) <_ ( X + t ) )
175	170	simp3d 1010	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t <_ ( ( Q ` ( i + 1 ) ) - X ) )
176		leaddsub2 10041	. . . . . . . . . . 11 |- ( ( X e. RR /\ t e. RR /\ ( Q ` ( i + 1 ) ) e. RR ) -> ( ( X + t ) <_ ( Q ` ( i + 1 ) ) <-> t <_ ( ( Q ` ( i + 1 ) ) - X ) ) )
177	159, 166, 162, 176	syl3anc 1228	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( X + t ) <_ ( Q ` ( i + 1 ) ) <-> t <_ ( ( Q ` ( i + 1 ) ) - X ) ) )
178	175, 177	mpbird 232	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( X + t ) <_ ( Q ` ( i + 1 ) ) )
179	167, 174, 178	3jca 1176	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( X + t ) e. RR /\ ( Q ` i ) <_ ( X + t ) /\ ( X + t ) <_ ( Q ` ( i + 1 ) ) ) )
180		elicc2 11601	. . . . . . . . 9 |- ( ( ( Q ` i ) e. RR /\ ( Q ` ( i + 1 ) ) e. RR ) -> ( ( X + t ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) <-> ( ( X + t ) e. RR /\ ( Q ` i ) <_ ( X + t ) /\ ( X + t ) <_ ( Q ` ( i + 1 ) ) ) ) )
181	160, 162, 180	syl2anc 661	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( X + t ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) <-> ( ( X + t ) e. RR /\ ( Q ` i ) <_ ( X + t ) /\ ( X + t ) <_ ( Q ` ( i + 1 ) ) ) ) )
182	179, 181	mpbird 232	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( X + t ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
183		fvres 5886	. . . . . . 7 |- ( ( X + t ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) = ( F ` ( X + t ) ) )
184	182, 183	syl 16	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) = ( F ` ( X + t ) ) )
185	184	itgeq2dv 22056	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> S. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) _d t = S. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ( F ` ( X + t ) ) _d t )
186	137, 158, 185	3eqtrd 2512	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` t ) _d t = S. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ( F ` ( X + t ) ) _d t )
187	186	sumeq2dv 13505	. . 3 |- ( ph -> sum_ i e. ( 0..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` t ) _d t = sum_ i e. ( 0..^ M ) S. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ( F ` ( X + t ) ) _d t )
188		oveq2 6303	. . . . . . 7 |- ( s = t -> ( X + s ) = ( X + t ) )
189	188	fveq2d 5876	. . . . . 6 |- ( s = t -> ( F ` ( X + s ) ) = ( F ` ( X + t ) ) )
190		nfcv 2629	. . . . . 6 |- F/_ t ( F ` ( X + s ) )
191		nfcv 2629	. . . . . 6 |- F/_ s ( F ` ( X + t ) )
192	189, 190, 191	cbvitg 22050	. . . . 5 |- S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + s ) ) _d s = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + t ) ) _d t
193	192	a1i 11	. . . 4 |- ( ph -> S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + s ) ) _d s = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + t ) ) _d t )
194		fourierdlem93.2	. . . . . . . . 9 |- H = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )
195	194	a1i 11	. . . . . . . 8 |- ( ph -> H = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) )
196		fveq2 5872	. . . . . . . . . 10 |- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
197	196	oveq1d 6310	. . . . . . . . 9 |- ( i = 0 -> ( ( Q ` i ) - X ) = ( ( Q ` 0 ) - X ) )
198	197	adantl 466	. . . . . . . 8 |- ( ( ph /\ i = 0 ) -> ( ( Q ` i ) - X ) = ( ( Q ` 0 ) - X ) )
199	2	nnzd 10977	. . . . . . . . . . 11 |- ( ph -> M e. ZZ )
200	21, 199, 21	3jca 1176	. . . . . . . . . 10 |- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) )
201		0re 9608	. . . . . . . . . . . . 13 |- 0 e. RR
202	201	leidi 10099	. . . . . . . . . . . 12 |- 0 <_ 0
203	202	a1i 11	. . . . . . . . . . 11 |- ( ph -> 0 <_ 0 )
204	201	a1i 11	. . . . . . . . . . . 12 |- ( ph -> 0 e. RR )
205	2	nnred 10563	. . . . . . . . . . . 12 |- ( ph -> M e. RR )
206	2	nngt0d 10591	. . . . . . . . . . . 12 |- ( ph -> 0 < M )
207	204, 205, 206	ltled 9744	. . . . . . . . . . 11 |- ( ph -> 0 <_ M )
208	203, 207	jca 532	. . . . . . . . . 10 |- ( ph -> ( 0 <_ 0 /\ 0 <_ M ) )
209	200, 208	jca 532	. . . . . . . . 9 |- ( ph -> ( ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) /\ ( 0 <_ 0 /\ 0 <_ M ) ) )
210		elfz2 11691	. . . . . . . . 9 |- ( 0 e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) /\ ( 0 <_ 0 /\ 0 <_ M ) ) )
211	209, 210	sylibr 212	. . . . . . . 8 |- ( ph -> 0 e. ( 0 ... M ) )
212	9, 30	syl6eqel 2563	. . . . . . . . 9 |- ( ph -> ( Q ` 0 ) e. RR )
213	212, 156	resubcld 9999	. . . . . . . 8 |- ( ph -> ( ( Q ` 0 ) - X ) e. RR )
214	195, 198, 211, 213	fvmptd 5962	. . . . . . 7 |- ( ph -> ( H ` 0 ) = ( ( Q ` 0 ) - X ) )
215	9	oveq1d 6310	. . . . . . 7 |- ( ph -> ( ( Q ` 0 ) - X ) = ( -u pi - X ) )
216	214, 215	eqtr2d 2509	. . . . . 6 |- ( ph -> ( -u pi - X ) = ( H ` 0 ) )
217		fveq2 5872	. . . . . . . . . 10 |- ( i = M -> ( Q ` i ) = ( Q ` M ) )
218	217	oveq1d 6310	. . . . . . . . 9 |- ( i = M -> ( ( Q ` i ) - X ) = ( ( Q ` M ) - X ) )
219	218	adantl 466	. . . . . . . 8 |- ( ( ph /\ i = M ) -> ( ( Q ` i ) - X ) = ( ( Q ` M ) - X ) )
220	21, 199, 199	3jca 1176	. . . . . . . . . 10 |- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ M e. ZZ ) )
221	205	leidd 10131	. . . . . . . . . . 11 |- ( ph -> M <_ M )
222	207, 221	jca 532	. . . . . . . . . 10 |- ( ph -> ( 0 <_ M /\ M <_ M ) )
223	220, 222	jca 532	. . . . . . . . 9 |- ( ph -> ( ( 0 e. ZZ /\ M e. ZZ /\ M e. ZZ ) /\ ( 0 <_ M /\ M <_ M ) ) )
224		elfz2 11691	. . . . . . . . 9 |- ( M e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ M e. ZZ ) /\ ( 0 <_ M /\ M <_ M ) ) )
225	223, 224	sylibr 212	. . . . . . . 8 |- ( ph -> M e. ( 0 ... M ) )
226	10, 29	syl6eqel 2563	. . . . . . . . 9 |- ( ph -> ( Q ` M ) e. RR )
227	226, 156	resubcld 9999	. . . . . . . 8 |- ( ph -> ( ( Q ` M ) - X ) e. RR )
228	195, 219, 225, 227	fvmptd 5962	. . . . . . 7 |- ( ph -> ( H ` M ) = ( ( Q ` M ) - X ) )
229	10	oveq1d 6310	. . . . . . 7 |- ( ph -> ( ( Q ` M ) - X ) = ( pi - X ) )
230	228, 229	eqtr2d 2509	. . . . . 6 |- ( ph -> ( pi - X ) = ( H ` M ) )
231	216, 230	oveq12d 6313	. . . . 5 |- ( ph -> ( ( -u pi - X ) [,] ( pi - X ) ) = ( ( H ` 0 ) [,] ( H ` M ) ) )
232		itgeq1 22047	. . . . 5 |- ( ( ( -u pi - X ) [,] ( pi - X ) ) = ( ( H ` 0 ) [,] ( H ` M ) ) -> S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + t ) ) _d t = S. ( ( H ` 0 ) [,] ( H ` M ) ) ( F ` ( X + t ) ) _d t )
233	231, 232	syl 16	. . . 4 |- ( ph -> S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + t ) ) _d t = S. ( ( H ` 0 ) [,] ( H ` M ) ) ( F ` ( X + t ) ) _d t )
234	37, 58	sylan 471	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
235	156	adantr 465	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0 ... M ) ) -> X e. RR )
236	234, 235	resubcld 9999	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( Q ` i ) - X ) e. RR )
237	236	ralrimiva 2881	. . . . . . 7 |- ( ph -> A. i e. ( 0 ... M ) ( ( Q ` i ) - X ) e. RR )
238	194	fmpt 6053	. . . . . . 7 |- ( A. i e. ( 0 ... M ) ( ( Q ` i ) - X ) e. RR <-> H : ( 0 ... M ) --> RR )
239	237, 238	sylib 196	. . . . . 6 |- ( ph -> H : ( 0 ... M ) --> RR )
240	59, 65, 157	ltsub1d 10173	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( ( Q ` i ) - X ) < ( ( Q ` ( i + 1 ) ) - X ) ) )
241	38, 240	mpbid 210	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - X ) < ( ( Q ` ( i + 1 ) ) - X ) )
242	56, 236	syldan 470	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - X ) e. RR )
243	194	fvmpt2 5964	. . . . . . . 8 |- ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) - X ) e. RR ) -> ( H ` i ) = ( ( Q ` i ) - X ) )
244	56, 242, 243	syl2anc 661	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` i ) = ( ( Q ` i ) - X ) )
245		nfcv 2629	. . . . . . . . . . 11 |- F/_ j ( ( Q ` i ) - X )
246		nfcv 2629	. . . . . . . . . . 11 |- F/_ i ( ( Q ` j ) - X )
247		fveq2 5872	. . . . . . . . . . . 12 |- ( i = j -> ( Q ` i ) = ( Q ` j ) )
248	247	oveq1d 6310	. . . . . . . . . . 11 |- ( i = j -> ( ( Q ` i ) - X ) = ( ( Q ` j ) - X ) )
249	245, 246, 248	cbvmpt 4543	. . . . . . . . . 10 |- ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
250	194, 249	eqtri 2496	. . . . . . . . 9 |- H = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
251	250	a1i 11	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> H = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) ) )
252		fveq2 5872	. . . . . . . . . 10 |- ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
253	252	oveq1d 6310	. . . . . . . . 9 |- ( j = ( i + 1 ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
254	253	adantl 466	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
255	65, 157	resubcld 9999	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) - X ) e. RR )
256	251, 254, 62, 255	fvmptd 5962	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) - X ) )
257	241, 244, 256	3brtr4d 4483	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` i ) < ( H ` ( i + 1 ) ) )
258		ffun 5739	. . . . . . . . . 10 |- ( F : ( -u pi [,] pi ) --> CC -> Fun F )
259	39, 258	syl 16	. . . . . . . . 9 |- ( ph -> Fun F )
260	259	adantr 465	. . . . . . . 8 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> Fun F )
261	156	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> X e. RR )
262	214, 213	eqeltrd 2555	. . . . . . . . . . . . . 14 |- ( ph -> ( H ` 0 ) e. RR )
263	262	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` 0 ) e. RR )
264	228, 227	eqeltrd 2555	. . . . . . . . . . . . . 14 |- ( ph -> ( H ` M ) e. RR )
265	264	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` M ) e. RR )
266		simpr 461	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. ( ( H ` 0 ) [,] ( H ` M ) ) )
267		eliccre 31427	. . . . . . . . . . . . 13 |- ( ( ( H ` 0 ) e. RR /\ ( H ` M ) e. RR /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. RR )
268	263, 265, 266, 267	syl3anc 1228	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. RR )
269	261, 268	readdcld 9635	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. RR )
270		elicc2 11601	. . . . . . . . . . . . . . . 16 |- ( ( ( H ` 0 ) e. RR /\ ( H ` M ) e. RR ) -> ( t e. ( ( H ` 0 ) [,] ( H ` M ) ) <-> ( t e. RR /\ ( H ` 0 ) <_ t /\ t <_ ( H ` M ) ) ) )
271	263, 265, 270	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( t e. ( ( H ` 0 ) [,] ( H ` M ) ) <-> ( t e. RR /\ ( H ` 0 ) <_ t /\ t <_ ( H ` M ) ) ) )
272	266, 271	mpbid 210	. . . . . . . . . . . . . 14 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( t e. RR /\ ( H ` 0 ) <_ t /\ t <_ ( H ` M ) ) )
273	272	simp2d 1009	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` 0 ) <_ t )
274	263, 268, 261	3jca 1176	. . . . . . . . . . . . . 14 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( ( H ` 0 ) e. RR /\ t e. RR /\ X e. RR ) )
275		leadd2 10033	. . . . . . . . . . . . . 14 |- ( ( ( H ` 0 ) e. RR /\ t e. RR /\ X e. RR ) -> ( ( H ` 0 ) <_ t <-> ( X + ( H ` 0 ) ) <_ ( X + t ) ) )
276	274, 275	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( ( H ` 0 ) <_ t <-> ( X + ( H ` 0 ) ) <_ ( X + t ) ) )
277	273, 276	mpbid 210	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + ( H ` 0 ) ) <_ ( X + t ) )
278	196	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i = 0 ) -> ( Q ` i ) = ( Q ` 0 ) )
279	278	oveq1d 6310	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i = 0 ) -> ( ( Q ` i ) - X ) = ( ( Q ` 0 ) - X ) )
280	195, 279, 211, 213	fvmptd 5962	. . . . . . . . . . . . . . . 16 |- ( ph -> ( H ` 0 ) = ( ( Q ` 0 ) - X ) )
281	280	oveq2d 6311	. . . . . . . . . . . . . . 15 |- ( ph -> ( X + ( H ` 0 ) ) = ( X + ( ( Q ` 0 ) - X ) ) )
282		ax-resscn 9561	. . . . . . . . . . . . . . . . 17 |- RR C_ CC
283	282, 156	sseldi 3507	. . . . . . . . . . . . . . . 16 |- ( ph -> X e. CC )
284	282, 212	sseldi 3507	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Q ` 0 ) e. CC )
285		pncan3 9840	. . . . . . . . . . . . . . . 16 |- ( ( X e. CC /\ ( Q ` 0 ) e. CC ) -> ( X + ( ( Q ` 0 ) - X ) ) = ( Q ` 0 ) )
286	283, 284, 285	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ph -> ( X + ( ( Q ` 0 ) - X ) ) = ( Q ` 0 ) )
287	281, 286, 9	3eqtrrd 2513	. . . . . . . . . . . . . 14 |- ( ph -> -u pi = ( X + ( H ` 0 ) ) )
288	287	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u pi = ( X + ( H ` 0 ) ) )
289	288	breq1d 4463	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( -u pi <_ ( X + t ) <-> ( X + ( H ` 0 ) ) <_ ( X + t ) ) )
290	277, 289	mpbird 232	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u pi <_ ( X + t ) )
291	272	simp3d 1010	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t <_ ( H ` M ) )
292		leadd2 10033	. . . . . . . . . . . . . 14 |- ( ( t e. RR /\ ( H ` M ) e. RR /\ X e. RR ) -> ( t <_ ( H ` M ) <-> ( X + t ) <_ ( X + ( H ` M ) ) ) )
293	268, 265, 261, 292	syl3anc 1228	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( t <_ ( H ` M ) <-> ( X + t ) <_ ( X + ( H ` M ) ) ) )
294	291, 293	mpbid 210	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) <_ ( X + ( H ` M ) ) )
295	228	oveq2d 6311	. . . . . . . . . . . . . . 15 |- ( ph -> ( X + ( H ` M ) ) = ( X + ( ( Q ` M ) - X ) ) )
296	282, 226	sseldi 3507	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Q ` M ) e. CC )
297		pncan3 9840	. . . . . . . . . . . . . . . 16 |- ( ( X e. CC /\ ( Q ` M ) e. CC ) -> ( X + ( ( Q ` M ) - X ) ) = ( Q ` M ) )
298	283, 296, 297	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ph -> ( X + ( ( Q ` M ) - X ) ) = ( Q ` M ) )
299	295, 298, 10	3eqtrrd 2513	. . . . . . . . . . . . . 14 |- ( ph -> pi = ( X + ( H ` M ) ) )
300	299	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> pi = ( X + ( H ` M ) ) )
301	300	breq2d 4465	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( ( X + t ) <_ pi <-> ( X + t ) <_ ( X + ( H ` M ) ) ) )
302	294, 301	mpbird 232	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) <_ pi )
303	269, 290, 302	3jca 1176	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( ( X + t ) e. RR /\ -u pi <_ ( X + t ) /\ ( X + t ) <_ pi ) )
304	30	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u pi e. RR )
305	29	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> pi e. RR )
306		elicc2 11601	. . . . . . . . . . 11 |- ( ( -u pi e. RR /\ pi e. RR ) -> ( ( X + t ) e. ( -u pi [,] pi ) <-> ( ( X + t ) e. RR /\ -u pi <_ ( X + t ) /\ ( X + t ) <_ pi ) ) )
307	304, 305, 306	syl2anc 661	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( ( X + t ) e. ( -u pi [,] pi ) <-> ( ( X + t ) e. RR /\ -u pi <_ ( X + t ) /\ ( X + t ) <_ pi ) ) )
308	303, 307	mpbird 232	. . . . . . . . 9 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. ( -u pi [,] pi ) )
309		fdm 5741	. . . . . . . . . . . 12 |- ( F : ( -u pi [,] pi ) --> CC -> dom F = ( -u pi [,] pi ) )
310	39, 309	syl 16	. . . . . . . . . . 11 |- ( ph -> dom F = ( -u pi [,] pi ) )
311	310	eqcomd 2475	. . . . . . . . . 10 |- ( ph -> ( -u pi [,] pi ) = dom F )
312	311	adantr 465	. . . . . . . . 9 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( -u pi [,] pi ) = dom F )
313	308, 312	eleqtrd 2557	. . . . . . . 8 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. dom F )
314		fvelrn 6025	. . . . . . . 8 |- ( ( Fun F /\ ( X + t ) e. dom F ) -> ( F ` ( X + t ) ) e. ran F )
315	260, 313, 314	syl2anc 661	. . . . . . 7 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( F ` ( X + t ) ) e. ran F )
316		frn 5743	. . . . . . . . . 10 |- ( F : ( -u pi [,] pi ) --> CC -> ran F C_ CC )
317	39, 316	syl 16	. . . . . . . . 9 |- ( ph -> ran F C_ CC )
318	317	adantr 465	. . . . . . . 8 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ran F C_ CC )
319	318	sseld 3508	. . . . . . 7 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( ( F ` ( X + t ) ) e. ran F -> ( F ` ( X + t ) ) e. CC ) )
320	315, 319	mpd 15	. . . . . 6 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( F ` ( X + t ) ) e. CC )
321	244, 242	eqeltrd 2555	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` i ) e. RR )
322	256, 255	eqeltrd 2555	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` ( i + 1 ) ) e. RR )
323		fssres 5757	. . . . . . . . . . . 12 |- ( ( F : ( -u pi [,] pi ) --> CC /\ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
324	139, 91, 323	syl2anc 661	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
325	60	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
326	66	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
327	157	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> X e. RR )
328		elioore 11571	. . . . . . . . . . . . . . . . . . 19 |- ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> t e. RR )
329	328	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t e. RR )
330	327, 329	readdcld 9635	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. RR )
331	330	rexrd 9655	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. RR* )
332	325, 326, 331	3jca 1176	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( X + t ) e. RR* ) )
333		simpr 461	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
334	321	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) e. RR )
335	334	rexrd 9655	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) e. RR* )
336	322	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` ( i + 1 ) ) e. RR* )
337	336	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` ( i + 1 ) ) e. RR* )
338		elioo2 11582	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( H ` i ) e. RR* /\ ( H ` ( i + 1 ) ) e. RR* ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) <-> ( t e. RR /\ ( H ` i ) < t /\ t < ( H ` ( i + 1 ) ) ) ) )
339	335, 337, 338	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) <-> ( t e. RR /\ ( H ` i ) < t /\ t < ( H ` ( i + 1 ) ) ) ) )
340	333, 339	mpbid 210	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( t e. RR /\ ( H ` i ) < t /\ t < ( H ` ( i + 1 ) ) ) )
341	340	simp2d 1009	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) < t )
342	334, 329, 327	ltadd2d 9749	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( H ` i ) < t <-> ( X + ( H ` i ) ) < ( X + t ) ) )
343	341, 342	mpbid 210	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + ( H ` i ) ) < ( X + t ) )
344	244	oveq2d 6311	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( H ` i ) ) = ( X + ( ( Q ` i ) - X ) ) )
345	283	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( 0..^ M ) ) -> X e. CC )
346	282, 59	sseldi 3507	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. CC )
347		pncan3 9840	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( X e. CC /\ ( Q ` i ) e. CC ) -> ( X + ( ( Q ` i ) - X ) ) = ( Q ` i ) )
348	345, 346, 347	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( ( Q ` i ) - X ) ) = ( Q ` i ) )
349		eqidd 2468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( Q ` i ) )
350	344, 348, 349	3eqtrrd 2513	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( X + ( H ` i ) ) )
351	350	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) = ( X + ( H ` i ) ) )
352	351	breq1d 4463	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) < ( X + t ) <-> ( X + ( H ` i ) ) < ( X + t ) ) )
353	343, 352	mpbird 232	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + t ) )
354	340	simp3d 1010	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t < ( H ` ( i + 1 ) ) )
355	322	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` ( i + 1 ) ) e. RR )
356	329, 355, 327	ltadd2d 9749	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( t < ( H ` ( i + 1 ) ) <-> ( X + t ) < ( X + ( H ` ( i + 1 ) ) ) ) )
357	354, 356	mpbid 210	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) < ( X + ( H ` ( i + 1 ) ) ) )
358	256	oveq2d 6311	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( X + ( ( Q ` ( i + 1 ) ) - X ) ) )
359	282, 65	sseldi 3507	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
360		pncan3 9840	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( X e. CC /\ ( Q ` ( i + 1 ) ) e. CC ) -> ( X + ( ( Q ` ( i + 1 ) ) - X ) ) = ( Q ` ( i + 1 ) ) )
361	345, 359, 360	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( ( Q ` ( i + 1 ) ) - X ) ) = ( Q ` ( i + 1 ) ) )
362		eqidd 2468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( i + 1 ) ) )
363	358, 361, 362	3eqtrd 2512	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( Q ` ( i + 1 ) ) )
364	363	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( Q ` ( i + 1 ) ) )
365	364	breq2d 4465	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( X + t ) < ( X + ( H ` ( i + 1 ) ) ) <-> ( X + t ) < ( Q ` ( i + 1 ) ) ) )
366	357, 365	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) < ( Q ` ( i + 1 ) ) )
367	353, 366	jca 532	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) < ( X + t ) /\ ( X + t ) < ( Q ` ( i + 1 ) ) ) )
368	332, 367	jca 532	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( X + t ) e. RR* ) /\ ( ( Q ` i ) < ( X + t ) /\ ( X + t ) < ( Q ` ( i + 1 ) ) ) ) )
369		elioo3g 11570	. . . . . . . . . . . . . 14 |- ( ( X + t ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ ( X + t ) e. RR* ) /\ ( ( Q ` i ) < ( X + t ) /\ ( X + t ) < ( Q ` ( i + 1 ) ) ) ) )
370	368, 369	sylibr 212	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
371	370	ralrimiva 2881	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A. t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ( X + t ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
372		eqid 2467	. . . . . . . . . . . . 13 |- ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
373	372	fmpt 6053	. . . . . . . . . . . 12 |- ( A. t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ( X + t ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) : ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) --> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
374	371, 373	sylib 196	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) : ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) --> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
375		fcompt 6068	. . . . . . . . . . 11 |- ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC /\ ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 )