Theorem fourierdlem93 31871

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	. . . . . . . 8 |- ( ph -> Q e. ( P ` M ) )
2		fourierdlem93.3	. . . . . . . . 9 |- ( ph -> M e. NN )
3		fourierdlem93.1	. . . . . . . . . 10 |- 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 31780	. . . . . . . . 9 |- ( 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	. . . . . . . 8 |- ( 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	. . . . . . 7 |- ( 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	. . . . . 6 |- ( ph -> ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
8	7	simplld 754	. . . . 5 |- ( ph -> ( Q ` 0 ) = -u pi )
9	8	eqcomd 2451	. . . 4 |- ( ph -> -u pi = ( Q ` 0 ) )
10	7	simplrd 31380	. . . . 5 |- ( ph -> ( Q ` M ) = pi )
11	10	eqcomd 2451	. . . 4 |- ( ph -> pi = ( Q ` M ) )
12	9, 11	oveq12d 6299	. . 3 |- ( ph -> ( -u pi [,] pi ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
13	12	itgeq1d 31645	. 2 |- ( ph -> S. ( -u pi [,] pi ) ( F ` t ) _d t = S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( F ` t ) _d t )
14		0zd 10883	. . 3 |- ( ph -> 0 e. ZZ )
15		nnuz 11126	. . . . 5 |- NN = ( ZZ>= ` 1 )
16	2, 15	syl6eleq 2541	. . . 4 |- ( ph -> M e. ( ZZ>= ` 1 ) )
17		1e0p1 11013	. . . . . 6 |- 1 = ( 0 + 1 )
18	17	a1i 11	. . . . 5 |- ( ph -> 1 = ( 0 + 1 ) )
19	18	fveq2d 5860	. . . 4 |- ( ph -> ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) ) )
20	16, 19	eleqtrd 2533	. . 3 |- ( ph -> M e. ( ZZ>= ` ( 0 + 1 ) ) )
21	3, 2, 1	fourierdlem15 31793	. . . 4 |- ( ph -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
22		pire 22827	. . . . . . 7 |- pi e. RR
23	22	renegcli 9885	. . . . . 6 |- -u pi e. RR
24		iccssre 11616	. . . . . 6 |- ( ( -u pi e. RR /\ pi e. RR ) -> ( -u pi [,] pi ) C_ RR )
25	23, 22, 24	mp2an 672	. . . . 5 |- ( -u pi [,] pi ) C_ RR
26	25	a1i 11	. . . 4 |- ( ph -> ( -u pi [,] pi ) C_ RR )
27	21, 26	fssd 5730	. . 3 |- ( ph -> Q : ( 0 ... M ) --> RR )
28	7	simprd 463	. . . 4 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
29	28	r19.21bi 2812	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
30		fourierdlem93.6	. . . . 5 |- ( ph -> F : ( -u pi [,] pi ) --> CC )
31	30	adantr 465	. . . 4 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> F : ( -u pi [,] pi ) --> CC )
32		simpr 461	. . . . 5 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
33	12	eqcomd 2451	. . . . . 6 |- ( ph -> ( ( Q ` 0 ) [,] ( Q ` M ) ) = ( -u pi [,] pi ) )
34	33	adantr 465	. . . . 5 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( ( Q ` 0 ) [,] ( Q ` M ) ) = ( -u pi [,] pi ) )
35	32, 34	eleqtrd 2533	. . . 4 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> t e. ( -u pi [,] pi ) )
36	31, 35	ffvelrnd 6017	. . 3 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( F ` t ) e. CC )
37	27	adantr 465	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
38		elfzofz 11824	. . . . . 6 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
39	38	adantl 466	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
40	37, 39	ffvelrnd 6017	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
41		fzofzp1 11890	. . . . . 6 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
42	41	adantl 466	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
43	37, 42	ffvelrnd 6017	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
44	30	feqmptd 5911	. . . . . . . . . 10 |- ( ph -> F = ( t e. ( -u pi [,] pi ) |-> ( F ` t ) ) )
45	44	adantr 465	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F = ( t e. ( -u pi [,] pi ) |-> ( F ` t ) ) )
46	45	reseq1d 5262	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( t e. ( -u pi [,] pi ) |-> ( F ` t ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
47		ioossicc 11620	. . . . . . . . . . 11 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
48	47	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
49	23	rexri 9649	. . . . . . . . . . . . . 14 |- -u pi e. RR*
50	49	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> -u pi e. RR* )
51	22	rexri 9649	. . . . . . . . . . . . . 14 |- pi e. RR*
52	51	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> pi e. RR* )
53	21	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
54		simplr 755	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0..^ M ) )
55		simpr 461	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
56	50, 52, 53, 54, 55	fourierdlem1 31779	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> t e. ( -u pi [,] pi ) )
57	56	ralrimiva 2857	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A. t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) t e. ( -u pi [,] pi ) )
58		dfss3 3479	. . . . . . . . . . 11 |- ( ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) <-> A. t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) t e. ( -u pi [,] pi ) )
59	57, 58	sylibr 212	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) )
60	48, 59	sstrd 3499	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) )
61	60	resmptd 5315	. . . . . . . 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 ) ) )
62	46, 61	eqtrd 2484	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) )
63	62	eqcomd 2451	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
64		fourierdlem93.7	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
65	63, 64	eqeltrd 2531	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
66		fourierdlem93.9	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
67	62	oveq1d 6296	. . . . . 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 ) ) ) )
68	66, 67	eleqtrd 2533	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) lim CC ( Q ` ( i + 1 ) ) ) )
69		fourierdlem93.8	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
70	62	oveq1d 6296	. . . . . 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 ) ) )
71	69, 70	eleqtrd 2533	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) lim CC ( Q ` i ) ) )
72	40, 43, 65, 68, 71	iblcncfioo 31667	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. L^1 )
73	30	ad2antrr 725	. . . . 5 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> F : ( -u pi [,] pi ) --> CC )
74	73, 56	ffvelrnd 6017	. . . 4 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` t ) e. CC )
75	40, 43, 72, 74	ibliooicc 31660	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. L^1 )
76	14, 20, 27, 29, 36, 75	itgspltprt 31668	. 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 )
77		fvres 5870	. . . . . . . 8 |- ( t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) = ( F ` t ) )
78	77	eqcomd 2451	. . . . . . 7 |- ( t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -> ( F ` t ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) )
79	78	adantl 466	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` t ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) )
80	79	itgeq2dv 22165	. . . . 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 )
81		eqid 2443	. . . . . 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 ) ) ) )
82	30	adantr 465	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F : ( -u pi [,] pi ) --> CC )
83	82, 59	fssresd 5742	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) --> CC )
84	48	resabs1d 5293	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
85	84, 64	eqeltrd 2531	. . . . . 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 ) )
86	84	oveq1d 6296	. . . . . . . 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 ) ) ) )
87	40, 43, 29, 83	limcicciooub 31551	. . . . . . . 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 ) ) ) )
88	86, 87	eqtr3d 2486	. . . . . . 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 ) ) ) )
89	66, 88	eleqtrd 2533	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
90	84	eqcomd 2451	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
91	90	oveq1d 6296	. . . . . . . 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 ) ) )
92	40, 43, 29, 83	limciccioolb 31535	. . . . . . . 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 ) ) )
93	91, 92	eqtrd 2484	. . . . . . 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 ) ) )
94	69, 93	eleqtrd 2533	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
95		fourierdlem93.5	. . . . . . 7 |- ( ph -> X e. RR )
96	95	adantr 465	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> X e. RR )
97	81, 40, 43, 29, 83, 85, 89, 94, 96	fourierdlem82 31860	. . . . 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 )
98	40	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( Q ` i ) e. RR )
99	43	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
100	95	ad2antrr 725	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> X e. RR )
101	98, 100	resubcld 9994	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( Q ` i ) - X ) e. RR )
102	99, 100	resubcld 9994	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( Q ` ( i + 1 ) ) - X ) e. RR )
103		simpr 461	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) )
104		eliccre 31476	. . . . . . . . . 10 |- ( ( ( ( Q ` i ) - X ) e. RR /\ ( ( Q ` ( i + 1 ) ) - X ) e. RR /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t e. RR )
105	101, 102, 103, 104	syl3anc 1229	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t e. RR )
106	100, 105	readdcld 9626	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( X + t ) e. RR )
107		elicc2 11599	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) )
108	101, 102, 107	syl2anc 661	. . . . . . . . . . 11 |- ( ( ( 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 ) ) ) )
109	103, 108	mpbid 210	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
110	109	simp2d 1010	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( Q ` i ) - X ) <_ t )
111	98, 100, 105	lesubadd2d 10158	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( ( Q ` i ) - X ) <_ t <-> ( Q ` i ) <_ ( X + t ) ) )
112	110, 111	mpbid 210	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( Q ` i ) <_ ( X + t ) )
113	109	simp3d 1011	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t <_ ( ( Q ` ( i + 1 ) ) - X ) )
114	100, 105, 99	leaddsub2d 10161	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( X + t ) <_ ( Q ` ( i + 1 ) ) <-> t <_ ( ( Q ` ( i + 1 ) ) - X ) ) )
115	113, 114	mpbird 232	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( X + t ) <_ ( Q ` ( i + 1 ) ) )
116	98, 99, 106, 112, 115	eliccd 31474	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( X + t ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
117		fvres 5870	. . . . . . 7 |- ( ( X + t ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) = ( F ` ( X + t ) ) )
118	116, 117	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 ) ) )
119	118	itgeq2dv 22165	. . . . 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 )
120	80, 97, 119	3eqtrd 2488	. . . 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 )
121	120	sumeq2dv 13506	. . 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 )
122		oveq2 6289	. . . . . . 7 |- ( s = t -> ( X + s ) = ( X + t ) )
123	122	fveq2d 5860	. . . . . 6 |- ( s = t -> ( F ` ( X + s ) ) = ( F ` ( X + t ) ) )
124	123	cbvitgv 22160	. . . . 5 |- S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + s ) ) _d s = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + t ) ) _d t
125	124	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 )
126		fourierdlem93.2	. . . . . . . . 9 |- H = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )
127	126	a1i 11	. . . . . . . 8 |- ( ph -> H = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) )
128		fveq2 5856	. . . . . . . . . 10 |- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
129	128	oveq1d 6296	. . . . . . . . 9 |- ( i = 0 -> ( ( Q ` i ) - X ) = ( ( Q ` 0 ) - X ) )
130	129	adantl 466	. . . . . . . 8 |- ( ( ph /\ i = 0 ) -> ( ( Q ` i ) - X ) = ( ( Q ` 0 ) - X ) )
131	2	nnzd 10974	. . . . . . . . . 10 |- ( ph -> M e. ZZ )
132	14, 131, 14	3jca 1177	. . . . . . . . 9 |- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) )
133		0le0 10632	. . . . . . . . . . 11 |- 0 <_ 0
134	133	a1i 11	. . . . . . . . . 10 |- ( ph -> 0 <_ 0 )
135		0red 9600	. . . . . . . . . . 11 |- ( ph -> 0 e. RR )
136	2	nnred 10558	. . . . . . . . . . 11 |- ( ph -> M e. RR )
137	2	nngt0d 10586	. . . . . . . . . . 11 |- ( ph -> 0 < M )
138	135, 136, 137	ltled 9736	. . . . . . . . . 10 |- ( ph -> 0 <_ M )
139	134, 138	jca 532	. . . . . . . . 9 |- ( ph -> ( 0 <_ 0 /\ 0 <_ M ) )
140		elfz2 11689	. . . . . . . . 9 |- ( 0 e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) /\ ( 0 <_ 0 /\ 0 <_ M ) ) )
141	132, 139, 140	sylanbrc 664	. . . . . . . 8 |- ( ph -> 0 e. ( 0 ... M ) )
142	8, 23	syl6eqel 2539	. . . . . . . . 9 |- ( ph -> ( Q ` 0 ) e. RR )
143	142, 95	resubcld 9994	. . . . . . . 8 |- ( ph -> ( ( Q ` 0 ) - X ) e. RR )
144	127, 130, 141, 143	fvmptd 5946	. . . . . . 7 |- ( ph -> ( H ` 0 ) = ( ( Q ` 0 ) - X ) )
145	8	oveq1d 6296	. . . . . . 7 |- ( ph -> ( ( Q ` 0 ) - X ) = ( -u pi - X ) )
146	144, 145	eqtr2d 2485	. . . . . 6 |- ( ph -> ( -u pi - X ) = ( H ` 0 ) )
147		fveq2 5856	. . . . . . . . . 10 |- ( i = M -> ( Q ` i ) = ( Q ` M ) )
148	147	oveq1d 6296	. . . . . . . . 9 |- ( i = M -> ( ( Q ` i ) - X ) = ( ( Q ` M ) - X ) )
149	148	adantl 466	. . . . . . . 8 |- ( ( ph /\ i = M ) -> ( ( Q ` i ) - X ) = ( ( Q ` M ) - X ) )
150	14, 131, 131	3jca 1177	. . . . . . . . 9 |- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ M e. ZZ ) )
151	136	leidd 10126	. . . . . . . . . 10 |- ( ph -> M <_ M )
152	138, 151	jca 532	. . . . . . . . 9 |- ( ph -> ( 0 <_ M /\ M <_ M ) )
153		elfz2 11689	. . . . . . . . 9 |- ( M e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ M e. ZZ ) /\ ( 0 <_ M /\ M <_ M ) ) )
154	150, 152, 153	sylanbrc 664	. . . . . . . 8 |- ( ph -> M e. ( 0 ... M ) )
155	10, 22	syl6eqel 2539	. . . . . . . . 9 |- ( ph -> ( Q ` M ) e. RR )
156	155, 95	resubcld 9994	. . . . . . . 8 |- ( ph -> ( ( Q ` M ) - X ) e. RR )
157	127, 149, 154, 156	fvmptd 5946	. . . . . . 7 |- ( ph -> ( H ` M ) = ( ( Q ` M ) - X ) )
158	10	oveq1d 6296	. . . . . . 7 |- ( ph -> ( ( Q ` M ) - X ) = ( pi - X ) )
159	157, 158	eqtr2d 2485	. . . . . 6 |- ( ph -> ( pi - X ) = ( H ` M ) )
160	146, 159	oveq12d 6299	. . . . 5 |- ( ph -> ( ( -u pi - X ) [,] ( pi - X ) ) = ( ( H ` 0 ) [,] ( H ` M ) ) )
161	160	itgeq1d 31645	. . . 4 |- ( ph -> S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + t ) ) _d t = S. ( ( H ` 0 ) [,] ( H ` M ) ) ( F ` ( X + t ) ) _d t )
162	27	fnvinran 31343	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
163	95	adantr 465	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... M ) ) -> X e. RR )
164	162, 163	resubcld 9994	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( Q ` i ) - X ) e. RR )
165	164, 126	fmptd 6040	. . . . . 6 |- ( ph -> H : ( 0 ... M ) --> RR )
166	40, 43, 96, 29	ltsub1dd 10171	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - X ) < ( ( Q ` ( i + 1 ) ) - X ) )
167	39, 164	syldan 470	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - X ) e. RR )
168	126	fvmpt2 5948	. . . . . . . 8 |- ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) - X ) e. RR ) -> ( H ` i ) = ( ( Q ` i ) - X ) )
169	39, 167, 168	syl2anc 661	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` i ) = ( ( Q ` i ) - X ) )
170		fveq2 5856	. . . . . . . . . . . 12 |- ( i = j -> ( Q ` i ) = ( Q ` j ) )
171	170	oveq1d 6296	. . . . . . . . . . 11 |- ( i = j -> ( ( Q ` i ) - X ) = ( ( Q ` j ) - X ) )
172	171	cbvmptv 4528	. . . . . . . . . 10 |- ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
173	126, 172	eqtri 2472	. . . . . . . . 9 |- H = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
174	173	a1i 11	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> H = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) ) )
175		fveq2 5856	. . . . . . . . . 10 |- ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
176	175	oveq1d 6296	. . . . . . . . 9 |- ( j = ( i + 1 ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
177	176	adantl 466	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
178	43, 96	resubcld 9994	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) - X ) e. RR )
179	174, 177, 42, 178	fvmptd 5946	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) - X ) )
180	166, 169, 179	3brtr4d 4467	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` i ) < ( H ` ( i + 1 ) ) )
181		frn 5727	. . . . . . . . 9 |- ( F : ( -u pi [,] pi ) --> CC -> ran F C_ CC )
182	30, 181	syl 16	. . . . . . . 8 |- ( ph -> ran F C_ CC )
183	182	adantr 465	. . . . . . 7 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ran F C_ CC )
184		ffun 5723	. . . . . . . . . 10 |- ( F : ( -u pi [,] pi ) --> CC -> Fun F )
185	30, 184	syl 16	. . . . . . . . 9 |- ( ph -> Fun F )
186	185	adantr 465	. . . . . . . 8 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> Fun F )
187	23	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u pi e. RR )
188	22	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> pi e. RR )
189	95	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> X e. RR )
190	144, 143	eqeltrd 2531	. . . . . . . . . . . . 13 |- ( ph -> ( H ` 0 ) e. RR )
191	190	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` 0 ) e. RR )
192	157, 156	eqeltrd 2531	. . . . . . . . . . . . 13 |- ( ph -> ( H ` M ) e. RR )
193	192	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` M ) e. RR )
194		simpr 461	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. ( ( H ` 0 ) [,] ( H ` M ) ) )
195		eliccre 31476	. . . . . . . . . . . 12 |- ( ( ( H ` 0 ) e. RR /\ ( H ` M ) e. RR /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. RR )
196	191, 193, 194, 195	syl3anc 1229	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. RR )
197	189, 196	readdcld 9626	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. RR )
198	128	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i = 0 ) -> ( Q ` i ) = ( Q ` 0 ) )
199	198	oveq1d 6296	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i = 0 ) -> ( ( Q ` i ) - X ) = ( ( Q ` 0 ) - X ) )
200	127, 199, 141, 143	fvmptd 5946	. . . . . . . . . . . . . 14 |- ( ph -> ( H ` 0 ) = ( ( Q ` 0 ) - X ) )
201	200	oveq2d 6297	. . . . . . . . . . . . 13 |- ( ph -> ( X + ( H ` 0 ) ) = ( X + ( ( Q ` 0 ) - X ) ) )
202	95	recnd 9625	. . . . . . . . . . . . . 14 |- ( ph -> X e. CC )
203	142	recnd 9625	. . . . . . . . . . . . . 14 |- ( ph -> ( Q ` 0 ) e. CC )
204	202, 203	pncan3d 9939	. . . . . . . . . . . . 13 |- ( ph -> ( X + ( ( Q ` 0 ) - X ) ) = ( Q ` 0 ) )
205	201, 204, 8	3eqtrrd 2489	. . . . . . . . . . . 12 |- ( ph -> -u pi = ( X + ( H ` 0 ) ) )
206	205	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u pi = ( X + ( H ` 0 ) ) )
207		elicc2 11599	. . . . . . . . . . . . . . 15 |- ( ( ( H ` 0 ) e. RR /\ ( H ` M ) e. RR ) -> ( t e. ( ( H ` 0 ) [,] ( H ` M ) ) <-> ( t e. RR /\ ( H ` 0 ) <_ t /\ t <_ ( H ` M ) ) ) )
208	191, 193, 207	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( t e. ( ( H ` 0 ) [,] ( H ` M ) ) <-> ( t e. RR /\ ( H ` 0 ) <_ t /\ t <_ ( H ` M ) ) ) )
209	194, 208	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( t e. RR /\ ( H ` 0 ) <_ t /\ t <_ ( H ` M ) ) )
210	209	simp2d 1010	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` 0 ) <_ t )
211	191, 196, 189, 210	leadd2dd 10174	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + ( H ` 0 ) ) <_ ( X + t ) )
212	206, 211	eqbrtrd 4457	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u pi <_ ( X + t ) )
213	209	simp3d 1011	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t <_ ( H ` M ) )
214	196, 193, 189, 213	leadd2dd 10174	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) <_ ( X + ( H ` M ) ) )
215	157	oveq2d 6297	. . . . . . . . . . . . 13 |- ( ph -> ( X + ( H ` M ) ) = ( X + ( ( Q ` M ) - X ) ) )
216	155	recnd 9625	. . . . . . . . . . . . . 14 |- ( ph -> ( Q ` M ) e. CC )
217	202, 216	pncan3d 9939	. . . . . . . . . . . . 13 |- ( ph -> ( X + ( ( Q ` M ) - X ) ) = ( Q ` M ) )
218	215, 217, 10	3eqtrrd 2489	. . . . . . . . . . . 12 |- ( ph -> pi = ( X + ( H ` M ) ) )
219	218	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> pi = ( X + ( H ` M ) ) )
220	214, 219	breqtrrd 4463	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) <_ pi )
221	187, 188, 197, 212, 220	eliccd 31474	. . . . . . . . 9 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. ( -u pi [,] pi ) )
222		fdm 5725	. . . . . . . . . . . 12 |- ( F : ( -u pi [,] pi ) --> CC -> dom F = ( -u pi [,] pi ) )
223	30, 222	syl 16	. . . . . . . . . . 11 |- ( ph -> dom F = ( -u pi [,] pi ) )
224	223	eqcomd 2451	. . . . . . . . . 10 |- ( ph -> ( -u pi [,] pi ) = dom F )
225	224	adantr 465	. . . . . . . . 9 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( -u pi [,] pi ) = dom F )
226	221, 225	eleqtrd 2533	. . . . . . . 8 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. dom F )
227		fvelrn 6009	. . . . . . . 8 |- ( ( Fun F /\ ( X + t ) e. dom F ) -> ( F ` ( X + t ) ) e. ran F )
228	186, 226, 227	syl2anc 661	. . . . . . 7 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( F ` ( X + t ) ) e. ran F )
229	183, 228	sseldd 3490	. . . . . 6 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( F ` ( X + t ) ) e. CC )
230	169, 167	eqeltrd 2531	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` i ) e. RR )
231	179, 178	eqeltrd 2531	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` ( i + 1 ) ) e. RR )
232	82, 60	fssresd 5742	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
233	40	rexrd 9646	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
234	233	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
235	43	rexrd 9646	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
236	235	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
237	95	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> X e. RR )
238		elioore 11569	. . . . . . . . . . . . . . 15 |- ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> t e. RR )
239	238	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t e. RR )
240	237, 239	readdcld 9626	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. RR )
241	169	oveq2d 6297	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( H ` i ) ) = ( X + ( ( Q ` i ) - X ) ) )
242	202	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> X e. CC )
243	40	recnd 9625	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. CC )
244	242, 243	pncan3d 9939	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( ( Q ` i ) - X ) ) = ( Q ` i ) )
245		eqidd 2444	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( Q ` i ) )
246	241, 244, 245	3eqtrrd 2489	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( X + ( H ` i ) ) )
247	246	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) = ( X + ( H ` i ) ) )
248	230	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) e. RR )
249		simpr 461	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
250	248	rexrd 9646	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) e. RR* )
251	231	rexrd 9646	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` ( i + 1 ) ) e. RR* )
252	251	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` ( i + 1 ) ) e. RR* )
253		elioo2 11580	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) ) )
254	250, 252, 253	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) ) ) )
255	249, 254	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( t e. RR /\ ( H ` i ) < t /\ t < ( H ` ( i + 1 ) ) ) )
256	255	simp2d 1010	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) < t )
257	248, 239, 237, 256	ltadd2dd 9744	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + ( H ` i ) ) < ( X + t ) )
258	247, 257	eqbrtrd 4457	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + t ) )
259	231	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` ( i + 1 ) ) e. RR )
260	255	simp3d 1011	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t < ( H ` ( i + 1 ) ) )
261	239, 259, 237, 260	ltadd2dd 9744	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) < ( X + ( H ` ( i + 1 ) ) ) )
262	179	oveq2d 6297	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( X + ( ( Q ` ( i + 1 ) ) - X ) ) )
263	43	recnd 9625	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
264	242, 263	pncan3d 9939	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( ( Q ` ( i + 1 ) ) - X ) ) = ( Q ` ( i + 1 ) ) )
265	262, 264	eqtrd 2484	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( Q ` ( i + 1 ) ) )
266	265	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( Q ` ( i + 1 ) ) )
267	261, 266	breqtrd 4461	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) < ( Q ` ( i + 1 ) ) )
268	234, 236, 240, 258, 267	eliood 31467	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
269		eqid 2443	. . . . . . . . . . . 12 |- ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
270	268, 269	fmptd 6040	. . . . . . . . . . 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 ) ) ) )
271		fcompt 6052	. . . . . . . . . . 11 |- ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC /\ ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) : ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) --> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) = ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) )
272	232, 270, 271	syl2anc 661	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) = ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) )
273		oveq2 6289	. . . . . . . . . . . . . . . 16 |- ( t = r -> ( X + t ) = ( X + r ) )
274	273	cbvmptv 4528	. . . . . . . . . . . . . . 15 |- ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) = ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) )
275	274	fveq1i 5857	. . . . . . . . . . . . . 14 |- ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) = ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s )
276	275	fveq2i 5859	. . . . . . . . . . . . 13 |- ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) )
277	276	mpteq2i 4520	. . . . . . . . . . . 12 |- ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) = ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) ) )
278	277	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) = ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) ) ) )
279		fveq2 5856	. . . . . . . . . . . . . 14 |- ( s = t -> ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) = ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) )
280	279	fveq2d 5860	. . . . . . . . . . . . 13 |- ( s = t -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) ) )
281	280	cbvmptv 4528	. . . . . . . . . . . 12 |- ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) ) )
282	281	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) ) ) )
283		eqidd 2444	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) = ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) )
284		oveq2 6289	. . . . . . . . . . . . . . . 16 |- ( r = t -> ( X + r ) = ( X + t ) )
285	284	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) /\ r = t ) -> ( X + r ) = ( X + t ) )
286	283, 285, 249, 240	fvmptd 5946	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) = ( X + t ) )
287	286	fveq2d 5860	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) )
288		fvres 5870	. . . . . . . . . . . . . 14 |- ( ( X + t ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) = ( F ` ( X + t ) ) )
289	268, 288	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) = ( F ` ( X + t ) ) )
290	287, 289	eqtrd 2484	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) ) = ( F ` ( X + t ) ) )
291	290	mpteq2dva 4523	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) )
292	278, 282, 291	3eqtrd 2488	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) )
293	272, 292	eqtr2d 2485	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) )
294		eqid 2443	. . . . . . . . . . 11 |- ( t e. CC |-> ( X + t ) ) = ( t e. CC |-> ( X + t ) )
295		ssid 3508	. . . . . . . . . . . . . . 15 |- CC C_ CC
296	295	a1i 11	. . . . . . . . . . . . . 14 |- ( X e. CC -> CC C_ CC )
297		id 22	. . . . . . . . . . . . . 14 |- ( X e. CC -> X e. CC )
298	296, 297, 296	constcncfg 31580	. . . . . . . . . . . . 13 |- ( X e. CC -> ( t e. CC |-> X ) e. ( CC -cn-> CC ) )
299		cncfmptid 21393	. . . . . . . . . . . . . . 15 |- ( ( CC C_ CC /\ CC C_ CC ) -> ( t e. CC |-> t ) e. ( CC -cn-> CC ) )
300	295, 295, 299	mp2an 672	. . . . . . . . . . . . . 14 |- ( t e. CC |-> t ) e. ( CC -cn-> CC )
301	300	a1i 11	. . . . . . . . . . . . 13 |- ( X e. CC -> ( t e. CC |-> t ) e. ( CC -cn-> CC ) )
302	298, 301	addcncf 31582	. . . . . . . . . . . 12 |- ( X e. CC -> ( t e. CC |-> ( X + t ) ) e. ( CC -cn-> CC ) )
303	242, 302	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. CC |-> ( X + t ) ) e. ( CC -cn-> CC ) )
304		ioosscn 31463	. . . . . . . . . . . 12 |- ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) C_ CC
305	304	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) C_ CC )
306		ioosscn 31463	. . . . . . . . . . . 12 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
307	306	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
308	294, 303, 305, 307, 268	cncfmptssg 31579	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -cn-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
309	308, 64	cncfco 21388	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -cn-> CC ) )
310	293, 309	eqeltrd 2531	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -cn-> CC ) )
311	233	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( Q ` i ) e. RR* )
312	235	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
313		simpr 461	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) )
314		vex 3098	. . . . . . . . . . . . . . . . . 18 |- r e. _V
315	269	elrnmpt 5239	. . . . . . . . . . . . . . . . . 18 |- ( r e. _V -> ( r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) <-> E. t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) r = ( X + t ) ) )
316	314, 315	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) <-> E. t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) r = ( X + t ) )
317	313, 316	sylib 196	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> E. t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) r = ( X + t ) )
318		nfv 1694	. . . . . . . . . . . . . . . . . 18 |- F/ t ( ph /\ i e. ( 0..^ M ) )
319		nfmpt1 4526	. . . . . . . . . . . . . . . . . . . 20 |- F/_ t ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
320	319	nfrn 5235	. . . . . . . . . . . . . . . . . . 19 |- F/_ t ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
321	320	nfcri 2598	. . . . . . . . . . . . . . . . . 18 |- F/ t r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
322	318, 321	nfan 1914	. . . . . . . . . . . . . . . . 17 |- F/ t ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) )
323		nfv 1694	. . . . . . . . . . . . . . . . 17 |- F/ t r e. RR
324		simp3 999	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r = ( X + t ) )
325	95	3ad2ant1 1018	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> X e. RR )
326	238	3ad2ant2 1019	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> t e. RR )
327	325, 326	readdcld 9626	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( X + t ) e. RR )
328	324, 327	eqeltrd 2531	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r e. RR )
329	328	3exp 1196	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> r e. RR ) ) )
330	329	ad2antrr 725	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> r e. RR ) ) )
331	322, 323, 330	rexlimd 2927	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( E. t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) r = ( X + t ) -> r e. RR ) )
332	317, 331	mpd 15	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r e. RR )
333		nfv 1694	. . . . . . . . . . . . . . . . 17 |- F/ t ( Q ` i ) < r
334	258	3adant3 1017	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( Q ` i ) < ( X + t ) )
335		simp3 999	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r = ( X + t ) )
336	334, 335	breqtrrd 4463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( Q ` i ) < r )
337	336	3exp 1196	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> ( Q ` i ) < r ) ) )
338	337	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> ( Q ` i ) < r ) ) )
339	322, 333, 338	rexlimd 2927	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( E. t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) r = ( X + t ) -> ( Q ` i ) < r ) )
340	317, 339	mpd 15	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( Q ` i ) < r )
341		nfv 1694	. . . . . . . . . . . . . . . . 17 |- F/ t r < ( Q ` ( i + 1 ) )
342	267	3adant3 1017	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( X + t ) < ( Q ` ( i + 1 ) ) )
343	335, 342	eqbrtrd 4457	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r < ( Q ` ( i + 1 ) ) )
344	343	3exp 1196	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> r < ( Q ` ( i + 1 ) ) ) ) )
345	344	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> r < ( Q ` ( i + 1 ) ) ) ) )
346	322, 341, 345	rexlimd 2927	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( E. t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) r = ( X + t ) -> r < ( Q ` ( i + 1 ) ) ) )
347	317, 346	mpd 15	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r < ( Q ` ( i + 1 ) ) )
348	311, 312, 332, 340, 347	eliood 31467	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
349	223	ineq2d 3685	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i dom F ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i ( -u pi [,] pi ) ) )
350	349	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i dom F ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i ( -u pi [,] pi ) ) )
351		dmres 5284	. . . . . . . . . . . . . . . . 17 |- dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i dom F )
352	351	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i dom F ) )
353		dfss 3476	. . . . . . . . . . . . . . . . 17 |- ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) <-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i ( -u pi [,] pi ) ) )
354	60, 353	sylib 196	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i ( -u pi [,] pi ) ) )
355	350, 352, 354	3eqtr4d 2494	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
356	355	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
357	348, 356	eleqtrrd 2534	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r e. dom ( F |` ( ( Q