Metamath Proof Explorer

Theorem fourierdlem21

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

Ref Expression
Hypotheses fourierdlem21.f 
|- ( ph -> F : RR --> RR )
fourierdlem21.c 
|- C = ( -u _pi (,) _pi )
fourierdlem21.fibl 
|- ( ph -> ( F |` C ) e. L^1 )
fourierdlem21.b 
|- B = ( n e. NN |-> ( S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
fourierdlem21.n 
|- ( ph -> N e. NN )
Assertion fourierdlem21 
|- ( ph -> ( ( ( B ` N ) e. RR /\ ( x e. C |-> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) ) e. L^1 ) /\ S. C ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x e. RR ) )

Proof

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