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 ffvelrnda 
 |-  ( ( 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 syl5eq 
 |-  ( ( 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 ffvelrnda 
 |-  ( ( ( 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 cncffvrn 
 |-  ( ( 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 ffvelrnd 
 |-  ( ( 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 sseldi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
159 43 158 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( -u _pi [,] _pi ) )
160 156 159 sseldi 
 |-  ( ( 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 ffvelrnd 
 |-  ( ( ( 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 simpr 
 |-  ( ( ph /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) )
175 elun 
 |-  ( s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) <-> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ s e. { ( Q ` i ) } ) )
176 174 175 sylib 
 |-  ( ( ph /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ s e. { ( Q ` i ) } ) )
177 176 adantlr 
 |-  ( ( ( 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 ) } ) )
178 elsni 
 |-  ( s e. { ( Q ` i ) } -> s = ( Q ` i ) )
179 178 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( Q ` i ) } ) -> s = ( Q ` i ) )
180 160 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( Q ` i ) } ) -> ( Q ` i ) e. RR )
181 179 180 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( Q ` i ) } ) -> s e. RR )
182 181 ex 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. { ( Q ` i ) } -> s e. RR ) )
183 182 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( s e. { ( Q ` i ) } -> s e. RR ) )
184 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 ) )
185 131 183 184 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 ) )
186 177 185 mpd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> s e. RR )
187 7 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> X e. RR )
188 186 187 resubcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) -> ( s - X ) e. RR )
189 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 ) )
190 188 189 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 )
191 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 ) ) ) )
192 173 190 191 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 ) ) ) )
193 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 ) ) )
194 146 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) /\ s = t ) -> ( s - X ) = ( t - X ) )
195 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 ) } ) )
196 193 194 195 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 ) )
197 196 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 ) ) )
198 197 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 ) ) ) )
199 192 198 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 ) ) ) )
200 eqid 
 |-  ( s e. CC |-> ( s - X ) ) = ( s e. CC |-> ( s - X ) )
201 simpr 
 |-  ( ( ph /\ s e. CC ) -> s e. CC )
202 94 adantr 
 |-  ( ( ph /\ s e. CC ) -> X e. CC )
203 201 202 negsubd 
 |-  ( ( ph /\ s e. CC ) -> ( s + -u X ) = ( s - X ) )
204 203 eqcomd 
 |-  ( ( ph /\ s e. CC ) -> ( s - X ) = ( s + -u X ) )
205 204 mpteq2dva 
 |-  ( ph -> ( s e. CC |-> ( s - X ) ) = ( s e. CC |-> ( s + -u X ) ) )
206 eqid 
 |-  ( s e. CC |-> ( s + -u X ) ) = ( s e. CC |-> ( s + -u X ) )
207 206 addccncf 
 |-  ( -u X e. CC -> ( s e. CC |-> ( s + -u X ) ) e. ( CC -cn-> CC ) )
208 99 207 syl 
 |-  ( ph -> ( s e. CC |-> ( s + -u X ) ) e. ( CC -cn-> CC ) )
209 205 208 eqeltrd 
 |-  ( ph -> ( s e. CC |-> ( s - X ) ) e. ( CC -cn-> CC ) )
210 209 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. CC |-> ( s - X ) ) e. ( CC -cn-> CC ) )
211 160 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
212 211 snssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { ( Q ` i ) } C_ CC )
213 108 212 unssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) C_ CC )
214 200 210 213 109 188 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 ) )
215 116 122 eqeltrd 
 |-  ( ph -> ( D ` N ) e. ( RR -cn-> CC ) )
216 215 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( D ` N ) e. ( RR -cn-> CC ) )
217 214 216 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 ) )
218 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
219 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) )
220 218 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
221 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
222 221 restid 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
223 220 222 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
224 223 eqcomi 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
225 218 219 224 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 ) ) )
226 213 113 225 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 ) ) )
227 217 226 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 ) ) )
228 199 227 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 ) ) )
229 218 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
230 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 ) } ) ) )
231 229 213 230 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 ) } ) ) )
232 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 ) ) ) )
233 231 229 232 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 ) ) ) )
234 228 233 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 ) ) )
235 234 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 ) )
236 eqidd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( Q ` i ) )
237 elsng 
 |-  ( ( Q ` i ) e. RR -> ( ( Q ` i ) e. { ( Q ` i ) } <-> ( Q ` i ) = ( Q ` i ) ) )
238 160 237 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) e. { ( Q ` i ) } <-> ( Q ` i ) = ( Q ` i ) ) )
239 236 238 mpbird 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. { ( Q ` i ) } )
240 239 olcd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ ( Q ` i ) e. { ( Q ` i ) } ) )
241 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 ) } ) )
242 240 241 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` i ) } ) )
243 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 ) ) )
244 243 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 ) ) ) )
245 244 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 ) ) )
246 235 242 245 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 ) ) )
247 172 246 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 ) ) )
248 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 ) ) )
249 219 218 248 139 108 211 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 ) ) ) )
250 247 249 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 ) ) )
251 129 139 140 10 250 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 ) ) )
252 fvres 
 |-  ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) = ( F ` t ) )
253 252 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) = ( F ` 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 ) ) = ( ( F ` t ) x. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( D ` N ) ` ( s - X ) ) ) ` t ) ) )
255 254 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 ) ) ) )
256 255 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 ) ) )
257 251 256 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 ) ) )
258 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 ) ) ) )
259 simpr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = t ) -> s = t )
260 259 oveq1d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = t ) -> ( s - X ) = ( t - X ) )
261 260 fveq2d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) /\ s = t ) -> ( ( D ` N ) ` ( s - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
262 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
263 115 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( D ` N ) : RR --> RR )
264 263 71 ffvelrnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
265 258 261 262 264 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 ) ) )
266 265 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 ) ) ) )
267 266 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 ) ) ) ) )
268 267 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 ) ) )
269 257 268 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 ) ) )
270 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 ) ) ) ) )
271 270 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 ) ) )
272 269 271 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( R x. ( ( D ` N ) ` ( ( Q ` i ) - X ) ) ) e. ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
273 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 ) ) )
274 oveq1 
 |-  ( t = ( Q ` ( i + 1 ) ) -> ( t - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
275 274 eqcomd 
 |-  ( t = ( Q ` ( i + 1 ) ) -> ( ( Q ` ( i + 1 ) ) - X ) = ( t - X ) )
276 275 fveq2d 
 |-  ( t = ( Q ` ( i + 1 ) ) -> ( ( D ` N ) ` ( ( Q ` ( i + 1 ) ) - X ) ) = ( ( D ` N ) ` ( t - X ) ) )
277 273 276 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 ) ) )
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 ) ) = ( ( D ` N ) ` ( t - X ) ) )
279 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 ) )
280 279 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 ) )
281 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 ) ) ) )
282 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 ) ) )
283 elun 
 |-  ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) <-> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ t e. { ( Q ` ( i + 1 ) ) } ) )
284 283 biimpi 
 |-  ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ t e. { ( Q ` ( i + 1 ) ) } ) )
285 284 orcomd 
 |-  ( t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) -> ( t e. { ( Q ` ( i + 1 ) ) } \/ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
286 285 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 ) ) ) ) )
287 velsn 
 |-  ( t e. { ( Q ` ( i + 1 ) ) } <-> t = ( Q ` ( i + 1 ) ) )
288 287 notbii 
 |-  ( -. t e. { ( Q ` ( i + 1 ) ) } <-> -. t = ( Q ` ( i + 1 ) ) )
289 288 biimpri 
 |-  ( -. t = ( Q ` ( i + 1 ) ) -> -. t e. { ( Q ` ( i + 1 ) ) } )
290 289 adantl 
 |-  ( ( ( ( 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 ) ) } )
291 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 ) ) ) ) )
292 286 290 291 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 ) ) ) )
293 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 )
294 292 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 )
295 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 )
296 294 295 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 )
297 293 296 ffvelrnd 
 |-  ( ( ( ( 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 )
298 281 282 292 297 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 ) ) )
299 280 298 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 ) ) )
300 278 299 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 ) ) )
301 300 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 ) ) ) )
302 eqid 
 |-  ( t e. RR |-> ( ( D ` N ) ` ( t - X ) ) ) = ( t e. RR |-> ( ( D ` N ) ` ( t - X ) ) )
303 106 a1i 
 |-  ( ph -> RR C_ CC )
304 simpr 
 |-  ( ( ph /\ t e. RR ) -> t e. RR )
305 7 adantr 
 |-  ( ( ph /\ t e. RR ) -> X e. RR )
306 304 305 resubcld 
 |-  ( ( ph /\ t e. RR ) -> ( t - X ) e. RR )
307 92 103 303 303 306 cncfmptssg 
 |-  ( ph -> ( t e. RR |-> ( t - X ) ) e. ( RR -cn-> RR ) )
308 307 215 cncfcompt 
 |-  ( ph -> ( t e. RR |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( RR -cn-> CC ) )
309 308 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. RR |-> ( ( D ` N ) ` ( t - X ) ) ) e. ( RR -cn-> CC ) )
310 105 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
311 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
312 311 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
313 43 312 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( -u _pi [,] _pi ) )
314 156 313 sseldi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
315 314 snssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { ( Q ` ( i + 1 ) ) } C_ RR )
316 310 315 unssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) C_ RR )
317 113 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> CC C_ CC )
318 173 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) -> ( D ` N ) : RR --> RR )
319 316 sselda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) -> t e. RR )
320 7 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) -> X e. RR )
321 319 320 resubcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) -> ( t - X ) e. RR )
322 318 321 ffvelrnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) -> ( ( D ` N ) ` ( t - X ) ) e. RR )
323 322 recnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) -> ( ( D ` N ) ` ( t - X ) ) e. CC )
324 302 309 316 317 323 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 ) )
325 156 106 sstri 
 |-  ( -u _pi [,] _pi ) C_ CC
326 325 313 sseldi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
327 326 snssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> { ( Q ` ( i + 1 ) ) } C_ CC )
328 108 327 unssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) C_ CC )
329 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 ) ) } ) )
330 218 329 224 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 ) ) )
331 328 113 330 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 ) ) )
332 324 331 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 ) ) )
333 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 ) ) } ) ) )
334 229 328 333 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 ) ) } ) ) )
335 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 ) ) ) )
336 334 229 335 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 ) ) ) )
337 332 336 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 ) ) )
338 337 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 ) )
339 eqidd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) = ( Q ` ( i + 1 ) ) )
340 elsng 
 |-  ( ( Q ` ( i + 1 ) ) e. RR -> ( ( Q ` ( i + 1 ) ) e. { ( Q ` ( i + 1 ) ) } <-> ( Q ` ( i + 1 ) ) = ( Q ` ( i + 1 ) ) ) )
341 314 340 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) e. { ( Q ` ( i + 1 ) ) } <-> ( Q ` ( i + 1 ) ) = ( Q ` ( i + 1 ) ) ) )
342 339 341 mpbird 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. { ( Q ` ( i + 1 ) ) } )
343 342 olcd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) \/ ( Q ` ( i + 1 ) ) e. { ( Q ` ( i + 1 ) ) } ) )
344 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 ) ) } ) )
345 343 344 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) )
346 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 ) ) ) )
347 346 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 ) ) ) ) )
348 347 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 ) ) ) )
349 338 345 348 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 ) ) ) )
350 301 349 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 ) ) ) )
351 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 ) ) )
352 329 218 351 139 108 326 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 ) ) ) ) )
353 350 352 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 ) ) ) )
354 129 139 140 11 353 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 ) ) ) )
355 267 255 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 ) ) ) ) )
356 355 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 ) ) ) )
357 354 356 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 ) ) ) )
358 2 32 5 4 7 33 127 272 357 fourierdlem93 
 |-  ( ph -> S. ( -u _pi [,] _pi ) ( G ` t ) _d t = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( G ` ( X + s ) ) _d s )
359 3 a1i 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> G = ( t e. ( -u _pi [,] _pi ) |-> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) ) )
360 fveq2 
 |-  ( t = ( X + s ) -> ( F ` t ) = ( F ` ( X + s ) ) )
361 360 oveq1d 
 |-  ( t = ( X + s ) -> ( ( F ` t ) x. ( ( D ` N ) ` ( t - X ) ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` N ) ` ( t - X ) ) ) )
362 361 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 ) ) ) )
363 oveq1 
 |-  ( t = ( X + s ) -> ( t - X ) = ( ( X + s ) - X ) )
364 94 adantr 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> X e. CC )
365 36 7 resubcld 
 |-  ( ph -> ( -u _pi - X ) e. RR )
366 365 adantr 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( -u _pi - X ) e. RR )
367 39 7 resubcld 
 |-  ( ph -> ( _pi - X ) e. RR )
368 367 adantr 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( _pi - X ) e. RR )
369 simpr 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) )
370 eliccre 
 |-  ( ( ( -u _pi - X ) e. RR /\ ( _pi - X ) e. RR /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> s e. RR )
371 366 368 369 370 syl3anc 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> s e. RR )
372 371 recnd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> s e. CC )
373 364 372 pncan2d 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( ( X + s ) - X ) = s )
374 363 373 sylan9eqr 
 |-  ( ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) /\ t = ( X + s ) ) -> ( t - X ) = s )
375 374 fveq2d 
 |-  ( ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) /\ t = ( X + s ) ) -> ( ( D ` N ) ` ( t - X ) ) = ( ( D ` N ) ` s ) )
376 375 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 ) ) )
377 362 376 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 ) ) )
378 16 a1i 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> -u _pi e. RR )
379 15 a1i 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> _pi e. RR )
380 7 adantr 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> X e. RR )
381 380 371 readdcld 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + s ) e. RR )
382 36 recnd 
 |-  ( ph -> -u _pi e. CC )
383 94 382 pncan3d 
 |-  ( ph -> ( X + ( -u _pi - X ) ) = -u _pi )
384 383 eqcomd 
 |-  ( ph -> -u _pi = ( X + ( -u _pi - X ) ) )
385 384 adantr 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> -u _pi = ( X + ( -u _pi - X ) ) )
386 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 ) ) ) )
387 366 368 386 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 ) ) ) )
388 369 387 mpbid 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( s e. RR /\ ( -u _pi - X ) <_ s /\ s <_ ( _pi - X ) ) )
389 388 simp2d 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( -u _pi - X ) <_ s )
390 366 371 380 389 leadd2dd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + ( -u _pi - X ) ) <_ ( X + s ) )
391 385 390 eqbrtrd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> -u _pi <_ ( X + s ) )
392 388 simp3d 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> s <_ ( _pi - X ) )
393 371 368 380 392 leadd2dd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + s ) <_ ( X + ( _pi - X ) ) )
394 picn 
 |-  _pi e. CC
395 394 a1i 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> _pi e. CC )
396 364 395 pncan3d 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + ( _pi - X ) ) = _pi )
397 393 396 breqtrd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + s ) <_ _pi )
398 378 379 381 391 397 eliccd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( X + s ) e. ( -u _pi [,] _pi ) )
399 8 adantr 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> F : ( -u _pi [,] _pi ) --> CC )
400 399 398 ffvelrnd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( F ` ( X + s ) ) e. CC )
401 371 111 syldan 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( ( D ` N ) ` s ) e. CC )
402 400 401 mulcld 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` N ) ` s ) ) e. CC )
403 359 377 398 402 fvmptd 
 |-  ( ( ph /\ s e. ( ( -u _pi - X ) [,] ( _pi - X ) ) ) -> ( G ` ( X + s ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` N ) ` s ) ) )
404 403 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 )
405 29 358 404 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 )