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