fourierdlem22

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

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

Proof

Step	Hyp	Ref	Expression
1		fourierdlem22.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem22.c	$⊢ C = (- π, π)$
3		fourierdlem22.fibl	$⊢ φ \to {F ↾}_{C} \in 𝐿^{1}$
4		fourierdlem22.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{C} F (x) \cos n x d x}{π})$
5		fourierdlem22.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{C} F (x) \sin n x d x}{π})$
6	1	adantr	$⊢ (φ \land x \in C) \to F : ℝ ⟶ ℝ$
7		ioossre	$⊢ (- π, π) \subseteq ℝ$
8		id	$⊢ x \in C \to x \in C$
9	8 2	eleqtrdi	$⊢ x \in C \to x \in (- π, π)$
10	7 9	sselid	$⊢ x \in C \to x \in ℝ$
11	10	adantl	$⊢ (φ \land x \in C) \to x \in ℝ$
12	6 11	ffvelcdmd	$⊢ (φ \land x \in C) \to F (x) \in ℝ$
13	12	adantlr	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to F (x) \in ℝ$
14		nn0re	$⊢ n \in ℕ_{0} \to n \in ℝ$
15	14	adantr	$⊢ (n \in ℕ_{0} \land x \in C) \to n \in ℝ$
16	10	adantl	$⊢ (n \in ℕ_{0} \land x \in C) \to x \in ℝ$
17	15 16	remulcld	$⊢ (n \in ℕ_{0} \land x \in C) \to n x \in ℝ$
18	17	recoscld	$⊢ (n \in ℕ_{0} \land x \in C) \to \cos n x \in ℝ$
19	18	adantll	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to \cos n x \in ℝ$
20	13 19	remulcld	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to F (x) \cos n x \in ℝ$
21		ioombl	$⊢ (- π, π) \in dom vol$
22	2 21	eqeltri	$⊢ C \in dom vol$
23	22	a1i	$⊢ (φ \land n \in ℕ_{0}) \to C \in dom vol$
24		eqidd	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \cos n x) = (x \in C ⟼ \cos n x)$
25		eqidd	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ F (x)) = (x \in C ⟼ F (x))$
26	23 19 13 24 25	offval2	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \cos n x) \times_{f} (x \in C ⟼ F (x)) = (x \in C ⟼ \cos n x F (x))$
27	19	recnd	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to \cos n x \in ℂ$
28	13	recnd	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to F (x) \in ℂ$
29	27 28	mulcomd	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to \cos n x F (x) = F (x) \cos n x$
30	29	mpteq2dva	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \cos n x F (x)) = (x \in C ⟼ F (x) \cos n x)$
31	26 30	eqtr2d	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ F (x) \cos n x) = (x \in C ⟼ \cos n x) \times_{f} (x \in C ⟼ F (x))$
32		coscn	$⊢ \cos : ℂ \underset{cn}{⟶} ℂ$
33	32	a1i	$⊢ n \in ℕ_{0} \to \cos : ℂ \underset{cn}{⟶} ℂ$
34	2 7	eqsstri	$⊢ C \subseteq ℝ$
35		ax-resscn	$⊢ ℝ \subseteq ℂ$
36	34 35	sstri	$⊢ C \subseteq ℂ$
37	36	a1i	$⊢ n \in ℕ_{0} \to C \subseteq ℂ$
38	14	recnd	$⊢ n \in ℕ_{0} \to n \in ℂ$
39		ssid	$⊢ ℂ \subseteq ℂ$
40	39	a1i	$⊢ n \in ℕ_{0} \to ℂ \subseteq ℂ$
41	37 38 40	constcncfg	$⊢ n \in ℕ_{0} \to (x \in C ⟼ n) : C \underset{cn}{⟶} ℂ$
42		cncfmptid	$⊢ (C \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in C ⟼ x) : C \underset{cn}{⟶} ℂ$
43	36 39 42	mp2an	$⊢ (x \in C ⟼ x) : C \underset{cn}{⟶} ℂ$
44	43	a1i	$⊢ n \in ℕ_{0} \to (x \in C ⟼ x) : C \underset{cn}{⟶} ℂ$
45	41 44	mulcncf	$⊢ n \in ℕ_{0} \to (x \in C ⟼ n x) : C \underset{cn}{⟶} ℂ$
46	33 45	cncfmpt1f	$⊢ n \in ℕ_{0} \to (x \in C ⟼ \cos n x) : C \underset{cn}{⟶} ℂ$
47		cnmbf	$⊢ (C \in dom vol \land (x \in C ⟼ \cos n x) : C \underset{cn}{⟶} ℂ) \to (x \in C ⟼ \cos n x) \in MblFn$
48	22 46 47	sylancr	$⊢ n \in ℕ_{0} \to (x \in C ⟼ \cos n x) \in MblFn$
49	48	adantl	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \cos n x) \in MblFn$
50	1	feqmptd	$⊢ φ \to F = (x \in ℝ ⟼ F (x))$
51	50	reseq1d	$⊢ φ \to {F ↾}_{C} = {(x \in ℝ ⟼ F (x)) ↾}_{C}$
52		resmpt	$⊢ C \subseteq ℝ \to {(x \in ℝ ⟼ F (x)) ↾}_{C} = (x \in C ⟼ F (x))$
53	34 52	mp1i	$⊢ φ \to {(x \in ℝ ⟼ F (x)) ↾}_{C} = (x \in C ⟼ F (x))$
54	51 53	eqtr2d	$⊢ φ \to (x \in C ⟼ F (x)) = {F ↾}_{C}$
55	54 3	eqeltrd	$⊢ φ \to (x \in C ⟼ F (x)) \in 𝐿^{1}$
56	55	adantr	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ F (x)) \in 𝐿^{1}$
57		1re	$⊢ 1 \in ℝ$
58		simpr	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \cos n x)) \to y \in dom (x \in C ⟼ \cos n x)$
59		nfv	$⊢ Ⅎ x n \in ℕ_{0}$
60		nfmpt1	$⊢ \underline{Ⅎ} x (x \in C ⟼ \cos n x)$
61	60	nfdm	$⊢ \underline{Ⅎ} x dom (x \in C ⟼ \cos n x)$
62	61	nfcri	$⊢ Ⅎ x y \in dom (x \in C ⟼ \cos n x)$
63	59 62	nfan	$⊢ Ⅎ x (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \cos n x))$
64	18	ex	$⊢ n \in ℕ_{0} \to (x \in C \to \cos n x \in ℝ)$
65	64	adantr	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \cos n x)) \to (x \in C \to \cos n x \in ℝ)$
66	63 65	ralrimi	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \cos n x)) \to \forall x \in C \cos n x \in ℝ$
67		dmmptg	$⊢ \forall x \in C \cos n x \in ℝ \to dom (x \in C ⟼ \cos n x) = C$
68	66 67	syl	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \cos n x)) \to dom (x \in C ⟼ \cos n x) = C$
69	58 68	eleqtrd	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \cos n x)) \to y \in C$
70		eqidd	$⊢ (n \in ℕ_{0} \land y \in C) \to (x \in C ⟼ \cos n x) = (x \in C ⟼ \cos n x)$
71		oveq2	$⊢ x = y \to n x = n y$
72	71	fveq2d	$⊢ x = y \to \cos n x = \cos n y$
73	72	adantl	$⊢ ((n \in ℕ_{0} \land y \in C) \land x = y) \to \cos n x = \cos n y$
74		simpr	$⊢ (n \in ℕ_{0} \land y \in C) \to y \in C$
75	14	adantr	$⊢ (n \in ℕ_{0} \land y \in C) \to n \in ℝ$
76	34 74	sselid	$⊢ (n \in ℕ_{0} \land y \in C) \to y \in ℝ$
77	75 76	remulcld	$⊢ (n \in ℕ_{0} \land y \in C) \to n y \in ℝ$
78	77	recoscld	$⊢ (n \in ℕ_{0} \land y \in C) \to \cos n y \in ℝ$
79	70 73 74 78	fvmptd	$⊢ (n \in ℕ_{0} \land y \in C) \to (x \in C ⟼ \cos n x) (y) = \cos n y$
80	79	fveq2d	$⊢ (n \in ℕ_{0} \land y \in C) \to \|(x \in C ⟼ \cos n x) (y)\| = \|\cos n y\|$
81		abscosbd	$⊢ n y \in ℝ \to \|\cos n y\| \leq 1$
82	77 81	syl	$⊢ (n \in ℕ_{0} \land y \in C) \to \|\cos n y\| \leq 1$
83	80 82	eqbrtrd	$⊢ (n \in ℕ_{0} \land y \in C) \to \|(x \in C ⟼ \cos n x) (y)\| \leq 1$
84	69 83	syldan	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \cos n x)) \to \|(x \in C ⟼ \cos n x) (y)\| \leq 1$
85	84	ralrimiva	$⊢ n \in ℕ_{0} \to \forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq 1$
86		breq2	$⊢ b = 1 \to (\|(x \in C ⟼ \cos n x) (y)\| \leq b \leftrightarrow \|(x \in C ⟼ \cos n x) (y)\| \leq 1)$
87	86	ralbidv	$⊢ b = 1 \to (\forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq b \leftrightarrow \forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq 1)$
88	87	rspcev	$⊢ (1 \in ℝ \land \forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq 1) \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq b$
89	57 85 88	sylancr	$⊢ n \in ℕ_{0} \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq b$
90	89	adantl	$⊢ (φ \land n \in ℕ_{0}) \to \exists b \in ℝ \forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq b$
91		bddmulibl	$⊢ ((x \in C ⟼ \cos n x) \in MblFn \land (x \in C ⟼ F (x)) \in 𝐿^{1} \land \exists b \in ℝ \forall y \in dom (x \in C ⟼ \cos n x) \|(x \in C ⟼ \cos n x) (y)\| \leq b) \to (x \in C ⟼ \cos n x) \times_{f} (x \in C ⟼ F (x)) \in 𝐿^{1}$
92	49 56 90 91	syl3anc	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \cos n x) \times_{f} (x \in C ⟼ F (x)) \in 𝐿^{1}$
93	31 92	eqeltrd	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ F (x) \cos n x) \in 𝐿^{1}$
94	20 93	itgrecl	$⊢ (φ \land n \in ℕ_{0}) \to \int_{C} F (x) \cos n x d x \in ℝ$
95		pire	$⊢ π \in ℝ$
96	95	a1i	$⊢ (φ \land n \in ℕ_{0}) \to π \in ℝ$
97		0re	$⊢ 0 \in ℝ$
98		pipos	$⊢ 0 < π$
99	97 98	gtneii	$⊢ π \neq 0$
100	99	a1i	$⊢ (φ \land n \in ℕ_{0}) \to π \neq 0$
101	94 96 100	redivcld	$⊢ (φ \land n \in ℕ_{0}) \to \frac{\int_{C} F (x) \cos n x d x}{π} \in ℝ$
102	101 4	fmptd	$⊢ φ \to A : ℕ_{0} ⟶ ℝ$
103	102	ffvelcdmda	$⊢ (φ \land n \in ℕ_{0}) \to A (n) \in ℝ$
104	103	ex	$⊢ φ \to (n \in ℕ_{0} \to A (n) \in ℝ)$
105		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
106	17	resincld	$⊢ (n \in ℕ_{0} \land x \in C) \to \sin n x \in ℝ$
107	106	adantll	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to \sin n x \in ℝ$
108	13 107	remulcld	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to F (x) \sin n x \in ℝ$
109		eqidd	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \sin n x) = (x \in C ⟼ \sin n x)$
110	23 107 13 109 25	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))$
111	107	recnd	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to \sin n x \in ℂ$
112	111 28	mulcomd	$⊢ ((φ \land n \in ℕ_{0}) \land x \in C) \to \sin n x F (x) = F (x) \sin n x$
113	112	mpteq2dva	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \sin n x F (x)) = (x \in C ⟼ F (x) \sin n x)$
114	110 113	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))$
115		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
116	115	a1i	$⊢ (φ \land n \in ℕ_{0}) \to \sin : ℂ \underset{cn}{⟶} ℂ$
117	45	adantl	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ n x) : C \underset{cn}{⟶} ℂ$
118	116 117	cncfmpt1f	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \sin n x) : C \underset{cn}{⟶} ℂ$
119		cnmbf	$⊢ (C \in dom vol \land (x \in C ⟼ \sin n x) : C \underset{cn}{⟶} ℂ) \to (x \in C ⟼ \sin n x) \in MblFn$
120	22 118 119	sylancr	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \sin n x) \in MblFn$
121		simpr	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \sin n x)) \to y \in dom (x \in C ⟼ \sin n x)$
122		nfmpt1	$⊢ \underline{Ⅎ} x (x \in C ⟼ \sin n x)$
123	122	nfdm	$⊢ \underline{Ⅎ} x dom (x \in C ⟼ \sin n x)$
124	123	nfcri	$⊢ Ⅎ x y \in dom (x \in C ⟼ \sin n x)$
125	59 124	nfan	$⊢ Ⅎ x (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \sin n x))$
126	106	ex	$⊢ n \in ℕ_{0} \to (x \in C \to \sin n x \in ℝ)$
127	126	adantr	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \sin n x)) \to (x \in C \to \sin n x \in ℝ)$
128	125 127	ralrimi	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \sin n x)) \to \forall x \in C \sin n x \in ℝ$
129		dmmptg	$⊢ \forall x \in C \sin n x \in ℝ \to dom (x \in C ⟼ \sin n x) = C$
130	128 129	syl	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \sin n x)) \to dom (x \in C ⟼ \sin n x) = C$
131	121 130	eleqtrd	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \sin n x)) \to y \in C$
132		eqidd	$⊢ (n \in ℕ_{0} \land y \in C) \to (x \in C ⟼ \sin n x) = (x \in C ⟼ \sin n x)$
133	71	fveq2d	$⊢ x = y \to \sin n x = \sin n y$
134	133	adantl	$⊢ ((n \in ℕ_{0} \land y \in C) \land x = y) \to \sin n x = \sin n y$
135	77	resincld	$⊢ (n \in ℕ_{0} \land y \in C) \to \sin n y \in ℝ$
136	132 134 74 135	fvmptd	$⊢ (n \in ℕ_{0} \land y \in C) \to (x \in C ⟼ \sin n x) (y) = \sin n y$
137	136	fveq2d	$⊢ (n \in ℕ_{0} \land y \in C) \to \|(x \in C ⟼ \sin n x) (y)\| = \|\sin n y\|$
138		abssinbd	$⊢ n y \in ℝ \to \|\sin n y\| \leq 1$
139	77 138	syl	$⊢ (n \in ℕ_{0} \land y \in C) \to \|\sin n y\| \leq 1$
140	137 139	eqbrtrd	$⊢ (n \in ℕ_{0} \land y \in C) \to \|(x \in C ⟼ \sin n x) (y)\| \leq 1$
141	131 140	syldan	$⊢ (n \in ℕ_{0} \land y \in dom (x \in C ⟼ \sin n x)) \to \|(x \in C ⟼ \sin n x) (y)\| \leq 1$
142	141	ralrimiva	$⊢ n \in ℕ_{0} \to \forall y \in dom (x \in C ⟼ \sin n x) \|(x \in C ⟼ \sin n x) (y)\| \leq 1$
143		breq2	$⊢ b = 1 \to (\|(x \in C ⟼ \sin n x) (y)\| \leq b \leftrightarrow \|(x \in C ⟼ \sin n x) (y)\| \leq 1)$
144	143	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)$
145	144	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$
146	57 142 145	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$
147	146	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$
148		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}$
149	120 56 147 148	syl3anc	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ \sin n x) \times_{f} (x \in C ⟼ F (x)) \in 𝐿^{1}$
150	114 149	eqeltrd	$⊢ (φ \land n \in ℕ_{0}) \to (x \in C ⟼ F (x) \sin n x) \in 𝐿^{1}$
151	108 150	itgrecl	$⊢ (φ \land n \in ℕ_{0}) \to \int_{C} F (x) \sin n x d x \in ℝ$
152	105 151	sylan2	$⊢ (φ \land n \in ℕ) \to \int_{C} F (x) \sin n x d x \in ℝ$
153	95	a1i	$⊢ (φ \land n \in ℕ) \to π \in ℝ$
154	99	a1i	$⊢ (φ \land n \in ℕ) \to π \neq 0$
155	152 153 154	redivcld	$⊢ (φ \land n \in ℕ) \to \frac{\int_{C} F (x) \sin n x d x}{π} \in ℝ$
156	155 5	fmptd	$⊢ φ \to B : ℕ ⟶ ℝ$
157	156	ffvelcdmda	$⊢ (φ \land n \in ℕ) \to B (n) \in ℝ$
158	157	ex	$⊢ φ \to (n \in ℕ \to B (n) \in ℝ)$
159	104 158	jca	$⊢ φ \to ((n \in ℕ_{0} \to A (n) \in ℝ) \land (n \in ℕ \to B (n) \in ℝ))$

Metamath Proof Explorer

Theorem fourierdlem22

Proof