Theorem fourierdlem58 46135

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

Hypotheses

Ref	Expression
fourierdlem58.k	⊢ 𝐾 = (𝑠 ∈ 𝐴 ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
fourierdlem58.ass	⊢ (𝜑 → 𝐴 ⊆ (-π[,]π))
fourierdlem58.0nA	⊢ (𝜑 → ¬ 0 ∈ 𝐴)
fourierdlem58.4	⊢ (𝜑 → 𝐴 ∈ (topGen‘ran (,)))

Assertion

Ref	Expression
fourierdlem58	⊢ (𝜑 → (ℝ D 𝐾) ∈ (𝐴–cn→ℝ))

Distinct variable groups:   𝐴,𝑠   𝜑,𝑠

Allowed substitution hint:   𝐾(𝑠)

Proof of Theorem fourierdlem58

Step	Hyp	Ref	Expression
1		pire 26342	. . . . . . . . . 10 ⊢ π ∈ ℝ
2	1	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → π ∈ ℝ)
3	2	renegcld 11581	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → -π ∈ ℝ)
4	3, 2	iccssred 13371	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (-π[,]π) ⊆ ℝ)
5		fourierdlem58.ass	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ (-π[,]π))
6	5	sselda 3943	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ (-π[,]π))
7	4, 6	sseldd 3944	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℝ)
8		2re 12236	. . . . . . . 8 ⊢ 2 ∈ ℝ
9	8	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 2 ∈ ℝ)
10	7	rehalfcld 12405	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑠 / 2) ∈ ℝ)
11	10	resincld 16087	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (sin‘(𝑠 / 2)) ∈ ℝ)
12	9, 11	remulcld 11180	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
13		2cnd 12240	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 2 ∈ ℂ)
14	7	recnd 11178	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℂ)
15	14	halfcld 12403	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑠 / 2) ∈ ℂ)
16	15	sincld 16074	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (sin‘(𝑠 / 2)) ∈ ℂ)
17		2ne0 12266	. . . . . . . 8 ⊢ 2 ≠ 0
18	17	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 2 ≠ 0)
19		eqcom 2736	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 0 ↔ 0 = 𝑠)
20	19	biimpi 216	. . . . . . . . . . . . 13 ⊢ (𝑠 = 0 → 0 = 𝑠)
21	20	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ 𝐴 ∧ 𝑠 = 0) → 0 = 𝑠)
22		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ 𝐴 ∧ 𝑠 = 0) → 𝑠 ∈ 𝐴)
23	21, 22	eqeltrd 2828	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ 𝐴 ∧ 𝑠 = 0) → 0 ∈ 𝐴)
24	23	adantll 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐴) ∧ 𝑠 = 0) → 0 ∈ 𝐴)
25		fourierdlem58.0nA	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 0 ∈ 𝐴)
26	25	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐴) ∧ 𝑠 = 0) → ¬ 0 ∈ 𝐴)
27	24, 26	pm2.65da 816	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ 𝑠 = 0)
28	27	neqned 2932	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ≠ 0)
29		fourierdlem44 46122	. . . . . . . 8 ⊢ ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
30	6, 28, 29	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (sin‘(𝑠 / 2)) ≠ 0)
31	13, 16, 18, 30	mulne0d 11806	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
32	7, 12, 31	redivcld 11986	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℝ)
33		fourierdlem58.k	. . . . 5 ⊢ 𝐾 = (𝑠 ∈ 𝐴 ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
34	32, 33	fmptd 7068	. . . 4 ⊢ (𝜑 → 𝐾:𝐴⟶ℝ)
35	1	a1i 11	. . . . . . 7 ⊢ (𝜑 → π ∈ ℝ)
36	35	renegcld 11581	. . . . . 6 ⊢ (𝜑 → -π ∈ ℝ)
37	36, 35	iccssred 13371	. . . . 5 ⊢ (𝜑 → (-π[,]π) ⊆ ℝ)
38	5, 37	sstrd 3954	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
39		dvfre 25831	. . . 4 ⊢ ((𝐾:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D 𝐾):dom (ℝ D 𝐾)⟶ℝ)
40	34, 38, 39	syl2anc 584	. . 3 ⊢ (𝜑 → (ℝ D 𝐾):dom (ℝ D 𝐾)⟶ℝ)
41		fourierdlem58.4	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ (topGen‘ran (,)))
42		eqidd 2730	. . . . . . . . 9 ⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 𝑠) = (𝑠 ∈ 𝐴 ↦ 𝑠))
43		eqidd 2730	. . . . . . . . 9 ⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))))
44	41, 7, 12, 42, 43	offval2 7653	. . . . . . . 8 ⊢ (𝜑 → ((𝑠 ∈ 𝐴 ↦ 𝑠) ∘f / (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ 𝐴 ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))))
45	33, 44	eqtr4id 2783	. . . . . . 7 ⊢ (𝜑 → 𝐾 = ((𝑠 ∈ 𝐴 ↦ 𝑠) ∘f / (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))))
46	45	oveq2d 7385	. . . . . 6 ⊢ (𝜑 → (ℝ D 𝐾) = (ℝ D ((𝑠 ∈ 𝐴 ↦ 𝑠) ∘f / (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))))))
47		reelprrecn 11136	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
48	47	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
49		eqid 2729	. . . . . . . 8 ⊢ (𝑠 ∈ 𝐴 ↦ 𝑠) = (𝑠 ∈ 𝐴 ↦ 𝑠)
50	14, 49	fmptd 7068	. . . . . . 7 ⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 𝑠):𝐴⟶ℂ)
51	13, 16	mulcld 11170	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
52	31	neneqd 2930	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
53		elsng 4599	. . . . . . . . . . 11 ⊢ ((2 · (sin‘(𝑠 / 2))) ∈ ℝ → ((2 · (sin‘(𝑠 / 2))) ∈ {0} ↔ (2 · (sin‘(𝑠 / 2))) = 0))
54	12, 53	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ((2 · (sin‘(𝑠 / 2))) ∈ {0} ↔ (2 · (sin‘(𝑠 / 2))) = 0))
55	52, 54	mtbird 325	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ (2 · (sin‘(𝑠 / 2))) ∈ {0})
56	51, 55	eldifd 3922	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
57		eqid 2729	. . . . . . . 8 ⊢ (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))
58	56, 57	fmptd 7068	. . . . . . 7 ⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))):𝐴⟶(ℂ ∖ {0}))
59		tgioo4 24669	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
60	41, 59	eleqtrdi 2838	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ((TopOpen‘ℂfld) ↾t ℝ))
61	48, 60	dvmptidg 45888	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ 𝑠)) = (𝑠 ∈ 𝐴 ↦ 1))
62		ax-resscn 11101	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℂ
63	62	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ⊆ ℂ)
64	38, 63	sstrd 3954	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
65		1cnd 11145	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
66		ssid 3966	. . . . . . . . . 10 ⊢ ℂ ⊆ ℂ
67	66	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℂ ⊆ ℂ)
68	64, 65, 67	constcncfg 45843	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 1) ∈ (𝐴–cn→ℂ))
69	61, 68	eqeltrd 2828	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ 𝑠)) ∈ (𝐴–cn→ℂ))
70	38	resmptd 6000	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ 𝐴) = (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))))
71	70	eqcomd 2735	. . . . . . . . . 10 ⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))) = ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ 𝐴))
72	71	oveq2d 7385	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) = (ℝ D ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ 𝐴)))
73		eqid 2729	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))
74		2cnd 12240	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℝ → 2 ∈ ℂ)
75		recn 11134	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℝ → 𝑠 ∈ ℂ)
76	75	halfcld 12403	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ℝ → (𝑠 / 2) ∈ ℂ)
77	76	sincld 16074	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℝ → (sin‘(𝑠 / 2)) ∈ ℂ)
78	74, 77	mulcld 11170	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℝ → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
79	73, 78	fmpti 7066	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))):ℝ⟶ℂ
80	79	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))):ℝ⟶ℂ)
81		ssid 3966	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℝ
82	81	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ⊆ ℝ)
83		eqid 2729	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
84	83, 59	dvres 25788	. . . . . . . . . 10 ⊢ (((ℝ ⊆ ℂ ∧ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ 𝐴 ⊆ ℝ)) → (ℝ D ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ 𝐴)) = ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘𝐴)))
85	63, 80, 82, 38, 84	syl22anc 838	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ 𝐴)) = ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘𝐴)))
86		retop 24625	. . . . . . . . . . . . . 14 ⊢ (topGen‘ran (,)) ∈ Top
87	86	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (topGen‘ran (,)) ∈ Top)
88		uniretop 24626	. . . . . . . . . . . . . 14 ⊢ ℝ = ∪ (topGen‘ran (,))
89	88	isopn3 22929	. . . . . . . . . . . . 13 ⊢ (((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
90	87, 38, 89	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴))
91	41, 90	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘𝐴) = 𝐴)
92	91	reseq2d 5939	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘𝐴)) = ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ 𝐴))
93		resmpt 5997	. . . . . . . . . . . . . . . 16 ⊢ (ℝ ⊆ ℂ → ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) = (𝑠 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑠)))))
94	62, 93	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) = (𝑠 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑠))))
95		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ℂ → 𝑠 ∈ ℂ)
96		2cnd 12240	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ℂ → 2 ∈ ℂ)
97	17	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ℂ → 2 ≠ 0)
98	95, 96, 97	divrec2d 11938	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ ℂ → (𝑠 / 2) = ((1 / 2) · 𝑠))
99	98	eqcomd 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ ℂ → ((1 / 2) · 𝑠) = (𝑠 / 2))
100	75, 99	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ ℝ → ((1 / 2) · 𝑠) = (𝑠 / 2))
101	100	fveq2d 6844	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ ℝ → (sin‘((1 / 2) · 𝑠)) = (sin‘(𝑠 / 2)))
102	101	oveq2d 7385	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ℝ → (2 · (sin‘((1 / 2) · 𝑠))) = (2 · (sin‘(𝑠 / 2))))
103	102	mpteq2ia 5197	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))
104	94, 103	eqtr2i 2753	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) = ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)
105	104	oveq2i 7380	. . . . . . . . . . . . 13 ⊢ (ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) = (ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ))
106		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))
107		halfcn 12372	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 / 2) ∈ ℂ
108	107	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ ℂ → (1 / 2) ∈ ℂ)
109	108, 95	mulcld 11170	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ ℂ → ((1 / 2) · 𝑠) ∈ ℂ)
110	109	sincld 16074	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ℂ → (sin‘((1 / 2) · 𝑠)) ∈ ℂ)
111	96, 110	mulcld 11170	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℂ → (2 · (sin‘((1 / 2) · 𝑠))) ∈ ℂ)
112	106, 111	fmpti 7066	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))):ℂ⟶ℂ
113		2cn 12237	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℂ
114		dvasinbx 45891	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))))
115	113, 107, 114	mp2an 692	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
116	113, 17	recidi 11889	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 · (1 / 2)) = 1
117	116	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ℂ → (2 · (1 / 2)) = 1)
118	99	fveq2d 6844	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ℂ → (cos‘((1 / 2) · 𝑠)) = (cos‘(𝑠 / 2)))
119	117, 118	oveq12d 7387	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ ℂ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) = (1 · (cos‘(𝑠 / 2))))
120		halfcl 12384	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 ∈ ℂ → (𝑠 / 2) ∈ ℂ)
121	120	coscld 16075	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ℂ → (cos‘(𝑠 / 2)) ∈ ℂ)
122	121	mullidd 11168	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ ℂ → (1 · (cos‘(𝑠 / 2))) = (cos‘(𝑠 / 2)))
123	119, 122	eqtrd 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 ∈ ℂ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) = (cos‘(𝑠 / 2)))
124	123	mpteq2ia 5197	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2)))
125	115, 124	eqtri 2752	. . . . . . . . . . . . . . . . 17 ⊢ (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2)))
126	125	dmeqi 5858	. . . . . . . . . . . . . . . 16 ⊢ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = dom (𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2)))
127		dmmptg 6203	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑠 ∈ ℂ (cos‘(𝑠 / 2)) ∈ ℂ → dom (𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) = ℂ)
128	127, 121	mprg 3050	. . . . . . . . . . . . . . . 16 ⊢ dom (𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) = ℂ
129	126, 128	eqtri 2752	. . . . . . . . . . . . . . 15 ⊢ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = ℂ
130	62, 129	sseqtrri 3993	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))))
131		dvres3 25790	. . . . . . . . . . . . . 14 ⊢ (((ℝ ∈ {ℝ, ℂ} ∧ (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))):ℂ⟶ℂ) ∧ (ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))))) → (ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) = ((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ))
132	47, 112, 66, 130, 131	mp4an 693	. . . . . . . . . . . . 13 ⊢ (ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) = ((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ)
133	125	reseq1i 5935	. . . . . . . . . . . . 13 ⊢ ((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) = ((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ ℝ)
134	105, 132, 133	3eqtri 2756	. . . . . . . . . . . 12 ⊢ (ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) = ((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ ℝ)
135	134	reseq1i 5935	. . . . . . . . . . 11 ⊢ ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ 𝐴) = (((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ ℝ) ↾ 𝐴)
136	135	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ 𝐴) = (((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ ℝ) ↾ 𝐴))
137	38	resabs1d 5968	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ ℝ) ↾ 𝐴) = ((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ 𝐴))
138	64	resmptd 6000	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ 𝐴) = (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2))))
139	137, 138	eqtrd 2764	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ ℝ) ↾ 𝐴) = (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2))))
140	92, 136, 139	3eqtrd 2768	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘𝐴)) = (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2))))
141	72, 85, 140	3eqtrd 2768	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2))))
142		coscn 26331	. . . . . . . . . 10 ⊢ cos ∈ (ℂ–cn→ℂ)
143	142	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → cos ∈ (ℂ–cn→ℂ))
144	64, 67	idcncfg 45844	. . . . . . . . . 10 ⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 𝑠) ∈ (𝐴–cn→ℂ))
145		2cnd 12240	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℂ)
146	17	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ≠ 0)
147		eldifsn 4746	. . . . . . . . . . . 12 ⊢ (2 ∈ (ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠ 0))
148	145, 146, 147	sylanbrc 583	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ (ℂ ∖ {0}))
149		difssd 4096	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
150	64, 148, 149	constcncfg 45843	. . . . . . . . . 10 ⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 2) ∈ (𝐴–cn→(ℂ ∖ {0})))
151	144, 150	divcncf 25324	. . . . . . . . 9 ⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (𝑠 / 2)) ∈ (𝐴–cn→ℂ))
152	143, 151	cncfmpt1f 24783	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2))) ∈ (𝐴–cn→ℂ))
153	141, 152	eqeltrd 2828	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) ∈ (𝐴–cn→ℂ))
154	48, 50, 58, 69, 153	dvdivcncf 45898	. . . . . 6 ⊢ (𝜑 → (ℝ D ((𝑠 ∈ 𝐴 ↦ 𝑠) ∘f / (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))))) ∈ (𝐴–cn→ℂ))
155	46, 154	eqeltrd 2828	. . . . 5 ⊢ (𝜑 → (ℝ D 𝐾) ∈ (𝐴–cn→ℂ))
156		cncff 24762	. . . . 5 ⊢ ((ℝ D 𝐾) ∈ (𝐴–cn→ℂ) → (ℝ D 𝐾):𝐴⟶ℂ)
157		fdm 6679	. . . . 5 ⊢ ((ℝ D 𝐾):𝐴⟶ℂ → dom (ℝ D 𝐾) = 𝐴)
158	155, 156, 157	3syl 18	. . . 4 ⊢ (𝜑 → dom (ℝ D 𝐾) = 𝐴)
159	158	feq2d 6654	. . 3 ⊢ (𝜑 → ((ℝ D 𝐾):dom (ℝ D 𝐾)⟶ℝ ↔ (ℝ D 𝐾):𝐴⟶ℝ))
160	40, 159	mpbid 232	. 2 ⊢ (𝜑 → (ℝ D 𝐾):𝐴⟶ℝ)
161		cncfcdm 24767	. . 3 ⊢ ((ℝ ⊆ ℂ ∧ (ℝ D 𝐾) ∈ (𝐴–cn→ℂ)) → ((ℝ D 𝐾) ∈ (𝐴–cn→ℝ) ↔ (ℝ D 𝐾):𝐴⟶ℝ))
162	63, 155, 161	syl2anc 584	. 2 ⊢ (𝜑 → ((ℝ D 𝐾) ∈ (𝐴–cn→ℝ) ↔ (ℝ D 𝐾):𝐴⟶ℝ))
163	160, 162	mpbird 257	1 ⊢ (𝜑 → (ℝ D 𝐾) ∈ (𝐴–cn→ℝ))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ≠ wne 2925   ∖ cdif 3908   ⊆ wss 3911  {csn 4585  {cpr 4587   ↦ cmpt 5183  dom cdm 5631  ran crn 5632   ↾ cres 5633  ⟶wf 6495  ‘cfv 6499  (class class class)co 7369   ∘_f cof 7631  ℂcc 11042  ℝcr 11043  0cc0 11044  1c1 11045   · cmul 11049  -cneg 11382   / cdiv 11811  2c2 12217  (,)cioo 13282  [,]cicc 13285  sincsin 16005  cosccos 16006  πcpi 16008   ↾_t crest 17359  TopOpenctopn 17360  topGenctg 17376  ℂ_fldccnfld 21240  Topctop 22756  intcnt 22880  –cn→ccncf 24745   D cdv 25740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-inf2 9570  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-pre-sup 11122  ax-addf 11123

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-iin 4954  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-of 7633  df-om 7823  df-1st 7947  df-2nd 7948  df-supp 8117  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-2o 8412  df-er 8648  df-map 8778  df-pm 8779  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9289  df-fi 9338  df-sup 9369  df-inf 9370  df-oi 9439  df-card 9868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812  df-nn 12163  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231  df-9 12232  df-n0 12419  df-z 12506  df-dec 12626  df-uz 12770  df-q 12884  df-rp 12928  df-xneg 13048  df-xadd 13049  df-xmul 13050  df-ioo 13286  df-ioc 13287  df-ico 13288  df-icc 13289  df-fz 13445  df-fzo 13592  df-fl 13730  df-mod 13808  df-seq 13943  df-exp 14003  df-fac 14215  df-bc 14244  df-hash 14272  df-shft 15009  df-cj 15041  df-re 15042  df-im 15043  df-sqrt 15177  df-abs 15178  df-limsup 15413  df-clim 15430  df-rlim 15431  df-sum 15629  df-ef 16009  df-sin 16011  df-cos 16012  df-pi 16014  df-struct 17093  df-sets 17110  df-slot 17128  df-ndx 17140  df-base 17156  df-ress 17177  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17361  df-topn 17362  df-0g 17380  df-gsum 17381  df-topgen 17382  df-pt 17383  df-prds 17386  df-xrs 17441  df-qtop 17446  df-imas 17447  df-xps 17449  df-mre 17523  df-mrc 17524  df-acs 17526  df-mgm 18543  df-sgrp 18622  df-mnd 18638  df-submnd 18687  df-mulg 18976  df-cntz 19225  df-cmn 19688  df-psmet 21232  df-xmet 21233  df-met 21234  df-bl 21235  df-mopn 21236  df-fbas 21237  df-fg 21238  df-cnfld 21241  df-top 22757  df-topon 22774  df-topsp 22796  df-bases 22809  df-cld 22882  df-ntr 22883  df-cls 22884  df-nei 22961  df-lp 22999  df-perf 23000  df-cn 23090  df-cnp 23091  df-t1 23177  df-haus 23178  df-tx 23425  df-hmeo 23618  df-fil 23709  df-fm 23801  df-flim 23802  df-flf 23803  df-xms 24184  df-ms 24185  df-tms 24186  df-cncf 24747  df-limc 25743  df-dv 25744

This theorem is referenced by:  fourierdlem72  46149