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