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