fourierdlem68

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

	Ref	Expression
Hypotheses	fourierdlem68.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem68.xre	$⊢ φ \to X \in ℝ$
	fourierdlem68.a	$⊢ φ \to A \in ℝ$
	fourierdlem68.b	$⊢ φ \to B \in ℝ$
	fourierdlem68.altb	$⊢ φ \to A < B$
	fourierdlem68.ab	$⊢ φ \to [A, B] \subseteq [- π, π]$
	fourierdlem68.n0	$⊢ φ \to \neg 0 \in [A, B]$
	fourierdlem68.fdv	$⊢ φ \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) ⟶ ℝ$
	fourierdlem68.d	$⊢ φ \to D \in ℝ$
	fourierdlem68.fbd	$⊢ (φ \land t \in (X + A, X + B)) \to \|F (t)\| \leq D$
	fourierdlem68.e	$⊢ φ \to E \in ℝ$
	fourierdlem68.fdvbd	$⊢ (φ \land t \in (X + A, X + B)) \to \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (t)\| \leq E$
	fourierdlem68.c	$⊢ φ \to C \in ℝ$
	fourierdlem68.o	$⊢ O = (s \in (A, B) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
Assertion	fourierdlem68	$⊢ φ \to (dom O_{ℝ}^{'} = (A, B) \land \exists b \in ℝ \forall s \in dom O_{ℝ}^{'} \|O_{ℝ}^{'} (s)\| \leq b)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem68.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem68.xre	$⊢ φ \to X \in ℝ$
3		fourierdlem68.a	$⊢ φ \to A \in ℝ$
4		fourierdlem68.b	$⊢ φ \to B \in ℝ$
5		fourierdlem68.altb	$⊢ φ \to A < B$
6		fourierdlem68.ab	$⊢ φ \to [A, B] \subseteq [- π, π]$
7		fourierdlem68.n0	$⊢ φ \to \neg 0 \in [A, B]$
8		fourierdlem68.fdv	$⊢ φ \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) ⟶ ℝ$
9		fourierdlem68.d	$⊢ φ \to D \in ℝ$
10		fourierdlem68.fbd	$⊢ (φ \land t \in (X + A, X + B)) \to \|F (t)\| \leq D$
11		fourierdlem68.e	$⊢ φ \to E \in ℝ$
12		fourierdlem68.fdvbd	$⊢ (φ \land t \in (X + A, X + B)) \to \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (t)\| \leq E$
13		fourierdlem68.c	$⊢ φ \to C \in ℝ$
14		fourierdlem68.o	$⊢ O = (s \in (A, B) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
15		ioossicc	$⊢ (A, B) \subseteq [A, B]$
16	15 6	sstrid	$⊢ φ \to (A, B) \subseteq [- π, π]$
17	15	sseli	$⊢ 0 \in (A, B) \to 0 \in [A, B]$
18	7 17	nsyl	$⊢ φ \to \neg 0 \in (A, B)$
19	1 2 3 4 8 16 18 13 14	fourierdlem57	$⊢ ((φ \to (O_{ℝ}^{'} : (A, B) ⟶ ℝ \land ℝ D O = (s \in (A, B) ⟼ \frac{{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C)}{{2 \sin (\frac{s}{2})}^{2}}))) \land \frac{d (s \in (A, B)⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in (A, B) ⟼ \cos (\frac{s}{2})))$
20	19	simpli	$⊢ φ \to (O_{ℝ}^{'} : (A, B) ⟶ ℝ \land ℝ D O = (s \in (A, B) ⟼ \frac{{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) 2 \sin (\frac{s}{2}) - \cos (\frac{s}{2}) (F (X + s) - C)}{{2 \sin (\frac{s}{2})}^{2}}))$
21	20	simpld	$⊢ φ \to O_{ℝ}^{'} : (A, B) ⟶ ℝ$
22	21	fdmd	$⊢ φ \to dom O_{ℝ}^{'} = (A, B)$
23		eqid	$⊢ (t \in [A, B] ⟼ 2 \sin (\frac{t}{2})) = (t \in [A, B] ⟼ 2 \sin (\frac{t}{2}))$
24	3 4 5	ltled	$⊢ φ \to A \leq B$
25		2re	$⊢ 2 \in ℝ$
26	25	a1i	$⊢ (φ \land t \in [A, B]) \to 2 \in ℝ$
27	3 4	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
28	27	sselda	$⊢ (φ \land t \in [A, B]) \to t \in ℝ$
29	28	rehalfcld	$⊢ (φ \land t \in [A, B]) \to \frac{t}{2} \in ℝ$
30	29	resincld	$⊢ (φ \land t \in [A, B]) \to \sin (\frac{t}{2}) \in ℝ$
31	26 30	remulcld	$⊢ (φ \land t \in [A, B]) \to 2 \sin (\frac{t}{2}) \in ℝ$
32		2cnd	$⊢ (φ \land t \in [A, B]) \to 2 \in ℂ$
33	30	recnd	$⊢ (φ \land t \in [A, B]) \to \sin (\frac{t}{2}) \in ℂ$
34		2ne0	$⊢ 2 \neq 0$
35	34	a1i	$⊢ (φ \land t \in [A, B]) \to 2 \neq 0$
36	6	sselda	$⊢ (φ \land t \in [A, B]) \to t \in [- π, π]$
37		eqcom	$⊢ t = 0 \leftrightarrow 0 = t$
38	37	bilani	$⊢ (t \in [A, B] \land t = 0) \to 0 = t$
39		simpl	$⊢ (t \in [A, B] \land t = 0) \to t \in [A, B]$
40	38 39	eqeltrd	$⊢ (t \in [A, B] \land t = 0) \to 0 \in [A, B]$
41	40	adantll	$⊢ ((φ \land t \in [A, B]) \land t = 0) \to 0 \in [A, B]$
42	7	ad2antrr	$⊢ ((φ \land t \in [A, B]) \land t = 0) \to \neg 0 \in [A, B]$
43	41 42	pm2.65da	$⊢ (φ \land t \in [A, B]) \to \neg t = 0$
44	43	neqned	$⊢ (φ \land t \in [A, B]) \to t \neq 0$
45		fourierdlem44	$⊢ (t \in [- π, π] \land t \neq 0) \to \sin (\frac{t}{2}) \neq 0$
46	36 44 45	syl2anc	$⊢ (φ \land t \in [A, B]) \to \sin (\frac{t}{2}) \neq 0$
47	32 33 35 46	mulne0d	$⊢ (φ \land t \in [A, B]) \to 2 \sin (\frac{t}{2}) \neq 0$
48		eldifsn	$⊢ 2 \sin (\frac{t}{2}) \in (ℝ ∖ \{0\}) \leftrightarrow (2 \sin (\frac{t}{2}) \in ℝ \land 2 \sin (\frac{t}{2}) \neq 0)$
49	31 47 48	sylanbrc	$⊢ (φ \land t \in [A, B]) \to 2 \sin (\frac{t}{2}) \in (ℝ ∖ \{0\})$
50	49 23	fmptd	$⊢ φ \to (t \in [A, B] ⟼ 2 \sin (\frac{t}{2})) : [A, B] ⟶ ℝ ∖ \{0\}$
51		difss	$⊢ ℝ ∖ \{0\} \subseteq ℝ$
52		ax-resscn	$⊢ ℝ \subseteq ℂ$
53	51 52	sstri	$⊢ ℝ ∖ \{0\} \subseteq ℂ$
54	53	a1i	$⊢ φ \to ℝ ∖ \{0\} \subseteq ℂ$
55	27 52	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
56		2cnd	$⊢ φ \to 2 \in ℂ$
57		ssid	$⊢ ℂ \subseteq ℂ$
58	57	a1i	$⊢ φ \to ℂ \subseteq ℂ$
59	55 56 58	constcncfg	$⊢ φ \to (t \in [A, B] ⟼ 2) : [A, B] \underset{cn}{⟶} ℂ$
60		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
61	60	a1i	$⊢ φ \to \sin : ℂ \underset{cn}{⟶} ℂ$
62	55 58	idcncfg	$⊢ φ \to (t \in [A, B] ⟼ t) : [A, B] \underset{cn}{⟶} ℂ$
63		eldifsn	$⊢ 2 \in (ℂ ∖ \{0\}) \leftrightarrow (2 \in ℂ \land 2 \neq 0)$
64	32 35 63	sylanbrc	$⊢ (φ \land t \in [A, B]) \to 2 \in (ℂ ∖ \{0\})$
65		eqid	$⊢ (t \in [A, B] ⟼ 2) = (t \in [A, B] ⟼ 2)$
66	64 65	fmptd	$⊢ φ \to (t \in [A, B] ⟼ 2) : [A, B] ⟶ ℂ ∖ \{0\}$
67		difssd	$⊢ φ \to ℂ ∖ \{0\} \subseteq ℂ$
68		cncfcdm	$⊢ (ℂ ∖ \{0\} \subseteq ℂ \land (t \in [A, B] ⟼ 2) : [A, B] \underset{cn}{⟶} ℂ) \to ((t \in [A, B] ⟼ 2) : [A, B] \underset{cn}{⟶} (ℂ ∖ \{0\}) \leftrightarrow (t \in [A, B] ⟼ 2) : [A, B] ⟶ ℂ ∖ \{0\})$
69	67 59 68	syl2anc	$⊢ φ \to ((t \in [A, B] ⟼ 2) : [A, B] \underset{cn}{⟶} (ℂ ∖ \{0\}) \leftrightarrow (t \in [A, B] ⟼ 2) : [A, B] ⟶ ℂ ∖ \{0\})$
70	66 69	mpbird	$⊢ φ \to (t \in [A, B] ⟼ 2) : [A, B] \underset{cn}{⟶} (ℂ ∖ \{0\})$
71	62 70	divcncf	$⊢ φ \to (t \in [A, B] ⟼ \frac{t}{2}) : [A, B] \underset{cn}{⟶} ℂ$
72	61 71	cncfmpt1f	$⊢ φ \to (t \in [A, B] ⟼ \sin (\frac{t}{2})) : [A, B] \underset{cn}{⟶} ℂ$
73	59 72	mulcncf	$⊢ φ \to (t \in [A, B] ⟼ 2 \sin (\frac{t}{2})) : [A, B] \underset{cn}{⟶} ℂ$
74		cncfcdm	$⊢ (ℝ ∖ \{0\} \subseteq ℂ \land (t \in [A, B] ⟼ 2 \sin (\frac{t}{2})) : [A, B] \underset{cn}{⟶} ℂ) \to ((t \in [A, B] ⟼ 2 \sin (\frac{t}{2})) : [A, B] \underset{cn}{⟶} (ℝ ∖ \{0\}) \leftrightarrow (t \in [A, B] ⟼ 2 \sin (\frac{t}{2})) : [A, B] ⟶ ℝ ∖ \{0\})$
75	54 73 74	syl2anc	$⊢ φ \to ((t \in [A, B] ⟼ 2 \sin (\frac{t}{2})) : [A, B] \underset{cn}{⟶} (ℝ ∖ \{0\}) \leftrightarrow (t \in [A, B] ⟼ 2 \sin (\frac{t}{2})) : [A, B] ⟶ ℝ ∖ \{0\})$
76	50 75	mpbird	$⊢ φ \to (t \in [A, B] ⟼ 2 \sin (\frac{t}{2})) : [A, B] \underset{cn}{⟶} (ℝ ∖ \{0\})$
77	23 3 4 24 76	cncficcgt0	$⊢ φ \to \exists c \in ℝ^{+} \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|$
78		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
79	78	a1i	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to ℝ \in \{ℝ, ℂ\}$
80	1	adantr	$⊢ (φ \land s \in (A, B)) \to F : ℝ ⟶ ℝ$
81	2	adantr	$⊢ (φ \land s \in (A, B)) \to X \in ℝ$
82		elioore	$⊢ s \in (A, B) \to s \in ℝ$
83	82	adantl	$⊢ (φ \land s \in (A, B)) \to s \in ℝ$
84	81 83	readdcld	$⊢ (φ \land s \in (A, B)) \to X + s \in ℝ$
85	80 84	ffvelcdmd	$⊢ (φ \land s \in (A, B)) \to F (X + s) \in ℝ$
86	13	adantr	$⊢ (φ \land s \in (A, B)) \to C \in ℝ$
87	85 86	resubcld	$⊢ (φ \land s \in (A, B)) \to F (X + s) - C \in ℝ$
88	87	recnd	$⊢ (φ \land s \in (A, B)) \to F (X + s) - C \in ℂ$
89	88	3ad2antl1	$⊢ ((φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \land s \in (A, B)) \to F (X + s) - C \in ℂ$
90	78	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
91	85	recnd	$⊢ (φ \land s \in (A, B)) \to F (X + s) \in ℂ$
92	8	adantr	$⊢ (φ \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) ⟶ ℝ$
93	2 3	readdcld	$⊢ φ \to X + A \in ℝ$
94	93	rexrd	$⊢ φ \to X + A \in ℝ^{*}$
95	94	adantr	$⊢ (φ \land s \in (A, B)) \to X + A \in ℝ^{*}$
96	2 4	readdcld	$⊢ φ \to X + B \in ℝ$
97	96	rexrd	$⊢ φ \to X + B \in ℝ^{*}$
98	97	adantr	$⊢ (φ \land s \in (A, B)) \to X + B \in ℝ^{*}$
99	3	adantr	$⊢ (φ \land s \in (A, B)) \to A \in ℝ$
100	99	rexrd	$⊢ (φ \land s \in (A, B)) \to A \in ℝ^{*}$
101	4	rexrd	$⊢ φ \to B \in ℝ^{*}$
102	101	adantr	$⊢ (φ \land s \in (A, B)) \to B \in ℝ^{*}$
103		simpr	$⊢ (φ \land s \in (A, B)) \to s \in (A, B)$
104		ioogtlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land s \in (A, B)) \to A < s$
105	100 102 103 104	syl3anc	$⊢ (φ \land s \in (A, B)) \to A < s$
106	99 83 81 105	ltadd2dd	$⊢ (φ \land s \in (A, B)) \to X + A < X + s$
107	4	adantr	$⊢ (φ \land s \in (A, B)) \to B \in ℝ$
108		iooltub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land s \in (A, B)) \to s < B$
109	100 102 103 108	syl3anc	$⊢ (φ \land s \in (A, B)) \to s < B$
110	83 107 81 109	ltadd2dd	$⊢ (φ \land s \in (A, B)) \to X + s < X + B$
111	95 98 84 106 110	eliood	$⊢ (φ \land s \in (A, B)) \to X + s \in (X + A, X + B)$
112	92 111	ffvelcdmd	$⊢ (φ \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) \in ℝ$
113		eqid	$⊢ ℝ D ({F ↾}_{(X + A, X + B)}) = ℝ D ({F ↾}_{(X + A, X + B)})$
114	1 2 3 4 113 8	fourierdlem28	$⊢ φ \to \frac{d (s \in (A, B)⟼ F (X + s))}{d_{ℝ} s} = (s \in (A, B) ⟼ {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s))$
115	86	recnd	$⊢ (φ \land s \in (A, B)) \to C \in ℂ$
116		0red	$⊢ (φ \land s \in (A, B)) \to 0 \in ℝ$
117		iooretop	$⊢ (A, B) \in topGen (ran (.))$
118		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
119	117 118	eleqtri	$⊢ (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
120	119	a1i	$⊢ φ \to (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
121	13	recnd	$⊢ φ \to C \in ℂ$
122	90 120 121	dvmptconst	$⊢ φ \to \frac{d (s \in (A, B)⟼ C)}{d_{ℝ} s} = (s \in (A, B) ⟼ 0)$
123	90 91 112 114 115 116 122	dvmptsub	$⊢ φ \to \frac{d (s \in (A, B)⟼ F (X + s) - C)}{d_{ℝ} s} = (s \in (A, B) ⟼ {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) - 0)$
124	112	recnd	$⊢ (φ \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) \in ℂ$
125	124	subid1d	$⊢ (φ \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) - 0 = {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)$
126	125	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) - 0) = (s \in (A, B) ⟼ {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s))$
127	123 126	eqtrd	$⊢ φ \to \frac{d (s \in (A, B)⟼ F (X + s) - C)}{d_{ℝ} s} = (s \in (A, B) ⟼ {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s))$
128	127	3ad2ant1	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to \frac{d (s \in (A, B)⟼ F (X + s) - C)}{d_{ℝ} s} = (s \in (A, B) ⟼ {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s))$
129	124	3ad2antl1	$⊢ ((φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) \in ℂ$
130		2cnd	$⊢ s \in (A, B) \to 2 \in ℂ$
131	82	recnd	$⊢ s \in (A, B) \to s \in ℂ$
132	131	halfcld	$⊢ s \in (A, B) \to \frac{s}{2} \in ℂ$
133	132	sincld	$⊢ s \in (A, B) \to \sin (\frac{s}{2}) \in ℂ$
134	130 133	mulcld	$⊢ s \in (A, B) \to 2 \sin (\frac{s}{2}) \in ℂ$
135	134	adantl	$⊢ ((φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \land s \in (A, B)) \to 2 \sin (\frac{s}{2}) \in ℂ$
136	11	3ad2ant1	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to E \in ℝ$
137		1re	$⊢ 1 \in ℝ$
138	25 137	remulcli	$⊢ 2 \cdot 1 \in ℝ$
139	138	a1i	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to 2 \cdot 1 \in ℝ$
140		1red	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to 1 \in ℝ$
141	121	abscld	$⊢ φ \to \|C\| \in ℝ$
142	9 141	readdcld	$⊢ φ \to D + \|C\| \in ℝ$
143	142	3ad2ant1	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to D + \|C\| \in ℝ$
144		simpl	$⊢ (φ \land s \in (A, B)) \to φ$
145	144 111	jca	$⊢ (φ \land s \in (A, B)) \to (φ \land X + s \in (X + A, X + B))$
146		eleq1	$⊢ t = X + s \to (t \in (X + A, X + B) \leftrightarrow X + s \in (X + A, X + B))$
147	146	anbi2d	$⊢ t = X + s \to ((φ \land t \in (X + A, X + B)) \leftrightarrow (φ \land X + s \in (X + A, X + B)))$
148		fveq2	$⊢ t = X + s \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (t) = {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)$
149	148	fveq2d	$⊢ t = X + s \to \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (t)\| = \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)\|$
150	149	breq1d	$⊢ t = X + s \to (\|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (t)\| \leq E \leftrightarrow \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)\| \leq E)$
151	147 150	imbi12d	$⊢ t = X + s \to (((φ \land t \in (X + A, X + B)) \to \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (t)\| \leq E) \leftrightarrow ((φ \land X + s \in (X + A, X + B)) \to \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)\| \leq E))$
152	151 12	vtoclg	$⊢ X + s \in ℝ \to ((φ \land X + s \in (X + A, X + B)) \to \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)\| \leq E)$
153	84 145 152	sylc	$⊢ (φ \land s \in (A, B)) \to \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)\| \leq E$
154	153	3ad2antl1	$⊢ ((φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \land s \in (A, B)) \to \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)\| \leq E$
155	130 133	absmuld	$⊢ s \in (A, B) \to \|2 \sin (\frac{s}{2})\| = \|2\| \|\sin (\frac{s}{2})\|$
156		0le2	$⊢ 0 \leq 2$
157		absid	$⊢ (2 \in ℝ \land 0 \leq 2) \to \|2\| = 2$
158	25 156 157	mp2an	$⊢ \|2\| = 2$
159	158	oveq1i	$⊢ \|2\| \|\sin (\frac{s}{2})\| = 2 \|\sin (\frac{s}{2})\|$
160	133	abscld	$⊢ s \in (A, B) \to \|\sin (\frac{s}{2})\| \in ℝ$
161		1red	$⊢ s \in (A, B) \to 1 \in ℝ$
162	25	a1i	$⊢ s \in (A, B) \to 2 \in ℝ$
163	156	a1i	$⊢ s \in (A, B) \to 0 \leq 2$
164	82	rehalfcld	$⊢ s \in (A, B) \to \frac{s}{2} \in ℝ$
165		abssinbd	$⊢ \frac{s}{2} \in ℝ \to \|\sin (\frac{s}{2})\| \leq 1$
166	164 165	syl	$⊢ s \in (A, B) \to \|\sin (\frac{s}{2})\| \leq 1$
167	160 161 162 163 166	lemul2ad	$⊢ s \in (A, B) \to 2 \|\sin (\frac{s}{2})\| \leq 2 \cdot 1$
168	159 167	eqbrtrid	$⊢ s \in (A, B) \to \|2\| \|\sin (\frac{s}{2})\| \leq 2 \cdot 1$
169	155 168	eqbrtrd	$⊢ s \in (A, B) \to \|2 \sin (\frac{s}{2})\| \leq 2 \cdot 1$
170	169	adantl	$⊢ ((φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \land s \in (A, B)) \to \|2 \sin (\frac{s}{2})\| \leq 2 \cdot 1$
171		abscosbd	$⊢ \frac{s}{2} \in ℝ \to \|\cos (\frac{s}{2})\| \leq 1$
172	103 164 171	3syl	$⊢ (φ \land s \in (A, B)) \to \|\cos (\frac{s}{2})\| \leq 1$
173	172	3ad2antl1	$⊢ ((φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \land s \in (A, B)) \to \|\cos (\frac{s}{2})\| \leq 1$
174	88	abscld	$⊢ (φ \land s \in (A, B)) \to \|F (X + s) - C\| \in ℝ$
175	91	abscld	$⊢ (φ \land s \in (A, B)) \to \|F (X + s)\| \in ℝ$
176	115	abscld	$⊢ (φ \land s \in (A, B)) \to \|C\| \in ℝ$
177	175 176	readdcld	$⊢ (φ \land s \in (A, B)) \to \|F (X + s)\| + \|C\| \in ℝ$
178	9	adantr	$⊢ (φ \land s \in (A, B)) \to D \in ℝ$
179	178 176	readdcld	$⊢ (φ \land s \in (A, B)) \to D + \|C\| \in ℝ$
180	91 115	abs2dif2d	$⊢ (φ \land s \in (A, B)) \to \|F (X + s) - C\| \leq \|F (X + s)\| + \|C\|$
181		fveq2	$⊢ t = X + s \to F (t) = F (X + s)$
182	181	fveq2d	$⊢ t = X + s \to \|F (t)\| = \|F (X + s)\|$
183	182	breq1d	$⊢ t = X + s \to (\|F (t)\| \leq D \leftrightarrow \|F (X + s)\| \leq D)$
184	147 183	imbi12d	$⊢ t = X + s \to (((φ \land t \in (X + A, X + B)) \to \|F (t)\| \leq D) \leftrightarrow ((φ \land X + s \in (X + A, X + B)) \to \|F (X + s)\| \leq D))$
185	184 10	vtoclg	$⊢ X + s \in (X + A, X + B) \to ((φ \land X + s \in (X + A, X + B)) \to \|F (X + s)\| \leq D)$
186	111 145 185	sylc	$⊢ (φ \land s \in (A, B)) \to \|F (X + s)\| \leq D$
187	175 178 176 186	leadd1dd	$⊢ (φ \land s \in (A, B)) \to \|F (X + s)\| + \|C\| \leq D + \|C\|$
188	174 177 179 180 187	letrd	$⊢ (φ \land s \in (A, B)) \to \|F (X + s) - C\| \leq D + \|C\|$
189	188	3ad2antl1	$⊢ ((φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \land s \in (A, B)) \to \|F (X + s) - C\| \leq D + \|C\|$
190	19	simpri	$⊢ \frac{d (s \in (A, B)⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in (A, B) ⟼ \cos (\frac{s}{2}))$
191	190	a1i	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to \frac{d (s \in (A, B)⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in (A, B) ⟼ \cos (\frac{s}{2}))$
192	132	coscld	$⊢ s \in (A, B) \to \cos (\frac{s}{2}) \in ℂ$
193	192	adantl	$⊢ ((φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \land s \in (A, B)) \to \cos (\frac{s}{2}) \in ℂ$
194		simp2	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to c \in ℝ^{+}$
195		oveq1	$⊢ t = s \to \frac{t}{2} = \frac{s}{2}$
196	195	fveq2d	$⊢ t = s \to \sin (\frac{t}{2}) = \sin (\frac{s}{2})$
197	196	oveq2d	$⊢ t = s \to 2 \sin (\frac{t}{2}) = 2 \sin (\frac{s}{2})$
198	197	fveq2d	$⊢ t = s \to \|2 \sin (\frac{t}{2})\| = \|2 \sin (\frac{s}{2})\|$
199	198	breq2d	$⊢ t = s \to (c \leq \|2 \sin (\frac{t}{2})\| \leftrightarrow c \leq \|2 \sin (\frac{s}{2})\|)$
200	199	cbvralvw	$⊢ \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\| \leftrightarrow \forall s \in [A, B] c \leq \|2 \sin (\frac{s}{2})\|$
201		nfv	$⊢ Ⅎ s φ$
202		nfra1	$⊢ Ⅎ s \forall s \in [A, B] c \leq \|2 \sin (\frac{s}{2})\|$
203	201 202	nfan	$⊢ Ⅎ s (φ \land \forall s \in [A, B] c \leq \|2 \sin (\frac{s}{2})\|)$
204		simplr	$⊢ ((φ \land \forall s \in [A, B] c \leq \|2 \sin (\frac{s}{2})\|) \land s \in (A, B)) \to \forall s \in [A, B] c \leq \|2 \sin (\frac{s}{2})\|$
205	15 103	sselid	$⊢ (φ \land s \in (A, B)) \to s \in [A, B]$
206	205	adantlr	$⊢ ((φ \land \forall s \in [A, B] c \leq \|2 \sin (\frac{s}{2})\|) \land s \in (A, B)) \to s \in [A, B]$
207		rspa	$⊢ (\forall s \in [A, B] c \leq \|2 \sin (\frac{s}{2})\| \land s \in [A, B]) \to c \leq \|2 \sin (\frac{s}{2})\|$
208	204 206 207	syl2anc	$⊢ ((φ \land \forall s \in [A, B] c \leq \|2 \sin (\frac{s}{2})\|) \land s \in (A, B)) \to c \leq \|2 \sin (\frac{s}{2})\|$
209	208	ex	$⊢ (φ \land \forall s \in [A, B] c \leq \|2 \sin (\frac{s}{2})\|) \to (s \in (A, B) \to c \leq \|2 \sin (\frac{s}{2})\|)$
210	203 209	ralrimi	$⊢ (φ \land \forall s \in [A, B] c \leq \|2 \sin (\frac{s}{2})\|) \to \forall s \in (A, B) c \leq \|2 \sin (\frac{s}{2})\|$
211	200 210	sylan2b	$⊢ (φ \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to \forall s \in (A, B) c \leq \|2 \sin (\frac{s}{2})\|$
212	211	3adant2	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to \forall s \in (A, B) c \leq \|2 \sin (\frac{s}{2})\|$
213		eqid	$⊢ \frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} = \frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s}$
214	79 89 128 129 135 136 139 140 143 154 170 173 189 191 193 194 212 213	dvdivbd	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to \exists b \in ℝ \forall s \in (A, B) \|\frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)\| \leq b$
215	214	rexlimdv3a	$⊢ φ \to (\exists c \in ℝ^{+} \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\| \to \exists b \in ℝ \forall s \in (A, B) \|\frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)\| \leq b)$
216	77 215	mpd	$⊢ φ \to \exists b \in ℝ \forall s \in (A, B) \|\frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)\| \leq b$
217		nfcv	$⊢ \underline{Ⅎ} s ℝ$
218		nfcv	$⊢ \underline{Ⅎ} s D$
219		nfmpt1	$⊢ \underline{Ⅎ} s (s \in (A, B) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
220	14 219	nfcxfr	$⊢ \underline{Ⅎ} s O$
221	217 218 220	nfov	$⊢ \underline{Ⅎ} s O_{ℝ}^{'}$
222	221	nfdm	$⊢ \underline{Ⅎ} s dom O_{ℝ}^{'}$
223		nfcv	$⊢ \underline{Ⅎ} s (A, B)$
224	222 223	raleqf	$⊢ dom O_{ℝ}^{'} = (A, B) \to (\forall s \in dom O_{ℝ}^{'} \|\frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)\| \leq b \leftrightarrow \forall s \in (A, B) \|\frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)\| \leq b)$
225	22 224	syl	$⊢ φ \to (\forall s \in dom O_{ℝ}^{'} \|\frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)\| \leq b \leftrightarrow \forall s \in (A, B) \|\frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)\| \leq b)$
226	225	rexbidv	$⊢ φ \to (\exists b \in ℝ \forall s \in dom O_{ℝ}^{'} \|\frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)\| \leq b \leftrightarrow \exists b \in ℝ \forall s \in (A, B) \|\frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)\| \leq b)$
227	216 226	mpbird	$⊢ φ \to \exists b \in ℝ \forall s \in dom O_{ℝ}^{'} \|\frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)\| \leq b$
228	14	a1i	$⊢ φ \to O = (s \in (A, B) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
229	228	oveq2d	$⊢ φ \to ℝ D O = \frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s}$
230	229	fveq1d	$⊢ φ \to O_{ℝ}^{'} (s) = \frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)$
231	230	fveq2d	$⊢ φ \to \|O_{ℝ}^{'} (s)\| = \|\frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)\|$
232	231	breq1d	$⊢ φ \to (\|O_{ℝ}^{'} (s)\| \leq b \leftrightarrow \|\frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)\| \leq b)$
233	232	rexralbidv	$⊢ φ \to (\exists b \in ℝ \forall s \in dom O_{ℝ}^{'} \|O_{ℝ}^{'} (s)\| \leq b \leftrightarrow \exists b \in ℝ \forall s \in dom O_{ℝ}^{'} \|\frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)\| \leq b)$
234	227 233	mpbird	$⊢ φ \to \exists b \in ℝ \forall s \in dom O_{ℝ}^{'} \|O_{ℝ}^{'} (s)\| \leq b$
235	22 234	jca	$⊢ φ \to (dom O_{ℝ}^{'} = (A, B) \land \exists b \in ℝ \forall s \in dom O_{ℝ}^{'} \|O_{ℝ}^{'} (s)\| \leq b)$

Metamath Proof Explorer

Theorem fourierdlem68

Proof