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

Metamath Proof Explorer

Theorem fourierdlem93

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

Ref Expression
Hypotheses fourierdlem93.1 
|- 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 ) ) ) } )
fourierdlem93.2 
|- H = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )
fourierdlem93.3 
|- ( ph -> M e. NN )
fourierdlem93.4 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem93.5 
|- ( ph -> X e. RR )
fourierdlem93.6 
|- ( ph -> F : ( -u _pi [,] _pi ) --> CC )
fourierdlem93.7 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem93.8 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
fourierdlem93.9 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
Assertion fourierdlem93 
|- ( ph -> S. ( -u _pi [,] _pi ) ( F ` t ) _d t = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( F ` ( X + s ) ) _d s )

Proof

Step Hyp Ref Expression
1 fourierdlem93.1 
 |-  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 ) ) ) } )
2 fourierdlem93.2 
 |-  H = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )
3 fourierdlem93.3 
 |-  ( ph -> M e. NN )
4 fourierdlem93.4 
 |-  ( ph -> Q e. ( P ` M ) )
5 fourierdlem93.5 
 |-  ( ph -> X e. RR )
6 fourierdlem93.6 
 |-  ( ph -> F : ( -u _pi [,] _pi ) --> CC )
7 fourierdlem93.7 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
8 fourierdlem93.8 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
9 fourierdlem93.9 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
10 1 fourierdlem2 
 |-  ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
11 3 10 syl 
 |-  ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
12 4 11 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
13 12 simprd 
 |-  ( ph -> ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
14 13 simplld 
 |-  ( ph -> ( Q ` 0 ) = -u _pi )
15 14 eqcomd 
 |-  ( ph -> -u _pi = ( Q ` 0 ) )
16 13 simplrd 
 |-  ( ph -> ( Q ` M ) = _pi )
17 16 eqcomd 
 |-  ( ph -> _pi = ( Q ` M ) )
18 15 17 oveq12d 
 |-  ( ph -> ( -u _pi [,] _pi ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
19 18 itgeq1d 
 |-  ( ph -> S. ( -u _pi [,] _pi ) ( F ` t ) _d t = S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( F ` t ) _d t )
20 0zd 
 |-  ( ph -> 0 e. ZZ )
21 nnuz 
 |-  NN = ( ZZ>= ` 1 )
22 3 21 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
23 1e0p1 
 |-  1 = ( 0 + 1 )
24 23 a1i 
 |-  ( ph -> 1 = ( 0 + 1 ) )
25 24 fveq2d 
 |-  ( ph -> ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) ) )
26 22 25 eleqtrd 
 |-  ( ph -> M e. ( ZZ>= ` ( 0 + 1 ) ) )
27 1 3 4 fourierdlem15 
 |-  ( ph -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
28 pire 
 |-  _pi e. RR
29 28 renegcli 
 |-  -u _pi e. RR
30 iccssre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR )
31 29 28 30 mp2an 
 |-  ( -u _pi [,] _pi ) C_ RR
32 31 a1i 
 |-  ( ph -> ( -u _pi [,] _pi ) C_ RR )
33 27 32 fssd 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
34 13 simprd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
35 34 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
36 6 adantr 
 |-  ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> F : ( -u _pi [,] _pi ) --> CC )
37 simpr 
 |-  ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
38 18 eqcomd 
 |-  ( ph -> ( ( Q ` 0 ) [,] ( Q ` M ) ) = ( -u _pi [,] _pi ) )
39 38 adantr 
 |-  ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( ( Q ` 0 ) [,] ( Q ` M ) ) = ( -u _pi [,] _pi ) )
40 37 39 eleqtrd 
 |-  ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> t e. ( -u _pi [,] _pi ) )
41 36 40 ffvelcdmd 
 |-  ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( F ` t ) e. CC )
42 33 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
43 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
44 43 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
45 42 44 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
46 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
47 46 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
48 42 47 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
49 6 feqmptd 
 |-  ( ph -> F = ( t e. ( -u _pi [,] _pi ) |-> ( F ` t ) ) )
50 49 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F = ( t e. ( -u _pi [,] _pi ) |-> ( F ` t ) ) )
51 50 reseq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( t e. ( -u _pi [,] _pi ) |-> ( F ` t ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
52 ioossicc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
53 52 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
54 29 rexri 
 |-  -u _pi e. RR*
55 54 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> -u _pi e. RR* )
56 28 rexri 
 |-  _pi e. RR*
57 56 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> _pi e. RR* )
58 27 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
59 simplr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0 ..^ M ) )
60 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
61 55 57 58 59 60 fourierdlem1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> t e. ( -u _pi [,] _pi ) )
62 61 ralrimiva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) t e. ( -u _pi [,] _pi ) )
63 dfss3 
 |-  ( ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) <-> A. t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) t e. ( -u _pi [,] _pi ) )
64 62 63 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
65 53 64 sstrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
66 65 resmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( t e. ( -u _pi [,] _pi ) |-> ( F ` t ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) )
67 51 66 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) )
68 67 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
69 68 7 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
70 67 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) limCC ( Q ` ( i + 1 ) ) ) )
71 9 70 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) limCC ( Q ` ( i + 1 ) ) ) )
72 67 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) limCC ( Q ` i ) ) )
73 8 72 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) limCC ( Q ` i ) ) )
74 45 48 69 71 73 iblcncfioo 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. L^1 )
75 6 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> F : ( -u _pi [,] _pi ) --> CC )
76 75 61 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` t ) e. CC )
77 45 48 74 76 ibliooicc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. L^1 )
78 20 26 33 35 41 77 itgspltprt 
 |-  ( ph -> S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( F ` t ) _d t = sum_ i e. ( 0 ..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` t ) _d t )
79 fvres 
 |-  ( t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) = ( F ` t ) )
80 79 eqcomd 
 |-  ( t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -> ( F ` t ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) )
81 80 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` t ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) )
82 81 itgeq2dv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` t ) _d t = S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) _d t )
83 eqid 
 |-  ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) ) = ( x e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> if ( x = ( Q ` i ) , R , if ( x = ( Q ` ( i + 1 ) ) , L , ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` x ) ) ) )
84 6 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F : ( -u _pi [,] _pi ) --> CC )
85 84 64 fssresd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) --> CC )
86 53 resabs1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
87 86 7 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
88 86 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
89 45 48 35 85 limcicciooub 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
90 88 89 eqtr3d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
91 9 90 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
92 86 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
93 92 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
94 45 48 35 85 limciccioolb 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
95 93 94 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
96 8 95 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
97 5 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. RR )
98 83 45 48 35 85 87 91 96 97 fourierdlem82 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) _d t = S. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) _d t )
99 45 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( Q ` i ) e. RR )
100 48 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
101 5 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> X e. RR )
102 99 101 resubcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( Q ` i ) - X ) e. RR )
103 100 101 resubcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( Q ` ( i + 1 ) ) - X ) e. RR )
104 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) )
105 eliccre 
 |-  ( ( ( ( Q ` i ) - X ) e. RR /\ ( ( Q ` ( i + 1 ) ) - X ) e. RR /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t e. RR )
106 102 103 104 105 syl3anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t e. RR )
107 101 106 readdcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( X + t ) e. RR )
108 elicc2 
 |-  ( ( ( ( Q ` i ) - X ) e. RR /\ ( ( Q ` ( i + 1 ) ) - X ) e. RR ) -> ( t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) <-> ( t e. RR /\ ( ( Q ` i ) - X ) <_ t /\ t <_ ( ( Q ` ( i + 1 ) ) - X ) ) ) )
109 102 103 108 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) <-> ( t e. RR /\ ( ( Q ` i ) - X ) <_ t /\ t <_ ( ( Q ` ( i + 1 ) ) - X ) ) ) )
110 104 109 mpbid 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( t e. RR /\ ( ( Q ` i ) - X ) <_ t /\ t <_ ( ( Q ` ( i + 1 ) ) - X ) ) )
111 110 simp2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( Q ` i ) - X ) <_ t )
112 99 101 106 lesubadd2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( ( Q ` i ) - X ) <_ t <-> ( Q ` i ) <_ ( X + t ) ) )
113 111 112 mpbid 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( Q ` i ) <_ ( X + t ) )
114 110 simp3d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t <_ ( ( Q ` ( i + 1 ) ) - X ) )
115 101 106 100 leaddsub2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( X + t ) <_ ( Q ` ( i + 1 ) ) <-> t <_ ( ( Q ` ( i + 1 ) ) - X ) ) )
116 114 115 mpbird 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( X + t ) <_ ( Q ` ( i + 1 ) ) )
117 99 100 107 113 116 eliccd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( X + t ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
118 fvres 
 |-  ( ( X + t ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) = ( F ` ( X + t ) ) )
119 117 118 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) = ( F ` ( X + t ) ) )
120 119 itgeq2dv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) _d t = S. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ( F ` ( X + t ) ) _d t )
121 82 98 120 3eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` t ) _d t = S. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ( F ` ( X + t ) ) _d t )
122 121 sumeq2dv 
 |-  ( ph -> sum_ i e. ( 0 ..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` t ) _d t = sum_ i e. ( 0 ..^ M ) S. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ( F ` ( X + t ) ) _d t )
123 oveq2 
 |-  ( s = t -> ( X + s ) = ( X + t ) )
124 123 fveq2d 
 |-  ( s = t -> ( F ` ( X + s ) ) = ( F ` ( X + t ) ) )
125 124 cbvitgv 
 |-  S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( F ` ( X + s ) ) _d s = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( F ` ( X + t ) ) _d t
126 125 a1i 
 |-  ( ph -> S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( F ` ( X + s ) ) _d s = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( F ` ( X + t ) ) _d t )
127 2 a1i 
 |-  ( ph -> H = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) )
128 fveq2 
 |-  ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
129 128 oveq1d 
 |-  ( i = 0 -> ( ( Q ` i ) - X ) = ( ( Q ` 0 ) - X ) )
130 129 adantl 
 |-  ( ( ph /\ i = 0 ) -> ( ( Q ` i ) - X ) = ( ( Q ` 0 ) - X ) )
131 3 nnzd 
 |-  ( ph -> M e. ZZ )
132 0le0 
 |-  0 <_ 0
133 132 a1i 
 |-  ( ph -> 0 <_ 0 )
134 0red 
 |-  ( ph -> 0 e. RR )
135 3 nnred 
 |-  ( ph -> M e. RR )
136 3 nngt0d 
 |-  ( ph -> 0 < M )
137 134 135 136 ltled 
 |-  ( ph -> 0 <_ M )
138 20 131 20 133 137 elfzd 
 |-  ( ph -> 0 e. ( 0 ... M ) )
139 14 29 eqeltrdi 
 |-  ( ph -> ( Q ` 0 ) e. RR )
140 139 5 resubcld 
 |-  ( ph -> ( ( Q ` 0 ) - X ) e. RR )
141 127 130 138 140 fvmptd 
 |-  ( ph -> ( H ` 0 ) = ( ( Q ` 0 ) - X ) )
142 14 oveq1d 
 |-  ( ph -> ( ( Q ` 0 ) - X ) = ( -u _pi - X ) )
143 141 142 eqtr2d 
 |-  ( ph -> ( -u _pi - X ) = ( H ` 0 ) )
144 fveq2 
 |-  ( i = M -> ( Q ` i ) = ( Q ` M ) )
145 144 oveq1d 
 |-  ( i = M -> ( ( Q ` i ) - X ) = ( ( Q ` M ) - X ) )
146 145 adantl 
 |-  ( ( ph /\ i = M ) -> ( ( Q ` i ) - X ) = ( ( Q ` M ) - X ) )
147 135 leidd 
 |-  ( ph -> M <_ M )
148 20 131 131 137 147 elfzd 
 |-  ( ph -> M e. ( 0 ... M ) )
149 16 28 eqeltrdi 
 |-  ( ph -> ( Q ` M ) e. RR )
150 149 5 resubcld 
 |-  ( ph -> ( ( Q ` M ) - X ) e. RR )
151 127 146 148 150 fvmptd 
 |-  ( ph -> ( H ` M ) = ( ( Q ` M ) - X ) )
152 16 oveq1d 
 |-  ( ph -> ( ( Q ` M ) - X ) = ( _pi - X ) )
153 151 152 eqtr2d 
 |-  ( ph -> ( _pi - X ) = ( H ` M ) )
154 143 153 oveq12d 
 |-  ( ph -> ( ( -u _pi - X ) [,] ( _pi - X ) ) = ( ( H ` 0 ) [,] ( H ` M ) ) )
155 154 itgeq1d 
 |-  ( ph -> S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( F ` ( X + t ) ) _d t = S. ( ( H ` 0 ) [,] ( H ` M ) ) ( F ` ( X + t ) ) _d t )
156 33 ffvelcdmda 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
157 5 adantr 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> X e. RR )
158 156 157 resubcld 
 |-  ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( Q ` i ) - X ) e. RR )
159 158 2 fmptd 
 |-  ( ph -> H : ( 0 ... M ) --> RR )
160 45 48 97 35 ltsub1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) - X ) < ( ( Q ` ( i + 1 ) ) - X ) )
161 44 158 syldan 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) - X ) e. RR )
162 2 fvmpt2 
 |-  ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) - X ) e. RR ) -> ( H ` i ) = ( ( Q ` i ) - X ) )
163 44 161 162 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` i ) = ( ( Q ` i ) - X ) )
164 fveq2 
 |-  ( i = j -> ( Q ` i ) = ( Q ` j ) )
165 164 oveq1d 
 |-  ( i = j -> ( ( Q ` i ) - X ) = ( ( Q ` j ) - X ) )
166 165 cbvmptv 
 |-  ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
167 2 166 eqtri 
 |-  H = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
168 167 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> H = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) ) )
169 fveq2 
 |-  ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
170 169 oveq1d 
 |-  ( j = ( i + 1 ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
171 170 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
172 48 97 resubcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) - X ) e. RR )
173 168 171 47 172 fvmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) - X ) )
174 160 163 173 3brtr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` i ) < ( H ` ( i + 1 ) ) )
175 frn 
 |-  ( F : ( -u _pi [,] _pi ) --> CC -> ran F C_ CC )
176 6 175 syl 
 |-  ( ph -> ran F C_ CC )
177 176 adantr 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ran F C_ CC )
178 ffun 
 |-  ( F : ( -u _pi [,] _pi ) --> CC -> Fun F )
179 6 178 syl 
 |-  ( ph -> Fun F )
180 179 adantr 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> Fun F )
181 29 a1i 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u _pi e. RR )
182 28 a1i 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> _pi e. RR )
183 5 adantr 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> X e. RR )
184 141 140 eqeltrd 
 |-  ( ph -> ( H ` 0 ) e. RR )
185 184 adantr 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` 0 ) e. RR )
186 151 150 eqeltrd 
 |-  ( ph -> ( H ` M ) e. RR )
187 186 adantr 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` M ) e. RR )
188 simpr 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. ( ( H ` 0 ) [,] ( H ` M ) ) )
189 eliccre 
 |-  ( ( ( H ` 0 ) e. RR /\ ( H ` M ) e. RR /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. RR )
190 185 187 188 189 syl3anc 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. RR )
191 183 190 readdcld 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. RR )
192 128 adantl 
 |-  ( ( ph /\ i = 0 ) -> ( Q ` i ) = ( Q ` 0 ) )
193 192 oveq1d 
 |-  ( ( ph /\ i = 0 ) -> ( ( Q ` i ) - X ) = ( ( Q ` 0 ) - X ) )
194 127 193 138 140 fvmptd 
 |-  ( ph -> ( H ` 0 ) = ( ( Q ` 0 ) - X ) )
195 194 oveq2d 
 |-  ( ph -> ( X + ( H ` 0 ) ) = ( X + ( ( Q ` 0 ) - X ) ) )
196 5 recnd 
 |-  ( ph -> X e. CC )
197 139 recnd 
 |-  ( ph -> ( Q ` 0 ) e. CC )
198 196 197 pncan3d 
 |-  ( ph -> ( X + ( ( Q ` 0 ) - X ) ) = ( Q ` 0 ) )
199 195 198 14 3eqtrrd 
 |-  ( ph -> -u _pi = ( X + ( H ` 0 ) ) )
200 199 adantr 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u _pi = ( X + ( H ` 0 ) ) )
201 elicc2 
 |-  ( ( ( H ` 0 ) e. RR /\ ( H ` M ) e. RR ) -> ( t e. ( ( H ` 0 ) [,] ( H ` M ) ) <-> ( t e. RR /\ ( H ` 0 ) <_ t /\ t <_ ( H ` M ) ) ) )
202 185 187 201 syl2anc 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( t e. ( ( H ` 0 ) [,] ( H ` M ) ) <-> ( t e. RR /\ ( H ` 0 ) <_ t /\ t <_ ( H ` M ) ) ) )
203 188 202 mpbid 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( t e. RR /\ ( H ` 0 ) <_ t /\ t <_ ( H ` M ) ) )
204 203 simp2d 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` 0 ) <_ t )
205 185 190 183 204 leadd2dd 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + ( H ` 0 ) ) <_ ( X + t ) )
206 200 205 eqbrtrd 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u _pi <_ ( X + t ) )
207 203 simp3d 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t <_ ( H ` M ) )
208 190 187 183 207 leadd2dd 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) <_ ( X + ( H ` M ) ) )
209 151 oveq2d 
 |-  ( ph -> ( X + ( H ` M ) ) = ( X + ( ( Q ` M ) - X ) ) )
210 149 recnd 
 |-  ( ph -> ( Q ` M ) e. CC )
211 196 210 pncan3d 
 |-  ( ph -> ( X + ( ( Q ` M ) - X ) ) = ( Q ` M ) )
212 209 211 16 3eqtrrd 
 |-  ( ph -> _pi = ( X + ( H ` M ) ) )
213 212 adantr 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> _pi = ( X + ( H ` M ) ) )
214 208 213 breqtrrd 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) <_ _pi )
215 181 182 191 206 214 eliccd 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. ( -u _pi [,] _pi ) )
216 fdm 
 |-  ( F : ( -u _pi [,] _pi ) --> CC -> dom F = ( -u _pi [,] _pi ) )
217 6 216 syl 
 |-  ( ph -> dom F = ( -u _pi [,] _pi ) )
218 217 eqcomd 
 |-  ( ph -> ( -u _pi [,] _pi ) = dom F )
219 218 adantr 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( -u _pi [,] _pi ) = dom F )
220 215 219 eleqtrd 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. dom F )
221 fvelrn 
 |-  ( ( Fun F /\ ( X + t ) e. dom F ) -> ( F ` ( X + t ) ) e. ran F )
222 180 220 221 syl2anc 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( F ` ( X + t ) ) e. ran F )
223 177 222 sseldd 
 |-  ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( F ` ( X + t ) ) e. CC )
224 163 161 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` i ) e. RR )
225 173 172 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` ( i + 1 ) ) e. RR )
226 84 65 fssresd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
227 45 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
228 227 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
229 48 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
230 229 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
231 5 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> X e. RR )
232 elioore 
 |-  ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> t e. RR )
233 232 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t e. RR )
234 231 233 readdcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. RR )
235 163 oveq2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( H ` i ) ) = ( X + ( ( Q ` i ) - X ) ) )
236 196 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. CC )
237 45 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
238 236 237 pncan3d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( ( Q ` i ) - X ) ) = ( Q ` i ) )
239 eqidd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( Q ` i ) )
240 235 238 239 3eqtrrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( X + ( H ` i ) ) )
241 240 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) = ( X + ( H ` i ) ) )
242 224 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) e. RR )
243 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
244 242 rexrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) e. RR* )
245 225 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` ( i + 1 ) ) e. RR* )
246 245 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` ( i + 1 ) ) e. RR* )
247 elioo2 
 |-  ( ( ( H ` i ) e. RR* /\ ( H ` ( i + 1 ) ) e. RR* ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) <-> ( t e. RR /\ ( H ` i ) < t /\ t < ( H ` ( i + 1 ) ) ) ) )
248 244 246 247 syl2anc 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) <-> ( t e. RR /\ ( H ` i ) < t /\ t < ( H ` ( i + 1 ) ) ) ) )
249 243 248 mpbid 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( t e. RR /\ ( H ` i ) < t /\ t < ( H ` ( i + 1 ) ) ) )
250 249 simp2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) < t )
251 242 233 231 250 ltadd2dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + ( H ` i ) ) < ( X + t ) )
252 241 251 eqbrtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + t ) )
253 225 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` ( i + 1 ) ) e. RR )
254 249 simp3d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t < ( H ` ( i + 1 ) ) )
255 233 253 231 254 ltadd2dd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) < ( X + ( H ` ( i + 1 ) ) ) )
256 173 oveq2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( X + ( ( Q ` ( i + 1 ) ) - X ) ) )
257 48 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
258 236 257 pncan3d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( ( Q ` ( i + 1 ) ) - X ) ) = ( Q ` ( i + 1 ) ) )
259 256 258 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( Q ` ( i + 1 ) ) )
260 259 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( Q ` ( i + 1 ) ) )
261 255 260 breqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) < ( Q ` ( i + 1 ) ) )
262 228 230 234 252 261 eliood 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
263 eqid 
 |-  ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
264 262 263 fmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) : ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) --> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
265 fcompt 
 |-  ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC /\ ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) : ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) --> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) = ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) )
266 226 264 265 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) = ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) )
267 oveq2 
 |-  ( t = r -> ( X + t ) = ( X + r ) )
268 267 cbvmptv 
 |-  ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) = ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) )
269 268 fveq1i 
 |-  ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) = ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s )
270 269 fveq2i 
 |-  ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) )
271 270 mpteq2i 
 |-  ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) = ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) ) )
272 271 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) = ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) ) ) )
273 fveq2 
 |-  ( s = t -> ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) = ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) )
274 273 fveq2d 
 |-  ( s = t -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) ) )
275 274 cbvmptv 
 |-  ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) ) )
276 275 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) ) ) )
277 eqidd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) = ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) )
278 oveq2 
 |-  ( r = t -> ( X + r ) = ( X + t ) )
279 278 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) /\ r = t ) -> ( X + r ) = ( X + t ) )
280 277 279 243 234 fvmptd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) = ( X + t ) )
281 280 fveq2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) )
282 fvres 
 |-  ( ( X + t ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) = ( F ` ( X + t ) ) )
283 262 282 syl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) = ( F ` ( X + t ) ) )
284 281 283 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) ) = ( F ` ( X + t ) ) )
285 284 mpteq2dva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) )
286 272 276 285 3eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) )
287 266 286 eqtr2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) )
288 eqid 
 |-  ( t e. CC |-> ( X + t ) ) = ( t e. CC |-> ( X + t ) )
289 ssid 
 |-  CC C_ CC
290 289 a1i 
 |-  ( X e. CC -> CC C_ CC )
291 id 
 |-  ( X e. CC -> X e. CC )
292 290 291 290 constcncfg 
 |-  ( X e. CC -> ( t e. CC |-> X ) e. ( CC -cn-> CC ) )
293 cncfmptid 
 |-  ( ( CC C_ CC /\ CC C_ CC ) -> ( t e. CC |-> t ) e. ( CC -cn-> CC ) )
294 289 289 293 mp2an 
 |-  ( t e. CC |-> t ) e. ( CC -cn-> CC )
295 294 a1i 
 |-  ( X e. CC -> ( t e. CC |-> t ) e. ( CC -cn-> CC ) )
296 292 295 addcncf 
 |-  ( X e. CC -> ( t e. CC |-> ( X + t ) ) e. ( CC -cn-> CC ) )
297 236 296 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. CC |-> ( X + t ) ) e. ( CC -cn-> CC ) )
298 ioosscn 
 |-  ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) C_ CC
299 298 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) C_ CC )
300 ioosscn 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
301 300 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
302 288 297 299 301 262 cncfmptssg 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -cn-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
303 302 7 cncfco 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -cn-> CC ) )
304 287 303 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -cn-> CC ) )
305 227 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( Q ` i ) e. RR* )
306 229 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
307 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) )
308 vex 
 |-  r e. _V
309 263 elrnmpt 
 |-  ( r e. _V -> ( r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) <-> E. t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) r = ( X + t ) ) )
310 308 309 ax-mp 
 |-  ( r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) <-> E. t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) r = ( X + t ) )
311 307 310 sylib 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> E. t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) r = ( X + t ) )
312 nfv 
 |-  F/ t ( ph /\ i e. ( 0 ..^ M ) )
313 nfmpt1 
 |-  F/_ t ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
314 313 nfrn 
 |-  F/_ t ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
315 314 nfcri 
 |-  F/ t r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
316 312 315 nfan 
 |-  F/ t ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) )
317 nfv 
 |-  F/ t r e. RR
318 simp3 
 |-  ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r = ( X + t ) )
319 5 3ad2ant1 
 |-  ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> X e. RR )
320 232 3ad2ant2 
 |-  ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> t e. RR )
321 319 320 readdcld 
 |-  ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( X + t ) e. RR )
322 318 321 eqeltrd 
 |-  ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r e. RR )
323 322 3exp 
 |-  ( ph -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> r e. RR ) ) )
324 323 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> r e. RR ) ) )
325 316 317 324 rexlimd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( E. t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) r = ( X + t ) -> r e. RR ) )
326 311 325 mpd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r e. RR )
327 nfv 
 |-  F/ t ( Q ` i ) < r
328 252 3adant3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( Q ` i ) < ( X + t ) )
329 simp3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r = ( X + t ) )
330 328 329 breqtrrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( Q ` i ) < r )
331 330 3exp 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> ( Q ` i ) < r ) ) )
332 331 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> ( Q ` i ) < r ) ) )
333 316 327 332 rexlimd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( E. t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) r = ( X + t ) -> ( Q ` i ) < r ) )
334 311 333 mpd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( Q ` i ) < r )
335 nfv 
 |-  F/ t r < ( Q ` ( i + 1 ) )
336 261 3adant3 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( X + t ) < ( Q ` ( i + 1 ) ) )
337 329 336 eqbrtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r < ( Q ` ( i + 1 ) ) )
338 337 3exp 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> r < ( Q ` ( i + 1 ) ) ) ) )
339 338 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> r < ( Q ` ( i + 1 ) ) ) ) )
340 316 335 339 rexlimd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( E. t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) r = ( X + t ) -> r < ( Q ` ( i + 1 ) ) ) )
341 311 340 mpd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r < ( Q ` ( i + 1 ) ) )
342 305 306 326 334 341 eliood 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
343 217 ineq2d 
 |-  ( ph -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i dom F ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i ( -u _pi [,] _pi ) ) )
344 343 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i dom F ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i ( -u _pi [,] _pi ) ) )
345 dmres 
 |-  dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i dom F )
346 345 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i dom F ) )
347 dfss 
 |-  ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) <-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i ( -u _pi [,] _pi ) ) )
348 65 347 sylib 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i ( -u _pi [,] _pi ) ) )
349 344 346 348 3eqtr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
350 349 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
351 342 350 eleqtrrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r e. dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
352 326 341 ltned 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r =/= ( Q ` ( i + 1 ) ) )
353 352 neneqd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> -. r = ( Q ` ( i + 1 ) ) )
354 velsn 
 |-  ( r e. { ( Q ` ( i + 1 ) ) } <-> r = ( Q ` ( i + 1 ) ) )
355 353 354 sylnibr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> -. r e. { ( Q ` ( i + 1 ) ) } )
356 351 355 eldifd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r e. ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` ( i + 1 ) ) } ) )
357 356 ralrimiva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) r e. ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` ( i + 1 ) ) } ) )
358 dfss3 
 |-  ( ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) C_ ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` ( i + 1 ) ) } ) <-> A. r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) r e. ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` ( i + 1 ) ) } ) )
359 357 358 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) C_ ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` ( i + 1 ) ) } ) )
360 eqid 
 |-  ( s e. CC |-> ( X + s ) ) = ( s e. CC |-> ( X + s ) )
361 196 adantr 
 |-  ( ( ph /\ s e. CC ) -> X e. CC )
362 simpr 
 |-  ( ( ph /\ s e. CC ) -> s e. CC )
363 361 362 addcomd 
 |-  ( ( ph /\ s e. CC ) -> ( X + s ) = ( s + X ) )
364 363 mpteq2dva 
 |-  ( ph -> ( s e. CC |-> ( X + s ) ) = ( s e. CC |-> ( s + X ) ) )
365 eqid 
 |-  ( s e. CC |-> ( s + X ) ) = ( s e. CC |-> ( s + X ) )
366 365 addccncf 
 |-  ( X e. CC -> ( s e. CC |-> ( s + X ) ) e. ( CC -cn-> CC ) )
367 196 366 syl 
 |-  ( ph -> ( s e. CC |-> ( s + X ) ) e. ( CC -cn-> CC ) )
368 364 367 eqeltrd 
 |-  ( ph -> ( s e. CC |-> ( X + s ) ) e. ( CC -cn-> CC ) )
369 368 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. CC |-> ( X + s ) ) e. ( CC -cn-> CC ) )
370 224 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` i ) e. RR* )
371 iocssre 
 |-  ( ( ( H ` i ) e. RR* /\ ( H ` ( i + 1 ) ) e. RR ) -> ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) C_ RR )
372 370 225 371 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) C_ RR )
373 ax-resscn 
 |-  RR C_ CC
374 372 373 sstrdi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) C_ CC )
375 289 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> CC C_ CC )
376 196 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) -> X e. CC )
377 374 sselda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) -> s e. CC )
378 376 377 addcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) -> ( X + s ) e. CC )
379 360 369 374 375 378 cncfmptssg 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) -cn-> CC ) )
380 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
381 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) = ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) )
382 380 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
383 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
384 383 restid 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
385 382 384 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
386 385 eqcomi 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
387 380 381 386 cncfcn 
 |-  ( ( ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) C_ CC /\ CC C_ CC ) -> ( ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` CCfld ) ) )
388 374 375 387 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` CCfld ) ) )
389 379 388 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` CCfld ) ) )
390 380 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
391 390 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
392 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) e. ( TopOn ` ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) )
393 391 374 392 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) e. ( TopOn ` ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) )
394 cncnp 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) e. ( TopOn ` ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) : ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) --> CC /\ A. t e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` t ) ) ) )
395 393 391 394 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) : ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) --> CC /\ A. t e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` t ) ) ) )
396 389 395 mpbid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) : ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) --> CC /\ A. t e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` t ) ) )
397 396 simprd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. t e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` t ) )
398 ubioc1 
 |-  ( ( ( H ` i ) e. RR* /\ ( H ` ( i + 1 ) ) e. RR* /\ ( H ` i ) < ( H ` ( i + 1 ) ) ) -> ( H ` ( i + 1 ) ) e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) )
399 370 245 174 398 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` ( i + 1 ) ) e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) )
400 fveq2 
 |-  ( t = ( H ` ( i + 1 ) ) -> ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` t ) = ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` ( i + 1 ) ) ) )
401 400 eleq2d 
 |-  ( t = ( H ` ( i + 1 ) ) -> ( ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` t ) <-> ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` ( i + 1 ) ) ) ) )
402 401 rspccva 
 |-  ( ( A. t e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` t ) /\ ( H ` ( i + 1 ) ) e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) -> ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` ( i + 1 ) ) ) )
403 397 399 402 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` ( i + 1 ) ) ) )
404 ioounsn 
 |-  ( ( ( H ` i ) e. RR* /\ ( H ` ( i + 1 ) ) e. RR* /\ ( H ` i ) < ( H ` ( i + 1 ) ) ) -> ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) = ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) )
405 370 245 174 404 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) = ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) )
406 259 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) = ( X + ( H ` ( i + 1 ) ) ) )
407 406 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) /\ s = ( H ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) = ( X + ( H ` ( i + 1 ) ) ) )
408 iftrue 
 |-  ( s = ( H ` ( i + 1 ) ) -> if ( s = ( H ` ( i + 1 ) ) , ( Q ` ( i + 1 ) ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( Q ` ( i + 1 ) ) )
409 408 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) /\ s = ( H ` ( i + 1 ) ) ) -> if ( s = ( H ` ( i + 1 ) ) , ( Q ` ( i + 1 ) ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( Q ` ( i + 1 ) ) )
410 oveq2 
 |-  ( s = ( H ` ( i + 1 ) ) -> ( X + s ) = ( X + ( H ` ( i + 1 ) ) ) )
411 410 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) /\ s = ( H ` ( i + 1 ) ) ) -> ( X + s ) = ( X + ( H ` ( i + 1 ) ) ) )
412 407 409 411 3eqtr4d 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) /\ s = ( H ` ( i + 1 ) ) ) -> if ( s = ( H ` ( i + 1 ) ) , ( Q ` ( i + 1 ) ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( X + s ) )
413 iffalse 
 |-  ( -. s = ( H ` ( i + 1 ) ) -> if ( s = ( H ` ( i + 1 ) ) , ( Q ` ( i + 1 ) ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) )
414 413 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) /\ -. s = ( H ` ( i + 1 ) ) ) -> if ( s = ( H ` ( i + 1 ) ) , ( Q ` ( i + 1 ) ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) )
415 eqidd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) /\ -. s = ( H ` ( i + 1 ) ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) )
416 oveq2 
 |-  ( t = s -> ( X + t ) = ( X + s ) )
417 416 adantl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) /\ -. s = ( H ` ( i + 1 ) ) ) /\ t = s ) -> ( X + t ) = ( X + s ) )
418 velsn 
 |-  ( s e. { ( H ` ( i + 1 ) ) } <-> s = ( H ` ( i + 1 ) ) )
419 418 notbii 
 |-  ( -. s e. { ( H ` ( i + 1 ) ) } <-> -. s = ( H ` ( i + 1 ) ) )
420 elun 
 |-  ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) <-> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` ( i + 1 ) ) } ) )
421 420 biimpi 
 |-  ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) -> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` ( i + 1 ) ) } ) )
422 421 orcomd 
 |-  ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) -> ( s e. { ( H ` ( i + 1 ) ) } \/ s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) )
423 422 ord 
 |-  ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) -> ( -. s e. { ( H ` ( i + 1 ) ) } -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) )
424 419 423 biimtrrid 
 |-  ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) -> ( -. s = ( H ` ( i + 1 ) ) -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) )
425 424 imp 
 |-  ( ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) /\ -. s = ( H ` ( i + 1 ) ) ) -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
426 425 adantll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) /\ -. s = ( H ` ( i + 1 ) ) ) -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
427 5 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) -> X e. RR )
428 elioore 
 |-  ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> s e. RR )
429 428 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> s e. RR )
430 elsni 
 |-  ( s e. { ( H ` ( i + 1 ) ) } -> s = ( H ` ( i + 1 ) ) )
431 430 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( H ` ( i + 1 ) ) } ) -> s = ( H ` ( i + 1 ) ) )
432 225 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( H ` ( i + 1 ) ) } ) -> ( H ` ( i + 1 ) ) e. RR )
433 431 432 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( H ` ( i + 1 ) ) } ) -> s e. RR )
434 429 433 jaodan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` ( i + 1 ) ) } ) ) -> s e. RR )
435 420 434 sylan2b 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) -> s e. RR )
436 427 435 readdcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) -> ( X + s ) e. RR )
437 436 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) /\ -. s = ( H ` ( i + 1 ) ) ) -> ( X + s ) e. RR )
438 415 417 426 437 fvmptd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) /\ -. s = ( H ` ( i + 1 ) ) ) -> ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) = ( X + s ) )
439 414 438 eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) /\ -. s = ( H ` ( i + 1 ) ) ) -> if ( s = ( H ` ( i + 1 ) ) , ( Q ` ( i + 1 ) ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( X + s ) )
440 412 439 pm2.61dan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) -> if ( s = ( H ` ( i + 1 ) ) , ( Q ` ( i + 1 ) ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( X + s ) )
441 405 440 mpteq12dva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) |-> if ( s = ( H ` ( i + 1 ) ) , ( Q ` ( i + 1 ) ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) = ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) )
442 405 oveq2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) )
443 442 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) = ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) )
444 443 fveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` ( i + 1 ) ) ) = ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` ( i + 1 ) ) ) )
445 403 441 444 3eltr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) |-> if ( s = ( H ` ( i + 1 ) ) , ( Q ` ( i + 1 ) ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` ( i + 1 ) ) ) )
446 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) )
447 eqid 
 |-  ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) |-> if ( s = ( H ` ( i + 1 ) ) , ( Q ` ( i + 1 ) ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) = ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) |-> if ( s = ( H ` ( i + 1 ) ) , ( Q ` ( i + 1 ) ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) )
448 264 301 fssd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) : ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) --> CC )
449 225 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` ( i + 1 ) ) e. CC )
450 446 380 447 448 299 449 ellimc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) limCC ( H ` ( i + 1 ) ) ) <-> ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) |-> if ( s = ( H ` ( i + 1 ) ) , ( Q ` ( i + 1 ) ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` ( i + 1 ) ) ) ) )
451 445 450 mpbird 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) limCC ( H ` ( i + 1 ) ) ) )
452 359 451 9 limccog 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) limCC ( H ` ( i + 1 ) ) ) )
453 266 286 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) )
454 453 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) limCC ( H ` ( i + 1 ) ) ) = ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) limCC ( H ` ( i + 1 ) ) ) )
455 452 454 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) limCC ( H ` ( i + 1 ) ) ) )
456 45 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( Q ` i ) e. RR )
457 456 334 gtned 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r =/= ( Q ` i ) )
458 457 neneqd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> -. r = ( Q ` i ) )
459 velsn 
 |-  ( r e. { ( Q ` i ) } <-> r = ( Q ` i ) )
460 458 459 sylnibr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> -. r e. { ( Q ` i ) } )
461 351 460 eldifd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r e. ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` i ) } ) )
462 461 ralrimiva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) r e. ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` i ) } ) )
463 dfss3 
 |-  ( ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) C_ ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` i ) } ) <-> A. r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) r e. ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` i ) } ) )
464 462 463 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) C_ ( dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) \ { ( Q ` i ) } ) )
465 icossre 
 |-  ( ( ( H ` i ) e. RR /\ ( H ` ( i + 1 ) ) e. RR* ) -> ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) C_ RR )
466 224 245 465 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) C_ RR )
467 466 373 sstrdi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) C_ CC )
468 196 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) -> X e. CC )
469 467 sselda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) -> s e. CC )
470 468 469 addcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) -> ( X + s ) e. CC )
471 360 369 467 375 470 cncfmptssg 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) -cn-> CC ) )
472 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) = ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
473 380 472 386 cncfcn 
 |-  ( ( ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) C_ CC /\ CC C_ CC ) -> ( ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` CCfld ) ) )
474 467 375 473 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` CCfld ) ) )
475 471 474 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` CCfld ) ) )
476 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) e. ( TopOn ` ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) )
477 391 467 476 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) e. ( TopOn ` ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) )
478 cncnp 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) e. ( TopOn ` ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) : ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) --> CC /\ A. t e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` t ) ) ) )
479 477 391 478 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) : ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) --> CC /\ A. t e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` t ) ) ) )
480 475 479 mpbid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) : ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) --> CC /\ A. t e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` t ) ) )
481 480 simprd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. t e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` t ) )
482 lbico1 
 |-  ( ( ( H ` i ) e. RR* /\ ( H ` ( i + 1 ) ) e. RR* /\ ( H ` i ) < ( H ` ( i + 1 ) ) ) -> ( H ` i ) e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
483 370 245 174 482 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` i ) e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
484 fveq2 
 |-  ( t = ( H ` i ) -> ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` t ) = ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` i ) ) )
485 484 eleq2d 
 |-  ( t = ( H ` i ) -> ( ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` t ) <-> ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` i ) ) ) )
486 485 rspccva 
 |-  ( ( A. t e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` t ) /\ ( H ` i ) e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) -> ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` i ) ) )
487 481 483 486 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` i ) ) )
488 uncom 
 |-  ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) = ( { ( H ` i ) } u. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
489 snunioo 
 |-  ( ( ( H ` i ) e. RR* /\ ( H ` ( i + 1 ) ) e. RR* /\ ( H ` i ) < ( H ` ( i + 1 ) ) ) -> ( { ( H ` i ) } u. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) = ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
490 370 245 174 489 syl3anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( { ( H ` i ) } u. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) = ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
491 488 490 eqtrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) = ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
492 iftrue 
 |-  ( s = ( H ` i ) -> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( Q ` i ) )
493 492 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s = ( H ` i ) ) -> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( Q ` i ) )
494 240 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s = ( H ` i ) ) -> ( Q ` i ) = ( X + ( H ` i ) ) )
495 oveq2 
 |-  ( s = ( H ` i ) -> ( X + s ) = ( X + ( H ` i ) ) )
496 495 eqcomd 
 |-  ( s = ( H ` i ) -> ( X + ( H ` i ) ) = ( X + s ) )
497 496 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s = ( H ` i ) ) -> ( X + ( H ` i ) ) = ( X + s ) )
498 493 494 497 3eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s = ( H ` i ) ) -> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( X + s ) )
499 498 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) /\ s = ( H ` i ) ) -> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( X + s ) )
500 iffalse 
 |-  ( -. s = ( H ` i ) -> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) )
501 500 adantl 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) /\ -. s = ( H ` i ) ) -> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) )
502 eqidd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) /\ -. s = ( H ` i ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) )
503 416 adantl 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) /\ -. s = ( H ` i ) ) /\ t = s ) -> ( X + t ) = ( X + s ) )
504 velsn 
 |-  ( s e. { ( H ` i ) } <-> s = ( H ` i ) )
505 504 notbii 
 |-  ( -. s e. { ( H ` i ) } <-> -. s = ( H ` i ) )
506 elun 
 |-  ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) <-> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` i ) } ) )
507 506 biimpi 
 |-  ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) -> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` i ) } ) )
508 507 orcomd 
 |-  ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) -> ( s e. { ( H ` i ) } \/ s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) )
509 508 ord 
 |-  ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) -> ( -. s e. { ( H ` i ) } -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) )
510 505 509 biimtrrid 
 |-  ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) -> ( -. s = ( H ` i ) -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) )
511 510 imp 
 |-  ( ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) /\ -. s = ( H ` i ) ) -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
512 511 adantll 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) /\ -. s = ( H ` i ) ) -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
513 5 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) -> X e. RR )
514 elsni 
 |-  ( s e. { ( H ` i ) } -> s = ( H ` i ) )
515 514 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( H ` i ) } ) -> s = ( H ` i ) )
516 224 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( H ` i ) } ) -> ( H ` i ) e. RR )
517 515 516 eqeltrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( H ` i ) } ) -> s e. RR )
518 429 517 jaodan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` i ) } ) ) -> s e. RR )
519 506 518 sylan2b 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) -> s e. RR )
520 513 519 readdcld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) -> ( X + s ) e. RR )
521 520 adantr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) /\ -. s = ( H ` i ) ) -> ( X + s ) e. RR )
522 502 503 512 521 fvmptd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) /\ -. s = ( H ` i ) ) -> ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) = ( X + s ) )
523 501 522 eqtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) /\ -. s = ( H ` i ) ) -> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( X + s ) )
524 499 523 pm2.61dan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) -> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( X + s ) )
525 491 524 mpteq12dva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) |-> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) = ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) )
526 491 oveq2d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) )
527 526 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) = ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) )
528 527 fveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` i ) ) = ( ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` i ) ) )
529 487 525 528 3eltr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) |-> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` i ) ) )
530 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) )
531 eqid 
 |-  ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) |-> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) = ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) |-> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) )
532 224 recnd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` i ) e. CC )
533 530 380 531 448 299 532 ellimc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) limCC ( H ` i ) ) <-> ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) |-> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) CnP ( TopOpen ` CCfld ) ) ` ( H ` i ) ) ) )
534 529 533 mpbird 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) limCC ( H ` i ) ) )
535 464 534 8 limccog 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) limCC ( H ` i ) ) )
536 453 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) limCC ( H ` i ) ) = ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) limCC ( H ` i ) ) )
537 535 536 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) limCC ( H ` i ) ) )
538 224 225 304 455 537 iblcncfioo 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) e. L^1 )
539 6 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> F : ( -u _pi [,] _pi ) --> CC )
540 54 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> -u _pi e. RR* )
541 56 a1i 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> _pi e. RR* )
542 27 ad2antrr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
543 simplr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> i e. ( 0 ..^ M ) )
544 simpr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) )
545 163 173 oveq12d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) = ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) )
546 545 adantr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) = ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) )
547 544 546 eleqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) )
548 547 117 syldan 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
549 540 541 542 543 548 fourierdlem1 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. ( -u _pi [,] _pi ) )
550 539 549 ffvelcdmd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> ( F ` ( X + t ) ) e. CC )
551 224 225 538 550 ibliooicc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) e. L^1 )
552 20 26 159 174 223 551 itgspltprt 
 |-  ( ph -> S. ( ( H ` 0 ) [,] ( H ` M ) ) ( F ` ( X + t ) ) _d t = sum_ i e. ( 0 ..^ M ) S. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ( F ` ( X + t ) ) _d t )
553 545 itgeq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> S. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ( F ` ( X + t ) ) _d t = S. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ( F ` ( X + t ) ) _d t )
554 553 sumeq2dv 
 |-  ( ph -> sum_ i e. ( 0 ..^ M ) S. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ( F ` ( X + t ) ) _d t = sum_ i e. ( 0 ..^ M ) S. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ( F ` ( X + t ) ) _d t )
555 552 554 eqtrd 
 |-  ( ph -> S. ( ( H ` 0 ) [,] ( H ` M ) ) ( F ` ( X + t ) ) _d t = sum_ i e. ( 0 ..^ M ) S. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ( F ` ( X + t ) ) _d t )
556 126 155 555 3eqtrd 
 |-  ( ph -> S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( F ` ( X + s ) ) _d s = sum_ i e. ( 0 ..^ M ) S. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ( F ` ( X + t ) ) _d t )
557 122 556 eqtr4d 
 |-  ( ph -> sum_ i e. ( 0 ..^ M ) S. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ( F ` t ) _d t = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( F ` ( X + s ) ) _d s )
558 19 78 557 3eqtrd 
 |-  ( ph -> S. ( -u _pi [,] _pi ) ( F ` t ) _d t = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( F ` ( X + s ) ) _d s )