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 46937

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 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)
3		fourierdlem57.xre	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ ℝ)
4		fourierdlem57.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5	3, 4	readdcld 11255	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ)
6	5	rexrd 11276	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ^*)
7	6	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) ∈ ℝ^*)
8		fourierdlem57.b	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9	3, 8	readdcld 11255	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ)
10	9	rexrd 11276	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ^*)
11	10	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) ∈ ℝ^*)
12	3	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ)
13		elioore 13420	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ)
14	13	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
15	12, 14	readdcld 11255	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
16	4	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
17	16	rexrd 11276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ^*)
18	8	rexrd 11276	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
19	18	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ^*)
20		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵))
21		ioogtlb 46271	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
22	17, 19, 20, 21	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
23	16, 14, 12, 22	ltadd2dd 11386	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠))
24	8	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ)
25		iooltub 46286	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
26	17, 19, 20, 25	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
27	14, 24, 12, 26	ltadd2dd 11386	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵))
28	7, 11, 15, 23, 27	eliood 46274	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))
29	2, 28	ffvelcdmd 7084	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℝ)
30		2re 12332	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
31	30	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℝ)
32		rehalfcl 12488	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ → (𝑠 / 2) ∈ ℝ)
33	14, 32	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑠 / 2) ∈ ℝ)
34	33	resincld 16223	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℝ)
35	31, 34	remulcld 11256	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
36	29, 35	remulcld 11256	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) ∈ ℝ)
37	33	recoscld 16224	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℝ)
38		fourierdlem57.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
39	38	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ)
40	39, 15	ffvelcdmd 7084	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
41		fourierdlem57.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℝ)
42	41	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ)
43	40, 42	resubcld 11659	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℝ)
44	37, 43	remulcld 11256	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ ℝ)
45	36, 44	resubcld 11659	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) ∈ ℝ)
46	35	resqcld 14181	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((2 · (sin‘(𝑠 / 2)))↑2) ∈ ℝ)
47		2cnd 12336	. . . . . . . . 9 ⊢ (𝑠 ∈ ℝ → 2 ∈ ℂ)
48	32	recnd 11254	. . . . . . . . . 10 ⊢ (𝑠 ∈ ℝ → (𝑠 / 2) ∈ ℂ)
49	48	sincld 16210	. . . . . . . . 9 ⊢ (𝑠 ∈ ℝ → (sin‘(𝑠 / 2)) ∈ ℂ)
50	47, 49	mulcld 11246	. . . . . . . 8 ⊢ (𝑠 ∈ ℝ → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
51	14, 50	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
52		2cnd 12336	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ)
53	14, 49	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ∈ ℂ)
54		2ne0 12364	. . . . . . . . 9 ⊢ 2 ≠ 0
55	54	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ≠ 0)
56		fourierdlem57.ab	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π))
57	56	sselda 3938	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (-π[,]π))
58		eqcom 2772	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 0 ↔ 0 = 𝑠)
59	58	bilani 510	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 = 𝑠)
60		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 𝑠 ∈ (𝐴(,)𝐵))
61	59, 60	eqeltrd 2865	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵))
62	61	adantll 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵))
63		fourierdlem57.n0	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))
64	63	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴(,)𝐵))
65	62, 64	pm2.65da 829	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 = 0)
66	65	neqned 2967	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≠ 0)
67		fourierdlem44 46925	. . . . . . . . 9 ⊢ ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
68	57, 66, 67	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (sin‘(𝑠 / 2)) ≠ 0)
69	52, 53, 55, 68	mulne0d 11883	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
70		2z 12643	. . . . . . . 8 ⊢ 2 ∈ ℤ
71	70	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 2 ∈ ℤ)
72	51, 69, 71	expne0d 14208	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((2 · (sin‘(𝑠 / 2)))↑2) ≠ 0)
73	45, 46, 72	redivcld 12060	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)) ∈ ℝ)
74		eqid 2765	. . . . 5 ⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)))
75	73, 74	fmptd 7113	. . . 4 ⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))):(𝐴(,)𝐵)⟶ℝ)
76		fourierdlem57.o	. . . . . . . 8 ⊢ 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
77	76	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
78	77	oveq2d 7435	. . . . . 6 ⊢ (𝜑 → (ℝ D 𝑂) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))))
79		reelprrecn 11209	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
80	79	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
81	43	recnd 11254	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
82	40	recnd 11254	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
83		eqid 2765	. . . . . . . . . 10 ⊢ (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) = (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
84	38, 3, 4, 8, 83, 1	fourierdlem28 46909	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
85	42	recnd 11254	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℂ)
86		0red 11228	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
87		iooretop 24975	. . . . . . . . . . . 12 ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
88		tgioo4 25015	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
89	87, 88	eleqtri 2863	. . . . . . . . . . 11 ⊢ (𝐴(,)𝐵) ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ)
90	89	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(,)𝐵) ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
91	41	recnd 11254	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℂ)
92	80, 90, 91	dvmptconst 46689	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 0))
93	80, 82, 29, 84, 85, 86, 92	dvmptsub 26179	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)))
94	29	recnd 11254	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ)
95	94	subid1d 11575	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))
96	95	mpteq2dva 5206	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
97	93, 96	eqtrd 2800	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
98		eldifsn 4755	. . . . . . . 8 ⊢ ((2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}) ↔ ((2 · (sin‘(𝑠 / 2))) ∈ ℂ ∧ (2 · (sin‘(𝑠 / 2))) ≠ 0))
99	51, 69, 98	sylanbrc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
100		recn 11207	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℝ → 𝑠 ∈ ℂ)
101	54	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℝ → 2 ≠ 0)
102	100, 47, 101	divrec2d 12012	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℝ → (𝑠 / 2) = ((1 / 2) · 𝑠))
103	102	eqcomd 2771	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ → ((1 / 2) · 𝑠) = (𝑠 / 2))
104	13, 103	syl 18	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((1 / 2) · 𝑠) = (𝑠 / 2))
105	104	fveq2d 6889	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘((1 / 2) · 𝑠)) = (cos‘(𝑠 / 2)))
106		halfcn 12475	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℂ
107	106	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℂ → (1 / 2) ∈ ℂ)
108		id 23	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℂ → 𝑠 ∈ ℂ)
109	107, 108	mulcld 11246	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℂ → ((1 / 2) · 𝑠) ∈ ℂ)
110	109	coscld 16211	. . . . . . . . . 10 ⊢ (𝑠 ∈ ℂ → (cos‘((1 / 2) · 𝑠)) ∈ ℂ)
111	13, 100, 110	3syl 19	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘((1 / 2) · 𝑠)) ∈ ℂ)
112	105, 111	eqeltrrd 2866	. . . . . . . 8 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘(𝑠 / 2)) ∈ ℂ)
113	112	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℂ)
114		ioossre 13452	. . . . . . . . . . . . 13 ⊢ (𝐴(,)𝐵) ⊆ ℝ
115		resmpt 6041	. . . . . . . . . . . . 13 ⊢ ((𝐴(,)𝐵) ⊆ ℝ → ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2)))))
116	114, 115	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))
117	116	eqcomi 2774	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2)))) = ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵))
118	117	oveq2i 7430	. . . . . . . . . 10 ⊢ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (ℝ D ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵)))
119		ax-resscn 11174	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℂ
120		eqid 2765	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))
121	120, 50	fmpti 7111	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))):ℝ⟶ℂ
122		ssid 3960	. . . . . . . . . . 11 ⊢ ℝ ⊆ ℝ
123		eqid 2765	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
124	123, 88	dvres 26123	. . . . . . . . . . 11 ⊢ (((ℝ ⊆ ℂ ∧ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ)) → (ℝ D ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵))) = ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵))))
125	119, 121, 122, 114, 124	mp4an 706	. . . . . . . . . 10 ⊢ (ℝ D ((𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ (𝐴(,)𝐵))) = ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)))
126		resmpt 6041	. . . . . . . . . . . . . . 15 ⊢ (ℝ ⊆ ℂ → ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) = (𝑠 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑠)))))
127	119, 126	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) = (𝑠 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑠))))
128	103	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ℝ → (sin‘((1 / 2) · 𝑠)) = (sin‘(𝑠 / 2)))
129	128	oveq2d 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℝ → (2 · (sin‘((1 / 2) · 𝑠))) = (2 · (sin‘(𝑠 / 2))))
130	129	mpteq2ia 5208	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))
131	127, 130	eqtr2i 2789	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2)))) = ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)
132	131	oveq2i 7430	. . . . . . . . . . . 12 ⊢ (ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) = (ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ))
133		ioontr 46287	. . . . . . . . . . . 12 ⊢ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) = (𝐴(,)𝐵)
134	132, 133	reseq12i 5978	. . . . . . . . . . 11 ⊢ ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵))) = ((ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) ↾ (𝐴(,)𝐵))
135		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))
136		2cnd 12336	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℂ → 2 ∈ ℂ)
137	109	sincld 16210	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℂ → (sin‘((1 / 2) · 𝑠)) ∈ ℂ)
138	136, 137	mulcld 11246	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ℂ → (2 · (sin‘((1 / 2) · 𝑠))) ∈ ℂ)
139	135, 138	fmpti 7111	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))):ℂ⟶ℂ
140		ssid 3960	. . . . . . . . . . . . 13 ⊢ ℂ ⊆ ℂ
141		dmmptg 6245	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑠 ∈ ℂ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) ∈ ℂ → dom (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) = ℂ)
142		2cn 12333	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℂ
143	142, 106	mulcli 11233	. . . . . . . . . . . . . . . . . 18 ⊢ (2 · (1 / 2)) ∈ ℂ
144	143	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ ℂ → (2 · (1 / 2)) ∈ ℂ)
145	144, 110	mulcld 11246	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ℂ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) ∈ ℂ)
146	141, 145	mprg 3087	. . . . . . . . . . . . . . 15 ⊢ dom (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) = ℂ
147	119, 146	sseqtrri 3987	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ dom (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
148		dvasinbx 46694	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))))
149	142, 106, 148	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
150	149	dmeqi 5896	. . . . . . . . . . . . . 14 ⊢ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = dom (𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
151	147, 150	sseqtrri 3987	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))))
152		dvres3 26125	. . . . . . . . . . . . 13 ⊢ (((ℝ ∈ {ℝ, ℂ} ∧ (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))):ℂ⟶ℂ) ∧ (ℂ ⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))))) → (ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) = ((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ))
153	79, 139, 140, 151, 152	mp4an 706	. . . . . . . . . . . 12 ⊢ (ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) = ((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ)
154	153	reseq1i 5976	. . . . . . . . . . 11 ⊢ ((ℝ D ((𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) ↾ (𝐴(,)𝐵)) = (((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) ↾ (𝐴(,)𝐵))
155	149	reseq1i 5976	. . . . . . . . . . . . 13 ⊢ ((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) = ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ ℝ)
156	155	reseq1i 5976	. . . . . . . . . . . 12 ⊢ (((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) ↾ (𝐴(,)𝐵)) = (((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ ℝ) ↾ (𝐴(,)𝐵))
157		resabs1 6007	. . . . . . . . . . . . 13 ⊢ ((𝐴(,)𝐵) ⊆ ℝ → (((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ ℝ) ↾ (𝐴(,)𝐵)) = ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ (𝐴(,)𝐵)))
158	114, 157	ax-mp 5	. . . . . . . . . . . 12 ⊢ (((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ ℝ) ↾ (𝐴(,)𝐵)) = ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ (𝐴(,)𝐵))
159		ioosscn 13453	. . . . . . . . . . . . 13 ⊢ (𝐴(,)𝐵) ⊆ ℂ
160		resmpt 6041	. . . . . . . . . . . . 13 ⊢ ((𝐴(,)𝐵) ⊆ ℂ → ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))))
161	159, 160	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
162	156, 158, 161	3eqtri 2792	. . . . . . . . . . 11 ⊢ (((ℂ D (𝑠 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) ↾ (𝐴(,)𝐵)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
163	134, 154, 162	3eqtri 2792	. . . . . . . . . 10 ⊢ ((ℝ D (𝑠 ∈ ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
164	118, 125, 163	3eqtri 2792	. . . . . . . . 9 ⊢ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))))
165		2thalfe1 12365	. . . . . . . . . . . . 13 ⊢ (2 · (1 / 2)) = 1
166	165	oveq1i 7429	. . . . . . . . . . . 12 ⊢ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) = (1 · (cos‘((1 / 2) · 𝑠)))
167	166	a1i 11	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) = (1 · (cos‘((1 / 2) · 𝑠))))
168	111	mullidd 11244	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (1 · (cos‘((1 / 2) · 𝑠))) = (cos‘((1 / 2) · 𝑠)))
169	167, 168, 105	3eqtrd 2804	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠))) = (cos‘(𝑠 / 2)))
170	169	mpteq2ia 5208	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))
171	164, 170	eqtri 2788	. . . . . . . 8 ⊢ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))
172	171	a1i 11	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))))
173	80, 81, 29, 97, 99, 113, 172	dvmptdiv 26186	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))
174	78, 173	eqtrd 2800	. . . . 5 ⊢ (𝜑 → (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))
175	174	feq1d 6691	. . . 4 ⊢ (𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ↔ (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))):(𝐴(,)𝐵)⟶ℝ))
176	75, 175	mpbird 260	. . 3 ⊢ (𝜑 → (ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ)
177	176, 174	jca 521	. 2 ⊢ (𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)))))
178	177, 171	pm3.2i 476	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

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∖ cdif 3903 ⊆ wss 3906 {csn 4591 {cpr 4593 class class class wbr 5111 ↦ cmpt 5194 dom cdm 5663 ran crn 5664 ↾ cres 5665 ⟶wf 6536 ‘cfv 6540 (class class class)co 7419 ℂcc 11115 ℝcr 11116 0cc0 11117 1c1 11118 + caddc 11120 · cmul 11122 ℝ^*cxr 11259 < clt 11260 − cmin 11458 -cneg 11459 / cdiv 11888 2c2 12312 ℤcz 12608 (,)cioo 13390 [,]cicc 13393 ↑cexp 14117 sincsin 16141 cosccos 16142 πcpi 16144 ↾_t crest 17497 TopOpenctopn 17498 topGenctg 17514 ℂ_fldccnfld 21574 intcnt 23226 D cdv 26075

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-inf2 9617 ax-cnex 11173 ax-resscn 11174 ax-1cn 11175 ax-icn 11176 ax-addcl 11177 ax-addrcl 11178 ax-mulcl 11179 ax-mulrcl 11180 ax-mulcom 11181 ax-addass 11182 ax-mulass 11183 ax-distr 11184 ax-i2m1 11185 ax-1ne0 11186 ax-1rid 11187 ax-rnegex 11188 ax-rrecex 11189 ax-cnre 11190 ax-pre-lttri 11191 ax-pre-lttrn 11192 ax-pre-ltadd 11193 ax-pre-mulgt0 11194 ax-pre-sup 11195 ax-addf 11196

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-of 7684 df-om 7869 df-1st 7992 df-2nd 7993 df-supp 8163 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-pm 8833 df-ixp 8902 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-fsupp 9329 df-fi 9378 df-sup 9409 df-inf 9410 df-oi 9479 df-card 9941 df-pnf 11262 df-mnf 11263 df-xr 11264 df-ltxr 11265 df-le 11266 df-sub 11460 df-neg 11461 df-div 11889 df-nn 12251 df-2 12320 df-3 12321 df-4 12322 df-5 12323 df-6 12324 df-7 12325 df-8 12326 df-9 12327 df-n0 12522 df-z 12609 df-dec 12730 df-uz 12881 df-q 12991 df-rp 13035 df-xneg 13155 df-xadd 13156 df-xmul 13157 df-ioo 13394 df-ioc 13395 df-ico 13396 df-icc 13397 df-fz 13554 df-fzo 13702 df-fl 13845 df-mod 13923 df-seq 14058 df-exp 14118 df-fac 14330 df-bc 14359 df-hash 14387 df-shft 15130 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-limsup 15548 df-clim 15565 df-rlim 15566 df-sum 15764 df-ef 16145 df-sin 16147 df-cos 16148 df-pi 16150 df-struct 17231 df-sets 17248 df-slot 17266 df-ndx 17278 df-base 17294 df-ress 17315 df-plusg 17347 df-mulr 17348 df-starv 17349 df-sca 17350 df-vsca 17351 df-ip 17352 df-tset 17353 df-ple 17354 df-ds 17356 df-unif 17357 df-hom 17358 df-cco 17359 df-rest 17499 df-topn 17500 df-0g 17518 df-gsum 17519 df-topgen 17520 df-pt 17521 df-prds 17524 df-xrs 17580 df-qtop 17585 df-imas 17586 df-xps 17588 df-mre 17662 df-mrc 17663 df-acs 17665 df-mgm 18722 df-sgrp 18811 df-mnd 18827 df-submnd 18881 df-mulg 19180 df-cntz 19433 df-cmn 19898 df-psmet 21566 df-xmet 21567 df-met 21568 df-bl 21569 df-mopn 21570 df-fbas 21571 df-fg 21572 df-cnfld 21575 df-top 23103 df-topon 23120 df-topsp 23142 df-bases 23155 df-cld 23228 df-ntr 23229 df-cls 23230 df-nei 23307 df-lp 23345 df-perf 23346 df-cn 23436 df-cnp 23437 df-t1 23523 df-haus 23524 df-tx 23772 df-hmeo 23965 df-fil 24056 df-fm 24148 df-flim 24149 df-flf 24150 df-xms 24530 df-ms 24531 df-tms 24532 df-cncf 25090 df-limc 26078 df-dv 26079

This theorem is used by: fourierdlem68 46948 fourierdlem80 46960

W3C validator