Metamath Proof Explorer

Theorem fourierdlem85

Description: Limit of the function G at the lower bounds of the partition intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem85.p 
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` m ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem85.f 
|- ( ph -> F : RR --> RR )
fourierdlem85.x 
|- ( ph -> X e. ran V )
fourierdlem85.y 
|- ( ph -> Y e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
fourierdlem85.w 
|- ( ph -> W e. RR )
fourierdlem85.h 
|- H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
fourierdlem85.k 
|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
fourierdlem85.u 
|- U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
fourierdlem85.n 
|- ( ph -> N e. RR )
fourierdlem85.s 
|- S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) )
fourierdlem85.g 
|- G = ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )
fourierdlem85.m 
|- ( ph -> M e. NN )
fourierdlem85.v 
|- ( ph -> V e. ( P ` M ) )
fourierdlem85.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` i ) ) )
fourierdlem85.q 
|- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
fourierdlem85.o 
|- O = ( 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 ) ) ) } )
fourierdlem85.i 
|- I = ( RR _D F )
fourierdlem85.ifn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( I |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> CC )
fourierdlem85.e 
|- ( ph -> E e. ( ( I |` ( X (,) +oo ) ) limCC X ) )
fourierdlem85.a 
|- A = ( ( if ( ( V ` i ) = X , E , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) ) x. ( K ` ( Q ` i ) ) ) x. ( S ` ( Q ` i ) ) )
Assertion fourierdlem85 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem85.p 
 |-  P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` m ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
2 fourierdlem85.f 
 |-  ( ph -> F : RR --> RR )
3 fourierdlem85.x 
 |-  ( ph -> X e. ran V )
4 fourierdlem85.y 
 |-  ( ph -> Y e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
5 fourierdlem85.w 
 |-  ( ph -> W e. RR )
6 fourierdlem85.h 
 |-  H = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , Y , W ) ) / s ) ) )
7 fourierdlem85.k 
 |-  K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
8 fourierdlem85.u 
 |-  U = ( s e. ( -u _pi [,] _pi ) |-> ( ( H ` s ) x. ( K ` s ) ) )
9 fourierdlem85.n 
 |-  ( ph -> N e. RR )
10 fourierdlem85.s 
 |-  S = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) )
11 fourierdlem85.g 
 |-  G = ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) )
12 fourierdlem85.m 
 |-  ( ph -> M e. NN )
13 fourierdlem85.v 
 |-  ( ph -> V e. ( P ` M ) )
14 fourierdlem85.r 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` i ) ) )
15 fourierdlem85.q 
 |-  Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
16 fourierdlem85.o 
 |-  O = ( 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 ) ) ) } )
17 fourierdlem85.i 
 |-  I = ( RR _D F )
18 fourierdlem85.ifn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( I |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> CC )
19 fourierdlem85.e 
 |-  ( ph -> E e. ( ( I |` ( X (,) +oo ) ) limCC X ) )
20 fourierdlem85.a 
 |-  A = ( ( if ( ( V ` i ) = X , E , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) ) x. ( K ` ( Q ` i ) ) ) x. ( S ` ( Q ` i ) ) )
21 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( U ` s ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( U ` s ) )
22 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( S ` s ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( S ` s ) )
23 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( U ` s ) x. ( S ` s ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( U ` s ) x. ( S ` s ) ) )
24 pire 
 |-  _pi e. RR
25 24 renegcli 
 |-  -u _pi e. RR
26 25 rexri 
 |-  -u _pi e. RR*
27 26 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> -u _pi e. RR* )
28 24 rexri 
 |-  _pi e. RR*
29 28 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> _pi e. RR* )
30 24 a1i 
 |-  ( ph -> _pi e. RR )
31 30 renegcld 
 |-  ( ph -> -u _pi e. RR )
32 1 fourierdlem2 
 |-  ( M e. NN -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
33 12 32 syl 
 |-  ( ph -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
34 13 33 mpbid 
 |-  ( ph -> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) )
35 34 simpld 
 |-  ( ph -> V e. ( RR ^m ( 0 ... M ) ) )
36 elmapi 
 |-  ( V e. ( RR ^m ( 0 ... M ) ) -> V : ( 0 ... M ) --> RR )
37 frn 
 |-  ( V : ( 0 ... M ) --> RR -> ran V C_ RR )
38 35 36 37 3syl 
 |-  ( ph -> ran V C_ RR )
39 38 3 sseldd 
 |-  ( ph -> X e. RR )
40 31 30 39 1 16 12 13 15 fourierdlem14 
 |-  ( ph -> Q e. ( O ` M ) )
41 16 12 40 fourierdlem15 
 |-  ( ph -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
42 41 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
43 42 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
44 simplr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0 ..^ M ) )
45 27 29 43 44 fourierdlem8 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
46 ioossicc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
47 46 sseli 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
48 47 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
49 45 48 sseldd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. ( -u _pi [,] _pi ) )
50 ioossre 
 |-  ( X (,) +oo ) C_ RR
51 50 a1i 
 |-  ( ph -> ( X (,) +oo ) C_ RR )
52 2 51 fssresd 
 |-  ( ph -> ( F |` ( X (,) +oo ) ) : ( X (,) +oo ) --> RR )
53 ax-resscn 
 |-  RR C_ CC
54 51 53 sstrdi 
 |-  ( ph -> ( X (,) +oo ) C_ CC )
55 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
56 pnfxr 
 |-  +oo e. RR*
57 56 a1i 
 |-  ( ph -> +oo e. RR* )
58 39 ltpnfd 
 |-  ( ph -> X < +oo )
59 55 57 39 58 lptioo1cn 
 |-  ( ph -> X e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( X (,) +oo ) ) )
60 52 54 59 4 limcrecl 
 |-  ( ph -> Y e. RR )
61 2 39 60 5 6 fourierdlem9 
 |-  ( ph -> H : ( -u _pi [,] _pi ) --> RR )
62 53 a1i 
 |-  ( ph -> RR C_ CC )
63 61 62 fssd 
 |-  ( ph -> H : ( -u _pi [,] _pi ) --> CC )
64 63 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> H : ( -u _pi [,] _pi ) --> CC )
65 64 49 ffvelrnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( H ` s ) e. CC )
66 7 fourierdlem43 
 |-  K : ( -u _pi [,] _pi ) --> RR
67 66 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> K : ( -u _pi [,] _pi ) --> RR )
68 67 49 ffvelrnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( K ` s ) e. RR )
69 68 recnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( K ` s ) e. CC )
70 65 69 mulcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( H ` s ) x. ( K ` s ) ) e. CC )
71 8 fvmpt2 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ ( ( H ` s ) x. ( K ` s ) ) e. CC ) -> ( U ` s ) = ( ( H ` s ) x. ( K ` s ) ) )
72 49 70 71 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( U ` s ) = ( ( H ` s ) x. ( K ` s ) ) )
73 72 70 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( U ` s ) e. CC )
74 9 10 fourierdlem18 
 |-  ( ph -> S e. ( ( -u _pi [,] _pi ) -cn-> RR ) )
75 cncff 
 |-  ( S e. ( ( -u _pi [,] _pi ) -cn-> RR ) -> S : ( -u _pi [,] _pi ) --> RR )
76 74 75 syl 
 |-  ( ph -> S : ( -u _pi [,] _pi ) --> RR )
77 76 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S : ( -u _pi [,] _pi ) --> RR )
78 77 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> S : ( -u _pi [,] _pi ) --> RR )
79 78 49 ffvelrnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( S ` s ) e. RR )
80 79 recnd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( S ` s ) e. CC )
81 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( H ` s ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( H ` s ) )
82 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( K ` s ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( K ` s ) )
83 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( H ` s ) x. ( K ` s ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( H ` s ) x. ( K ` s ) ) )
84 eqid 
 |-  if ( ( V ` i ) = X , E , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) ) = if ( ( V ` i ) = X , E , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) )
85 39 1 2 3 4 5 6 12 13 14 15 16 17 18 19 84 fourierdlem75 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> if ( ( V ` i ) = X , E , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) ) e. ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
86 61 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> H : ( -u _pi [,] _pi ) --> RR )
87 26 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -u _pi e. RR* )
88 28 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> _pi e. RR* )
89 simpr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
90 87 88 42 89 fourierdlem8 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
91 46 90 sstrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
92 86 91 feqresmpt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( H ` s ) ) )
93 92 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( H ` s ) ) limCC ( Q ` i ) ) )
94 85 93 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> if ( ( V ` i ) = X , E , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( H ` s ) ) limCC ( Q ` i ) ) )
95 limcresi 
 |-  ( K limCC ( Q ` i ) ) C_ ( ( K |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) )
96 ssid 
 |-  CC C_ CC
97 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( ( -u _pi [,] _pi ) -cn-> RR ) C_ ( ( -u _pi [,] _pi ) -cn-> CC ) )
98 53 96 97 mp2an 
 |-  ( ( -u _pi [,] _pi ) -cn-> RR ) C_ ( ( -u _pi [,] _pi ) -cn-> CC )
99 7 fourierdlem62 
 |-  K e. ( ( -u _pi [,] _pi ) -cn-> RR )
100 98 99 sselii 
 |-  K e. ( ( -u _pi [,] _pi ) -cn-> CC )
101 100 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> K e. ( ( -u _pi [,] _pi ) -cn-> CC ) )
102 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
103 102 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
104 42 103 ffvelrnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( -u _pi [,] _pi ) )
105 101 104 cnlimci 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( K ` ( Q ` i ) ) e. ( K limCC ( Q ` i ) ) )
106 95 105 sselid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( K ` ( Q ` i ) ) e. ( ( K |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
107 cncff 
 |-  ( K e. ( ( -u _pi [,] _pi ) -cn-> CC ) -> K : ( -u _pi [,] _pi ) --> CC )
108 100 107 mp1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> K : ( -u _pi [,] _pi ) --> CC )
109 108 91 feqresmpt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( K |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( K ` s ) ) )
110 109 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( K |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( K ` s ) ) limCC ( Q ` i ) ) )
111 106 110 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( K ` ( Q ` i ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( K ` s ) ) limCC ( Q ` i ) ) )
112 81 82 83 65 69 94 111 mullimc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( if ( ( V ` i ) = X , E , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) ) x. ( K ` ( Q ` i ) ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( H ` s ) x. ( K ` s ) ) ) limCC ( Q ` i ) ) )
113 72 mpteq2dva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( U ` s ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( H ` s ) x. ( K ` s ) ) ) )
114 113 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( U ` s ) ) limCC ( Q ` i ) ) = ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( H ` s ) x. ( K ` s ) ) ) limCC ( Q ` i ) ) )
115 112 114 eleqtrrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( if ( ( V ` i ) = X , E , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) ) x. ( K ` ( Q ` i ) ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( U ` s ) ) limCC ( Q ` i ) ) )
116 limcresi 
 |-  ( S limCC ( Q ` i ) ) C_ ( ( S |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) )
117 74 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S e. ( ( -u _pi [,] _pi ) -cn-> RR ) )
118 117 104 cnlimci 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` ( Q ` i ) ) e. ( S limCC ( Q ` i ) ) )
119 116 118 sselid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` ( Q ` i ) ) e. ( ( S |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
120 77 91 feqresmpt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( S ` s ) ) )
121 120 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( S |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( S ` s ) ) limCC ( Q ` i ) ) )
122 119 121 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( S ` ( Q ` i ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( S ` s ) ) limCC ( Q ` i ) ) )
123 21 22 23 73 80 115 122 mullimc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( if ( ( V ` i ) = X , E , ( ( R - if ( ( V ` i ) < X , W , Y ) ) / ( Q ` i ) ) ) x. ( K ` ( Q ` i ) ) ) x. ( S ` ( Q ` i ) ) ) e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( U ` s ) x. ( S ` s ) ) ) limCC ( Q ` i ) ) )
124 20 123 eqeltrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( U ` s ) x. ( S ` s ) ) ) limCC ( Q ` i ) ) )
125 11 reseq1i 
 |-  ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
126 91 resmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( s e. ( -u _pi [,] _pi ) |-> ( ( U ` s ) x. ( S ` s ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( U ` s ) x. ( S ` s ) ) ) )
127 125 126 eqtr2id 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( U ` s ) x. ( S ` s ) ) ) = ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
128 127 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( U ` s ) x. ( S ` s ) ) ) limCC ( Q ` i ) ) = ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
129 124 128 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A e. ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )