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 ) )