This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ) )