# 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 ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
fourierdlem80.xre ${⊢}{\phi }\to {X}\in ℝ$
fourierdlem80.a ${⊢}{\phi }\to {A}\in ℝ$
fourierdlem80.b ${⊢}{\phi }\to {B}\in ℝ$
fourierdlem80.ab ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
fourierdlem80.n0 ${⊢}{\phi }\to ¬0\in \left[{A},{B}\right]$
fourierdlem80.c ${⊢}{\phi }\to {C}\in ℝ$
fourierdlem80.o ${⊢}{O}=\left({s}\in \left[{A},{B}\right]⟼\frac{{F}\left({X}+{s}\right)-{C}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
fourierdlem80.i ${⊢}{I}=\left({X}+{S}\left({j}\right),{X}+{S}\left({j}+1\right)\right)$
fourierdlem80.fbdioo ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}\right)\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in {I}\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}$
fourierdlem80.fdvbdioo ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in {I}\phantom{\rule{.4em}{0ex}}\left|{\left({{F}↾}_{{I}}\right)}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
fourierdlem80.sf ${⊢}{\phi }\to {S}:\left(0\dots {N}\right)⟶\left[{A},{B}\right]$
fourierdlem80.slt ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}\right)\right)\to {S}\left({j}\right)<{S}\left({j}+1\right)$
fourierdlem80.sjss ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}\right)\right)\to \left[{S}\left({j}\right),{S}\left({j}+1\right)\right]\subseteq \left[{A},{B}\right]$
fourierdlem80.relioo ${⊢}\left(\left({\phi }\wedge {r}\in \left[{A},{B}\right]\right)\wedge ¬{r}\in \mathrm{ran}{S}\right)\to \exists {k}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{r}\in \left({S}\left({k}\right),{S}\left({k}+1\right)\right)$
fdv ${⊢}\left({\phi }\wedge {j}\in \left(0..^{N}\right)\right)\to {\left({{F}↾}_{{I}}\right)}_{ℝ}^{\prime }:{I}⟶ℝ$
fourierdlem80.y ${⊢}{Y}=\left({s}\in \left({S}\left({j}\right),{S}\left({j}+1\right)\right)⟼\frac{{F}\left({X}+{s}\right)-{C}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
fourierdlem80.ch ${⊢}{\chi }↔\left(\left(\left(\left(\left({\phi }\wedge {j}\in \left(0..^{N}\right)\right)\wedge {w}\in ℝ\right)\wedge {z}\in ℝ\right)\wedge \forall {t}\in {I}\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)\wedge \forall {t}\in {I}\phantom{\rule{.4em}{0ex}}\left|{\left({{F}↾}_{{I}}\right)}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)$
Assertion fourierdlem80 ${⊢}{\phi }\to \exists {b}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {s}\in \mathrm{dom}{{O}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{O}}_{ℝ}^{\prime }\left({s}\right)\right|\le {b}$

### Proof

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