Metamath Proof Explorer

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 ffvelrnd ⊢ ( 𝑠 ∈ ( 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 syl5eq ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) )
145 140 144 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
146 fzofzp1 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
147 146 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
148 141 147 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ffvelrni ⊢ ( 𝑠 ∈ 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 syl5eq ⊢ ( 𝜒 → ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 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 𝑂 ) ‘ 𝑠 ) ) ≤ 𝑏 )