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