fourierdlem58

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

	Ref	Expression
Hypotheses	fourierdlem58.k	$⊢ K = (s \in A ⟼ \frac{s}{2 \sin (\frac{s}{2})})$
	fourierdlem58.ass	$⊢ φ \to A \subseteq [- π, π]$
	fourierdlem58.0nA	$⊢ φ \to \neg 0 \in A$
	fourierdlem58.4	$⊢ φ \to A \in topGen (ran (.))$
Assertion	fourierdlem58	$⊢ φ \to K_{ℝ}^{'} : A \underset{cn}{⟶} ℝ$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem58.k	$⊢ K = (s \in A ⟼ \frac{s}{2 \sin (\frac{s}{2})})$
2		fourierdlem58.ass	$⊢ φ \to A \subseteq [- π, π]$
3		fourierdlem58.0nA	$⊢ φ \to \neg 0 \in A$
4		fourierdlem58.4	$⊢ φ \to A \in topGen (ran (.))$
5		pire	$⊢ π \in ℝ$
6	5	a1i	$⊢ (φ \land s \in A) \to π \in ℝ$
7	6	renegcld	$⊢ (φ \land s \in A) \to - π \in ℝ$
8	7 6	iccssred	$⊢ (φ \land s \in A) \to [- π, π] \subseteq ℝ$
9	2	sselda	$⊢ (φ \land s \in A) \to s \in [- π, π]$
10	8 9	sseldd	$⊢ (φ \land s \in A) \to s \in ℝ$
11		2re	$⊢ 2 \in ℝ$
12	11	a1i	$⊢ (φ \land s \in A) \to 2 \in ℝ$
13	10	rehalfcld	$⊢ (φ \land s \in A) \to \frac{s}{2} \in ℝ$
14	13	resincld	$⊢ (φ \land s \in A) \to \sin (\frac{s}{2}) \in ℝ$
15	12 14	remulcld	$⊢ (φ \land s \in A) \to 2 \sin (\frac{s}{2}) \in ℝ$
16		2cnd	$⊢ (φ \land s \in A) \to 2 \in ℂ$
17	10	recnd	$⊢ (φ \land s \in A) \to s \in ℂ$
18	17	halfcld	$⊢ (φ \land s \in A) \to \frac{s}{2} \in ℂ$
19	18	sincld	$⊢ (φ \land s \in A) \to \sin (\frac{s}{2}) \in ℂ$
20		2ne0	$⊢ 2 \neq 0$
21	20	a1i	$⊢ (φ \land s \in A) \to 2 \neq 0$
22		eqcom	$⊢ s = 0 \leftrightarrow 0 = s$
23	22	biimpi	$⊢ s = 0 \to 0 = s$
24	23	adantl	$⊢ (s \in A \land s = 0) \to 0 = s$
25		simpl	$⊢ (s \in A \land s = 0) \to s \in A$
26	24 25	eqeltrd	$⊢ (s \in A \land s = 0) \to 0 \in A$
27	26	adantll	$⊢ ((φ \land s \in A) \land s = 0) \to 0 \in A$
28	3	ad2antrr	$⊢ ((φ \land s \in A) \land s = 0) \to \neg 0 \in A$
29	27 28	pm2.65da	$⊢ (φ \land s \in A) \to \neg s = 0$
30	29	neqned	$⊢ (φ \land s \in A) \to s \neq 0$
31		fourierdlem44	$⊢ (s \in [- π, π] \land s \neq 0) \to \sin (\frac{s}{2}) \neq 0$
32	9 30 31	syl2anc	$⊢ (φ \land s \in A) \to \sin (\frac{s}{2}) \neq 0$
33	16 19 21 32	mulne0d	$⊢ (φ \land s \in A) \to 2 \sin (\frac{s}{2}) \neq 0$
34	10 15 33	redivcld	$⊢ (φ \land s \in A) \to \frac{s}{2 \sin (\frac{s}{2})} \in ℝ$
35	34 1	fmptd	$⊢ φ \to K : A ⟶ ℝ$
36	5	a1i	$⊢ φ \to π \in ℝ$
37	36	renegcld	$⊢ φ \to - π \in ℝ$
38	37 36	iccssred	$⊢ φ \to [- π, π] \subseteq ℝ$
39	2 38	sstrd	$⊢ φ \to A \subseteq ℝ$
40		dvfre	$⊢ (K : A ⟶ ℝ \land A \subseteq ℝ) \to K_{ℝ}^{'} : dom K_{ℝ}^{'} ⟶ ℝ$
41	35 39 40	syl2anc	$⊢ φ \to K_{ℝ}^{'} : dom K_{ℝ}^{'} ⟶ ℝ$
42		eqidd	$⊢ φ \to (s \in A ⟼ s) = (s \in A ⟼ s)$
43		eqidd	$⊢ φ \to (s \in A ⟼ 2 \sin (\frac{s}{2})) = (s \in A ⟼ 2 \sin (\frac{s}{2}))$
44	4 10 15 42 43	offval2	$⊢ φ \to (s \in A ⟼ s) \div_{f} (s \in A ⟼ 2 \sin (\frac{s}{2})) = (s \in A ⟼ \frac{s}{2 \sin (\frac{s}{2})})$
45	1 44	eqtr4id	$⊢ φ \to K = (s \in A ⟼ s) \div_{f} (s \in A ⟼ 2 \sin (\frac{s}{2}))$
46	45	oveq2d	$⊢ φ \to ℝ D K = ℝ D ((s \in A ⟼ s) \div_{f} (s \in A ⟼ 2 \sin (\frac{s}{2})))$
47		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
48	47	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
49		eqid	$⊢ (s \in A ⟼ s) = (s \in A ⟼ s)$
50	17 49	fmptd	$⊢ φ \to (s \in A ⟼ s) : A ⟶ ℂ$
51	16 19	mulcld	$⊢ (φ \land s \in A) \to 2 \sin (\frac{s}{2}) \in ℂ$
52	33	neneqd	$⊢ (φ \land s \in A) \to \neg 2 \sin (\frac{s}{2}) = 0$
53		elsng	$⊢ 2 \sin (\frac{s}{2}) \in ℝ \to (2 \sin (\frac{s}{2}) \in \{0\} \leftrightarrow 2 \sin (\frac{s}{2}) = 0)$
54	15 53	syl	$⊢ (φ \land s \in A) \to (2 \sin (\frac{s}{2}) \in \{0\} \leftrightarrow 2 \sin (\frac{s}{2}) = 0)$
55	52 54	mtbird	$⊢ (φ \land s \in A) \to \neg 2 \sin (\frac{s}{2}) \in \{0\}$
56	51 55	eldifd	$⊢ (φ \land s \in A) \to 2 \sin (\frac{s}{2}) \in (ℂ ∖ \{0\})$
57		eqid	$⊢ (s \in A ⟼ 2 \sin (\frac{s}{2})) = (s \in A ⟼ 2 \sin (\frac{s}{2}))$
58	56 57	fmptd	$⊢ φ \to (s \in A ⟼ 2 \sin (\frac{s}{2})) : A ⟶ ℂ ∖ \{0\}$
59		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
60	59	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
61	4 60	eleqtrdi	$⊢ φ \to A \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
62	48 61	dvmptidg	$⊢ φ \to \frac{d (s \in A⟼ s)}{d_{ℝ} s} = (s \in A ⟼ 1)$
63		ax-resscn	$⊢ ℝ \subseteq ℂ$
64	63	a1i	$⊢ φ \to ℝ \subseteq ℂ$
65	39 64	sstrd	$⊢ φ \to A \subseteq ℂ$
66		1cnd	$⊢ φ \to 1 \in ℂ$
67		ssid	$⊢ ℂ \subseteq ℂ$
68	67	a1i	$⊢ φ \to ℂ \subseteq ℂ$
69	65 66 68	constcncfg	$⊢ φ \to (s \in A ⟼ 1) : A \underset{cn}{⟶} ℂ$
70	62 69	eqeltrd	$⊢ φ \to \frac{d (s \in A⟼ s)}{d_{ℝ} s} : A \underset{cn}{⟶} ℂ$
71	39	resmptd	$⊢ φ \to {(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{A} = (s \in A ⟼ 2 \sin (\frac{s}{2}))$
72	71	eqcomd	$⊢ φ \to (s \in A ⟼ 2 \sin (\frac{s}{2})) = {(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{A}$
73	72	oveq2d	$⊢ φ \to \frac{d (s \in A⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = ℝ D ({(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{A})$
74		eqid	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) = (s \in ℝ ⟼ 2 \sin (\frac{s}{2}))$
75		2cnd	$⊢ s \in ℝ \to 2 \in ℂ$
76		recn	$⊢ s \in ℝ \to s \in ℂ$
77	76	halfcld	$⊢ s \in ℝ \to \frac{s}{2} \in ℂ$
78	77	sincld	$⊢ s \in ℝ \to \sin (\frac{s}{2}) \in ℂ$
79	75 78	mulcld	$⊢ s \in ℝ \to 2 \sin (\frac{s}{2}) \in ℂ$
80	74 79	fmpti	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) : ℝ ⟶ ℂ$
81	80	a1i	$⊢ φ \to (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) : ℝ ⟶ ℂ$
82		ssid	$⊢ ℝ \subseteq ℝ$
83	82	a1i	$⊢ φ \to ℝ \subseteq ℝ$
84	59 60	dvres	$⊢ ((ℝ \subseteq ℂ \land (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) : ℝ ⟶ ℂ) \land (ℝ \subseteq ℝ \land A \subseteq ℝ)) \to ℝ D ({(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{A}) = {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{int (topGen (ran (.))) (A)}$
85	64 81 83 39 84	syl22anc	$⊢ φ \to ℝ D ({(s \in ℝ ⟼ 2 \sin (\frac{s}{2})) ↾}_{A}) = {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{int (topGen (ran (.))) (A)}$
86		retop	$⊢ topGen (ran (.)) \in Top$
87	86	a1i	$⊢ φ \to topGen (ran (.)) \in Top$
88		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
89	88	isopn3	$⊢ (topGen (ran (.)) \in Top \land A \subseteq ℝ) \to (A \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) (A) = A)$
90	87 39 89	syl2anc	$⊢ φ \to (A \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) (A) = A)$
91	4 90	mpbid	$⊢ φ \to int (topGen (ran (.))) (A) = A$
92	91	reseq2d	$⊢ φ \to {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{int (topGen (ran (.))) (A)} = {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{A}$
93		resmpt	$⊢ ℝ \subseteq ℂ \to {(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ} = (s \in ℝ ⟼ 2 \sin (\frac{1}{2}) s)$
94	63 93	ax-mp	$⊢ {(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ} = (s \in ℝ ⟼ 2 \sin (\frac{1}{2}) s)$
95		id	$⊢ s \in ℂ \to s \in ℂ$
96		2cnd	$⊢ s \in ℂ \to 2 \in ℂ$
97	20	a1i	$⊢ s \in ℂ \to 2 \neq 0$
98	95 96 97	divrec2d	$⊢ s \in ℂ \to \frac{s}{2} = (\frac{1}{2}) s$
99	98	eqcomd	$⊢ s \in ℂ \to (\frac{1}{2}) s = \frac{s}{2}$
100	76 99	syl	$⊢ s \in ℝ \to (\frac{1}{2}) s = \frac{s}{2}$
101	100	fveq2d	$⊢ s \in ℝ \to \sin (\frac{1}{2}) s = \sin (\frac{s}{2})$
102	101	oveq2d	$⊢ s \in ℝ \to 2 \sin (\frac{1}{2}) s = 2 \sin (\frac{s}{2})$
103	102	mpteq2ia	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{1}{2}) s) = (s \in ℝ ⟼ 2 \sin (\frac{s}{2}))$
104	94 103	eqtr2i	$⊢ (s \in ℝ ⟼ 2 \sin (\frac{s}{2})) = {(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ}$
105	104	oveq2i	$⊢ \frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = ℝ D ({(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ})$
106		eqid	$⊢ (s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) = (s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s)$
107		halfcn	$⊢ \frac{1}{2} \in ℂ$
108	107	a1i	$⊢ s \in ℂ \to \frac{1}{2} \in ℂ$
109	108 95	mulcld	$⊢ s \in ℂ \to (\frac{1}{2}) s \in ℂ$
110	109	sincld	$⊢ s \in ℂ \to \sin (\frac{1}{2}) s \in ℂ$
111	96 110	mulcld	$⊢ s \in ℂ \to 2 \sin (\frac{1}{2}) s \in ℂ$
112	106 111	fmpti	$⊢ (s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) : ℂ ⟶ ℂ$
113		2cn	$⊢ 2 \in ℂ$
114		dvasinbx	$⊢ (2 \in ℂ \land \frac{1}{2} \in ℂ) \to \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} = (s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s)$
115	113 107 114	mp2an	$⊢ \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} = (s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s)$
116	113 20	recidi	$⊢ 2 (\frac{1}{2}) = 1$
117	116	a1i	$⊢ s \in ℂ \to 2 (\frac{1}{2}) = 1$
118	99	fveq2d	$⊢ s \in ℂ \to \cos (\frac{1}{2}) s = \cos (\frac{s}{2})$
119	117 118	oveq12d	$⊢ s \in ℂ \to 2 (\frac{1}{2}) \cos (\frac{1}{2}) s = 1 \cos (\frac{s}{2})$
120		halfcl	$⊢ s \in ℂ \to \frac{s}{2} \in ℂ$
121	120	coscld	$⊢ s \in ℂ \to \cos (\frac{s}{2}) \in ℂ$
122	121	mullidd	$⊢ s \in ℂ \to 1 \cos (\frac{s}{2}) = \cos (\frac{s}{2})$
123	119 122	eqtrd	$⊢ s \in ℂ \to 2 (\frac{1}{2}) \cos (\frac{1}{2}) s = \cos (\frac{s}{2})$
124	123	mpteq2ia	$⊢ (s \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) s) = (s \in ℂ ⟼ \cos (\frac{s}{2}))$
125	115 124	eqtri	$⊢ \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} = (s \in ℂ ⟼ \cos (\frac{s}{2}))$
126	125	dmeqi	$⊢ dom \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} = dom (s \in ℂ ⟼ \cos (\frac{s}{2}))$
127		dmmptg	$⊢ \forall s \in ℂ \cos (\frac{s}{2}) \in ℂ \to dom (s \in ℂ ⟼ \cos (\frac{s}{2})) = ℂ$
128	127 121	mprg	$⊢ dom (s \in ℂ ⟼ \cos (\frac{s}{2})) = ℂ$
129	126 128	eqtri	$⊢ dom \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} = ℂ$
130	63 129	sseqtrri	$⊢ ℝ \subseteq dom \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s}$
131		dvres3	$⊢ ((ℝ \in \{ℝ, ℂ\} \land (s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) : ℂ ⟶ ℂ) \land (ℂ \subseteq ℂ \land ℝ \subseteq dom \frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s})) \to ℝ D ({(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ}) = {\frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} ↾}_{ℝ}$
132	47 112 67 130 131	mp4an	$⊢ ℝ D ({(s \in ℂ ⟼ 2 \sin (\frac{1}{2}) s) ↾}_{ℝ}) = {\frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} ↾}_{ℝ}$
133	125	reseq1i	$⊢ {\frac{d (s \in ℂ⟼ 2 \sin (\frac{1}{2}) s)}{d_{ℂ} s} ↾}_{ℝ} = {(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{ℝ}$
134	105 132 133	3eqtri	$⊢ \frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = {(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{ℝ}$
135	134	reseq1i	$⊢ {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{A} = {({(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{ℝ}) ↾}_{A}$
136	135	a1i	$⊢ φ \to {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{A} = {({(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{ℝ}) ↾}_{A}$
137	39	resabs1d	$⊢ φ \to {({(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{ℝ}) ↾}_{A} = {(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{A}$
138	65	resmptd	$⊢ φ \to {(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{A} = (s \in A ⟼ \cos (\frac{s}{2}))$
139	137 138	eqtrd	$⊢ φ \to {({(s \in ℂ ⟼ \cos (\frac{s}{2})) ↾}_{ℝ}) ↾}_{A} = (s \in A ⟼ \cos (\frac{s}{2}))$
140	92 136 139	3eqtrd	$⊢ φ \to {\frac{d (s \in ℝ⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} ↾}_{int (topGen (ran (.))) (A)} = (s \in A ⟼ \cos (\frac{s}{2}))$
141	73 85 140	3eqtrd	$⊢ φ \to \frac{d (s \in A⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} = (s \in A ⟼ \cos (\frac{s}{2}))$
142		coscn	$⊢ \cos : ℂ \underset{cn}{⟶} ℂ$
143	142	a1i	$⊢ φ \to \cos : ℂ \underset{cn}{⟶} ℂ$
144	65 68	idcncfg	$⊢ φ \to (s \in A ⟼ s) : A \underset{cn}{⟶} ℂ$
145		2cnd	$⊢ φ \to 2 \in ℂ$
146	20	a1i	$⊢ φ \to 2 \neq 0$
147		eldifsn	$⊢ 2 \in (ℂ ∖ \{0\}) \leftrightarrow (2 \in ℂ \land 2 \neq 0)$
148	145 146 147	sylanbrc	$⊢ φ \to 2 \in (ℂ ∖ \{0\})$
149		difssd	$⊢ φ \to ℂ ∖ \{0\} \subseteq ℂ$
150	65 148 149	constcncfg	$⊢ φ \to (s \in A ⟼ 2) : A \underset{cn}{⟶} (ℂ ∖ \{0\})$
151	144 150	divcncf	$⊢ φ \to (s \in A ⟼ \frac{s}{2}) : A \underset{cn}{⟶} ℂ$
152	143 151	cncfmpt1f	$⊢ φ \to (s \in A ⟼ \cos (\frac{s}{2})) : A \underset{cn}{⟶} ℂ$
153	141 152	eqeltrd	$⊢ φ \to \frac{d (s \in A⟼ 2 \sin (\frac{s}{2}))}{d_{ℝ} s} : A \underset{cn}{⟶} ℂ$
154	48 50 58 70 153	dvdivcncf	$⊢ φ \to {((s \in A ⟼ s) \div_{f} (s \in A ⟼ 2 \sin (\frac{s}{2})))}_{ℝ}^{'} : A \underset{cn}{⟶} ℂ$
155	46 154	eqeltrd	$⊢ φ \to K_{ℝ}^{'} : A \underset{cn}{⟶} ℂ$
156		cncff	$⊢ K_{ℝ}^{'} : A \underset{cn}{⟶} ℂ \to K_{ℝ}^{'} : A ⟶ ℂ$
157		fdm	$⊢ K_{ℝ}^{'} : A ⟶ ℂ \to dom K_{ℝ}^{'} = A$
158	155 156 157	3syl	$⊢ φ \to dom K_{ℝ}^{'} = A$
159	158	feq2d	$⊢ φ \to (K_{ℝ}^{'} : dom K_{ℝ}^{'} ⟶ ℝ \leftrightarrow K_{ℝ}^{'} : A ⟶ ℝ)$
160	41 159	mpbid	$⊢ φ \to K_{ℝ}^{'} : A ⟶ ℝ$
161		cncfcdm	$⊢ (ℝ \subseteq ℂ \land K_{ℝ}^{'} : A \underset{cn}{⟶} ℂ) \to (K_{ℝ}^{'} : A \underset{cn}{⟶} ℝ \leftrightarrow K_{ℝ}^{'} : A ⟶ ℝ)$
162	64 155 161	syl2anc	$⊢ φ \to (K_{ℝ}^{'} : A \underset{cn}{⟶} ℝ \leftrightarrow K_{ℝ}^{'} : A ⟶ ℝ)$
163	160 162	mpbird	$⊢ φ \to K_{ℝ}^{'} : A \underset{cn}{⟶} ℝ$

Metamath Proof Explorer

Theorem fourierdlem58

Proof