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 )