Theorem fourierdlem111

Description: The fourier partial sum for F is the sum of two integrals, with the same integrand involving F and the Dirichlet Kernel D , but on two opposite intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem111.a	|- A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( cos ` ( n x. t ) ) ) _d t / _pi ) )
	fourierdlem111.b	|- B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( sin ` ( n x. t ) ) ) _d t / _pi ) )
	fourierdlem111.s	|- S = ( m e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) )
	fourierdlem111.d	|- D = ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
	fourierdlem111.p	|- 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 ) ) ) } )
	fourierdlem111.m	|- ( ph -> M e. NN )
	fourierdlem111.q	|- ( ph -> Q e. ( P ` M ) )
	fourierdlem111.x	|- ( ph -> X e. RR )
	fourierdlem111.6	|- ( ph -> F : RR --> RR )
	fourierdlem111.fper	|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
	fourierdlem111.g	|- G = ( x e. RR |-> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) )
	fourierdlem111.fcn	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
	fourierdlem111.r	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
	fourierdlem111.l	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
	fourierdlem111.t	|- T = ( 2 x. _pi )
	fourierdlem111.o	|- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u _pi - X ) /\ ( p ` m ) = ( _pi - X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
	fourierdlem111.14	|- W = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )
Assertion	fourierdlem111	|- ( ( ph /\ n e. NN ) -> ( S ` n ) = ( S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s + S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem111.a	|- A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( cos ` ( n x. t ) ) ) _d t / _pi ) )
2		fourierdlem111.b	|- B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( sin ` ( n x. t ) ) ) _d t / _pi ) )
3		fourierdlem111.s	|- S = ( m e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) )
4		fourierdlem111.d	|- D = ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
5		fourierdlem111.p	|- 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 ) ) ) } )
6		fourierdlem111.m	|- ( ph -> M e. NN )
7		fourierdlem111.q	|- ( ph -> Q e. ( P ` M ) )
8		fourierdlem111.x	|- ( ph -> X e. RR )
9		fourierdlem111.6	|- ( ph -> F : RR --> RR )
10		fourierdlem111.fper	|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
11		fourierdlem111.g	|- G = ( x e. RR |-> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) )
12		fourierdlem111.fcn	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
13		fourierdlem111.r	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
14		fourierdlem111.l	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
15		fourierdlem111.t	|- T = ( 2 x. _pi )
16		fourierdlem111.o	|- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u _pi - X ) /\ ( p ` m ) = ( _pi - X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
17		fourierdlem111.14	|- W = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )
18		eleq1	|- ( k = n -> ( k e. NN <-> n e. NN ) )
19	18	anbi2d	|- ( k = n -> ( ( ph /\ k e. NN ) <-> ( ph /\ n e. NN ) ) )
20		fveq2	|- ( k = n -> ( S ` k ) = ( S ` n ) )
21		fveq2	|- ( k = n -> ( D ` k ) = ( D ` n ) )
22	21	fveq1d	|- ( k = n -> ( ( D ` k ) ` ( t - X ) ) = ( ( D ` n ) ` ( t - X ) ) )
23	22	oveq2d	|- ( k = n -> ( ( F ` t ) x. ( ( D ` k ) ` ( t - X ) ) ) = ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
24	23	adantr	|- ( ( k = n /\ t e. ( -u _pi (,) _pi ) ) -> ( ( F ` t ) x. ( ( D ` k ) ` ( t - X ) ) ) = ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
25	24	itgeq2dv	|- ( k = n -> S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( ( D ` k ) ` ( t - X ) ) ) _d t = S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t )
26	20 25	eqeq12d	|- ( k = n -> ( ( S ` k ) = S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( ( D ` k ) ` ( t - X ) ) ) _d t <-> ( S ` n ) = S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t ) )
27	19 26	imbi12d	|- ( k = n -> ( ( ( ph /\ k e. NN ) -> ( S ` k ) = S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( ( D ` k ) ` ( t - X ) ) ) _d t ) <-> ( ( ph /\ n e. NN ) -> ( S ` n ) = S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t ) ) )
28	9	adantr	|- ( ( ph /\ k e. NN ) -> F : RR --> RR )
29		eqid	|- ( -u _pi (,) _pi ) = ( -u _pi (,) _pi )
30		ioossre	|- ( -u _pi (,) _pi ) C_ RR
31	30	a1i	|- ( ph -> ( -u _pi (,) _pi ) C_ RR )
32	9 31	feqresmpt	|- ( ph -> ( F |` ( -u _pi (,) _pi ) ) = ( x e. ( -u _pi (,) _pi ) |-> ( F ` x ) ) )
33		ioossicc	|- ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi )
34	33	a1i	|- ( ph -> ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi ) )
35		ioombl	|- ( -u _pi (,) _pi ) e. dom vol
36	35	a1i	|- ( ph -> ( -u _pi (,) _pi ) e. dom vol )
37	9	adantr	|- ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> F : RR --> RR )
38		pire	|- _pi e. RR
39	38	renegcli	|- -u _pi e. RR
40	39 38	elicc2i	|- ( t e. ( -u _pi [,] _pi ) <-> ( t e. RR /\ -u _pi <_ t /\ t <_ _pi ) )
41	40	simp1bi	|- ( t e. ( -u _pi [,] _pi ) -> t e. RR )
42	41	ssriv	|- ( -u _pi [,] _pi ) C_ RR
43	42	a1i	|- ( ph -> ( -u _pi [,] _pi ) C_ RR )
44	43	sselda	|- ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> x e. RR )
45	37 44	ffvelrnd	|- ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> ( F ` x ) e. RR )
46	9 43	feqresmpt	|- ( ph -> ( F |` ( -u _pi [,] _pi ) ) = ( x e. ( -u _pi [,] _pi ) |-> ( F ` x ) ) )
47		ax-resscn	|- RR C_ CC
48	47	a1i	|- ( ph -> RR C_ CC )
49	9 48	fssd	|- ( ph -> F : RR --> CC )
50	49 43	fssresd	|- ( ph -> ( F |` ( -u _pi [,] _pi ) ) : ( -u _pi [,] _pi ) --> CC )
51		ioossicc	|- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
52	39	rexri	|- -u _pi e. RR*
53	52	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> -u _pi e. RR* )
54	38	rexri	|- _pi e. RR*
55	54	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> _pi e. RR* )
56	5 6 7	fourierdlem15	|- ( ph -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
57	56	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
58		simpr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
59	53 55 57 58	fourierdlem8	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
60	51 59	sstrid	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
61	60	resabs1d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
62	61 12	eqeltrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
63	61	oveq1d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
64	13 63	eleqtrrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
65	61	oveq1d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
66	14 65	eleqtrrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
67	5 6 7 50 62 64 66	fourierdlem69	|- ( ph -> ( F |` ( -u _pi [,] _pi ) ) e. L^1 )
68	46 67	eqeltrrd	|- ( ph -> ( x e. ( -u _pi [,] _pi ) |-> ( F ` x ) ) e. L^1 )
69	34 36 45 68	iblss	|- ( ph -> ( x e. ( -u _pi (,) _pi ) |-> ( F ` x ) ) e. L^1 )
70	32 69	eqeltrd	|- ( ph -> ( F |` ( -u _pi (,) _pi ) ) e. L^1 )
71	70	adantr	|- ( ( ph /\ k e. NN ) -> ( F |` ( -u _pi (,) _pi ) ) e. L^1 )
72	8	adantr	|- ( ( ph /\ k e. NN ) -> X e. RR )
73		simpr	|- ( ( ph /\ k e. NN ) -> k e. NN )
74	28 29 71 1 2 72 3 4 73	fourierdlem83	|- ( ( ph /\ k e. NN ) -> ( S ` k ) = S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( ( D ` k ) ` ( t - X ) ) ) _d t )
75	27 74	chvarvv	|- ( ( ph /\ n e. NN ) -> ( S ` n ) = S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t )
76	39	a1i	|- ( ( ph /\ n e. NN ) -> -u _pi e. RR )
77	38	a1i	|- ( ( ph /\ n e. NN ) -> _pi e. RR )
78	49	adantr	|- ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> F : RR --> CC )
79	41	adantl	|- ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> t e. RR )
80	78 79	ffvelrnd	|- ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> ( F ` t ) e. CC )
81	80	adantlr	|- ( ( ( ph /\ n e. NN ) /\ t e. ( -u _pi [,] _pi ) ) -> ( F ` t ) e. CC )
82	4	dirkerf	|- ( n e. NN -> ( D ` n ) : RR --> RR )
83	82	ad2antlr	|- ( ( ( ph /\ n e. NN ) /\ t e. ( -u _pi [,] _pi ) ) -> ( D ` n ) : RR --> RR )
84	8	adantr	|- ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> X e. RR )
85	79 84	resubcld	|- ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> ( t - X ) e. RR )
86	85	adantlr	|- ( ( ( ph /\ n e. NN ) /\ t e. ( -u _pi [,] _pi ) ) -> ( t - X ) e. RR )
87	83 86	ffvelrnd	|- ( ( ( ph /\ n e. NN ) /\ t e. ( -u _pi [,] _pi ) ) -> ( ( D ` n ) ` ( t - X ) ) e. RR )
88	87	recnd	|- ( ( ( ph /\ n e. NN ) /\ t e. ( -u _pi [,] _pi ) ) -> ( ( D ` n ) ` ( t - X ) ) e. CC )
89	81 88	mulcld	|- ( ( ( ph /\ n e. NN ) /\ t e. ( -u _pi [,] _pi ) ) -> ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) e. CC )
90	76 77 89	itgioo	|- ( ( ph /\ n e. NN ) -> S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t = S. ( -u _pi [,] _pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t )
91		fvres	|- ( t e. ( -u _pi [,] _pi ) -> ( ( F |` ( -u _pi [,] _pi ) ) ` t ) = ( F ` t ) )
92	91	eqcomd	|- ( t e. ( -u _pi [,] _pi ) -> ( F ` t ) = ( ( F |` ( -u _pi [,] _pi ) ) ` t ) )
93	92	oveq1d	|- ( t e. ( -u _pi [,] _pi ) -> ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) = ( ( ( F |` ( -u _pi [,] _pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
94	93	adantl	|- ( ( ( ph /\ n e. NN ) /\ t e. ( -u _pi [,] _pi ) ) -> ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) = ( ( ( F |` ( -u _pi [,] _pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
95	94	itgeq2dv	|- ( ( ph /\ n e. NN ) -> S. ( -u _pi [,] _pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t = S. ( -u _pi [,] _pi ) ( ( ( F |` ( -u _pi [,] _pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t )
96		simpl	|- ( ( n = m /\ y e. RR ) -> n = m )
97	96	oveq2d	|- ( ( n = m /\ y e. RR ) -> ( 2 x. n ) = ( 2 x. m ) )
98	97	oveq1d	|- ( ( n = m /\ y e. RR ) -> ( ( 2 x. n ) + 1 ) = ( ( 2 x. m ) + 1 ) )
99	98	oveq1d	|- ( ( n = m /\ y e. RR ) -> ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) = ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) )
100	96	oveq1d	|- ( ( n = m /\ y e. RR ) -> ( n + ( 1 / 2 ) ) = ( m + ( 1 / 2 ) ) )
101	100	oveq1d	|- ( ( n = m /\ y e. RR ) -> ( ( n + ( 1 / 2 ) ) x. y ) = ( ( m + ( 1 / 2 ) ) x. y ) )
102	101	fveq2d	|- ( ( n = m /\ y e. RR ) -> ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) = ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) )
103	102	oveq1d	|- ( ( n = m /\ y e. RR ) -> ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) )
104	99 103	ifeq12d	|- ( ( n = m /\ y e. RR ) -> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
105	104	mpteq2dva	|- ( n = m -> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) = ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
106	105	cbvmptv	|- ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) ) = ( m e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
107	4 106	eqtri	|- D = ( m e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
108		fveq2	|- ( s = t -> ( ( F |` ( -u _pi [,] _pi ) ) ` s ) = ( ( F |` ( -u _pi [,] _pi ) ) ` t ) )
109		oveq1	|- ( s = t -> ( s - X ) = ( t - X ) )
110	109	fveq2d	|- ( s = t -> ( ( D ` n ) ` ( s - X ) ) = ( ( D ` n ) ` ( t - X ) ) )
111	108 110	oveq12d	|- ( s = t -> ( ( ( F |` ( -u _pi [,] _pi ) ) ` s ) x. ( ( D ` n ) ` ( s - X ) ) ) = ( ( ( F |` ( -u _pi [,] _pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
112	111	cbvmptv	|- ( s e. ( -u _pi [,] _pi ) |-> ( ( ( F |` ( -u _pi [,] _pi ) ) ` s ) x. ( ( D ` n ) ` ( s - X ) ) ) ) = ( t e. ( -u _pi [,] _pi ) |-> ( ( ( F |` ( -u _pi [,] _pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) )
113	7	adantr	|- ( ( ph /\ n e. NN ) -> Q e. ( P ` M ) )
114	6	adantr	|- ( ( ph /\ n e. NN ) -> M e. NN )
115		simpr	|- ( ( ph /\ n e. NN ) -> n e. NN )
116	8	adantr	|- ( ( ph /\ n e. NN ) -> X e. RR )
117	50	adantr	|- ( ( ph /\ n e. NN ) -> ( F |` ( -u _pi [,] _pi ) ) : ( -u _pi [,] _pi ) --> CC )
118	62	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
119	64	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> R e. ( ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
120	66	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> L e. ( ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
121	107 5 112 113 114 115 116 117 118 119 120	fourierdlem101	|- ( ( ph /\ n e. NN ) -> S. ( -u _pi [,] _pi ) ( ( ( F |` ( -u _pi [,] _pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( ( ( F |` ( -u _pi [,] _pi ) ) ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y )
122		oveq2	|- ( s = y -> ( X + s ) = ( X + y ) )
123	122	fveq2d	|- ( s = y -> ( F ` ( X + s ) ) = ( F ` ( X + y ) ) )
124		fveq2	|- ( s = y -> ( ( D ` n ) ` s ) = ( ( D ` n ) ` y ) )
125	123 124	oveq12d	|- ( s = y -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) )
126	125	cbvitgv	|- S. ( ( -u _pi - X ) (,) ( _pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s = S. ( ( -u _pi - X ) (,) ( _pi - X ) ) ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y
127	126	a1i	|- ( ( ph /\ n e. NN ) -> S. ( ( -u _pi - X ) (,) ( _pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s = S. ( ( -u _pi - X ) (,) ( _pi - X ) ) ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y )
128	39	a1i	|- ( ph -> -u _pi e. RR )
129	128 8	resubcld	|- ( ph -> ( -u _pi - X ) e. RR )
130	129	adantr	|- ( ( ph /\ n e. NN ) -> ( -u _pi - X ) e. RR )
131	38	a1i	|- ( ph -> _pi e. RR )
132	131 8	resubcld	|- ( ph -> ( _pi - X ) e. RR )
133	132	adantr	|- ( ( ph /\ n e. NN ) -> ( _pi - X ) e. RR )
134	49	adantr	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> F : RR --> CC )
135	8	adantr	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> X e. RR )
136		simpr	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) )
137	129	adantr	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( -u _pi - X ) e. RR )
138	132	adantr	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( _pi - X ) e. RR )
139		elicc2	|- ( ( ( -u _pi - X ) e. RR /\ ( _pi - X ) e. RR ) -> ( y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) <-> ( y e. RR /\ ( -u _pi - X ) <_ y /\ y <_ ( _pi - X ) ) ) )
140	137 138 139	syl2anc	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) <-> ( y e. RR /\ ( -u _pi - X ) <_ y /\ y <_ ( _pi - X ) ) ) )
141	136 140	mpbid	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( y e. RR /\ ( -u _pi - X ) <_ y /\ y <_ ( _pi - X ) ) )
142	141	simp1d	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> y e. RR )
143	135 142	readdcld	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + y ) e. RR )
144	134 143	ffvelrnd	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( F ` ( X + y ) ) e. CC )
145	144	adantlr	|- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( F ` ( X + y ) ) e. CC )
146	82	ad2antlr	|- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( D ` n ) : RR --> RR )
147	142	adantlr	|- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> y e. RR )
148	146 147	ffvelrnd	|- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( ( D ` n ) ` y ) e. RR )
149	148	recnd	|- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( ( D ` n ) ` y ) e. CC )
150	145 149	mulcld	|- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) e. CC )
151	130 133 150	itgioo	|- ( ( ph /\ n e. NN ) -> S. ( ( -u _pi - X ) (,) ( _pi - X ) ) ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y )
152	39	a1i	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> -u _pi e. RR )
153	38	a1i	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> _pi e. RR )
154	8	recnd	|- ( ph -> X e. CC )
155	131	recnd	|- ( ph -> _pi e. CC )
156	155	negcld	|- ( ph -> -u _pi e. CC )
157	154 156	pncan3d	|- ( ph -> ( X + ( -u _pi - X ) ) = -u _pi )
158	157	eqcomd	|- ( ph -> -u _pi = ( X + ( -u _pi - X ) ) )
159	158	adantr	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> -u _pi = ( X + ( -u _pi - X ) ) )
160	141	simp2d	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( -u _pi - X ) <_ y )
161	137 142 135 160	leadd2dd	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + ( -u _pi - X ) ) <_ ( X + y ) )
162	159 161	eqbrtrd	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> -u _pi <_ ( X + y ) )
163	141	simp3d	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> y <_ ( _pi - X ) )
164	142 138 135 163	leadd2dd	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + y ) <_ ( X + ( _pi - X ) ) )
165	154	adantr	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> X e. CC )
166	155	adantr	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> _pi e. CC )
167	165 166	pncan3d	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + ( _pi - X ) ) = _pi )
168	164 167	breqtrd	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + y ) <_ _pi )
169	152 153 143 162 168	eliccd	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + y ) e. ( -u _pi [,] _pi ) )
170		fvres	|- ( ( X + y ) e. ( -u _pi [,] _pi ) -> ( ( F |` ( -u _pi [,] _pi ) ) ` ( X + y ) ) = ( F ` ( X + y ) ) )
171	169 170	syl	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( ( F |` ( -u _pi [,] _pi ) ) ` ( X + y ) ) = ( F ` ( X + y ) ) )
172	171	eqcomd	|- ( ( ph /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( F ` ( X + y ) ) = ( ( F |` ( -u _pi [,] _pi ) ) ` ( X + y ) ) )
173	172	adantlr	|- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( F ` ( X + y ) ) = ( ( F |` ( -u _pi [,] _pi ) ) ` ( X + y ) ) )
174	173	oveq1d	|- ( ( ( ph /\ n e. NN ) /\ y e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) = ( ( ( F |` ( -u _pi [,] _pi ) ) ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) )
175	174	itgeq2dv	|- ( ( ph /\ n e. NN ) -> S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( ( F ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( ( ( F |` ( -u _pi [,] _pi ) ) ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y )
176	127 151 175	3eqtrrd	|- ( ( ph /\ n e. NN ) -> S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( ( ( F |` ( -u _pi [,] _pi ) ) ` ( X + y ) ) x. ( ( D ` n ) ` y ) ) _d y = S. ( ( -u _pi - X ) (,) ( _pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
177	121 176	eqtrd	|- ( ( ph /\ n e. NN ) -> S. ( -u _pi [,] _pi ) ( ( ( F |` ( -u _pi [,] _pi ) ) ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t = S. ( ( -u _pi - X ) (,) ( _pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
178	90 95 177	3eqtrd	|- ( ( ph /\ n e. NN ) -> S. ( -u _pi (,) _pi ) ( ( F ` t ) x. ( ( D ` n ) ` ( t - X ) ) ) _d t = S. ( ( -u _pi - X ) (,) ( _pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
179		elioore	|- ( s e. ( ( -u _pi - X ) (,) ( _pi - X ) ) -> s e. RR )
180	179	adantl	|- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u _pi - X ) (,) ( _pi - X ) ) ) -> s e. RR )
181	49	adantr	|- ( ( ph /\ s e. ( ( -u _pi - X ) (,) ( _pi - X ) ) ) -> F : RR --> CC )
182	8	adantr	|- ( ( ph /\ s e. ( ( -u _pi - X ) (,) ( _pi - X ) ) ) -> X e. RR )
183	179	adantl	|- ( ( ph /\ s e. ( ( -u _pi - X ) (,) ( _pi - X ) ) ) -> s e. RR )
184	182 183	readdcld	|- ( ( ph /\ s e. ( ( -u _pi - X ) (,) ( _pi - X ) ) ) -> ( X + s ) e. RR )
185	181 184	ffvelrnd	|- ( ( ph /\ s e. ( ( -u _pi - X ) (,) ( _pi - X ) ) ) -> ( F ` ( X + s ) ) e. CC )
186	185	adantlr	|- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u _pi - X ) (,) ( _pi - X ) ) ) -> ( F ` ( X + s ) ) e. CC )
187	82	ad2antlr	|- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u _pi - X ) (,) ( _pi - X ) ) ) -> ( D ` n ) : RR --> RR )
188	187 180	ffvelrnd	|- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u _pi - X ) (,) ( _pi - X ) ) ) -> ( ( D ` n ) ` s ) e. RR )
189	188	recnd	|- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u _pi - X ) (,) ( _pi - X ) ) ) -> ( ( D ` n ) ` s ) e. CC )
190	186 189	mulcld	|- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u _pi - X ) (,) ( _pi - X ) ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. CC )
191		oveq2	|- ( x = s -> ( X + x ) = ( X + s ) )
192	191	fveq2d	|- ( x = s -> ( F ` ( X + x ) ) = ( F ` ( X + s ) ) )
193		fveq2	|- ( x = s -> ( ( D ` n ) ` x ) = ( ( D ` n ) ` s ) )
194	192 193	oveq12d	|- ( x = s -> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
195	194	cbvmptv	|- ( x e. RR |-> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) ) = ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
196	11 195	eqtri	|- G = ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
197	196	fvmpt2	|- ( ( s e. RR /\ ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. CC ) -> ( G ` s ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
198	180 190 197	syl2anc	|- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u _pi - X ) (,) ( _pi - X ) ) ) -> ( G ` s ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
199	198	eqcomd	|- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u _pi - X ) (,) ( _pi - X ) ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( G ` s ) )
200	199	itgeq2dv	|- ( ( ph /\ n e. NN ) -> S. ( ( -u _pi - X ) (,) ( _pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s = S. ( ( -u _pi - X ) (,) ( _pi - X ) ) ( G ` s ) _d s )
201	49	adantr	|- ( ( ph /\ x e. RR ) -> F : RR --> CC )
202	8	adantr	|- ( ( ph /\ x e. RR ) -> X e. RR )
203		simpr	|- ( ( ph /\ x e. RR ) -> x e. RR )
204	202 203	readdcld	|- ( ( ph /\ x e. RR ) -> ( X + x ) e. RR )
205	201 204	ffvelrnd	|- ( ( ph /\ x e. RR ) -> ( F ` ( X + x ) ) e. CC )
206	205	adantlr	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( F ` ( X + x ) ) e. CC )
207	82	adantl	|- ( ( ph /\ n e. NN ) -> ( D ` n ) : RR --> RR )
208	207	ffvelrnda	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` x ) e. RR )
209	208	recnd	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` x ) e. CC )
210	206 209	mulcld	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) e. CC )
211	210 11	fmptd	|- ( ( ph /\ n e. NN ) -> G : RR --> CC )
212	211	adantr	|- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> G : RR --> CC )
213	129	adantr	|- ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( -u _pi - X ) e. RR )
214	132	adantr	|- ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( _pi - X ) e. RR )
215		simpr	|- ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) )
216		eliccre	|- ( ( ( -u _pi - X ) e. RR /\ ( _pi - X ) e. RR /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> s e. RR )
217	213 214 215 216	syl3anc	|- ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> s e. RR )
218	217	adantlr	|- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> s e. RR )
219	212 218	ffvelrnd	|- ( ( ( ph /\ n e. NN ) /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( G ` s ) e. CC )
220	130 133 219	itgioo	|- ( ( ph /\ n e. NN ) -> S. ( ( -u _pi - X ) (,) ( _pi - X ) ) ( G ` s ) _d s = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( G ` s ) _d s )
221		fveq2	|- ( s = x -> ( G ` s ) = ( G ` x ) )
222	221	cbvitgv	|- S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( G ` s ) _d s = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( G ` x ) _d x
223	220 222	eqtrdi	|- ( ( ph /\ n e. NN ) -> S. ( ( -u _pi - X ) (,) ( _pi - X ) ) ( G ` s ) _d s = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( G ` x ) _d x )
224	200 223	eqtrd	|- ( ( ph /\ n e. NN ) -> S. ( ( -u _pi - X ) (,) ( _pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( G ` x ) _d x )
225		eqid	|- ( ( _pi - X ) - ( -u _pi - X ) ) = ( ( _pi - X ) - ( -u _pi - X ) )
226	116	renegcld	|- ( ( ph /\ n e. NN ) -> -u X e. RR )
227	5	fourierdlem2	|- ( 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 ) ) ) ) ) )
228	6 227	syl	|- ( 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 ) ) ) ) ) )
229	7 228	mpbid	|- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
230	229	simpld	|- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
231		elmapi	|- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
232	230 231	syl	|- ( ph -> Q : ( 0 ... M ) --> RR )
233	232	ffvelrnda	|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
234	8	adantr	|- ( ( ph /\ i e. ( 0 ... M ) ) -> X e. RR )
235	233 234	resubcld	|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( Q ` i ) - X ) e. RR )
236	235 17	fmptd	|- ( ph -> W : ( 0 ... M ) --> RR )
237		reex	|- RR e. _V
238		ovex	|- ( 0 ... M ) e. _V
239	237 238	pm3.2i	|- ( RR e. _V /\ ( 0 ... M ) e. _V )
240		elmapg	|- ( ( RR e. _V /\ ( 0 ... M ) e. _V ) -> ( W e. ( RR ^m ( 0 ... M ) ) <-> W : ( 0 ... M ) --> RR ) )
241	239 240	mp1i	|- ( ph -> ( W e. ( RR ^m ( 0 ... M ) ) <-> W : ( 0 ... M ) --> RR ) )
242	236 241	mpbird	|- ( ph -> W e. ( RR ^m ( 0 ... M ) ) )
243	17	a1i	|- ( ph -> W = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) )
244		fveq2	|- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
245	229	simprd	|- ( ph -> ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
246	245	simpld	|- ( ph -> ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) )
247	246	simpld	|- ( ph -> ( Q ` 0 ) = -u _pi )
248	244 247	sylan9eqr	|- ( ( ph /\ i = 0 ) -> ( Q ` i ) = -u _pi )
249	248	oveq1d	|- ( ( ph /\ i = 0 ) -> ( ( Q ` i ) - X ) = ( -u _pi - X ) )
250		0zd	|- ( ph -> 0 e. ZZ )
251	6	nnzd	|- ( ph -> M e. ZZ )
252		0red	|- ( M e. NN -> 0 e. RR )
253		nnre	|- ( M e. NN -> M e. RR )
254		nngt0	|- ( M e. NN -> 0 < M )
255	252 253 254	ltled	|- ( M e. NN -> 0 <_ M )
256	6 255	syl	|- ( ph -> 0 <_ M )
257		eluz2	|- ( M e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 <_ M ) )
258	250 251 256 257	syl3anbrc	|- ( ph -> M e. ( ZZ>= ` 0 ) )
259		eluzfz1	|- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
260	258 259	syl	|- ( ph -> 0 e. ( 0 ... M ) )
261	243 249 260 129	fvmptd	|- ( ph -> ( W ` 0 ) = ( -u _pi - X ) )
262		fveq2	|- ( i = M -> ( Q ` i ) = ( Q ` M ) )
263	246	simprd	|- ( ph -> ( Q ` M ) = _pi )
264	262 263	sylan9eqr	|- ( ( ph /\ i = M ) -> ( Q ` i ) = _pi )
265	264	oveq1d	|- ( ( ph /\ i = M ) -> ( ( Q ` i ) - X ) = ( _pi - X ) )
266		eluzfz2	|- ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
267	258 266	syl	|- ( ph -> M e. ( 0 ... M ) )
268	243 265 267 132	fvmptd	|- ( ph -> ( W ` M ) = ( _pi - X ) )
269	261 268	jca	|- ( ph -> ( ( W ` 0 ) = ( -u _pi - X ) /\ ( W ` M ) = ( _pi - X ) ) )
270	232	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
271		elfzofz	|- ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
272	271	adantl	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
273	270 272	ffvelrnd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
274		fzofzp1	|- ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
275	274	adantl	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
276	270 275	ffvelrnd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
277	8	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. RR )
278	245	simprd	|- ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
279	278	r19.21bi	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
280	273 276 277 279	ltsub1dd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) - X ) < ( ( Q ` ( i + 1 ) ) - X ) )
281	272 235	syldan	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) - X ) e. RR )
282	17	fvmpt2	|- ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) - X ) e. RR ) -> ( W ` i ) = ( ( Q ` i ) - X ) )
283	272 281 282	syl2anc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( W ` i ) = ( ( Q ` i ) - X ) )
284		fveq2	|- ( i = j -> ( Q ` i ) = ( Q ` j ) )
285	284	oveq1d	|- ( i = j -> ( ( Q ` i ) - X ) = ( ( Q ` j ) - X ) )
286	285	cbvmptv	|- ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
287	17 286	eqtri	|- W = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
288	287	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> W = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) ) )
289		fveq2	|- ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
290	289	oveq1d	|- ( j = ( i + 1 ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
291	290	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
292	276 277	resubcld	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) - X ) e. RR )
293	288 291 275 292	fvmptd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( W ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) - X ) )
294	280 283 293	3brtr4d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( W ` i ) < ( W ` ( i + 1 ) ) )
295	294	ralrimiva	|- ( ph -> A. i e. ( 0 ..^ M ) ( W ` i ) < ( W ` ( i + 1 ) ) )
296	242 269 295	jca32	|- ( ph -> ( W e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( W ` 0 ) = ( -u _pi - X ) /\ ( W ` M ) = ( _pi - X ) ) /\ A. i e. ( 0 ..^ M ) ( W ` i ) < ( W ` ( i + 1 ) ) ) ) )
297	16	fourierdlem2	|- ( M e. NN -> ( W e. ( O ` M ) <-> ( W e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( W ` 0 ) = ( -u _pi - X ) /\ ( W ` M ) = ( _pi - X ) ) /\ A. i e. ( 0 ..^ M ) ( W ` i ) < ( W ` ( i + 1 ) ) ) ) ) )
298	6 297	syl	|- ( ph -> ( W e. ( O ` M ) <-> ( W e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( W ` 0 ) = ( -u _pi - X ) /\ ( W ` M ) = ( _pi - X ) ) /\ A. i e. ( 0 ..^ M ) ( W ` i ) < ( W ` ( i + 1 ) ) ) ) ) )
299	296 298	mpbird	|- ( ph -> W e. ( O ` M ) )
300	299	adantr	|- ( ( ph /\ n e. NN ) -> W e. ( O ` M ) )
301	155 156 154	nnncan2d	|- ( ph -> ( ( _pi - X ) - ( -u _pi - X ) ) = ( _pi - -u _pi ) )
302		picn	|- _pi e. CC
303	302	2timesi	|- ( 2 x. _pi ) = ( _pi + _pi )
304	302 302	subnegi	|- ( _pi - -u _pi ) = ( _pi + _pi )
305	303 15 304	3eqtr4i	|- T = ( _pi - -u _pi )
306	301 305	eqtr4di	|- ( ph -> ( ( _pi - X ) - ( -u _pi - X ) ) = T )
307	306	oveq2d	|- ( ph -> ( x + ( ( _pi - X ) - ( -u _pi - X ) ) ) = ( x + T ) )
308	307	fveq2d	|- ( ph -> ( G ` ( x + ( ( _pi - X ) - ( -u _pi - X ) ) ) ) = ( G ` ( x + T ) ) )
309	308	ad2antrr	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` ( x + ( ( _pi - X ) - ( -u _pi - X ) ) ) ) = ( G ` ( x + T ) ) )
310		simpr	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> x e. RR )
311	11	fvmpt2	|- ( ( x e. RR /\ ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) e. CC ) -> ( G ` x ) = ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) )
312	310 210 311	syl2anc	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` x ) = ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) )
313	154	adantr	|- ( ( ph /\ x e. RR ) -> X e. CC )
314	203	recnd	|- ( ( ph /\ x e. RR ) -> x e. CC )
315		2re	|- 2 e. RR
316	315 38	remulcli	|- ( 2 x. _pi ) e. RR
317	15 316	eqeltri	|- T e. RR
318	317	a1i	|- ( ph -> T e. RR )
319	318	recnd	|- ( ph -> T e. CC )
320	319	adantr	|- ( ( ph /\ x e. RR ) -> T e. CC )
321	313 314 320	addassd	|- ( ( ph /\ x e. RR ) -> ( ( X + x ) + T ) = ( X + ( x + T ) ) )
322	321	eqcomd	|- ( ( ph /\ x e. RR ) -> ( X + ( x + T ) ) = ( ( X + x ) + T ) )
323	322	fveq2d	|- ( ( ph /\ x e. RR ) -> ( F ` ( X + ( x + T ) ) ) = ( F ` ( ( X + x ) + T ) ) )
324		simpl	|- ( ( ph /\ x e. RR ) -> ph )
325	324 204	jca	|- ( ( ph /\ x e. RR ) -> ( ph /\ ( X + x ) e. RR ) )
326		eleq1	|- ( s = ( X + x ) -> ( s e. RR <-> ( X + x ) e. RR ) )
327	326	anbi2d	|- ( s = ( X + x ) -> ( ( ph /\ s e. RR ) <-> ( ph /\ ( X + x ) e. RR ) ) )
328		oveq1	|- ( s = ( X + x ) -> ( s + T ) = ( ( X + x ) + T ) )
329	328	fveq2d	|- ( s = ( X + x ) -> ( F ` ( s + T ) ) = ( F ` ( ( X + x ) + T ) ) )
330		fveq2	|- ( s = ( X + x ) -> ( F ` s ) = ( F ` ( X + x ) ) )
331	329 330	eqeq12d	|- ( s = ( X + x ) -> ( ( F ` ( s + T ) ) = ( F ` s ) <-> ( F ` ( ( X + x ) + T ) ) = ( F ` ( X + x ) ) ) )
332	327 331	imbi12d	|- ( s = ( X + x ) -> ( ( ( ph /\ s e. RR ) -> ( F ` ( s + T ) ) = ( F ` s ) ) <-> ( ( ph /\ ( X + x ) e. RR ) -> ( F ` ( ( X + x ) + T ) ) = ( F ` ( X + x ) ) ) ) )
333		eleq1	|- ( x = s -> ( x e. RR <-> s e. RR ) )
334	333	anbi2d	|- ( x = s -> ( ( ph /\ x e. RR ) <-> ( ph /\ s e. RR ) ) )
335		oveq1	|- ( x = s -> ( x + T ) = ( s + T ) )
336	335	fveq2d	|- ( x = s -> ( F ` ( x + T ) ) = ( F ` ( s + T ) ) )
337		fveq2	|- ( x = s -> ( F ` x ) = ( F ` s ) )
338	336 337	eqeq12d	|- ( x = s -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( s + T ) ) = ( F ` s ) ) )
339	334 338	imbi12d	|- ( x = s -> ( ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ s e. RR ) -> ( F ` ( s + T ) ) = ( F ` s ) ) ) )
340	339 10	chvarvv	|- ( ( ph /\ s e. RR ) -> ( F ` ( s + T ) ) = ( F ` s ) )
341	332 340	vtoclg	|- ( ( X + x ) e. RR -> ( ( ph /\ ( X + x ) e. RR ) -> ( F ` ( ( X + x ) + T ) ) = ( F ` ( X + x ) ) ) )
342	204 325 341	sylc	|- ( ( ph /\ x e. RR ) -> ( F ` ( ( X + x ) + T ) ) = ( F ` ( X + x ) ) )
343	323 342	eqtr2d	|- ( ( ph /\ x e. RR ) -> ( F ` ( X + x ) ) = ( F ` ( X + ( x + T ) ) ) )
344	343	adantlr	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( F ` ( X + x ) ) = ( F ` ( X + ( x + T ) ) ) )
345	4 15	dirkerper	|- ( ( n e. NN /\ x e. RR ) -> ( ( D ` n ) ` ( x + T ) ) = ( ( D ` n ) ` x ) )
346	345	eqcomd	|- ( ( n e. NN /\ x e. RR ) -> ( ( D ` n ) ` x ) = ( ( D ` n ) ` ( x + T ) ) )
347	346	adantll	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` x ) = ( ( D ` n ) ` ( x + T ) ) )
348	344 347	oveq12d	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) = ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) )
349	196	a1i	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> G = ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) )
350		oveq2	|- ( s = ( x + T ) -> ( X + s ) = ( X + ( x + T ) ) )
351	350	fveq2d	|- ( s = ( x + T ) -> ( F ` ( X + s ) ) = ( F ` ( X + ( x + T ) ) ) )
352		fveq2	|- ( s = ( x + T ) -> ( ( D ` n ) ` s ) = ( ( D ` n ) ` ( x + T ) ) )
353	351 352	oveq12d	|- ( s = ( x + T ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) )
354	353	adantl	|- ( ( ( ( ph /\ n e. NN ) /\ x e. RR ) /\ s = ( x + T ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) )
355	317	a1i	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> T e. RR )
356	310 355	readdcld	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( x + T ) e. RR )
357	317	a1i	|- ( ( ph /\ x e. RR ) -> T e. RR )
358	203 357	readdcld	|- ( ( ph /\ x e. RR ) -> ( x + T ) e. RR )
359	202 358	readdcld	|- ( ( ph /\ x e. RR ) -> ( X + ( x + T ) ) e. RR )
360	201 359	ffvelrnd	|- ( ( ph /\ x e. RR ) -> ( F ` ( X + ( x + T ) ) ) e. CC )
361	360	adantlr	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( F ` ( X + ( x + T ) ) ) e. CC )
362	82	ad2antlr	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( D ` n ) : RR --> RR )
363	362 356	ffvelrnd	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` ( x + T ) ) e. RR )
364	363	recnd	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( D ` n ) ` ( x + T ) ) e. CC )
365	361 364	mulcld	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) e. CC )
366	349 354 356 365	fvmptd	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` ( x + T ) ) = ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) )
367	366	eqcomd	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( ( F ` ( X + ( x + T ) ) ) x. ( ( D ` n ) ` ( x + T ) ) ) = ( G ` ( x + T ) ) )
368	312 348 367	3eqtrrd	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` ( x + T ) ) = ( G ` x ) )
369	309 368	eqtrd	|- ( ( ( ph /\ n e. NN ) /\ x e. RR ) -> ( G ` ( x + ( ( _pi - X ) - ( -u _pi - X ) ) ) ) = ( G ` x ) )
370	196	reseq1i	|- ( G |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) )
371	370	a1i	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) )
372		ioossre	|- ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) C_ RR
373		resmpt	|- ( ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) C_ RR -> ( ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) )
374	372 373	ax-mp	|- ( ( s e. RR |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
375	371 374	eqtrdi	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) )
376	273	rexrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
377	376	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
378	276	rexrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
379	378	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
380	8	adantr	|- ( ( ph /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> X e. RR )
381		elioore	|- ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) -> s e. RR )
382	381	adantl	|- ( ( ph /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> s e. RR )
383	380 382	readdcld	|- ( ( ph /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + s ) e. RR )
384	383	adantlr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + s ) e. RR )
385		eleq1	|- ( x = s -> ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) <-> s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) )
386	385	anbi2d	|- ( x = s -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) <-> ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) ) )
387	191	breq2d	|- ( x = s -> ( ( Q ` i ) < ( X + x ) <-> ( Q ` i ) < ( X + s ) ) )
388	386 387	imbi12d	|- ( x = s -> ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + x ) ) <-> ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + s ) ) ) )
389	154	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. CC )
390	283 281	eqeltrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( W ` i ) e. RR )
391	390	recnd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( W ` i ) e. CC )
392	389 391	addcomd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( W ` i ) ) = ( ( W ` i ) + X ) )
393	283	oveq1d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( W ` i ) + X ) = ( ( ( Q ` i ) - X ) + X ) )
394	273	recnd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
395	394 389	npcand	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) - X ) + X ) = ( Q ` i ) )
396	392 393 395	3eqtrrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( X + ( W ` i ) ) )
397	396	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) = ( X + ( W ` i ) ) )
398	390	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` i ) e. RR )
399		elioore	|- ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) -> x e. RR )
400	399	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> x e. RR )
401	8	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> X e. RR )
402	390	rexrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( W ` i ) e. RR* )
403	402	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` i ) e. RR* )
404	293 292	eqeltrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( W ` ( i + 1 ) ) e. RR )
405	404	rexrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( W ` ( i + 1 ) ) e. RR* )
406	405	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` ( i + 1 ) ) e. RR* )
407		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) )
408		ioogtlb	|- ( ( ( W ` i ) e. RR* /\ ( W ` ( i + 1 ) ) e. RR* /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` i ) < x )
409	403 406 407 408	syl3anc	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` i ) < x )
410	398 400 401 409	ltadd2dd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + ( W ` i ) ) < ( X + x ) )
411	397 410	eqbrtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + x ) )
412	388 411	chvarvv	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + s ) )
413	191	breq1d	|- ( x = s -> ( ( X + x ) < ( Q ` ( i + 1 ) ) <-> ( X + s ) < ( Q ` ( i + 1 ) ) ) )
414	386 413	imbi12d	|- ( x = s -> ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + x ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + s ) < ( Q ` ( i + 1 ) ) ) ) )
415	404	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` ( i + 1 ) ) e. RR )
416		iooltub	|- ( ( ( W ` i ) e. RR* /\ ( W ` ( i + 1 ) ) e. RR* /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> x < ( W ` ( i + 1 ) ) )
417	403 406 407 416	syl3anc	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> x < ( W ` ( i + 1 ) ) )
418	400 415 401 417	ltadd2dd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + x ) < ( X + ( W ` ( i + 1 ) ) ) )
419	404	recnd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( W ` ( i + 1 ) ) e. CC )
420	389 419	addcomd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( W ` ( i + 1 ) ) ) = ( ( W ` ( i + 1 ) ) + X ) )
421	293	oveq1d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( W ` ( i + 1 ) ) + X ) = ( ( ( Q ` ( i + 1 ) ) - X ) + X ) )
422	276	recnd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
423	422 389	npcand	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` ( i + 1 ) ) - X ) + X ) = ( Q ` ( i + 1 ) ) )
424	420 421 423	3eqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( W ` ( i + 1 ) ) ) = ( Q ` ( i + 1 ) ) )
425	424	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + ( W ` ( i + 1 ) ) ) = ( Q ` ( i + 1 ) ) )
426	418 425	breqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + x ) < ( Q ` ( i + 1 ) ) )
427	414 426	chvarvv	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + s ) < ( Q ` ( i + 1 ) ) )
428	377 379 384 412 427	eliood	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + s ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
429	191	cbvmptv	|- ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) = ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + s ) )
430	429	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) = ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + s ) ) )
431		ioossre	|- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
432	431	a1i	|- ( ph -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
433	9 432	feqresmpt	|- ( ph -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
434	433	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( x e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` x ) ) )
435		fveq2	|- ( x = ( X + s ) -> ( F ` x ) = ( F ` ( X + s ) ) )
436	428 430 434 435	fmptco	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ) = ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) )
437		eqid	|- ( x e. CC |-> ( X + x ) ) = ( x e. CC |-> ( X + x ) )
438		ssid	|- CC C_ CC
439	438	a1i	|- ( ph -> CC C_ CC )
440	439 154 439	constcncfg	|- ( ph -> ( x e. CC |-> X ) e. ( CC -cn-> CC ) )
441		cncfmptid	|- ( ( CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) )
442	438 438 441	mp2an	|- ( x e. CC |-> x ) e. ( CC -cn-> CC )
443	442	a1i	|- ( ph -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) )
444	440 443	addcncf	|- ( ph -> ( x e. CC |-> ( X + x ) ) e. ( CC -cn-> CC ) )
445	444	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. CC |-> ( X + x ) ) e. ( CC -cn-> CC ) )
446		ioosscn	|- ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) C_ CC
447	446	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) C_ CC )
448		ioosscn	|- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
449	448	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
450	376	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
451	378	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
452	8	adantr	|- ( ( ph /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> X e. RR )
453	399	adantl	|- ( ( ph /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> x e. RR )
454	452 453	readdcld	|- ( ( ph /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + x ) e. RR )
455	454	adantlr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + x ) e. RR )
456	450 451 455 411 426	eliood	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + x ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
457	437 445 447 449 456	cncfmptssg	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) e. ( ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) -cn-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
458	457 12	cncfco	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ) e. ( ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) -cn-> CC ) )
459	436 458	eqeltrrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) e. ( ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) -cn-> CC ) )
460	459	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) e. ( ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) -cn-> CC ) )
461		eqid	|- ( s e. RR |-> ( ( D ` n ) ` s ) ) = ( s e. RR |-> ( ( D ` n ) ` s ) )
462	82	feqmptd	|- ( n e. NN -> ( D ` n ) = ( s e. RR |-> ( ( D ` n ) ` s ) ) )
463		cncfss	|- ( ( RR C_ CC /\ CC C_ CC ) -> ( RR -cn-> RR ) C_ ( RR -cn-> CC ) )
464	47 438 463	mp2an	|- ( RR -cn-> RR ) C_ ( RR -cn-> CC )
465	4	dirkercncf	|- ( n e. NN -> ( D ` n ) e. ( RR -cn-> RR ) )
466	464 465	sselid	|- ( n e. NN -> ( D ` n ) e. ( RR -cn-> CC ) )
467	462 466	eqeltrrd	|- ( n e. NN -> ( s e. RR |-> ( ( D ` n ) ` s ) ) e. ( RR -cn-> CC ) )
468	372	a1i	|- ( n e. NN -> ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) C_ RR )
469	438	a1i	|- ( n e. NN -> CC C_ CC )
470		cncff	|- ( ( D ` n ) e. ( RR -cn-> CC ) -> ( D ` n ) : RR --> CC )
471	466 470	syl	|- ( n e. NN -> ( D ` n ) : RR --> CC )
472	471	adantr	|- ( ( n e. NN /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( D ` n ) : RR --> CC )
473	381	adantl	|- ( ( n e. NN /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> s e. RR )
474	472 473	ffvelrnd	|- ( ( n e. NN /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( ( D ` n ) ` s ) e. CC )
475	461 467 468 469 474	cncfmptssg	|- ( n e. NN -> ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( D ` n ) ` s ) ) e. ( ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) -cn-> CC ) )
476	475	ad2antlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( D ` n ) ` s ) ) e. ( ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) -cn-> CC ) )
477	460 476	mulcncf	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) e. ( ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) -cn-> CC ) )
478	375 477	eqeltrd	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) e. ( ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) -cn-> CC ) )
479	453 205	syldan	|- ( ( ph /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( F ` ( X + x ) ) e. CC )
480	479	adantlr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( F ` ( X + x ) ) e. CC )
481		eqid	|- ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) = ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) )
482	480 481	fmptd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) : ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) --> CC )
483	482	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) : ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) --> CC )
484	82	ad2antlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( D ` n ) : RR --> RR )
485	372	a1i	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) C_ RR )
486	484 485	fssresd	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) : ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) --> RR )
487	47	a1i	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> RR C_ CC )
488	486 487	fssd	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) : ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) --> CC )
489		eqid	|- ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) ` s ) x. ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) ` s ) ) ) = ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) ` s ) x. ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) ` s ) ) )
490		fdm	|- ( F : RR --> CC -> dom F = RR )
491	49 490	syl	|- ( ph -> dom F = RR )
492	431 491	sseqtrrid	|- ( ph -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F )
493		ssdmres	|- ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom F <-> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
494	492 493	sylib	|- ( ph -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
495	494	eqcomd	|- ( ph -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
496	495	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
497	456 496	eleqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + x ) e. dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
498	273	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
499	498 411	gtned	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + x ) =/= ( Q ` i ) )
500		eldifsn	|- ( ( X + x ) e. ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` i ) } ) <-> ( ( X + x ) e. dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ ( X + x ) =/= ( Q ` i ) ) )
501	497 499 500	sylanbrc	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + x ) e. ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` i ) } ) )
502	501	ralrimiva	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ( X + x ) e. ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` i ) } ) )
503		eqid	|- ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) = ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) )
504	503	rnmptss	|- ( A. x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ( X + x ) e. ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` i ) } ) -> ran ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) C_ ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` i ) } ) )
505	502 504	syl	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ran ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) C_ ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` i ) } ) )
506		eqidd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) = ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) )
507		oveq2	|- ( x = ( W ` i ) -> ( X + x ) = ( X + ( W ` i ) ) )
508	507	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( W ` i ) ) -> ( X + x ) = ( X + ( W ` i ) ) )
509	390	leidd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( W ` i ) <_ ( W ` i ) )
510	390 404 294	ltled	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( W ` i ) <_ ( W ` ( i + 1 ) ) )
511	390 404 390 509 510	eliccd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( W ` i ) e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) )
512	396 273	eqeltrrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( W ` i ) ) e. RR )
513	506 508 511 512	fvmptd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ` ( W ` i ) ) = ( X + ( W ` i ) ) )
514	396	eqcomd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( W ` i ) ) = ( Q ` i ) )
515	513 514	eqtr2d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ` ( W ` i ) ) )
516	390 404	iccssred	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) C_ RR )
517	516 47	sstrdi	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) C_ CC )
518	517	resmptd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( x e. CC |-> ( X + x ) ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) = ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) )
519		rescncf	|- ( ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) C_ CC -> ( ( x e. CC |-> ( X + x ) ) e. ( CC -cn-> CC ) -> ( ( x e. CC |-> ( X + x ) ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) e. ( ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) -cn-> CC ) ) )
520	517 445 519	sylc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( x e. CC |-> ( X + x ) ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) e. ( ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) -cn-> CC ) )
521	518 520	eqeltrrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) e. ( ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) -cn-> CC ) )
522	521 511	cnlimci	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ` ( W ` i ) ) e. ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) limCC ( W ` i ) ) )
523	515 522	eqeltrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) limCC ( W ` i ) ) )
524		ioossicc	|- ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) C_ ( ( W ` i ) [,] ( W ` ( i + 1 ) ) )
525		resmpt	|- ( ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) C_ ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) -> ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) )
526	524 525	ax-mp	|- ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) )
527	526	eqcomi	|- ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) = ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) )
528	527	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) = ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) )
529	528	oveq1d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) limCC ( W ` i ) ) = ( ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) )
530	154	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) -> X e. CC )
531	390	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) -> ( W ` i ) e. RR )
532	404	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) -> ( W ` ( i + 1 ) ) e. RR )
533		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) -> x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) )
534		eliccre	|- ( ( ( W ` i ) e. RR /\ ( W ` ( i + 1 ) ) e. RR /\ x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) -> x e. RR )
535	531 532 533 534	syl3anc	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) -> x e. RR )
536	535	recnd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) -> x e. CC )
537	530 536	addcld	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) -> ( X + x ) e. CC )
538		eqid	|- ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) = ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) )
539	537 538	fmptd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) : ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) --> CC )
540	390 404 294 539	limciccioolb	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) = ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) limCC ( W ` i ) ) )
541	529 540	eqtr2d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) limCC ( W ` i ) ) = ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) limCC ( W ` i ) ) )
542	523 541	eleqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) limCC ( W ` i ) ) )
543	505 542 13	limccog	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ) limCC ( W ` i ) ) )
544	49 432	fssresd	|- ( ph -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
545	544	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
546	456 503	fmptd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) : ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) --> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
547		fcompt	|- ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC /\ ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) : ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) --> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ) = ( y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ` y ) ) ) )
548	545 546 547	syl2anc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ) = ( y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ` y ) ) ) )
549		eqidd	|- ( ( ph /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) = ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) )
550		oveq2	|- ( x = y -> ( X + x ) = ( X + y ) )
551	550	adantl	|- ( ( ( ph /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) /\ x = y ) -> ( X + x ) = ( X + y ) )
552		simpr	|- ( ( ph /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) )
553	8	adantr	|- ( ( ph /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> X e. RR )
554	372 552	sselid	|- ( ( ph /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> y e. RR )
555	553 554	readdcld	|- ( ( ph /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + y ) e. RR )
556	549 551 552 555	fvmptd	|- ( ( ph /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ` y ) = ( X + y ) )
557	556	fveq2d	|- ( ( ph /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ` y ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( X + y ) ) )
558	557	adantlr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ` y ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( X + y ) ) )
559	376	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
560	378	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
561	555	adantlr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + y ) e. RR )
562	396	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) = ( X + ( W ` i ) ) )
563	390	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` i ) e. RR )
564	554	adantlr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> y e. RR )
565	8	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> X e. RR )
566	402	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` i ) e. RR* )
567	405	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` ( i + 1 ) ) e. RR* )
568		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) )
569		ioogtlb	|- ( ( ( W ` i ) e. RR* /\ ( W ` ( i + 1 ) ) e. RR* /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` i ) < y )
570	566 567 568 569	syl3anc	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` i ) < y )
571	563 564 565 570	ltadd2dd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + ( W ` i ) ) < ( X + y ) )
572	562 571	eqbrtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + y ) )
573	404	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( W ` ( i + 1 ) ) e. RR )
574		iooltub	|- ( ( ( W ` i ) e. RR* /\ ( W ` ( i + 1 ) ) e. RR* /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> y < ( W ` ( i + 1 ) ) )
575	566 567 568 574	syl3anc	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> y < ( W ` ( i + 1 ) ) )
576	564 573 565 575	ltadd2dd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + y ) < ( X + ( W ` ( i + 1 ) ) ) )
577	424	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + ( W ` ( i + 1 ) ) ) = ( Q ` ( i + 1 ) ) )
578	576 577	breqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + y ) < ( Q ` ( i + 1 ) ) )
579	559 560 561 572 578	eliood	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + y ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
580		fvres	|- ( ( X + y ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( X + y ) ) = ( F ` ( X + y ) ) )
581	579 580	syl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( X + y ) ) = ( F ` ( X + y ) ) )
582	558 581	eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ` y ) ) = ( F ` ( X + y ) ) )
583	582	mpteq2dva	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ` y ) ) ) = ( y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + y ) ) ) )
584	550	fveq2d	|- ( x = y -> ( F ` ( X + x ) ) = ( F ` ( X + y ) ) )
585	584	cbvmptv	|- ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) = ( y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + y ) ) )
586	583 585	eqtr4di	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( y e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ` y ) ) ) = ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) )
587	548 586	eqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ) = ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) )
588	587	oveq1d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ) limCC ( W ` i ) ) = ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) limCC ( W ` i ) ) )
589	543 588	eleqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) limCC ( W ` i ) ) )
590	589	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> R e. ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) limCC ( W ` i ) ) )
591		fvres	|- ( ( W ` i ) e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) ` ( W ` i ) ) = ( ( D ` n ) ` ( W ` i ) ) )
592	511 591	syl	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) ` ( W ` i ) ) = ( ( D ` n ) ` ( W ` i ) ) )
593	592	eqcomd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( D ` n ) ` ( W ` i ) ) = ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) ` ( W ` i ) ) )
594	593	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( D ` n ) ` ( W ` i ) ) = ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) ` ( W ` i ) ) )
595	516	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) C_ RR )
596	465	ad2antlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( D ` n ) e. ( RR -cn-> RR ) )
597		rescncf	|- ( ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) C_ RR -> ( ( D ` n ) e. ( RR -cn-> RR ) -> ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) e. ( ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) -cn-> RR ) ) )
598	595 596 597	sylc	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) e. ( ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) -cn-> RR ) )
599	511	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( W ` i ) e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) )
600	598 599	cnlimci	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) ` ( W ` i ) ) e. ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) )
601	594 600	eqeltrd	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( D ` n ) ` ( W ` i ) ) e. ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) )
602	524	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) C_ ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) )
603	602	resabs1d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) )
604	603	eqcomd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) )
605	604	oveq1d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) = ( ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) )
606	605	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) = ( ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) )
607	390	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( W ` i ) e. RR )
608	404	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( W ` ( i + 1 ) ) e. RR )
609	294	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( W ` i ) < ( W ` ( i + 1 ) ) )
610	471	ad2antlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( D ` n ) : RR --> CC )
611	610 595	fssresd	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) : ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) --> CC )
612	607 608 609 611	limciccioolb	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) = ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) )
613	606 612	eqtr2d	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) = ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) )
614	601 613	eleqtrd	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( D ` n ) ` ( W ` i ) ) e. ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) )
615	483 488 489 590 614	mullimcf	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( R x. ( ( D ` n ) ` ( W ` i ) ) ) e. ( ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) ` s ) x. ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) ` s ) ) ) limCC ( W ` i ) ) )
616		eqidd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) = ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) )
617	192	adantl	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) /\ x = s ) -> ( F ` ( X + x ) ) = ( F ` ( X + s ) ) )
618		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) )
619	49	adantr	|- ( ( ph /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> F : RR --> CC )
620	619 383	ffvelrnd	|- ( ( ph /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. CC )
621	620	adantlr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. CC )
622	616 617 618 621	fvmptd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) ` s ) = ( F ` ( X + s ) ) )
623	622	adantllr	|- ( ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) ` s ) = ( F ` ( X + s ) ) )
624		fvres	|- ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) ` s ) = ( ( D ` n ) ` s ) )
625	624	adantl	|- ( ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) ` s ) = ( ( D ` n ) ` s ) )
626	623 625	oveq12d	|- ( ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) ` s ) x. ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) ` s ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
627	626	eqcomd	|- ( ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) ` s ) x. ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) ` s ) ) )
628	627	mpteq2dva	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) = ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) ` s ) x. ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) ` s ) ) ) )
629	375 628	eqtr2d	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) ` s ) x. ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) ` s ) ) ) = ( G |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) )
630	629	oveq1d	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) ` s ) x. ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) ` s ) ) ) limCC ( W ` i ) ) = ( ( G |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) )
631	615 630	eleqtrd	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( R x. ( ( D ` n ) ` ( W ` i ) ) ) e. ( ( G |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` i ) ) )
632	455 426	ltned	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + x ) =/= ( Q ` ( i + 1 ) ) )
633		eldifsn	|- ( ( X + x ) e. ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` ( i + 1 ) ) } ) <-> ( ( X + x ) e. dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ ( X + x ) =/= ( Q ` ( i + 1 ) ) ) )
634	497 632 633	sylanbrc	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) -> ( X + x ) e. ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` ( i + 1 ) ) } ) )
635	634	ralrimiva	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ( X + x ) e. ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` ( i + 1 ) ) } ) )
636	503	rnmptss	|- ( A. x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ( X + x ) e. ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` ( i + 1 ) ) } ) -> ran ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) C_ ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` ( i + 1 ) ) } ) )
637	635 636	syl	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ran ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) C_ ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` ( i + 1 ) ) } ) )
638	404	leidd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( W ` ( i + 1 ) ) <_ ( W ` ( i + 1 ) ) )
639	390 404 404 510 638	eliccd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( W ` ( i + 1 ) ) e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) )
640	521 639	cnlimci	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ` ( W ` ( i + 1 ) ) ) e. ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) limCC ( W ` ( i + 1 ) ) ) )
641		oveq2	|- ( x = ( W ` ( i + 1 ) ) -> ( X + x ) = ( X + ( W ` ( i + 1 ) ) ) )
642	641	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ x = ( W ` ( i + 1 ) ) ) -> ( X + x ) = ( X + ( W ` ( i + 1 ) ) ) )
643	277 404	readdcld	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( W ` ( i + 1 ) ) ) e. RR )
644	506 642 639 643	fvmptd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ` ( W ` ( i + 1 ) ) ) = ( X + ( W ` ( i + 1 ) ) ) )
645	644 424	eqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ` ( W ` ( i + 1 ) ) ) = ( Q ` ( i + 1 ) ) )
646	528	oveq1d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) limCC ( W ` ( i + 1 ) ) ) = ( ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` ( i + 1 ) ) ) )
647	390 404 294 539	limcicciooub	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` ( i + 1 ) ) ) = ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) limCC ( W ` ( i + 1 ) ) ) )
648	646 647	eqtr2d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( x e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) limCC ( W ` ( i + 1 ) ) ) = ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) limCC ( W ` ( i + 1 ) ) ) )
649	640 645 648	3eltr3d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) limCC ( W ` ( i + 1 ) ) ) )
650	637 649 14	limccog	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ) limCC ( W ` ( i + 1 ) ) ) )
651	587	oveq1d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( X + x ) ) ) limCC ( W ` ( i + 1 ) ) ) = ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) limCC ( W ` ( i + 1 ) ) ) )
652	650 651	eleqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) limCC ( W ` ( i + 1 ) ) ) )
653	652	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> L e. ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) limCC ( W ` ( i + 1 ) ) ) )
654	639	adantlr	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( W ` ( i + 1 ) ) e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) )
655	598 654	cnlimci	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) ` ( W ` ( i + 1 ) ) ) e. ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) limCC ( W ` ( i + 1 ) ) ) )
656		fvres	|- ( ( W ` ( i + 1 ) ) e. ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) ` ( W ` ( i + 1 ) ) ) = ( ( D ` n ) ` ( W ` ( i + 1 ) ) ) )
657	654 656	syl	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) ` ( W ` ( i + 1 ) ) ) = ( ( D ` n ) ` ( W ` ( i + 1 ) ) ) )
658	607 608 609 611	limcicciooub	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` ( i + 1 ) ) ) = ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) limCC ( W ` ( i + 1 ) ) ) )
659	658	eqcomd	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) limCC ( W ` ( i + 1 ) ) ) = ( ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` ( i + 1 ) ) ) )
660		resabs1	|- ( ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) C_ ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) )
661	524 660	mp1i	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) = ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) )
662	661	oveq1d	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` ( i + 1 ) ) ) = ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` ( i + 1 ) ) ) )
663	659 662	eqtrd	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( ( D ` n ) |` ( ( W ` i ) [,] ( W ` ( i + 1 ) ) ) ) limCC ( W ` ( i + 1 ) ) ) = ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` ( i + 1 ) ) ) )
664	655 657 663	3eltr3d	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( D ` n ) ` ( W ` ( i + 1 ) ) ) e. ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` ( i + 1 ) ) ) )
665	483 488 489 653 664	mullimcf	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( L x. ( ( D ` n ) ` ( W ` ( i + 1 ) ) ) ) e. ( ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) ` s ) x. ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) ` s ) ) ) limCC ( W ` ( i + 1 ) ) ) )
666	629	oveq1d	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( ( s e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( ( ( x e. ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) |-> ( F ` ( X + x ) ) ) ` s ) x. ( ( ( D ` n ) |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) ` s ) ) ) limCC ( W ` ( i + 1 ) ) ) = ( ( G |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` ( i + 1 ) ) ) )
667	665 666	eleqtrd	|- ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ M ) ) -> ( L x. ( ( D ` n ) ` ( W ` ( i + 1 ) ) ) ) e. ( ( G |` ( ( W ` i ) (,) ( W ` ( i + 1 ) ) ) ) limCC ( W ` ( i + 1 ) ) ) )
668	130 133 225 226 16 114 300 211 369 478 631 667	fourierdlem110	|- ( ( ph /\ n e. NN ) -> S. ( ( ( -u _pi - X ) - -u X ) [,] ( ( _pi - X ) - -u X ) ) ( G ` x ) _d x = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( G ` x ) _d x )
669	668	eqcomd	|- ( ( ph /\ n e. NN ) -> S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( G ` x ) _d x = S. ( ( ( -u _pi - X ) - -u X ) [,] ( ( _pi - X ) - -u X ) ) ( G ` x ) _d x )
670	129	recnd	|- ( ph -> ( -u _pi - X ) e. CC )
671	670 154	subnegd	|- ( ph -> ( ( -u _pi - X ) - -u X ) = ( ( -u _pi - X ) + X ) )
672	156 154	npcand	|- ( ph -> ( ( -u _pi - X ) + X ) = -u _pi )
673	671 672	eqtrd	|- ( ph -> ( ( -u _pi - X ) - -u X ) = -u _pi )
674	132	recnd	|- ( ph -> ( _pi - X ) e. CC )
675	674 154	subnegd	|- ( ph -> ( ( _pi - X ) - -u X ) = ( ( _pi - X ) + X ) )
676	155 154	npcand	|- ( ph -> ( ( _pi - X ) + X ) = _pi )
677	675 676	eqtrd	|- ( ph -> ( ( _pi - X ) - -u X ) = _pi )
678	673 677	oveq12d	|- ( ph -> ( ( ( -u _pi - X ) - -u X ) [,] ( ( _pi - X ) - -u X ) ) = ( -u _pi [,] _pi ) )
679	678	itgeq1d	|- ( ph -> S. ( ( ( -u _pi - X ) - -u X ) [,] ( ( _pi - X ) - -u X ) ) ( G ` x ) _d x = S. ( -u _pi [,] _pi ) ( G ` x ) _d x )
680	679	adantr	|- ( ( ph /\ n e. NN ) -> S. ( ( ( -u _pi - X ) - -u X ) [,] ( ( _pi - X ) - -u X ) ) ( G ` x ) _d x = S. ( -u _pi [,] _pi ) ( G ` x ) _d x )
681	669 680	eqtrd	|- ( ( ph /\ n e. NN ) -> S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( G ` x ) _d x = S. ( -u _pi [,] _pi ) ( G ` x ) _d x )
682		fveq2	|- ( x = s -> ( G ` x ) = ( G ` s ) )
683	682	cbvitgv	|- S. ( -u _pi (,) _pi ) ( G ` x ) _d x = S. ( -u _pi (,) _pi ) ( G ` s ) _d s
684	211	adantr	|- ( ( ( ph /\ n e. NN ) /\ x e. ( -u _pi [,] _pi ) ) -> G : RR --> CC )
685	44	adantlr	|- ( ( ( ph /\ n e. NN ) /\ x e. ( -u _pi [,] _pi ) ) -> x e. RR )
686	684 685	ffvelrnd	|- ( ( ( ph /\ n e. NN ) /\ x e. ( -u _pi [,] _pi ) ) -> ( G ` x ) e. CC )
687	76 77 686	itgioo	|- ( ( ph /\ n e. NN ) -> S. ( -u _pi (,) _pi ) ( G ` x ) _d x = S. ( -u _pi [,] _pi ) ( G ` x ) _d x )
688		elioore	|- ( s e. ( -u _pi (,) _pi ) -> s e. RR )
689	688	adantl	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi (,) _pi ) ) -> s e. RR )
690	49	adantr	|- ( ( ph /\ s e. ( -u _pi (,) _pi ) ) -> F : RR --> CC )
691	8	adantr	|- ( ( ph /\ s e. ( -u _pi (,) _pi ) ) -> X e. RR )
692	688	adantl	|- ( ( ph /\ s e. ( -u _pi (,) _pi ) ) -> s e. RR )
693	691 692	readdcld	|- ( ( ph /\ s e. ( -u _pi (,) _pi ) ) -> ( X + s ) e. RR )
694	690 693	ffvelrnd	|- ( ( ph /\ s e. ( -u _pi (,) _pi ) ) -> ( F ` ( X + s ) ) e. CC )
695	694	adantlr	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi (,) _pi ) ) -> ( F ` ( X + s ) ) e. CC )
696	82	ad2antlr	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi (,) _pi ) ) -> ( D ` n ) : RR --> RR )
697	696 689	ffvelrnd	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi (,) _pi ) ) -> ( ( D ` n ) ` s ) e. RR )
698	697	recnd	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi (,) _pi ) ) -> ( ( D ` n ) ` s ) e. CC )
699	695 698	mulcld	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi (,) _pi ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. CC )
700	689 699 197	syl2anc	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi (,) _pi ) ) -> ( G ` s ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
701	700	itgeq2dv	|- ( ( ph /\ n e. NN ) -> S. ( -u _pi (,) _pi ) ( G ` s ) _d s = S. ( -u _pi (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
702	683 687 701	3eqtr3a	|- ( ( ph /\ n e. NN ) -> S. ( -u _pi [,] _pi ) ( G ` x ) _d x = S. ( -u _pi (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
703	224 681 702	3eqtrd	|- ( ( ph /\ n e. NN ) -> S. ( ( -u _pi - X ) (,) ( _pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s = S. ( -u _pi (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
704	75 178 703	3eqtrd	|- ( ( ph /\ n e. NN ) -> ( S ` n ) = S. ( -u _pi (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
705	77	renegcld	|- ( ( ph /\ n e. NN ) -> -u _pi e. RR )
706		0red	|- ( ( ph /\ n e. NN ) -> 0 e. RR )
707		0re	|- 0 e. RR
708		negpilt0	|- -u _pi < 0
709	39 707 708	ltleii	|- -u _pi <_ 0
710	709	a1i	|- ( ( ph /\ n e. NN ) -> -u _pi <_ 0 )
711		pipos	|- 0 < _pi
712	707 38 711	ltleii	|- 0 <_ _pi
713	712	a1i	|- ( ( ph /\ n e. NN ) -> 0 <_ _pi )
714	76 77 706 710 713	eliccd	|- ( ( ph /\ n e. NN ) -> 0 e. ( -u _pi [,] _pi ) )
715		ioossicc	|- ( -u _pi (,) 0 ) C_ ( -u _pi [,] 0 )
716	715	a1i	|- ( ( ph /\ n e. NN ) -> ( -u _pi (,) 0 ) C_ ( -u _pi [,] 0 ) )
717		ioombl	|- ( -u _pi (,) 0 ) e. dom vol
718	717	a1i	|- ( ( ph /\ n e. NN ) -> ( -u _pi (,) 0 ) e. dom vol )
719	49	adantr	|- ( ( ph /\ s e. ( -u _pi [,] 0 ) ) -> F : RR --> CC )
720	8	adantr	|- ( ( ph /\ s e. ( -u _pi [,] 0 ) ) -> X e. RR )
721	39	a1i	|- ( s e. ( -u _pi [,] 0 ) -> -u _pi e. RR )
722		0red	|- ( s e. ( -u _pi [,] 0 ) -> 0 e. RR )
723		id	|- ( s e. ( -u _pi [,] 0 ) -> s e. ( -u _pi [,] 0 ) )
724		eliccre	|- ( ( -u _pi e. RR /\ 0 e. RR /\ s e. ( -u _pi [,] 0 ) ) -> s e. RR )
725	721 722 723 724	syl3anc	|- ( s e. ( -u _pi [,] 0 ) -> s e. RR )
726	725	adantl	|- ( ( ph /\ s e. ( -u _pi [,] 0 ) ) -> s e. RR )
727	720 726	readdcld	|- ( ( ph /\ s e. ( -u _pi [,] 0 ) ) -> ( X + s ) e. RR )
728	719 727	ffvelrnd	|- ( ( ph /\ s e. ( -u _pi [,] 0 ) ) -> ( F ` ( X + s ) ) e. CC )
729	728	adantlr	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] 0 ) ) -> ( F ` ( X + s ) ) e. CC )
730	82	ad2antlr	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] 0 ) ) -> ( D ` n ) : RR --> RR )
731	725	adantl	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] 0 ) ) -> s e. RR )
732	730 731	ffvelrnd	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] 0 ) ) -> ( ( D ` n ) ` s ) e. RR )
733	732	recnd	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] 0 ) ) -> ( ( D ` n ) ` s ) e. CC )
734	729 733	mulcld	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] 0 ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. CC )
735	731 734 197	syl2anc	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] 0 ) ) -> ( G ` s ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
736	735	eqcomd	|- ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] 0 ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( G ` s ) )
737	736	mpteq2dva	|- ( ( ph /\ n e. NN ) -> ( s e. ( -u _pi [,] 0 ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) = ( s e. ( -u _pi [,] 0 ) |-> ( G ` s ) ) )
738	306	oveq2d	|- ( ph -> ( s + ( ( _pi - X ) - ( -u _pi - X ) ) ) = ( s + T ) )
739	738	ad2antrr	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( s + ( ( _pi - X ) - ( -u _pi - X ) ) ) = ( s + T ) )
740	739	fveq2d	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( G ` ( s + ( ( _pi - X ) - ( -u _pi - X ) ) ) ) = ( G ` ( s + T ) ) )
741	11	a1i	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> G = ( x e. RR |-> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) ) )
742		oveq2	|- ( x = ( s + T ) -> ( X + x ) = ( X + ( s + T ) ) )
743	742	fveq2d	|- ( x = ( s + T ) -> ( F ` ( X + x ) ) = ( F ` ( X + ( s + T ) ) ) )
744		fveq2	|- ( x = ( s + T ) -> ( ( D ` n ) ` x ) = ( ( D ` n ) ` ( s + T ) ) )
745	743 744	oveq12d	|- ( x = ( s + T ) -> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) = ( ( F ` ( X + ( s + T ) ) ) x. ( ( D ` n ) ` ( s + T ) ) ) )
746	745	adantl	|- ( ( ( ( ph /\ n e. NN ) /\ s e. RR ) /\ x = ( s + T ) ) -> ( ( F ` ( X + x ) ) x. ( ( D ` n ) ` x ) ) = ( ( F ` ( X + ( s + T ) ) ) x. ( ( D ` n ) ` ( s + T ) ) ) )
747		simpr	|- ( ( ph /\ s e. RR ) -> s e. RR )
748	317	a1i	|- ( ( ph /\ s e. RR ) -> T e. RR )
749	747 748	readdcld	|- ( ( ph /\ s e. RR ) -> ( s + T ) e. RR )
750	749	adantlr	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( s + T ) e. RR )
751	49	adantr	|- ( ( ph /\ s e. RR ) -> F : RR --> CC )
752	8	adantr	|- ( ( ph /\ s e. RR ) -> X e. RR )
753	752 749	readdcld	|- ( ( ph /\ s e. RR ) -> ( X + ( s + T ) ) e. RR )
754	751 753	ffvelrnd	|- ( ( ph /\ s e. RR ) -> ( F ` ( X + ( s + T ) ) ) e. CC )
755	754	adantlr	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( F ` ( X + ( s + T ) ) ) e. CC )
756	82	ad2antlr	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( D ` n ) : RR --> RR )
757	756 750	ffvelrnd	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( ( D ` n ) ` ( s + T ) ) e. RR )
758	757	recnd	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( ( D ` n ) ` ( s + T ) ) e. CC )
759	755 758	mulcld	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( ( F ` ( X + ( s + T ) ) ) x. ( ( D ` n ) ` ( s + T ) ) ) e. CC )
760	741 746 750 759	fvmptd	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( G ` ( s + T ) ) = ( ( F ` ( X + ( s + T ) ) ) x. ( ( D ` n ) ` ( s + T ) ) ) )
761	154	adantr	|- ( ( ph /\ s e. RR ) -> X e. CC )
762	747	recnd	|- ( ( ph /\ s e. RR ) -> s e. CC )
763	319	adantr	|- ( ( ph /\ s e. RR ) -> T e. CC )
764	761 762 763	addassd	|- ( ( ph /\ s e. RR ) -> ( ( X + s ) + T ) = ( X + ( s + T ) ) )
765	764	eqcomd	|- ( ( ph /\ s e. RR ) -> ( X + ( s + T ) ) = ( ( X + s ) + T ) )
766	765	fveq2d	|- ( ( ph /\ s e. RR ) -> ( F ` ( X + ( s + T ) ) ) = ( F ` ( ( X + s ) + T ) ) )
767	752 747	readdcld	|- ( ( ph /\ s e. RR ) -> ( X + s ) e. RR )
768		simpl	|- ( ( ph /\ s e. RR ) -> ph )
769	768 767	jca	|- ( ( ph /\ s e. RR ) -> ( ph /\ ( X + s ) e. RR ) )
770		eleq1	|- ( x = ( X + s ) -> ( x e. RR <-> ( X + s ) e. RR ) )
771	770	anbi2d	|- ( x = ( X + s ) -> ( ( ph /\ x e. RR ) <-> ( ph /\ ( X + s ) e. RR ) ) )
772		oveq1	|- ( x = ( X + s ) -> ( x + T ) = ( ( X + s ) + T ) )
773	772	fveq2d	|- ( x = ( X + s ) -> ( F ` ( x + T ) ) = ( F ` ( ( X + s ) + T ) ) )
774	773 435	eqeq12d	|- ( x = ( X + s ) -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( ( X + s ) + T ) ) = ( F ` ( X + s ) ) ) )
775	771 774	imbi12d	|- ( x = ( X + s ) -> ( ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ ( X + s ) e. RR ) -> ( F ` ( ( X + s ) + T ) ) = ( F ` ( X + s ) ) ) ) )
776	775 10	vtoclg	|- ( ( X + s ) e. RR -> ( ( ph /\ ( X + s ) e. RR ) -> ( F ` ( ( X + s ) + T ) ) = ( F ` ( X + s ) ) ) )
777	767 769 776	sylc	|- ( ( ph /\ s e. RR ) -> ( F ` ( ( X + s ) + T ) ) = ( F ` ( X + s ) ) )
778	766 777	eqtrd	|- ( ( ph /\ s e. RR ) -> ( F ` ( X + ( s + T ) ) ) = ( F ` ( X + s ) ) )
779	778	adantlr	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( F ` ( X + ( s + T ) ) ) = ( F ` ( X + s ) ) )
780	4 15	dirkerper	|- ( ( n e. NN /\ s e. RR ) -> ( ( D ` n ) ` ( s + T ) ) = ( ( D ` n ) ` s ) )
781	780	adantll	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( ( D ` n ) ` ( s + T ) ) = ( ( D ` n ) ` s ) )
782	779 781	oveq12d	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( ( F ` ( X + ( s + T ) ) ) x. ( ( D ` n ) ` ( s + T ) ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
783		simpr	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> s e. RR )
784	782 759	eqeltrrd	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. CC )
785	783 784 197	syl2anc	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( G ` s ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
786	785	eqcomd	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( G ` s ) )
787	782 786	eqtrd	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( ( F ` ( X + ( s + T ) ) ) x. ( ( D ` n ) ` ( s + T ) ) ) = ( G ` s ) )
788	740 760 787	3eqtrd	|- ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( G ` ( s + ( ( _pi - X ) - ( -u _pi - X ) ) ) ) = ( G ` s ) )
789		0ltpnf	|- 0 < +oo
790		pnfxr	|- +oo e. RR*
791		elioo2	|- ( ( -u _pi e. RR* /\ +oo e. RR* ) -> ( 0 e. ( -u _pi (,) +oo ) <-> ( 0 e. RR /\ -u _pi < 0 /\ 0 < +oo ) ) )
792	52 790 791	mp2an	|- ( 0 e. ( -u _pi (,) +oo ) <-> ( 0 e. RR /\ -u _pi < 0 /\ 0 < +oo ) )
793	707 708 789 792	mpbir3an	|- 0 e. ( -u _pi (,) +oo )
794	793	a1i	|- ( ( ph /\ n e. NN ) -> 0 e. ( -u _pi (,) +oo ) )
795	16 225 114 300 211 788 478 631 667 76 794	fourierdlem105	|- ( ( ph /\ n e. NN ) -> ( s e. ( -u _pi [,] 0 ) |-> ( G ` s ) ) e. L^1 )
796	737 795	eqeltrd	|- ( ( ph /\ n e. NN ) -> ( s e. ( -u _pi [,] 0 ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) e. L^1 )
797	716 718 734 796	iblss	|- ( ( ph /\ n e. NN ) -> ( s e. ( -u _pi (,) 0 ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) e. L^1 )
798		elioore	|- ( s e. ( 0 (,) _pi ) -> s e. RR )
799	798	adantl	|- ( ( ( ph /\ n e. NN ) /\ s e. ( 0 (,) _pi ) ) -> s e. RR )
800	799 784	syldan	|- ( ( ( ph /\ n e. NN ) /\ s e. ( 0 (,) _pi ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. CC )
801	799 800 197	syl2anc	|- ( ( ( ph /\ n e. NN ) /\ s e. ( 0 (,) _pi ) ) -> ( G ` s ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
802	801	eqcomd	|- ( ( ( ph /\ n e. NN ) /\ s e. ( 0 (,) _pi ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) = ( G ` s ) )
803	802	mpteq2dva	|- ( ( ph /\ n e. NN ) -> ( s e. ( 0 (,) _pi ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) = ( s e. ( 0 (,) _pi ) |-> ( G ` s ) ) )
804		ioossicc	|- ( 0 (,) _pi ) C_ ( 0 [,] _pi )
805	804	a1i	|- ( ( ph /\ n e. NN ) -> ( 0 (,) _pi ) C_ ( 0 [,] _pi ) )
806		ioombl	|- ( 0 (,) _pi ) e. dom vol
807	806	a1i	|- ( ( ph /\ n e. NN ) -> ( 0 (,) _pi ) e. dom vol )
808	211	adantr	|- ( ( ( ph /\ n e. NN ) /\ s e. ( 0 [,] _pi ) ) -> G : RR --> CC )
809		0red	|- ( ( ph /\ s e. ( 0 [,] _pi ) ) -> 0 e. RR )
810	38	a1i	|- ( ( ph /\ s e. ( 0 [,] _pi ) ) -> _pi e. RR )
811		simpr	|- ( ( ph /\ s e. ( 0 [,] _pi ) ) -> s e. ( 0 [,] _pi ) )
812		eliccre	|- ( ( 0 e. RR /\ _pi e. RR /\ s e. ( 0 [,] _pi ) ) -> s e. RR )
813	809 810 811 812	syl3anc	|- ( ( ph /\ s e. ( 0 [,] _pi ) ) -> s e. RR )
814	813	adantlr	|- ( ( ( ph /\ n e. NN ) /\ s e. ( 0 [,] _pi ) ) -> s e. RR )
815	808 814	ffvelrnd	|- ( ( ( ph /\ n e. NN ) /\ s e. ( 0 [,] _pi ) ) -> ( G ` s ) e. CC )
816		0xr	|- 0 e. RR*
817	816	a1i	|- ( ( ph /\ n e. NN ) -> 0 e. RR* )
818	790	a1i	|- ( ( ph /\ n e. NN ) -> +oo e. RR* )
819	711	a1i	|- ( ( ph /\ n e. NN ) -> 0 < _pi )
820		ltpnf	|- ( _pi e. RR -> _pi < +oo )
821	38 820	mp1i	|- ( ( ph /\ n e. NN ) -> _pi < +oo )
822	817 818 77 819 821	eliood	|- ( ( ph /\ n e. NN ) -> _pi e. ( 0 (,) +oo ) )
823	16 225 114 300 211 788 478 631 667 706 822	fourierdlem105	|- ( ( ph /\ n e. NN ) -> ( s e. ( 0 [,] _pi ) |-> ( G ` s ) ) e. L^1 )
824	805 807 815 823	iblss	|- ( ( ph /\ n e. NN ) -> ( s e. ( 0 (,) _pi ) |-> ( G ` s ) ) e. L^1 )
825	803 824	eqeltrd	|- ( ( ph /\ n e. NN ) -> ( s e. ( 0 (,) _pi ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) e. L^1 )
826	705 77 714 699 797 825	itgsplitioo	|- ( ( ph /\ n e. NN ) -> S. ( -u _pi (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s = ( S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s + S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s ) )
827	704 826	eqtrd	|- ( ( ph /\ n e. NN ) -> ( S ` n ) = ( S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s + S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s ) )