Metamath Proof Explorer


Theorem fourierdlem22

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

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

Proof

Step Hyp Ref Expression
1 fourierdlem22.f
 |-  ( ph -> F : RR --> RR )
2 fourierdlem22.c
 |-  C = ( -u _pi (,) _pi )
3 fourierdlem22.fibl
 |-  ( ph -> ( F |` C ) e. L^1 )
4 fourierdlem22.a
 |-  A = ( n e. NN0 |-> ( S. C ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
5 fourierdlem22.b
 |-  B = ( n e. NN |-> ( S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
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 ffvelrnd
 |-  ( ( 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 ffvelrnda
 |-  ( ( ph /\ n e. NN0 ) -> ( A ` n ) e. RR )
104 103 ex
 |-  ( ph -> ( n e. NN0 -> ( A ` n ) e. RR ) )
105 nnnn0
 |-  ( n e. NN -> n e. NN0 )
106 17 resincld
 |-  ( ( n e. NN0 /\ x e. C ) -> ( sin ` ( n x. x ) ) e. RR )
107 106 adantll
 |-  ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( sin ` ( n x. x ) ) e. RR )
108 13 107 remulcld
 |-  ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) e. RR )
109 eqidd
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( sin ` ( n x. x ) ) ) = ( x e. C |-> ( sin ` ( n x. x ) ) ) )
110 23 107 13 109 25 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 ) ) ) )
111 107 recnd
 |-  ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( sin ` ( n x. x ) ) e. CC )
112 111 28 mulcomd
 |-  ( ( ( ph /\ n e. NN0 ) /\ x e. C ) -> ( ( sin ` ( n x. x ) ) x. ( F ` x ) ) = ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) )
113 112 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 ) ) ) ) )
114 110 113 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 ) ) ) )
115 sincn
 |-  sin e. ( CC -cn-> CC )
116 115 a1i
 |-  ( ( ph /\ n e. NN0 ) -> sin e. ( CC -cn-> CC ) )
117 45 adantl
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( n x. x ) ) e. ( C -cn-> CC ) )
118 116 117 cncfmpt1f
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( sin ` ( n x. x ) ) ) e. ( C -cn-> CC ) )
119 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 )
120 22 118 119 sylancr
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( sin ` ( n x. x ) ) ) e. MblFn )
121 simpr
 |-  ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) ) ) -> y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) ) )
122 nfmpt1
 |-  F/_ x ( x e. C |-> ( sin ` ( n x. x ) ) )
123 122 nfdm
 |-  F/_ x dom ( x e. C |-> ( sin ` ( n x. x ) ) )
124 123 nfcri
 |-  F/ x y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) )
125 59 124 nfan
 |-  F/ x ( n e. NN0 /\ y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) ) )
126 106 ex
 |-  ( n e. NN0 -> ( x e. C -> ( sin ` ( n x. x ) ) e. RR ) )
127 126 adantr
 |-  ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) ) ) -> ( x e. C -> ( sin ` ( n x. x ) ) e. RR ) )
128 125 127 ralrimi
 |-  ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) ) ) -> A. x e. C ( sin ` ( n x. x ) ) e. RR )
129 dmmptg
 |-  ( A. x e. C ( sin ` ( n x. x ) ) e. RR -> dom ( x e. C |-> ( sin ` ( n x. x ) ) ) = C )
130 128 129 syl
 |-  ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) ) ) -> dom ( x e. C |-> ( sin ` ( n x. x ) ) ) = C )
131 121 130 eleqtrd
 |-  ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) ) ) -> y e. C )
132 eqidd
 |-  ( ( n e. NN0 /\ y e. C ) -> ( x e. C |-> ( sin ` ( n x. x ) ) ) = ( x e. C |-> ( sin ` ( n x. x ) ) ) )
133 71 fveq2d
 |-  ( x = y -> ( sin ` ( n x. x ) ) = ( sin ` ( n x. y ) ) )
134 133 adantl
 |-  ( ( ( n e. NN0 /\ y e. C ) /\ x = y ) -> ( sin ` ( n x. x ) ) = ( sin ` ( n x. y ) ) )
135 77 resincld
 |-  ( ( n e. NN0 /\ y e. C ) -> ( sin ` ( n x. y ) ) e. RR )
136 132 134 74 135 fvmptd
 |-  ( ( n e. NN0 /\ y e. C ) -> ( ( x e. C |-> ( sin ` ( n x. x ) ) ) ` y ) = ( sin ` ( n x. y ) ) )
137 136 fveq2d
 |-  ( ( n e. NN0 /\ y e. C ) -> ( abs ` ( ( x e. C |-> ( sin ` ( n x. x ) ) ) ` y ) ) = ( abs ` ( sin ` ( n x. y ) ) ) )
138 abssinbd
 |-  ( ( n x. y ) e. RR -> ( abs ` ( sin ` ( n x. y ) ) ) <_ 1 )
139 77 138 syl
 |-  ( ( n e. NN0 /\ y e. C ) -> ( abs ` ( sin ` ( n x. y ) ) ) <_ 1 )
140 137 139 eqbrtrd
 |-  ( ( n e. NN0 /\ y e. C ) -> ( abs ` ( ( x e. C |-> ( sin ` ( n x. x ) ) ) ` y ) ) <_ 1 )
141 131 140 syldan
 |-  ( ( n e. NN0 /\ y e. dom ( x e. C |-> ( sin ` ( n x. x ) ) ) ) -> ( abs ` ( ( x e. C |-> ( sin ` ( n x. x ) ) ) ` y ) ) <_ 1 )
142 141 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 )
143 breq2
 |-  ( b = 1 -> ( ( abs ` ( ( x e. C |-> ( sin ` ( n x. x ) ) ) ` y ) ) <_ b <-> ( abs ` ( ( x e. C |-> ( sin ` ( n x. x ) ) ) ` y ) ) <_ 1 ) )
144 143 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 ) )
145 144 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 )
146 57 142 145 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 )
147 146 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 )
148 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 )
149 120 56 147 148 syl3anc
 |-  ( ( ph /\ n e. NN0 ) -> ( ( x e. C |-> ( sin ` ( n x. x ) ) ) oF x. ( x e. C |-> ( F ` x ) ) ) e. L^1 )
150 114 149 eqeltrd
 |-  ( ( ph /\ n e. NN0 ) -> ( x e. C |-> ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) ) e. L^1 )
151 108 150 itgrecl
 |-  ( ( ph /\ n e. NN0 ) -> S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x e. RR )
152 105 151 sylan2
 |-  ( ( ph /\ n e. NN ) -> S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x e. RR )
153 95 a1i
 |-  ( ( ph /\ n e. NN ) -> _pi e. RR )
154 99 a1i
 |-  ( ( ph /\ n e. NN ) -> _pi =/= 0 )
155 152 153 154 redivcld
 |-  ( ( ph /\ n e. NN ) -> ( S. C ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) e. RR )
156 155 5 fmptd
 |-  ( ph -> B : NN --> RR )
157 156 ffvelrnda
 |-  ( ( ph /\ n e. NN ) -> ( B ` n ) e. RR )
158 157 ex
 |-  ( ph -> ( n e. NN -> ( B ` n ) e. RR ) )
159 104 158 jca
 |-  ( ph -> ( ( n e. NN0 -> ( A ` n ) e. RR ) /\ ( n e. NN -> ( B ` n ) e. RR ) ) )