dirkeritg

Description: The definite integral of the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	dirkeritg.d	$⊢ D = (n \in ℕ ⟼ (x \in ℝ ⟼ if (x \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})})))$
	dirkeritg.n	$⊢ φ \to N \in ℕ$
	dirkeritg.f	$⊢ F = D (N)$
	dirkeritg.a	$⊢ φ \to A \in ℝ$
	dirkeritg.b	$⊢ φ \to B \in ℝ$
	dirkeritg.aleb	$⊢ φ \to A \leq B$
	dirkeritg.g	$⊢ G = (x \in [A, B] ⟼ \frac{(\frac{x}{2}) + \sum_{k = 1}^{N} (\frac{\sin k x}{k})}{π})$
Assertion	dirkeritg	$⊢ φ \to \int_{(A, B)} F (x) d x = G (B) - G (A)$

Proof

Step	Hyp	Ref	Expression
1		dirkeritg.d	$⊢ D = (n \in ℕ ⟼ (x \in ℝ ⟼ if (x \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})})))$
2		dirkeritg.n	$⊢ φ \to N \in ℕ$
3		dirkeritg.f	$⊢ F = D (N)$
4		dirkeritg.a	$⊢ φ \to A \in ℝ$
5		dirkeritg.b	$⊢ φ \to B \in ℝ$
6		dirkeritg.aleb	$⊢ φ \to A \leq B$
7		dirkeritg.g	$⊢ G = (x \in [A, B] ⟼ \frac{(\frac{x}{2}) + \sum_{k = 1}^{N} (\frac{\sin k x}{k})}{π})$
8		fveq2	$⊢ x = s \to F (x) = F (s)$
9	8	cbvitgv	$⊢ \int_{(A, B)} F (x) d x = \int_{(A, B)} F (s) d s$
10	9	a1i	$⊢ φ \to \int_{(A, B)} F (x) d x = \int_{(A, B)} F (s) d s$
11		elioore	$⊢ s \in (A, B) \to s \in ℝ$
12	11	adantl	$⊢ (φ \land s \in (A, B)) \to s \in ℝ$
13		halfre	$⊢ \frac{1}{2} \in ℝ$
14	13	a1i	$⊢ s \in ℝ \to \frac{1}{2} \in ℝ$
15		fzfid	$⊢ s \in ℝ \to (1 \dots N) \in Fin$
16		elfzelz	$⊢ k \in (1 \dots N) \to k \in ℤ$
17	16	zred	$⊢ k \in (1 \dots N) \to k \in ℝ$
18	17	adantl	$⊢ (s \in ℝ \land k \in (1 \dots N)) \to k \in ℝ$
19		simpl	$⊢ (s \in ℝ \land k \in (1 \dots N)) \to s \in ℝ$
20	18 19	remulcld	$⊢ (s \in ℝ \land k \in (1 \dots N)) \to k s \in ℝ$
21	20	recoscld	$⊢ (s \in ℝ \land k \in (1 \dots N)) \to \cos k s \in ℝ$
22	15 21	fsumrecl	$⊢ s \in ℝ \to \sum_{k = 1}^{N} \cos k s \in ℝ$
23	14 22	readdcld	$⊢ s \in ℝ \to (\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s \in ℝ$
24		pire	$⊢ π \in ℝ$
25	24	a1i	$⊢ s \in ℝ \to π \in ℝ$
26		pipos	$⊢ 0 < π$
27	24 26	gt0ne0ii	$⊢ π \neq 0$
28	27	a1i	$⊢ s \in ℝ \to π \neq 0$
29	23 25 28	redivcld	$⊢ s \in ℝ \to \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π} \in ℝ$
30	12 29	syl	$⊢ (φ \land s \in (A, B)) \to \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π} \in ℝ$
31		eqid	$⊢ (s \in ℝ ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}) = (s \in ℝ ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π})$
32	31	fvmpt2	$⊢ (s \in ℝ \land \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π} \in ℝ) \to (s \in ℝ ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}) (s) = \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}$
33	12 30 32	syl2anc	$⊢ (φ \land s \in (A, B)) \to (s \in ℝ ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}) (s) = \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}$
34		oveq1	$⊢ x = s \to x \mod 2 π = s \mod 2 π$
35	34	eqeq1d	$⊢ x = s \to (x \mod 2 π = 0 \leftrightarrow s \mod 2 π = 0)$
36		oveq2	$⊢ x = s \to (n + (\frac{1}{2})) x = (n + (\frac{1}{2})) s$
37	36	fveq2d	$⊢ x = s \to \sin (n + (\frac{1}{2})) x = \sin (n + (\frac{1}{2})) s$
38		oveq1	$⊢ x = s \to \frac{x}{2} = \frac{s}{2}$
39	38	fveq2d	$⊢ x = s \to \sin (\frac{x}{2}) = \sin (\frac{s}{2})$
40	39	oveq2d	$⊢ x = s \to 2 π \sin (\frac{x}{2}) = 2 π \sin (\frac{s}{2})$
41	37 40	oveq12d	$⊢ x = s \to \frac{\sin (n + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})} = \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}$
42	35 41	ifbieq2d	$⊢ x = s \to if (x \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})}) = if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})$
43	42	cbvmptv	$⊢ (x \in ℝ ⟼ if (x \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})})) = (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})}))$
44	43	mpteq2i	$⊢ (n \in ℕ ⟼ (x \in ℝ ⟼ if (x \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) x}{2 π \sin (\frac{x}{2})}))) = (n \in ℕ ⟼ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})))$
45	1 44	eqtri	$⊢ D = (n \in ℕ ⟼ (s \in ℝ ⟼ if (s \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) s}{2 π \sin (\frac{s}{2})})))$
46	45 2 3 31	dirkertrigeq	$⊢ φ \to F = (s \in ℝ ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π})$
47	46	fveq1d	$⊢ φ \to F (s) = (s \in ℝ ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}) (s)$
48	47	adantr	$⊢ (φ \land s \in (A, B)) \to F (s) = (s \in ℝ ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}) (s)$
49		oveq2	$⊢ x = s \to k x = k s$
50	49	fveq2d	$⊢ x = s \to \sin k x = \sin k s$
51	50	oveq1d	$⊢ x = s \to \frac{\sin k x}{k} = \frac{\sin k s}{k}$
52	51	sumeq2sdv	$⊢ x = s \to \sum_{k = 1}^{N} (\frac{\sin k x}{k}) = \sum_{k = 1}^{N} (\frac{\sin k s}{k})$
53	38 52	oveq12d	$⊢ x = s \to (\frac{x}{2}) + \sum_{k = 1}^{N} (\frac{\sin k x}{k}) = (\frac{s}{2}) + \sum_{k = 1}^{N} (\frac{\sin k s}{k})$
54	53	oveq1d	$⊢ x = s \to \frac{(\frac{x}{2}) + \sum_{k = 1}^{N} (\frac{\sin k x}{k})}{π} = \frac{(\frac{s}{2}) + \sum_{k = 1}^{N} (\frac{\sin k s}{k})}{π}$
55	54	cbvmptv	$⊢ (x \in [A, B] ⟼ \frac{(\frac{x}{2}) + \sum_{k = 1}^{N} (\frac{\sin k x}{k})}{π}) = (s \in [A, B] ⟼ \frac{(\frac{s}{2}) + \sum_{k = 1}^{N} (\frac{\sin k s}{k})}{π})$
56	7 55	eqtri	$⊢ G = (s \in [A, B] ⟼ \frac{(\frac{s}{2}) + \sum_{k = 1}^{N} (\frac{\sin k s}{k})}{π})$
57	56	oveq2i	$⊢ ℝ D G = \frac{d (s \in [A, B]⟼ \frac{(\frac{s}{2}) + \sum_{k = 1}^{N} (\frac{\sin k s}{k})}{π})}{d_{ℝ} s}$
58		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
59	58	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
60		recn	$⊢ s \in ℝ \to s \in ℂ$
61	60	halfcld	$⊢ s \in ℝ \to \frac{s}{2} \in ℂ$
62	16	zcnd	$⊢ k \in (1 \dots N) \to k \in ℂ$
63	62	adantl	$⊢ (s \in ℝ \land k \in (1 \dots N)) \to k \in ℂ$
64	60	adantr	$⊢ (s \in ℝ \land k \in (1 \dots N)) \to s \in ℂ$
65	63 64	mulcld	$⊢ (s \in ℝ \land k \in (1 \dots N)) \to k s \in ℂ$
66	65	sincld	$⊢ (s \in ℝ \land k \in (1 \dots N)) \to \sin k s \in ℂ$
67		0red	$⊢ k \in (1 \dots N) \to 0 \in ℝ$
68		1red	$⊢ k \in (1 \dots N) \to 1 \in ℝ$
69		0lt1	$⊢ 0 < 1$
70	69	a1i	$⊢ k \in (1 \dots N) \to 0 < 1$
71		elfzle1	$⊢ k \in (1 \dots N) \to 1 \leq k$
72	67 68 17 70 71	ltletrd	$⊢ k \in (1 \dots N) \to 0 < k$
73	72	gt0ne0d	$⊢ k \in (1 \dots N) \to k \neq 0$
74	73	adantl	$⊢ (s \in ℝ \land k \in (1 \dots N)) \to k \neq 0$
75	66 63 74	divcld	$⊢ (s \in ℝ \land k \in (1 \dots N)) \to \frac{\sin k s}{k} \in ℂ$
76	15 75	fsumcl	$⊢ s \in ℝ \to \sum_{k = 1}^{N} (\frac{\sin k s}{k}) \in ℂ$
77	61 76	addcld	$⊢ s \in ℝ \to (\frac{s}{2}) + \sum_{k = 1}^{N} (\frac{\sin k s}{k}) \in ℂ$
78		picn	$⊢ π \in ℂ$
79	78	a1i	$⊢ s \in ℝ \to π \in ℂ$
80	77 79 28	divcld	$⊢ s \in ℝ \to \frac{(\frac{s}{2}) + \sum_{k = 1}^{N} (\frac{\sin k s}{k})}{π} \in ℂ$
81	80	adantl	$⊢ (φ \land s \in ℝ) \to \frac{(\frac{s}{2}) + \sum_{k = 1}^{N} (\frac{\sin k s}{k})}{π} \in ℂ$
82	29	adantl	$⊢ (φ \land s \in ℝ) \to \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π} \in ℝ$
83	77	adantl	$⊢ (φ \land s \in ℝ) \to (\frac{s}{2}) + \sum_{k = 1}^{N} (\frac{\sin k s}{k}) \in ℂ$
84	23	adantl	$⊢ (φ \land s \in ℝ) \to (\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s \in ℝ$
85	61	adantl	$⊢ (φ \land s \in ℝ) \to \frac{s}{2} \in ℂ$
86	13	a1i	$⊢ (φ \land s \in ℝ) \to \frac{1}{2} \in ℝ$
87	60	adantl	$⊢ (φ \land s \in ℝ) \to s \in ℂ$
88		1red	$⊢ (φ \land s \in ℝ) \to 1 \in ℝ$
89	59	dvmptid	$⊢ φ \to \frac{d (s \in ℝ⟼ s)}{d_{ℝ} s} = (s \in ℝ ⟼ 1)$
90		2cnd	$⊢ φ \to 2 \in ℂ$
91		2ne0	$⊢ 2 \neq 0$
92	91	a1i	$⊢ φ \to 2 \neq 0$
93	59 87 88 89 90 92	dvmptdivc	$⊢ φ \to \frac{d (s \in ℝ⟼ \frac{s}{2})}{d_{ℝ} s} = (s \in ℝ ⟼ \frac{1}{2})$
94	76	adantl	$⊢ (φ \land s \in ℝ) \to \sum_{k = 1}^{N} (\frac{\sin k s}{k}) \in ℂ$
95	22	adantl	$⊢ (φ \land s \in ℝ) \to \sum_{k = 1}^{N} \cos k s \in ℝ$
96		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
97		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
98		reopn	$⊢ ℝ \in topGen (ran (.))$
99	98	a1i	$⊢ φ \to ℝ \in topGen (ran (.))$
100		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
101	75	ancoms	$⊢ (k \in (1 \dots N) \land s \in ℝ) \to \frac{\sin k s}{k} \in ℂ$
102	101	3adant1	$⊢ (φ \land k \in (1 \dots N) \land s \in ℝ) \to \frac{\sin k s}{k} \in ℂ$
103	21	ancoms	$⊢ (k \in (1 \dots N) \land s \in ℝ) \to \cos k s \in ℝ$
104	103	recnd	$⊢ (k \in (1 \dots N) \land s \in ℝ) \to \cos k s \in ℂ$
105	104	3adant1	$⊢ (φ \land k \in (1 \dots N) \land s \in ℝ) \to \cos k s \in ℂ$
106	58	a1i	$⊢ k \in (1 \dots N) \to ℝ \in \{ℝ, ℂ\}$
107	66	ancoms	$⊢ (k \in (1 \dots N) \land s \in ℝ) \to \sin k s \in ℂ$
108	62	adantr	$⊢ (k \in (1 \dots N) \land s \in ℂ) \to k \in ℂ$
109		simpr	$⊢ (k \in (1 \dots N) \land s \in ℂ) \to s \in ℂ$
110	108 109	mulcld	$⊢ (k \in (1 \dots N) \land s \in ℂ) \to k s \in ℂ$
111	110	coscld	$⊢ (k \in (1 \dots N) \land s \in ℂ) \to \cos k s \in ℂ$
112	108 111	mulcld	$⊢ (k \in (1 \dots N) \land s \in ℂ) \to k \cos k s \in ℂ$
113	60 112	sylan2	$⊢ (k \in (1 \dots N) \land s \in ℝ) \to k \cos k s \in ℂ$
114		ax-resscn	$⊢ ℝ \subseteq ℂ$
115		resmpt	$⊢ ℝ \subseteq ℂ \to {(s \in ℂ ⟼ \sin k s) ↾}_{ℝ} = (s \in ℝ ⟼ \sin k s)$
116	114 115	mp1i	$⊢ k \in (1 \dots N) \to {(s \in ℂ ⟼ \sin k s) ↾}_{ℝ} = (s \in ℝ ⟼ \sin k s)$
117	116	eqcomd	$⊢ k \in (1 \dots N) \to (s \in ℝ ⟼ \sin k s) = {(s \in ℂ ⟼ \sin k s) ↾}_{ℝ}$
118	117	oveq2d	$⊢ k \in (1 \dots N) \to \frac{d (s \in ℝ⟼ \sin k s)}{d_{ℝ} s} = ℝ D ({(s \in ℂ ⟼ \sin k s) ↾}_{ℝ})$
119	110	sincld	$⊢ (k \in (1 \dots N) \land s \in ℂ) \to \sin k s \in ℂ$
120	119	fmpttd	$⊢ k \in (1 \dots N) \to (s \in ℂ ⟼ \sin k s) : ℂ ⟶ ℂ$
121	112	ralrimiva	$⊢ k \in (1 \dots N) \to \forall s \in ℂ k \cos k s \in ℂ$
122		dmmptg	$⊢ \forall s \in ℂ k \cos k s \in ℂ \to dom (s \in ℂ ⟼ k \cos k s) = ℂ$
123	121 122	syl	$⊢ k \in (1 \dots N) \to dom (s \in ℂ ⟼ k \cos k s) = ℂ$
124	114 123	sseqtrrid	$⊢ k \in (1 \dots N) \to ℝ \subseteq dom (s \in ℂ ⟼ k \cos k s)$
125		dvsinax	$⊢ k \in ℂ \to \frac{d (s \in ℂ⟼ \sin k s)}{d_{ℂ} s} = (s \in ℂ ⟼ k \cos k s)$
126	62 125	syl	$⊢ k \in (1 \dots N) \to \frac{d (s \in ℂ⟼ \sin k s)}{d_{ℂ} s} = (s \in ℂ ⟼ k \cos k s)$
127	126	dmeqd	$⊢ k \in (1 \dots N) \to dom \frac{d (s \in ℂ⟼ \sin k s)}{d_{ℂ} s} = dom (s \in ℂ ⟼ k \cos k s)$
128	124 127	sseqtrrd	$⊢ k \in (1 \dots N) \to ℝ \subseteq dom \frac{d (s \in ℂ⟼ \sin k s)}{d_{ℂ} s}$
129		dvcnre	$⊢ ((s \in ℂ ⟼ \sin k s) : ℂ ⟶ ℂ \land ℝ \subseteq dom \frac{d (s \in ℂ⟼ \sin k s)}{d_{ℂ} s}) \to ℝ D ({(s \in ℂ ⟼ \sin k s) ↾}_{ℝ}) = {\frac{d (s \in ℂ⟼ \sin k s)}{d_{ℂ} s} ↾}_{ℝ}$
130	120 128 129	syl2anc	$⊢ k \in (1 \dots N) \to ℝ D ({(s \in ℂ ⟼ \sin k s) ↾}_{ℝ}) = {\frac{d (s \in ℂ⟼ \sin k s)}{d_{ℂ} s} ↾}_{ℝ}$
131	126	reseq1d	$⊢ k \in (1 \dots N) \to {\frac{d (s \in ℂ⟼ \sin k s)}{d_{ℂ} s} ↾}_{ℝ} = {(s \in ℂ ⟼ k \cos k s) ↾}_{ℝ}$
132		resmpt	$⊢ ℝ \subseteq ℂ \to {(s \in ℂ ⟼ k \cos k s) ↾}_{ℝ} = (s \in ℝ ⟼ k \cos k s)$
133	114 132	ax-mp	$⊢ {(s \in ℂ ⟼ k \cos k s) ↾}_{ℝ} = (s \in ℝ ⟼ k \cos k s)$
134	131 133	eqtrdi	$⊢ k \in (1 \dots N) \to {\frac{d (s \in ℂ⟼ \sin k s)}{d_{ℂ} s} ↾}_{ℝ} = (s \in ℝ ⟼ k \cos k s)$
135	118 130 134	3eqtrd	$⊢ k \in (1 \dots N) \to \frac{d (s \in ℝ⟼ \sin k s)}{d_{ℝ} s} = (s \in ℝ ⟼ k \cos k s)$
136	106 107 113 135 62 73	dvmptdivc	$⊢ k \in (1 \dots N) \to \frac{d (s \in ℝ⟼ \frac{\sin k s}{k})}{d_{ℝ} s} = (s \in ℝ ⟼ \frac{k \cos k s}{k})$
137	62	adantr	$⊢ (k \in (1 \dots N) \land s \in ℝ) \to k \in ℂ$
138	73	adantr	$⊢ (k \in (1 \dots N) \land s \in ℝ) \to k \neq 0$
139	104 137 138	divcan3d	$⊢ (k \in (1 \dots N) \land s \in ℝ) \to \frac{k \cos k s}{k} = \cos k s$
140	139	mpteq2dva	$⊢ k \in (1 \dots N) \to (s \in ℝ ⟼ \frac{k \cos k s}{k}) = (s \in ℝ ⟼ \cos k s)$
141	136 140	eqtrd	$⊢ k \in (1 \dots N) \to \frac{d (s \in ℝ⟼ \frac{\sin k s}{k})}{d_{ℝ} s} = (s \in ℝ ⟼ \cos k s)$
142	141	adantl	$⊢ (φ \land k \in (1 \dots N)) \to \frac{d (s \in ℝ⟼ \frac{\sin k s}{k})}{d_{ℝ} s} = (s \in ℝ ⟼ \cos k s)$
143	96 97 59 99 100 102 105 142	dvmptfsum	$⊢ φ \to \frac{d (s \in ℝ⟼ \sum_{k = 1}^{N} (\frac{\sin k s}{k}))}{d_{ℝ} s} = (s \in ℝ ⟼ \sum_{k = 1}^{N} \cos k s)$
144	59 85 86 93 94 95 143	dvmptadd	$⊢ φ \to \frac{d (s \in ℝ⟼ (\frac{s}{2}) + \sum_{k = 1}^{N} (\frac{\sin k s}{k}))}{d_{ℝ} s} = (s \in ℝ ⟼ (\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s)$
145	78	a1i	$⊢ φ \to π \in ℂ$
146	27	a1i	$⊢ φ \to π \neq 0$
147	59 83 84 144 145 146	dvmptdivc	$⊢ φ \to \frac{d (s \in ℝ⟼ \frac{(\frac{s}{2}) + \sum_{k = 1}^{N} (\frac{\sin k s}{k})}{π})}{d_{ℝ} s} = (s \in ℝ ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π})$
148	4 5	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
149		iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
150	4 5 149	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([A, B]) = (A, B)$
151	59 81 82 147 148 96 97 150	dvmptres2	$⊢ φ \to \frac{d (s \in [A, B]⟼ \frac{(\frac{s}{2}) + \sum_{k = 1}^{N} (\frac{\sin k s}{k})}{π})}{d_{ℝ} s} = (s \in (A, B) ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π})$
152	57 151	eqtrid	$⊢ φ \to ℝ D G = (s \in (A, B) ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π})$
153	152 30	fvmpt2d	$⊢ (φ \land s \in (A, B)) \to G_{ℝ}^{'} (s) = \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}$
154	33 48 153	3eqtr4d	$⊢ (φ \land s \in (A, B)) \to F (s) = G_{ℝ}^{'} (s)$
155	154	itgeq2dv	$⊢ φ \to \int_{(A, B)} F (s) d s = \int_{(A, B)} G_{ℝ}^{'} (s) d s$
156		ioosscn	$⊢ (A, B) \subseteq ℂ$
157	156	a1i	$⊢ φ \to (A, B) \subseteq ℂ$
158		halfcn	$⊢ \frac{1}{2} \in ℂ$
159	158	a1i	$⊢ φ \to \frac{1}{2} \in ℂ$
160		ssid	$⊢ ℂ \subseteq ℂ$
161	160	a1i	$⊢ φ \to ℂ \subseteq ℂ$
162	157 159 161	constcncfg	$⊢ φ \to (s \in (A, B) ⟼ \frac{1}{2}) : (A, B) \underset{cn}{⟶} ℂ$
163		eqid	$⊢ (s \in ℂ ⟼ \cos k s) = (s \in ℂ ⟼ \cos k s)$
164		coscn	$⊢ \cos : ℂ \underset{cn}{⟶} ℂ$
165	164	a1i	$⊢ k \in (1 \dots N) \to \cos : ℂ \underset{cn}{⟶} ℂ$
166		eqid	$⊢ (s \in ℂ ⟼ k s) = (s \in ℂ ⟼ k s)$
167	166	mulc1cncf	$⊢ k \in ℂ \to (s \in ℂ ⟼ k s) : ℂ \underset{cn}{⟶} ℂ$
168	62 167	syl	$⊢ k \in (1 \dots N) \to (s \in ℂ ⟼ k s) : ℂ \underset{cn}{⟶} ℂ$
169	165 168	cncfmpt1f	$⊢ k \in (1 \dots N) \to (s \in ℂ ⟼ \cos k s) : ℂ \underset{cn}{⟶} ℂ$
170	156	a1i	$⊢ k \in (1 \dots N) \to (A, B) \subseteq ℂ$
171	160	a1i	$⊢ k \in (1 \dots N) \to ℂ \subseteq ℂ$
172	11 104	sylan2	$⊢ (k \in (1 \dots N) \land s \in (A, B)) \to \cos k s \in ℂ$
173	163 169 170 171 172	cncfmptssg	$⊢ k \in (1 \dots N) \to (s \in (A, B) ⟼ \cos k s) : (A, B) \underset{cn}{⟶} ℂ$
174	173	adantl	$⊢ (φ \land k \in (1 \dots N)) \to (s \in (A, B) ⟼ \cos k s) : (A, B) \underset{cn}{⟶} ℂ$
175	157 100 174	fsumcncf	$⊢ φ \to (s \in (A, B) ⟼ \sum_{k = 1}^{N} \cos k s) : (A, B) \underset{cn}{⟶} ℂ$
176	162 175	addcncf	$⊢ φ \to (s \in (A, B) ⟼ (\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s) : (A, B) \underset{cn}{⟶} ℂ$
177		eqid	$⊢ (s \in ℂ ⟼ π) = (s \in ℂ ⟼ π)$
178		cncfmptc	$⊢ (π \in ℂ \land ℂ \subseteq ℂ \land ℂ \subseteq ℂ) \to (s \in ℂ ⟼ π) : ℂ \underset{cn}{⟶} ℂ$
179	78 160 160 178	mp3an	$⊢ (s \in ℂ ⟼ π) : ℂ \underset{cn}{⟶} ℂ$
180	179	a1i	$⊢ φ \to (s \in ℂ ⟼ π) : ℂ \underset{cn}{⟶} ℂ$
181		difssd	$⊢ φ \to ℂ ∖ \{0\} \subseteq ℂ$
182		eldifsn	$⊢ π \in (ℂ ∖ \{0\}) \leftrightarrow (π \in ℂ \land π \neq 0)$
183	78 27 182	mpbir2an	$⊢ π \in (ℂ ∖ \{0\})$
184	183	a1i	$⊢ (φ \land s \in (A, B)) \to π \in (ℂ ∖ \{0\})$
185	177 180 157 181 184	cncfmptssg	$⊢ φ \to (s \in (A, B) ⟼ π) : (A, B) \underset{cn}{⟶} (ℂ ∖ \{0\})$
186	176 185	divcncf	$⊢ φ \to (s \in (A, B) ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}) : (A, B) \underset{cn}{⟶} ℂ$
187	152 186	eqeltrd	$⊢ φ \to G_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
188		ioossicc	$⊢ (A, B) \subseteq [A, B]$
189	188	a1i	$⊢ φ \to (A, B) \subseteq [A, B]$
190		ioombl	$⊢ (A, B) \in dom vol$
191	190	a1i	$⊢ φ \to (A, B) \in dom vol$
192	13	a1i	$⊢ (φ \land s \in [A, B]) \to \frac{1}{2} \in ℝ$
193		fzfid	$⊢ (φ \land s \in [A, B]) \to (1 \dots N) \in Fin$
194	17	adantl	$⊢ ((φ \land s \in [A, B]) \land k \in (1 \dots N)) \to k \in ℝ$
195	148	sselda	$⊢ (φ \land s \in [A, B]) \to s \in ℝ$
196	195	adantr	$⊢ ((φ \land s \in [A, B]) \land k \in (1 \dots N)) \to s \in ℝ$
197	194 196	remulcld	$⊢ ((φ \land s \in [A, B]) \land k \in (1 \dots N)) \to k s \in ℝ$
198	197	recoscld	$⊢ ((φ \land s \in [A, B]) \land k \in (1 \dots N)) \to \cos k s \in ℝ$
199	193 198	fsumrecl	$⊢ (φ \land s \in [A, B]) \to \sum_{k = 1}^{N} \cos k s \in ℝ$
200	192 199	readdcld	$⊢ (φ \land s \in [A, B]) \to (\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s \in ℝ$
201	24	a1i	$⊢ (φ \land s \in [A, B]) \to π \in ℝ$
202	27	a1i	$⊢ (φ \land s \in [A, B]) \to π \neq 0$
203	200 201 202	redivcld	$⊢ (φ \land s \in [A, B]) \to \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π} \in ℝ$
204	148 114	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
205	204 159 161	constcncfg	$⊢ φ \to (s \in [A, B] ⟼ \frac{1}{2}) : [A, B] \underset{cn}{⟶} ℂ$
206		eqid	$⊢ (s \in ℂ ⟼ \sum_{k = 1}^{N} \cos k s) = (s \in ℂ ⟼ \sum_{k = 1}^{N} \cos k s)$
207	169	adantl	$⊢ (φ \land k \in (1 \dots N)) \to (s \in ℂ ⟼ \cos k s) : ℂ \underset{cn}{⟶} ℂ$
208	161 100 207	fsumcncf	$⊢ φ \to (s \in ℂ ⟼ \sum_{k = 1}^{N} \cos k s) : ℂ \underset{cn}{⟶} ℂ$
209	199	recnd	$⊢ (φ \land s \in [A, B]) \to \sum_{k = 1}^{N} \cos k s \in ℂ$
210	206 208 204 161 209	cncfmptssg	$⊢ φ \to (s \in [A, B] ⟼ \sum_{k = 1}^{N} \cos k s) : [A, B] \underset{cn}{⟶} ℂ$
211	205 210	addcncf	$⊢ φ \to (s \in [A, B] ⟼ (\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s) : [A, B] \underset{cn}{⟶} ℂ$
212	183	a1i	$⊢ φ \to π \in (ℂ ∖ \{0\})$
213	204 212 181	constcncfg	$⊢ φ \to (s \in [A, B] ⟼ π) : [A, B] \underset{cn}{⟶} (ℂ ∖ \{0\})$
214	211 213	divcncf	$⊢ φ \to (s \in [A, B] ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}) : [A, B] \underset{cn}{⟶} ℂ$
215		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (s \in [A, B] ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}) : [A, B] \underset{cn}{⟶} ℂ) \to (s \in [A, B] ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}) \in 𝐿^{1}$
216	4 5 214 215	syl3anc	$⊢ φ \to (s \in [A, B] ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}) \in 𝐿^{1}$
217	189 191 203 216	iblss	$⊢ φ \to (s \in (A, B) ⟼ \frac{(\frac{1}{2}) + \sum_{k = 1}^{N} \cos k s}{π}) \in 𝐿^{1}$
218	152 217	eqeltrd	$⊢ φ \to ℝ D G \in 𝐿^{1}$
219	204 161	idcncfg	$⊢ φ \to (s \in [A, B] ⟼ s) : [A, B] \underset{cn}{⟶} ℂ$
220		2cn	$⊢ 2 \in ℂ$
221		eldifsn	$⊢ 2 \in (ℂ ∖ \{0\}) \leftrightarrow (2 \in ℂ \land 2 \neq 0)$
222	220 91 221	mpbir2an	$⊢ 2 \in (ℂ ∖ \{0\})$
223	222	a1i	$⊢ φ \to 2 \in (ℂ ∖ \{0\})$
224	204 223 181	constcncfg	$⊢ φ \to (s \in [A, B] ⟼ 2) : [A, B] \underset{cn}{⟶} (ℂ ∖ \{0\})$
225	219 224	divcncf	$⊢ φ \to (s \in [A, B] ⟼ \frac{s}{2}) : [A, B] \underset{cn}{⟶} ℂ$
226		eqid	$⊢ (s \in ℂ ⟼ \sin k s) = (s \in ℂ ⟼ \sin k s)$
227		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
228	227	a1i	$⊢ k \in (1 \dots N) \to \sin : ℂ \underset{cn}{⟶} ℂ$
229	228 168	cncfmpt1f	$⊢ k \in (1 \dots N) \to (s \in ℂ ⟼ \sin k s) : ℂ \underset{cn}{⟶} ℂ$
230	229	adantl	$⊢ (φ \land k \in (1 \dots N)) \to (s \in ℂ ⟼ \sin k s) : ℂ \underset{cn}{⟶} ℂ$
231	204	adantr	$⊢ (φ \land k \in (1 \dots N)) \to [A, B] \subseteq ℂ$
232	160	a1i	$⊢ (φ \land k \in (1 \dots N)) \to ℂ \subseteq ℂ$
233	62	ad2antlr	$⊢ ((φ \land k \in (1 \dots N)) \land s \in [A, B]) \to k \in ℂ$
234	195	recnd	$⊢ (φ \land s \in [A, B]) \to s \in ℂ$
235	234	adantlr	$⊢ ((φ \land k \in (1 \dots N)) \land s \in [A, B]) \to s \in ℂ$
236	233 235	mulcld	$⊢ ((φ \land k \in (1 \dots N)) \land s \in [A, B]) \to k s \in ℂ$
237	236	sincld	$⊢ ((φ \land k \in (1 \dots N)) \land s \in [A, B]) \to \sin k s \in ℂ$
238	226 230 231 232 237	cncfmptssg	$⊢ (φ \land k \in (1 \dots N)) \to (s \in [A, B] ⟼ \sin k s) : [A, B] \underset{cn}{⟶} ℂ$
239		eldifsn	$⊢ k \in (ℂ ∖ \{0\}) \leftrightarrow (k \in ℂ \land k \neq 0)$
240	62 73 239	sylanbrc	$⊢ k \in (1 \dots N) \to k \in (ℂ ∖ \{0\})$
241	240	adantl	$⊢ (φ \land k \in (1 \dots N)) \to k \in (ℂ ∖ \{0\})$
242		difssd	$⊢ (φ \land k \in (1 \dots N)) \to ℂ ∖ \{0\} \subseteq ℂ$
243	231 241 242	constcncfg	$⊢ (φ \land k \in (1 \dots N)) \to (s \in [A, B] ⟼ k) : [A, B] \underset{cn}{⟶} (ℂ ∖ \{0\})$
244	238 243	divcncf	$⊢ (φ \land k \in (1 \dots N)) \to (s \in [A, B] ⟼ \frac{\sin k s}{k}) : [A, B] \underset{cn}{⟶} ℂ$
245	204 100 244	fsumcncf	$⊢ φ \to (s \in [A, B] ⟼ \sum_{k = 1}^{N} (\frac{\sin k s}{k})) : [A, B] \underset{cn}{⟶} ℂ$
246	225 245	addcncf	$⊢ φ \to (s \in [A, B] ⟼ (\frac{s}{2}) + \sum_{k = 1}^{N} (\frac{\sin k s}{k})) : [A, B] \underset{cn}{⟶} ℂ$
247	246 213	divcncf	$⊢ φ \to (s \in [A, B] ⟼ \frac{(\frac{s}{2}) + \sum_{k = 1}^{N} (\frac{\sin k s}{k})}{π}) : [A, B] \underset{cn}{⟶} ℂ$
248	56 247	eqeltrid	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℂ$
249	4 5 6 187 218 248	ftc2	$⊢ φ \to \int_{(A, B)} G_{ℝ}^{'} (s) d s = G (B) - G (A)$
250	10 155 249	3eqtrd	$⊢ φ \to \int_{(A, B)} F (x) d x = G (B) - G (A)$

Metamath Proof Explorer

Theorem dirkeritg

Proof