fourierdlem39

Description: Integration by parts of S. ( A (,) B ) ( ( Fx ) x. ( sin( R x. x ) ) ) _d x (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem39.a	$⊢ φ \to A \in ℝ$
	fourierdlem39.b	$⊢ φ \to B \in ℝ$
	fourierdlem39.aleb	$⊢ φ \to A \leq B$
	fourierdlem39.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
	fourierdlem39.g	$⊢ G = ℝ D F$
	fourierdlem39.gcn	$⊢ φ \to G : (A, B) \underset{cn}{⟶} ℂ$
	fourierdlem39.gbd	$⊢ φ \to \exists y \in ℝ \forall x \in (A, B) \|G (x)\| \leq y$
	fourierdlem39.r	$⊢ φ \to R \in ℝ^{+}$
Assertion	fourierdlem39	$⊢ φ \to \int_{(A, B)} F (x) \sin R x d x = F (B) (- \frac{\cos R B}{R}) - F (A) (- \frac{\cos R A}{R}) - \int_{(A, B)} G (x) (- \frac{\cos R x}{R}) d x$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem39.a	$⊢ φ \to A \in ℝ$
2		fourierdlem39.b	$⊢ φ \to B \in ℝ$
3		fourierdlem39.aleb	$⊢ φ \to A \leq B$
4		fourierdlem39.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
5		fourierdlem39.g	$⊢ G = ℝ D F$
6		fourierdlem39.gcn	$⊢ φ \to G : (A, B) \underset{cn}{⟶} ℂ$
7		fourierdlem39.gbd	$⊢ φ \to \exists y \in ℝ \forall x \in (A, B) \|G (x)\| \leq y$
8		fourierdlem39.r	$⊢ φ \to R \in ℝ^{+}$
9		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℂ \to F : [A, B] ⟶ ℂ$
10	4 9	syl	$⊢ φ \to F : [A, B] ⟶ ℂ$
11	10	feqmptd	$⊢ φ \to F = (x \in [A, B] ⟼ F (x))$
12	11	eqcomd	$⊢ φ \to (x \in [A, B] ⟼ F (x)) = F$
13	12 4	eqeltrd	$⊢ φ \to (x \in [A, B] ⟼ F (x)) : [A, B] \underset{cn}{⟶} ℂ$
14		coscn	$⊢ \cos : ℂ \underset{cn}{⟶} ℂ$
15	14	a1i	$⊢ φ \to \cos : ℂ \underset{cn}{⟶} ℂ$
16	1 2	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
17		ax-resscn	$⊢ ℝ \subseteq ℂ$
18	16 17	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
19	8	rpred	$⊢ φ \to R \in ℝ$
20	19	recnd	$⊢ φ \to R \in ℂ$
21		ssid	$⊢ ℂ \subseteq ℂ$
22	21	a1i	$⊢ φ \to ℂ \subseteq ℂ$
23	18 20 22	constcncfg	$⊢ φ \to (x \in [A, B] ⟼ R) : [A, B] \underset{cn}{⟶} ℂ$
24	18 22	idcncfg	$⊢ φ \to (x \in [A, B] ⟼ x) : [A, B] \underset{cn}{⟶} ℂ$
25	23 24	mulcncf	$⊢ φ \to (x \in [A, B] ⟼ R x) : [A, B] \underset{cn}{⟶} ℂ$
26	15 25	cncfmpt1f	$⊢ φ \to (x \in [A, B] ⟼ \cos R x) : [A, B] \underset{cn}{⟶} ℂ$
27	8	rpcnne0d	$⊢ φ \to (R \in ℂ \land R \neq 0)$
28		eldifsn	$⊢ R \in (ℂ ∖ \{0\}) \leftrightarrow (R \in ℂ \land R \neq 0)$
29	27 28	sylibr	$⊢ φ \to R \in (ℂ ∖ \{0\})$
30		difssd	$⊢ φ \to ℂ ∖ \{0\} \subseteq ℂ$
31	18 29 30	constcncfg	$⊢ φ \to (x \in [A, B] ⟼ R) : [A, B] \underset{cn}{⟶} (ℂ ∖ \{0\})$
32	26 31	divcncf	$⊢ φ \to (x \in [A, B] ⟼ \frac{\cos R x}{R}) : [A, B] \underset{cn}{⟶} ℂ$
33	32	negcncfg	$⊢ φ \to (x \in [A, B] ⟼ - \frac{\cos R x}{R}) : [A, B] \underset{cn}{⟶} ℂ$
34		cncff	$⊢ G : (A, B) \underset{cn}{⟶} ℂ \to G : (A, B) ⟶ ℂ$
35	6 34	syl	$⊢ φ \to G : (A, B) ⟶ ℂ$
36	35	feqmptd	$⊢ φ \to G = (x \in (A, B) ⟼ G (x))$
37	36	eqcomd	$⊢ φ \to (x \in (A, B) ⟼ G (x)) = G$
38	37 6	eqeltrd	$⊢ φ \to (x \in (A, B) ⟼ G (x)) : (A, B) \underset{cn}{⟶} ℂ$
39		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
40	39	a1i	$⊢ φ \to \sin : ℂ \underset{cn}{⟶} ℂ$
41		ioosscn	$⊢ (A, B) \subseteq ℂ$
42	41	a1i	$⊢ φ \to (A, B) \subseteq ℂ$
43	42 20 22	constcncfg	$⊢ φ \to (x \in (A, B) ⟼ R) : (A, B) \underset{cn}{⟶} ℂ$
44	42 22	idcncfg	$⊢ φ \to (x \in (A, B) ⟼ x) : (A, B) \underset{cn}{⟶} ℂ$
45	43 44	mulcncf	$⊢ φ \to (x \in (A, B) ⟼ R x) : (A, B) \underset{cn}{⟶} ℂ$
46	40 45	cncfmpt1f	$⊢ φ \to (x \in (A, B) ⟼ \sin R x) : (A, B) \underset{cn}{⟶} ℂ$
47		ioombl	$⊢ (A, B) \in dom vol$
48	47	a1i	$⊢ φ \to (A, B) \in dom vol$
49		volioo	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B)) = B - A$
50	1 2 3 49	syl3anc	$⊢ φ \to vol ((A, B)) = B - A$
51	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
52	50 51	eqeltrd	$⊢ φ \to vol ((A, B)) \in ℝ$
53		eqid	$⊢ (x \in [A, B] ⟼ F (x)) = (x \in [A, B] ⟼ F (x))$
54		ioossicc	$⊢ (A, B) \subseteq [A, B]$
55	54	a1i	$⊢ φ \to (A, B) \subseteq [A, B]$
56	10	adantr	$⊢ (φ \land x \in (A, B)) \to F : [A, B] ⟶ ℂ$
57	55	sselda	$⊢ (φ \land x \in (A, B)) \to x \in [A, B]$
58	56 57	ffvelcdmd	$⊢ (φ \land x \in (A, B)) \to F (x) \in ℂ$
59	53 13 55 22 58	cncfmptssg	$⊢ φ \to (x \in (A, B) ⟼ F (x)) : (A, B) \underset{cn}{⟶} ℂ$
60	59 46	mulcncf	$⊢ φ \to (x \in (A, B) ⟼ F (x) \sin R x) : (A, B) \underset{cn}{⟶} ℂ$
61		cniccbdd	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to \exists y \in ℝ \forall z \in [A, B] \|F (z)\| \leq y$
62	1 2 4 61	syl3anc	$⊢ φ \to \exists y \in ℝ \forall z \in [A, B] \|F (z)\| \leq y$
63		nfra1	$⊢ Ⅎ z \forall z \in [A, B] \|F (z)\| \leq y$
64	54	sseli	$⊢ z \in (A, B) \to z \in [A, B]$
65		rspa	$⊢ (\forall z \in [A, B] \|F (z)\| \leq y \land z \in [A, B]) \to \|F (z)\| \leq y$
66	64 65	sylan2	$⊢ (\forall z \in [A, B] \|F (z)\| \leq y \land z \in (A, B)) \to \|F (z)\| \leq y$
67	66	ex	$⊢ \forall z \in [A, B] \|F (z)\| \leq y \to (z \in (A, B) \to \|F (z)\| \leq y)$
68	63 67	ralrimi	$⊢ \forall z \in [A, B] \|F (z)\| \leq y \to \forall z \in (A, B) \|F (z)\| \leq y$
69	68	a1i	$⊢ (φ \land y \in ℝ) \to (\forall z \in [A, B] \|F (z)\| \leq y \to \forall z \in (A, B) \|F (z)\| \leq y)$
70	69	reximdva	$⊢ φ \to (\exists y \in ℝ \forall z \in [A, B] \|F (z)\| \leq y \to \exists y \in ℝ \forall z \in (A, B) \|F (z)\| \leq y)$
71	62 70	mpd	$⊢ φ \to \exists y \in ℝ \forall z \in (A, B) \|F (z)\| \leq y$
72		nfv	$⊢ Ⅎ z (φ \land y \in ℝ)$
73		nfra1	$⊢ Ⅎ z \forall z \in (A, B) \|F (z)\| \leq y$
74	72 73	nfan	$⊢ Ⅎ z ((φ \land y \in ℝ) \land \forall z \in (A, B) \|F (z)\| \leq y)$
75		simpll	$⊢ (((φ \land y \in ℝ) \land \forall z \in (A, B) \|F (z)\| \leq y) \land z \in dom (x \in (A, B) ⟼ F (x) \sin R x)) \to (φ \land y \in ℝ)$
76		simpr	$⊢ (φ \land z \in dom (x \in (A, B) ⟼ F (x) \sin R x)) \to z \in dom (x \in (A, B) ⟼ F (x) \sin R x)$
77	19	adantr	$⊢ (φ \land x \in (A, B)) \to R \in ℝ$
78		elioore	$⊢ x \in (A, B) \to x \in ℝ$
79	78	adantl	$⊢ (φ \land x \in (A, B)) \to x \in ℝ$
80	77 79	remulcld	$⊢ (φ \land x \in (A, B)) \to R x \in ℝ$
81	80	resincld	$⊢ (φ \land x \in (A, B)) \to \sin R x \in ℝ$
82	81	recnd	$⊢ (φ \land x \in (A, B)) \to \sin R x \in ℂ$
83	58 82	mulcld	$⊢ (φ \land x \in (A, B)) \to F (x) \sin R x \in ℂ$
84	83	ralrimiva	$⊢ φ \to \forall x \in (A, B) F (x) \sin R x \in ℂ$
85		dmmptg	$⊢ \forall x \in (A, B) F (x) \sin R x \in ℂ \to dom (x \in (A, B) ⟼ F (x) \sin R x) = (A, B)$
86	84 85	syl	$⊢ φ \to dom (x \in (A, B) ⟼ F (x) \sin R x) = (A, B)$
87	86	adantr	$⊢ (φ \land z \in dom (x \in (A, B) ⟼ F (x) \sin R x)) \to dom (x \in (A, B) ⟼ F (x) \sin R x) = (A, B)$
88	76 87	eleqtrd	$⊢ (φ \land z \in dom (x \in (A, B) ⟼ F (x) \sin R x)) \to z \in (A, B)$
89	88	ad4ant14	$⊢ (((φ \land y \in ℝ) \land \forall z \in (A, B) \|F (z)\| \leq y) \land z \in dom (x \in (A, B) ⟼ F (x) \sin R x)) \to z \in (A, B)$
90		simplr	$⊢ ((φ \land \forall z \in (A, B) \|F (z)\| \leq y) \land z \in dom (x \in (A, B) ⟼ F (x) \sin R x)) \to \forall z \in (A, B) \|F (z)\| \leq y$
91	88	adantlr	$⊢ ((φ \land \forall z \in (A, B) \|F (z)\| \leq y) \land z \in dom (x \in (A, B) ⟼ F (x) \sin R x)) \to z \in (A, B)$
92		rspa	$⊢ (\forall z \in (A, B) \|F (z)\| \leq y \land z \in (A, B)) \to \|F (z)\| \leq y$
93	90 91 92	syl2anc	$⊢ ((φ \land \forall z \in (A, B) \|F (z)\| \leq y) \land z \in dom (x \in (A, B) ⟼ F (x) \sin R x)) \to \|F (z)\| \leq y$
94	93	adantllr	$⊢ (((φ \land y \in ℝ) \land \forall z \in (A, B) \|F (z)\| \leq y) \land z \in dom (x \in (A, B) ⟼ F (x) \sin R x)) \to \|F (z)\| \leq y$
95		eqidd	$⊢ (φ \land z \in (A, B)) \to (x \in (A, B) ⟼ F (x) \sin R x) = (x \in (A, B) ⟼ F (x) \sin R x)$
96		fveq2	$⊢ x = z \to F (x) = F (z)$
97		oveq2	$⊢ x = z \to R x = R z$
98	97	fveq2d	$⊢ x = z \to \sin R x = \sin R z$
99	96 98	oveq12d	$⊢ x = z \to F (x) \sin R x = F (z) \sin R z$
100	99	adantl	$⊢ ((φ \land z \in (A, B)) \land x = z) \to F (x) \sin R x = F (z) \sin R z$
101		simpr	$⊢ (φ \land z \in (A, B)) \to z \in (A, B)$
102	10	adantr	$⊢ (φ \land z \in (A, B)) \to F : [A, B] ⟶ ℂ$
103	54 101	sselid	$⊢ (φ \land z \in (A, B)) \to z \in [A, B]$
104	102 103	ffvelcdmd	$⊢ (φ \land z \in (A, B)) \to F (z) \in ℂ$
105	20	adantr	$⊢ (φ \land z \in (A, B)) \to R \in ℂ$
106	41 101	sselid	$⊢ (φ \land z \in (A, B)) \to z \in ℂ$
107	105 106	mulcld	$⊢ (φ \land z \in (A, B)) \to R z \in ℂ$
108	107	sincld	$⊢ (φ \land z \in (A, B)) \to \sin R z \in ℂ$
109	104 108	mulcld	$⊢ (φ \land z \in (A, B)) \to F (z) \sin R z \in ℂ$
110	95 100 101 109	fvmptd	$⊢ (φ \land z \in (A, B)) \to (x \in (A, B) ⟼ F (x) \sin R x) (z) = F (z) \sin R z$
111	110	fveq2d	$⊢ (φ \land z \in (A, B)) \to \|(x \in (A, B) ⟼ F (x) \sin R x) (z)\| = \|F (z) \sin R z\|$
112	104 108	absmuld	$⊢ (φ \land z \in (A, B)) \to \|F (z) \sin R z\| = \|F (z)\| \|\sin R z\|$
113	111 112	eqtrd	$⊢ (φ \land z \in (A, B)) \to \|(x \in (A, B) ⟼ F (x) \sin R x) (z)\| = \|F (z)\| \|\sin R z\|$
114	113	adantlr	$⊢ ((φ \land y \in ℝ) \land z \in (A, B)) \to \|(x \in (A, B) ⟼ F (x) \sin R x) (z)\| = \|F (z)\| \|\sin R z\|$
115	114	adantr	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to \|(x \in (A, B) ⟼ F (x) \sin R x) (z)\| = \|F (z)\| \|\sin R z\|$
116		simplll	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to φ$
117		simplr	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to z \in (A, B)$
118	116 117 104	syl2anc	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to F (z) \in ℂ$
119	118	abscld	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to \|F (z)\| \in ℝ$
120	20	ad3antrrr	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to R \in ℂ$
121	41 117	sselid	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to z \in ℂ$
122	120 121	mulcld	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to R z \in ℂ$
123	122	sincld	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to \sin R z \in ℂ$
124	123	abscld	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to \|\sin R z\| \in ℝ$
125	119 124	remulcld	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to \|F (z)\| \|\sin R z\| \in ℝ$
126		1red	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to 1 \in ℝ$
127	119 126	remulcld	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to \|F (z)\| \cdot 1 \in ℝ$
128		simpllr	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to y \in ℝ$
129	128 126	remulcld	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to y \cdot 1 \in ℝ$
130	108	abscld	$⊢ (φ \land z \in (A, B)) \to \|\sin R z\| \in ℝ$
131		1red	$⊢ (φ \land z \in (A, B)) \to 1 \in ℝ$
132	104	abscld	$⊢ (φ \land z \in (A, B)) \to \|F (z)\| \in ℝ$
133	104	absge0d	$⊢ (φ \land z \in (A, B)) \to 0 \leq \|F (z)\|$
134	19	adantr	$⊢ (φ \land z \in (A, B)) \to R \in ℝ$
135		elioore	$⊢ z \in (A, B) \to z \in ℝ$
136	135	adantl	$⊢ (φ \land z \in (A, B)) \to z \in ℝ$
137	134 136	remulcld	$⊢ (φ \land z \in (A, B)) \to R z \in ℝ$
138		abssinbd	$⊢ R z \in ℝ \to \|\sin R z\| \leq 1$
139	137 138	syl	$⊢ (φ \land z \in (A, B)) \to \|\sin R z\| \leq 1$
140	130 131 132 133 139	lemul2ad	$⊢ (φ \land z \in (A, B)) \to \|F (z)\| \|\sin R z\| \leq \|F (z)\| \cdot 1$
141	140	adantlr	$⊢ ((φ \land y \in ℝ) \land z \in (A, B)) \to \|F (z)\| \|\sin R z\| \leq \|F (z)\| \cdot 1$
142	141	adantr	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to \|F (z)\| \|\sin R z\| \leq \|F (z)\| \cdot 1$
143		0le1	$⊢ 0 \leq 1$
144	143	a1i	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to 0 \leq 1$
145		simpr	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to \|F (z)\| \leq y$
146	119 128 126 144 145	lemul1ad	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to \|F (z)\| \cdot 1 \leq y \cdot 1$
147	125 127 129 142 146	letrd	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to \|F (z)\| \|\sin R z\| \leq y \cdot 1$
148	115 147	eqbrtrd	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to \|(x \in (A, B) ⟼ F (x) \sin R x) (z)\| \leq y \cdot 1$
149	128	recnd	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to y \in ℂ$
150	149	mulridd	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to y \cdot 1 = y$
151	148 150	breqtrd	$⊢ (((φ \land y \in ℝ) \land z \in (A, B)) \land \|F (z)\| \leq y) \to \|(x \in (A, B) ⟼ F (x) \sin R x) (z)\| \leq y$
152	75 89 94 151	syl21anc	$⊢ (((φ \land y \in ℝ) \land \forall z \in (A, B) \|F (z)\| \leq y) \land z \in dom (x \in (A, B) ⟼ F (x) \sin R x)) \to \|(x \in (A, B) ⟼ F (x) \sin R x) (z)\| \leq y$
153	152	ex	$⊢ ((φ \land y \in ℝ) \land \forall z \in (A, B) \|F (z)\| \leq y) \to (z \in dom (x \in (A, B) ⟼ F (x) \sin R x) \to \|(x \in (A, B) ⟼ F (x) \sin R x) (z)\| \leq y)$
154	74 153	ralrimi	$⊢ ((φ \land y \in ℝ) \land \forall z \in (A, B) \|F (z)\| \leq y) \to \forall z \in dom (x \in (A, B) ⟼ F (x) \sin R x) \|(x \in (A, B) ⟼ F (x) \sin R x) (z)\| \leq y$
155	154	ex	$⊢ (φ \land y \in ℝ) \to (\forall z \in (A, B) \|F (z)\| \leq y \to \forall z \in dom (x \in (A, B) ⟼ F (x) \sin R x) \|(x \in (A, B) ⟼ F (x) \sin R x) (z)\| \leq y)$
156	155	reximdva	$⊢ φ \to (\exists y \in ℝ \forall z \in (A, B) \|F (z)\| \leq y \to \exists y \in ℝ \forall z \in dom (x \in (A, B) ⟼ F (x) \sin R x) \|(x \in (A, B) ⟼ F (x) \sin R x) (z)\| \leq y)$
157	71 156	mpd	$⊢ φ \to \exists y \in ℝ \forall z \in dom (x \in (A, B) ⟼ F (x) \sin R x) \|(x \in (A, B) ⟼ F (x) \sin R x) (z)\| \leq y$
158	48 52 60 157	cnbdibl	$⊢ φ \to (x \in (A, B) ⟼ F (x) \sin R x) \in 𝐿^{1}$
159	15 45	cncfmpt1f	$⊢ φ \to (x \in (A, B) ⟼ \cos R x) : (A, B) \underset{cn}{⟶} ℂ$
160	42 29 30	constcncfg	$⊢ φ \to (x \in (A, B) ⟼ R) : (A, B) \underset{cn}{⟶} (ℂ ∖ \{0\})$
161	159 160	divcncf	$⊢ φ \to (x \in (A, B) ⟼ \frac{\cos R x}{R}) : (A, B) \underset{cn}{⟶} ℂ$
162	161	negcncfg	$⊢ φ \to (x \in (A, B) ⟼ - \frac{\cos R x}{R}) : (A, B) \underset{cn}{⟶} ℂ$
163	38 162	mulcncf	$⊢ φ \to (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) : (A, B) \underset{cn}{⟶} ℂ$
164		simpr	$⊢ (φ \land y \in ℝ) \to y \in ℝ$
165	19	adantr	$⊢ (φ \land y \in ℝ) \to R \in ℝ$
166	8	rpne0d	$⊢ φ \to R \neq 0$
167	166	adantr	$⊢ (φ \land y \in ℝ) \to R \neq 0$
168	164 165 167	redivcld	$⊢ (φ \land y \in ℝ) \to \frac{y}{R} \in ℝ$
169	168	adantr	$⊢ ((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \to \frac{y}{R} \in ℝ$
170		simpr	$⊢ (φ \land z \in dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R}))) \to z \in dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R}))$
171	35	ffvelcdmda	$⊢ (φ \land x \in (A, B)) \to G (x) \in ℂ$
172	20	adantr	$⊢ (φ \land x \in (A, B)) \to R \in ℂ$
173	78	recnd	$⊢ x \in (A, B) \to x \in ℂ$
174	173	adantl	$⊢ (φ \land x \in (A, B)) \to x \in ℂ$
175	172 174	mulcld	$⊢ (φ \land x \in (A, B)) \to R x \in ℂ$
176	175	coscld	$⊢ (φ \land x \in (A, B)) \to \cos R x \in ℂ$
177	166	adantr	$⊢ (φ \land x \in (A, B)) \to R \neq 0$
178	176 172 177	divcld	$⊢ (φ \land x \in (A, B)) \to \frac{\cos R x}{R} \in ℂ$
179	178	negcld	$⊢ (φ \land x \in (A, B)) \to - \frac{\cos R x}{R} \in ℂ$
180	171 179	mulcld	$⊢ (φ \land x \in (A, B)) \to G (x) (- \frac{\cos R x}{R}) \in ℂ$
181	180	ralrimiva	$⊢ φ \to \forall x \in (A, B) G (x) (- \frac{\cos R x}{R}) \in ℂ$
182	181	adantr	$⊢ (φ \land z \in dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R}))) \to \forall x \in (A, B) G (x) (- \frac{\cos R x}{R}) \in ℂ$
183		dmmptg	$⊢ \forall x \in (A, B) G (x) (- \frac{\cos R x}{R}) \in ℂ \to dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) = (A, B)$
184	182 183	syl	$⊢ (φ \land z \in dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R}))) \to dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) = (A, B)$
185	170 184	eleqtrd	$⊢ (φ \land z \in dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R}))) \to z \in (A, B)$
186	185	ad4ant14	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R}))) \to z \in (A, B)$
187		eqidd	$⊢ (φ \land z \in (A, B)) \to (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) = (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R}))$
188		fveq2	$⊢ x = z \to G (x) = G (z)$
189	97	fveq2d	$⊢ x = z \to \cos R x = \cos R z$
190	189	oveq1d	$⊢ x = z \to \frac{\cos R x}{R} = \frac{\cos R z}{R}$
191	190	negeqd	$⊢ x = z \to - \frac{\cos R x}{R} = - \frac{\cos R z}{R}$
192	188 191	oveq12d	$⊢ x = z \to G (x) (- \frac{\cos R x}{R}) = G (z) (- \frac{\cos R z}{R})$
193	192	adantl	$⊢ ((φ \land z \in (A, B)) \land x = z) \to G (x) (- \frac{\cos R x}{R}) = G (z) (- \frac{\cos R z}{R})$
194	35	ffvelcdmda	$⊢ (φ \land z \in (A, B)) \to G (z) \in ℂ$
195	107	coscld	$⊢ (φ \land z \in (A, B)) \to \cos R z \in ℂ$
196	166	adantr	$⊢ (φ \land z \in (A, B)) \to R \neq 0$
197	195 105 196	divcld	$⊢ (φ \land z \in (A, B)) \to \frac{\cos R z}{R} \in ℂ$
198	197	negcld	$⊢ (φ \land z \in (A, B)) \to - \frac{\cos R z}{R} \in ℂ$
199	194 198	mulcld	$⊢ (φ \land z \in (A, B)) \to G (z) (- \frac{\cos R z}{R}) \in ℂ$
200	187 193 101 199	fvmptd	$⊢ (φ \land z \in (A, B)) \to (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) (z) = G (z) (- \frac{\cos R z}{R})$
201	200	fveq2d	$⊢ (φ \land z \in (A, B)) \to \|(x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) (z)\| = \|G (z) (- \frac{\cos R z}{R})\|$
202	201	ad4ant14	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to \|(x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) (z)\| = \|G (z) (- \frac{\cos R z}{R})\|$
203	35	ad2antrr	$⊢ ((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \to G : (A, B) ⟶ ℂ$
204	203	ffvelcdmda	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to G (z) \in ℂ$
205	204	abscld	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to \|G (z)\| \in ℝ$
206		simpllr	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to y \in ℝ$
207	20	ad3antrrr	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to R \in ℂ$
208	106	ad4ant14	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to z \in ℂ$
209	207 208	mulcld	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to R z \in ℂ$
210	209	coscld	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to \cos R z \in ℂ$
211	166	ad3antrrr	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to R \neq 0$
212	210 207 211	divcld	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to \frac{\cos R z}{R} \in ℂ$
213	212	negcld	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to - \frac{\cos R z}{R} \in ℂ$
214	213	abscld	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to \|- \frac{\cos R z}{R}\| \in ℝ$
215	8	rprecred	$⊢ φ \to \frac{1}{R} \in ℝ$
216	215	ad3antrrr	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to \frac{1}{R} \in ℝ$
217	204	absge0d	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to 0 \leq \|G (z)\|$
218	213	absge0d	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to 0 \leq \|- \frac{\cos R z}{R}\|$
219	188	fveq2d	$⊢ x = z \to \|G (x)\| = \|G (z)\|$
220	219	breq1d	$⊢ x = z \to (\|G (x)\| \leq y \leftrightarrow \|G (z)\| \leq y)$
221	220	rspccva	$⊢ (\forall x \in (A, B) \|G (x)\| \leq y \land z \in (A, B)) \to \|G (z)\| \leq y$
222	221	adantll	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to \|G (z)\| \leq y$
223	197	absnegd	$⊢ (φ \land z \in (A, B)) \to \|- \frac{\cos R z}{R}\| = \|\frac{\cos R z}{R}\|$
224	195 105 196	absdivd	$⊢ (φ \land z \in (A, B)) \to \|\frac{\cos R z}{R}\| = \frac{\|\cos R z\|}{\|R\|}$
225	8	rpge0d	$⊢ φ \to 0 \leq R$
226	19 225	absidd	$⊢ φ \to \|R\| = R$
227	226	oveq2d	$⊢ φ \to \frac{\|\cos R z\|}{\|R\|} = \frac{\|\cos R z\|}{R}$
228	227	adantr	$⊢ (φ \land z \in (A, B)) \to \frac{\|\cos R z\|}{\|R\|} = \frac{\|\cos R z\|}{R}$
229	223 224 228	3eqtrd	$⊢ (φ \land z \in (A, B)) \to \|- \frac{\cos R z}{R}\| = \frac{\|\cos R z\|}{R}$
230	195	abscld	$⊢ (φ \land z \in (A, B)) \to \|\cos R z\| \in ℝ$
231	8	adantr	$⊢ (φ \land z \in (A, B)) \to R \in ℝ^{+}$
232		abscosbd	$⊢ R z \in ℝ \to \|\cos R z\| \leq 1$
233	137 232	syl	$⊢ (φ \land z \in (A, B)) \to \|\cos R z\| \leq 1$
234	230 131 231 233	lediv1dd	$⊢ (φ \land z \in (A, B)) \to \frac{\|\cos R z\|}{R} \leq \frac{1}{R}$
235	229 234	eqbrtrd	$⊢ (φ \land z \in (A, B)) \to \|- \frac{\cos R z}{R}\| \leq \frac{1}{R}$
236	235	ad4ant14	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to \|- \frac{\cos R z}{R}\| \leq \frac{1}{R}$
237	205 206 214 216 217 218 222 236	lemul12ad	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to \|G (z)\| \|- \frac{\cos R z}{R}\| \leq y (\frac{1}{R})$
238	194 198	absmuld	$⊢ (φ \land z \in (A, B)) \to \|G (z) (- \frac{\cos R z}{R})\| = \|G (z)\| \|- \frac{\cos R z}{R}\|$
239	238	ad4ant14	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to \|G (z) (- \frac{\cos R z}{R})\| = \|G (z)\| \|- \frac{\cos R z}{R}\|$
240	206	recnd	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to y \in ℂ$
241	240 207 211	divrecd	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to \frac{y}{R} = y (\frac{1}{R})$
242	237 239 241	3brtr4d	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to \|G (z) (- \frac{\cos R z}{R})\| \leq \frac{y}{R}$
243	202 242	eqbrtrd	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in (A, B)) \to \|(x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) (z)\| \leq \frac{y}{R}$
244	186 243	syldan	$⊢ (((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \land z \in dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R}))) \to \|(x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) (z)\| \leq \frac{y}{R}$
245	244	ralrimiva	$⊢ ((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \to \forall z \in dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) \|(x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) (z)\| \leq \frac{y}{R}$
246		breq2	$⊢ w = \frac{y}{R} \to (\|(x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) (z)\| \leq w \leftrightarrow \|(x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) (z)\| \leq \frac{y}{R})$
247	246	ralbidv	$⊢ w = \frac{y}{R} \to (\forall z \in dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) \|(x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) (z)\| \leq w \leftrightarrow \forall z \in dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) \|(x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) (z)\| \leq \frac{y}{R})$
248	247	rspcev	$⊢ (\frac{y}{R} \in ℝ \land \forall z \in dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) \|(x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) (z)\| \leq \frac{y}{R}) \to \exists w \in ℝ \forall z \in dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) \|(x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) (z)\| \leq w$
249	169 245 248	syl2anc	$⊢ ((φ \land y \in ℝ) \land \forall x \in (A, B) \|G (x)\| \leq y) \to \exists w \in ℝ \forall z \in dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) \|(x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) (z)\| \leq w$
250	249 7	r19.29a	$⊢ φ \to \exists w \in ℝ \forall z \in dom (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) \|(x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) (z)\| \leq w$
251	48 52 163 250	cnbdibl	$⊢ φ \to (x \in (A, B) ⟼ G (x) (- \frac{\cos R x}{R})) \in 𝐿^{1}$
252	12	oveq2d	$⊢ φ \to \frac{d (x \in [A, B]⟼ F (x))}{d_{ℝ} x} = ℝ D F$
253	5	eqcomi	$⊢ ℝ D F = G$
254	253	a1i	$⊢ φ \to ℝ D F = G$
255	252 254 36	3eqtrd	$⊢ φ \to \frac{d (x \in [A, B]⟼ F (x))}{d_{ℝ} x} = (x \in (A, B) ⟼ G (x))$
256		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
257	256	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
258	20	adantr	$⊢ (φ \land x \in ℝ) \to R \in ℂ$
259		recn	$⊢ x \in ℝ \to x \in ℂ$
260	259	adantl	$⊢ (φ \land x \in ℝ) \to x \in ℂ$
261	258 260	mulcld	$⊢ (φ \land x \in ℝ) \to R x \in ℂ$
262	261	coscld	$⊢ (φ \land x \in ℝ) \to \cos R x \in ℂ$
263	166	adantr	$⊢ (φ \land x \in ℝ) \to R \neq 0$
264	262 258 263	divcld	$⊢ (φ \land x \in ℝ) \to \frac{\cos R x}{R} \in ℂ$
265	264	negcld	$⊢ (φ \land x \in ℝ) \to - \frac{\cos R x}{R} \in ℂ$
266	19	adantr	$⊢ (φ \land x \in ℝ) \to R \in ℝ$
267		simpr	$⊢ (φ \land x \in ℝ) \to x \in ℝ$
268	266 267	remulcld	$⊢ (φ \land x \in ℝ) \to R x \in ℝ$
269	268	resincld	$⊢ (φ \land x \in ℝ) \to \sin R x \in ℝ$
270	269	renegcld	$⊢ (φ \land x \in ℝ) \to - \sin R x \in ℝ$
271	270 266	remulcld	$⊢ (φ \land x \in ℝ) \to (- \sin R x) R \in ℝ$
272	271 266 263	redivcld	$⊢ (φ \land x \in ℝ) \to \frac{(- \sin R x) R}{R} \in ℝ$
273	272	renegcld	$⊢ (φ \land x \in ℝ) \to - \frac{(- \sin R x) R}{R} \in ℝ$
274		recoscl	$⊢ y \in ℝ \to \cos y \in ℝ$
275	274	adantl	$⊢ (φ \land y \in ℝ) \to \cos y \in ℝ$
276	275	recnd	$⊢ (φ \land y \in ℝ) \to \cos y \in ℂ$
277		resincl	$⊢ y \in ℝ \to \sin y \in ℝ$
278	277	renegcld	$⊢ y \in ℝ \to - \sin y \in ℝ$
279	278	adantl	$⊢ (φ \land y \in ℝ) \to - \sin y \in ℝ$
280		1red	$⊢ (φ \land x \in ℝ) \to 1 \in ℝ$
281	257	dvmptid	$⊢ φ \to \frac{d (x \in ℝ⟼ x)}{d_{ℝ} x} = (x \in ℝ ⟼ 1)$
282	257 260 280 281 20	dvmptcmul	$⊢ φ \to \frac{d (x \in ℝ⟼ R x)}{d_{ℝ} x} = (x \in ℝ ⟼ R \cdot 1)$
283	258	mulridd	$⊢ (φ \land x \in ℝ) \to R \cdot 1 = R$
284	283	mpteq2dva	$⊢ φ \to (x \in ℝ ⟼ R \cdot 1) = (x \in ℝ ⟼ R)$
285	282 284	eqtrd	$⊢ φ \to \frac{d (x \in ℝ⟼ R x)}{d_{ℝ} x} = (x \in ℝ ⟼ R)$
286		dvcosre	$⊢ \frac{d (y \in ℝ⟼ \cos y)}{d_{ℝ} y} = (y \in ℝ ⟼ - \sin y)$
287	286	a1i	$⊢ φ \to \frac{d (y \in ℝ⟼ \cos y)}{d_{ℝ} y} = (y \in ℝ ⟼ - \sin y)$
288		fveq2	$⊢ y = R x \to \cos y = \cos R x$
289		fveq2	$⊢ y = R x \to \sin y = \sin R x$
290	289	negeqd	$⊢ y = R x \to - \sin y = - \sin R x$
291	257 257 268 266 276 279 285 287 288 290	dvmptco	$⊢ φ \to \frac{d (x \in ℝ⟼ \cos R x)}{d_{ℝ} x} = (x \in ℝ ⟼ (- \sin R x) R)$
292	257 262 271 291 20 166	dvmptdivc	$⊢ φ \to \frac{d (x \in ℝ⟼ \frac{\cos R x}{R})}{d_{ℝ} x} = (x \in ℝ ⟼ \frac{(- \sin R x) R}{R})$
293	257 264 272 292	dvmptneg	$⊢ φ \to \frac{d (x \in ℝ⟼ - \frac{\cos R x}{R})}{d_{ℝ} x} = (x \in ℝ ⟼ - \frac{(- \sin R x) R}{R})$
294		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
295	294	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
296		iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
297	1 2 296	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([A, B]) = (A, B)$
298	257 265 273 293 16 295 294 297	dvmptres2	$⊢ φ \to \frac{d (x \in [A, B]⟼ - \frac{\cos R x}{R})}{d_{ℝ} x} = (x \in (A, B) ⟼ - \frac{(- \sin R x) R}{R})$
299	82 172	mulneg1d	$⊢ (φ \land x \in (A, B)) \to (- \sin R x) R = - \sin R x R$
300	299	oveq1d	$⊢ (φ \land x \in (A, B)) \to \frac{(- \sin R x) R}{R} = \frac{- \sin R x R}{R}$
301	82 172	mulcld	$⊢ (φ \land x \in (A, B)) \to \sin R x R \in ℂ$
302	301 172 177	divnegd	$⊢ (φ \land x \in (A, B)) \to - \frac{\sin R x R}{R} = \frac{- \sin R x R}{R}$
303	300 302	eqtr4d	$⊢ (φ \land x \in (A, B)) \to \frac{(- \sin R x) R}{R} = - \frac{\sin R x R}{R}$
304	303	negeqd	$⊢ (φ \land x \in (A, B)) \to - \frac{(- \sin R x) R}{R} = - (- \frac{\sin R x R}{R})$
305	301 172 177	divcld	$⊢ (φ \land x \in (A, B)) \to \frac{\sin R x R}{R} \in ℂ$
306	305	negnegd	$⊢ (φ \land x \in (A, B)) \to - (- \frac{\sin R x R}{R}) = \frac{\sin R x R}{R}$
307	82 172 177	divcan4d	$⊢ (φ \land x \in (A, B)) \to \frac{\sin R x R}{R} = \sin R x$
308	304 306 307	3eqtrd	$⊢ (φ \land x \in (A, B)) \to - \frac{(- \sin R x) R}{R} = \sin R x$
309	308	mpteq2dva	$⊢ φ \to (x \in (A, B) ⟼ - \frac{(- \sin R x) R}{R}) = (x \in (A, B) ⟼ \sin R x)$
310	298 309	eqtrd	$⊢ φ \to \frac{d (x \in [A, B]⟼ - \frac{\cos R x}{R})}{d_{ℝ} x} = (x \in (A, B) ⟼ \sin R x)$
311		fveq2	$⊢ x = A \to F (x) = F (A)$
312		oveq2	$⊢ x = A \to R x = R A$
313	312	fveq2d	$⊢ x = A \to \cos R x = \cos R A$
314	313	oveq1d	$⊢ x = A \to \frac{\cos R x}{R} = \frac{\cos R A}{R}$
315	314	negeqd	$⊢ x = A \to - \frac{\cos R x}{R} = - \frac{\cos R A}{R}$
316	311 315	oveq12d	$⊢ x = A \to F (x) (- \frac{\cos R x}{R}) = F (A) (- \frac{\cos R A}{R})$
317	316	adantl	$⊢ (φ \land x = A) \to F (x) (- \frac{\cos R x}{R}) = F (A) (- \frac{\cos R A}{R})$
318		fveq2	$⊢ x = B \to F (x) = F (B)$
319		oveq2	$⊢ x = B \to R x = R B$
320	319	fveq2d	$⊢ x = B \to \cos R x = \cos R B$
321	320	oveq1d	$⊢ x = B \to \frac{\cos R x}{R} = \frac{\cos R B}{R}$
322	321	negeqd	$⊢ x = B \to - \frac{\cos R x}{R} = - \frac{\cos R B}{R}$
323	318 322	oveq12d	$⊢ x = B \to F (x) (- \frac{\cos R x}{R}) = F (B) (- \frac{\cos R B}{R})$
324	323	adantl	$⊢ (φ \land x = B) \to F (x) (- \frac{\cos R x}{R}) = F (B) (- \frac{\cos R B}{R})$
325	1 2 3 13 33 38 46 158 251 255 310 317 324	itgparts	$⊢ φ \to \int_{(A, B)} F (x) \sin R x d x = F (B) (- \frac{\cos R B}{R}) - F (A) (- \frac{\cos R A}{R}) - \int_{(A, B)} G (x) (- \frac{\cos R x}{R}) d x$

Metamath Proof Explorer

Theorem fourierdlem39

Proof