Theorem fourierdlem93 40416

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

Hypotheses

Ref	Expression
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 ) ) ) ) lim CC ( Q ` i ) ) )
fourierdlem93.9	|- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )

Assertion

Ref	Expression
fourierdlem93	|- ( ph -> S. ( -u pi [,] pi ) ( F ` t ) _d t = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + s ) ) _d s )

Distinct variable groups:   i, F, s, t   i, H, s, t   t, L   i, M, m, p   M, s, t   Q, i, p   Q, s, t   t, R   i, X, s, t   ph, i, s, t

Allowed substitution hints:   ph( m, p)   P( t, i, m, s, p)   Q( m)   R( i, m, s, p)   F( m, p)   H( m, p)   L( i, m, s, p)   X( m, p)

Proof of Theorem fourierdlem93

Dummy variables x r j are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem93.4	. . . . . . . 8 |- ( ph -> Q e. ( P ` M ) )
2		fourierdlem93.3	. . . . . . . . 9 |- ( ph -> M e. NN )
3		fourierdlem93.1	. . . . . . . . . 10 |- 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 ) ) ) } )
4	3	fourierdlem2 40326	. . . . . . . . 9 |- ( 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 ) ) ) ) ) )
5	2, 4	syl 17	. . . . . . . 8 |- ( 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 ) ) ) ) ) )
6	1, 5	mpbid 222	. . . . . . 7 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
7	6	simprd 479	. . . . . 6 |- ( ph -> ( ( ( Q ` 0 ) = -u pi /\ ( Q ` M ) = pi ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
8	7	simplld 791	. . . . 5 |- ( ph -> ( Q ` 0 ) = -u pi )
9	8	eqcomd 2628	. . . 4 |- ( ph -> -u pi = ( Q ` 0 ) )
10	7	simplrd 793	. . . . 5 |- ( ph -> ( Q ` M ) = pi )
11	10	eqcomd 2628	. . . 4 |- ( ph -> pi = ( Q ` M ) )
12	9, 11	oveq12d 6668	. . 3 |- ( ph -> ( -u pi [,] pi ) = ( ( Q ` 0 ) [,] ( Q ` M ) ) )
13	12	itgeq1d 40172	. 2 |- ( ph -> S. ( -u pi [,] pi ) ( F ` t ) _d t = S. ( ( Q ` 0 ) [,] ( Q ` M ) ) ( F ` t ) _d t )
14		0zd 11389	. . 3 |- ( ph -> 0 e. ZZ )
15		nnuz 11723	. . . . 5 |- NN = ( ZZ>= ` 1 )
16	2, 15	syl6eleq 2711	. . . 4 |- ( ph -> M e. ( ZZ>= ` 1 ) )
17		1e0p1 11552	. . . . . 6 |- 1 = ( 0 + 1 )
18	17	a1i 11	. . . . 5 |- ( ph -> 1 = ( 0 + 1 ) )
19	18	fveq2d 6195	. . . 4 |- ( ph -> ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) ) )
20	16, 19	eleqtrd 2703	. . 3 |- ( ph -> M e. ( ZZ>= ` ( 0 + 1 ) ) )
21	3, 2, 1	fourierdlem15 40339	. . . 4 |- ( ph -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
22		pire 24210	. . . . . . 7 |- pi e. RR
23	22	renegcli 10342	. . . . . 6 |- -u pi e. RR
24		iccssre 12255	. . . . . 6 |- ( ( -u pi e. RR /\ pi e. RR ) -> ( -u pi [,] pi ) C_ RR )
25	23, 22, 24	mp2an 708	. . . . 5 |- ( -u pi [,] pi ) C_ RR
26	25	a1i 11	. . . 4 |- ( ph -> ( -u pi [,] pi ) C_ RR )
27	21, 26	fssd 6057	. . 3 |- ( ph -> Q : ( 0 ... M ) --> RR )
28	7	simprd 479	. . . 4 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
29	28	r19.21bi 2932	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
30		fourierdlem93.6	. . . . 5 |- ( ph -> F : ( -u pi [,] pi ) --> CC )
31	30	adantr 481	. . . 4 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> F : ( -u pi [,] pi ) --> CC )
32		simpr 477	. . . . 5 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
33	12	eqcomd 2628	. . . . . 6 |- ( ph -> ( ( Q ` 0 ) [,] ( Q ` M ) ) = ( -u pi [,] pi ) )
34	33	adantr 481	. . . . 5 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( ( Q ` 0 ) [,] ( Q ` M ) ) = ( -u pi [,] pi ) )
35	32, 34	eleqtrd 2703	. . . 4 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> t e. ( -u pi [,] pi ) )
36	31, 35	ffvelrnd 6360	. . 3 |- ( ( ph /\ t e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( F ` t ) e. CC )
37	27	adantr 481	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
38		elfzofz 12485	. . . . . 6 |- ( i e. ( 0..^ M ) -> i e. ( 0 ... M ) )
39	38	adantl 482	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> i e. ( 0 ... M ) )
40	37, 39	ffvelrnd 6360	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR )
41		fzofzp1 12565	. . . . . 6 |- ( i e. ( 0..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
42	41	adantl 482	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
43	37, 42	ffvelrnd 6360	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
44	30	feqmptd 6249	. . . . . . . . . 10 |- ( ph -> F = ( t e. ( -u pi [,] pi ) |-> ( F ` t ) ) )
45	44	adantr 481	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F = ( t e. ( -u pi [,] pi ) |-> ( F ` t ) ) )
46	45	reseq1d 5395	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( t e. ( -u pi [,] pi ) |-> ( F ` t ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
47		ioossicc 12259	. . . . . . . . . . 11 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
48	47	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
49	23	rexri 10097	. . . . . . . . . . . . . 14 |- -u pi e. RR*
50	49	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> -u pi e. RR* )
51	22	rexri 10097	. . . . . . . . . . . . . 14 |- pi e. RR*
52	51	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> pi e. RR* )
53	21	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
54		simplr 792	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> i e. ( 0..^ M ) )
55		simpr 477	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
56	50, 52, 53, 54, 55	fourierdlem1 40325	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> t e. ( -u pi [,] pi ) )
57	56	ralrimiva 2966	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A. t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) t e. ( -u pi [,] pi ) )
58		dfss3 3592	. . . . . . . . . . 11 |- ( ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) <-> A. t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) t e. ( -u pi [,] pi ) )
59	57, 58	sylibr 224	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) )
60	48, 59	sstrd 3613	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u pi [,] pi ) )
61	60	resmptd 5452	. . . . . . . 8 |- ( ( 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 ) ) )
62	46, 61	eqtrd 2656	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) )
63	62	eqcomd 2628	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
64		fourierdlem93.7	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
65	63, 64	eqeltrd 2701	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
66		fourierdlem93.9	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
67	62	oveq1d 6665	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) lim CC ( Q ` ( i + 1 ) ) ) )
68	66, 67	eleqtrd 2703	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) lim CC ( Q ` ( i + 1 ) ) ) )
69		fourierdlem93.8	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
70	62	oveq1d 6665	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) = ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) lim CC ( Q ` i ) ) )
71	69, 70	eleqtrd 2703	. . . . 5 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) lim CC ( Q ` i ) ) )
72	40, 43, 65, 68, 71	iblcncfioo 40194	. . . 4 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. L^1 )
73	30	ad2antrr 762	. . . . 5 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> F : ( -u pi [,] pi ) --> CC )
74	73, 56	ffvelrnd 6360	. . . 4 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` t ) e. CC )
75	40, 43, 72, 74	ibliooicc 40187	. . 3 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) |-> ( F ` t ) ) e. L^1 )
76	14, 20, 27, 29, 36, 75	itgspltprt 40195	. 2 |- ( 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 )
77		fvres 6207	. . . . . . . 8 |- ( t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) = ( F ` t ) )
78	77	eqcomd 2628	. . . . . . 7 |- ( t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -> ( F ` t ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) )
79	78	adantl 482	. . . . . 6 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) -> ( F ` t ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` t ) )
80	79	itgeq2dv 23548	. . . . 5 |- ( ( 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 )
81		eqid 2622	. . . . . 6 |- ( 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 ) ) ) )
82	30	adantr 481	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> F : ( -u pi [,] pi ) --> CC )
83	82, 59	fssresd 6071	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) --> CC )
84	48	resabs1d 5428	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
85	84, 64	eqeltrd 2701	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
86	84	oveq1d 6665	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
87	40, 43, 29, 83	limcicciooub 39869	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
88	86, 87	eqtr3d 2658	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
89	66, 88	eleqtrd 2703	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` ( i + 1 ) ) ) )
90	84	eqcomd 2628	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
91	90	oveq1d 6665	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) = ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
92	40, 43, 29, 83	limciccioolb 39853	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
93	91, 92	eqtrd 2656	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) = ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
94	69, 93	eleqtrd 2703	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) lim CC ( Q ` i ) ) )
95		fourierdlem93.5	. . . . . . 7 |- ( ph -> X e. RR )
96	95	adantr 481	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> X e. RR )
97	81, 40, 43, 29, 83, 85, 89, 94, 96	fourierdlem82 40405	. . . . 5 |- ( ( 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 )
98	40	adantr 481	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( Q ` i ) e. RR )
99	43	adantr 481	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
100	95	ad2antrr 762	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> X e. RR )
101	98, 100	resubcld 10458	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( Q ` i ) - X ) e. RR )
102	99, 100	resubcld 10458	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( Q ` ( i + 1 ) ) - X ) e. RR )
103		simpr 477	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) )
104		eliccre 39728	. . . . . . . . . 10 |- ( ( ( ( Q ` i ) - X ) e. RR /\ ( ( Q ` ( i + 1 ) ) - X ) e. RR /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t e. RR )
105	101, 102, 103, 104	syl3anc 1326	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t e. RR )
106	100, 105	readdcld 10069	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( X + t ) e. RR )
107		elicc2 12238	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) )
108	101, 102, 107	syl2anc 693	. . . . . . . . . . 11 |- ( ( ( 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 ) ) ) )
109	103, 108	mpbid 222	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
110	109	simp2d 1074	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( Q ` i ) - X ) <_ t )
111	98, 100, 105	lesubadd2d 10626	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( ( Q ` i ) - X ) <_ t <-> ( Q ` i ) <_ ( X + t ) ) )
112	110, 111	mpbid 222	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( Q ` i ) <_ ( X + t ) )
113	109	simp3d 1075	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> t <_ ( ( Q ` ( i + 1 ) ) - X ) )
114	100, 105, 99	leaddsub2d 10629	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( ( X + t ) <_ ( Q ` ( i + 1 ) ) <-> t <_ ( ( Q ` ( i + 1 ) ) - X ) ) )
115	113, 114	mpbird 247	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( X + t ) <_ ( Q ` ( i + 1 ) ) )
116	98, 99, 106, 112, 115	eliccd 39726	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) ) -> ( X + t ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) )
117		fvres 6207	. . . . . . 7 |- ( ( X + t ) e. ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) = ( F ` ( X + t ) ) )
118	116, 117	syl 17	. . . . . 6 |- ( ( ( 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 ) ) )
119	118	itgeq2dv 23548	. . . . 5 |- ( ( 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 )
120	80, 97, 119	3eqtrd 2660	. . . 4 |- ( ( 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 )
121	120	sumeq2dv 14433	. . 3 |- ( 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 )
122		oveq2 6658	. . . . . . 7 |- ( s = t -> ( X + s ) = ( X + t ) )
123	122	fveq2d 6195	. . . . . 6 |- ( s = t -> ( F ` ( X + s ) ) = ( F ` ( X + t ) ) )
124	123	cbvitgv 23543	. . . . 5 |- S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + s ) ) _d s = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + t ) ) _d t
125	124	a1i 11	. . . 4 |- ( ph -> S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + s ) ) _d s = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + t ) ) _d t )
126		fourierdlem93.2	. . . . . . . . 9 |- H = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )
127	126	a1i 11	. . . . . . . 8 |- ( ph -> H = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) )
128		fveq2 6191	. . . . . . . . . 10 |- ( i = 0 -> ( Q ` i ) = ( Q ` 0 ) )
129	128	oveq1d 6665	. . . . . . . . 9 |- ( i = 0 -> ( ( Q ` i ) - X ) = ( ( Q ` 0 ) - X ) )
130	129	adantl 482	. . . . . . . 8 |- ( ( ph /\ i = 0 ) -> ( ( Q ` i ) - X ) = ( ( Q ` 0 ) - X ) )
131	2	nnzd 11481	. . . . . . . . . 10 |- ( ph -> M e. ZZ )
132	14, 131, 14	3jca 1242	. . . . . . . . 9 |- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) )
133		0le0 11110	. . . . . . . . . . 11 |- 0 <_ 0
134	133	a1i 11	. . . . . . . . . 10 |- ( ph -> 0 <_ 0 )
135		0red 10041	. . . . . . . . . . 11 |- ( ph -> 0 e. RR )
136	2	nnred 11035	. . . . . . . . . . 11 |- ( ph -> M e. RR )
137	2	nngt0d 11064	. . . . . . . . . . 11 |- ( ph -> 0 < M )
138	135, 136, 137	ltled 10185	. . . . . . . . . 10 |- ( ph -> 0 <_ M )
139	134, 138	jca 554	. . . . . . . . 9 |- ( ph -> ( 0 <_ 0 /\ 0 <_ M ) )
140		elfz2 12333	. . . . . . . . 9 |- ( 0 e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) /\ ( 0 <_ 0 /\ 0 <_ M ) ) )
141	132, 139, 140	sylanbrc 698	. . . . . . . 8 |- ( ph -> 0 e. ( 0 ... M ) )
142	8, 23	syl6eqel 2709	. . . . . . . . 9 |- ( ph -> ( Q ` 0 ) e. RR )
143	142, 95	resubcld 10458	. . . . . . . 8 |- ( ph -> ( ( Q ` 0 ) - X ) e. RR )
144	127, 130, 141, 143	fvmptd 6288	. . . . . . 7 |- ( ph -> ( H ` 0 ) = ( ( Q ` 0 ) - X ) )
145	8	oveq1d 6665	. . . . . . 7 |- ( ph -> ( ( Q ` 0 ) - X ) = ( -u pi - X ) )
146	144, 145	eqtr2d 2657	. . . . . 6 |- ( ph -> ( -u pi - X ) = ( H ` 0 ) )
147		fveq2 6191	. . . . . . . . . 10 |- ( i = M -> ( Q ` i ) = ( Q ` M ) )
148	147	oveq1d 6665	. . . . . . . . 9 |- ( i = M -> ( ( Q ` i ) - X ) = ( ( Q ` M ) - X ) )
149	148	adantl 482	. . . . . . . 8 |- ( ( ph /\ i = M ) -> ( ( Q ` i ) - X ) = ( ( Q ` M ) - X ) )
150	14, 131, 131	3jca 1242	. . . . . . . . 9 |- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ M e. ZZ ) )
151	136	leidd 10594	. . . . . . . . . 10 |- ( ph -> M <_ M )
152	138, 151	jca 554	. . . . . . . . 9 |- ( ph -> ( 0 <_ M /\ M <_ M ) )
153		elfz2 12333	. . . . . . . . 9 |- ( M e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ M e. ZZ ) /\ ( 0 <_ M /\ M <_ M ) ) )
154	150, 152, 153	sylanbrc 698	. . . . . . . 8 |- ( ph -> M e. ( 0 ... M ) )
155	10, 22	syl6eqel 2709	. . . . . . . . 9 |- ( ph -> ( Q ` M ) e. RR )
156	155, 95	resubcld 10458	. . . . . . . 8 |- ( ph -> ( ( Q ` M ) - X ) e. RR )
157	127, 149, 154, 156	fvmptd 6288	. . . . . . 7 |- ( ph -> ( H ` M ) = ( ( Q ` M ) - X ) )
158	10	oveq1d 6665	. . . . . . 7 |- ( ph -> ( ( Q ` M ) - X ) = ( pi - X ) )
159	157, 158	eqtr2d 2657	. . . . . 6 |- ( ph -> ( pi - X ) = ( H ` M ) )
160	146, 159	oveq12d 6668	. . . . 5 |- ( ph -> ( ( -u pi - X ) [,] ( pi - X ) ) = ( ( H ` 0 ) [,] ( H ` M ) ) )
161	160	itgeq1d 40172	. . . 4 |- ( ph -> S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + t ) ) _d t = S. ( ( H ` 0 ) [,] ( H ` M ) ) ( F ` ( X + t ) ) _d t )
162	27	ffvelrnda 6359	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
163	95	adantr 481	. . . . . . . 8 |- ( ( ph /\ i e. ( 0 ... M ) ) -> X e. RR )
164	162, 163	resubcld 10458	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( ( Q ` i ) - X ) e. RR )
165	164, 126	fmptd 6385	. . . . . 6 |- ( ph -> H : ( 0 ... M ) --> RR )
166	40, 43, 96, 29	ltsub1dd 10639	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - X ) < ( ( Q ` ( i + 1 ) ) - X ) )
167	39, 164	syldan 487	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) - X ) e. RR )
168	126	fvmpt2 6291	. . . . . . . 8 |- ( ( i e. ( 0 ... M ) /\ ( ( Q ` i ) - X ) e. RR ) -> ( H ` i ) = ( ( Q ` i ) - X ) )
169	39, 167, 168	syl2anc 693	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` i ) = ( ( Q ` i ) - X ) )
170		fveq2 6191	. . . . . . . . . . . 12 |- ( i = j -> ( Q ` i ) = ( Q ` j ) )
171	170	oveq1d 6665	. . . . . . . . . . 11 |- ( i = j -> ( ( Q ` i ) - X ) = ( ( Q ` j ) - X ) )
172	171	cbvmptv 4750	. . . . . . . . . 10 |- ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) ) = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
173	126, 172	eqtri 2644	. . . . . . . . 9 |- H = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) )
174	173	a1i 11	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> H = ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) ) )
175		fveq2 6191	. . . . . . . . . 10 |- ( j = ( i + 1 ) -> ( Q ` j ) = ( Q ` ( i + 1 ) ) )
176	175	oveq1d 6665	. . . . . . . . 9 |- ( j = ( i + 1 ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
177	176	adantl 482	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( Q ` j ) - X ) = ( ( Q ` ( i + 1 ) ) - X ) )
178	43, 96	resubcld 10458	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) - X ) e. RR )
179	174, 177, 42, 178	fvmptd 6288	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` ( i + 1 ) ) = ( ( Q ` ( i + 1 ) ) - X ) )
180	166, 169, 179	3brtr4d 4685	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` i ) < ( H ` ( i + 1 ) ) )
181		frn 6053	. . . . . . . . 9 |- ( F : ( -u pi [,] pi ) --> CC -> ran F C_ CC )
182	30, 181	syl 17	. . . . . . . 8 |- ( ph -> ran F C_ CC )
183	182	adantr 481	. . . . . . 7 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ran F C_ CC )
184		ffun 6048	. . . . . . . . . 10 |- ( F : ( -u pi [,] pi ) --> CC -> Fun F )
185	30, 184	syl 17	. . . . . . . . 9 |- ( ph -> Fun F )
186	185	adantr 481	. . . . . . . 8 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> Fun F )
187	23	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u pi e. RR )
188	22	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> pi e. RR )
189	95	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> X e. RR )
190	144, 143	eqeltrd 2701	. . . . . . . . . . . . 13 |- ( ph -> ( H ` 0 ) e. RR )
191	190	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` 0 ) e. RR )
192	157, 156	eqeltrd 2701	. . . . . . . . . . . . 13 |- ( ph -> ( H ` M ) e. RR )
193	192	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` M ) e. RR )
194		simpr 477	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. ( ( H ` 0 ) [,] ( H ` M ) ) )
195		eliccre 39728	. . . . . . . . . . . 12 |- ( ( ( H ` 0 ) e. RR /\ ( H ` M ) e. RR /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. RR )
196	191, 193, 194, 195	syl3anc 1326	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t e. RR )
197	189, 196	readdcld 10069	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. RR )
198	128	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i = 0 ) -> ( Q ` i ) = ( Q ` 0 ) )
199	198	oveq1d 6665	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i = 0 ) -> ( ( Q ` i ) - X ) = ( ( Q ` 0 ) - X ) )
200	127, 199, 141, 143	fvmptd 6288	. . . . . . . . . . . . . 14 |- ( ph -> ( H ` 0 ) = ( ( Q ` 0 ) - X ) )
201	200	oveq2d 6666	. . . . . . . . . . . . 13 |- ( ph -> ( X + ( H ` 0 ) ) = ( X + ( ( Q ` 0 ) - X ) ) )
202	95	recnd 10068	. . . . . . . . . . . . . 14 |- ( ph -> X e. CC )
203	142	recnd 10068	. . . . . . . . . . . . . 14 |- ( ph -> ( Q ` 0 ) e. CC )
204	202, 203	pncan3d 10395	. . . . . . . . . . . . 13 |- ( ph -> ( X + ( ( Q ` 0 ) - X ) ) = ( Q ` 0 ) )
205	201, 204, 8	3eqtrrd 2661	. . . . . . . . . . . 12 |- ( ph -> -u pi = ( X + ( H ` 0 ) ) )
206	205	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u pi = ( X + ( H ` 0 ) ) )
207		elicc2 12238	. . . . . . . . . . . . . . 15 |- ( ( ( 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 693	. . . . . . . . . . . . . 14 |- ( ( 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 222	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( t e. RR /\ ( H ` 0 ) <_ t /\ t <_ ( H ` M ) ) )
210	209	simp2d 1074	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( H ` 0 ) <_ t )
211	191, 196, 189, 210	leadd2dd 10642	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + ( H ` 0 ) ) <_ ( X + t ) )
212	206, 211	eqbrtrd 4675	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> -u pi <_ ( X + t ) )
213	209	simp3d 1075	. . . . . . . . . . . 12 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> t <_ ( H ` M ) )
214	196, 193, 189, 213	leadd2dd 10642	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) <_ ( X + ( H ` M ) ) )
215	157	oveq2d 6666	. . . . . . . . . . . . 13 |- ( ph -> ( X + ( H ` M ) ) = ( X + ( ( Q ` M ) - X ) ) )
216	155	recnd 10068	. . . . . . . . . . . . . 14 |- ( ph -> ( Q ` M ) e. CC )
217	202, 216	pncan3d 10395	. . . . . . . . . . . . 13 |- ( ph -> ( X + ( ( Q ` M ) - X ) ) = ( Q ` M ) )
218	215, 217, 10	3eqtrrd 2661	. . . . . . . . . . . 12 |- ( ph -> pi = ( X + ( H ` M ) ) )
219	218	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> pi = ( X + ( H ` M ) ) )
220	214, 219	breqtrrd 4681	. . . . . . . . . 10 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) <_ pi )
221	187, 188, 197, 212, 220	eliccd 39726	. . . . . . . . 9 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. ( -u pi [,] pi ) )
222		fdm 6051	. . . . . . . . . . . 12 |- ( F : ( -u pi [,] pi ) --> CC -> dom F = ( -u pi [,] pi ) )
223	30, 222	syl 17	. . . . . . . . . . 11 |- ( ph -> dom F = ( -u pi [,] pi ) )
224	223	eqcomd 2628	. . . . . . . . . 10 |- ( ph -> ( -u pi [,] pi ) = dom F )
225	224	adantr 481	. . . . . . . . 9 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( -u pi [,] pi ) = dom F )
226	221, 225	eleqtrd 2703	. . . . . . . 8 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( X + t ) e. dom F )
227		fvelrn 6352	. . . . . . . 8 |- ( ( Fun F /\ ( X + t ) e. dom F ) -> ( F ` ( X + t ) ) e. ran F )
228	186, 226, 227	syl2anc 693	. . . . . . 7 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( F ` ( X + t ) ) e. ran F )
229	183, 228	sseldd 3604	. . . . . 6 |- ( ( ph /\ t e. ( ( H ` 0 ) [,] ( H ` M ) ) ) -> ( F ` ( X + t ) ) e. CC )
230	169, 167	eqeltrd 2701	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` i ) e. RR )
231	179, 178	eqeltrd 2701	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` ( i + 1 ) ) e. RR )
232	82, 60	fssresd 6071	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
233	40	rexrd 10089	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. RR* )
234	233	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
235	43	rexrd 10089	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
236	235	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
237	95	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> X e. RR )
238		elioore 12205	. . . . . . . . . . . . . . 15 |- ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> t e. RR )
239	238	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t e. RR )
240	237, 239	readdcld 10069	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. RR )
241	169	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( H ` i ) ) = ( X + ( ( Q ` i ) - X ) ) )
242	202	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> X e. CC )
243	40	recnd 10068	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. CC )
244	242, 243	pncan3d 10395	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( ( Q ` i ) - X ) ) = ( Q ` i ) )
245		eqidd 2623	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( Q ` i ) )
246	241, 244, 245	3eqtrrd 2661	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) = ( X + ( H ` i ) ) )
247	246	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) = ( X + ( H ` i ) ) )
248	230	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) e. RR )
249		simpr 477	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
250	248	rexrd 10089	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) e. RR* )
251	231	rexrd 10089	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` ( i + 1 ) ) e. RR* )
252	251	adantr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` ( i + 1 ) ) e. RR* )
253		elioo2 12216	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 693	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 222	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 1074	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` i ) < t )
257	248, 239, 237, 256	ltadd2dd 10196	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + ( H ` i ) ) < ( X + t ) )
258	247, 257	eqbrtrd 4675	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( X + t ) )
259	231	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( H ` ( i + 1 ) ) e. RR )
260	255	simp3d 1075	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> t < ( H ` ( i + 1 ) ) )
261	239, 259, 237, 260	ltadd2dd 10196	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) < ( X + ( H ` ( i + 1 ) ) ) )
262	179	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( X + ( ( Q ` ( i + 1 ) ) - X ) ) )
263	43	recnd 10068	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. CC )
264	242, 263	pncan3d 10395	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( ( Q ` ( i + 1 ) ) - X ) ) = ( Q ` ( i + 1 ) ) )
265	262, 264	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( Q ` ( i + 1 ) ) )
266	265	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + ( H ` ( i + 1 ) ) ) = ( Q ` ( i + 1 ) ) )
267	261, 266	breqtrd 4679	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) < ( Q ` ( i + 1 ) ) )
268	234, 236, 240, 258, 267	eliood 39720	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
269		eqid 2622	. . . . . . . . . . . 12 |- ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) = ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
270	268, 269	fmptd 6385	. . . . . . . . . . 11 |- ( ( 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 6400	. . . . . . . . . . 11 |- ( ( ( 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 693	. . . . . . . . . 10 |- ( ( 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 6658	. . . . . . . . . . . . . . . 16 |- ( t = r -> ( X + t ) = ( X + r ) )
274	273	cbvmptv 4750	. . . . . . . . . . . . . . 15 |- ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) = ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) )
275	274	fveq1i 6192	. . . . . . . . . . . . . 14 |- ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) = ( ( r e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + r ) ) ` s )
276	275	fveq2i 6194	. . . . . . . . . . . . 13 |- ( ( 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 4741	. . . . . . . . . . . 12 |- ( 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 11	. . . . . . . . . . 11 |- ( ( 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 6191	. . . . . . . . . . . . . 14 |- ( 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 6195	. . . . . . . . . . . . 13 |- ( 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 4750	. . . . . . . . . . . 12 |- ( 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 11	. . . . . . . . . . 11 |- ( ( 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 2623	. . . . . . . . . . . . . . 15 |- ( ( ( 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 6658	. . . . . . . . . . . . . . . 16 |- ( r = t -> ( X + r ) = ( X + t ) )
285	284	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) /\ r = t ) -> ( X + r ) = ( X + t ) )
286	283, 285, 249, 240	fvmptd 6288	. . . . . . . . . . . . . 14 |- ( ( ( 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 6195	. . . . . . . . . . . . 13 |- ( ( ( 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 6207	. . . . . . . . . . . . . 14 |- ( ( X + t ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` ( X + t ) ) = ( F ` ( X + t ) ) )
289	268, 288	syl 17	. . . . . . . . . . . . 13 |- ( ( ( 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 2656	. . . . . . . . . . . 12 |- ( ( ( 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 4744	. . . . . . . . . . 11 |- ( ( 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 2660	. . . . . . . . . 10 |- ( ( 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 2657	. . . . . . . . 9 |- ( ( 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 2622	. . . . . . . . . . 11 |- ( t e. CC |-> ( X + t ) ) = ( t e. CC |-> ( X + t ) )
295		ssid 3624	. . . . . . . . . . . . . . 15 |- CC C_ CC
296	295	a1i 11	. . . . . . . . . . . . . 14 |- ( X e. CC -> CC C_ CC )
297		id 22	. . . . . . . . . . . . . 14 |- ( X e. CC -> X e. CC )
298	296, 297, 296	constcncfg 40084	. . . . . . . . . . . . 13 |- ( X e. CC -> ( t e. CC |-> X ) e. ( CC -cn-> CC ) )
299		cncfmptid 22715	. . . . . . . . . . . . . . 15 |- ( ( CC C_ CC /\ CC C_ CC ) -> ( t e. CC |-> t ) e. ( CC -cn-> CC ) )
300	295, 295, 299	mp2an 708	. . . . . . . . . . . . . 14 |- ( t e. CC |-> t ) e. ( CC -cn-> CC )
301	300	a1i 11	. . . . . . . . . . . . 13 |- ( X e. CC -> ( t e. CC |-> t ) e. ( CC -cn-> CC ) )
302	298, 301	addcncf 40086	. . . . . . . . . . . 12 |- ( X e. CC -> ( t e. CC |-> ( X + t ) ) e. ( CC -cn-> CC ) )
303	242, 302	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. CC |-> ( X + t ) ) e. ( CC -cn-> CC ) )
304		ioosscn 39716	. . . . . . . . . . . 12 |- ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) C_ CC
305	304	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) C_ CC )
306		ioosscn 39716	. . . . . . . . . . . 12 |- ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
307	306	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
308	294, 303, 305, 307, 268	cncfmptssg 40083	. . . . . . . . . 10 |- ( ( 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, 64	cncfco 22710	. . . . . . . . 9 |- ( ( 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 2701	. . . . . . . 8 |- ( ( 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 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( Q ` i ) e. RR* )
312	235	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
313		simpr 477	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 3203	. . . . . . . . . . . . . . . . . 18 |- r e. _V
315	269	elrnmpt 5372	. . . . . . . . . . . . . . . . . 18 |- ( 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 5	. . . . . . . . . . . . . . . . 17 |- ( 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 208	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 1843	. . . . . . . . . . . . . . . . . 18 |- F/ t ( ph /\ i e. ( 0..^ M ) )
319		nfmpt1 4747	. . . . . . . . . . . . . . . . . . . 20 |- F/_ t ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
320	319	nfrn 5368	. . . . . . . . . . . . . . . . . . 19 |- F/_ t ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
321	320	nfcri 2758	. . . . . . . . . . . . . . . . . 18 |- F/ t r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) )
322	318, 321	nfan 1828	. . . . . . . . . . . . . . . . 17 |- F/ t ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) )
323		nfv 1843	. . . . . . . . . . . . . . . . 17 |- F/ t r e. RR
324		simp3 1063	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r = ( X + t ) )
325	95	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> X e. RR )
326	238	3ad2ant2 1083	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> t e. RR )
327	325, 326	readdcld 10069	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( X + t ) e. RR )
328	324, 327	eqeltrd 2701	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r e. RR )
329	328	3exp 1264	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> r e. RR ) ) )
330	329	ad2antrr 762	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 3026	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 15	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r e. RR )
333		nfv 1843	. . . . . . . . . . . . . . . . 17 |- F/ t ( Q ` i ) < r
334	258	3adant3 1081	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( Q ` i ) < ( X + t ) )
335		simp3 1063	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r = ( X + t ) )
336	334, 335	breqtrrd 4681	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( Q ` i ) < r )
337	336	3exp 1264	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> ( Q ` i ) < r ) ) )
338	337	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 3026	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 15	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> ( Q ` i ) < r )
341		nfv 1843	. . . . . . . . . . . . . . . . 17 |- F/ t r < ( Q ` ( i + 1 ) )
342	267	3adant3 1081	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> ( X + t ) < ( Q ` ( i + 1 ) ) )
343	335, 342	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) /\ r = ( X + t ) ) -> r < ( Q ` ( i + 1 ) ) )
344	343	3exp 1264	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> ( r = ( X + t ) -> r < ( Q ` ( i + 1 ) ) ) ) )
345	344	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 3026	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 15	. . . . . . . . . . . . . . 15 |- ( ( ( 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 39720	. . . . . . . . . . . . . 14 |- ( ( ( 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 3814	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i dom F ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i ( -u pi [,] pi ) ) )
350	349	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( 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 5419	. . . . . . . . . . . . . . . . 17 |- dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i dom F )
352	351	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) i^i dom F ) )
353		dfss 3589	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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	60, 353	sylib 208	. . . . . . . . . . . . . . . 16 |- ( ( 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 2666	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> dom ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
356	355	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( 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 2704	. . . . . . . . . . . . 13 |- ( ( ( 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 10173	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r =/= ( Q ` ( i + 1 ) ) )
359	358	neneqd 2799	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> -. r = ( Q ` ( i + 1 ) ) )
360		velsn 4193	. . . . . . . . . . . . . 14 |- ( r e. { ( Q ` ( i + 1 ) ) } <-> r = ( Q ` ( i + 1 ) ) )
361	359, 360	sylnibr 319	. . . . . . . . . . . . 13 |- ( ( ( 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 3585	. . . . . . . . . . . 12 |- ( ( ( 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 2966	. . . . . . . . . . 11 |- ( ( 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 3592	. . . . . . . . . . 11 |- ( 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 224	. . . . . . . . . 10 |- ( ( 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 2622	. . . . . . . . . . . . . . . . 17 |- ( s e. CC |-> ( X + s ) ) = ( s e. CC |-> ( X + s ) )
367	202	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ s e. CC ) -> X e. CC )
368		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ s e. CC ) -> s e. CC )
369	367, 368	addcomd 10238	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ s e. CC ) -> ( X + s ) = ( s + X ) )
370	369	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( s e. CC |-> ( X + s ) ) = ( s e. CC |-> ( s + X ) ) )
371		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. CC |-> ( s + X ) ) = ( s e. CC |-> ( s + X ) )
372	371	addccncf 22719	. . . . . . . . . . . . . . . . . . . 20 |- ( X e. CC -> ( s e. CC |-> ( s + X ) ) e. ( CC -cn-> CC ) )
373	202, 372	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( s e. CC |-> ( s + X ) ) e. ( CC -cn-> CC ) )
374	370, 373	eqeltrd 2701	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( s e. CC |-> ( X + s ) ) e. ( CC -cn-> CC ) )
375	374	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. CC |-> ( X + s ) ) e. ( CC -cn-> CC ) )
376	230	rexrd 10089	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` i ) e. RR* )
377		iocssre 12253	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( H ` i ) e. RR* /\ ( H ` ( i + 1 ) ) e. RR ) -> ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) C_ RR )
378	376, 231, 377	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) C_ RR )
379		ax-resscn 9993	. . . . . . . . . . . . . . . . . 18 |- RR C_ CC
380	378, 379	syl6ss 3615	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) C_ CC )
381	295	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> CC C_ CC )
382	202	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) -> X e. CC )
383	380	sselda 3603	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) -> s e. CC )
384	382, 383	addcld 10059	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) -> ( X + s ) e. CC )
385	366, 375, 380, 381, 384	cncfmptssg 40083	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) -cn-> CC ) )
386		eqid 2622	. . . . . . . . . . . . . . . . . 18 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
387		eqid 2622	. . . . . . . . . . . . . . . . . 18 |- ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) )
388	386	cnfldtop 22587	. . . . . . . . . . . . . . . . . . . 20 |- ( TopOpen ` ℂfld ) e. Top
389		unicntop 22589	. . . . . . . . . . . . . . . . . . . . 21 |- CC = U. ( TopOpen ` ℂfld )
390	389	restid 16094	. . . . . . . . . . . . . . . . . . . 20 |- ( ( TopOpen ` ℂfld ) e. Top -> ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld ) )
391	388, 390	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld )
392	391	eqcomi 2631	. . . . . . . . . . . . . . . . . 18 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
393	386, 387, 392	cncfcn 22712	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) C_ CC /\ CC C_ CC ) -> ( ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` ℂfld ) ) )
394	380, 381, 393	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` ℂfld ) ) )
395	385, 394	eleqtrd 2703	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` ℂfld ) ) )
396	386	cnfldtopon 22586	. . . . . . . . . . . . . . . . . 18 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
397	396	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( TopOpen ` ℂfld ) e. (TopOn ` CC ) )
398		resttopon 20965	. . . . . . . . . . . . . . . . 17 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) e. (TopOn ` ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) )
399	397, 380, 398	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) e. (TopOn ` ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) )
400		cncnp 21084	. . . . . . . . . . . . . . . 16 |- ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) e. (TopOn ` ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) /\ ( TopOpen ` ℂfld ) e. (TopOn ` CC ) ) -> ( ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` ℂfld ) ) <-> ( ( 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 ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` t ) ) ) )
401	399, 397, 400	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` ℂfld ) ) <-> ( ( 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 ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` t ) ) ) )
402	395, 401	mpbid 222	. . . . . . . . . . . . . 14 |- ( ( 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 ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` t ) ) )
403	402	simprd 479	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A. t e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` t ) )
404		ubioc1 12227	. . . . . . . . . . . . . 14 |- ( ( ( 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 1326	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` ( i + 1 ) ) e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) )
406		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( t = ( H ` ( i + 1 ) ) -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` t ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` ( i + 1 ) ) ) )
407	406	eleq2d 2687	. . . . . . . . . . . . . 14 |- ( t = ( H ` ( i + 1 ) ) -> ( ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` t ) <-> ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` ( i + 1 ) ) ) ) )
408	407	rspccva 3308	. . . . . . . . . . . . 13 |- ( ( A. t e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` t ) /\ ( H ` ( i + 1 ) ) e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) -> ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` ( i + 1 ) ) ) )
409	403, 405, 408	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` ( i + 1 ) ) ) )
410		snunioo2 39731	. . . . . . . . . . . . . 14 |- ( ( ( 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 1326	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) = ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) )
412	265	eqcomd 2628	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) = ( X + ( H ` ( i + 1 ) ) ) )
413	412	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 4092	. . . . . . . . . . . . . . . 16 |- ( 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 482	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 6658	. . . . . . . . . . . . . . . 16 |- ( s = ( H ` ( i + 1 ) ) -> ( X + s ) = ( X + ( H ` ( i + 1 ) ) ) )
417	416	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 2666	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 4095	. . . . . . . . . . . . . . . 16 |- ( -. 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 482	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 2623	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 6658	. . . . . . . . . . . . . . . . 17 |- ( t = s -> ( X + t ) = ( X + s ) )
423	422	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 4193	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. { ( H ` ( i + 1 ) ) } <-> s = ( H ` ( i + 1 ) ) )
425	424	notbii 310	. . . . . . . . . . . . . . . . . . 19 |- ( -. s e. { ( H ` ( i + 1 ) ) } <-> -. s = ( H ` ( i + 1 ) ) )
426		elun 3753	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 206	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 403	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 392	. . . . . . . . . . . . . . . . . . 19 |- ( 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 233	. . . . . . . . . . . . . . . . . 18 |- ( 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 445	. . . . . . . . . . . . . . . . 17 |- ( ( 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 750	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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	95	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) -> X e. RR )
434		elioore 12205	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) -> s e. RR )
435	434	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) -> s e. RR )
436		elsni 4194	. . . . . . . . . . . . . . . . . . . . . 22 |- ( s e. { ( H ` ( i + 1 ) ) } -> s = ( H ` ( i + 1 ) ) )
437	436	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. { ( H ` ( i + 1 ) ) } ) -> s = ( H ` ( i + 1 ) ) )
438	231	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. { ( H ` ( i + 1 ) ) } ) -> ( H ` ( i + 1 ) ) e. RR )
439	437, 438	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. { ( H ` ( i + 1 ) ) } ) -> s e. RR )
440	435, 439	jaodan 826	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` ( i + 1 ) ) } ) ) -> s e. RR )
441	426, 440	sylan2b 492	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) -> s e. RR )
442	433, 441	readdcld 10069	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) -> ( X + s ) e. RR )
443	442	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 6288	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 2656	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 832	. . . . . . . . . . . . 13 |- ( ( ( 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 4732	. . . . . . . . . . . 12 |- ( ( 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 6666	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) )
449	448	oveq1d 6665	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` ℂfld ) ) = ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) )
450	449	fveq1d 6193	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` ( i + 1 ) ) ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) (,] ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` ( i + 1 ) ) ) )
451	409, 447, 450	3eltr4d 2716	. . . . . . . . . . 11 |- ( ( 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 ` ℂfld ) ↾t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` ( i + 1 ) ) ) )
452		eqid 2622	. . . . . . . . . . . 12 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) )
453		eqid 2622	. . . . . . . . . . . 12 |- ( 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 6057	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) : ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) --> CC )
455	231	recnd 10068	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` ( i + 1 ) ) e. CC )
456	452, 386, 453, 454, 305, 455	ellimc 23637	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` ( i + 1 ) ) e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) lim CC ( 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 ` ℂfld ) ↾t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` ( i + 1 ) ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` ( i + 1 ) ) ) ) )
457	451, 456	mpbird 247	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) lim CC ( H ` ( i + 1 ) ) ) )
458	365, 457, 66	limccog 39852	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) lim CC ( H ` ( i + 1 ) ) ) )
459	272, 292	eqtrd 2656	. . . . . . . . . 10 |- ( ( 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 6665	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) lim CC ( H ` ( i + 1 ) ) ) = ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) lim CC ( H ` ( i + 1 ) ) ) )
461	458, 460	eleqtrd 2703	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> L e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) lim CC ( H ` ( i + 1 ) ) ) )
462	40	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 10172	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> r =/= ( Q ` i ) )
464	463	neneqd 2799	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ r e. ran ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) -> -. r = ( Q ` i ) )
465		velsn 4193	. . . . . . . . . . . . . 14 |- ( r e. { ( Q ` i ) } <-> r = ( Q ` i ) )
466	464, 465	sylnibr 319	. . . . . . . . . . . . 13 |- ( ( ( 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 3585	. . . . . . . . . . . 12 |- ( ( ( 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 2966	. . . . . . . . . . 11 |- ( ( 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 3592	. . . . . . . . . . 11 |- ( 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 224	. . . . . . . . . 10 |- ( ( 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 12254	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( H ` i ) e. RR /\ ( H ` ( i + 1 ) ) e. RR* ) -> ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) C_ RR )
472	230, 251, 471	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) C_ RR )
473	472, 379	syl6ss 3615	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) C_ CC )
474	202	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) -> X e. CC )
475	473	sselda 3603	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) -> s e. CC )
476	474, 475	addcld 10059	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) -> ( X + s ) e. CC )
477	366, 375, 473, 381, 476	cncfmptssg 40083	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) -cn-> CC ) )
478		eqid 2622	. . . . . . . . . . . . . . . . . 18 |- ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
479	386, 478, 392	cncfcn 22712	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) C_ CC /\ CC C_ CC ) -> ( ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` ℂfld ) ) )
480	473, 381, 479	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` ℂfld ) ) )
481	477, 480	eleqtrd 2703	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` ℂfld ) ) )
482		resttopon 20965	. . . . . . . . . . . . . . . . 17 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) e. (TopOn ` ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) )
483	397, 473, 482	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) e. (TopOn ` ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) )
484		cncnp 21084	. . . . . . . . . . . . . . . 16 |- ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) e. (TopOn ` ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) /\ ( TopOpen ` ℂfld ) e. (TopOn ` CC ) ) -> ( ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` ℂfld ) ) <-> ( ( 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 ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` t ) ) ) )
485	483, 397, 484	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) Cn ( TopOpen ` ℂfld ) ) <-> ( ( 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 ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` t ) ) ) )
486	481, 485	mpbid 222	. . . . . . . . . . . . . 14 |- ( ( 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 ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` t ) ) )
487	486	simprd 479	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> A. t e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` t ) )
488		lbico1 12228	. . . . . . . . . . . . . 14 |- ( ( ( 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 1326	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` i ) e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
490		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( t = ( H ` i ) -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` t ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` i ) ) )
491	490	eleq2d 2687	. . . . . . . . . . . . . 14 |- ( t = ( H ` i ) -> ( ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` t ) <-> ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` i ) ) ) )
492	491	rspccva 3308	. . . . . . . . . . . . 13 |- ( ( A. t e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` t ) /\ ( H ` i ) e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) -> ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` i ) ) )
493	487, 489, 492	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( s e. ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) |-> ( X + s ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` i ) ) )
494		uncom 3757	. . . . . . . . . . . . . 14 |- ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) = ( { ( H ` i ) } u. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
495		snunioo 12298	. . . . . . . . . . . . . . 15 |- ( ( ( 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 1326	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( { ( H ` i ) } u. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) = ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
497	494, 496	syl5eq 2668	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) = ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) )
498		iftrue 4092	. . . . . . . . . . . . . . . . 17 |- ( s = ( H ` i ) -> if ( s = ( H ` i ) , ( Q ` i ) , ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ` s ) ) = ( Q ` i ) )
499	498	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s = ( H ` i ) ) -> ( Q ` i ) = ( X + ( H ` i ) ) )
501		oveq2 6658	. . . . . . . . . . . . . . . . . 18 |- ( s = ( H ` i ) -> ( X + s ) = ( X + ( H ` i ) ) )
502	501	eqcomd 2628	. . . . . . . . . . . . . . . . 17 |- ( s = ( H ` i ) -> ( X + ( H ` i ) ) = ( X + s ) )
503	502	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s = ( H ` i ) ) -> ( X + ( H ` i ) ) = ( X + s ) )
504	499, 500, 503	3eqtrd 2660	. . . . . . . . . . . . . . 15 |- ( ( ( 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 751	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 4095	. . . . . . . . . . . . . . . 16 |- ( -. 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 482	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 2623	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 482	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 4193	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. { ( H ` i ) } <-> s = ( H ` i ) )
511	510	notbii 310	. . . . . . . . . . . . . . . . . . 19 |- ( -. s e. { ( H ` i ) } <-> -. s = ( H ` i ) )
512		elun 3753	. . . . . . . . . . . . . . . . . . . . . 22 |- ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) <-> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` i ) } ) )
513	512	biimpi 206	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) -> ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` i ) } ) )
514	513	orcomd 403	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) -> ( s e. { ( H ` i ) } \/ s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) )
515	514	ord 392	. . . . . . . . . . . . . . . . . . 19 |- ( 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 233	. . . . . . . . . . . . . . . . . 18 |- ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) -> ( -. s = ( H ` i ) -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) ) )
517	516	imp 445	. . . . . . . . . . . . . . . . 17 |- ( ( s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) /\ -. s = ( H ` i ) ) -> s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) )
518	517	adantll 750	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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	95	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) -> X e. RR )
520		elsni 4194	. . . . . . . . . . . . . . . . . . . . . 22 |- ( s e. { ( H ` i ) } -> s = ( H ` i ) )
521	520	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. { ( H ` i ) } ) -> s = ( H ` i ) )
522	230	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. { ( H ` i ) } ) -> ( H ` i ) e. RR )
523	521, 522	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. { ( H ` i ) } ) -> s e. RR )
524	435, 523	jaodan 826	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ ( s e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) \/ s e. { ( H ` i ) } ) ) -> s e. RR )
525	512, 524	sylan2b 492	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) -> s e. RR )
526	519, 525	readdcld 10069	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ s e. ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) -> ( X + s ) e. RR )
527	526	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 6288	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 2656	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 832	. . . . . . . . . . . . 13 |- ( ( ( 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 4732	. . . . . . . . . . . 12 |- ( ( 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 6666	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) )
533	532	oveq1d 6665	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) = ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) )
534	533	fveq1d 6193	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` i ) ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( H ` i ) [,) ( H ` ( i + 1 ) ) ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` i ) ) )
535	493, 531, 534	3eltr4d 2716	. . . . . . . . . . 11 |- ( ( 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 ` ℂfld ) ↾t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` i ) ) )
536		eqid 2622	. . . . . . . . . . . 12 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) )
537		eqid 2622	. . . . . . . . . . . 12 |- ( 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 10068	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( H ` i ) e. CC )
539	536, 386, 537, 454, 305, 538	ellimc 23637	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( Q ` i ) e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) lim CC ( 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 ` ℂfld ) ↾t ( ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) u. { ( H ` i ) } ) ) CnP ( TopOpen ` ℂfld ) ) ` ( H ` i ) ) ) )
540	535, 539	mpbird 247	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) lim CC ( H ` i ) ) )
541	470, 540, 69	limccog 39852	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) lim CC ( H ` i ) ) )
542	459	oveq1d 6665	. . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) o. ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( X + t ) ) ) lim CC ( H ` i ) ) = ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) lim CC ( H ` i ) ) )
543	541, 542	eleqtrd 2703	. . . . . . . 8 |- ( ( ph /\ i e. ( 0..^ M ) ) -> R e. ( ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) lim CC ( H ` i ) ) )
544	230, 231, 310, 461, 543	iblcncfioo 40194	. . . . . . 7 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( H ` i ) (,) ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) e. L^1 )
545	30	ad2antrr 762	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> F : ( -u pi [,] pi ) --> CC )
546	49	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> -u pi e. RR* )
547	51	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> pi e. RR* )
548	21	ad2antrr 762	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( -u pi [,] pi ) )
549		simplr 792	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> i e. ( 0..^ M ) )
550		simpr 477	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) )
551	169, 179	oveq12d 6668	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) = ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) )
552	551	adantr 481	. . . . . . . . . . 11 |- ( ( ( 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 2703	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> t e. ( ( ( Q ` i ) - X ) [,] ( ( Q ` ( i + 1 ) ) - X ) ) )
554	553, 116	syldan 487	. . . . . . . . 9 |- ( ( ( 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 40325	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> ( X + t ) e. ( -u pi [,] pi ) )
556	545, 555	ffvelrnd 6360	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0..^ M ) ) /\ t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) ) -> ( F ` ( X + t ) ) e. CC )
557	230, 231, 544, 556	ibliooicc 40187	. . . . . 6 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( t e. ( ( H ` i ) [,] ( H ` ( i + 1 ) ) ) |-> ( F ` ( X + t ) ) ) e. L^1 )
558	14, 20, 165, 180, 229, 557	itgspltprt 40195	. . . . 5 |- ( 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 40172	. . . . . 6 |- ( ( 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 14433	. . . . 5 |- ( 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 2656	. . . 4 |- ( 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	125, 161, 561	3eqtrd 2660	. . 3 |- ( 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	121, 562	eqtr4d 2659	. 2 |- ( 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	13, 76, 563	3eqtrd 2660	1 |- ( ph -> S. ( -u pi [,] pi ) ( F ` t ) _d t = S. ( ( -u pi - X ) [,] ( pi - X ) ) ( F ` ( X + s ) ) _d s )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   ifcif 4086   {csn 4177   class class class wbr 4653   |-> cmpt 4729   dom cdm 5114   ran crn 5115   |` cres 5116   o. ccom 5118   Fun wfun 5882   -->wf 5884   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   -ucneg 10267   NNcn 11020   ZZcz 11377   ZZ>=cuz 11687   (,)cioo 12175   (,]cioc 12176   [,)cico 12177   [,]cicc 12178   ...cfz 12326  ..^cfzo 12465   sum_csu 14416   picpi 14797   ↾_t crest 16081   TopOpenctopn 16082  ℂ_fldccnfld 19746   Topctop 20698  TopOnctopon 20715   Cn ccn 21028   CnP ccnp 21029   -cn->ccncf 22679   S.citg 23387   lim CC climc 23626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cc 9257  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-disj 4621  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-ofr 6898  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-omul 7565  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-acn 8768  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ioc 12180  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-fac 13061  df-bc 13090  df-hash 13118  df-shft 13807  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-limsup 14202  df-clim 14219  df-rlim 14220  df-sum 14417  df-ef 14798  df-sin 14800  df-cos 14801  df-pi 14803  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-xrs 16162  df-qtop 16167  df-imas 16168  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-submnd 17336  df-mulg 17541  df-cntz 17750  df-cmn 18195  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-lp 20940  df-perf 20941  df-cn 21031  df-cnp 21032  df-haus 21119  df-cmp 21190  df-tx 21365  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-xms 22125  df-ms 22126  df-tms 22127  df-cncf 22681  df-ovol 23233  df-vol 23234  df-mbf 23388  df-itg1 23389  df-itg2 23390  df-ibl 23391  df-itg 23392  df-0p 23437  df-ditg 23611  df-limc 23630  df-dv 23631

This theorem is referenced by:  fourierdlem101  40424