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 sseldi
 |-  ( ( 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 sseldi
 |-  ( ( 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 ) ) )