itgcoscmulx

Description: Exercise: the integral of x |-> cos a x on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	itgcoscmulx.a	$⊢ φ \to A \in ℂ$
	itgcoscmulx.b	$⊢ φ \to B \in ℝ$
	itgcoscmulx.c	$⊢ φ \to C \in ℝ$
	itgcoscmulx.blec	$⊢ φ \to B \leq C$
	itgcoscmulx.an0	$⊢ φ \to A \neq 0$
Assertion	itgcoscmulx	$⊢ φ \to \int_{(B, C)} \cos A x d x = \frac{\sin A C - \sin A B}{A}$

Proof

Step	Hyp	Ref	Expression
1		itgcoscmulx.a	$⊢ φ \to A \in ℂ$
2		itgcoscmulx.b	$⊢ φ \to B \in ℝ$
3		itgcoscmulx.c	$⊢ φ \to C \in ℝ$
4		itgcoscmulx.blec	$⊢ φ \to B \leq C$
5		itgcoscmulx.an0	$⊢ φ \to A \neq 0$
6	2 3	iccssred	$⊢ φ \to [B, C] \subseteq ℝ$
7	6	resmptd	$⊢ φ \to {(y \in ℝ ⟼ \frac{\sin A y}{A}) ↾}_{[B, C]} = (y \in [B, C] ⟼ \frac{\sin A y}{A})$
8	7	eqcomd	$⊢ φ \to (y \in [B, C] ⟼ \frac{\sin A y}{A}) = {(y \in ℝ ⟼ \frac{\sin A y}{A}) ↾}_{[B, C]}$
9	8	oveq2d	$⊢ φ \to \frac{d (y \in [B, C]⟼ \frac{\sin A y}{A})}{d_{ℝ} y} = ℝ D ({(y \in ℝ ⟼ \frac{\sin A y}{A}) ↾}_{[B, C]})$
10		ax-resscn	$⊢ ℝ \subseteq ℂ$
11	10	a1i	$⊢ φ \to ℝ \subseteq ℂ$
12	11	sselda	$⊢ (φ \land y \in ℝ) \to y \in ℂ$
13	1	adantr	$⊢ (φ \land y \in ℂ) \to A \in ℂ$
14		simpr	$⊢ (φ \land y \in ℂ) \to y \in ℂ$
15	13 14	mulcld	$⊢ (φ \land y \in ℂ) \to A y \in ℂ$
16	15	sincld	$⊢ (φ \land y \in ℂ) \to \sin A y \in ℂ$
17	5	adantr	$⊢ (φ \land y \in ℂ) \to A \neq 0$
18	16 13 17	divcld	$⊢ (φ \land y \in ℂ) \to \frac{\sin A y}{A} \in ℂ$
19	12 18	syldan	$⊢ (φ \land y \in ℝ) \to \frac{\sin A y}{A} \in ℂ$
20	19	fmpttd	$⊢ φ \to (y \in ℝ ⟼ \frac{\sin A y}{A}) : ℝ ⟶ ℂ$
21		ssidd	$⊢ φ \to ℝ \subseteq ℝ$
22		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
23		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
24	22 23	dvres	$⊢ ((ℝ \subseteq ℂ \land (y \in ℝ ⟼ \frac{\sin A y}{A}) : ℝ ⟶ ℂ) \land (ℝ \subseteq ℝ \land [B, C] \subseteq ℝ)) \to ℝ D ({(y \in ℝ ⟼ \frac{\sin A y}{A}) ↾}_{[B, C]}) = {\frac{d (y \in ℝ⟼ \frac{\sin A y}{A})}{d_{ℝ} y} ↾}_{int (topGen (ran (.))) ([B, C])}$
25	11 20 21 6 24	syl22anc	$⊢ φ \to ℝ D ({(y \in ℝ ⟼ \frac{\sin A y}{A}) ↾}_{[B, C]}) = {\frac{d (y \in ℝ⟼ \frac{\sin A y}{A})}{d_{ℝ} y} ↾}_{int (topGen (ran (.))) ([B, C])}$
26		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
27	26	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
28	12 16	syldan	$⊢ (φ \land y \in ℝ) \to \sin A y \in ℂ$
29	1	adantr	$⊢ (φ \land y \in ℝ) \to A \in ℂ$
30	29 12	mulcld	$⊢ (φ \land y \in ℝ) \to A y \in ℂ$
31	30	coscld	$⊢ (φ \land y \in ℝ) \to \cos A y \in ℂ$
32	29 31	mulcld	$⊢ (φ \land y \in ℝ) \to A \cos A y \in ℂ$
33	11	resmptd	$⊢ φ \to {(y \in ℂ ⟼ \sin A y) ↾}_{ℝ} = (y \in ℝ ⟼ \sin A y)$
34	33	eqcomd	$⊢ φ \to (y \in ℝ ⟼ \sin A y) = {(y \in ℂ ⟼ \sin A y) ↾}_{ℝ}$
35	34	oveq2d	$⊢ φ \to \frac{d (y \in ℝ⟼ \sin A y)}{d_{ℝ} y} = ℝ D ({(y \in ℂ ⟼ \sin A y) ↾}_{ℝ})$
36	16	fmpttd	$⊢ φ \to (y \in ℂ ⟼ \sin A y) : ℂ ⟶ ℂ$
37		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
38		dvsinax	$⊢ A \in ℂ \to \frac{d (y \in ℂ⟼ \sin A y)}{d_{ℂ} y} = (y \in ℂ ⟼ A \cos A y)$
39	1 38	syl	$⊢ φ \to \frac{d (y \in ℂ⟼ \sin A y)}{d_{ℂ} y} = (y \in ℂ ⟼ A \cos A y)$
40	39	dmeqd	$⊢ φ \to dom \frac{d (y \in ℂ⟼ \sin A y)}{d_{ℂ} y} = dom (y \in ℂ ⟼ A \cos A y)$
41	15	coscld	$⊢ (φ \land y \in ℂ) \to \cos A y \in ℂ$
42	13 41	mulcld	$⊢ (φ \land y \in ℂ) \to A \cos A y \in ℂ$
43	42	ralrimiva	$⊢ φ \to \forall y \in ℂ A \cos A y \in ℂ$
44		dmmptg	$⊢ \forall y \in ℂ A \cos A y \in ℂ \to dom (y \in ℂ ⟼ A \cos A y) = ℂ$
45	43 44	syl	$⊢ φ \to dom (y \in ℂ ⟼ A \cos A y) = ℂ$
46	40 45	eqtr2d	$⊢ φ \to ℂ = dom \frac{d (y \in ℂ⟼ \sin A y)}{d_{ℂ} y}$
47	10 46	sseqtrid	$⊢ φ \to ℝ \subseteq dom \frac{d (y \in ℂ⟼ \sin A y)}{d_{ℂ} y}$
48		dvres3	$⊢ ((ℝ \in \{ℝ, ℂ\} \land (y \in ℂ ⟼ \sin A y) : ℂ ⟶ ℂ) \land (ℂ \subseteq ℂ \land ℝ \subseteq dom \frac{d (y \in ℂ⟼ \sin A y)}{d_{ℂ} y})) \to ℝ D ({(y \in ℂ ⟼ \sin A y) ↾}_{ℝ}) = {\frac{d (y \in ℂ⟼ \sin A y)}{d_{ℂ} y} ↾}_{ℝ}$
49	27 36 37 47 48	syl22anc	$⊢ φ \to ℝ D ({(y \in ℂ ⟼ \sin A y) ↾}_{ℝ}) = {\frac{d (y \in ℂ⟼ \sin A y)}{d_{ℂ} y} ↾}_{ℝ}$
50	39	reseq1d	$⊢ φ \to {\frac{d (y \in ℂ⟼ \sin A y)}{d_{ℂ} y} ↾}_{ℝ} = {(y \in ℂ ⟼ A \cos A y) ↾}_{ℝ}$
51	11	resmptd	$⊢ φ \to {(y \in ℂ ⟼ A \cos A y) ↾}_{ℝ} = (y \in ℝ ⟼ A \cos A y)$
52	49 50 51	3eqtrd	$⊢ φ \to ℝ D ({(y \in ℂ ⟼ \sin A y) ↾}_{ℝ}) = (y \in ℝ ⟼ A \cos A y)$
53	35 52	eqtrd	$⊢ φ \to \frac{d (y \in ℝ⟼ \sin A y)}{d_{ℝ} y} = (y \in ℝ ⟼ A \cos A y)$
54	27 28 32 53 1 5	dvmptdivc	$⊢ φ \to \frac{d (y \in ℝ⟼ \frac{\sin A y}{A})}{d_{ℝ} y} = (y \in ℝ ⟼ \frac{A \cos A y}{A})$
55		iccntr	$⊢ (B \in ℝ \land C \in ℝ) \to int (topGen (ran (.))) ([B, C]) = (B, C)$
56	2 3 55	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([B, C]) = (B, C)$
57	54 56	reseq12d	$⊢ φ \to {\frac{d (y \in ℝ⟼ \frac{\sin A y}{A})}{d_{ℝ} y} ↾}_{int (topGen (ran (.))) ([B, C])} = {(y \in ℝ ⟼ \frac{A \cos A y}{A}) ↾}_{(B, C)}$
58		ioossre	$⊢ (B, C) \subseteq ℝ$
59		resmpt	$⊢ (B, C) \subseteq ℝ \to {(y \in ℝ ⟼ \frac{A \cos A y}{A}) ↾}_{(B, C)} = (y \in (B, C) ⟼ \frac{A \cos A y}{A})$
60	58 59	mp1i	$⊢ φ \to {(y \in ℝ ⟼ \frac{A \cos A y}{A}) ↾}_{(B, C)} = (y \in (B, C) ⟼ \frac{A \cos A y}{A})$
61		elioore	$⊢ y \in (B, C) \to y \in ℝ$
62	61	recnd	$⊢ y \in (B, C) \to y \in ℂ$
63	62 41	sylan2	$⊢ (φ \land y \in (B, C)) \to \cos A y \in ℂ$
64	1	adantr	$⊢ (φ \land y \in (B, C)) \to A \in ℂ$
65	5	adantr	$⊢ (φ \land y \in (B, C)) \to A \neq 0$
66	63 64 65	divcan3d	$⊢ (φ \land y \in (B, C)) \to \frac{A \cos A y}{A} = \cos A y$
67	66	mpteq2dva	$⊢ φ \to (y \in (B, C) ⟼ \frac{A \cos A y}{A}) = (y \in (B, C) ⟼ \cos A y)$
68	57 60 67	3eqtrd	$⊢ φ \to {\frac{d (y \in ℝ⟼ \frac{\sin A y}{A})}{d_{ℝ} y} ↾}_{int (topGen (ran (.))) ([B, C])} = (y \in (B, C) ⟼ \cos A y)$
69	9 25 68	3eqtrd	$⊢ φ \to \frac{d (y \in [B, C]⟼ \frac{\sin A y}{A})}{d_{ℝ} y} = (y \in (B, C) ⟼ \cos A y)$
70	69	adantr	$⊢ (φ \land x \in (B, C)) \to \frac{d (y \in [B, C]⟼ \frac{\sin A y}{A})}{d_{ℝ} y} = (y \in (B, C) ⟼ \cos A y)$
71		oveq2	$⊢ y = x \to A y = A x$
72	71	fveq2d	$⊢ y = x \to \cos A y = \cos A x$
73	72	adantl	$⊢ ((φ \land x \in (B, C)) \land y = x) \to \cos A y = \cos A x$
74		simpr	$⊢ (φ \land x \in (B, C)) \to x \in (B, C)$
75	1	adantr	$⊢ (φ \land x \in (B, C)) \to A \in ℂ$
76	58 11	sstrid	$⊢ φ \to (B, C) \subseteq ℂ$
77	76	sselda	$⊢ (φ \land x \in (B, C)) \to x \in ℂ$
78	75 77	mulcld	$⊢ (φ \land x \in (B, C)) \to A x \in ℂ$
79	78	coscld	$⊢ (φ \land x \in (B, C)) \to \cos A x \in ℂ$
80	70 73 74 79	fvmptd	$⊢ (φ \land x \in (B, C)) \to \frac{d (y \in [B, C]⟼ \frac{\sin A y}{A})}{d_{ℝ} y} (x) = \cos A x$
81	80	eqcomd	$⊢ (φ \land x \in (B, C)) \to \cos A x = \frac{d (y \in [B, C]⟼ \frac{\sin A y}{A})}{d_{ℝ} y} (x)$
82	81	itgeq2dv	$⊢ φ \to \int_{(B, C)} \cos A x d x = \int_{(B, C)} \frac{d (y \in [B, C]⟼ \frac{\sin A y}{A})}{d_{ℝ} y} (x) d x$
83		eqidd	$⊢ φ \to (y \in [B, C] ⟼ \frac{\sin A y}{A}) = (y \in [B, C] ⟼ \frac{\sin A y}{A})$
84		oveq2	$⊢ y = C \to A y = A C$
85	84	fveq2d	$⊢ y = C \to \sin A y = \sin A C$
86	85	oveq1d	$⊢ y = C \to \frac{\sin A y}{A} = \frac{\sin A C}{A}$
87	86	adantl	$⊢ (φ \land y = C) \to \frac{\sin A y}{A} = \frac{\sin A C}{A}$
88	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
89	3	rexrd	$⊢ φ \to C \in ℝ^{*}$
90		ubicc2	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land B \leq C) \to C \in [B, C]$
91	88 89 4 90	syl3anc	$⊢ φ \to C \in [B, C]$
92	3	recnd	$⊢ φ \to C \in ℂ$
93	1 92	mulcld	$⊢ φ \to A C \in ℂ$
94	93	sincld	$⊢ φ \to \sin A C \in ℂ$
95	94 1 5	divcld	$⊢ φ \to \frac{\sin A C}{A} \in ℂ$
96	83 87 91 95	fvmptd	$⊢ φ \to (y \in [B, C] ⟼ \frac{\sin A y}{A}) (C) = \frac{\sin A C}{A}$
97		oveq2	$⊢ y = B \to A y = A B$
98	97	fveq2d	$⊢ y = B \to \sin A y = \sin A B$
99	98	oveq1d	$⊢ y = B \to \frac{\sin A y}{A} = \frac{\sin A B}{A}$
100	99	adantl	$⊢ (φ \land y = B) \to \frac{\sin A y}{A} = \frac{\sin A B}{A}$
101		lbicc2	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land B \leq C) \to B \in [B, C]$
102	88 89 4 101	syl3anc	$⊢ φ \to B \in [B, C]$
103	2	recnd	$⊢ φ \to B \in ℂ$
104	1 103	mulcld	$⊢ φ \to A B \in ℂ$
105	104	sincld	$⊢ φ \to \sin A B \in ℂ$
106	105 1 5	divcld	$⊢ φ \to \frac{\sin A B}{A} \in ℂ$
107	83 100 102 106	fvmptd	$⊢ φ \to (y \in [B, C] ⟼ \frac{\sin A y}{A}) (B) = \frac{\sin A B}{A}$
108	96 107	oveq12d	$⊢ φ \to (y \in [B, C] ⟼ \frac{\sin A y}{A}) (C) - (y \in [B, C] ⟼ \frac{\sin A y}{A}) (B) = (\frac{\sin A C}{A}) - (\frac{\sin A B}{A})$
109		coscn	$⊢ \cos : ℂ \underset{cn}{⟶} ℂ$
110	109	a1i	$⊢ φ \to \cos : ℂ \underset{cn}{⟶} ℂ$
111	76 1 37	constcncfg	$⊢ φ \to (y \in (B, C) ⟼ A) : (B, C) \underset{cn}{⟶} ℂ$
112	76 37	idcncfg	$⊢ φ \to (y \in (B, C) ⟼ y) : (B, C) \underset{cn}{⟶} ℂ$
113	111 112	mulcncf	$⊢ φ \to (y \in (B, C) ⟼ A y) : (B, C) \underset{cn}{⟶} ℂ$
114	110 113	cncfmpt1f	$⊢ φ \to (y \in (B, C) ⟼ \cos A y) : (B, C) \underset{cn}{⟶} ℂ$
115	69 114	eqeltrd	$⊢ φ \to \frac{d (y \in [B, C]⟼ \frac{\sin A y}{A})}{d_{ℝ} y} : (B, C) \underset{cn}{⟶} ℂ$
116		ioossicc	$⊢ (B, C) \subseteq [B, C]$
117	116	a1i	$⊢ φ \to (B, C) \subseteq [B, C]$
118		ioombl	$⊢ (B, C) \in dom vol$
119	118	a1i	$⊢ φ \to (B, C) \in dom vol$
120	1	adantr	$⊢ (φ \land y \in [B, C]) \to A \in ℂ$
121	6 10	sstrdi	$⊢ φ \to [B, C] \subseteq ℂ$
122	121	sselda	$⊢ (φ \land y \in [B, C]) \to y \in ℂ$
123	120 122	mulcld	$⊢ (φ \land y \in [B, C]) \to A y \in ℂ$
124	123	coscld	$⊢ (φ \land y \in [B, C]) \to \cos A y \in ℂ$
125	121 1 37	constcncfg	$⊢ φ \to (y \in [B, C] ⟼ A) : [B, C] \underset{cn}{⟶} ℂ$
126	121 37	idcncfg	$⊢ φ \to (y \in [B, C] ⟼ y) : [B, C] \underset{cn}{⟶} ℂ$
127	125 126	mulcncf	$⊢ φ \to (y \in [B, C] ⟼ A y) : [B, C] \underset{cn}{⟶} ℂ$
128	110 127	cncfmpt1f	$⊢ φ \to (y \in [B, C] ⟼ \cos A y) : [B, C] \underset{cn}{⟶} ℂ$
129		cniccibl	$⊢ (B \in ℝ \land C \in ℝ \land (y \in [B, C] ⟼ \cos A y) : [B, C] \underset{cn}{⟶} ℂ) \to (y \in [B, C] ⟼ \cos A y) \in 𝐿^{1}$
130	2 3 128 129	syl3anc	$⊢ φ \to (y \in [B, C] ⟼ \cos A y) \in 𝐿^{1}$
131	117 119 124 130	iblss	$⊢ φ \to (y \in (B, C) ⟼ \cos A y) \in 𝐿^{1}$
132	69 131	eqeltrd	$⊢ φ \to \frac{d (y \in [B, C]⟼ \frac{\sin A y}{A})}{d_{ℝ} y} \in 𝐿^{1}$
133		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
134	133	a1i	$⊢ φ \to \sin : ℂ \underset{cn}{⟶} ℂ$
135	134 127	cncfmpt1f	$⊢ φ \to (y \in [B, C] ⟼ \sin A y) : [B, C] \underset{cn}{⟶} ℂ$
136		neneq	$⊢ A \neq 0 \to \neg A = 0$
137		elsni	$⊢ A \in \{0\} \to A = 0$
138	137	con3i	$⊢ \neg A = 0 \to \neg A \in \{0\}$
139	5 136 138	3syl	$⊢ φ \to \neg A \in \{0\}$
140	1 139	eldifd	$⊢ φ \to A \in (ℂ ∖ \{0\})$
141		difssd	$⊢ φ \to ℂ ∖ \{0\} \subseteq ℂ$
142	121 140 141	constcncfg	$⊢ φ \to (y \in [B, C] ⟼ A) : [B, C] \underset{cn}{⟶} (ℂ ∖ \{0\})$
143	135 142	divcncf	$⊢ φ \to (y \in [B, C] ⟼ \frac{\sin A y}{A}) : [B, C] \underset{cn}{⟶} ℂ$
144	2 3 4 115 132 143	ftc2	$⊢ φ \to \int_{(B, C)} \frac{d (y \in [B, C]⟼ \frac{\sin A y}{A})}{d_{ℝ} y} (x) d x = (y \in [B, C] ⟼ \frac{\sin A y}{A}) (C) - (y \in [B, C] ⟼ \frac{\sin A y}{A}) (B)$
145	94 105 1 5	divsubdird	$⊢ φ \to \frac{\sin A C - \sin A B}{A} = (\frac{\sin A C}{A}) - (\frac{\sin A B}{A})$
146	108 144 145	3eqtr4d	$⊢ φ \to \int_{(B, C)} \frac{d (y \in [B, C]⟼ \frac{\sin A y}{A})}{d_{ℝ} y} (x) d x = \frac{\sin A C - \sin A B}{A}$
147	82 146	eqtrd	$⊢ φ \to \int_{(B, C)} \cos A x d x = \frac{\sin A C - \sin A B}{A}$

Metamath Proof Explorer

Theorem itgcoscmulx

Proof