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