fourierdlem21

Description: The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem21.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem21.c	$⊢ C = (- π, π)$
	fourierdlem21.fibl	$⊢ φ \to {F ↾}_{C} \in 𝐿^{1}$
	fourierdlem21.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{C} F (x) \sin n x d x}{π})$
	fourierdlem21.n	$⊢ φ \to N \in ℕ$
Assertion	fourierdlem21	$⊢ φ \to ((B (N) \in ℝ \land (x \in C ⟼ F (x) \sin N x) \in 𝐿^{1}) \land \int_{C} F (x) \sin N x d x \in ℝ)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem21.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem21.c	$⊢ C = (- π, π)$
3		fourierdlem21.fibl	$⊢ φ \to {F ↾}_{C} \in 𝐿^{1}$
4		fourierdlem21.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{C} F (x) \sin n x d x}{π})$
5		fourierdlem21.n	$⊢ φ \to N \in ℕ$
6		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
7	1	adantr	$⊢ (φ \land x \in C) \to F : ℝ ⟶ ℝ$
8		ioossre	$⊢ (- π, π) \subseteq ℝ$
9		id	$⊢ x \in C \to x \in C$
10	9 2	eleqtrdi	$⊢ x \in C \to x \in (- π, π)$
11	8 10	sseldi	$⊢ x \in C \to x \in ℝ$
12	11	adantl	$⊢ (φ \land x \in C) \to x \in ℝ$
13	7 12	ffvelrnd	$⊢ (φ \land x \in C) \to F (x) \in ℝ$
14	13	adantlr	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to F (x) \in ℝ$
15		nn0re	$⊢ n \in ℕ_{0} \to n \in ℝ$
16	15	adantr	$⊢ (n \in ℕ_{0} \land x \in C) \to n \in ℝ$
17	11	adantl	$⊢ (n \in ℕ_{0} \land x \in C) \to x \in ℝ$
18	16 17	remulcld	$⊢ (n \in ℕ_{0} \land x \in C) \to n x \in ℝ$
19	18	resincld	$⊢ (n \in ℕ_{0} \land x \in C) \to \sin n x \in ℝ$
20	19	adantll	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to \sin n x \in ℝ$
21	14 20	remulcld	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to F (x) \sin n x \in ℝ$
22		ioombl	$⊢ (- π, π) \in dom vol$
23	2 22	eqeltri	$⊢ C \in dom vol$
24	23	a1i	$⊢ (φ \land n \in ℕ_{0}) \to C \in dom vol$
25		eqidd	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \sin n x) = (x \in C ⟼ \sin n x)$
26		eqidd	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ F (x)) = (x \in C ⟼ F (x))$
27	24 20 14 25 26	offval2	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \sin n x) \times_{f} (x \in C ⟼ F (x)) = (x \in C ⟼ \sin n x F (x))$
28	20	recnd	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to \sin n x \in ℂ$
29	14	recnd	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to F (x) \in ℂ$
30	28 29	mulcomd	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to \sin n x F (x) = F (x) \sin n x$
31	30	mpteq2dva	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \sin n x F (x)) = (x \in C ⟼ F (x) \sin n x)$
32	27 31	eqtr2d	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ F (x) \sin n x) = (x \in C ⟼ \sin n x) \times_{f} (x \in C ⟼ F (x))$
33		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
34	33	a1i	$⊢ (φ \land n \in ℕ_{0}) \to \sin : ℂ \underset{cn}{⟶} ℂ$
35	2 8	eqsstri	$⊢ C \subseteq ℝ$
36		ax-resscn	$⊢ ℝ \subseteq ℂ$
37	35 36	sstri	$⊢ C \subseteq ℂ$
38	37	a1i	$⊢ n \in ℕ_{0} \to C \subseteq ℂ$
39	15	recnd	$⊢ n \in ℕ_{0} \to n \in ℂ$
40		ssid	$⊢ ℂ \subseteq ℂ$
41	40	a1i	$⊢ n \in ℕ_{0} \to ℂ \subseteq ℂ$
42	38 39 41	constcncfg	$⊢ n \in ℕ_{0} \to (x \in C ⟼ n) : C \underset{cn}{⟶} ℂ$
43	38 41	idcncfg	$⊢ n \in ℕ_{0} \to (x \in C ⟼ x) : C \underset{cn}{⟶} ℂ$
44	42 43	mulcncf	$⊢ n \in ℕ_{0} \to (x \in C ⟼ n x) : C \underset{cn}{⟶} ℂ$
45	44	adantl	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ n x) : C \underset{cn}{⟶} ℂ$
46	34 45	cncfmpt1f	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \sin n x) : C \underset{cn}{⟶} ℂ$
47		cnmbf	$⊢ (C \in dom vol \land (x \in C ⟼ \sin n x) : C \underset{cn}{⟶} ℂ) \to (x \in C ⟼ \sin n x) \in MblFn$
48	23 46 47	sylancr	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \sin n x) \in MblFn$
49	1	feqmptd	$⊢ φ \to F = (x \in ℝ ⟼ F (x))$
50	49	reseq1d	$⊢ φ \to {F ↾}_{C} = {(x \in ℝ ⟼ F (x)) ↾}_{C}$
51		resmpt	$⊢ C \subseteq ℝ \to {(x \in ℝ ⟼ F (x)) ↾}_{C} = (x \in C ⟼ F (x))$
52	35 51	mp1i	$⊢ φ \to {(x \in ℝ ⟼ F (x)) ↾}_{C} = (x \in C ⟼ F (x))$
53	50 52	eqtr2d	$⊢ φ \to (x \in C ⟼ F (x)) = {F ↾}_{C}$
54	53 3	eqeltrd	$⊢ φ \to (x \in C ⟼ F (x)) \in 𝐿^{1}$
55	54	adantr	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ F (x)) \in 𝐿^{1}$
56		1re	$⊢ 1 \in ℝ$
57		simpr	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \sin n x)) \to y \in dom (x \in C ⟼ \sin n x)$
58		nfv	$⊢ Ⅎ x n \in ℕ_{0}$
59		nfmpt1	$⊢ \underline{Ⅎ} x (x \in C ⟼ \sin n x)$
60	59	nfdm	$⊢ \underline{Ⅎ} x dom (x \in C ⟼ \sin n x)$
61	60	nfcri	$⊢ Ⅎ x y \in dom (x \in C ⟼ \sin n x)$
62	58 61	nfan	$⊢ Ⅎ x (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \sin n x))$
63	19	ex	$⊢ n \in ℕ_{0} \to (x \in C \to \sin n x \in ℝ)$
64	63	adantr	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \sin n x)) \to (x \in C \to \sin n x \in ℝ)$
65	62 64	ralrimi	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \sin n x)) \to \forall x \in C \sin n x \in ℝ$
66		dmmptg	$⊢ \forall x \in C \sin n x \in ℝ \to dom (x \in C ⟼ \sin n x) = C$
67	65 66	syl	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \sin n x)) \to dom (x \in C ⟼ \sin n x) = C$
68	57 67	eleqtrd	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \sin n x)) \to y \in C$
69		eqidd	$⊢ (n \in ℕ_{0} \land y \in C) \to (x \in C ⟼ \sin n x) = (x \in C ⟼ \sin n x)$
70		oveq2	$⊢ x = y \to n x = n y$
71	70	fveq2d	$⊢ x = y \to \sin n x = \sin n y$
72	71	adantl	$⊢ ((n \in ℕ_{0} \land y \in C) \land x = y) \to \sin n x = \sin n y$
73		simpr	$⊢ (n \in ℕ_{0} \land y \in C) \to y \in C$
74	15	adantr	$⊢ (n \in ℕ_{0} \land y \in C) \to n \in ℝ$
75	35 73	sseldi	$⊢ (n \in ℕ_{0} \land y \in C) \to y \in ℝ$
76	74 75	remulcld	$⊢ (n \in ℕ_{0} \land y \in C) \to n y \in ℝ$
77	76	resincld	$⊢ (n \in ℕ_{0} \land y \in C) \to \sin n y \in ℝ$
78	69 72 73 77	fvmptd	$⊢ (n \in ℕ_{0} \land y \in C) \to (x \in C ⟼ \sin n x) (y) = \sin n y$
79	78	fveq2d	$⊢ (n \in ℕ_{0} \land y \in C) \to \|(x \in C ⟼ \sin n x) (y)\| = \|\sin n y\|$
80		abssinbd	$⊢ n y \in ℝ \to \|\sin n y\| \leq 1$
81	76 80	syl	$⊢ (n \in ℕ_{0} \land y \in C) \to \|\sin n y\| \leq 1$
82	79 81	eqbrtrd	$⊢ (n \in ℕ_{0} \land y \in C) \to \|(x \in C ⟼ \sin n x) (y)\| \leq 1$
83	68 82	syldan	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \sin n x)) \to \|(x \in C ⟼ \sin n x) (y)\| \leq 1$
84	83	ralrimiva	$⊢ n \in ℕ_{0} \to \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq 1$
85		breq2	$⊢ b = 1 \to (\|(x \in C ⟼ \sin n x) (y)\| \leq b \leftrightarrow \|(x \in C ⟼ \sin n x) (y)\| \leq 1)$
86	85	ralbidv	$⊢ b = 1 \to (\forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq b \leftrightarrow \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq 1)$
87	86	rspcev	$⊢ (1 \in ℝ \land \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq 1) \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq b$
88	56 84 87	sylancr	$⊢ n \in ℕ_{0} \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq b$
89	88	adantl	$⊢ (φ \land n \in ℕ_{0}) \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq b$
90		bddmulibl	$⊢ ((x \in C ⟼ \sin n x) \in MblFn \land (x \in C ⟼ F (x)) \in 𝐿^{1} \land \exists b \in ℝ \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq b) \to (x \in C ⟼ \sin n x) \times_{f} (x \in C ⟼ F (x)) \in 𝐿^{1}$
91	48 55 89 90	syl3anc	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \sin n x) \times_{f} (x \in C ⟼ F (x)) \in 𝐿^{1}$
92	32 91	eqeltrd	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ F (x) \sin n x) \in 𝐿^{1}$
93	21 92	itgrecl	$⊢ (φ \land n \in ℕ_{0}) \to \int_{C} F (x) \sin n x d x \in ℝ$
94	6 93	sylan2	$⊢ (φ \land n \in ℕ) \to \int_{C} F (x) \sin n x d x \in ℝ$
95		pire	$⊢ π \in ℝ$
96	95	a1i	$⊢ (φ \land n \in ℕ) \to π \in ℝ$
97		0re	$⊢ 0 \in ℝ$
98		pipos	$⊢ 0 < π$
99	97 98	gtneii	$⊢ π \neq 0$
100	99	a1i	$⊢ (φ \land n \in ℕ) \to π \neq 0$
101	94 96 100	redivcld	$⊢ (φ \land n \in ℕ) \to \frac{\int_{C} F (x) \sin n x d x}{π} \in ℝ$
102	101 4	fmptd	$⊢ φ \to B : ℕ ⟶ ℝ$
103	102 5	ffvelrnd	$⊢ φ \to B (N) \in ℝ$
104	5	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
105		eleq1	$⊢ n = N \to (n \in ℕ_{0} \leftrightarrow N \in ℕ_{0})$
106	105	anbi2d	$⊢ n = N \to ((φ \land n \in ℕ_{0}) \leftrightarrow (φ \land N \in ℕ_{0}))$
107		simpl	$⊢ (n = N \land x \in C) \to n = N$
108	107	oveq1d	$⊢ (n = N \land x \in C) \to n x = N x$
109	108	fveq2d	$⊢ (n = N \land x \in C) \to \sin n x = \sin N x$
110	109	oveq2d	$⊢ (n = N \land x \in C) \to F (x) \sin n x = F (x) \sin N x$
111	110	mpteq2dva	$⊢ n = N \to (x \in C ⟼ F (x) \sin n x) = (x \in C ⟼ F (x) \sin N x)$
112	111	eleq1d	$⊢ n = N \to ((x \in C ⟼ F (x) \sin n x) \in 𝐿^{1} \leftrightarrow (x \in C ⟼ F (x) \sin N x) \in 𝐿^{1})$
113	106 112	imbi12d	$⊢ n = N \to (((φ \land n \in ℕ_{0}) \to (x \in C ⟼ F (x) \sin n x) \in 𝐿^{1}) \leftrightarrow ((φ \land N \in ℕ_{0}) \to (x \in C ⟼ F (x) \sin N x) \in 𝐿^{1}))$
114	113 92	vtoclg	$⊢ N \in ℕ_{0} \to ((φ \land N \in ℕ_{0}) \to (x \in C ⟼ F (x) \sin N x) \in 𝐿^{1})$
115	114	anabsi7	$⊢ (φ \land N \in ℕ_{0}) \to (x \in C ⟼ F (x) \sin N x) \in 𝐿^{1}$
116	104 115	mpdan	$⊢ φ \to (x \in C ⟼ F (x) \sin N x) \in 𝐿^{1}$
117	5	ancli	$⊢ φ \to (φ \land N \in ℕ)$
118		eleq1	$⊢ n = N \to (n \in ℕ \leftrightarrow N \in ℕ)$
119	118	anbi2d	$⊢ n = N \to ((φ \land n \in ℕ) \leftrightarrow (φ \land N \in ℕ))$
120	110	itgeq2dv	$⊢ n = N \to \int_{C} F (x) \sin n x d x = \int_{C} F (x) \sin N x d x$
121	120	eleq1d	$⊢ n = N \to (\int_{C} F (x) \sin n x d x \in ℝ \leftrightarrow \int_{C} F (x) \sin N x d x \in ℝ)$
122	119 121	imbi12d	$⊢ n = N \to (((φ \land n \in ℕ) \to \int_{C} F (x) \sin n x d x \in ℝ) \leftrightarrow ((φ \land N \in ℕ) \to \int_{C} F (x) \sin N x d x \in ℝ))$
123	122 94	vtoclg	$⊢ N \in ℕ \to ((φ \land N \in ℕ) \to \int_{C} F (x) \sin N x d x \in ℝ)$
124	5 117 123	sylc	$⊢ φ \to \int_{C} F (x) \sin N x d x \in ℝ$
125	103 116 124	jca31	$⊢ φ \to ((B (N) \in ℝ \land (x \in C ⟼ F (x) \sin N x) \in 𝐿^{1}) \land \int_{C} F (x) \sin N x d x \in ℝ)$

Metamath Proof Explorer

Theorem fourierdlem21

Proof