fourierdlem57 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fourierdlem57		Structured version Visualization version GIF version

Theorem fourierdlem57 46161

Description: The derivative of 𝑂. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem57.f	⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
fourierdlem57.xre	⊢ (𝜑 → 𝑋 ∈ ℝ)
fourierdlem57.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
fourierdlem57.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
fourierdlem57.fdv	⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)
fourierdlem57.ab	⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π))
fourierdlem57.n0	⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))
fourierdlem57.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
fourierdlem57.o	⊢ 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))

**Assertion**
Ref	Expression
fourierdlem57	⊢ ((𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))) ∧ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))))

Distinct variable groups: 𝐴,𝑠 𝐵,𝑠 𝐶,𝑠 𝐹,𝑠 𝑋,𝑠 𝜑,𝑠 Allowed substitution hint: 𝑂(𝑠)

**Proof of Theorem fourierdlem57**
Step	Hyp	Ref	Expression
1		fourierdlem57.fdv	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)
2	1	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)
3		fourierdlem57.xre	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ ℝ)
4		fourierdlem57.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5	3, 4	readdcld 11203	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ)
6	5	rexrd 11224	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ^*)
7	6	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) ∈ ℝ^*)
8		fourierdlem57.b	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9	3, 8	readdcld 11203	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ)
10	9	rexrd 11224	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ^*)
11	10	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) ∈ ℝ^*)
12	3	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ)
13		elioore 13336	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ)
14	13	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
15	12, 14	readdcld 11203	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
16	4	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
17	16	rexrd 11224	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ^*)
18	8	rexrd 11224	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
19	18	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ^*)
20		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵))
21		ioogtlb 45493	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
22	17, 19, 20, 21	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
23	16, 14, 12, 22	ltadd2dd 11333	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠))
24	8	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ)
25		iooltub 45508	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
26	17, 19, 20, 25	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
27	14, 24, 12, 26	ltadd2dd 11333	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵))
28	7, 11, 15, 23, 27	eliood 45496	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))
29	2, 28	ffvelcdmd 7057	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℝ)
30		2re 12260	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
31	30	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℝ)
32		rehalfcl 12409	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ → (𝑠 / 2) ∈ ℝ)
33	14, 32	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / 2) ∈ ℝ)
34	33	resincld 16111	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℝ)
35	31, 34	remulcld 11204	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
36	29, 35	remulcld 11204	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) ∈ ℝ)
37	33	recoscld 16112	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℝ)
38		fourierdlem57.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
39	38	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ)
40	39, 15	ffvelcdmd 7057	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
41		fourierdlem57.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
42	41	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ)
43	40, 42	resubcld 11606	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℝ)
44	37, 43	remulcld 11204	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ ℝ)
45	36, 44	resubcld 11606	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) ∈ ℝ)
46	35	resqcld 14090	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((2 · (sin‘(𝑠 / 2)))↑2) ∈ ℝ)
47		2cnd 12264	. . . . . . . . 9 ⊢ (𝑠 ∈ ℝ → 2 ∈ ℂ)
48	32	recnd 11202	. . . . . . . . . 10 ⊢ (𝑠 ∈ ℝ → (𝑠 / 2) ∈ ℂ)
49	48	sincld 16098	. . . . . . . . 9 ⊢ (𝑠 ∈ ℝ → (sin‘(𝑠 / 2)) ∈ ℂ)
50	47, 49	mulcld 11194	. . . . . . . 8 ⊢ (𝑠 ∈ ℝ → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
51	14, 50	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
52		2cnd 12264	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ)
53	14, 49	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ)
54		2ne0 12290	. . . . . . . . 9 ⊢ 2 ≠ 0
55	54	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ≠ 0)
56		fourierdlem57.ab	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π))
57	56	sselda 3946	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (-π[,]π))
58		eqcom 2736	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 0 ↔ 0 = 𝑠)
59	58	biimpi 216	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 0 → 0 = 𝑠)
60	59	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 = 𝑠)
61		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 𝑠 ∈ (𝐴(,)𝐵))
62	60, 61	eqeltrd 2828	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵))
63	62	adantll 714	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵))
64		fourierdlem57.n0	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))
65	64	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴(,)𝐵))
66	63, 65	pm2.65da 816	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 = 0)
67	66	neqned 2932	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≠ 0)
68		fourierdlem44 46149	. . . . . . . . 9 ⊢ ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
69	57, 67, 68	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ≠ 0)
70	52, 53, 55, 69	mulne0d 11830	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
71		2z 12565	. . . . . . . 8 ⊢ 2 ∈ ℤ
72	71	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℤ)
73	51, 70, 72	expne0d 14117	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((2 · (sin‘(𝑠 / 2)))↑2) ≠ 0)
74	45, 46, 73	redivcld 12010	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)) ∈ ℝ)
75		eqid 2729	. . . . 5 ⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)))
76	74, 75	fmptd 7086	. . . 4 ⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))):(𝐴(,)𝐵)⟶ℝ)
77		fourierdlem57.o	. . . . . . . 8 ⊢ 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
78	77	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
79	78	oveq2d 7403	. . . . . 6 ⊢ (𝜑 → (ℝ D 𝑂) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))))
80		reelprrecn 11160	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
81	80	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
82	43	recnd 11202	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
83	40	recnd 11202	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
84		eqid 2729	. . . . . . . . . 10 ⊢ (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) = (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
85	38, 3, 4, 8, 84, 1	fourierdlem28 46133	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
86	42	recnd 11202	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℂ)
87		0red 11177	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
88		iooretop 24653	. . . . . . . . . . . 12 ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
89		tgioo4 24693	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
90	88, 89	eleqtri 2826	. . . . . . . . . . 11 ⊢ (𝐴(,)𝐵) ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ)
91	90	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(,)𝐵) ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
92	41	recnd 11202	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℂ)
93	81, 91, 92	dvmptconst 45913	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 0))
94	81, 83, 29, 85, 86, 87, 93	dvmptsub 25871	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)))
95	29	recnd 11202	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ)
96	95	subid1d 11522	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))
97	96	mpteq2dva 5200	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
98	94, 97	eqtrd 2764	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
99		eldifsn 4750	. . . . . . . 8 ⊢ ((2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}) ↔ ((2 · (sin‘(𝑠 / 2))) ∈ ℂ ∧ (2 · (sin‘(𝑠 / 2))) ≠ 0))
100	51, 70, 99	sylanbrc 583	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
101		recn 11158	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℝ → 𝑠 ∈ ℂ)
102	54	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℝ → 2 ≠ 0)
103	101, 47, 102	divrec2d 11962	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℝ → (𝑠 / 2) = ((1 / 2) · 𝑠))
104	103	eqcomd 2735	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ → ((1 / 2) · 𝑠) = (𝑠 / 2))
105	13, 104	syl 17	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((1 / 2) · 𝑠) = (𝑠 / 2))
106	105	fveq2d 6862	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘((1 / 2) · 𝑠)) = (cos‘(𝑠 / 2)))
107		halfcn 12396	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℂ
108	107	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℂ → (1 / 2) ∈ ℂ)
109		id 22	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℂ → 𝑠 ∈ ℂ)
110	108, 109	mulcld 11194	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℂ → ((1 / 2) · 𝑠) ∈ ℂ)
111	110	coscld 16099	. . . . . . . . . 10 ⊢ (𝑠 ∈ ℂ → (cos‘((1 / 2) · 𝑠)) ∈ ℂ)
112	13, 101, 111	3syl 18	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘((1 / 2) · 𝑠)) ∈ ℂ)
113	106, 112	eqeltrrd 2829	. . . . . . . 8 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘(𝑠 / 2)) ∈ ℂ)
114	113	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℂ)
115		ioossre 13368	. . . . . . . . . . . . 13 ⊢ (𝐴(,)𝐵) ⊆ ℝ
116		resmpt 6008	. . . . . . . . . . . . 13 ⊢ ((𝐴(,)𝐵) ⊆ ℝ → ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2)))))
117	115, 116	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))
118	117	eqcomi 2738	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2)))) = ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵))
119	118	oveq2i 7398	. . . . . . . . . 10 ⊢ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (ℝ D ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵)))
120		ax-resscn 11125	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℂ
121		eqid 2729	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))
122	121, 50	fmpti 7084	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))):ℝ⟶ℂ
123		ssid 3969	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℝ
124		eqid 2729	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
125	124, 89	dvres 25812	. . . . . . . . . . 11 ⊢ (((ℝ ⊆ ℂ ∧ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ)) → (ℝ D ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵))) = ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵))))
126	120, 122, 123, 115, 125	mp4an 693	. . . . . . . . . 10 ⊢ (ℝ D ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵))) = ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)))
127		resmpt 6008	. . . . . . . . . . . . . . 15 ⊢ (ℝ ⊆ ℂ → ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) = (𝑠 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑠)))))
128	120, 127	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) = (𝑠 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑠))))
129	104	fveq2d 6862	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ℝ → (sin‘((1 / 2) · 𝑠)) = (sin‘(𝑠 / 2)))
130	129	oveq2d 7403	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℝ → (2 · (sin‘((1 / 2) · 𝑠))) = (2 · (sin‘(𝑠 / 2))))
131	130	mpteq2ia 5202	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))
132	128, 131	eqtr2i 2753	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) = ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)
133	132	oveq2i 7398	. . . . . . . . . . . 12 ⊢ (ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) = (ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ))
134		ioontr 45509	. . . . . . . . . . . 12 ⊢ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) = (𝐴(,)𝐵)
135	133, 134	reseq12i 5948	. . . . . . . . . . 11 ⊢ ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵))) = ((ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) ↾ (𝐴(,)𝐵))
136		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))
137		2cnd 12264	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℂ → 2 ∈ ℂ)
138	110	sincld 16098	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℂ → (sin‘((1 / 2) · 𝑠)) ∈ ℂ)
139	137, 138	mulcld 11194	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ℂ → (2 · (sin‘((1 / 2) · 𝑠))) ∈ ℂ)
140	136, 139	fmpti 7084	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))):ℂ⟶ℂ
141		ssid 3969	. . . . . . . . . . . . 13 ⊢ ℂ ⊆ ℂ
142		dmmptg 6215	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑠 ∈ ℂ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) ∈ ℂ → dom (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) = ℂ)
143		2cn 12261	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℂ
144	143, 107	mulcli 11181	. . . . . . . . . . . . . . . . . 18 ⊢ (2 · (1 / 2)) ∈ ℂ
145	144	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ ℂ → (2 · (1 / 2)) ∈ ℂ)
146	145, 111	mulcld 11194	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ℂ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) ∈ ℂ)
147	142, 146	mprg 3050	. . . . . . . . . . . . . . 15 ⊢ dom (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) = ℂ
148	120, 147	sseqtrri 3996	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ dom (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
149		dvasinbx 45918	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))))
150	143, 107, 149	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
151	150	dmeqi 5868	. . . . . . . . . . . . . 14 ⊢ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = dom (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
152	148, 151	sseqtrri 3996	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))))
153		dvres3 25814	. . . . . . . . . . . . 13 ⊢ (((ℝ ∈ {ℝ, ℂ} ∧ (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))):ℂ⟶ℂ) ∧ (ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))))) → (ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) = ((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ))
154	80, 140, 141, 152, 153	mp4an 693	. . . . . . . . . . . 12 ⊢ (ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) = ((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ)
155	154	reseq1i 5946	. . . . . . . . . . 11 ⊢ ((ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) ↾ (𝐴(,)𝐵)) = (((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) ↾ (𝐴(,)𝐵))
156	150	reseq1i 5946	. . . . . . . . . . . . 13 ⊢ ((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) = ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ ℝ)
157	156	reseq1i 5946	. . . . . . . . . . . 12 ⊢ (((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) ↾ (𝐴(,)𝐵)) = (((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ ℝ) ↾ (𝐴(,)𝐵))
158		resabs1 5977	. . . . . . . . . . . . 13 ⊢ ((𝐴(,)𝐵) ⊆ ℝ → (((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ ℝ) ↾ (𝐴(,)𝐵)) = ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ (𝐴(,)𝐵)))
159	115, 158	ax-mp 5	. . . . . . . . . . . 12 ⊢ (((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ ℝ) ↾ (𝐴(,)𝐵)) = ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ (𝐴(,)𝐵))
160		ioosscn 13369	. . . . . . . . . . . . 13 ⊢ (𝐴(,)𝐵) ⊆ ℂ
161		resmpt 6008	. . . . . . . . . . . . 13 ⊢ ((𝐴(,)𝐵) ⊆ ℂ → ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))))
162	160, 161	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
163	157, 159, 162	3eqtri 2756	. . . . . . . . . . 11 ⊢ (((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
164	135, 155, 163	3eqtri 2756	. . . . . . . . . 10 ⊢ ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
165	119, 126, 164	3eqtri 2756	. . . . . . . . 9 ⊢ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
166	143, 54	recidi 11913	. . . . . . . . . . . . 13 ⊢ (2 · (1 / 2)) = 1
167	166	oveq1i 7397	. . . . . . . . . . . 12 ⊢ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) = (1 · (cos‘((1 / 2) · 𝑠)))
168	167	a1i 11	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) = (1 · (cos‘((1 / 2) · 𝑠))))
169	112	mullidd 11192	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (1 · (cos‘((1 / 2) · 𝑠))) = (cos‘((1 / 2) · 𝑠)))
170	168, 169, 106	3eqtrd 2768	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) = (cos‘(𝑠 / 2)))
171	170	mpteq2ia 5202	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))
172	165, 171	eqtri 2752	. . . . . . . 8 ⊢ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))
173	172	a1i 11	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))))
174	81, 82, 29, 98, 100, 114, 173	dvmptdiv 25878	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))
175	79, 174	eqtrd 2764	. . . . 5 ⊢ (𝜑 → (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))
176	175	feq1d 6670	. . . 4 ⊢ (𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ↔ (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))):(𝐴(,)𝐵)⟶ℝ))
177	76, 176	mpbird 257	. . 3 ⊢ (𝜑 → (ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ)
178	177, 175	jca 511	. 2 ⊢ (𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)))))
179	178, 172	pm3.2i 470	1 ⊢ ((𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))) ∧ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∖ cdif 3911 ⊆ wss 3914 {csn 4589 {cpr 4591 class class class wbr 5107 ↦ cmpt 5188 dom cdm 5638 ran crn 5639 ↾ cres 5640 ⟶wf 6507 ‘cfv 6511 (class class class)co 7387 ℂcc 11066 ℝcr 11067 0cc0 11068 1c1 11069 + caddc 11071 · cmul 11073 ℝ^*cxr 11207 < clt 11208 − cmin 11405 -cneg 11406 / cdiv 11835 2c2 12241 ℤcz 12529 (,)cioo 13306 [,]cicc 13309 ↑cexp 14026 sincsin 16029 cosccos 16030 πcpi 16032 ↾_t crest 17383 TopOpenctopn 17384 topGenctg 17400 ℂ_fldccnfld 21264 intcnt 22904 D cdv 25764

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 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146 ax-addf 11147

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 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-iin 4958 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-of 7653 df-om 7843 df-1st 7968 df-2nd 7969 df-supp 8140 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-2o 8435 df-er 8671 df-map 8801 df-pm 8802 df-ixp 8871 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-fsupp 9313 df-fi 9362 df-sup 9393 df-inf 9394 df-oi 9463 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-4 12251 df-5 12252 df-6 12253 df-7 12254 df-8 12255 df-9 12256 df-n0 12443 df-z 12530 df-dec 12650 df-uz 12794 df-q 12908 df-rp 12952 df-xneg 13072 df-xadd 13073 df-xmul 13074 df-ioo 13310 df-ioc 13311 df-ico 13312 df-icc 13313 df-fz 13469 df-fzo 13616 df-fl 13754 df-mod 13832 df-seq 13967 df-exp 14027 df-fac 14239 df-bc 14268 df-hash 14296 df-shft 15033 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-limsup 15437 df-clim 15454 df-rlim 15455 df-sum 15653 df-ef 16033 df-sin 16035 df-cos 16036 df-pi 16038 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-rest 17385 df-topn 17386 df-0g 17404 df-gsum 17405 df-topgen 17406 df-pt 17407 df-prds 17410 df-xrs 17465 df-qtop 17470 df-imas 17471 df-xps 17473 df-mre 17547 df-mrc 17548 df-acs 17550 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-submnd 18711 df-mulg 19000 df-cntz 19249 df-cmn 19712 df-psmet 21256 df-xmet 21257 df-met 21258 df-bl 21259 df-mopn 21260 df-fbas 21261 df-fg 21262 df-cnfld 21265 df-top 22781 df-topon 22798 df-topsp 22820 df-bases 22833 df-cld 22906 df-ntr 22907 df-cls 22908 df-nei 22985 df-lp 23023 df-perf 23024 df-cn 23114 df-cnp 23115 df-t1 23201 df-haus 23202 df-tx 23449 df-hmeo 23642 df-fil 23733 df-fm 23825 df-flim 23826 df-flf 23827 df-xms 24208 df-ms 24209 df-tms 24210 df-cncf 24771 df-limc 25767 df-dv 25768

This theorem is referenced by: fourierdlem68 46172 fourierdlem80 46184

W3C validator