Theorem fourierdlem80

Description: The derivative of O is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem80.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
	fourierdlem80.xre	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	fourierdlem80.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	fourierdlem80.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	fourierdlem80.ab	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
	fourierdlem80.n0	⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
	fourierdlem80.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	fourierdlem80.o	⊢ 𝑂 = ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
	fourierdlem80.i	⊢ 𝐼 = ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
	fourierdlem80.fbdioo	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 )
	fourierdlem80.fdvbdioo	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 )
	fourierdlem80.sf	⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐴 [,] 𝐵 ) )
	fourierdlem80.slt	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
	fourierdlem80.sjss	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
	fourierdlem80.relioo	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑟 ∈ ran 𝑆 ) → ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑟 ∈ ( ( 𝑆 ‘ 𝑘 ) (,) ( 𝑆 ‘ ( 𝑘 + 1 ) ) ) )
	fdv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝐹 ↾ 𝐼 ) ) : 𝐼 ⟶ ℝ )
	fourierdlem80.y	⊢ 𝑌 = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
	fourierdlem80.ch	⊢ ( 𝜒 ↔ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) )
Assertion	fourierdlem80	⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ dom ( ℝ D 𝑂 ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑏 )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem80.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2		fourierdlem80.xre	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3		fourierdlem80.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4		fourierdlem80.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5		fourierdlem80.ab	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
6		fourierdlem80.n0	⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
7		fourierdlem80.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
8		fourierdlem80.o	⊢ 𝑂 = ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
9		fourierdlem80.i	⊢ 𝐼 = ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
10		fourierdlem80.fbdioo	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 )
11		fourierdlem80.fdvbdioo	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 )
12		fourierdlem80.sf	⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐴 [,] 𝐵 ) )
13		fourierdlem80.slt	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
14		fourierdlem80.sjss	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
15		fourierdlem80.relioo	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑟 ∈ ran 𝑆 ) → ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑟 ∈ ( ( 𝑆 ‘ 𝑘 ) (,) ( 𝑆 ‘ ( 𝑘 + 1 ) ) ) )
16		fdv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝐹 ↾ 𝐼 ) ) : 𝐼 ⟶ ℝ )
17		fourierdlem80.y	⊢ 𝑌 = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
18		fourierdlem80.ch	⊢ ( 𝜒 ↔ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) )
19		oveq2	⊢ ( 𝑠 = 𝑡 → ( 𝑋 + 𝑠 ) = ( 𝑋 + 𝑡 ) )
20	19	fveq2d	⊢ ( 𝑠 = 𝑡 → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) )
21	20	oveq1d	⊢ ( 𝑠 = 𝑡 → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) = ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) )
22		oveq1	⊢ ( 𝑠 = 𝑡 → ( 𝑠 / 2 ) = ( 𝑡 / 2 ) )
23	22	fveq2d	⊢ ( 𝑠 = 𝑡 → ( sin ‘ ( 𝑠 / 2 ) ) = ( sin ‘ ( 𝑡 / 2 ) ) )
24	23	oveq2d	⊢ ( 𝑠 = 𝑡 → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) = ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) )
25	21 24	oveq12d	⊢ ( 𝑠 = 𝑡 → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) )
26	25	cbvmptv	⊢ ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) )
27	8 26	eqtr2i	⊢ ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) = 𝑂
28	27	oveq2i	⊢ ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) = ( ℝ D 𝑂 )
29	28	dmeqi	⊢ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) = dom ( ℝ D 𝑂 )
30	29	ineq2i	⊢ ( ran 𝑆 ∩ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) ) = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) )
31	30	sneqi	⊢ { ( ran 𝑆 ∩ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) ) } = { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) }
32	31	uneq1i	⊢ ( { ( ran 𝑆 ∩ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
33		snfi	⊢ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∈ Fin
34		fzofi	⊢ ( 0 ..^ 𝑁 ) ∈ Fin
35		eqid	⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
36	35	rnmptfi	⊢ ( ( 0 ..^ 𝑁 ) ∈ Fin → ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ Fin )
37	34 36	ax-mp	⊢ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ Fin
38		unfi	⊢ ( ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∈ Fin ∧ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ Fin ) → ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ∈ Fin )
39	33 37 38	mp2an	⊢ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ∈ Fin
40	39	a1i	⊢ ( 𝜑 → ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ∈ Fin )
41	32 40	eqeltrid	⊢ ( 𝜑 → ( { ( ran 𝑆 ∩ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ∈ Fin )
42		id	⊢ ( 𝑠 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → 𝑠 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
43	32	unieqi	⊢ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) = ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
44	42 43	eleqtrdi	⊢ ( 𝑠 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → 𝑠 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
45		simpl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) → 𝜑 )
46		uniun	⊢ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
47	46	eleq2i	⊢ ( 𝑠 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ↔ 𝑠 ∈ ( ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
48		elun	⊢ ( 𝑠 ∈ ( ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ↔ ( 𝑠 ∈ ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∨ 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
49	47 48	sylbb	⊢ ( 𝑠 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → ( 𝑠 ∈ ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∨ 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
50	49	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) → ( 𝑠 ∈ ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∨ 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
51		ovex	⊢ ( 0 ... 𝑁 ) ∈ V
52	51	a1i	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
53	12 52	fexd	⊢ ( 𝜑 → 𝑆 ∈ V )
54		rnexg	⊢ ( 𝑆 ∈ V → ran 𝑆 ∈ V )
55	53 54	syl	⊢ ( 𝜑 → ran 𝑆 ∈ V )
56		inex1g	⊢ ( ran 𝑆 ∈ V → ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ∈ V )
57	55 56	syl	⊢ ( 𝜑 → ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ∈ V )
58		unisng	⊢ ( ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ∈ V → ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) )
59	57 58	syl	⊢ ( 𝜑 → ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) )
60	59	eleq2d	⊢ ( 𝜑 → ( 𝑠 ∈ ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ↔ 𝑠 ∈ ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ) )
61	60	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) → ( 𝑠 ∈ ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ↔ 𝑠 ∈ ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ) )
62	61	orbi1d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) → ( ( 𝑠 ∈ ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∨ 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ↔ ( 𝑠 ∈ ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ∨ 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) )
63	50 62	mpbid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) → ( 𝑠 ∈ ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ∨ 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
64		dvf	⊢ ( ℝ D 𝑂 ) : dom ( ℝ D 𝑂 ) ⟶ ℂ
65	64	a1i	⊢ ( 𝑠 ∈ ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) → ( ℝ D 𝑂 ) : dom ( ℝ D 𝑂 ) ⟶ ℂ )
66		elinel2	⊢ ( 𝑠 ∈ ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) → 𝑠 ∈ dom ( ℝ D 𝑂 ) )
67	65 66	ffvelcdmd	⊢ ( 𝑠 ∈ ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) → ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ∈ ℂ )
68	67	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ) → ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ∈ ℂ )
69		ovex	⊢ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∈ V
70	69	dfiun3	⊢ ∪ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
71	70	eleq2i	⊢ ( 𝑠 ∈ ∪ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↔ 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
72	71	biimpri	⊢ ( 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ∪ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
73	72	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → 𝑠 ∈ ∪ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
74		eliun	⊢ ( 𝑠 ∈ ∪ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↔ ∃ 𝑗 ∈ ( 0 ..^ 𝑁 ) 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
75	73 74	sylib	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑁 ) 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
76		nfv	⊢ Ⅎ 𝑗 𝜑
77		nfmpt1	⊢ Ⅎ 𝑗 ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
78	77	nfrn	⊢ Ⅎ 𝑗 ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
79	78	nfuni	⊢ Ⅎ 𝑗 ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
80	79	nfcri	⊢ Ⅎ 𝑗 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
81	76 80	nfan	⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
82		nfv	⊢ Ⅎ 𝑗 ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ∈ ℂ
83	64	a1i	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ℝ D 𝑂 ) : dom ( ℝ D 𝑂 ) ⟶ ℂ )
84	8	reseq1i	⊢ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
85		ioossicc	⊢ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
86	85 14	sstrid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
87	86	resmptd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
88	84 87	eqtrid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
89	17 88	eqtr4id	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑌 = ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
90	89	oveq2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D 𝑌 ) = ( ℝ D ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
91		ax-resscn	⊢ ℝ ⊆ ℂ
92	91	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
93	1	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐹 : ℝ ⟶ ℝ )
94	2	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑋 ∈ ℝ )
95	3 4	iccssred	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
96	95	sselda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ∈ ℝ )
97	94 96	readdcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
98	93 97	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
99	98	recnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
100	7	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
101	100	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐶 ∈ ℂ )
102	99 101	subcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ∈ ℂ )
103		2cnd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 2 ∈ ℂ )
104	95 92	sstrd	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
105	104	sselda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ∈ ℂ )
106	105	halfcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑠 / 2 ) ∈ ℂ )
107	106	sincld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
108	103 107	mulcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
109		2ne0	⊢ 2 ≠ 0
110	109	a1i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 2 ≠ 0 )
111	5	sselda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ∈ ( - π [,] π ) )
112		eqcom	⊢ ( 𝑠 = 0 ↔ 0 = 𝑠 )
113	112	biimpi	⊢ ( 𝑠 = 0 → 0 = 𝑠 )
114	113	adantl	⊢ ( ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑠 = 0 ) → 0 = 𝑠 )
115		simpl	⊢ ( ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑠 = 0 ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
116	114 115	eqeltrd	⊢ ( ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑠 = 0 ) → 0 ∈ ( 𝐴 [,] 𝐵 ) )
117	116	adantll	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑠 = 0 ) → 0 ∈ ( 𝐴 [,] 𝐵 ) )
118	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑠 = 0 ) → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
119	117 118	pm2.65da	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ¬ 𝑠 = 0 )
120	119	neqned	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ≠ 0 )
121		fourierdlem44	⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 𝑠 ≠ 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
122	111 120 121	syl2anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
123	103 107 110 122	mulne0d	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 )
124	102 108 123	divcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ℂ )
125	124 8	fmptd	⊢ ( 𝜑 → 𝑂 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
126		ioossre	⊢ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ℝ
127	126	a1i	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ℝ )
128		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
129	128	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
130	128 129	dvres	⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝑂 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ) ∧ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ℝ ) ) → ( ℝ D ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( ( ℝ D 𝑂 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
131	92 125 95 127 130	syl22anc	⊢ ( 𝜑 → ( ℝ D ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( ( ℝ D 𝑂 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
132		ioontr	⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
133	132	reseq2i	⊢ ( ( ℝ D 𝑂 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( ( ℝ D 𝑂 ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
134	131 133	eqtrdi	⊢ ( 𝜑 → ( ℝ D ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( ( ℝ D 𝑂 ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
135	134	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( ( ℝ D 𝑂 ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
136	90 135	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ℝ D 𝑂 ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( ℝ D 𝑌 ) )
137	136	dmeqd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → dom ( ( ℝ D 𝑂 ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = dom ( ℝ D 𝑌 ) )
138	1	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐹 : ℝ ⟶ ℝ )
139	2	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑋 ∈ ℝ )
140	95	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
141	12	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐴 [,] 𝐵 ) )
142		elfzofz	⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
143	142	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
144	141 143	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) )
145	140 144	sseldd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
146		fzofzp1	⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
147	146	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
148	141 147	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
149	140 148	sseldd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
150	9	feq2i	⊢ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) : 𝐼 ⟶ ℝ ↔ ( ℝ D ( 𝐹 ↾ 𝐼 ) ) : ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⟶ ℝ )
151	16 150	sylib	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝐹 ↾ 𝐼 ) ) : ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⟶ ℝ )
152	9	reseq2i	⊢ ( 𝐹 ↾ 𝐼 ) = ( 𝐹 ↾ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
153	152	oveq2i	⊢ ( ℝ D ( 𝐹 ↾ 𝐼 ) ) = ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
154	153	feq1i	⊢ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) : ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⟶ ℝ ↔ ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) : ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⟶ ℝ )
155	151 154	sylib	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) : ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⟶ ℝ )
156	5	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
157	86 156	sstrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( - π [,] π ) )
158	6	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
159	86 158	ssneldd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ¬ 0 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
160	7	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ∈ ℝ )
161	138 139 145 149 155 157 159 160 17	fourierdlem57	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ℝ D 𝑌 ) : ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⟶ ℝ ∧ ( ℝ D 𝑌 ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) ) ) ∧ ( ℝ D ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( cos ‘ ( 𝑠 / 2 ) ) ) )
162	161	simpli	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ℝ D 𝑌 ) : ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⟶ ℝ ∧ ( ℝ D 𝑌 ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) · ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) − ( ( cos ‘ ( 𝑠 / 2 ) ) · ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ) / ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ↑ 2 ) ) ) ) )
163	162	simpld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ℝ D 𝑌 ) : ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⟶ ℝ )
164		fdm	⊢ ( ( ℝ D 𝑌 ) : ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⟶ ℝ → dom ( ℝ D 𝑌 ) = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
165	163 164	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → dom ( ℝ D 𝑌 ) = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
166	137 165	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = dom ( ( ℝ D 𝑂 ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
167		resss	⊢ ( ( ℝ D 𝑂 ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ℝ D 𝑂 )
168		dmss	⊢ ( ( ( ℝ D 𝑂 ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ℝ D 𝑂 ) → dom ( ( ℝ D 𝑂 ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ dom ( ℝ D 𝑂 ) )
169	167 168	mp1i	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → dom ( ( ℝ D 𝑂 ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ dom ( ℝ D 𝑂 ) )
170	166 169	eqsstrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ dom ( ℝ D 𝑂 ) )
171	170	3adant3	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ dom ( ℝ D 𝑂 ) )
172		simp3	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
173	171 172	sseldd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ dom ( ℝ D 𝑂 ) )
174	83 173	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ∈ ℂ )
175	174	3exp	⊢ ( 𝜑 → ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ∈ ℂ ) ) )
176	175	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ∈ ℂ ) ) )
177	81 82 176	rexlimd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → ( ∃ 𝑗 ∈ ( 0 ..^ 𝑁 ) 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ∈ ℂ ) )
178	75 177	mpd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ∈ ℂ )
179	68 178	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ∨ 𝑠 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) → ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ∈ ℂ )
180	45 63 179	syl2anc	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) → ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ∈ ℂ )
181	180	abscld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) → ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ∈ ℝ )
182	44 181	sylan2	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) → ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ∈ ℝ )
183		id	⊢ ( 𝑟 ∈ ( { ( ran 𝑆 ∩ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → 𝑟 ∈ ( { ( ran 𝑆 ∩ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
184	183 32	eleqtrdi	⊢ ( 𝑟 ∈ ( { ( ran 𝑆 ∩ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → 𝑟 ∈ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
185		elsni	⊢ ( 𝑟 ∈ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } → 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) )
186		simpr	⊢ ( ( 𝜑 ∧ 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ) → 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) )
187		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
188		rnffi	⊢ ( ( 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐴 [,] 𝐵 ) ∧ ( 0 ... 𝑁 ) ∈ Fin ) → ran 𝑆 ∈ Fin )
189	12 187 188	syl2anc	⊢ ( 𝜑 → ran 𝑆 ∈ Fin )
190		infi	⊢ ( ran 𝑆 ∈ Fin → ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ∈ Fin )
191	189 190	syl	⊢ ( 𝜑 → ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ∈ Fin )
192	191	adantr	⊢ ( ( 𝜑 ∧ 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ) → ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ∈ Fin )
193	186 192	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ) → 𝑟 ∈ Fin )
194		nfv	⊢ Ⅎ 𝑠 𝜑
195		nfcv	⊢ Ⅎ 𝑠 ran 𝑆
196		nfcv	⊢ Ⅎ 𝑠 ℝ
197		nfcv	⊢ Ⅎ 𝑠 D
198		nfmpt1	⊢ Ⅎ 𝑠 ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
199	8 198	nfcxfr	⊢ Ⅎ 𝑠 𝑂
200	196 197 199	nfov	⊢ Ⅎ 𝑠 ( ℝ D 𝑂 )
201	200	nfdm	⊢ Ⅎ 𝑠 dom ( ℝ D 𝑂 )
202	195 201	nfin	⊢ Ⅎ 𝑠 ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) )
203	202	nfeq2	⊢ Ⅎ 𝑠 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) )
204	194 203	nfan	⊢ Ⅎ 𝑠 ( 𝜑 ∧ 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) )
205		simpr	⊢ ( ( 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ∧ 𝑠 ∈ 𝑟 ) → 𝑠 ∈ 𝑟 )
206		simpl	⊢ ( ( 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ∧ 𝑠 ∈ 𝑟 ) → 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) )
207	205 206	eleqtrd	⊢ ( ( 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ∧ 𝑠 ∈ 𝑟 ) → 𝑠 ∈ ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) )
208	207 66	syl	⊢ ( ( 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ∧ 𝑠 ∈ 𝑟 ) → 𝑠 ∈ dom ( ℝ D 𝑂 ) )
209	208	adantll	⊢ ( ( ( 𝜑 ∧ 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ) ∧ 𝑠 ∈ 𝑟 ) → 𝑠 ∈ dom ( ℝ D 𝑂 ) )
210	64	ffvelcdmi	⊢ ( 𝑠 ∈ dom ( ℝ D 𝑂 ) → ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ∈ ℂ )
211	210	abscld	⊢ ( 𝑠 ∈ dom ( ℝ D 𝑂 ) → ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ∈ ℝ )
212	209 211	syl	⊢ ( ( ( 𝜑 ∧ 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ) ∧ 𝑠 ∈ 𝑟 ) → ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ∈ ℝ )
213	212	ex	⊢ ( ( 𝜑 ∧ 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ) → ( 𝑠 ∈ 𝑟 → ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ∈ ℝ ) )
214	204 213	ralrimi	⊢ ( ( 𝜑 ∧ 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ) → ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ∈ ℝ )
215		fimaxre3	⊢ ( ( 𝑟 ∈ Fin ∧ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ∈ ℝ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 )
216	193 214 215	syl2anc	⊢ ( ( 𝜑 ∧ 𝑟 = ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 )
217	185 216	sylan2	⊢ ( ( 𝜑 ∧ 𝑟 ∈ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 )
218	217	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ∧ 𝑟 ∈ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 )
219		simpll	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ∧ ¬ 𝑟 ∈ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ) → 𝜑 )
220		elunnel1	⊢ ( ( 𝑟 ∈ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ∧ ¬ 𝑟 ∈ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ) → 𝑟 ∈ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
221	220	adantll	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ∧ ¬ 𝑟 ∈ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ) → 𝑟 ∈ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
222		vex	⊢ 𝑟 ∈ V
223	35	elrnmpt	⊢ ( 𝑟 ∈ V → ( 𝑟 ∈ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ↔ ∃ 𝑗 ∈ ( 0 ..^ 𝑁 ) 𝑟 = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
224	222 223	ax-mp	⊢ ( 𝑟 ∈ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ↔ ∃ 𝑗 ∈ ( 0 ..^ 𝑁 ) 𝑟 = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
225	224	biimpi	⊢ ( 𝑟 ∈ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑁 ) 𝑟 = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
226	225	adantl	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑁 ) 𝑟 = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
227	78	nfcri	⊢ Ⅎ 𝑗 𝑟 ∈ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
228	76 227	nfan	⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
229		nfv	⊢ Ⅎ 𝑗 ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦
230		reeanv	⊢ ( ∃ 𝑤 ∈ ℝ ∃ 𝑧 ∈ ℝ ( ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) ↔ ( ∃ 𝑤 ∈ ℝ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) )
231	10 11 230	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑤 ∈ ℝ ∃ 𝑧 ∈ ℝ ( ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) )
232		simp1	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ( ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) ) → ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) )
233		simp2l	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ( ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) ) → 𝑤 ∈ ℝ )
234		simp2r	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ( ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) ) → 𝑧 ∈ ℝ )
235	232 233 234	jca31	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ( ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) ) → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) )
236		simp3l	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ( ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) ) → ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 )
237		simp3r	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ( ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) ) → ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 )
238	235 236 237	jca31	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ( ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) ) → ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) )
239	238 18	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ( ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) ) → 𝜒 )
240	18	biimpi	⊢ ( 𝜒 → ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) )
241		simp-5l	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) → 𝜑 )
242	240 241	syl	⊢ ( 𝜒 → 𝜑 )
243	242 1	syl	⊢ ( 𝜒 → 𝐹 : ℝ ⟶ ℝ )
244	242 2	syl	⊢ ( 𝜒 → 𝑋 ∈ ℝ )
245		simp-4l	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) → ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) )
246	240 245	syl	⊢ ( 𝜒 → ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) )
247	246 145	syl	⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
248	246 149	syl	⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
249	246 13	syl	⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
250	14 156	sstrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( - π [,] π ) )
251	246 250	syl	⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( - π [,] π ) )
252	14 158	ssneldd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ¬ 0 ∈ ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
253	246 252	syl	⊢ ( 𝜒 → ¬ 0 ∈ ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
254	246 155	syl	⊢ ( 𝜒 → ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) : ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⟶ ℝ )
255		simp-4r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) → 𝑤 ∈ ℝ )
256	240 255	syl	⊢ ( 𝜒 → 𝑤 ∈ ℝ )
257	240	simplrd	⊢ ( 𝜒 → ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 )
258		id	⊢ ( 𝑡 ∈ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
259	258 9	eleqtrrdi	⊢ ( 𝑡 ∈ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑡 ∈ 𝐼 )
260		rspa	⊢ ( ( ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ 𝑡 ∈ 𝐼 ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 )
261	257 259 260	syl2an	⊢ ( ( 𝜒 ∧ 𝑡 ∈ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 )
262		simpllr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ) ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) → 𝑧 ∈ ℝ )
263	240 262	syl	⊢ ( 𝜒 → 𝑧 ∈ ℝ )
264	153	fveq1i	⊢ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) = ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ‘ 𝑡 )
265	264	fveq2i	⊢ ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) = ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ‘ 𝑡 ) )
266	240	simprd	⊢ ( 𝜒 → ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 )
267	266	r19.21bi	⊢ ( ( 𝜒 ∧ 𝑡 ∈ 𝐼 ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 )
268	265 267	eqbrtrrid	⊢ ( ( 𝜒 ∧ 𝑡 ∈ 𝐼 ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ‘ 𝑡 ) ) ≤ 𝑧 )
269	259 268	sylan2	⊢ ( ( 𝜒 ∧ 𝑡 ∈ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) (,) ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ‘ 𝑡 ) ) ≤ 𝑧 )
270	242 7	syl	⊢ ( 𝜒 → 𝐶 ∈ ℝ )
271	243 244 247 248 249 251 253 254 256 261 263 269 270 17	fourierdlem68	⊢ ( 𝜒 → ( dom ( ℝ D 𝑌 ) = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ dom ( ℝ D 𝑌 ) ( abs ‘ ( ( ℝ D 𝑌 ) ‘ 𝑠 ) ) ≤ 𝑦 ) )
272	271	simprd	⊢ ( 𝜒 → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ dom ( ℝ D 𝑌 ) ( abs ‘ ( ( ℝ D 𝑌 ) ‘ 𝑠 ) ) ≤ 𝑦 )
273	271	simpld	⊢ ( 𝜒 → dom ( ℝ D 𝑌 ) = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
274	273	raleqdv	⊢ ( 𝜒 → ( ∀ 𝑠 ∈ dom ( ℝ D 𝑌 ) ( abs ‘ ( ( ℝ D 𝑌 ) ‘ 𝑠 ) ) ≤ 𝑦 ↔ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑌 ) ‘ 𝑠 ) ) ≤ 𝑦 ) )
275	274	rexbidv	⊢ ( 𝜒 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ dom ( ℝ D 𝑌 ) ( abs ‘ ( ( ℝ D 𝑌 ) ‘ 𝑠 ) ) ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑌 ) ‘ 𝑠 ) ) ≤ 𝑦 ) )
276	272 275	mpbid	⊢ ( 𝜒 → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑌 ) ‘ 𝑠 ) ) ≤ 𝑦 )
277	132	eqcomi	⊢ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
278	277	reseq2i	⊢ ( ( ℝ D 𝑂 ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( ( ℝ D 𝑂 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
279	278	fveq1i	⊢ ( ( ( ℝ D 𝑂 ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ‘ 𝑠 ) = ( ( ( ℝ D 𝑂 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ‘ 𝑠 )
280		fvres	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( ( ( ℝ D 𝑂 ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ‘ 𝑠 ) = ( ( ℝ D 𝑂 ) ‘ 𝑠 ) )
281	280	adantl	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ( ( ℝ D 𝑂 ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ‘ 𝑠 ) = ( ( ℝ D 𝑂 ) ‘ 𝑠 ) )
282	246 86	syl	⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
283	282	resmptd	⊢ ( 𝜒 → ( ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
284	84 283	eqtrid	⊢ ( 𝜒 → ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
285	17 284	eqtr4id	⊢ ( 𝜒 → 𝑌 = ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
286	285	oveq2d	⊢ ( 𝜒 → ( ℝ D 𝑌 ) = ( ℝ D ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
287	286	fveq1d	⊢ ( 𝜒 → ( ( ℝ D 𝑌 ) ‘ 𝑠 ) = ( ( ℝ D ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ‘ 𝑠 ) )
288	131	fveq1d	⊢ ( 𝜑 → ( ( ℝ D ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ‘ 𝑠 ) = ( ( ( ℝ D 𝑂 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ‘ 𝑠 ) )
289	242 288	syl	⊢ ( 𝜒 → ( ( ℝ D ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ‘ 𝑠 ) = ( ( ( ℝ D 𝑂 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ‘ 𝑠 ) )
290	287 289	eqtr2d	⊢ ( 𝜒 → ( ( ( ℝ D 𝑂 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ‘ 𝑠 ) = ( ( ℝ D 𝑌 ) ‘ 𝑠 ) )
291	290	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ( ( ℝ D 𝑂 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ‘ 𝑠 ) = ( ( ℝ D 𝑌 ) ‘ 𝑠 ) )
292	279 281 291	3eqtr3a	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ( ℝ D 𝑂 ) ‘ 𝑠 ) = ( ( ℝ D 𝑌 ) ‘ 𝑠 ) )
293	292	fveq2d	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) = ( abs ‘ ( ( ℝ D 𝑌 ) ‘ 𝑠 ) ) )
294	293	breq1d	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 ↔ ( abs ‘ ( ( ℝ D 𝑌 ) ‘ 𝑠 ) ) ≤ 𝑦 ) )
295	294	ralbidva	⊢ ( 𝜒 → ( ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 ↔ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑌 ) ‘ 𝑠 ) ) ≤ 𝑦 ) )
296	295	rexbidv	⊢ ( 𝜒 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑌 ) ‘ 𝑠 ) ) ≤ 𝑦 ) )
297	276 296	mpbird	⊢ ( 𝜒 → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 )
298	239 297	syl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ( ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 )
299	298	3exp	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 ) ) )
300	299	rexlimdvv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ∃ 𝑤 ∈ ℝ ∃ 𝑧 ∈ ℝ ( ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ≤ 𝑤 ∧ ∀ 𝑡 ∈ 𝐼 ( abs ‘ ( ( ℝ D ( 𝐹 ↾ 𝐼 ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 ) )
301	231 300	mpd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 )
302	301	3adant3	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑟 = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 )
303		raleq	⊢ ( 𝑟 = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 ↔ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 ) )
304	303	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑟 = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 ↔ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 ) )
305	304	rexbidv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑟 = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 ) )
306	302 305	mpbird	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑟 = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 )
307	306	3exp	⊢ ( 𝜑 → ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → ( 𝑟 = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 ) ) )
308	307	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → ( 𝑟 = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 ) ) )
309	228 229 308	rexlimd	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → ( ∃ 𝑗 ∈ ( 0 ..^ 𝑁 ) 𝑟 = ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 ) )
310	226 309	mpd	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 )
311	219 221 310	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) ∧ ¬ 𝑟 ∈ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 )
312	218 311	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 )
313	184 312	sylan2	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( { ( ran 𝑆 ∩ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑠 ∈ 𝑟 ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑦 )
314		pm3.22	⊢ ( ( 𝑟 ∈ dom ( ℝ D 𝑂 ) ∧ 𝑟 ∈ ran 𝑆 ) → ( 𝑟 ∈ ran 𝑆 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) )
315		elin	⊢ ( 𝑟 ∈ ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) ↔ ( 𝑟 ∈ ran 𝑆 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) )
316	314 315	sylibr	⊢ ( ( 𝑟 ∈ dom ( ℝ D 𝑂 ) ∧ 𝑟 ∈ ran 𝑆 ) → 𝑟 ∈ ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) )
317	316	adantll	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) ∧ 𝑟 ∈ ran 𝑆 ) → 𝑟 ∈ ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) )
318	59	eqcomd	⊢ ( 𝜑 → ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) = ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } )
319	318	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) ∧ 𝑟 ∈ ran 𝑆 ) → ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) = ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } )
320	317 319	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) ∧ 𝑟 ∈ ran 𝑆 ) → 𝑟 ∈ ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } )
321	320	orcd	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) ∧ 𝑟 ∈ ran 𝑆 ) → ( 𝑟 ∈ ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∨ 𝑟 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
322		simpll	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) ∧ ¬ 𝑟 ∈ ran 𝑆 ) → 𝜑 )
323	91	a1i	⊢ ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) → ℝ ⊆ ℂ )
324	125	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) → 𝑂 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
325	3	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) → 𝐴 ∈ ℝ )
326	4	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) → 𝐵 ∈ ℝ )
327	325 326	iccssred	⊢ ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
328	323 324 327	dvbss	⊢ ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) → dom ( ℝ D 𝑂 ) ⊆ ( 𝐴 [,] 𝐵 ) )
329		simpr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) → 𝑟 ∈ dom ( ℝ D 𝑂 ) )
330	328 329	sseldd	⊢ ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) → 𝑟 ∈ ( 𝐴 [,] 𝐵 ) )
331	330	adantr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) ∧ ¬ 𝑟 ∈ ran 𝑆 ) → 𝑟 ∈ ( 𝐴 [,] 𝐵 ) )
332		simpr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) ∧ ¬ 𝑟 ∈ ran 𝑆 ) → ¬ 𝑟 ∈ ran 𝑆 )
333		fveq2	⊢ ( 𝑗 = 𝑘 → ( 𝑆 ‘ 𝑗 ) = ( 𝑆 ‘ 𝑘 ) )
334		oveq1	⊢ ( 𝑗 = 𝑘 → ( 𝑗 + 1 ) = ( 𝑘 + 1 ) )
335	334	fveq2d	⊢ ( 𝑗 = 𝑘 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑆 ‘ ( 𝑘 + 1 ) ) )
336	333 335	oveq12d	⊢ ( 𝑗 = 𝑘 → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝑆 ‘ 𝑘 ) (,) ( 𝑆 ‘ ( 𝑘 + 1 ) ) ) )
337		ovex	⊢ ( ( 𝑆 ‘ 𝑘 ) (,) ( 𝑆 ‘ ( 𝑘 + 1 ) ) ) ∈ V
338	336 35 337	fvmpt	⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ‘ 𝑘 ) = ( ( 𝑆 ‘ 𝑘 ) (,) ( 𝑆 ‘ ( 𝑘 + 1 ) ) ) )
339	338	eleq2d	⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝑟 ∈ ( ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ‘ 𝑘 ) ↔ 𝑟 ∈ ( ( 𝑆 ‘ 𝑘 ) (,) ( 𝑆 ‘ ( 𝑘 + 1 ) ) ) ) )
340	339	rexbiia	⊢ ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑟 ∈ ( ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ‘ 𝑘 ) ↔ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑟 ∈ ( ( 𝑆 ‘ 𝑘 ) (,) ( 𝑆 ‘ ( 𝑘 + 1 ) ) ) )
341	15 340	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑟 ∈ ran 𝑆 ) → ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑟 ∈ ( ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ‘ 𝑘 ) )
342	69 35	dmmpti	⊢ dom ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( 0 ..^ 𝑁 )
343	342	rexeqi	⊢ ( ∃ 𝑘 ∈ dom ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) 𝑟 ∈ ( ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ‘ 𝑘 ) ↔ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑟 ∈ ( ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ‘ 𝑘 ) )
344	341 343	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑟 ∈ ran 𝑆 ) → ∃ 𝑘 ∈ dom ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) 𝑟 ∈ ( ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ‘ 𝑘 ) )
345	322 331 332 344	syl21anc	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) ∧ ¬ 𝑟 ∈ ran 𝑆 ) → ∃ 𝑘 ∈ dom ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) 𝑟 ∈ ( ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ‘ 𝑘 ) )
346		funmpt	⊢ Fun ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
347		elunirn	⊢ ( Fun ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑟 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ↔ ∃ 𝑘 ∈ dom ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) 𝑟 ∈ ( ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ‘ 𝑘 ) ) )
348	346 347	mp1i	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) ∧ ¬ 𝑟 ∈ ran 𝑆 ) → ( 𝑟 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ↔ ∃ 𝑘 ∈ dom ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) 𝑟 ∈ ( ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ‘ 𝑘 ) ) )
349	345 348	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) ∧ ¬ 𝑟 ∈ ran 𝑆 ) → 𝑟 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
350	349	olcd	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) ∧ ¬ 𝑟 ∈ ran 𝑆 ) → ( 𝑟 ∈ ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∨ 𝑟 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
351	321 350	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) → ( 𝑟 ∈ ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∨ 𝑟 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
352		elun	⊢ ( 𝑟 ∈ ( ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ↔ ( 𝑟 ∈ ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∨ 𝑟 ∈ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
353	351 352	sylibr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) → 𝑟 ∈ ( ∪ { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
354	353 46	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑟 ∈ dom ( ℝ D 𝑂 ) ) → 𝑟 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
355	354	ralrimiva	⊢ ( 𝜑 → ∀ 𝑟 ∈ dom ( ℝ D 𝑂 ) 𝑟 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
356		dfss3	⊢ ( dom ( ℝ D 𝑂 ) ⊆ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ↔ ∀ 𝑟 ∈ dom ( ℝ D 𝑂 ) 𝑟 ∈ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
357	355 356	sylibr	⊢ ( 𝜑 → dom ( ℝ D 𝑂 ) ⊆ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D 𝑂 ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
358	357 43	sseqtrrdi	⊢ ( 𝜑 → dom ( ℝ D 𝑂 ) ⊆ ∪ ( { ( ran 𝑆 ∩ dom ( ℝ D ( 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑡 ) ) − 𝐶 ) / ( 2 · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) ) } ∪ ran ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
359	41 182 313 358	ssfiunibd	⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑠 ∈ dom ( ℝ D 𝑂 ) ( abs ‘ ( ( ℝ D 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑏 )