Metamath Proof Explorer


Theorem fourierdlem16

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

Ref Expression
Hypotheses fourierdlem16.f φ F :
fourierdlem16.c C = π π
fourierdlem16.fibl φ F C 𝐿 1
fourierdlem16.a A = n 0 C F x cos n x dx π
fourierdlem16.n φ N 0
Assertion fourierdlem16 φ A N x C F x 𝐿 1 C F x cos N x dx

Proof

Step Hyp Ref Expression
1 fourierdlem16.f φ F :
2 fourierdlem16.c C = π π
3 fourierdlem16.fibl φ F C 𝐿 1
4 fourierdlem16.a A = n 0 C F x cos n x dx π
5 fourierdlem16.n φ N 0
6 1 adantr φ x C F :
7 ioossre π π
8 id x C x C
9 8 2 eleqtrdi x C x π π
10 7 9 sseldi x C x
11 10 adantl φ x C x
12 6 11 ffvelrnd φ x C F x
13 12 adantlr φ n 0 x C F x
14 nn0re n 0 n
15 14 adantr n 0 x C n
16 10 adantl n 0 x C x
17 15 16 remulcld n 0 x C n x
18 17 recoscld n 0 x C cos n x
19 18 adantll φ n 0 x C cos n x
20 13 19 remulcld φ n 0 x C F x cos n x
21 ioombl π π dom vol
22 2 21 eqeltri C dom vol
23 22 a1i φ n 0 C dom vol
24 eqidd φ n 0 x C cos n x = x C cos n x
25 eqidd φ n 0 x C F x = x C F x
26 23 19 13 24 25 offval2 φ n 0 x C cos n x × f x C F x = x C cos n x F x
27 19 recnd φ n 0 x C cos n x
28 13 recnd φ n 0 x C F x
29 27 28 mulcomd φ n 0 x C cos n x F x = F x cos n x
30 29 mpteq2dva φ n 0 x C cos n x F x = x C F x cos n x
31 26 30 eqtr2d φ n 0 x C F x cos n x = x C cos n x × f x C F x
32 coscn cos : cn
33 32 a1i n 0 cos : cn
34 2 7 eqsstri C
35 ax-resscn
36 34 35 sstri C
37 36 a1i n 0 C
38 14 recnd n 0 n
39 ssid
40 39 a1i n 0
41 37 38 40 constcncfg n 0 x C n : C cn
42 cncfmptid C x C x : C cn
43 36 39 42 mp2an x C x : C cn
44 43 a1i n 0 x C x : C cn
45 41 44 mulcncf n 0 x C n x : C cn
46 33 45 cncfmpt1f n 0 x C cos n x : C cn
47 cnmbf C dom vol x C cos n x : C cn x C cos n x MblFn
48 22 46 47 sylancr n 0 x C cos n x MblFn
49 48 adantl φ n 0 x C cos n x MblFn
50 1 feqmptd φ F = x F x
51 50 reseq1d φ F C = x F x C
52 resmpt C x F x C = x C F x
53 34 52 mp1i φ x F x C = x C F x
54 51 53 eqtr2d φ x C F x = F C
55 54 3 eqeltrd φ x C F x 𝐿 1
56 55 adantr φ n 0 x C F x 𝐿 1
57 1re 1
58 simpr n 0 y dom x C cos n x y dom x C cos n x
59 nfv x n 0
60 nfmpt1 _ x x C cos n x
61 60 nfdm _ x dom x C cos n x
62 61 nfcri x y dom x C cos n x
63 59 62 nfan x n 0 y dom x C cos n x
64 18 ex n 0 x C cos n x
65 64 adantr n 0 y dom x C cos n x x C cos n x
66 63 65 ralrimi n 0 y dom x C cos n x x C cos n x
67 dmmptg x C cos n x dom x C cos n x = C
68 66 67 syl n 0 y dom x C cos n x dom x C cos n x = C
69 58 68 eleqtrd n 0 y dom x C cos n x y C
70 eqidd n 0 y C x C cos n x = x C cos n x
71 oveq2 x = y n x = n y
72 71 fveq2d x = y cos n x = cos n y
73 72 adantl n 0 y C x = y cos n x = cos n y
74 simpr n 0 y C y C
75 14 adantr n 0 y C n
76 34 74 sseldi n 0 y C y
77 75 76 remulcld n 0 y C n y
78 77 recoscld n 0 y C cos n y
79 70 73 74 78 fvmptd n 0 y C x C cos n x y = cos n y
80 79 fveq2d n 0 y C x C cos n x y = cos n y
81 abscosbd n y cos n y 1
82 77 81 syl n 0 y C cos n y 1
83 80 82 eqbrtrd n 0 y C x C cos n x y 1
84 69 83 syldan n 0 y dom x C cos n x x C cos n x y 1
85 84 ralrimiva n 0 y dom x C cos n x x C cos n x y 1
86 breq2 b = 1 x C cos n x y b x C cos n x y 1
87 86 ralbidv b = 1 y dom x C cos n x x C cos n x y b y dom x C cos n x x C cos n x y 1
88 87 rspcev 1 y dom x C cos n x x C cos n x y 1 b y dom x C cos n x x C cos n x y b
89 57 85 88 sylancr n 0 b y dom x C cos n x x C cos n x y b
90 89 adantl φ n 0 b y dom x C cos n x x C cos n x y b
91 bddmulibl x C cos n x MblFn x C F x 𝐿 1 b y dom x C cos n x x C cos n x y b x C cos n x × f x C F x 𝐿 1
92 49 56 90 91 syl3anc φ n 0 x C cos n x × f x C F x 𝐿 1
93 31 92 eqeltrd φ n 0 x C F x cos n x 𝐿 1
94 20 93 itgrecl φ n 0 C F x cos n x dx
95 pire π
96 95 a1i φ n 0 π
97 0re 0
98 pipos 0 < π
99 97 98 gtneii π 0
100 99 a1i φ n 0 π 0
101 94 96 100 redivcld φ n 0 C F x cos n x dx π
102 101 4 fmptd φ A : 0
103 102 5 ffvelrnd φ A N
104 5 ancli φ φ N 0
105 eleq1 n = N n 0 N 0
106 105 anbi2d n = N φ n 0 φ N 0
107 simpl n = N x C n = N
108 107 oveq1d n = N x C n x = N x
109 108 fveq2d n = N x C cos n x = cos N x
110 109 oveq2d n = N x C F x cos n x = F x cos N x
111 110 itgeq2dv n = N C F x cos n x dx = C F x cos N x dx
112 111 eleq1d n = N C F x cos n x dx C F x cos N x dx
113 106 112 imbi12d n = N φ n 0 C F x cos n x dx φ N 0 C F x cos N x dx
114 113 94 vtoclg N 0 φ N 0 C F x cos N x dx
115 5 104 114 sylc φ C F x cos N x dx
116 103 55 115 jca31 φ A N x C F x 𝐿 1 C F x cos N x dx