itgsincmulx

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

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

Proof

Step	Hyp	Ref	Expression
1		itgsincmulx.a	$⊢ φ \to A \in ℂ$
2		itgsincmulx.an0	$⊢ φ \to A \neq 0$
3		itgsincmulx.b	$⊢ φ \to B \in ℝ$
4		itgsincmulx.c	$⊢ φ \to C \in ℝ$
5		itgsincmulx.blec	$⊢ φ \to B \leq C$
6		eqid	$⊢ (y \in ℂ ⟼ \frac{- \cos A y}{A}) = (y \in ℂ ⟼ \frac{- \cos A y}{A})$
7	1	adantr	$⊢ (φ \land y \in ℂ) \to A \in ℂ$
8		simpr	$⊢ (φ \land y \in ℂ) \to y \in ℂ$
9	7 8	mulcld	$⊢ (φ \land y \in ℂ) \to A y \in ℂ$
10	9	coscld	$⊢ (φ \land y \in ℂ) \to \cos A y \in ℂ$
11	10	negcld	$⊢ (φ \land y \in ℂ) \to - \cos A y \in ℂ$
12	2	adantr	$⊢ (φ \land y \in ℂ) \to A \neq 0$
13	11 7 12	divcld	$⊢ (φ \land y \in ℂ) \to \frac{- \cos A y}{A} \in ℂ$
14		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
15	14	a1i	$⊢ φ \to ℂ \in \{ℝ, ℂ\}$
16	9	sincld	$⊢ (φ \land y \in ℂ) \to \sin A y \in ℂ$
17	16	negcld	$⊢ (φ \land y \in ℂ) \to - \sin A y \in ℂ$
18	7 17	mulcld	$⊢ (φ \land y \in ℂ) \to A (- \sin A y) \in ℂ$
19	18	negcld	$⊢ (φ \land y \in ℂ) \to - A (- \sin A y) \in ℂ$
20		dvcosax	$⊢ A \in ℂ \to \frac{d (y \in ℂ⟼ \cos A y)}{d_{ℂ} y} = (y \in ℂ ⟼ A (- \sin A y))$
21	1 20	syl	$⊢ φ \to \frac{d (y \in ℂ⟼ \cos A y)}{d_{ℂ} y} = (y \in ℂ ⟼ A (- \sin A y))$
22	15 10 18 21	dvmptneg	$⊢ φ \to \frac{d (y \in ℂ⟼ - \cos A y)}{d_{ℂ} y} = (y \in ℂ ⟼ - A (- \sin A y))$
23	15 11 19 22 1 2	dvmptdivc	$⊢ φ \to \frac{d (y \in ℂ⟼ \frac{- \cos A y}{A})}{d_{ℂ} y} = (y \in ℂ ⟼ \frac{- A (- \sin A y)}{A})$
24	18 7 12	divnegd	$⊢ (φ \land y \in ℂ) \to - \frac{A (- \sin A y)}{A} = \frac{- A (- \sin A y)}{A}$
25	24	eqcomd	$⊢ (φ \land y \in ℂ) \to \frac{- A (- \sin A y)}{A} = - \frac{A (- \sin A y)}{A}$
26	17 7 12	divcan3d	$⊢ (φ \land y \in ℂ) \to \frac{A (- \sin A y)}{A} = - \sin A y$
27	26	negeqd	$⊢ (φ \land y \in ℂ) \to - \frac{A (- \sin A y)}{A} = - (- \sin A y)$
28	16	negnegd	$⊢ (φ \land y \in ℂ) \to - (- \sin A y) = \sin A y$
29	25 27 28	3eqtrd	$⊢ (φ \land y \in ℂ) \to \frac{- A (- \sin A y)}{A} = \sin A y$
30	29	mpteq2dva	$⊢ φ \to (y \in ℂ ⟼ \frac{- A (- \sin A y)}{A}) = (y \in ℂ ⟼ \sin A y)$
31	23 30	eqtrd	$⊢ φ \to \frac{d (y \in ℂ⟼ \frac{- \cos A y}{A})}{d_{ℂ} y} = (y \in ℂ ⟼ \sin A y)$
32	6 13 31 16 3 4	dvmptresicc	$⊢ φ \to \frac{d (y \in [B, C]⟼ \frac{- \cos A y}{A})}{d_{ℝ} y} = (y \in (B, C) ⟼ \sin A y)$
33	32	fveq1d	$⊢ φ \to \frac{d (y \in [B, C]⟼ \frac{- \cos A y}{A})}{d_{ℝ} y} (x) = (y \in (B, C) ⟼ \sin A y) (x)$
34	33	adantr	$⊢ (φ \land x \in (B, C)) \to \frac{d (y \in [B, C]⟼ \frac{- \cos A y}{A})}{d_{ℝ} y} (x) = (y \in (B, C) ⟼ \sin A y) (x)$
35		eqidd	$⊢ (φ \land x \in (B, C)) \to (y \in (B, C) ⟼ \sin A y) = (y \in (B, C) ⟼ \sin A y)$
36		oveq2	$⊢ y = x \to A y = A x$
37	36	fveq2d	$⊢ y = x \to \sin A y = \sin A x$
38	37	adantl	$⊢ ((φ \land x \in (B, C)) \land y = x) \to \sin A y = \sin A x$
39		simpr	$⊢ (φ \land x \in (B, C)) \to x \in (B, C)$
40	1	adantr	$⊢ (φ \land x \in (B, C)) \to A \in ℂ$
41		ioosscn	$⊢ (B, C) \subseteq ℂ$
42	41 39	sseldi	$⊢ (φ \land x \in (B, C)) \to x \in ℂ$
43	40 42	mulcld	$⊢ (φ \land x \in (B, C)) \to A x \in ℂ$
44	43	sincld	$⊢ (φ \land x \in (B, C)) \to \sin A x \in ℂ$
45	35 38 39 44	fvmptd	$⊢ (φ \land x \in (B, C)) \to (y \in (B, C) ⟼ \sin A y) (x) = \sin A x$
46	34 45	eqtr2d	$⊢ (φ \land x \in (B, C)) \to \sin A x = \frac{d (y \in [B, C]⟼ \frac{- \cos A y}{A})}{d_{ℝ} y} (x)$
47	46	itgeq2dv	$⊢ φ \to \int_{(B, C)} \sin A x d x = \int_{(B, C)} \frac{d (y \in [B, C]⟼ \frac{- \cos A y}{A})}{d_{ℝ} y} (x) d x$
48		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
49	48	a1i	$⊢ φ \to \sin : ℂ \underset{cn}{⟶} ℂ$
50	41	a1i	$⊢ φ \to (B, C) \subseteq ℂ$
51		ssid	$⊢ ℂ \subseteq ℂ$
52	51	a1i	$⊢ φ \to ℂ \subseteq ℂ$
53	50 1 52	constcncfg	$⊢ φ \to (y \in (B, C) ⟼ A) : (B, C) \underset{cn}{⟶} ℂ$
54	50 52	idcncfg	$⊢ φ \to (y \in (B, C) ⟼ y) : (B, C) \underset{cn}{⟶} ℂ$
55	53 54	mulcncf	$⊢ φ \to (y \in (B, C) ⟼ A y) : (B, C) \underset{cn}{⟶} ℂ$
56	49 55	cncfmpt1f	$⊢ φ \to (y \in (B, C) ⟼ \sin A y) : (B, C) \underset{cn}{⟶} ℂ$
57	32 56	eqeltrd	$⊢ φ \to \frac{d (y \in [B, C]⟼ \frac{- \cos A y}{A})}{d_{ℝ} y} : (B, C) \underset{cn}{⟶} ℂ$
58		ioossicc	$⊢ (B, C) \subseteq [B, C]$
59	58	a1i	$⊢ φ \to (B, C) \subseteq [B, C]$
60		ioombl	$⊢ (B, C) \in dom vol$
61	60	a1i	$⊢ φ \to (B, C) \in dom vol$
62	1	adantr	$⊢ (φ \land y \in [B, C]) \to A \in ℂ$
63	3 4	iccssred	$⊢ φ \to [B, C] \subseteq ℝ$
64		ax-resscn	$⊢ ℝ \subseteq ℂ$
65	63 64	sstrdi	$⊢ φ \to [B, C] \subseteq ℂ$
66	65	sselda	$⊢ (φ \land y \in [B, C]) \to y \in ℂ$
67	62 66	mulcld	$⊢ (φ \land y \in [B, C]) \to A y \in ℂ$
68	67	sincld	$⊢ (φ \land y \in [B, C]) \to \sin A y \in ℂ$
69	65 1 52	constcncfg	$⊢ φ \to (y \in [B, C] ⟼ A) : [B, C] \underset{cn}{⟶} ℂ$
70	65 52	idcncfg	$⊢ φ \to (y \in [B, C] ⟼ y) : [B, C] \underset{cn}{⟶} ℂ$
71	69 70	mulcncf	$⊢ φ \to (y \in [B, C] ⟼ A y) : [B, C] \underset{cn}{⟶} ℂ$
72	49 71	cncfmpt1f	$⊢ φ \to (y \in [B, C] ⟼ \sin A y) : [B, C] \underset{cn}{⟶} ℂ$
73		cniccibl	$⊢ (B \in ℝ \land C \in ℝ \land (y \in [B, C] ⟼ \sin A y) : [B, C] \underset{cn}{⟶} ℂ) \to (y \in [B, C] ⟼ \sin A y) \in 𝐿^{1}$
74	3 4 72 73	syl3anc	$⊢ φ \to (y \in [B, C] ⟼ \sin A y) \in 𝐿^{1}$
75	59 61 68 74	iblss	$⊢ φ \to (y \in (B, C) ⟼ \sin A y) \in 𝐿^{1}$
76	32 75	eqeltrd	$⊢ φ \to \frac{d (y \in [B, C]⟼ \frac{- \cos A y}{A})}{d_{ℝ} y} \in 𝐿^{1}$
77		coscn	$⊢ \cos : ℂ \underset{cn}{⟶} ℂ$
78	77	a1i	$⊢ φ \to \cos : ℂ \underset{cn}{⟶} ℂ$
79	78 71	cncfmpt1f	$⊢ φ \to (y \in [B, C] ⟼ \cos A y) : [B, C] \underset{cn}{⟶} ℂ$
80	79	negcncfg	$⊢ φ \to (y \in [B, C] ⟼ - \cos A y) : [B, C] \underset{cn}{⟶} ℂ$
81	2	neneqd	$⊢ φ \to \neg A = 0$
82		elsng	$⊢ A \in ℂ \to (A \in \{0\} \leftrightarrow A = 0)$
83	1 82	syl	$⊢ φ \to (A \in \{0\} \leftrightarrow A = 0)$
84	81 83	mtbird	$⊢ φ \to \neg A \in \{0\}$
85	1 84	eldifd	$⊢ φ \to A \in (ℂ ∖ \{0\})$
86		difssd	$⊢ φ \to ℂ ∖ \{0\} \subseteq ℂ$
87	65 85 86	constcncfg	$⊢ φ \to (y \in [B, C] ⟼ A) : [B, C] \underset{cn}{⟶} (ℂ ∖ \{0\})$
88	80 87	divcncf	$⊢ φ \to (y \in [B, C] ⟼ \frac{- \cos A y}{A}) : [B, C] \underset{cn}{⟶} ℂ$
89	3 4 5 57 76 88	ftc2	$⊢ φ \to \int_{(B, C)} \frac{d (y \in [B, C]⟼ \frac{- \cos A y}{A})}{d_{ℝ} y} (x) d x = (y \in [B, C] ⟼ \frac{- \cos A y}{A}) (C) - (y \in [B, C] ⟼ \frac{- \cos A y}{A}) (B)$
90		eqidd	$⊢ φ \to (y \in [B, C] ⟼ \frac{- \cos A y}{A}) = (y \in [B, C] ⟼ \frac{- \cos A y}{A})$
91		oveq2	$⊢ y = C \to A y = A C$
92	91	fveq2d	$⊢ y = C \to \cos A y = \cos A C$
93	92	negeqd	$⊢ y = C \to - \cos A y = - \cos A C$
94	93	oveq1d	$⊢ y = C \to \frac{- \cos A y}{A} = \frac{- \cos A C}{A}$
95	94	adantl	$⊢ (φ \land y = C) \to \frac{- \cos A y}{A} = \frac{- \cos A C}{A}$
96	3	rexrd	$⊢ φ \to B \in ℝ^{*}$
97	4	rexrd	$⊢ φ \to C \in ℝ^{*}$
98		ubicc2	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land B \leq C) \to C \in [B, C]$
99	96 97 5 98	syl3anc	$⊢ φ \to C \in [B, C]$
100		ovexd	$⊢ φ \to \frac{- \cos A C}{A} \in V$
101	90 95 99 100	fvmptd	$⊢ φ \to (y \in [B, C] ⟼ \frac{- \cos A y}{A}) (C) = \frac{- \cos A C}{A}$
102		oveq2	$⊢ y = B \to A y = A B$
103	102	fveq2d	$⊢ y = B \to \cos A y = \cos A B$
104	103	negeqd	$⊢ y = B \to - \cos A y = - \cos A B$
105	104	oveq1d	$⊢ y = B \to \frac{- \cos A y}{A} = \frac{- \cos A B}{A}$
106	105	adantl	$⊢ (φ \land y = B) \to \frac{- \cos A y}{A} = \frac{- \cos A B}{A}$
107		lbicc2	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land B \leq C) \to B \in [B, C]$
108	96 97 5 107	syl3anc	$⊢ φ \to B \in [B, C]$
109		ovexd	$⊢ φ \to \frac{- \cos A B}{A} \in V$
110	90 106 108 109	fvmptd	$⊢ φ \to (y \in [B, C] ⟼ \frac{- \cos A y}{A}) (B) = \frac{- \cos A B}{A}$
111	101 110	oveq12d	$⊢ φ \to (y \in [B, C] ⟼ \frac{- \cos A y}{A}) (C) - (y \in [B, C] ⟼ \frac{- \cos A y}{A}) (B) = (\frac{- \cos A C}{A}) - (\frac{- \cos A B}{A})$
112	3	recnd	$⊢ φ \to B \in ℂ$
113	1 112	mulcld	$⊢ φ \to A B \in ℂ$
114	113	coscld	$⊢ φ \to \cos A B \in ℂ$
115	114 1 2	divnegd	$⊢ φ \to - \frac{\cos A B}{A} = \frac{- \cos A B}{A}$
116	115	eqcomd	$⊢ φ \to \frac{- \cos A B}{A} = - \frac{\cos A B}{A}$
117	116	oveq2d	$⊢ φ \to (\frac{- \cos A C}{A}) - (\frac{- \cos A B}{A}) = (\frac{- \cos A C}{A}) - (- \frac{\cos A B}{A})$
118	4	recnd	$⊢ φ \to C \in ℂ$
119	1 118	mulcld	$⊢ φ \to A C \in ℂ$
120	119	coscld	$⊢ φ \to \cos A C \in ℂ$
121	120	negcld	$⊢ φ \to - \cos A C \in ℂ$
122	121 1 2	divcld	$⊢ φ \to \frac{- \cos A C}{A} \in ℂ$
123	114 1 2	divcld	$⊢ φ \to \frac{\cos A B}{A} \in ℂ$
124	122 123	subnegd	$⊢ φ \to (\frac{- \cos A C}{A}) - (- \frac{\cos A B}{A}) = (\frac{- \cos A C}{A}) + (\frac{\cos A B}{A})$
125	111 117 124	3eqtrd	$⊢ φ \to (y \in [B, C] ⟼ \frac{- \cos A y}{A}) (C) - (y \in [B, C] ⟼ \frac{- \cos A y}{A}) (B) = (\frac{- \cos A C}{A}) + (\frac{\cos A B}{A})$
126	122 123	addcomd	$⊢ φ \to (\frac{- \cos A C}{A}) + (\frac{\cos A B}{A}) = (\frac{\cos A B}{A}) + (\frac{- \cos A C}{A})$
127	120 1 2	divnegd	$⊢ φ \to - \frac{\cos A C}{A} = \frac{- \cos A C}{A}$
128	127	eqcomd	$⊢ φ \to \frac{- \cos A C}{A} = - \frac{\cos A C}{A}$
129	128	oveq2d	$⊢ φ \to (\frac{\cos A B}{A}) + (\frac{- \cos A C}{A}) = (\frac{\cos A B}{A}) + (- \frac{\cos A C}{A})$
130	120 1 2	divcld	$⊢ φ \to \frac{\cos A C}{A} \in ℂ$
131	123 130	negsubd	$⊢ φ \to (\frac{\cos A B}{A}) + (- \frac{\cos A C}{A}) = (\frac{\cos A B}{A}) - (\frac{\cos A C}{A})$
132	114 120 1 2	divsubdird	$⊢ φ \to \frac{\cos A B - \cos A C}{A} = (\frac{\cos A B}{A}) - (\frac{\cos A C}{A})$
133	132	eqcomd	$⊢ φ \to (\frac{\cos A B}{A}) - (\frac{\cos A C}{A}) = \frac{\cos A B - \cos A C}{A}$
134	129 131 133	3eqtrd	$⊢ φ \to (\frac{\cos A B}{A}) + (\frac{- \cos A C}{A}) = \frac{\cos A B - \cos A C}{A}$
135	125 126 134	3eqtrd	$⊢ φ \to (y \in [B, C] ⟼ \frac{- \cos A y}{A}) (C) - (y \in [B, C] ⟼ \frac{- \cos A y}{A}) (B) = \frac{\cos A B - \cos A C}{A}$
136	47 89 135	3eqtrd	$⊢ φ \to \int_{(B, C)} \sin A x d x = \frac{\cos A B - \cos A C}{A}$

Metamath Proof Explorer

Theorem itgsincmulx

Proof