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 44652

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 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)
3		fourierdlem57.xre	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ ℝ)
4		fourierdlem57.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5	3, 4	readdcld 11225	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ)
6	5	rexrd 11246	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ^*)
7	6	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) ∈ ℝ^*)
8		fourierdlem57.b	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9	3, 8	readdcld 11225	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ)
10	9	rexrd 11246	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ^*)
11	10	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) ∈ ℝ^*)
12	3	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ)
13		elioore 13336	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ)
14	13	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
15	12, 14	readdcld 11225	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
16	4	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
17	16	rexrd 11246	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ^*)
18	8	rexrd 11246	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
19	18	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ^*)
20		simpr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵))
21		ioogtlb 43981	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
22	17, 19, 20, 21	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
23	16, 14, 12, 22	ltadd2dd 11355	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠))
24	8	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ)
25		iooltub 43996	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
26	17, 19, 20, 25	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
27	14, 24, 12, 26	ltadd2dd 11355	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵))
28	7, 11, 15, 23, 27	eliood 43984	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))
29	2, 28	ffvelcdmd 7072	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℝ)
30		2re 12268	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
31	30	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℝ)
32		rehalfcl 12420	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ → (𝑠 / 2) ∈ ℝ)
33	14, 32	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / 2) ∈ ℝ)
34	33	resincld 16068	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℝ)
35	31, 34	remulcld 11226	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
36	29, 35	remulcld 11226	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) ∈ ℝ)
37	33	recoscld 16069	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℝ)
38		fourierdlem57.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
39	38	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ)
40	39, 15	ffvelcdmd 7072	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
41		fourierdlem57.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
42	41	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ)
43	40, 42	resubcld 11624	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℝ)
44	37, 43	remulcld 11226	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ ℝ)
45	36, 44	resubcld 11624	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) ∈ ℝ)
46	35	resqcld 14072	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((2 · (sin‘(𝑠 / 2)))↑2) ∈ ℝ)
47		2cnd 12272	. . . . . . . . 9 ⊢ (𝑠 ∈ ℝ → 2 ∈ ℂ)
48	32	recnd 11224	. . . . . . . . . 10 ⊢ (𝑠 ∈ ℝ → (𝑠 / 2) ∈ ℂ)
49	48	sincld 16055	. . . . . . . . 9 ⊢ (𝑠 ∈ ℝ → (sin‘(𝑠 / 2)) ∈ ℂ)
50	47, 49	mulcld 11216	. . . . . . . 8 ⊢ (𝑠 ∈ ℝ → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
51	14, 50	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
52		2cnd 12272	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ)
53	14, 49	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ)
54		2ne0 12298	. . . . . . . . 9 ⊢ 2 ≠ 0
55	54	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ≠ 0)
56		fourierdlem57.ab	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π))
57	56	sselda 3978	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (-π[,]π))
58		eqcom 2738	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 0 ↔ 0 = 𝑠)
59	58	biimpi 215	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 0 → 0 = 𝑠)
60	59	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 = 𝑠)
61		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 𝑠 ∈ (𝐴(,)𝐵))
62	60, 61	eqeltrd 2832	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵))
63	62	adantll 712	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵))
64		fourierdlem57.n0	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))
65	64	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴(,)𝐵))
66	63, 65	pm2.65da 815	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 = 0)
67	66	neqned 2946	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≠ 0)
68		fourierdlem44 44640	. . . . . . . . 9 ⊢ ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
69	57, 67, 68	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ≠ 0)
70	52, 53, 55, 69	mulne0d 11848	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
71		2z 12576	. . . . . . . 8 ⊢ 2 ∈ ℤ
72	71	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℤ)
73	51, 70, 72	expne0d 14099	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((2 · (sin‘(𝑠 / 2)))↑2) ≠ 0)
74	45, 46, 73	redivcld 12024	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)) ∈ ℝ)
75		eqid 2731	. . . . 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 7098	. . . 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 7409	. . . . . 6 ⊢ (𝜑 → (ℝ D 𝑂) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))))
80		reelprrecn 11184	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
81	80	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
82	43	recnd 11224	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
83	40	recnd 11224	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
84		eqid 2731	. . . . . . . . . 10 ⊢ (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) = (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
85	38, 3, 4, 8, 84, 1	fourierdlem28 44624	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
86	42	recnd 11224	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℂ)
87		0red 11199	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
88		iooretop 24211	. . . . . . . . . . . 12 ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
89		eqid 2731	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
90	89	tgioo2 24248	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
91	88, 90	eleqtri 2830	. . . . . . . . . . 11 ⊢ (𝐴(,)𝐵) ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ)
92	91	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(,)𝐵) ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
93	41	recnd 11224	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℂ)
94	81, 92, 93	dvmptconst 44404	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 0))
95	81, 83, 29, 85, 86, 87, 94	dvmptsub 25413	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)))
96	29	recnd 11224	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ)
97	96	subid1d 11542	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))
98	97	mpteq2dva 5241	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
99	95, 98	eqtrd 2771	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
100		eldifsn 4783	. . . . . . . 8 ⊢ ((2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}) ↔ ((2 · (sin‘(𝑠 / 2))) ∈ ℂ ∧ (2 · (sin‘(𝑠 / 2))) ≠ 0))
101	51, 70, 100	sylanbrc 583	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
102		recn 11182	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℝ → 𝑠 ∈ ℂ)
103	54	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℝ → 2 ≠ 0)
104	102, 47, 103	divrec2d 11976	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℝ → (𝑠 / 2) = ((1 / 2) · 𝑠))
105	104	eqcomd 2737	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ → ((1 / 2) · 𝑠) = (𝑠 / 2))
106	13, 105	syl 17	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((1 / 2) · 𝑠) = (𝑠 / 2))
107	106	fveq2d 6882	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘((1 / 2) · 𝑠)) = (cos‘(𝑠 / 2)))
108		halfcn 12409	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℂ
109	108	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℂ → (1 / 2) ∈ ℂ)
110		id 22	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℂ → 𝑠 ∈ ℂ)
111	109, 110	mulcld 11216	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℂ → ((1 / 2) · 𝑠) ∈ ℂ)
112	111	coscld 16056	. . . . . . . . . 10 ⊢ (𝑠 ∈ ℂ → (cos‘((1 / 2) · 𝑠)) ∈ ℂ)
113	13, 102, 112	3syl 18	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘((1 / 2) · 𝑠)) ∈ ℂ)
114	107, 113	eqeltrrd 2833	. . . . . . . 8 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘(𝑠 / 2)) ∈ ℂ)
115	114	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℂ)
116		ioossre 13367	. . . . . . . . . . . . 13 ⊢ (𝐴(,)𝐵) ⊆ ℝ
117		resmpt 6027	. . . . . . . . . . . . 13 ⊢ ((𝐴(,)𝐵) ⊆ ℝ → ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2)))))
118	116, 117	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))
119	118	eqcomi 2740	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2)))) = ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵))
120	119	oveq2i 7404	. . . . . . . . . 10 ⊢ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (ℝ D ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵)))
121		ax-resscn 11149	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℂ
122		eqid 2731	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))
123	122, 50	fmpti 7096	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))):ℝ⟶ℂ
124		ssid 4000	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℝ
125	89, 90	dvres 25357	. . . . . . . . . . 11 ⊢ (((ℝ ⊆ ℂ ∧ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ)) → (ℝ D ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵))) = ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵))))
126	121, 123, 124, 116, 125	mp4an 691	. . . . . . . . . 10 ⊢ (ℝ D ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵))) = ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)))
127		resmpt 6027	. . . . . . . . . . . . . . 15 ⊢ (ℝ ⊆ ℂ → ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) = (𝑠 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑠)))))
128	121, 127	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) = (𝑠 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑠))))
129	105	fveq2d 6882	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ℝ → (sin‘((1 / 2) · 𝑠)) = (sin‘(𝑠 / 2)))
130	129	oveq2d 7409	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℝ → (2 · (sin‘((1 / 2) · 𝑠))) = (2 · (sin‘(𝑠 / 2))))
131	130	mpteq2ia 5244	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))
132	128, 131	eqtr2i 2760	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) = ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)
133	132	oveq2i 7404	. . . . . . . . . . . 12 ⊢ (ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) = (ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ))
134		ioontr 43997	. . . . . . . . . . . 12 ⊢ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) = (𝐴(,)𝐵)
135	133, 134	reseq12i 5971	. . . . . . . . . . 11 ⊢ ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵))) = ((ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) ↾ (𝐴(,)𝐵))
136		eqid 2731	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))
137		2cnd 12272	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℂ → 2 ∈ ℂ)
138	111	sincld 16055	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℂ → (sin‘((1 / 2) · 𝑠)) ∈ ℂ)
139	137, 138	mulcld 11216	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ℂ → (2 · (sin‘((1 / 2) · 𝑠))) ∈ ℂ)
140	136, 139	fmpti 7096	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))):ℂ⟶ℂ
141		ssid 4000	. . . . . . . . . . . . 13 ⊢ ℂ ⊆ ℂ
142		dmmptg 6230	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑠 ∈ ℂ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) ∈ ℂ → dom (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) = ℂ)
143		2cn 12269	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℂ
144	143, 108	mulcli 11203	. . . . . . . . . . . . . . . . . 18 ⊢ (2 · (1 / 2)) ∈ ℂ
145	144	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ ℂ → (2 · (1 / 2)) ∈ ℂ)
146	145, 112	mulcld 11216	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ℂ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) ∈ ℂ)
147	142, 146	mprg 3066	. . . . . . . . . . . . . . 15 ⊢ dom (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) = ℂ
148	121, 147	sseqtrri 4015	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ dom (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
149		dvasinbx 44409	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))))
150	143, 108, 149	mp2an 690	. . . . . . . . . . . . . . 15 ⊢ (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
151	150	dmeqi 5896	. . . . . . . . . . . . . 14 ⊢ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = dom (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
152	148, 151	sseqtrri 4015	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))))
153		dvres3 25359	. . . . . . . . . . . . 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 691	. . . . . . . . . . . 12 ⊢ (ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) = ((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ)
155	154	reseq1i 5969	. . . . . . . . . . 11 ⊢ ((ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) ↾ (𝐴(,)𝐵)) = (((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) ↾ (𝐴(,)𝐵))
156	150	reseq1i 5969	. . . . . . . . . . . . 13 ⊢ ((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) = ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ ℝ)
157	156	reseq1i 5969	. . . . . . . . . . . 12 ⊢ (((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) ↾ (𝐴(,)𝐵)) = (((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ ℝ) ↾ (𝐴(,)𝐵))
158		resabs1 6003	. . . . . . . . . . . . 13 ⊢ ((𝐴(,)𝐵) ⊆ ℝ → (((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ ℝ) ↾ (𝐴(,)𝐵)) = ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ (𝐴(,)𝐵)))
159	116, 158	ax-mp 5	. . . . . . . . . . . 12 ⊢ (((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ ℝ) ↾ (𝐴(,)𝐵)) = ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ (𝐴(,)𝐵))
160		ioosscn 13368	. . . . . . . . . . . . 13 ⊢ (𝐴(,)𝐵) ⊆ ℂ
161		resmpt 6027	. . . . . . . . . . . . 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 2763	. . . . . . . . . . 11 ⊢ (((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
164	135, 155, 163	3eqtri 2763	. . . . . . . . . 10 ⊢ ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
165	120, 126, 164	3eqtri 2763	. . . . . . . . 9 ⊢ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
166	143, 54	recidi 11927	. . . . . . . . . . . . 13 ⊢ (2 · (1 / 2)) = 1
167	166	oveq1i 7403	. . . . . . . . . . . 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	113	mullidd 11214	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (1 · (cos‘((1 / 2) · 𝑠))) = (cos‘((1 / 2) · 𝑠)))
170	168, 169, 107	3eqtrd 2775	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) = (cos‘(𝑠 / 2)))
171	170	mpteq2ia 5244	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))
172	165, 171	eqtri 2759	. . . . . . . 8 ⊢ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))
173	172	a1i 11	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))))
174	81, 82, 29, 99, 101, 115, 173	dvmptdiv 25420	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))
175	79, 174	eqtrd 2771	. . . . 5 ⊢ (𝜑 → (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))
176	175	feq1d 6689	. . . 4 ⊢ (𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ↔ (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))):(𝐴(,)𝐵)⟶ℝ))
177	76, 176	mpbird 256	. . 3 ⊢ (𝜑 → (ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ)
178	177, 175	jca 512	. 2 ⊢ (𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)))))
179	178, 172	pm3.2i 471	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 396 = wceq 1541 ∈ wcel 2106 ≠ wne 2939 ∖ cdif 3941 ⊆ wss 3944 {csn 4622 {cpr 4624 class class class wbr 5141 ↦ cmpt 5224 dom cdm 5669 ran crn 5670 ↾ cres 5671 ⟶wf 6528 ‘cfv 6532 (class class class)co 7393 ℂcc 11090 ℝcr 11091 0cc0 11092 1c1 11093 + caddc 11095 · cmul 11097 ℝ^*cxr 11229 < clt 11230 − cmin 11426 -cneg 11427 / cdiv 11853 2c2 12249 ℤcz 12540 (,)cioo 13306 [,]cicc 13309 ↑cexp 14009 sincsin 15989 cosccos 15990 πcpi 15992 ↾_t crest 17348 TopOpenctopn 17349 topGenctg 17365 ℂ_fldccnfld 20878 intcnt 22450 D cdv 25309

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7708 ax-inf2 9618 ax-cnex 11148 ax-resscn 11149 ax-1cn 11150 ax-icn 11151 ax-addcl 11152 ax-addrcl 11153 ax-mulcl 11154 ax-mulrcl 11155 ax-mulcom 11156 ax-addass 11157 ax-mulass 11158 ax-distr 11159 ax-i2m1 11160 ax-1ne0 11161 ax-1rid 11162 ax-rnegex 11163 ax-rrecex 11164 ax-cnre 11165 ax-pre-lttri 11166 ax-pre-lttrn 11167 ax-pre-ltadd 11168 ax-pre-mulgt0 11169 ax-pre-sup 11170 ax-addf 11171 ax-mulf 11172

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4523 df-pw 4598 df-sn 4623 df-pr 4625 df-tp 4627 df-op 4629 df-uni 4902 df-int 4944 df-iun 4992 df-iin 4993 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-se 5625 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6289 df-ord 6356 df-on 6357 df-lim 6358 df-suc 6359 df-iota 6484 df-fun 6534 df-fn 6535 df-f 6536 df-f1 6537 df-fo 6538 df-f1o 6539 df-fv 6540 df-isom 6541 df-riota 7349 df-ov 7396 df-oprab 7397 df-mpo 7398 df-of 7653 df-om 7839 df-1st 7957 df-2nd 7958 df-supp 8129 df-frecs 8248 df-wrecs 8279 df-recs 8353 df-rdg 8392 df-1o 8448 df-2o 8449 df-er 8686 df-map 8805 df-pm 8806 df-ixp 8875 df-en 8923 df-dom 8924 df-sdom 8925 df-fin 8926 df-fsupp 9345 df-fi 9388 df-sup 9419 df-inf 9420 df-oi 9487 df-card 9916 df-pnf 11232 df-mnf 11233 df-xr 11234 df-ltxr 11235 df-le 11236 df-sub 11428 df-neg 11429 df-div 11854 df-nn 12195 df-2 12257 df-3 12258 df-4 12259 df-5 12260 df-6 12261 df-7 12262 df-8 12263 df-9 12264 df-n0 12455 df-z 12541 df-dec 12660 df-uz 12805 df-q 12915 df-rp 12957 df-xneg 13074 df-xadd 13075 df-xmul 13076 df-ioo 13310 df-ioc 13311 df-ico 13312 df-icc 13313 df-fz 13467 df-fzo 13610 df-fl 13739 df-mod 13817 df-seq 13949 df-exp 14010 df-fac 14216 df-bc 14245 df-hash 14273 df-shft 14996 df-cj 15028 df-re 15029 df-im 15030 df-sqrt 15164 df-abs 15165 df-limsup 15397 df-clim 15414 df-rlim 15415 df-sum 15615 df-ef 15993 df-sin 15995 df-cos 15996 df-pi 15998 df-struct 17062 df-sets 17079 df-slot 17097 df-ndx 17109 df-base 17127 df-ress 17156 df-plusg 17192 df-mulr 17193 df-starv 17194 df-sca 17195 df-vsca 17196 df-ip 17197 df-tset 17198 df-ple 17199 df-ds 17201 df-unif 17202 df-hom 17203 df-cco 17204 df-rest 17350 df-topn 17351 df-0g 17369 df-gsum 17370 df-topgen 17371 df-pt 17372 df-prds 17375 df-xrs 17430 df-qtop 17435 df-imas 17436 df-xps 17438 df-mre 17512 df-mrc 17513 df-acs 17515 df-mgm 18543 df-sgrp 18592 df-mnd 18603 df-submnd 18648 df-mulg 18923 df-cntz 19147 df-cmn 19614 df-psmet 20870 df-xmet 20871 df-met 20872 df-bl 20873 df-mopn 20874 df-fbas 20875 df-fg 20876 df-cnfld 20879 df-top 22325 df-topon 22342 df-topsp 22364 df-bases 22378 df-cld 22452 df-ntr 22453 df-cls 22454 df-nei 22531 df-lp 22569 df-perf 22570 df-cn 22660 df-cnp 22661 df-t1 22747 df-haus 22748 df-tx 22995 df-hmeo 23188 df-fil 23279 df-fm 23371 df-flim 23372 df-flf 23373 df-xms 23755 df-ms 23756 df-tms 23757 df-cncf 24323 df-limc 25312 df-dv 25313

This theorem is referenced by: fourierdlem68 44663 fourierdlem80 44675

W3C validator