Metamath Proof Explorer

Theorem fourierdlem101

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

Ref Expression
Hypotheses fourierdlem101.d 
|- D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
fourierdlem101.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 ) ) ) } )
fourierdlem101.g 
|- G = ( t e. ( -u _pi [,] _pi ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) )
fourierdlem101.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem101.6 
|- ( ph -> M e. NN )
fourierdlem101.n 
|- ( ph -> N e. NN )
fourierdlem101.x 
|- ( ph -> X e. RR )
fourierdlem101.f 
|- ( ph -> F : ( -u _pi [,] _pi ) --> CC )
fourierdlem101.fcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem101.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
fourierdlem101.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
Assertion fourierdlem101 
|- ( ph -> 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 )

Proof

Step Hyp Ref Expression
1 fourierdlem101.d 
 |-  D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
2 fourierdlem101.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 ) ) ) } )
3 fourierdlem101.g 
 |-  G = ( t e. ( -u _pi [,] _pi ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) )
4 fourierdlem101.q 
 |-  ( ph -> Q e. ( P ` M ) )
5 fourierdlem101.6 
 |-  ( ph -> M e. NN )
6 fourierdlem101.n 
 |-  ( ph -> N e. NN )
7 fourierdlem101.x 
 |-  ( ph -> X e. RR )
8 fourierdlem101.f 
 |-  ( ph -> F : ( -u _pi [,] _pi ) --> CC )
9 fourierdlem101.fcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
10 fourierdlem101.r 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
11 fourierdlem101.l 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
12 simpr 
 |-  ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> t e. ( -u _pi [,] _pi ) )
13 8 ffvelcdmda 
 |-  ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> ( F ` t ) e. CC )
14 6 adantr 
 |-  ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> N e. NN )
15 pire 
 |-  _pi e. RR
16 15 renegcli 
 |-  -u _pi e. RR
17 eliccre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR /\ t e. ( -u _pi [,] _pi ) ) -> t e. RR )
18 16 15 17 mp3an12 
 |-  ( t e. ( -u _pi [,] _pi ) -> t e. RR )
19 18 adantl 
 |-  ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> t e. RR )
20 7 adantr 
 |-  ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> X e. RR )
21 19 20 resubcld 
 |-  ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> ( t - X ) e. RR )
22 1 dirkerre 
 |-  ( ( N e. NN /\ ( t - X ) e. RR ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
23 14 21 22 syl2anc 
 |-  ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
24 23 recnd 
 |-  ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> ( ( D ` N ) ` ( t - X ) ) e. CC )
25 13 24 mulcld 
 |-  ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) e. CC )
26 3 fvmpt2 
 |-  ( ( t e. ( -u _pi [,] _pi ) /\ ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) e. CC ) -> ( G ` t ) = ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) )
27 12 25 26 syl2anc 
 |-  ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> ( G ` t ) = ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) )
28 27 eqcomd 
 |-  ( ( ph /\ t e. ( -u _pi [,] _pi ) ) -> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) = ( G ` t ) )
29 28 itgeq2dv 
 |-  ( ph -> S. ( -u _pi [,] _pi ) ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) _d t = S. ( -u _pi [,] _pi ) ( G ` t ) _d t )
30 fveq2 
 |-  ( j = i -> ( Q ` j ) = ( Q ` i ) )
31 30 oveq1d 
 |-  ( j = i -> ( ( Q ` j ) - X ) = ( ( Q ` i ) - X ) )
32 31 cbvmptv 
 |-  ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) ) = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )
33 25 3 fmptd 
 |-  ( ph -> G : ( -u _pi [,] _pi ) --> CC )
34 3 reseq1i 
 |-  ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( t e. ( -u _pi [,] _pi ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
35 ioossicc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
36 16 a1i 
 |-  ( ph -> -u _pi e. RR )
37 36 rexrd 
 |-  ( ph -> -u _pi e. RR* )
38 37 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -u _pi e. RR* )
39 15 a1i 
 |-  ( ph -> _pi e. RR )
40 39 rexrd 
 |-  ( ph -> _pi e. RR* )
41 40 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> _pi e. RR* )
42 2 5 4 fourierdlem15 
 |-  ( ph -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
43 42 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
44 simpr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
45 38 41 43 44 fourierdlem8 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
46 35 45 sstrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
47 46 resmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( t e. ( -u _pi [,] _pi ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) )
48 34 47 eqtrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) )
49 8 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F : ( -u _pi [,] _pi ) --> CC )
50 49 46 feqresmpt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) )
51 50 9 eqeltrrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
52 eqidd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( s e. RR |-> ( ( D ` N ) ` s ) ) = ( s e. RR |-> ( ( D ` N ) ` s ) ) )
53 simpr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) -> s = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) )
54 eqidd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) )
55 oveq1 
 |-  ( t = r -> ( t - X ) = ( r - X ) )
56 55 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ t = r ) -> ( t - X ) = ( r - X ) )
57 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
58 elioore 
 |-  ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> r e. RR )
59 58 adantl 
 |-  ( ( ph /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> r e. RR )
60 7 adantr 
 |-  ( ( ph /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
61 59 60 resubcld 
 |-  ( ( ph /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r - X ) e. RR )
62 61 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( r - X ) e. RR )
63 54 56 57 62 fvmptd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) = ( r - X ) )
64 63 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) = ( r - X ) )
65 53 64 eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) -> s = ( r - X ) )
66 65 fveq2d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) -> ( ( D ` N ) ` s ) = ( ( D ` N ) ` ( r - X ) ) )
67 elioore 
 |-  ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> t e. RR )
68 67 adantl 
 |-  ( ( ph /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> t e. RR )
69 7 adantr 
 |-  ( ( ph /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
70 68 69 resubcld 
 |-  ( ( ph /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( t - X ) e. RR )
71 70 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( t - X ) e. RR )
72 eqid 
 |-  ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) )
73 71 72 fmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> RR )
74 73 ffvelcdmda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) e. RR )
75 6 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> N e. NN )
76 1 dirkerre 
 |-  ( ( N e. NN /\ ( r - X ) e. RR ) -> ( ( D ` N ) ` ( r - X ) ) e. RR )
77 75 62 76 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` N ) ` ( r - X ) ) e. RR )
78 52 66 74 77 fvmptd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) ` ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) = ( ( D ` N ) ` ( r - X ) ) )
79 78 eqcomd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` N ) ` ( r - X ) ) = ( ( s e. RR |-> ( ( D ` N ) ` s ) ) ` ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) )
80 79 mpteq2dva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( r - X ) ) ) = ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) ` ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) ) )
81 55 fveq2d 
 |-  ( t = r -> ( ( D ` N ) ` ( t - X ) ) = ( ( D ` N ) ` ( r - X ) ) )
82 81 cbvmptv 
 |-  ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( t - X ) ) ) = ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( r - X ) ) )
83 82 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( t - X ) ) ) = ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( r - X ) ) ) )
84 1 dirkerre 
 |-  ( ( N e. NN /\ s e. RR ) -> ( ( D ` N ) ` s ) e. RR )
85 6 84 sylan 
 |-  ( ( ph /\ s e. RR ) -> ( ( D ` N ) ` s ) e. RR )
86 eqid 
 |-  ( s e. RR |-> ( ( D ` N ) ` s ) ) = ( s e. RR |-> ( ( D ` N ) ` s ) )
87 85 86 fmptd 
 |-  ( ph -> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> RR )
88 87 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> RR )
89 fcompt 
 |-  ( ( ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> RR /\ ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> RR ) -> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) o. ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ) = ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) ` ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) ) )
90 88 73 89 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) o. ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ) = ( r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) ` ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ` r ) ) ) )
91 80 83 90 3eqtr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( t - X ) ) ) = ( ( s e. RR |-> ( ( D ` N ) ` s ) ) o. ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ) )
92 eqid 
 |-  ( t e. CC |-> ( t - X ) ) = ( t e. CC |-> ( t - X ) )
93 simpr 
 |-  ( ( ph /\ t e. CC ) -> t e. CC )
94 7 recnd 
 |-  ( ph -> X e. CC )
95 94 adantr 
 |-  ( ( ph /\ t e. CC ) -> X e. CC )
96 93 95 negsubd 
 |-  ( ( ph /\ t e. CC ) -> ( t + -u X ) = ( t - X ) )
97 96 eqcomd 
 |-  ( ( ph /\ t e. CC ) -> ( t - X ) = ( t + -u X ) )
98 97 mpteq2dva 
 |-  ( ph -> ( t e. CC |-> ( t - X ) ) = ( t e. CC |-> ( t + -u X ) ) )
99 94 negcld 
 |-  ( ph -> -u X e. CC )
100 eqid 
 |-  ( t e. CC |-> ( t + -u X ) ) = ( t e. CC |-> ( t + -u X ) )
101 100 addccncf 
 |-  ( -u X e. CC -> ( t e. CC |-> ( t + -u X ) ) e. ( CC -cn-> CC ) )
102 99 101 syl 
 |-  ( ph -> ( t e. CC |-> ( t + -u X ) ) e. ( CC -cn-> CC ) )
103 98 102 eqeltrd 
 |-  ( ph -> ( t e. CC |-> ( t - X ) ) e. ( CC -cn-> CC ) )
104 103 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. CC |-> ( t - X ) ) e. ( CC -cn-> CC ) )
105 ioossre 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
106 ax-resscn 
 |-  RR C_ CC
107 105 106 sstri 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
108 107 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
109 106 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> RR C_ CC )
110 92 104 108 109 71 cncfmptssg 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> RR ) )
111 85 recnd 
 |-  ( ( ph /\ s e. RR ) -> ( ( D ` N ) ` s ) e. CC )
112 111 86 fmptd 
 |-  ( ph -> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> CC )
113 ssid 
 |-  CC C_ CC
114 1 dirkerf 
 |-  ( N e. NN -> ( D ` N ) : RR --> RR )
115 6 114 syl 
 |-  ( ph -> ( D ` N ) : RR --> RR )
116 115 feqmptd 
 |-  ( ph -> ( D ` N ) = ( s e. RR |-> ( ( D ` N ) ` s ) ) )
117 1 dirkercncf 
 |-  ( N e. NN -> ( D ` N ) e. ( RR -cn-> RR ) )
118 6 117 syl 
 |-  ( ph -> ( D ` N ) e. ( RR -cn-> RR ) )
119 116 118 eqeltrrd 
 |-  ( ph -> ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> RR ) )
120 cncfcdm 
 |-  ( ( CC C_ CC /\ ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> RR ) ) -> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> CC ) <-> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> CC ) )
121 113 119 120 sylancr 
 |-  ( ph -> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> CC ) <-> ( s e. RR |-> ( ( D ` N ) ` s ) ) : RR --> CC ) )
122 112 121 mpbird 
 |-  ( ph -> ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> CC ) )
123 122 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. RR |-> ( ( D ` N ) ` s ) ) e. ( RR -cn-> CC ) )
124 110 123 cncfco 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( s e. RR |-> ( ( D ` N ) ` s ) ) o. ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( t - X ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
125 91 124 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
126 51 125 mulcncf 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
127 48 126 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
128 cncff 
 |-  ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
129 9 128 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
130 115 adantr 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( D ` N ) : RR --> RR )
131 elioore 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. RR )
132 131 adantl 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
133 7 adantr 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
134 132 133 resubcld 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( s - X ) e. RR )
135 130 134 ffvelcdmd 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` N ) ` ( s - X ) ) e. RR )
136 135 recnd 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` N ) ` ( s - X ) ) e. CC )
137 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) )
138 136 137 fmptd 
 |-  ( ph -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
139 138 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
140 eqid 
 |-  ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) )
141 oveq1 
 |-  ( t = ( Q ` i ) -> ( t - X ) = ( ( Q ` i ) - X ) )
142 141 fveq2d 
 |-  ( t = ( Q ` i ) -> ( ( D ` N ) ` ( t - X ) ) = ( ( D ` N ) ` ( ( Q ` i ) - X ) ) )
143 142 eqcomd 
 |-  ( t = ( Q ` i ) -> ( ( D ` N ) ` ( ( Q ` i ) - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
144 143 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ t = ( Q ` i ) ) -> ( ( D ` N ) ` ( ( Q ` i ) - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
145 eqidd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) )
146 oveq1 
 |-  ( s = t -> ( s - X ) = ( t - X ) )
147 146 fveq2d 
 |-  ( s = t -> ( ( D ` N ) ` ( s - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
148 147 adantl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) /\ s = t ) -> ( ( D ` N ) ` ( s - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
149 velsn 
 |-  ( t e. { ( Q ` i ) } <-> t = ( Q ` i ) )
150 149 notbii 
 |-  ( -. t e. { ( Q ` i ) } <-> -. t = ( Q ` i ) )
151 elunnel2 
 |-  ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) /\ -. t e. { ( Q ` i ) } ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
152 150 151 sylan2br 
 |-  ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) /\ -. t = ( Q ` i ) ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
153 152 adantll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
154 115 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( D ` N ) : RR --> RR )
155 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t = ( Q ` i ) ) -> t = ( Q ` i ) )
156 18 ssriv 
 |-  ( -u _pi [,] _pi ) C_ RR
157 fzossfz 
 |-  ( 0 ..^ M ) C_ ( 0 ... M )
158 157 44 sselid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
159 43 158 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( -u _pi [,] _pi ) )
160 156 159 sselid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
161 160 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t = ( Q ` i ) ) -> ( Q ` i ) e. RR )
162 155 161 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t = ( Q ` i ) ) -> t e. RR )
163 162 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ t = ( Q ` i ) ) -> t e. RR )
164 153 67 syl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) -> t e. RR )
165 163 164 pm2.61dan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> t e. RR )
166 7 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> X e. RR )
167 165 166 resubcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( t - X ) e. RR )
168 154 167 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
169 168 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
170 145 148 153 169 fvmptd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ -. t = ( Q ` i ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) = ( ( D ` N ) ` ( t - X ) ) )
171 144 170 ifeqda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> if ( t = ( Q ` i ) , ( ( D ` N ) ` ( ( Q ` i ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( D ` N ) ` ( t - X ) ) )
172 171 mpteq2dva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> if ( t = ( Q ` i ) , ( ( D ` N ) ` ( ( Q ` i ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) = ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) )
173 115 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( D ` N ) : RR --> RR )
174 elun 
 |-  ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) <-> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ s e. { ( Q ` i ) } ) )
175 174 bilani 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ s e. { ( Q ` i ) } ) )
176 elsni 
 |-  ( s e. { ( Q ` i ) } -> s = ( Q ` i ) )
177 176 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( Q ` i ) } ) -> s = ( Q ` i ) )
178 160 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( Q ` i ) } ) -> ( Q ` i ) e. RR )
179 177 178 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( Q ` i ) } ) -> s e. RR )
180 179 ex 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. { ( Q ` i ) } -> s e. RR ) )
181 180 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( s e. { ( Q ` i ) } -> s e. RR ) )
182 pm3.44 
 |-  ( ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. RR ) /\ ( s e. { ( Q ` i ) } -> s e. RR ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ s e. { ( Q ` i ) } ) -> s e. RR ) )
183 131 181 182 sylancr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ s e. { ( Q ` i ) } ) -> s e. RR ) )
184 175 183 mpd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> s e. RR )
185 7 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> X e. RR )
186 184 185 resubcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( s - X ) e. RR )
187 eqid 
 |-  ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) = ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) )
188 186 187 fmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) : ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) --> RR )
189 fcompt 
 |-  ( ( ( D ` N ) : RR --> RR /\ ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) : ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) --> RR ) -> ( ( D ` N ) o. ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ) = ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ` t ) ) ) )
190 173 188 189 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( D ` N ) o. ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ) = ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ` t ) ) ) )
191 eqidd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) = ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) )
192 146 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ s = t ) -> ( s - X ) = ( t - X ) )
193 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) )
194 191 192 193 167 fvmptd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ` t ) = ( t - X ) )
195 194 fveq2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( ( D ` N ) ` ( ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ` t ) ) = ( ( D ` N ) ` ( t - X ) ) )
196 195 mpteq2dva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ` t ) ) ) = ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) )
197 190 196 eqtr2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) = ( ( D ` N ) o. ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ) )
198 eqid 
 |-  ( s e. CC |-> ( s - X ) ) = ( s e. CC |-> ( s - X ) )
199 simpr 
 |-  ( ( ph /\ s e. CC ) -> s e. CC )
200 94 adantr 
 |-  ( ( ph /\ s e. CC ) -> X e. CC )
201 199 200 negsubd 
 |-  ( ( ph /\ s e. CC ) -> ( s + -u X ) = ( s - X ) )
202 201 eqcomd 
 |-  ( ( ph /\ s e. CC ) -> ( s - X ) = ( s + -u X ) )
203 202 mpteq2dva 
 |-  ( ph -> ( s e. CC |-> ( s - X ) ) = ( s e. CC |-> ( s + -u X ) ) )
204 eqid 
 |-  ( s e. CC |-> ( s + -u X ) ) = ( s e. CC |-> ( s + -u X ) )
205 204 addccncf 
 |-  ( -u X e. CC -> ( s e. CC |-> ( s + -u X ) ) e. ( CC -cn-> CC ) )
206 99 205 syl 
 |-  ( ph -> ( s e. CC |-> ( s + -u X ) ) e. ( CC -cn-> CC ) )
207 203 206 eqeltrd 
 |-  ( ph -> ( s e. CC |-> ( s - X ) ) e. ( CC -cn-> CC ) )
208 207 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. CC |-> ( s - X ) ) e. ( CC -cn-> CC ) )
209 160 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
210 209 snssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { ( Q ` i ) } C_ CC )
211 108 210 unssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) C_ CC )
212 198 208 211 109 186 cncfmptssg 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) e. ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) -cn-> RR ) )
213 116 122 eqeltrd 
 |-  ( ph -> ( D ` N ) e. ( RR -cn-> CC ) )
214 213 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( D ` N ) e. ( RR -cn-> CC ) )
215 212 214 cncfco 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( D ` N ) o. ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ) e. ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) -cn-> CC ) )
216 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
217 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) )
218 216 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
219 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
220 219 restid 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
221 218 220 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
222 221 eqcomi 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
223 216 217 222 cncfcn 
 |-  ( ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) C_ CC /\ CC C_ CC ) -> ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) Cn ( TopOpen ` CCfld ) ) )
224 211 113 223 sylancl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) Cn ( TopOpen ` CCfld ) ) )
225 215 224 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( D ` N ) o. ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( s - X ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) Cn ( TopOpen ` CCfld ) ) )
226 197 225 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) Cn ( TopOpen ` CCfld ) ) )
227 216 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
228 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) e. ( TopOn ` ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) )
229 227 211 228 sylancr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) e. ( TopOn ` ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) )
230 cncnp 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) e. ( TopOn ` ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) : ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) --> CC /\ A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) ) )
231 229 227 230 sylancl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) : ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) --> CC /\ A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) ) )
232 226 231 mpbid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) : ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) --> CC /\ A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) )
233 232 simprd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
234 eqidd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( Q ` i ) )
235 elsng 
 |-  ( ( Q ` i ) e. RR -> ( ( Q ` i ) e. { ( Q ` i ) } <-> ( Q ` i ) = ( Q ` i ) ) )
236 160 235 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) e. { ( Q ` i ) } <-> ( Q ` i ) = ( Q ` i ) ) )
237 234 236 mpbird 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. { ( Q ` i ) } )
238 237 olcd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ ( Q ` i ) e. { ( Q ` i ) } ) )
239 elun 
 |-  ( ( Q ` i ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) <-> ( ( Q ` i ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ ( Q ` i ) e. { ( Q ` i ) } ) )
240 238 239 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) )
241 fveq2 
 |-  ( s = ( Q ` i ) -> ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) = ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( Q ` i ) ) )
242 241 eleq2d 
 |-  ( s = ( Q ` i ) -> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) <-> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( Q ` i ) ) ) )
243 242 rspccva 
 |-  ( ( A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) /\ ( Q ` i ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( Q ` i ) ) )
244 233 240 243 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( Q ` i ) ) )
245 172 244 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> if ( t = ( Q ` i ) , ( ( D ` N ) ` ( ( Q ` i ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( Q ` i ) ) )
246 eqid 
 |-  ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> if ( t = ( Q ` i ) , ( ( D ` N ) ` ( ( Q ` i ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) = ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> if ( t = ( Q ` i ) , ( ( D ` N ) ` ( ( Q ` i ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) )
247 217 216 246 139 108 209 ellimc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( D ` N ) ` ( ( Q ` i ) - X ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) limCC ( Q ` i ) ) <-> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) |-> if ( t = ( Q ` i ) , ( ( D ` N ) ` ( ( Q ` i ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( Q ` i ) ) ) )
248 245 247 mpbird 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( D ` N ) ` ( ( Q ` i ) - X ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) limCC ( Q ` i ) ) )
249 129 139 140 10 248 mullimcf 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( R x. ( ( D ` N ) ` ( ( Q ` i ) - X ) ) ) e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) limCC ( Q ` i ) ) )
250 fvres 
 |-  ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) = ( F ` t ) )
251 250 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) = ( F ` t ) )
252 251 oveq1d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) )
253 252 mpteq2dva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) )
254 253 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) limCC ( Q ` i ) ) = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) limCC ( Q ` i ) ) )
255 249 254 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( R x. ( ( D ` N ) ` ( ( Q ` i ) - X ) ) ) e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) limCC ( Q ` i ) ) )
256 eqidd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) )
257 simpr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = t ) -> s = t )
258 257 oveq1d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = t ) -> ( s - X ) = ( t - X ) )
259 258 fveq2d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = t ) -> ( ( D ` N ) ` ( s - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
260 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
261 115 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( D ` N ) : RR --> RR )
262 261 71 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
263 256 259 260 262 fvmptd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) = ( ( D ` N ) ` ( t - X ) ) )
264 263 oveq2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) )
265 264 mpteq2dva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) )
266 265 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) limCC ( Q ` i ) ) = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) limCC ( Q ` i ) ) )
267 255 266 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( R x. ( ( D ` N ) ` ( ( Q ` i ) - X ) ) ) e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) limCC ( Q ` i ) ) )
268 48 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) = ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
269 268 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) limCC ( Q ` i ) ) = ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
270 267 269 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( R x. ( ( D ` N ) ` ( ( Q ` i ) - X ) ) ) e. ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
271 iftrue 
 |-  ( t = ( Q ` ( i + 1 ) ) -> if ( t = ( Q ` ( i + 1 ) ) , ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) )
272 oveq1 
 |-  ( t = ( Q ` ( i + 1 ) ) -> ( t - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
273 272 eqcomd 
 |-  ( t = ( Q ` ( i + 1 ) ) -> ( ( Q ` ( i + 1 ) ) - X ) = ( t - X ) )
274 273 fveq2d 
 |-  ( t = ( Q ` ( i + 1 ) ) -> ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
275 271 274 eqtrd 
 |-  ( t = ( Q ` ( i + 1 ) ) -> if ( t = ( Q ` ( i + 1 ) ) , ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( D ` N ) ` ( t - X ) ) )
276 275 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ t = ( Q ` ( i + 1 ) ) ) -> if ( t = ( Q ` ( i + 1 ) ) , ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( D ` N ) ` ( t - X ) ) )
277 iffalse 
 |-  ( -. t = ( Q ` ( i + 1 ) ) -> if ( t = ( Q ` ( i + 1 ) ) , ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) )
278 277 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ -. t = ( Q ` ( i + 1 ) ) ) -> if ( t = ( Q ` ( i + 1 ) ) , ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) )
279 eqidd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ -. t = ( Q ` ( i + 1 ) ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) )
280 147 adantl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ -. t = ( Q ` ( i + 1 ) ) ) /\ s = t ) -> ( ( D ` N ) ` ( s - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
281 elun 
 |-  ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) <-> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ t e. { ( Q ` ( i + 1 ) ) } ) )
282 281 biimpi 
 |-  ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ t e. { ( Q ` ( i + 1 ) ) } ) )
283 282 orcomd 
 |-  ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) -> ( t e. { ( Q ` ( i + 1 ) ) } \/ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
284 283 ad2antlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ -. t = ( Q ` ( i + 1 ) ) ) -> ( t e. { ( Q ` ( i + 1 ) ) } \/ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
285 velsn 
 |-  ( t e. { ( Q ` ( i + 1 ) ) } <-> t = ( Q ` ( i + 1 ) ) )
286 285 notbii 
 |-  ( -. t e. { ( Q ` ( i + 1 ) ) } <-> -. t = ( Q ` ( i + 1 ) ) )
287 286 bilanri 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ -. t = ( Q ` ( i + 1 ) ) ) -> -. t e. { ( Q ` ( i + 1 ) ) } )
288 pm2.53 
 |-  ( ( t e. { ( Q ` ( i + 1 ) ) } \/ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( -. t e. { ( Q ` ( i + 1 ) ) } -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
289 284 287 288 sylc 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ -. t = ( Q ` ( i + 1 ) ) ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
290 173 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ -. t = ( Q ` ( i + 1 ) ) ) -> ( D ` N ) : RR --> RR )
291 289 67 syl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ -. t = ( Q ` ( i + 1 ) ) ) -> t e. RR )
292 7 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ -. t = ( Q ` ( i + 1 ) ) ) -> X e. RR )
293 291 292 resubcld 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ -. t = ( Q ` ( i + 1 ) ) ) -> ( t - X ) e. RR )
294 290 293 ffvelcdmd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ -. t = ( Q ` ( i + 1 ) ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
295 279 280 289 294 fvmptd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ -. t = ( Q ` ( i + 1 ) ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) = ( ( D ` N ) ` ( t - X ) ) )
296 278 295 eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ -. t = ( Q ` ( i + 1 ) ) ) -> if ( t = ( Q ` ( i + 1 ) ) , ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( D ` N ) ` ( t - X ) ) )
297 276 296 pm2.61dan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) -> if ( t = ( Q ` ( i + 1 ) ) , ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) = ( ( D ` N ) ` ( t - X ) ) )
298 297 mpteq2dva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> if ( t = ( Q ` ( i + 1 ) ) , ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) = ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) )
299 eqid 
 |-  ( t e. RR |-> ( ( D ` N ) ` ( t - X ) ) ) = ( t e. RR |-> ( ( D ` N ) ` ( t - X ) ) )
300 106 a1i 
 |-  ( ph -> RR C_ CC )
301 simpr 
 |-  ( ( ph /\ t e. RR ) -> t e. RR )
302 7 adantr 
 |-  ( ( ph /\ t e. RR ) -> X e. RR )
303 301 302 resubcld 
 |-  ( ( ph /\ t e. RR ) -> ( t - X ) e. RR )
304 92 103 300 300 303 cncfmptssg 
 |-  ( ph -> ( t e. RR |-> ( t - X ) ) e. ( RR -cn-> RR ) )
305 304 213 cncfcompt 
 |-  ( ph -> ( t e. RR |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( RR -cn-> CC ) )
306 305 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. RR |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( RR -cn-> CC ) )
307 105 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
308 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
309 308 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
310 43 309 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( -u _pi [,] _pi ) )
311 156 310 sselid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
312 311 snssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { ( Q ` ( i + 1 ) ) } C_ RR )
313 307 312 unssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) C_ RR )
314 113 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> CC C_ CC )
315 173 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) -> ( D ` N ) : RR --> RR )
316 313 sselda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) -> t e. RR )
317 7 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) -> X e. RR )
318 316 317 resubcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) -> ( t - X ) e. RR )
319 315 318 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
320 319 recnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) -> ( ( D ` N ) ` ( t - X ) ) e. CC )
321 299 306 313 314 320 cncfmptssg 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) -cn-> CC ) )
322 156 106 sstri 
 |-  ( -u _pi [,] _pi ) C_ CC
323 322 310 sselid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
324 323 snssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { ( Q ` ( i + 1 ) ) } C_ CC )
325 108 324 unssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) C_ CC )
326 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) )
327 216 326 222 cncfcn 
 |-  ( ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) C_ CC /\ CC C_ CC ) -> ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) Cn ( TopOpen ` CCfld ) ) )
328 325 113 327 sylancl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) Cn ( TopOpen ` CCfld ) ) )
329 321 328 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) Cn ( TopOpen ` CCfld ) ) )
330 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) e. ( TopOn ` ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) )
331 227 325 330 sylancr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) e. ( TopOn ` ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) )
332 cncnp 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) e. ( TopOn ` ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) : ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) --> CC /\ A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) ) )
333 331 227 332 sylancl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) : ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) --> CC /\ A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) ) )
334 329 333 mpbid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) : ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) --> CC /\ A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) )
335 334 simprd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
336 eqidd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( i + 1 ) ) )
337 elsng 
 |-  ( ( Q ` ( i + 1 ) ) e. RR -> ( ( Q ` ( i + 1 ) ) e. { ( Q ` ( i + 1 ) ) } <-> ( Q ` ( i + 1 ) ) = ( Q ` ( i + 1 ) ) ) )
338 311 337 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) e. { ( Q ` ( i + 1 ) ) } <-> ( Q ` ( i + 1 ) ) = ( Q ` ( i + 1 ) ) ) )
339 336 338 mpbird 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. { ( Q ` ( i + 1 ) ) } )
340 339 olcd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ ( Q ` ( i + 1 ) ) e. { ( Q ` ( i + 1 ) ) } ) )
341 elun 
 |-  ( ( Q ` ( i + 1 ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) <-> ( ( Q ` ( i + 1 ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ ( Q ` ( i + 1 ) ) e. { ( Q ` ( i + 1 ) ) } ) )
342 340 341 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) )
343 fveq2 
 |-  ( s = ( Q ` ( i + 1 ) ) -> ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) = ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( Q ` ( i + 1 ) ) ) )
344 343 eleq2d 
 |-  ( s = ( Q ` ( i + 1 ) ) -> ( ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) <-> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( Q ` ( i + 1 ) ) ) ) )
345 344 rspccva 
 |-  ( ( A. s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) /\ ( Q ` ( i + 1 ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( Q ` ( i + 1 ) ) ) )
346 335 342 345 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( Q ` ( i + 1 ) ) ) )
347 298 346 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> if ( t = ( Q ` ( i + 1 ) ) , ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( Q ` ( i + 1 ) ) ) )
348 eqid 
 |-  ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> if ( t = ( Q ` ( i + 1 ) ) , ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) = ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> if ( t = ( Q ` ( i + 1 ) ) , ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) )
349 326 216 348 139 108 323 ellimc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) limCC ( Q ` ( i + 1 ) ) ) <-> ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) |-> if ( t = ( Q ` ( i + 1 ) ) , ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( Q ` ( i + 1 ) ) ) ) )
350 347 349 mpbird 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
351 129 139 140 11 350 mullimcf 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( L x. ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) ) e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
352 265 253 48 3eqtr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) = ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
353 352 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
354 351 353 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( L x. ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) ) e. ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
355 2 32 5 4 7 33 127 270 354 fourierdlem93 
 |-  ( ph -> S. ( -u _pi [,] _pi ) ( G ` t ) _d t = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( G ` ( X + s ) ) _d s )
356 3 a1i 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> G = ( t e. ( -u _pi [,] _pi ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) )
357 fveq2 
 |-  ( t = ( X + s ) -> ( F ` t ) = ( F ` ( X + s ) ) )
358 357 oveq1d 
 |-  ( t = ( X + s ) -> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` N ) ` ( t - X ) ) ) )
359 358 adantl 
 |-  ( ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) /\ t = ( X + s ) ) -> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` N ) ` ( t - X ) ) ) )
360 oveq1 
 |-  ( t = ( X + s ) -> ( t - X ) = ( ( X + s ) - X ) )
361 94 adantr 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> X e. CC )
362 36 7 resubcld 
 |-  ( ph -> ( -u _pi - X ) e. RR )
363 362 adantr 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( -u _pi - X ) e. RR )
364 39 7 resubcld 
 |-  ( ph -> ( _pi - X ) e. RR )
365 364 adantr 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( _pi - X ) e. RR )
366 simpr 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) )
367 eliccre 
 |-  ( ( ( -u _pi - X ) e. RR /\ ( _pi - X ) e. RR /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> s e. RR )
368 363 365 366 367 syl3anc 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> s e. RR )
369 368 recnd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> s e. CC )
370 361 369 pncan2d 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( ( X + s ) - X ) = s )
371 360 370 sylan9eqr 
 |-  ( ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) /\ t = ( X + s ) ) -> ( t - X ) = s )
372 371 fveq2d 
 |-  ( ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) /\ t = ( X + s ) ) -> ( ( D ` N ) ` ( t - X ) ) = ( ( D ` N ) ` s ) )
373 372 oveq2d 
 |-  ( ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) /\ t = ( X + s ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` N ) ` ( t - X ) ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` N ) ` s ) ) )
374 359 373 eqtrd 
 |-  ( ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) /\ t = ( X + s ) ) -> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` N ) ` s ) ) )
375 16 a1i 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> -u _pi e. RR )
376 15 a1i 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> _pi e. RR )
377 7 adantr 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> X e. RR )
378 377 368 readdcld 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + s ) e. RR )
379 36 recnd 
 |-  ( ph -> -u _pi e. CC )
380 94 379 pncan3d 
 |-  ( ph -> ( X + ( -u _pi - X ) ) = -u _pi )
381 380 eqcomd 
 |-  ( ph -> -u _pi = ( X + ( -u _pi - X ) ) )
382 381 adantr 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> -u _pi = ( X + ( -u _pi - X ) ) )
383 elicc2 
 |-  ( ( ( -u _pi - X ) e. RR /\ ( _pi - X ) e. RR ) -> ( s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) <-> ( s e. RR /\ ( -u _pi - X ) <_ s /\ s <_ ( _pi - X ) ) ) )
384 363 365 383 syl2anc 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) <-> ( s e. RR /\ ( -u _pi - X ) <_ s /\ s <_ ( _pi - X ) ) ) )
385 366 384 mpbid 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( s e. RR /\ ( -u _pi - X ) <_ s /\ s <_ ( _pi - X ) ) )
386 385 simp2d 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( -u _pi - X ) <_ s )
387 363 368 377 386 leadd2dd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + ( -u _pi - X ) ) <_ ( X + s ) )
388 382 387 eqbrtrd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> -u _pi <_ ( X + s ) )
389 385 simp3d 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> s <_ ( _pi - X ) )
390 368 365 377 389 leadd2dd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + s ) <_ ( X + ( _pi - X ) ) )
391 picn 
 |-  _pi e. CC
392 391 a1i 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> _pi e. CC )
393 361 392 pncan3d 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + ( _pi - X ) ) = _pi )
394 390 393 breqtrd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + s ) <_ _pi )
395 375 376 378 388 394 eliccd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + s ) e. ( -u _pi [,] _pi ) )
396 8 adantr 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> F : ( -u _pi [,] _pi ) --> CC )
397 396 395 ffvelcdmd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( F ` ( X + s ) ) e. CC )
398 368 111 syldan 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( ( D ` N ) ` s ) e. CC )
399 397 398 mulcld 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` N ) ` s ) ) e. CC )
400 356 374 395 399 fvmptd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( G ` ( X + s ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` N ) ` s ) ) )
401 400 itgeq2dv 
 |-  ( ph -> S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( G ` ( X + s ) ) _d s = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( ( F ` ( X + s ) ) x. ( ( D ` N ) ` s ) ) _d s )
402 29 355 401 3eqtrd 
 |-  ( ph -> 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 )