This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> F : RR --> RR )
fourierdlem16.c 
|- C = ( -u _pi (,) _pi )
fourierdlem16.fibl 
|- ( ph -> ( F |` C ) e. L^1 )
fourierdlem16.a 
|- A = ( n e. NN0 |-> ( S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
fourierdlem16.n 
|- ( ph -> N e. NN0 )
Assertion fourierdlem16 
|- ( ph -> ( ( ( A ` N ) e. RR /\ ( x e. C |-> ( F ` x ) ) e. L^1 ) /\ S. C ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x e. RR ) )

Proof

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