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		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
120	119	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
121	118 120	eleqtri	$⊢ (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
122	121	a1i	$⊢ φ \to (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
123	13	recnd	$⊢ φ \to C \in ℂ$
124	91 122 123	dvmptconst	$⊢ φ \to \frac{d (s \in (A, B)⟼ C)}{d_{ℝ} s} = (s \in (A, B) ⟼ 0)$
125	91 92 113 115 116 117 124	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)$
126	113	recnd	$⊢ (φ \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) \in ℂ$
127	126	subid1d	$⊢ (φ \land s \in (A, B)) \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s) - 0 = {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)$
128	127	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))$
129	125 128	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))$
130	129	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))$
131	126	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 ℂ$
132		2cnd	$⊢ s \in (A, B) \to 2 \in ℂ$
133	83	recnd	$⊢ s \in (A, B) \to s \in ℂ$
134	133	halfcld	$⊢ s \in (A, B) \to \frac{s}{2} \in ℂ$
135	134	sincld	$⊢ s \in (A, B) \to \sin (\frac{s}{2}) \in ℂ$
136	132 135	mulcld	$⊢ s \in (A, B) \to 2 \sin (\frac{s}{2}) \in ℂ$
137	136	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 ℂ$
138	11	3ad2ant1	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to E \in ℝ$
139		1re	$⊢ 1 \in ℝ$
140	25 139	remulcli	$⊢ 2 \cdot 1 \in ℝ$
141	140	a1i	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to 2 \cdot 1 \in ℝ$
142		1red	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to 1 \in ℝ$
143	123	abscld	$⊢ φ \to \|C\| \in ℝ$
144	9 143	readdcld	$⊢ φ \to D + \|C\| \in ℝ$
145	144	3ad2ant1	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to D + \|C\| \in ℝ$
146		simpl	$⊢ (φ \land s \in (A, B)) \to φ$
147	146 112	jca	$⊢ (φ \land s \in (A, B)) \to (φ \land X + s \in (X + A, X + B))$
148		eleq1	$⊢ t = X + s \to (t \in (X + A, X + B) \leftrightarrow X + s \in (X + A, X + B))$
149	148	anbi2d	$⊢ t = X + s \to ((φ \land t \in (X + A, X + B)) \leftrightarrow (φ \land X + s \in (X + A, X + B)))$
150		fveq2	$⊢ t = X + s \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (t) = {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)$
151	150	fveq2d	$⊢ t = X + s \to \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (t)\| = \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)\|$
152	151	breq1d	$⊢ t = X + s \to (\|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (t)\| \leq E \leftrightarrow \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)\| \leq E)$
153	149 152	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))$
154	153 12	vtoclg	$⊢ X + s \in ℝ \to ((φ \land X + s \in (X + A, X + B)) \to \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)\| \leq E)$
155	85 147 154	sylc	$⊢ (φ \land s \in (A, B)) \to \|{({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)\| \leq E$
156	155	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$
157	132 135	absmuld	$⊢ s \in (A, B) \to \|2 \sin (\frac{s}{2})\| = \|2\| \|\sin (\frac{s}{2})\|$
158		0le2	$⊢ 0 \leq 2$
159		absid	$⊢ (2 \in ℝ \land 0 \leq 2) \to \|2\| = 2$
160	25 158 159	mp2an	$⊢ \|2\| = 2$
161	160	oveq1i	$⊢ \|2\| \|\sin (\frac{s}{2})\| = 2 \|\sin (\frac{s}{2})\|$
162	135	abscld	$⊢ s \in (A, B) \to \|\sin (\frac{s}{2})\| \in ℝ$
163		1red	$⊢ s \in (A, B) \to 1 \in ℝ$
164	25	a1i	$⊢ s \in (A, B) \to 2 \in ℝ$
165	158	a1i	$⊢ s \in (A, B) \to 0 \leq 2$
166	83	rehalfcld	$⊢ s \in (A, B) \to \frac{s}{2} \in ℝ$
167		abssinbd	$⊢ \frac{s}{2} \in ℝ \to \|\sin (\frac{s}{2})\| \leq 1$
168	166 167	syl	$⊢ s \in (A, B) \to \|\sin (\frac{s}{2})\| \leq 1$
169	162 163 164 165 168	lemul2ad	$⊢ s \in (A, B) \to 2 \|\sin (\frac{s}{2})\| \leq 2 \cdot 1$
170	161 169	eqbrtrid	$⊢ s \in (A, B) \to \|2\| \|\sin (\frac{s}{2})\| \leq 2 \cdot 1$
171	157 170	eqbrtrd	$⊢ s \in (A, B) \to \|2 \sin (\frac{s}{2})\| \leq 2 \cdot 1$
172	171	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$
173		abscosbd	$⊢ \frac{s}{2} \in ℝ \to \|\cos (\frac{s}{2})\| \leq 1$
174	104 166 173	3syl	$⊢ (φ \land s \in (A, B)) \to \|\cos (\frac{s}{2})\| \leq 1$
175	174	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$
176	89	abscld	$⊢ (φ \land s \in (A, B)) \to \|F (X + s) - C\| \in ℝ$
177	92	abscld	$⊢ (φ \land s \in (A, B)) \to \|F (X + s)\| \in ℝ$
178	116	abscld	$⊢ (φ \land s \in (A, B)) \to \|C\| \in ℝ$
179	177 178	readdcld	$⊢ (φ \land s \in (A, B)) \to \|F (X + s)\| + \|C\| \in ℝ$
180	9	adantr	$⊢ (φ \land s \in (A, B)) \to D \in ℝ$
181	180 178	readdcld	$⊢ (φ \land s \in (A, B)) \to D + \|C\| \in ℝ$
182	92 116	abs2dif2d	$⊢ (φ \land s \in (A, B)) \to \|F (X + s) - C\| \leq \|F (X + s)\| + \|C\|$
183		fveq2	$⊢ t = X + s \to F (t) = F (X + s)$
184	183	fveq2d	$⊢ t = X + s \to \|F (t)\| = \|F (X + s)\|$
185	184	breq1d	$⊢ t = X + s \to (\|F (t)\| \leq D \leftrightarrow \|F (X + s)\| \leq D)$
186	149 185	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))$
187	186 10	vtoclg	$⊢ X + s \in (X + A, X + B) \to ((φ \land X + s \in (X + A, X + B)) \to \|F (X + s)\| \leq D)$
188	112 147 187	sylc	$⊢ (φ \land s \in (A, B)) \to \|F (X + s)\| \leq D$
189	177 180 178 188	leadd1dd	$⊢ (φ \land s \in (A, B)) \to \|F (X + s)\| + \|C\| \leq D + \|C\|$
190	176 179 181 182 189	letrd	$⊢ (φ \land s \in (A, B)) \to \|F (X + s) - C\| \leq D + \|C\|$
191	190	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\|$
192	19	simpri	$⊢ \frac{d (s \in (A, B)⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in (A, B) ⟼ \cos (\frac{s}{2}))$
193	192	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}))$
194	134	coscld	$⊢ s \in (A, B) \to \cos (\frac{s}{2}) \in ℂ$
195	194	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 ℂ$
196		simp2	$⊢ (φ \land c \in ℝ^{+} \land \forall t \in [A, B] c \leq \|2 \sin (\frac{t}{2})\|) \to c \in ℝ^{+}$
197		oveq1	$⊢ t = s \to \frac{t}{2} = \frac{s}{2}$
198	197	fveq2d	$⊢ t = s \to \sin (\frac{t}{2}) = \sin (\frac{s}{2})$
199	198	oveq2d	$⊢ t = s \to 2 \sin (\frac{t}{2}) = 2 \sin (\frac{s}{2})$
200	199	fveq2d	$⊢ t = s \to \|2 \sin (\frac{t}{2})\| = \|2 \sin (\frac{s}{2})\|$
201	200	breq2d	$⊢ t = s \to (c \leq \|2 \sin (\frac{t}{2})\| \leftrightarrow c \leq \|2 \sin (\frac{s}{2})\|)$
202	201	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})\|$
203		nfv	$⊢ Ⅎ s φ$
204		nfra1	$⊢ Ⅎ s \forall s \in [A, B] c \leq \|2 \sin (\frac{s}{2})\|$
205	203 204	nfan	$⊢ Ⅎ s (φ \land \forall s \in [A, B] c \leq \|2 \sin (\frac{s}{2})\|)$
206		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})\|$
207	15 104	sselid	$⊢ (φ \land s \in (A, B)) \to s \in [A, B]$
208	207	adantlr	$⊢ ((φ \land \forall s \in [A, B] c \leq \|2 \sin (\frac{s}{2})\|) \land s \in (A, B)) \to s \in [A, B]$
209		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})\|$
210	206 208 209	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})\|$
211	210	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})\|)$
212	205 211	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})\|$
213	202 212	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})\|$
214	213	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})\|$
215		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}$
216	80 90 130 131 137 138 141 142 145 156 172 175 191 193 195 196 214 215	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$
217	216	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)$
218	78 217	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$
219		nfcv	$⊢ \underline{Ⅎ} s ℝ$
220		nfcv	$⊢ \underline{Ⅎ} s D$
221		nfmpt1	$⊢ \underline{Ⅎ} s (s \in (A, B) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
222	14 221	nfcxfr	$⊢ \underline{Ⅎ} s O$
223	219 220 222	nfov	$⊢ \underline{Ⅎ} s O_{ℝ}^{'}$
224	223	nfdm	$⊢ \underline{Ⅎ} s dom O_{ℝ}^{'}$
225		nfcv	$⊢ \underline{Ⅎ} s (A, B)$
226	224 225	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)$
227	22 226	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)$
228	227	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)$
229	218 228	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$
230	14	a1i	$⊢ φ \to O = (s \in (A, B) ⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})$
231	230	oveq2d	$⊢ φ \to ℝ D O = \frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s}$
232	231	fveq1d	$⊢ φ \to O_{ℝ}^{'} (s) = \frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)$
233	232	fveq2d	$⊢ φ \to \|O_{ℝ}^{'} (s)\| = \|\frac{d (s \in (A, B)⟼ \frac{F (X + s) - C}{2 \sin (\frac{s}{2})})}{d_{ℝ} s} (s)\|$
234	233	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)$
235	234	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)$
236	229 235	mpbird	$⊢ φ \to \exists b \in ℝ \forall s \in dom O_{ℝ}^{'} \|O_{ℝ}^{'} (s)\| \leq b$
237	22 236	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