Theorem fourierdlem101

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

	Ref	Expression
Hypotheses	fourierdlem101.d	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
	fourierdlem101.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
	fourierdlem101.g	⊢ 𝐺 = ( 𝑡 ∈ ( - π [,] π ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
	fourierdlem101.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
	fourierdlem101.6	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	fourierdlem101.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	fourierdlem101.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	fourierdlem101.f	⊢ ( 𝜑 → 𝐹 : ( - π [,] π ) ⟶ ℂ )
	fourierdlem101.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
	fourierdlem101.r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
	fourierdlem101.l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
Assertion	fourierdlem101	⊢ ( 𝜑 → ∫ ( - π [,] π ) ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) d 𝑡 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) d 𝑠 )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem101.d	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
2		fourierdlem101.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
3		fourierdlem101.g	⊢ 𝐺 = ( 𝑡 ∈ ( - π [,] π ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
4		fourierdlem101.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
5		fourierdlem101.6	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
6		fourierdlem101.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7		fourierdlem101.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
8		fourierdlem101.f	⊢ ( 𝜑 → 𝐹 : ( - π [,] π ) ⟶ ℂ )
9		fourierdlem101.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
10		fourierdlem101.r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
11		fourierdlem101.l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → 𝑡 ∈ ( - π [,] π ) )
13	8	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
14	6	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → 𝑁 ∈ ℕ )
15		pire	⊢ π ∈ ℝ
16	15	renegcli	⊢ - π ∈ ℝ
17		eliccre	⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ∧ 𝑡 ∈ ( - π [,] π ) ) → 𝑡 ∈ ℝ )
18	16 15 17	mp3an12	⊢ ( 𝑡 ∈ ( - π [,] π ) → 𝑡 ∈ ℝ )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → 𝑡 ∈ ℝ )
20	7	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → 𝑋 ∈ ℝ )
21	19 20	resubcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
22	1	dirkerre	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑡 − 𝑋 ) ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
23	14 21 22	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
24	23	recnd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℂ )
25	13 24	mulcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ℂ )
26	3	fvmpt2	⊢ ( ( 𝑡 ∈ ( - π [,] π ) ∧ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ℂ ) → ( 𝐺 ‘ 𝑡 ) = ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
27	12 25 26	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( 𝐺 ‘ 𝑡 ) = ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
28	27	eqcomd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( - π [,] π ) ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( 𝐺 ‘ 𝑡 ) )
29	28	itgeq2dv	⊢ ( 𝜑 → ∫ ( - π [,] π ) ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) d 𝑡 = ∫ ( - π [,] π ) ( 𝐺 ‘ 𝑡 ) d 𝑡 )
30		fveq2	⊢ ( 𝑗 = 𝑖 → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) )
31	30	oveq1d	⊢ ( 𝑗 = 𝑖 → ( ( 𝑄 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) )
32	31	cbvmptv	⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑗 ) − 𝑋 ) ) = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) )
33	25 3	fmptd	⊢ ( 𝜑 → 𝐺 : ( - π [,] π ) ⟶ ℂ )
34	3	reseq1i	⊢ ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑡 ∈ ( - π [,] π ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
35		ioossicc	⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
36	16	a1i	⊢ ( 𝜑 → - π ∈ ℝ )
37	36	rexrd	⊢ ( 𝜑 → - π ∈ ℝ* )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → - π ∈ ℝ* )
39	15	a1i	⊢ ( 𝜑 → π ∈ ℝ )
40	39	rexrd	⊢ ( 𝜑 → π ∈ ℝ* )
41	40	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → π ∈ ℝ* )
42	2 5 4	fourierdlem15	⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
43	42	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
44		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
45	38 41 43 44	fourierdlem8	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
46	35 45	sstrid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
47	46	resmptd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( - π [,] π ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) )
48	34 47	eqtrid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) )
49	8	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 : ( - π [,] π ) ⟶ ℂ )
50	49 46	feqresmpt	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ 𝑡 ) ) )
51	50 9	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
52		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) = ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) )
53		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) → 𝑠 = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) )
54		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) )
55		oveq1	⊢ ( 𝑡 = 𝑟 → ( 𝑡 − 𝑋 ) = ( 𝑟 − 𝑋 ) )
56	55	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑡 = 𝑟 ) → ( 𝑡 − 𝑋 ) = ( 𝑟 − 𝑋 ) )
57		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
58		elioore	⊢ ( 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑟 ∈ ℝ )
59	58	adantl	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑟 ∈ ℝ )
60	7	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
61	59 60	resubcld	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑟 − 𝑋 ) ∈ ℝ )
62	61	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑟 − 𝑋 ) ∈ ℝ )
63	54 56 57 62	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) = ( 𝑟 − 𝑋 ) )
64	63	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) = ( 𝑟 − 𝑋 ) )
65	53 64	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) → 𝑠 = ( 𝑟 − 𝑋 ) )
66	65	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) )
67		elioore	⊢ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑡 ∈ ℝ )
68	67	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ℝ )
69	7	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
70	68 69	resubcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
71	70	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
72		eqid	⊢ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) )
73	71 72	fmptd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
74	73	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ∈ ℝ )
75	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑁 ∈ ℕ )
76	1	dirkerre	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑟 − 𝑋 ) ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) ∈ ℝ )
77	75 62 76	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) ∈ ℝ )
78	52 66 74 77	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ‘ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) )
79	78	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) = ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ‘ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) )
80	79	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) ) = ( 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ‘ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) ) )
81	55	fveq2d	⊢ ( 𝑡 = 𝑟 → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) )
82	81	cbvmptv	⊢ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) )
83	82	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑟 − 𝑋 ) ) ) )
84	1	dirkerre	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑠 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ∈ ℝ )
85	6 84	sylan	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ∈ ℝ )
86		eqid	⊢ ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) = ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) )
87	85 86	fmptd	⊢ ( 𝜑 → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) : ℝ ⟶ ℝ )
88	87	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) : ℝ ⟶ ℝ )
89		fcompt	⊢ ( ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) : ℝ ⟶ ℝ ∧ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ ) → ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∘ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ) = ( 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ‘ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) ) )
90	88 73 89	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∘ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ) = ( 𝑟 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ‘ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ‘ 𝑟 ) ) ) )
91	80 83 90	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∘ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ) )
92		eqid	⊢ ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) ) = ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) )
93		simpr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → 𝑡 ∈ ℂ )
94	7	recnd	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
95	94	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → 𝑋 ∈ ℂ )
96	93 95	negsubd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( 𝑡 + - 𝑋 ) = ( 𝑡 − 𝑋 ) )
97	96	eqcomd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℂ ) → ( 𝑡 − 𝑋 ) = ( 𝑡 + - 𝑋 ) )
98	97	mpteq2dva	⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) ) = ( 𝑡 ∈ ℂ ↦ ( 𝑡 + - 𝑋 ) ) )
99	94	negcld	⊢ ( 𝜑 → - 𝑋 ∈ ℂ )
100		eqid	⊢ ( 𝑡 ∈ ℂ ↦ ( 𝑡 + - 𝑋 ) ) = ( 𝑡 ∈ ℂ ↦ ( 𝑡 + - 𝑋 ) )
101	100	addccncf	⊢ ( - 𝑋 ∈ ℂ → ( 𝑡 ∈ ℂ ↦ ( 𝑡 + - 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
102	99 101	syl	⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ ( 𝑡 + - 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
103	98 102	eqeltrd	⊢ ( 𝜑 → ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
104	103	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ℂ ↦ ( 𝑡 − 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
105		ioossre	⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
106		ax-resscn	⊢ ℝ ⊆ ℂ
107	105 106	sstri	⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ
108	107	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
109	106	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ℝ ⊆ ℂ )
110	92 104 108 109 71	cncfmptssg	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℝ ) )
111	85	recnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ∈ ℂ )
112	111 86	fmptd	⊢ ( 𝜑 → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) : ℝ ⟶ ℂ )
113		ssid	⊢ ℂ ⊆ ℂ
114	1	dirkerf	⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
115	6 114	syl	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
116	115	feqmptd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) = ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) )
117	1	dirkercncf	⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) ∈ ( ℝ –cn→ ℝ ) )
118	6 117	syl	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) ∈ ( ℝ –cn→ ℝ ) )
119	116 118	eqeltrrd	⊢ ( 𝜑 → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ( ℝ –cn→ ℝ ) )
120		cncfcdm	⊢ ( ( ℂ ⊆ ℂ ∧ ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ( ℝ –cn→ ℝ ) ) → ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ( ℝ –cn→ ℂ ) ↔ ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) : ℝ ⟶ ℂ ) )
121	113 119 120	sylancr	⊢ ( 𝜑 → ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ( ℝ –cn→ ℂ ) ↔ ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) : ℝ ⟶ ℂ ) )
122	112 121	mpbird	⊢ ( 𝜑 → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ( ℝ –cn→ ℂ ) )
123	122	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ( ℝ –cn→ ℂ ) )
124	110 123	cncfco	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑠 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∘ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
125	91 124	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
126	51 125	mulcncf	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
127	48 126	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
128		cncff	⊢ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
129	9 128	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
130	115	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
131		elioore	⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ℝ )
132	131	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
133	7	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
134	132 133	resubcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑠 − 𝑋 ) ∈ ℝ )
135	130 134	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ∈ ℝ )
136	135	recnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ∈ ℂ )
137		eqid	⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) )
138	136 137	fmptd	⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
139	138	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
140		eqid	⊢ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) )
141		oveq1	⊢ ( 𝑡 = ( 𝑄 ‘ 𝑖 ) → ( 𝑡 − 𝑋 ) = ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) )
142	141	fveq2d	⊢ ( 𝑡 = ( 𝑄 ‘ 𝑖 ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) )
143	142	eqcomd	⊢ ( 𝑡 = ( 𝑄 ‘ 𝑖 ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
144	143	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
145		eqidd	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) )
146		oveq1	⊢ ( 𝑠 = 𝑡 → ( 𝑠 − 𝑋 ) = ( 𝑡 − 𝑋 ) )
147	146	fveq2d	⊢ ( 𝑠 = 𝑡 → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
148	147	adantl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) ∧ 𝑠 = 𝑡 ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
149		velsn	⊢ ( 𝑡 ∈ { ( 𝑄 ‘ 𝑖 ) } ↔ 𝑡 = ( 𝑄 ‘ 𝑖 ) )
150	149	notbii	⊢ ( ¬ 𝑡 ∈ { ( 𝑄 ‘ 𝑖 ) } ↔ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) )
151		elunnel2	⊢ ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ∧ ¬ 𝑡 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
152	150 151	sylan2br	⊢ ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ∧ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
153	152	adantll	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
154	115	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
155		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → 𝑡 = ( 𝑄 ‘ 𝑖 ) )
156	18	ssriv	⊢ ( - π [,] π ) ⊆ ℝ
157		fzossfz	⊢ ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 )
158	157 44	sselid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
159	43 158	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( - π [,] π ) )
160	156 159	sselid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
161	160	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
162	155 161	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → 𝑡 ∈ ℝ )
163	162	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → 𝑡 ∈ ℝ )
164	153 67	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → 𝑡 ∈ ℝ )
165	163 164	pm2.61dan	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑡 ∈ ℝ )
166	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑋 ∈ ℝ )
167	165 166	resubcld	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
168	154 167	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
169	168	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
170	145 148 153 169	fvmptd	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ 𝑖 ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
171	144 170	ifeqda	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
172	171	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
173	115	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
174		simpr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) )
175		elun	⊢ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↔ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) )
176	174 175	sylib	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) )
177	176	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) )
178		elsni	⊢ ( 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } → 𝑠 = ( 𝑄 ‘ 𝑖 ) )
179	178	adantl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → 𝑠 = ( 𝑄 ‘ 𝑖 ) )
180	160	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
181	179 180	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → 𝑠 ∈ ℝ )
182	181	ex	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } → 𝑠 ∈ ℝ ) )
183	182	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } → 𝑠 ∈ ℝ ) )
184		pm3.44	⊢ ( ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ℝ ) ∧ ( 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } → 𝑠 ∈ ℝ ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → 𝑠 ∈ ℝ ) )
185	131 183 184	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑠 ∈ { ( 𝑄 ‘ 𝑖 ) } ) → 𝑠 ∈ ℝ ) )
186	177 185	mpd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑠 ∈ ℝ )
187	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑋 ∈ ℝ )
188	186 187	resubcld	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑠 − 𝑋 ) ∈ ℝ )
189		eqid	⊢ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) = ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) )
190	188 189	fmptd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⟶ ℝ )
191		fcompt	⊢ ( ( ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ ∧ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⟶ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) ) ) )
192	173 190 191	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) ) ) )
193		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) = ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) )
194	146	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ 𝑠 = 𝑡 ) → ( 𝑠 − 𝑋 ) = ( 𝑡 − 𝑋 ) )
195		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) )
196	193 194 195 167	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) = ( 𝑡 − 𝑋 ) )
197	196	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
198	197	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
199	192 198	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) )
200		eqid	⊢ ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) )
201		simpr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → 𝑠 ∈ ℂ )
202	94	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → 𝑋 ∈ ℂ )
203	201 202	negsubd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → ( 𝑠 + - 𝑋 ) = ( 𝑠 − 𝑋 ) )
204	203	eqcomd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℂ ) → ( 𝑠 − 𝑋 ) = ( 𝑠 + - 𝑋 ) )
205	204	mpteq2dva	⊢ ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) ) )
206		eqid	⊢ ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) ) = ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) )
207	206	addccncf	⊢ ( - 𝑋 ∈ ℂ → ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
208	99 207	syl	⊢ ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑠 + - 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
209	205 208	eqeltrd	⊢ ( 𝜑 → ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
210	209	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ℂ ↦ ( 𝑠 − 𝑋 ) ) ∈ ( ℂ –cn→ ℂ ) )
211	160	recnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℂ )
212	211	snssd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { ( 𝑄 ‘ 𝑖 ) } ⊆ ℂ )
213	108 212	unssd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⊆ ℂ )
214	200 210 213 109 188	cncfmptssg	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ∈ ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) –cn→ ℝ ) )
215	116 122	eqeltrd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) ∈ ( ℝ –cn→ ℂ ) )
216	215	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐷 ‘ 𝑁 ) ∈ ( ℝ –cn→ ℂ ) )
217	214 216	cncfco	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) ∈ ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) –cn→ ℂ ) )
218		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
219		eqid	⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) )
220	218	cnfldtop	⊢ ( TopOpen ‘ ℂfld ) ∈ Top
221		unicntop	⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
222	221	restid	⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
223	220 222	ax-mp	⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
224	223	eqcomi	⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
225	218 219 224	cncfcn	⊢ ( ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
226	213 113 225	sylancl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
227	217 226	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ∘ ( 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( 𝑠 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
228	199 227	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
229	218	cnfldtopon	⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
230		resttopon	⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) )
231	229 213 230	sylancr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) )
232		cncnp	⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) ) )
233	231 229 232	sylancl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) ) )
234	228 233	mpbid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) )
235	234	simprd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) )
236		eqidd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑖 ) )
237		elsng	⊢ ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ → ( ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } ↔ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑖 ) ) )
238	160 237	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } ↔ ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑖 ) ) )
239	236 238	mpbird	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } )
240	239	olcd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } ) )
241		elun	⊢ ( ( 𝑄 ‘ 𝑖 ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↔ ( ( 𝑄 ‘ 𝑖 ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ ( 𝑄 ‘ 𝑖 ) ∈ { ( 𝑄 ‘ 𝑖 ) } ) )
242	240 241	sylibr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) )
243		fveq2	⊢ ( 𝑠 = ( 𝑄 ‘ 𝑖 ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) )
244	243	eleq2d	⊢ ( 𝑠 = ( 𝑄 ‘ 𝑖 ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ↔ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) ) )
245	244	rspccva	⊢ ( ( ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ∧ ( 𝑄 ‘ 𝑖 ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) )
246	235 242 245	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) )
247	172 246	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) )
248		eqid	⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) )
249	219 218 248 139 108 211	ellimc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ↔ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ 𝑖 ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ 𝑖 ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ 𝑖 ) ) ) )
250	247 249	mpbird	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
251	129 139 140 10 250	mullimcf	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑅 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ) ∈ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
252		fvres	⊢ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) = ( 𝐹 ‘ 𝑡 ) )
253	252	adantl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) = ( 𝐹 ‘ 𝑡 ) )
254	253	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) )
255	254	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) )
256	255	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
257	251 256	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑅 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ) ∈ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
258		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) )
259		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = 𝑡 ) → 𝑠 = 𝑡 )
260	259	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = 𝑡 ) → ( 𝑠 − 𝑋 ) = ( 𝑡 − 𝑋 ) )
261	260	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑠 = 𝑡 ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
262		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
263	115	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
264	263 71	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
265	258 261 262 264	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
266	265	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
267	266	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) )
268	267	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
269	257 268	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑅 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ) ∈ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
270	48	eqcomd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) = ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
271	270	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
272	269 271	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑅 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ 𝑖 ) − 𝑋 ) ) ) ∈ ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
273		iftrue	⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
274		oveq1	⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( 𝑡 − 𝑋 ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
275	274	eqcomd	⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) = ( 𝑡 − 𝑋 ) )
276	275	fveq2d	⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
277	273 276	eqtrd	⊢ ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
278	277	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
279		iffalse	⊢ ( ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) )
280	279	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) )
281		eqidd	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) )
282	147	adantl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 = 𝑡 ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
283		elun	⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↔ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
284	283	biimpi	⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
285	284	orcomd	⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ∨ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
286	285	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ∨ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
287		velsn	⊢ ( 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ↔ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
288	287	notbii	⊢ ( ¬ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ↔ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
289	288	biimpri	⊢ ( ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ¬ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } )
290	289	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ¬ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } )
291		pm2.53	⊢ ( ( 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ∨ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ¬ 𝑡 ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
292	286 290 291	sylc	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
293	173	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
294	292 67	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑡 ∈ ℝ )
295	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑋 ∈ ℝ )
296	294 295	resubcld	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
297	293 296	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
298	281 282 292 297	fvmptd	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
299	280 298	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ¬ 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
300	278 299	pm2.61dan	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
301	300	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
302		eqid	⊢ ( 𝑡 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) )
303	106	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
304		simpr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℝ )
305	7	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → 𝑋 ∈ ℝ )
306	304 305	resubcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
307	92 103 303 303 306	cncfmptssg	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( 𝑡 − 𝑋 ) ) ∈ ( ℝ –cn→ ℝ ) )
308	307 215	cncfcompt	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ℝ –cn→ ℂ ) )
309	308	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ℝ ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ℝ –cn→ ℂ ) )
310	105	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
311		fzofzp1	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
312	311	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
313	43 312	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( - π [,] π ) )
314	156 313	sselid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
315	314	snssd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ⊆ ℝ )
316	310 315	unssd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⊆ ℝ )
317	113	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ℂ ⊆ ℂ )
318	173	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )
319	316	sselda	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → 𝑡 ∈ ℝ )
320	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → 𝑋 ∈ ℝ )
321	319 320	resubcld	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → ( 𝑡 − 𝑋 ) ∈ ℝ )
322	318 321	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℝ )
323	322	recnd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ∈ ℂ )
324	302 309 316 317 323	cncfmptssg	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) –cn→ ℂ ) )
325	156 106	sstri	⊢ ( - π [,] π ) ⊆ ℂ
326	325 313	sselid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
327	326	snssd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ⊆ ℂ )
328	108 327	unssd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⊆ ℂ )
329		eqid	⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
330	218 329 224	cncfcn	⊢ ( ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
331	328 113 330	sylancl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
332	324 331	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
333		resttopon	⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) )
334	229 328 333	sylancr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) )
335		cncnp	⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∈ ( TopOn ‘ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) ) )
336	334 229 335	sylancl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) ) )
337	332 336	mpbid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) : ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ⟶ ℂ ∧ ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ) )
338	337	simprd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) )
339		eqidd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
340		elsng	⊢ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ↔ ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
341	314 340	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ↔ ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
342	339 341	mpbird	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } )
343	342	olcd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
344		elun	⊢ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↔ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∨ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
345	343 344	sylibr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
346		fveq2	⊢ ( 𝑠 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
347	346	eleq2d	⊢ ( 𝑠 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ↔ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
348	347	rspccva	⊢ ( ( ∀ 𝑠 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑠 ) ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
349	338 345 348	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
350	301 349	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
351		eqid	⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) )
352	329 218 351 139 108 326	ellimc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ↦ if ( 𝑡 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
353	350 352	mpbird	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
354	129 139 140 11 353	mullimcf	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐿 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) ∈ ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
355	267 255 48	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) = ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
356	355	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) · ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑠 − 𝑋 ) ) ) ‘ 𝑡 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
357	354 356	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐿 · ( ( 𝐷 ‘ 𝑁 ) ‘ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) ) ∈ ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
358	2 32 5 4 7 33 127 272 357	fourierdlem93	⊢ ( 𝜑 → ∫ ( - π [,] π ) ( 𝐺 ‘ 𝑡 ) d 𝑡 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐺 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 )
359	3	a1i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝐺 = ( 𝑡 ∈ ( - π [,] π ) ↦ ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) ) )
360		fveq2	⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
361	360	oveq1d	⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
362	361	adantl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) )
363		oveq1	⊢ ( 𝑡 = ( 𝑋 + 𝑠 ) → ( 𝑡 − 𝑋 ) = ( ( 𝑋 + 𝑠 ) − 𝑋 ) )
364	94	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑋 ∈ ℂ )
365	36 7	resubcld	⊢ ( 𝜑 → ( - π − 𝑋 ) ∈ ℝ )
366	365	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( - π − 𝑋 ) ∈ ℝ )
367	39 7	resubcld	⊢ ( 𝜑 → ( π − 𝑋 ) ∈ ℝ )
368	367	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( π − 𝑋 ) ∈ ℝ )
369		simpr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) )
370		eliccre	⊢ ( ( ( - π − 𝑋 ) ∈ ℝ ∧ ( π − 𝑋 ) ∈ ℝ ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ∈ ℝ )
371	366 368 369 370	syl3anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ∈ ℝ )
372	371	recnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ∈ ℂ )
373	364 372	pncan2d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( ( 𝑋 + 𝑠 ) − 𝑋 ) = 𝑠 )
374	363 373	sylan9eqr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( 𝑡 − 𝑋 ) = 𝑠 )
375	374	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) = ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) )
376	375	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) )
377	362 376	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) ∧ 𝑡 = ( 𝑋 + 𝑠 ) ) → ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) )
378	16	a1i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → - π ∈ ℝ )
379	15	a1i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → π ∈ ℝ )
380	7	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑋 ∈ ℝ )
381	380 371	readdcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
382	36	recnd	⊢ ( 𝜑 → - π ∈ ℂ )
383	94 382	pncan3d	⊢ ( 𝜑 → ( 𝑋 + ( - π − 𝑋 ) ) = - π )
384	383	eqcomd	⊢ ( 𝜑 → - π = ( 𝑋 + ( - π − 𝑋 ) ) )
385	384	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → - π = ( 𝑋 + ( - π − 𝑋 ) ) )
386		elicc2	⊢ ( ( ( - π − 𝑋 ) ∈ ℝ ∧ ( π − 𝑋 ) ∈ ℝ ) → ( 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ↔ ( 𝑠 ∈ ℝ ∧ ( - π − 𝑋 ) ≤ 𝑠 ∧ 𝑠 ≤ ( π − 𝑋 ) ) ) )
387	366 368 386	syl2anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ↔ ( 𝑠 ∈ ℝ ∧ ( - π − 𝑋 ) ≤ 𝑠 ∧ 𝑠 ≤ ( π − 𝑋 ) ) ) )
388	369 387	mpbid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑠 ∈ ℝ ∧ ( - π − 𝑋 ) ≤ 𝑠 ∧ 𝑠 ≤ ( π − 𝑋 ) ) )
389	388	simp2d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( - π − 𝑋 ) ≤ 𝑠 )
390	366 371 380 389	leadd2dd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + ( - π − 𝑋 ) ) ≤ ( 𝑋 + 𝑠 ) )
391	385 390	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → - π ≤ ( 𝑋 + 𝑠 ) )
392	388	simp3d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝑠 ≤ ( π − 𝑋 ) )
393	371 368 380 392	leadd2dd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ≤ ( 𝑋 + ( π − 𝑋 ) ) )
394		picn	⊢ π ∈ ℂ
395	394	a1i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → π ∈ ℂ )
396	364 395	pncan3d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + ( π − 𝑋 ) ) = π )
397	393 396	breqtrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ≤ π )
398	378 379 381 391 397	eliccd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝑋 + 𝑠 ) ∈ ( - π [,] π ) )
399	8	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → 𝐹 : ( - π [,] π ) ⟶ ℂ )
400	399 398	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
401	371 111	syldan	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ∈ ℂ )
402	400 401	mulcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) ∈ ℂ )
403	359 377 398 402	fvmptd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ) → ( 𝐺 ‘ ( 𝑋 + 𝑠 ) ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) )
404	403	itgeq2dv	⊢ ( 𝜑 → ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( 𝐺 ‘ ( 𝑋 + 𝑠 ) ) d 𝑠 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) d 𝑠 )
405	29 358 404	3eqtrd	⊢ ( 𝜑 → ∫ ( - π [,] π ) ( ( 𝐹 ‘ 𝑡 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑡 − 𝑋 ) ) ) d 𝑡 = ∫ ( ( - π − 𝑋 ) [,] ( π − 𝑋 ) ) ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) · ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑠 ) ) d 𝑠 )