fourierdlem16

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

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

Proof

Step	Hyp	Ref	Expression
1		fourierdlem16.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem16.c	$⊢ C = (- π, π)$
3		fourierdlem16.fibl	$⊢ φ \to {F ↾}_{C} \in 𝐿^{1}$
4		fourierdlem16.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{C} F (x) \cos n x d x}{π})$
5		fourierdlem16.n	$⊢ φ \to N \in ℕ_{0}$
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	sseldi	$⊢ x \in C \to x \in ℝ$
11	10	adantl	$⊢ (φ \land x \in C) \to x \in ℝ$
12	6 11	ffvelrnd	$⊢ (φ \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	sseldi	$⊢ (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 5	ffvelrnd	$⊢ φ \to A (N) \in ℝ$
104	5	ancli	$⊢ φ \to (φ \land 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 \cos n x = \cos N x$
110	109	oveq2d	$⊢ (n = N \land x \in C) \to F (x) \cos n x = F (x) \cos N x$
111	110	itgeq2dv	$⊢ n = N \to \int_{C} F (x) \cos n x d x = \int_{C} F (x) \cos N x d x$
112	111	eleq1d	$⊢ n = N \to (\int_{C} F (x) \cos n x d x \in ℝ \leftrightarrow \int_{C} F (x) \cos N x d x \in ℝ)$
113	106 112	imbi12d	$⊢ n = N \to (((φ \land n \in ℕ_{0}) \to \int_{C} F (x) \cos n x d x \in ℝ) \leftrightarrow ((φ \land N \in ℕ_{0}) \to \int_{C} F (x) \cos N x d x \in ℝ))$
114	113 94	vtoclg	$⊢ N \in ℕ_{0} \to ((φ \land N \in ℕ_{0}) \to \int_{C} F (x) \cos N x d x \in ℝ)$
115	5 104 114	sylc	$⊢ φ \to \int_{C} F (x) \cos N x d x \in ℝ$
116	103 55 115	jca31	$⊢ φ \to ((A (N) \in ℝ \land (x \in C ⟼ F (x)) \in 𝐿^{1}) \land \int_{C} F (x) \cos N x d x \in ℝ)$

Metamath Proof Explorer

Theorem fourierdlem16

Proof