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	ffvelrnd	|- ( ( 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	ffvelrnd	|- ( ( 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	ffvelrnd	|- ( ( 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	ffvelrnd	|- ( ( ( 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	20 131 20	3jca	|- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) )
133		0le0	|- 0 <_ 0
134	133	a1i	|- ( ph -> 0 <_ 0 )
135		0red	|- ( ph -> 0 e. RR )
136	3	nnred	|- ( ph -> M e. RR )
137	3	nngt0d	|- ( ph -> 0 < M )
138	135 136 137	ltled	|- ( ph -> 0 <_ M )
139	134 138	jca	|- ( ph -> ( 0 <_ 0 /\ 0 <_ M ) )
140		elfz2	|- ( 0 e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) /\ ( 0 <_ 0 /\ 0 <_ M ) ) )
141	132 139 140	sylanbrc	|- ( ph -> 0 e. ( 0 ... M ) )
142	14 29	eqeltrdi	|- ( ph -> ( Q ` 0 ) e. RR )
143	142 5	resubcld	|- ( ph -> ( ( Q ` 0 ) - X ) e. RR )
144	127 130 141 143	fvmptd	|- ( ph -> ( H ` 0 ) = ( ( Q ` 0 ) - X ) )
145	14	oveq1d	|- ( ph -> ( ( Q ` 0 ) - X ) = ( -u _pi - X ) )
146	144 145	eqtr2d	|- ( ph -> ( -u _pi - X ) = ( H ` 0 ) )
147		fveq2	|- ( i = M -> ( Q ` i ) = ( Q ` M ) )
148	147	oveq1d	|- ( i = M -> ( ( Q ` i ) - X ) = ( ( Q ` M ) - X ) )
149	148	adantl	|- ( ( ph /\ i = M ) -> ( ( Q ` i ) - X ) = ( ( Q ` M ) - X ) )
150	20 131 131	3jca	|- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ M e. ZZ ) )
151	136	leidd	|- ( ph -> M <_ M )
152	138 151	jca	|- ( ph -> ( 0 <_ M /\ M <_ M ) )
153		elfz2	|- ( M e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ M e. ZZ ) /\ ( 0 <_ M /\ M <_ M ) ) )
154	150 152 153	sylanbrc	|- ( ph -> M e. ( 0 ... M ) )
155	16 28	eqeltrdi	|- ( ph -> ( Q ` M ) e. RR )
156	155 5	resubcld	|- ( ph -> ( ( Q ` M ) - X ) e. RR )
157	127 149 154 156	fvmptd	|- ( ph -> ( H ` M ) = ( ( Q ` M ) - X ) )
158	16	oveq1d	|- ( ph -> ( ( Q ` M ) - X ) = ( _pi - X ) )
159	157 158	eqtr2d	|- ( ph -> ( _pi - X ) = ( H ` M ) )
160	146 159	oveq12d	|- ( ph -> ( ( -u _pi - X ) [,] ( _pi - X ) ) = ( ( H ` 0 ) [,] ( H ` M ) ) )
161	160	itgeq1d	|- ( ph -> S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( F ` ( X + t ) ) _d t = S. ( ( H ` 0 ) [,] ( H ` M ) ) ( F ` ( X + t ) ) _d t )
162	33	ffvelrnda	|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
163	5	adantr	|- ( ( ph /\ i e. ( 0 ... M ) ) -> X e. RR )
164	162 163	resubcld	|- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( Q ` i ) - X ) e. RR )
165	164 2	fmptd	|- ( ph -> H : ( 0 ... M ) --> RR )
166	45 48 97 35	ltsub1dd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) - X ) < ( ( Q ` ( i + 1 ) ) - X ) )
167	44 164	syldan	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) - X ) e. RR )
168	2	fvmpt2	|- ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) - X ) e. RR ) -> ( H ` i ) = ( ( Q ` i ) - X ) )
169	44 167 168	syl2anc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` i ) = ( ( Q ` i ) - X ) )
170		fveq2	|- ( i = j -> ( Q ` i ) = ( Q ` j ) )
171	170	oveq1d	|- ( i = j -> ( ( Q ` i ) - X ) = ( ( Q ` j ) - X ) )
172	171	cbvmptv	|- ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
173	2 172	eqtri	|- H = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
174	173	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> H = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) ) )
175		fveq2	|- ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
176	175	oveq1d	|- ( j = ( i + 1 ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
177	176	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
178	48 97	resubcld	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` ( i + 1 ) ) - X ) e. RR )
179	174 177 47 178	fvmptd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) - X ) )
180	166 169 179	3brtr4d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` i ) < ( H ` ( i + 1 ) ) )
181		frn	|- ( F : ( -u _pi [,] _pi ) --> CC -> ran F C_ CC )
182	6 181	syl	|- ( ph -> ran F C_ CC )
183	182	adantr	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ran F C_ CC )
184		ffun	|- ( F : ( -u _pi [,] _pi ) --> CC -> Fun F )
185	6 184	syl	|- ( ph -> Fun F )
186	185	adantr	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> Fun F )
187	29	a1i	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u _pi e. RR )
188	28	a1i	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> _pi e. RR )
189	5	adantr	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> X e. RR )
190	144 143	eqeltrd	|- ( ph -> ( H ` 0 ) e. RR )
191	190	adantr	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` 0 ) e. RR )
192	157 156	eqeltrd	|- ( ph -> ( H ` M ) e. RR )
193	192	adantr	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` M ) e. RR )
194		simpr	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. ( ( H ` 0 ) [,] ( H ` M ) ) )
195		eliccre	|- ( ( ( H ` 0 ) e. RR /\ ( H ` M ) e. RR /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. RR )
196	191 193 194 195	syl3anc	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. RR )
197	189 196	readdcld	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. RR )
198	128	adantl	|- ( ( ph /\ i = 0 ) -> ( Q ` i ) = ( Q ` 0 ) )
199	198	oveq1d	|- ( ( ph /\ i = 0 ) -> ( ( Q ` i ) - X ) = ( ( Q ` 0 ) - X ) )
200	127 199 141 143	fvmptd	|- ( ph -> ( H ` 0 ) = ( ( Q ` 0 ) - X ) )
201	200	oveq2d	|- ( ph -> ( X + ( H ` 0 ) ) = ( X + ( ( Q ` 0 ) - X ) ) )
202	5	recnd	|- ( ph -> X e. CC )
203	142	recnd	|- ( ph -> ( Q ` 0 ) e. CC )
204	202 203	pncan3d	|- ( ph -> ( X + ( ( Q ` 0 ) - X ) ) = ( Q ` 0 ) )
205	201 204 14	3eqtrrd	|- ( ph -> -u _pi = ( X + ( H ` 0 ) ) )
206	205	adantr	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u _pi = ( X + ( H ` 0 ) ) )
207		elicc2	|- ( ( ( H ` 0 ) e. RR /\ ( H ` M ) e. RR ) -> ( t e. ( ( H ` 0 ) [,] ( H ` M ) ) <-> ( t e. RR /\ ( H ` 0 ) <_ t /\ t <_ ( H ` M ) ) ) )
208	191 193 207	syl2anc	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( t e. ( ( H ` 0 ) [,] ( H ` M ) ) <-> ( t e. RR /\ ( H ` 0 ) <_ t /\ t <_ ( H ` M ) ) ) )
209	194 208	mpbid	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( t e. RR /\ ( H ` 0 ) <_ t /\ t <_ ( H ` M ) ) )
210	209	simp2d	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` 0 ) <_ t )
211	191 196 189 210	leadd2dd	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + ( H ` 0 ) ) <_ ( X + t ) )
212	206 211	eqbrtrd	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u _pi <_ ( X + t ) )
213	209	simp3d	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t <_ ( H ` M ) )
214	196 193 189 213	leadd2dd	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) <_ ( X + ( H ` M ) ) )
215	157	oveq2d	|- ( ph -> ( X + ( H ` M ) ) = ( X + ( ( Q ` M ) - X ) ) )
216	155	recnd	|- ( ph -> ( Q ` M ) e. CC )
217	202 216	pncan3d	|- ( ph -> ( X + ( ( Q ` M ) - X ) ) = ( Q ` M ) )
218	215 217 16	3eqtrrd	|- ( ph -> _pi = ( X + ( H ` M ) ) )
219	218	adantr	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> _pi = ( X + ( H ` M ) ) )
220	214 219	breqtrrd	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) <_ _pi )
221	187 188 197 212 220	eliccd	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. ( -u _pi [,] _pi ) )
222		fdm	|- ( F : ( -u _pi [,] _pi ) --> CC -> dom F = ( -u _pi [,] _pi ) )
223	6 222	syl	|- ( ph -> dom F = ( -u _pi [,] _pi ) )
224	223	eqcomd	|- ( ph -> ( -u _pi [,] _pi ) = dom F )
225	224	adantr	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( -u _pi [,] _pi ) = dom F )
226	221 225	eleqtrd	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. dom F )
227		fvelrn	|- ( ( Fun F /\ ( X + t ) e. dom F ) -> ( F ` ( X + t ) ) e. ran F )
228	186 226 227	syl2anc	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( F ` ( X + t ) ) e. ran F )
229	183 228	sseldd	|- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( F ` ( X + t ) ) e. CC )
230	169 167	eqeltrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` i ) e. RR )
231	179 178	eqeltrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` ( i + 1 ) ) e. RR )
232	84 65	fssresd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
233	45	rexrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
234	233	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
235	48	rexrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
236	235	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
237	5	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> X e. RR )
238		elioore	|- ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> t e. RR )
239	238	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t e. RR )
240	237 239	readdcld	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. RR )
241	169	oveq2d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( H ` i ) ) = ( X + ( ( Q ` i ) - X ) ) )
242	202	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. CC )
243	45	recnd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. CC )
244	242 243	pncan3d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( ( Q ` i ) - X ) ) = ( Q ` i ) )
245		eqidd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( Q ` i ) )
246	241 244 245	3eqtrrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( X + ( H ` i ) ) )
247	246	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) = ( X + ( H ` i ) ) )
248	230	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) e. RR )
249		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
250	248	rexrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) e. RR* )
251	231	rexrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` ( i + 1 ) ) e. RR* )
252	251	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` ( i + 1 ) ) e. RR* )
253		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 ) ) ) ) )
254	250 252 253	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 ) ) ) ) )
255	249 254	mpbid	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( t e. RR /\ ( H ` i ) < t /\ t < ( H ` ( i + 1 ) ) ) )
256	255	simp2d	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) < t )
257	248 239 237 256	ltadd2dd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + ( H ` i ) ) < ( X + t ) )
258	247 257	eqbrtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + t ) )
259	231	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` ( i + 1 ) ) e. RR )
260	255	simp3d	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t < ( H ` ( i + 1 ) ) )
261	239 259 237 260	ltadd2dd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) < ( X + ( H ` ( i + 1 ) ) ) )
262	179	oveq2d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( X + ( ( Q ` ( i + 1 ) ) - X ) ) )
263	48	recnd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
264	242 263	pncan3d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( ( Q ` ( i + 1 ) ) - X ) ) = ( Q ` ( i + 1 ) ) )
265	262 264	eqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( Q ` ( i + 1 ) ) )
266	265	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( Q ` ( i + 1 ) ) )
267	261 266	breqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) < ( Q ` ( i + 1 ) ) )
268	234 236 240 258 267	eliood	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
269		eqid	|- ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
270	268 269	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 ) ) ) )
271		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 ) ) ) )
272	232 270 271	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 ) ) ) )
273		oveq2	|- ( t = r -> ( X + t ) = ( X + r ) )
274	273	cbvmptv	|- ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) = ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) )
275	274	fveq1i	|- ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) = ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s )
276	275	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 ) )
277	276	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 ) ) )
278	277	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 ) ) ) )
279		fveq2	|- ( s = t -> ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s ) = ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` t ) )
280	279	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 ) ) )
281	280	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 ) ) )
282	281	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 ) ) ) )
283		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 ) ) )
284		oveq2	|- ( r = t -> ( X + r ) = ( X + t ) )
285	284	adantl	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) /\ r = t ) -> ( X + r ) = ( X + t ) )
286	283 285 249 240	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 ) )
287	286	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 ) ) )
288		fvres	|- ( ( X + t ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) = ( F ` ( X + t ) ) )
289	268 288	syl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) = ( F ` ( X + t ) ) )
290	287 289	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 ) ) )
291	290	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 ) ) ) )
292	278 282 291	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 ) ) ) )
293	272 292	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 ) ) ) )
294		eqid	|- ( t e. CC |-> ( X + t ) ) = ( t e. CC |-> ( X + t ) )
295		ssid	|- CC C_ CC
296	295	a1i	|- ( X e. CC -> CC C_ CC )
297		id	|- ( X e. CC -> X e. CC )
298	296 297 296	constcncfg	|- ( X e. CC -> ( t e. CC |-> X ) e. ( CC -cn-> CC ) )
299		cncfmptid	|- ( ( CC C_ CC /\ CC C_ CC ) -> ( t e. CC |-> t ) e. ( CC -cn-> CC ) )
300	295 295 299	mp2an	|- ( t e. CC |-> t ) e. ( CC -cn-> CC )
301	300	a1i	|- ( X e. CC -> ( t e. CC |-> t ) e. ( CC -cn-> CC ) )
302	298 301	addcncf	|- ( X e. CC -> ( t e. CC |-> ( X + t ) ) e. ( CC -cn-> CC ) )
303	242 302	syl	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. CC |-> ( X + t ) ) e. ( CC -cn-> CC ) )
304		ioosscn	|- ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) C_ CC
305	304	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) C_ CC )
306		ioosscn	|- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
307	306	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
308	294 303 305 307 268	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 ) ) ) ) )
309	308 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 ) )
310	293 309	eqeltrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -cn-> CC ) )
311	233	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( Q ` i ) e. RR* )
312	235	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
313		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 ) ) )
314		vex	|- r e. _V
315	269	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 ) ) )
316	314 315	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 ) )
317	313 316	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 ) )
318		nfv	|- F/ t ( ph /\ i e. ( 0 ..^ M ) )
319		nfmpt1	|- F/_ t ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
320	319	nfrn	|- F/_ t ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
321	320	nfcri	|- F/ t r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
322	318 321	nfan	|- F/ t ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) )
323		nfv	|- F/ t r e. RR
324		simp3	|- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r = ( X + t ) )
325	5	3ad2ant1	|- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> X e. RR )
326	238	3ad2ant2	|- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> t e. RR )
327	325 326	readdcld	|- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( X + t ) e. RR )
328	324 327	eqeltrd	|- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r e. RR )
329	328	3exp	|- ( ph -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> r e. RR ) ) )
330	329	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 ) ) )
331	322 323 330	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 ) )
332	317 331	mpd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r e. RR )
333		nfv	|- F/ t ( Q ` i ) < r
334	258	3adant3	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( Q ` i ) < ( X + t ) )
335		simp3	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r = ( X + t ) )
336	334 335	breqtrrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( Q ` i ) < r )
337	336	3exp	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> ( Q ` i ) < r ) ) )
338	337	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 ) ) )
339	322 333 338	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 ) )
340	317 339	mpd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( Q ` i ) < r )
341		nfv	|- F/ t r < ( Q ` ( i + 1 ) )
342	267	3adant3	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( X + t ) < ( Q ` ( i + 1 ) ) )
343	335 342	eqbrtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r < ( Q ` ( i + 1 ) ) )
344	343	3exp	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> r < ( Q ` ( i + 1 ) ) ) ) )
345	344	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 ) ) ) ) )
346	322 341 345	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 ) ) ) )
347	317 346	mpd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r < ( Q ` ( i + 1 ) ) )
348	311 312 332 340 347	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 ) ) ) )
349	223	ineq2d	|- ( ph -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i dom F ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i ( -u _pi [,] _pi ) ) )
350	349	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 ) ) )
351		dmres	|- dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i dom F )
352	351	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i dom F ) )
353		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 ) ) )
354	65 353	sylib	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i ( -u _pi [,] _pi ) ) )
355	350 352 354	3eqtr4d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
356	355	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 ) ) ) )
357	348 356	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 ) ) ) ) )
358	332 347	ltned	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r =/= ( Q ` ( i + 1 ) ) )
359	358	neneqd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> -. r = ( Q ` ( i + 1 ) ) )
360		velsn	|- ( r e. { ( Q ` ( i + 1 ) ) } <-> r = ( Q ` ( i + 1 ) ) )
361	359 360	sylnibr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> -. r e. { ( Q ` ( i + 1 ) ) } )
362	357 361	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 ) ) } ) )
363	362	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 ) ) } ) )
364		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 ) ) } ) )
365	363 364	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 ) ) } ) )
366		eqid	|- ( s e. CC |-> ( X + s ) ) = ( s e. CC |-> ( X + s ) )
367	202	adantr	|- ( ( ph /\ s e. CC ) -> X e. CC )
368		simpr	|- ( ( ph /\ s e. CC ) -> s e. CC )
369	367 368	addcomd	|- ( ( ph /\ s e. CC ) -> ( X + s ) = ( s + X ) )
370	369	mpteq2dva	|- ( ph -> ( s e. CC |-> ( X + s ) ) = ( s e. CC |-> ( s + X ) ) )
371		eqid	|- ( s e. CC |-> ( s + X ) ) = ( s e. CC |-> ( s + X ) )
372	371	addccncf	|- ( X e. CC -> ( s e. CC |-> ( s + X ) ) e. ( CC -cn-> CC ) )
373	202 372	syl	|- ( ph -> ( s e. CC |-> ( s + X ) ) e. ( CC -cn-> CC ) )
374	370 373	eqeltrd	|- ( ph -> ( s e. CC |-> ( X + s ) ) e. ( CC -cn-> CC ) )
375	374	adantr	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. CC |-> ( X + s ) ) e. ( CC -cn-> CC ) )
376	230	rexrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` i ) e. RR* )
377		iocssre	|- ( ( ( H ` i ) e. RR* /\ ( H ` ( i + 1 ) ) e. RR ) -> ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) C_ RR )
378	376 231 377	syl2anc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) C_ RR )
379		ax-resscn	|- RR C_ CC
380	378 379	sstrdi	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) C_ CC )
381	295	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> CC C_ CC )
382	202	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) -> X e. CC )
383	380	sselda	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) -> s e. CC )
384	382 383	addcld	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) -> ( X + s ) e. CC )
385	366 375 380 381 384	cncfmptssg	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) -cn-> CC ) )
386		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
387		eqid	|- ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) = ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) )
388	386	cnfldtop	|- ( TopOpen ` CCfld ) e. Top
389		unicntop	|- CC = U. ( TopOpen ` CCfld )
390	389	restid	|- ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
391	388 390	ax-mp	|- ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
392	391	eqcomi	|- ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
393	386 387 392	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 ) ) )
394	380 381 393	syl2anc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` CCfld ) ) )
395	385 394	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 ) ) )
396	386	cnfldtopon	|- ( TopOpen ` CCfld ) e. ( TopOn ` CC )
397	396	a1i	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
398		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 ) ) ) ) )
399	397 380 398	syl2anc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) e. ( TopOn ` ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) )
400		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 ) ) ) )
401	399 397 400	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 ) ) ) )
402	395 401	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 ) ) )
403	402	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 ) )
404		ubioc1	|- ( ( ( H ` i ) e. RR* /\ ( H ` ( i + 1 ) ) e. RR* /\ ( H ` i ) < ( H ` ( i + 1 ) ) ) -> ( H ` ( i + 1 ) ) e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) )
405	376 251 180 404	syl3anc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` ( i + 1 ) ) e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) )
406		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 ) ) ) )
407	406	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 ) ) ) ) )
408	407	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 ) ) ) )
409	403 405 408	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 ) ) ) )
410		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 ) ) ) )
411	376 251 180 410	syl3anc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) = ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) )
412	265	eqcomd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) = ( X + ( H ` ( i + 1 ) ) ) )
413	412	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 ) ) ) )
414		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 ) ) )
415	414	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 ) ) )
416		oveq2	|- ( s = ( H ` ( i + 1 ) ) -> ( X + s ) = ( X + ( H ` ( i + 1 ) ) ) )
417	416	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 ) ) ) )
418	413 415 417	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 ) )
419		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 ) )
420	419	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 ) )
421		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 ) ) )
422		oveq2	|- ( t = s -> ( X + t ) = ( X + s ) )
423	422	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 ) )
424		velsn	|- ( s e. { ( H ` ( i + 1 ) ) } <-> s = ( H ` ( i + 1 ) ) )
425	424	notbii	|- ( -. s e. { ( H ` ( i + 1 ) ) } <-> -. s = ( H ` ( i + 1 ) ) )
426		elun	|- ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) <-> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` ( i + 1 ) ) } ) )
427	426	biimpi	|- ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) -> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` ( i + 1 ) ) } ) )
428	427	orcomd	|- ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) -> ( s e. { ( H ` ( i + 1 ) ) } \/ s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) )
429	428	ord	|- ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) -> ( -. s e. { ( H ` ( i + 1 ) ) } -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) )
430	425 429	syl5bir	|- ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) -> ( -. s = ( H ` ( i + 1 ) ) -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) )
431	430	imp	|- ( ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) /\ -. s = ( H ` ( i + 1 ) ) ) -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
432	431	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 ) ) ) )
433	5	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) -> X e. RR )
434		elioore	|- ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> s e. RR )
435	434	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> s e. RR )
436		elsni	|- ( s e. { ( H ` ( i + 1 ) ) } -> s = ( H ` ( i + 1 ) ) )
437	436	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( H ` ( i + 1 ) ) } ) -> s = ( H ` ( i + 1 ) ) )
438	231	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( H ` ( i + 1 ) ) } ) -> ( H ` ( i + 1 ) ) e. RR )
439	437 438	eqeltrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( H ` ( i + 1 ) ) } ) -> s e. RR )
440	435 439	jaodan	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` ( i + 1 ) ) } ) ) -> s e. RR )
441	426 440	sylan2b	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) -> s e. RR )
442	433 441	readdcld	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) -> ( X + s ) e. RR )
443	442	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 )
444	421 423 432 443	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 ) )
445	420 444	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 ) )
446	418 445	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 ) )
447	411 446	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 ) ) )
448	411	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 ) ) ) ) )
449	448	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 ) ) )
450	449	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 ) ) ) )
451	409 447 450	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 ) ) ) )
452		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 ) ) } ) )
453		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 ) ) )
454	270 307	fssd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) : ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) --> CC )
455	231	recnd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` ( i + 1 ) ) e. CC )
456	452 386 453 454 305 455	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 ) ) ) ) )
457	451 456	mpbird	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) limCC ( H ` ( i + 1 ) ) ) )
458	365 457 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 ) ) ) )
459	272 292	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 ) ) ) )
460	459	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 ) ) ) )
461	458 460	eleqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) limCC ( H ` ( i + 1 ) ) ) )
462	45	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( Q ` i ) e. RR )
463	462 340	gtned	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r =/= ( Q ` i ) )
464	463	neneqd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> -. r = ( Q ` i ) )
465		velsn	|- ( r e. { ( Q ` i ) } <-> r = ( Q ` i ) )
466	464 465	sylnibr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> -. r e. { ( Q ` i ) } )
467	357 466	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 ) } ) )
468	467	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 ) } ) )
469		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 ) } ) )
470	468 469	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 ) } ) )
471		icossre	|- ( ( ( H ` i ) e. RR /\ ( H ` ( i + 1 ) ) e. RR* ) -> ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) C_ RR )
472	230 251 471	syl2anc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) C_ RR )
473	472 379	sstrdi	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) C_ CC )
474	202	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) -> X e. CC )
475	473	sselda	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) -> s e. CC )
476	474 475	addcld	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) -> ( X + s ) e. CC )
477	366 375 473 381 476	cncfmptssg	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) -cn-> CC ) )
478		eqid	|- ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) = ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
479	386 478 392	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 ) ) )
480	473 381 479	syl2anc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` CCfld ) ) )
481	477 480	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 ) ) )
482		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 ) ) ) ) )
483	397 473 482	syl2anc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( TopOpen ` CCfld ) |`t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) e. ( TopOn ` ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) )
484		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 ) ) ) )
485	483 397 484	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 ) ) ) )
486	481 485	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 ) ) )
487	486	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 ) )
488		lbico1	|- ( ( ( H ` i ) e. RR* /\ ( H ` ( i + 1 ) ) e. RR* /\ ( H ` i ) < ( H ` ( i + 1 ) ) ) -> ( H ` i ) e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
489	376 251 180 488	syl3anc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` i ) e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
490		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 ) ) )
491	490	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 ) ) ) )
492	491	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 ) ) )
493	487 489 492	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 ) ) )
494		uncom	|- ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) = ( { ( H ` i ) } u. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
495		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 ) ) ) )
496	376 251 180 495	syl3anc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( { ( H ` i ) } u. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) = ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
497	494 496	syl5eq	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) = ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
498		iftrue	|- ( s = ( H ` i ) -> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( Q ` i ) )
499	498	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 ) )
500	246	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s = ( H ` i ) ) -> ( Q ` i ) = ( X + ( H ` i ) ) )
501		oveq2	|- ( s = ( H ` i ) -> ( X + s ) = ( X + ( H ` i ) ) )
502	501	eqcomd	|- ( s = ( H ` i ) -> ( X + ( H ` i ) ) = ( X + s ) )
503	502	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s = ( H ` i ) ) -> ( X + ( H ` i ) ) = ( X + s ) )
504	499 500 503	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 ) )
505	504	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 ) )
506		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 ) )
507	506	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 ) )
508		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 ) ) )
509	422	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 ) )
510		velsn	|- ( s e. { ( H ` i ) } <-> s = ( H ` i ) )
511	510	notbii	|- ( -. s e. { ( H ` i ) } <-> -. s = ( H ` i ) )
512		elun	|- ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) <-> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` i ) } ) )
513	512	biimpi	|- ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) -> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` i ) } ) )
514	513	orcomd	|- ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) -> ( s e. { ( H ` i ) } \/ s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) )
515	514	ord	|- ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) -> ( -. s e. { ( H ` i ) } -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) )
516	511 515	syl5bir	|- ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) -> ( -. s = ( H ` i ) -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) )
517	516	imp	|- ( ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) /\ -. s = ( H ` i ) ) -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
518	517	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 ) ) ) )
519	5	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) -> X e. RR )
520		elsni	|- ( s e. { ( H ` i ) } -> s = ( H ` i ) )
521	520	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( H ` i ) } ) -> s = ( H ` i ) )
522	230	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( H ` i ) } ) -> ( H ` i ) e. RR )
523	521 522	eqeltrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. { ( H ` i ) } ) -> s e. RR )
524	435 523	jaodan	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` i ) } ) ) -> s e. RR )
525	512 524	sylan2b	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) -> s e. RR )
526	519 525	readdcld	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) -> ( X + s ) e. RR )
527	526	adantr	|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) /\ -. s = ( H ` i ) ) -> ( X + s ) e. RR )
528	508 509 518 527	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 ) )
529	507 528	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 ) )
530	505 529	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 ) )
531	497 530	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 ) ) )
532	497	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 ) ) ) ) )
533	532	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 ) ) )
534	533	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 ) ) )
535	493 531 534	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 ) ) )
536		eqid	|- ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) )
537		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 ) ) )
538	230	recnd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H ` i ) e. CC )
539	536 386 537 454 305 538	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 ) ) ) )
540	535 539	mpbird	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) limCC ( H ` i ) ) )
541	470 540 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 ) ) )
542	459	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 ) ) )
543	541 542	eleqtrd	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) limCC ( H ` i ) ) )
544	230 231 310 461 543	iblcncfioo	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) e. L^1 )
545	6	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> F : ( -u _pi [,] _pi ) --> CC )
546	54	a1i	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> -u _pi e. RR* )
547	56	a1i	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> _pi e. RR* )
548	27	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
549		simplr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> i e. ( 0 ..^ M ) )
550		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) )
551	169 179	oveq12d	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) = ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) )
552	551	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 ) ) )
553	550 552	eleqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) )
554	553 117	syldan	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
555	546 547 548 549 554	fourierdlem1	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. ( -u _pi [,] _pi ) )
556	545 555	ffvelrnd	|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> ( F ` ( X + t ) ) e. CC )
557	230 231 544 556	ibliooicc	|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) e. L^1 )
558	20 26 165 180 229 557	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 )
559	551	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 )
560	559	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 )
561	558 560	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 )
562	126 161 561	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 )
563	122 562	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 )
564	19 78 563	3eqtrd	|- ( ph -> S. ( -u _pi [,] _pi ) ( F ` t ) _d t = S. ( ( -u _pi - X ) [,] ( _pi - X ) ) ( F ` ( X + s ) ) _d s )