fourierdlem72

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

	Ref	Expression
Hypotheses	fourierdlem72.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem72.xre	$⊢ φ \to X \in ℝ$
	fourierdlem72.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π + X \land p (m) = π + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem72.m	$⊢ φ \to M \in ℕ$
	fourierdlem72.v	$⊢ φ \to V \in P (M)$
	fourierdlem72.dvcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℝ$
	fourierdlem72.a	$⊢ φ \to A \in ℝ$
	fourierdlem72.b	$⊢ φ \to B \in ℝ$
	fourierdlem72.altb	$⊢ φ \to A < B$
	fourierdlem72.ab	$⊢ φ \to (A, B) \subseteq [- π, π]$
	fourierdlem72.n0	$⊢ φ \to \neg 0 \in [A, B]$
	fourierdlem72.c	$⊢ φ \to C \in ℝ$
	fourierdlem72.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
	fourierdlem72.u	$⊢ φ \to U \in (0 ..^M)$
	fourierdlem72.abss	$⊢ φ \to (A, B) \subseteq (Q (U), Q (U + 1))$
	fourierdlem72.h	$⊢ H = (s \in (A, B) ⟼ \frac{F (X + s) - C}{s})$
	fourierdlem72.k	$⊢ K = (s \in (A, B) ⟼ \frac{s}{2 \sin (\frac{s}{2})})$
	fourierdlem72.o	$⊢ O = (s \in (A, B) ⟼ H (s) K (s))$
Assertion	fourierdlem72	$⊢ φ \to O_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem72.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem72.xre	$⊢ φ \to X \in ℝ$
3		fourierdlem72.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π + X \land p (m) = π + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
4		fourierdlem72.m	$⊢ φ \to M \in ℕ$
5		fourierdlem72.v	$⊢ φ \to V \in P (M)$
6		fourierdlem72.dvcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℝ$
7		fourierdlem72.a	$⊢ φ \to A \in ℝ$
8		fourierdlem72.b	$⊢ φ \to B \in ℝ$
9		fourierdlem72.altb	$⊢ φ \to A < B$
10		fourierdlem72.ab	$⊢ φ \to (A, B) \subseteq [- π, π]$
11		fourierdlem72.n0	$⊢ φ \to \neg 0 \in [A, B]$
12		fourierdlem72.c	$⊢ φ \to C \in ℝ$
13		fourierdlem72.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
14		fourierdlem72.u	$⊢ φ \to U \in (0 ..^M)$
15		fourierdlem72.abss	$⊢ φ \to (A, B) \subseteq (Q (U), Q (U + 1))$
16		fourierdlem72.h	$⊢ H = (s \in (A, B) ⟼ \frac{F (X + s) - C}{s})$
17		fourierdlem72.k	$⊢ K = (s \in (A, B) ⟼ \frac{s}{2 \sin (\frac{s}{2})})$
18		fourierdlem72.o	$⊢ O = (s \in (A, B) ⟼ H (s) K (s))$
19		ovex	$⊢ (A, B) \in V$
20	19	a1i	$⊢ φ \to (A, B) \in V$
21	1	adantr	$⊢ (φ \land s \in (A, B)) \to F : ℝ ⟶ ℝ$
22	2	adantr	$⊢ (φ \land s \in (A, B)) \to X \in ℝ$
23		elioore	$⊢ s \in (A, B) \to s \in ℝ$
24	23	adantl	$⊢ (φ \land s \in (A, B)) \to s \in ℝ$
25	22 24	readdcld	$⊢ (φ \land s \in (A, B)) \to X + s \in ℝ$
26	21 25	ffvelrnd	$⊢ (φ \land s \in (A, B)) \to F (X + s) \in ℝ$
27	12	adantr	$⊢ (φ \land s \in (A, B)) \to C \in ℝ$
28	26 27	resubcld	$⊢ (φ \land s \in (A, B)) \to F (X + s) - C \in ℝ$
29		ioossicc	$⊢ (A, B) \subseteq [A, B]$
30	29	sseli	$⊢ s \in (A, B) \to s \in [A, B]$
31	30	ad2antlr	$⊢ ((φ \land s \in (A, B)) \land \neg s \neq 0) \to s \in [A, B]$
32		id	$⊢ s \neq 0 \to s \neq 0$
33	32	necon1bi	$⊢ \neg s \neq 0 \to s = 0$
34	33	eleq1d	$⊢ \neg s \neq 0 \to (s \in [A, B] \leftrightarrow 0 \in [A, B])$
35	34	adantl	$⊢ ((φ \land s \in (A, B)) \land \neg s \neq 0) \to (s \in [A, B] \leftrightarrow 0 \in [A, B])$
36	31 35	mpbid	$⊢ ((φ \land s \in (A, B)) \land \neg s \neq 0) \to 0 \in [A, B]$
37	11	ad2antrr	$⊢ ((φ \land s \in (A, B)) \land \neg s \neq 0) \to \neg 0 \in [A, B]$
38	36 37	condan	$⊢ (φ \land s \in (A, B)) \to s \neq 0$
39	28 24 38	redivcld	$⊢ (φ \land s \in (A, B)) \to \frac{F (X + s) - C}{s} \in ℝ$
40	39 16	fmptd	$⊢ φ \to H : (A, B) ⟶ ℝ$
41	40	ffvelrnda	$⊢ (φ \land s \in (A, B)) \to H (s) \in ℝ$
42		2re	$⊢ 2 \in ℝ$
43	42	a1i	$⊢ (φ \land s \in (A, B)) \to 2 \in ℝ$
44	24	rehalfcld	$⊢ (φ \land s \in (A, B)) \to \frac{s}{2} \in ℝ$
45	44	resincld	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \in ℝ$
46	43 45	remulcld	$⊢ (φ \land s \in (A, B)) \to 2 \sin (\frac{s}{2}) \in ℝ$
47		2cnd	$⊢ (φ \land s \in (A, B)) \to 2 \in ℂ$
48	24	recnd	$⊢ (φ \land s \in (A, B)) \to s \in ℂ$
49	48	halfcld	$⊢ (φ \land s \in (A, B)) \to \frac{s}{2} \in ℂ$
50	49	sincld	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \in ℂ$
51		2ne0	$⊢ 2 \neq 0$
52	51	a1i	$⊢ (φ \land s \in (A, B)) \to 2 \neq 0$
53	10	sselda	$⊢ (φ \land s \in (A, B)) \to s \in [- π, π]$
54		fourierdlem44	$⊢ (s \in [- π, π] \land s \neq 0) \to \sin (\frac{s}{2}) \neq 0$
55	53 38 54	syl2anc	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \neq 0$
56	47 50 52 55	mulne0d	$⊢ (φ \land s \in (A, B)) \to 2 \sin (\frac{s}{2}) \neq 0$
57	24 46 56	redivcld	$⊢ (φ \land s \in (A, B)) \to \frac{s}{2 \sin (\frac{s}{2})} \in ℝ$
58	57 17	fmptd	$⊢ φ \to K : (A, B) ⟶ ℝ$
59	58	ffvelrnda	$⊢ (φ \land s \in (A, B)) \to K (s) \in ℝ$
60	40	feqmptd	$⊢ φ \to H = (s \in (A, B) ⟼ H (s))$
61	58	feqmptd	$⊢ φ \to K = (s \in (A, B) ⟼ K (s))$
62	20 41 59 60 61	offval2	$⊢ φ \to H \times_{f} K = (s \in (A, B) ⟼ H (s) K (s))$
63	18 62	eqtr4id	$⊢ φ \to O = H \times_{f} K$
64	63	oveq2d	$⊢ φ \to ℝ D O = ℝ D (H \times_{f} K)$
65		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
66	65	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
67	26	recnd	$⊢ (φ \land s \in (A, B)) \to F (X + s) \in ℂ$
68	12	recnd	$⊢ φ \to C \in ℂ$
69	68	adantr	$⊢ (φ \land s \in (A, B)) \to C \in ℂ$
70	67 69	subcld	$⊢ (φ \land s \in (A, B)) \to F (X + s) - C \in ℂ$
71		ioossre	$⊢ (A, B) \subseteq ℝ$
72	71	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
73	72	sselda	$⊢ (φ \land s \in (A, B)) \to s \in ℝ$
74	73	recnd	$⊢ (φ \land s \in (A, B)) \to s \in ℂ$
75	70 74 38	divcld	$⊢ (φ \land s \in (A, B)) \to \frac{F (X + s) - C}{s} \in ℂ$
76	75 16	fmptd	$⊢ φ \to H : (A, B) ⟶ ℂ$
77	74	halfcld	$⊢ (φ \land s \in (A, B)) \to \frac{s}{2} \in ℂ$
78	77	sincld	$⊢ (φ \land s \in (A, B)) \to \sin (\frac{s}{2}) \in ℂ$
79	47 78	mulcld	$⊢ (φ \land s \in (A, B)) \to 2 \sin (\frac{s}{2}) \in ℂ$
80	74 79 56	divcld	$⊢ (φ \land s \in (A, B)) \to \frac{s}{2 \sin (\frac{s}{2})} \in ℂ$
81	80 17	fmptd	$⊢ φ \to K : (A, B) ⟶ ℂ$
82		ax-resscn	$⊢ ℝ \subseteq ℂ$
83	82	a1i	$⊢ φ \to ℝ \subseteq ℂ$
84		ssid	$⊢ ℂ \subseteq ℂ$
85	84	a1i	$⊢ φ \to ℂ \subseteq ℂ$
86		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to (A, B) \underset{cn}{⟶} ℝ \subseteq (A, B) \underset{cn}{⟶} ℂ$
87	83 85 86	syl2anc	$⊢ φ \to (A, B) \underset{cn}{⟶} ℝ \subseteq (A, B) \underset{cn}{⟶} ℂ$
88	38	nelrdva	$⊢ φ \to \neg 0 \in (A, B)$
89	1 83	fssd	$⊢ φ \to F : ℝ ⟶ ℂ$
90		ssid	$⊢ ℝ \subseteq ℝ$
91	90	a1i	$⊢ φ \to ℝ \subseteq ℝ$
92		ioossre	$⊢ (X + A, X + B) \subseteq ℝ$
93	92	a1i	$⊢ φ \to (X + A, X + B) \subseteq ℝ$
94		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
95	94	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
96	94 95	dvres	$⊢ ((ℝ \subseteq ℂ \land F : ℝ ⟶ ℂ) \land (ℝ \subseteq ℝ \land (X + A, X + B) \subseteq ℝ)) \to ℝ D ({F ↾}_{(X + A, X + B)}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((X + A, X + B))}$
97	83 89 91 93 96	syl22anc	$⊢ φ \to ℝ D ({F ↾}_{(X + A, X + B)}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((X + A, X + B))}$
98		ioontr	$⊢ int (topGen (ran (.))) ((X + A, X + B)) = (X + A, X + B)$
99	98	reseq2i	$⊢ {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((X + A, X + B))} = {F_{ℝ}^{'} ↾}_{(X + A, X + B)}$
100	97 99	eqtrdi	$⊢ φ \to ℝ D ({F ↾}_{(X + A, X + B)}) = {F_{ℝ}^{'} ↾}_{(X + A, X + B)}$
101	3	fourierdlem2	$⊢ M \in ℕ \to (V \in P (M) \leftrightarrow (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))))$
102	4 101	syl	$⊢ φ \to (V \in P (M) \leftrightarrow (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))))$
103	5 102	mpbid	$⊢ φ \to (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1)))$
104	103	simpld	$⊢ φ \to V \in (ℝ^{(0 \dots M)})$
105		elmapi	$⊢ V \in (ℝ^{(0 \dots M)}) \to V : (0 \dots M) ⟶ ℝ$
106	104 105	syl	$⊢ φ \to V : (0 \dots M) ⟶ ℝ$
107		elfzofz	$⊢ U \in (0 ..^M) \to U \in (0 \dots M)$
108	14 107	syl	$⊢ φ \to U \in (0 \dots M)$
109	106 108	ffvelrnd	$⊢ φ \to V (U) \in ℝ$
110	109	rexrd	$⊢ φ \to V (U) \in ℝ^{*}$
111		fzofzp1	$⊢ U \in (0 ..^M) \to U + 1 \in (0 \dots M)$
112	14 111	syl	$⊢ φ \to U + 1 \in (0 \dots M)$
113	106 112	ffvelrnd	$⊢ φ \to V (U + 1) \in ℝ$
114	113	rexrd	$⊢ φ \to V (U + 1) \in ℝ^{*}$
115		pire	$⊢ π \in ℝ$
116	115	a1i	$⊢ φ \to π \in ℝ$
117	116	renegcld	$⊢ φ \to - π \in ℝ$
118	117 116 2 3 4 5 108 13	fourierdlem13	$⊢ φ \to (Q (U) = V (U) - X \land V (U) = X + Q (U))$
119	118	simprd	$⊢ φ \to V (U) = X + Q (U)$
120	118	simpld	$⊢ φ \to Q (U) = V (U) - X$
121	109 2	resubcld	$⊢ φ \to V (U) - X \in ℝ$
122	120 121	eqeltrd	$⊢ φ \to Q (U) \in ℝ$
123	117 116 2 3 4 5 112 13	fourierdlem13	$⊢ φ \to (Q (U + 1) = V (U + 1) - X \land V (U + 1) = X + Q (U + 1))$
124	123	simpld	$⊢ φ \to Q (U + 1) = V (U + 1) - X$
125	113 2	resubcld	$⊢ φ \to V (U + 1) - X \in ℝ$
126	124 125	eqeltrd	$⊢ φ \to Q (U + 1) \in ℝ$
127	122 126 7 8 9 15	fourierdlem10	$⊢ φ \to (Q (U) \leq A \land B \leq Q (U + 1))$
128	127	simpld	$⊢ φ \to Q (U) \leq A$
129	122 7 2 128	leadd2dd	$⊢ φ \to X + Q (U) \leq X + A$
130	119 129	eqbrtrd	$⊢ φ \to V (U) \leq X + A$
131	127	simprd	$⊢ φ \to B \leq Q (U + 1)$
132	8 126 2 131	leadd2dd	$⊢ φ \to X + B \leq X + Q (U + 1)$
133	123	simprd	$⊢ φ \to V (U + 1) = X + Q (U + 1)$
134	132 133	breqtrrd	$⊢ φ \to X + B \leq V (U + 1)$
135		ioossioo	$⊢ ((V (U) \in ℝ^{} \land V (U + 1) \in ℝ^{}) \land (V (U) \leq X + A \land X + B \leq V (U + 1))) \to (X + A, X + B) \subseteq (V (U), V (U + 1))$
136	110 114 130 134 135	syl22anc	$⊢ φ \to (X + A, X + B) \subseteq (V (U), V (U + 1))$
137	136	resabs1d	$⊢ φ \to {({F_{ℝ}^{'} ↾}_{(V (U), V (U + 1))}) ↾}_{(X + A, X + B)} = {F_{ℝ}^{'} ↾}_{(X + A, X + B)}$
138	137	eqcomd	$⊢ φ \to {F_{ℝ}^{'} ↾}_{(X + A, X + B)} = {({F_{ℝ}^{'} ↾}_{(V (U), V (U + 1))}) ↾}_{(X + A, X + B)}$
139	14	ancli	$⊢ φ \to (φ \land U \in (0 ..^M))$
140		eleq1	$⊢ i = U \to (i \in (0 ..^M) \leftrightarrow U \in (0 ..^M))$
141	140	anbi2d	$⊢ i = U \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land U \in (0 ..^M)))$
142		fveq2	$⊢ i = U \to V (i) = V (U)$
143		oveq1	$⊢ i = U \to i + 1 = U + 1$
144	143	fveq2d	$⊢ i = U \to V (i + 1) = V (U + 1)$
145	142 144	oveq12d	$⊢ i = U \to (V (i), V (i + 1)) = (V (U), V (U + 1))$
146	145	reseq2d	$⊢ i = U \to {F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))} = {F_{ℝ}^{'} ↾}_{(V (U), V (U + 1))}$
147	145	oveq1d	$⊢ i = U \to (V (i), V (i + 1)) \underset{cn}{⟶} ℝ = (V (U), V (U + 1)) \underset{cn}{⟶} ℝ$
148	146 147	eleq12d	$⊢ i = U \to (({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℝ \leftrightarrow ({F_{ℝ}^{'} ↾}_{(V (U), V (U + 1))}) : (V (U), V (U + 1)) \underset{cn}{⟶} ℝ)$
149	141 148	imbi12d	$⊢ i = U \to (((φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℝ) \leftrightarrow ((φ \land U \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(V (U), V (U + 1))}) : (V (U), V (U + 1)) \underset{cn}{⟶} ℝ))$
150	149 6	vtoclg	$⊢ U \in (0 ..^M) \to ((φ \land U \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(V (U), V (U + 1))}) : (V (U), V (U + 1)) \underset{cn}{⟶} ℝ)$
151	14 139 150	sylc	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{(V (U), V (U + 1))}) : (V (U), V (U + 1)) \underset{cn}{⟶} ℝ$
152		rescncf	$⊢ (X + A, X + B) \subseteq (V (U), V (U + 1)) \to (({F_{ℝ}^{'} ↾}_{(V (U), V (U + 1))}) : (V (U), V (U + 1)) \underset{cn}{⟶} ℝ \to ({({F_{ℝ}^{'} ↾}_{(V (U), V (U + 1))}) ↾}_{(X + A, X + B)}) : (X + A, X + B) \underset{cn}{⟶} ℝ)$
153	136 151 152	sylc	$⊢ φ \to ({({F_{ℝ}^{'} ↾}_{(V (U), V (U + 1))}) ↾}_{(X + A, X + B)}) : (X + A, X + B) \underset{cn}{⟶} ℝ$
154	138 153	eqeltrd	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{(X + A, X + B)}) : (X + A, X + B) \underset{cn}{⟶} ℝ$
155	100 154	eqeltrd	$⊢ φ \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) \underset{cn}{⟶} ℝ$
156	1 2 7 8 88 155 12 16	fourierdlem59	$⊢ φ \to H_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℝ$
157	87 156	sseldd	$⊢ φ \to H_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
158		iooretop	$⊢ (A, B) \in topGen (ran (.))$
159	158	a1i	$⊢ φ \to (A, B) \in topGen (ran (.))$
160	17 10 88 159	fourierdlem58	$⊢ φ \to K_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℝ$
161	87 160	sseldd	$⊢ φ \to K_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
162	66 76 81 157 161	dvmulcncf	$⊢ φ \to {(H \times_{f} K)}_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
163	64 162	eqeltrd	$⊢ φ \to O_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem fourierdlem72

Proof