Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem73.a |
β’ ( π β π΄ β β ) |
2 |
|
fourierdlem73.b |
β’ ( π β π΅ β β ) |
3 |
|
fourierdlem73.f |
β’ ( π β πΉ : ( π΄ [,] π΅ ) βΆ β ) |
4 |
|
fourierdlem73.m |
β’ ( π β π β β ) |
5 |
|
fourierdlem73.qf |
β’ ( π β π : ( 0 ... π ) βΆ ( π΄ [,] π΅ ) ) |
6 |
|
fourierdlem73.q0 |
β’ ( π β ( π β 0 ) = π΄ ) |
7 |
|
fourierdlem73.qm |
β’ ( π β ( π β π ) = π΅ ) |
8 |
|
fourierdlem73.qilt |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π β π ) < ( π β ( π + 1 ) ) ) |
9 |
|
fourierdlem73.fcn |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
10 |
|
fourierdlem73.l |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β πΏ β ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) limβ ( π β ( π + 1 ) ) ) ) |
11 |
|
fourierdlem73.r |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π
β ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) limβ ( π β π ) ) ) |
12 |
|
fourierdlem73.g |
β’ πΊ = ( β D πΉ ) |
13 |
|
fourierdlem73.gcn |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
14 |
|
fourierdlem73.gbd |
β’ ( π β β π¦ β β β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) |
15 |
|
fourierdlem73.s |
β’ π = ( π β β+ β¦ β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
16 |
|
fourierdlem73.d |
β’ π· = ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β¦ if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) ) |
17 |
|
cncff |
β’ ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) β ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) : ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βΆ β ) |
18 |
13 17
|
syl |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) : ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βΆ β ) |
19 |
|
ax-resscn |
β’ β β β |
20 |
19
|
a1i |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β β β β ) |
21 |
1 2
|
iccssred |
β’ ( π β ( π΄ [,] π΅ ) β β ) |
22 |
5 21
|
fssd |
β’ ( π β π : ( 0 ... π ) βΆ β ) |
23 |
22
|
adantr |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π : ( 0 ... π ) βΆ β ) |
24 |
|
elfzofz |
β’ ( π β ( 0 ..^ π ) β π β ( 0 ... π ) ) |
25 |
24
|
adantl |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π β ( 0 ... π ) ) |
26 |
23 25
|
ffvelcdmd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π β π ) β β ) |
27 |
|
fzofzp1 |
β’ ( π β ( 0 ..^ π ) β ( π + 1 ) β ( 0 ... π ) ) |
28 |
27
|
adantl |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π + 1 ) β ( 0 ... π ) ) |
29 |
23 28
|
ffvelcdmd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π β ( π + 1 ) ) β β ) |
30 |
26 29
|
iccssred |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β β ) |
31 |
|
limccl |
β’ ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) limβ ( π β π ) ) β β |
32 |
31 11
|
sselid |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π
β β ) |
33 |
32
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π
β β ) |
34 |
|
limccl |
β’ ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) limβ ( π β ( π + 1 ) ) ) β β |
35 |
34 10
|
sselid |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β πΏ β β ) |
36 |
35
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β πΏ β β ) |
37 |
3
|
ad2antrr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β πΉ : ( π΄ [,] π΅ ) βΆ β ) |
38 |
1
|
ad2antrr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π΄ β β ) |
39 |
2
|
ad2antrr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π΅ β β ) |
40 |
26
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π β π ) β β ) |
41 |
29
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π β ( π + 1 ) ) β β ) |
42 |
|
simpr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) |
43 |
|
eliccre |
β’ ( ( ( π β π ) β β β§ ( π β ( π + 1 ) ) β β β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ β β ) |
44 |
40 41 42 43
|
syl3anc |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ β β ) |
45 |
1
|
rexrd |
β’ ( π β π΄ β β* ) |
46 |
45
|
adantr |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π΄ β β* ) |
47 |
2
|
rexrd |
β’ ( π β π΅ β β* ) |
48 |
47
|
adantr |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π΅ β β* ) |
49 |
5
|
adantr |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π : ( 0 ... π ) βΆ ( π΄ [,] π΅ ) ) |
50 |
49 25
|
ffvelcdmd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π β π ) β ( π΄ [,] π΅ ) ) |
51 |
|
iccgelb |
β’ ( ( π΄ β β* β§ π΅ β β* β§ ( π β π ) β ( π΄ [,] π΅ ) ) β π΄ β€ ( π β π ) ) |
52 |
46 48 50 51
|
syl3anc |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π΄ β€ ( π β π ) ) |
53 |
52
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π΄ β€ ( π β π ) ) |
54 |
40
|
rexrd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π β π ) β β* ) |
55 |
41
|
rexrd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π β ( π + 1 ) ) β β* ) |
56 |
|
iccgelb |
β’ ( ( ( π β π ) β β* β§ ( π β ( π + 1 ) ) β β* β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π β π ) β€ π₯ ) |
57 |
54 55 42 56
|
syl3anc |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π β π ) β€ π₯ ) |
58 |
38 40 44 53 57
|
letrd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π΄ β€ π₯ ) |
59 |
|
iccleub |
β’ ( ( ( π β π ) β β* β§ ( π β ( π + 1 ) ) β β* β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ β€ ( π β ( π + 1 ) ) ) |
60 |
54 55 42 59
|
syl3anc |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ β€ ( π β ( π + 1 ) ) ) |
61 |
45
|
ad2antrr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π΄ β β* ) |
62 |
47
|
ad2antrr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π΅ β β* ) |
63 |
49 28
|
ffvelcdmd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π β ( π + 1 ) ) β ( π΄ [,] π΅ ) ) |
64 |
63
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π β ( π + 1 ) ) β ( π΄ [,] π΅ ) ) |
65 |
|
iccleub |
β’ ( ( π΄ β β* β§ π΅ β β* β§ ( π β ( π + 1 ) ) β ( π΄ [,] π΅ ) ) β ( π β ( π + 1 ) ) β€ π΅ ) |
66 |
61 62 64 65
|
syl3anc |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π β ( π + 1 ) ) β€ π΅ ) |
67 |
44 41 39 60 66
|
letrd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ β€ π΅ ) |
68 |
38 39 44 58 67
|
eliccd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ β ( π΄ [,] π΅ ) ) |
69 |
37 68
|
ffvelcdmd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( πΉ β π₯ ) β β ) |
70 |
36 69
|
ifcld |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) β β ) |
71 |
33 70
|
ifcld |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) β β ) |
72 |
71 16
|
fmptd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π· : ( ( π β π ) [,] ( π β ( π + 1 ) ) ) βΆ β ) |
73 |
|
eqid |
β’ ( TopOpen β βfld ) = ( TopOpen β βfld ) |
74 |
73
|
tgioo2 |
β’ ( topGen β ran (,) ) = ( ( TopOpen β βfld ) βΎt β ) |
75 |
|
iccntr |
β’ ( ( ( π β π ) β β β§ ( π β ( π + 1 ) ) β β ) β ( ( int β ( topGen β ran (,) ) ) β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) = ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) |
76 |
26 29 75
|
syl2anc |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( int β ( topGen β ran (,) ) ) β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) = ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) |
77 |
20 30 72 74 73 76
|
dvresntr |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( β D π· ) = ( β D ( π· βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) ) |
78 |
|
ioossicc |
β’ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) |
79 |
78
|
sseli |
β’ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) |
80 |
79
|
adantl |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) |
81 |
|
fvres |
β’ ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β ( ( πΉ βΎ ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ ) = ( πΉ β π₯ ) ) |
82 |
80 81
|
syl |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( πΉ βΎ ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ ) = ( πΉ β π₯ ) ) |
83 |
80 71
|
syldan |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) β β ) |
84 |
16
|
fvmpt2 |
β’ ( ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β§ if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) β β ) β ( π· β π₯ ) = if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) ) |
85 |
80 83 84
|
syl2anc |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π· β π₯ ) = if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) ) |
86 |
26
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π β π ) β β ) |
87 |
80 54
|
syldan |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π β π ) β β* ) |
88 |
80 55
|
syldan |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π β ( π + 1 ) ) β β* ) |
89 |
|
simpr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) |
90 |
|
ioogtlb |
β’ ( ( ( π β π ) β β* β§ ( π β ( π + 1 ) ) β β* β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π β π ) < π₯ ) |
91 |
87 88 89 90
|
syl3anc |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π β π ) < π₯ ) |
92 |
86 91
|
gtned |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ β ( π β π ) ) |
93 |
92
|
neneqd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β Β¬ π₯ = ( π β π ) ) |
94 |
93
|
iffalsed |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) = if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) |
95 |
|
elioore |
β’ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β π₯ β β ) |
96 |
95
|
adantl |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ β β ) |
97 |
|
iooltub |
β’ ( ( ( π β π ) β β* β§ ( π β ( π + 1 ) ) β β* β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ < ( π β ( π + 1 ) ) ) |
98 |
87 88 89 97
|
syl3anc |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ < ( π β ( π + 1 ) ) ) |
99 |
96 98
|
ltned |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ β ( π β ( π + 1 ) ) ) |
100 |
99
|
neneqd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β Β¬ π₯ = ( π β ( π + 1 ) ) ) |
101 |
100
|
iffalsed |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) = ( πΉ β π₯ ) ) |
102 |
85 94 101
|
3eqtrrd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( πΉ β π₯ ) = ( π· β π₯ ) ) |
103 |
82 102
|
eqtr2d |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π· β π₯ ) = ( ( πΉ βΎ ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ ) ) |
104 |
103
|
ralrimiva |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( π· β π₯ ) = ( ( πΉ βΎ ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ ) ) |
105 |
|
ffn |
β’ ( π· : ( ( π β π ) [,] ( π β ( π + 1 ) ) ) βΆ β β π· Fn ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) |
106 |
72 105
|
syl |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π· Fn ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) |
107 |
|
ffn |
β’ ( πΉ : ( π΄ [,] π΅ ) βΆ β β πΉ Fn ( π΄ [,] π΅ ) ) |
108 |
3 107
|
syl |
β’ ( π β πΉ Fn ( π΄ [,] π΅ ) ) |
109 |
108
|
adantr |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β πΉ Fn ( π΄ [,] π΅ ) ) |
110 |
|
simpr |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π β ( 0 ..^ π ) ) |
111 |
46 48 49 110
|
fourierdlem8 |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β ( π΄ [,] π΅ ) ) |
112 |
|
fnssres |
β’ ( ( πΉ Fn ( π΄ [,] π΅ ) β§ ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β ( π΄ [,] π΅ ) ) β ( πΉ βΎ ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) Fn ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) |
113 |
109 111 112
|
syl2anc |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( πΉ βΎ ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) Fn ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) |
114 |
78
|
a1i |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) |
115 |
|
fvreseq |
β’ ( ( ( π· Fn ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β§ ( πΉ βΎ ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) Fn ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( ( π· βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( ( πΉ βΎ ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( π· β π₯ ) = ( ( πΉ βΎ ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ ) ) ) |
116 |
106 113 114 115
|
syl21anc |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( π· βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( ( πΉ βΎ ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( π· β π₯ ) = ( ( πΉ βΎ ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ ) ) ) |
117 |
104 116
|
mpbird |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π· βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( ( πΉ βΎ ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) |
118 |
114
|
resabs1d |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( πΉ βΎ ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) |
119 |
117 118
|
eqtrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π· βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) |
120 |
119
|
oveq2d |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( β D ( π· βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) = ( β D ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) ) |
121 |
3
|
adantr |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β πΉ : ( π΄ [,] π΅ ) βΆ β ) |
122 |
21
|
adantr |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π΄ [,] π΅ ) β β ) |
123 |
114 30
|
sstrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β β ) |
124 |
73 74
|
dvres |
β’ ( ( ( β β β β§ πΉ : ( π΄ [,] π΅ ) βΆ β ) β§ ( ( π΄ [,] π΅ ) β β β§ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β β ) ) β ( β D ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) = ( ( β D πΉ ) βΎ ( ( int β ( topGen β ran (,) ) ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) ) |
125 |
20 121 122 123 124
|
syl22anc |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( β D ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) = ( ( β D πΉ ) βΎ ( ( int β ( topGen β ran (,) ) ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) ) |
126 |
12
|
eqcomi |
β’ ( β D πΉ ) = πΊ |
127 |
126
|
a1i |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( β D πΉ ) = πΊ ) |
128 |
|
iooretop |
β’ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β ( topGen β ran (,) ) |
129 |
|
retop |
β’ ( topGen β ran (,) ) β Top |
130 |
|
uniretop |
β’ β = βͺ ( topGen β ran (,) ) |
131 |
130
|
isopn3 |
β’ ( ( ( topGen β ran (,) ) β Top β§ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β β ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β ( topGen β ran (,) ) β ( ( int β ( topGen β ran (,) ) ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) |
132 |
129 123 131
|
sylancr |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β ( topGen β ran (,) ) β ( ( int β ( topGen β ran (,) ) ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) |
133 |
128 132
|
mpbii |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( int β ( topGen β ran (,) ) ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) |
134 |
127 133
|
reseq12d |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( β D πΉ ) βΎ ( ( int β ( topGen β ran (,) ) ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) = ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) |
135 |
125 134
|
eqtrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( β D ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) = ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) |
136 |
77 120 135
|
3eqtrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( β D π· ) = ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) |
137 |
136
|
feq1d |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( β D π· ) : ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βΆ β β ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) : ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βΆ β ) ) |
138 |
18 137
|
mpbird |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( β D π· ) : ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βΆ β ) |
139 |
138
|
feqmptd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( β D π· ) = ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( β D π· ) β π₯ ) ) ) |
140 |
139 136
|
eqtr3d |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( β D π· ) β π₯ ) ) = ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) |
141 |
|
ioombl |
β’ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β dom vol |
142 |
141
|
a1i |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β dom vol ) |
143 |
26 29 8
|
ltled |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π β π ) β€ ( π β ( π + 1 ) ) ) |
144 |
|
volioo |
β’ ( ( ( π β π ) β β β§ ( π β ( π + 1 ) ) β β β§ ( π β π ) β€ ( π β ( π + 1 ) ) ) β ( vol β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( ( π β ( π + 1 ) ) β ( π β π ) ) ) |
145 |
26 29 143 144
|
syl3anc |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( vol β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( ( π β ( π + 1 ) ) β ( π β π ) ) ) |
146 |
29 26
|
resubcld |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( π β ( π + 1 ) ) β ( π β π ) ) β β ) |
147 |
145 146
|
eqeltrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( vol β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β β ) |
148 |
14
|
adantr |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β β π¦ β β β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) |
149 |
|
nfv |
β’ β² π₯ ( ( π β§ π β ( 0 ..^ π ) ) β§ π¦ β β ) |
150 |
|
nfra1 |
β’ β² π₯ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ |
151 |
149 150
|
nfan |
β’ β² π₯ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π¦ β β ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) |
152 |
|
simpr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) β π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) |
153 |
|
fdm |
β’ ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) : ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βΆ β β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) |
154 |
18 153
|
syl |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) |
155 |
154
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) |
156 |
152 155
|
eleqtrd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) |
157 |
|
fvres |
β’ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) = ( πΊ β π₯ ) ) |
158 |
156 157
|
syl |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) β ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) = ( πΊ β π₯ ) ) |
159 |
158
|
fveq2d |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) β ( abs β ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) = ( abs β ( πΊ β π₯ ) ) ) |
160 |
159
|
ad4ant14 |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π¦ β β ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β§ π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) β ( abs β ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) = ( abs β ( πΊ β π₯ ) ) ) |
161 |
|
simplr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β§ π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) β β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) |
162 |
|
ssdmres |
β’ ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β dom πΊ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) |
163 |
154 162
|
sylibr |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β dom πΊ ) |
164 |
163
|
sselda |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ β dom πΊ ) |
165 |
156 164
|
syldan |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) β π₯ β dom πΊ ) |
166 |
165
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β§ π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) β π₯ β dom πΊ ) |
167 |
|
rsp |
β’ ( β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ β ( π₯ β dom πΊ β ( abs β ( πΊ β π₯ ) ) β€ π¦ ) ) |
168 |
161 166 167
|
sylc |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β§ π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) β ( abs β ( πΊ β π₯ ) ) β€ π¦ ) |
169 |
168
|
adantllr |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π¦ β β ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β§ π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) β ( abs β ( πΊ β π₯ ) ) β€ π¦ ) |
170 |
160 169
|
eqbrtrd |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π¦ β β ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β§ π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) β ( abs β ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) β€ π¦ ) |
171 |
170
|
ex |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π¦ β β ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β ( π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) β€ π¦ ) ) |
172 |
151 171
|
ralrimi |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π¦ β β ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β β π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ( abs β ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) β€ π¦ ) |
173 |
172
|
ex |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π¦ β β ) β ( β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ β β π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ( abs β ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) β€ π¦ ) ) |
174 |
173
|
reximdva |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( β π¦ β β β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ β β π¦ β β β π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ( abs β ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) β€ π¦ ) ) |
175 |
148 174
|
mpd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β β π¦ β β β π₯ β dom ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ( abs β ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) β€ π¦ ) |
176 |
142 147 13 175
|
cnbdibl |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β πΏ1 ) |
177 |
140 176
|
eqeltrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( β D π· ) β π₯ ) ) β πΏ1 ) |
178 |
177
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( β D π· ) β π₯ ) ) β πΏ1 ) |
179 |
141
|
a1i |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β dom vol ) |
180 |
147
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( vol β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β β ) |
181 |
140 13
|
eqeltrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( β D π· ) β π₯ ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
182 |
181
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( β D π· ) β π₯ ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
183 |
|
coscn |
β’ cos β ( β βcnβ β ) |
184 |
183
|
a1i |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β cos β ( β βcnβ β ) ) |
185 |
|
ioosscn |
β’ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β β |
186 |
185
|
a1i |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β β ) |
187 |
|
simpr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β π β β ) |
188 |
187
|
recnd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β π β β ) |
189 |
|
ssid |
β’ β β β |
190 |
189
|
a1i |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β β β β ) |
191 |
186 188 190
|
constcncfg |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ π ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
192 |
185
|
a1i |
β’ ( π β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β β ) |
193 |
189
|
a1i |
β’ ( π β β β β ) |
194 |
192 193
|
idcncfg |
β’ ( π β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ π₯ ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
195 |
194
|
ad2antrr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ π₯ ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
196 |
191 195
|
mulcncf |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( π Β· π₯ ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
197 |
184 196
|
cncfmpt1f |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( cos β ( π Β· π₯ ) ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
198 |
197
|
negcncfg |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ - ( cos β ( π Β· π₯ ) ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
199 |
182 198
|
mulcncf |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
200 |
|
nfv |
β’ β² π₯ ( π β§ π β ( 0 ..^ π ) ) |
201 |
200 150
|
nfan |
β’ β² π₯ ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) |
202 |
136
|
fveq1d |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( β D π· ) β π₯ ) = ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) |
203 |
202 157
|
sylan9eq |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( β D π· ) β π₯ ) = ( πΊ β π₯ ) ) |
204 |
203
|
fveq2d |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( ( β D π· ) β π₯ ) ) = ( abs β ( πΊ β π₯ ) ) ) |
205 |
204
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( ( β D π· ) β π₯ ) ) = ( abs β ( πΊ β π₯ ) ) ) |
206 |
|
simplr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) |
207 |
164
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ β dom πΊ ) |
208 |
206 207 167
|
sylc |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( πΊ β π₯ ) ) β€ π¦ ) |
209 |
205 208
|
eqbrtrd |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) |
210 |
209
|
ex |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) ) |
211 |
201 210
|
ralrimi |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ ) β β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) |
212 |
211
|
ex |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ β β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) ) |
213 |
212
|
reximdv |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( β π¦ β β β π₯ β dom πΊ ( abs β ( πΊ β π₯ ) ) β€ π¦ β β π¦ β β β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) ) |
214 |
148 213
|
mpd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β β π¦ β β β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) |
215 |
214
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β β π¦ β β β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) |
216 |
|
eqidd |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) = ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) ) |
217 |
|
fveq2 |
β’ ( π₯ = π§ β ( ( β D π· ) β π₯ ) = ( ( β D π· ) β π§ ) ) |
218 |
|
eleq1w |
β’ ( π₯ = π§ β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) |
219 |
218
|
anbi2d |
β’ ( π₯ = π§ β ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( π β§ π β ( 0 ..^ π ) ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) ) ) |
220 |
|
fveq2 |
β’ ( π₯ = π§ β ( πΊ β π₯ ) = ( πΊ β π§ ) ) |
221 |
217 220
|
eqeq12d |
β’ ( π₯ = π§ β ( ( ( β D π· ) β π₯ ) = ( πΊ β π₯ ) β ( ( β D π· ) β π§ ) = ( πΊ β π§ ) ) ) |
222 |
219 221
|
imbi12d |
β’ ( π₯ = π§ β ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( β D π· ) β π₯ ) = ( πΊ β π₯ ) ) β ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( β D π· ) β π§ ) = ( πΊ β π§ ) ) ) ) |
223 |
222 203
|
chvarvv |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( β D π· ) β π§ ) = ( πΊ β π§ ) ) |
224 |
217 223
|
sylan9eqr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β§ π₯ = π§ ) β ( ( β D π· ) β π₯ ) = ( πΊ β π§ ) ) |
225 |
|
oveq2 |
β’ ( π₯ = π§ β ( π Β· π₯ ) = ( π Β· π§ ) ) |
226 |
225
|
fveq2d |
β’ ( π₯ = π§ β ( cos β ( π Β· π₯ ) ) = ( cos β ( π Β· π§ ) ) ) |
227 |
226
|
negeqd |
β’ ( π₯ = π§ β - ( cos β ( π Β· π₯ ) ) = - ( cos β ( π Β· π§ ) ) ) |
228 |
227
|
adantl |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β§ π₯ = π§ ) β - ( cos β ( π Β· π₯ ) ) = - ( cos β ( π Β· π§ ) ) ) |
229 |
224 228
|
oveq12d |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β§ π₯ = π§ ) β ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) = ( ( πΊ β π§ ) Β· - ( cos β ( π Β· π§ ) ) ) ) |
230 |
229
|
adantllr |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β§ π₯ = π§ ) β ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) = ( ( πΊ β π§ ) Β· - ( cos β ( π Β· π§ ) ) ) ) |
231 |
|
simpr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) |
232 |
|
fvres |
β’ ( π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π§ ) = ( πΊ β π§ ) ) |
233 |
232
|
adantl |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π§ ) = ( πΊ β π§ ) ) |
234 |
18
|
ffvelcdmda |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( πΊ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π§ ) β β ) |
235 |
233 234
|
eqeltrrd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( πΊ β π§ ) β β ) |
236 |
235
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( πΊ β π§ ) β β ) |
237 |
|
simpl |
β’ ( ( π β β β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π β β ) |
238 |
|
elioore |
β’ ( π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β π§ β β ) |
239 |
238
|
adantl |
β’ ( ( π β β β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π§ β β ) |
240 |
237 239
|
remulcld |
β’ ( ( π β β β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π Β· π§ ) β β ) |
241 |
240
|
recnd |
β’ ( ( π β β β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π Β· π§ ) β β ) |
242 |
241
|
coscld |
β’ ( ( π β β β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( cos β ( π Β· π§ ) ) β β ) |
243 |
242
|
negcld |
β’ ( ( π β β β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β - ( cos β ( π Β· π§ ) ) β β ) |
244 |
243
|
adantll |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β - ( cos β ( π Β· π§ ) ) β β ) |
245 |
236 244
|
mulcld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( πΊ β π§ ) Β· - ( cos β ( π Β· π§ ) ) ) β β ) |
246 |
216 230 231 245
|
fvmptd |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) β π§ ) = ( ( πΊ β π§ ) Β· - ( cos β ( π Β· π§ ) ) ) ) |
247 |
246
|
fveq2d |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) β π§ ) ) = ( abs β ( ( πΊ β π§ ) Β· - ( cos β ( π Β· π§ ) ) ) ) ) |
248 |
247
|
ad4ant14 |
β’ ( ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π¦ β β ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) β π§ ) ) = ( abs β ( ( πΊ β π§ ) Β· - ( cos β ( π Β· π§ ) ) ) ) ) |
249 |
245
|
abscld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( ( πΊ β π§ ) Β· - ( cos β ( π Β· π§ ) ) ) ) β β ) |
250 |
249
|
ad4ant14 |
β’ ( ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π¦ β β ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( ( πΊ β π§ ) Β· - ( cos β ( π Β· π§ ) ) ) ) β β ) |
251 |
236
|
abscld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( πΊ β π§ ) ) β β ) |
252 |
251
|
ad4ant14 |
β’ ( ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π¦ β β ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( πΊ β π§ ) ) β β ) |
253 |
|
simpllr |
β’ ( ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π¦ β β ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π¦ β β ) |
254 |
244
|
abscld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β - ( cos β ( π Β· π§ ) ) ) β β ) |
255 |
|
1red |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β 1 β β ) |
256 |
236
|
absge0d |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β 0 β€ ( abs β ( πΊ β π§ ) ) ) |
257 |
242
|
absnegd |
β’ ( ( π β β β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β - ( cos β ( π Β· π§ ) ) ) = ( abs β ( cos β ( π Β· π§ ) ) ) ) |
258 |
|
abscosbd |
β’ ( ( π Β· π§ ) β β β ( abs β ( cos β ( π Β· π§ ) ) ) β€ 1 ) |
259 |
240 258
|
syl |
β’ ( ( π β β β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( cos β ( π Β· π§ ) ) ) β€ 1 ) |
260 |
257 259
|
eqbrtrd |
β’ ( ( π β β β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β - ( cos β ( π Β· π§ ) ) ) β€ 1 ) |
261 |
260
|
adantll |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β - ( cos β ( π Β· π§ ) ) ) β€ 1 ) |
262 |
254 255 251 256 261
|
lemul2ad |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( abs β ( πΊ β π§ ) ) Β· ( abs β - ( cos β ( π Β· π§ ) ) ) ) β€ ( ( abs β ( πΊ β π§ ) ) Β· 1 ) ) |
263 |
236 244
|
absmuld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( ( πΊ β π§ ) Β· - ( cos β ( π Β· π§ ) ) ) ) = ( ( abs β ( πΊ β π§ ) ) Β· ( abs β - ( cos β ( π Β· π§ ) ) ) ) ) |
264 |
251
|
recnd |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( πΊ β π§ ) ) β β ) |
265 |
264
|
mulridd |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( abs β ( πΊ β π§ ) ) Β· 1 ) = ( abs β ( πΊ β π§ ) ) ) |
266 |
265
|
eqcomd |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( πΊ β π§ ) ) = ( ( abs β ( πΊ β π§ ) ) Β· 1 ) ) |
267 |
262 263 266
|
3brtr4d |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( ( πΊ β π§ ) Β· - ( cos β ( π Β· π§ ) ) ) ) β€ ( abs β ( πΊ β π§ ) ) ) |
268 |
267
|
ad4ant14 |
β’ ( ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π¦ β β ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( ( πΊ β π§ ) Β· - ( cos β ( π Β· π§ ) ) ) ) β€ ( abs β ( πΊ β π§ ) ) ) |
269 |
|
simpr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) |
270 |
|
nfra1 |
β’ β² π₯ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ |
271 |
200 270
|
nfan |
β’ β² π₯ ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) |
272 |
204
|
eqcomd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( πΊ β π₯ ) ) = ( abs β ( ( β D π· ) β π₯ ) ) ) |
273 |
272
|
adantr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β§ ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β ( abs β ( πΊ β π₯ ) ) = ( abs β ( ( β D π· ) β π₯ ) ) ) |
274 |
|
simpr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β§ ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) |
275 |
273 274
|
eqbrtrd |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β§ ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β ( abs β ( πΊ β π₯ ) ) β€ π¦ ) |
276 |
275
|
ex |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ β ( abs β ( πΊ β π₯ ) ) β€ π¦ ) ) |
277 |
276
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ β ( abs β ( πΊ β π₯ ) ) β€ π¦ ) ) |
278 |
271 277
|
ralimdaa |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β ( β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ β β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( πΊ β π₯ ) ) β€ π¦ ) ) |
279 |
269 278
|
mpd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( πΊ β π₯ ) ) β€ π¦ ) |
280 |
220
|
fveq2d |
β’ ( π₯ = π§ β ( abs β ( πΊ β π₯ ) ) = ( abs β ( πΊ β π§ ) ) ) |
281 |
280
|
breq1d |
β’ ( π₯ = π§ β ( ( abs β ( πΊ β π₯ ) ) β€ π¦ β ( abs β ( πΊ β π§ ) ) β€ π¦ ) ) |
282 |
281
|
cbvralvw |
β’ ( β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( πΊ β π₯ ) ) β€ π¦ β β π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( πΊ β π§ ) ) β€ π¦ ) |
283 |
279 282
|
sylib |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β β π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( πΊ β π§ ) ) β€ π¦ ) |
284 |
283
|
ad4ant14 |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π¦ β β ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β β π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( πΊ β π§ ) ) β€ π¦ ) |
285 |
284
|
r19.21bi |
β’ ( ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π¦ β β ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( πΊ β π§ ) ) β€ π¦ ) |
286 |
250 252 253 268 285
|
letrd |
β’ ( ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π¦ β β ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( ( πΊ β π§ ) Β· - ( cos β ( π Β· π§ ) ) ) ) β€ π¦ ) |
287 |
248 286
|
eqbrtrd |
β’ ( ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π¦ β β ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β§ π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( abs β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) β π§ ) ) β€ π¦ ) |
288 |
287
|
ralrimiva |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π¦ β β ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β β π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) β π§ ) ) β€ π¦ ) |
289 |
138
|
ffvelcdmda |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( β D π· ) β π₯ ) β β ) |
290 |
289
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( β D π· ) β π₯ ) β β ) |
291 |
|
simpl |
β’ ( ( π β β β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π β β ) |
292 |
95
|
adantl |
β’ ( ( π β β β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ β β ) |
293 |
291 292
|
remulcld |
β’ ( ( π β β β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π Β· π₯ ) β β ) |
294 |
293
|
recnd |
β’ ( ( π β β β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π Β· π₯ ) β β ) |
295 |
294
|
coscld |
β’ ( ( π β β β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( cos β ( π Β· π₯ ) ) β β ) |
296 |
295
|
negcld |
β’ ( ( π β β β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β - ( cos β ( π Β· π₯ ) ) β β ) |
297 |
296
|
adantll |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β - ( cos β ( π Β· π₯ ) ) β β ) |
298 |
290 297
|
mulcld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) β β ) |
299 |
298
|
ralrimiva |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) β β ) |
300 |
|
dmmptg |
β’ ( β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) β β β dom ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) = ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) |
301 |
299 300
|
syl |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β dom ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) = ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) |
302 |
301
|
ad2antrr |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π¦ β β ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β dom ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) = ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) |
303 |
302
|
raleqdv |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π¦ β β ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β ( β π§ β dom ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) ( abs β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) β π§ ) ) β€ π¦ β β π§ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) β π§ ) ) β€ π¦ ) ) |
304 |
288 303
|
mpbird |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π¦ β β ) β§ β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) β β π§ β dom ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) ( abs β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) β π§ ) ) β€ π¦ ) |
305 |
304
|
ex |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π¦ β β ) β ( β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ β β π§ β dom ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) ( abs β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) β π§ ) ) β€ π¦ ) ) |
306 |
305
|
reximdva |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( β π¦ β β β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ β β π¦ β β β π§ β dom ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) ( abs β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) β π§ ) ) β€ π¦ ) ) |
307 |
215 306
|
mpd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β β π¦ β β β π§ β dom ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) ( abs β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) β π§ ) ) β€ π¦ ) |
308 |
179 180 199 307
|
cnbdibl |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) β πΏ1 ) |
309 |
308
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π β β ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( ( β D π· ) β π₯ ) Β· - ( cos β ( π Β· π₯ ) ) ) ) β πΏ1 ) |
310 |
289
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( β D π· ) β π₯ ) β β ) |
311 |
|
simpr |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β§ π β β ) β π β β ) |
312 |
185
|
sseli |
β’ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β π₯ β β ) |
313 |
312
|
ad2antlr |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β§ π β β ) β π₯ β β ) |
314 |
311 313
|
mulcld |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β§ π β β ) β ( π Β· π₯ ) β β ) |
315 |
314
|
coscld |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β§ π β β ) β ( cos β ( π Β· π₯ ) ) β β ) |
316 |
293
|
ancoms |
β’ ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β§ π β β ) β ( π Β· π₯ ) β β ) |
317 |
|
abscosbd |
β’ ( ( π Β· π₯ ) β β β ( abs β ( cos β ( π Β· π₯ ) ) ) β€ 1 ) |
318 |
316 317
|
syl |
β’ ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β§ π β β ) β ( abs β ( cos β ( π Β· π₯ ) ) ) β€ 1 ) |
319 |
318
|
adantll |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β§ π β β ) β ( abs β ( cos β ( π Β· π₯ ) ) ) β€ 1 ) |
320 |
16
|
a1i |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π· = ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β¦ if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) ) ) |
321 |
26
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ = ( π β ( π + 1 ) ) ) β ( π β π ) β β ) |
322 |
8
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ = ( π β ( π + 1 ) ) ) β ( π β π ) < ( π β ( π + 1 ) ) ) |
323 |
|
eqcom |
β’ ( ( π β ( π + 1 ) ) = π₯ β π₯ = ( π β ( π + 1 ) ) ) |
324 |
323
|
biimpri |
β’ ( π₯ = ( π β ( π + 1 ) ) β ( π β ( π + 1 ) ) = π₯ ) |
325 |
324
|
adantl |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ = ( π β ( π + 1 ) ) ) β ( π β ( π + 1 ) ) = π₯ ) |
326 |
322 325
|
breqtrd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ = ( π β ( π + 1 ) ) ) β ( π β π ) < π₯ ) |
327 |
321 326
|
gtned |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ = ( π β ( π + 1 ) ) ) β π₯ β ( π β π ) ) |
328 |
327
|
neneqd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ = ( π β ( π + 1 ) ) ) β Β¬ π₯ = ( π β π ) ) |
329 |
328
|
iffalsed |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ = ( π β ( π + 1 ) ) ) β if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) = if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) |
330 |
|
iftrue |
β’ ( π₯ = ( π β ( π + 1 ) ) β if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) = πΏ ) |
331 |
330
|
adantl |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ = ( π β ( π + 1 ) ) ) β if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) = πΏ ) |
332 |
329 331
|
eqtrd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ = ( π β ( π + 1 ) ) ) β if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) = πΏ ) |
333 |
29
|
leidd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π β ( π + 1 ) ) β€ ( π β ( π + 1 ) ) ) |
334 |
26 29 29 143 333
|
eliccd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π β ( π + 1 ) ) β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) |
335 |
320 332 334 10
|
fvmptd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π· β ( π β ( π + 1 ) ) ) = πΏ ) |
336 |
335 35
|
eqeltrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π· β ( π β ( π + 1 ) ) ) β β ) |
337 |
336
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β ( π· β ( π β ( π + 1 ) ) ) β β ) |
338 |
|
eqid |
β’ ( abs β ( π· β ( π β ( π + 1 ) ) ) ) = ( abs β ( π· β ( π β ( π + 1 ) ) ) ) |
339 |
|
iftrue |
β’ ( π₯ = ( π β π ) β if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) = π
) |
340 |
339
|
adantl |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ = ( π β π ) ) β if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) = π
) |
341 |
26
|
rexrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π β π ) β β* ) |
342 |
29
|
rexrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π β ( π + 1 ) ) β β* ) |
343 |
|
lbicc2 |
β’ ( ( ( π β π ) β β* β§ ( π β ( π + 1 ) ) β β* β§ ( π β π ) β€ ( π β ( π + 1 ) ) ) β ( π β π ) β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) |
344 |
341 342 143 343
|
syl3anc |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π β π ) β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) |
345 |
320 340 344 11
|
fvmptd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π· β ( π β π ) ) = π
) |
346 |
345 32
|
eqeltrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π· β ( π β π ) ) β β ) |
347 |
346
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β ( π· β ( π β π ) ) β β ) |
348 |
|
eqid |
β’ ( abs β ( π· β ( π β π ) ) ) = ( abs β ( π· β ( π β π ) ) ) |
349 |
|
eqid |
β’ β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) d π₯ = β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) d π₯ |
350 |
|
simpr |
β’ ( ( π β§ π β β+ ) β π β β+ ) |
351 |
4
|
nnrpd |
β’ ( π β π β β+ ) |
352 |
351
|
adantr |
β’ ( ( π β§ π β β+ ) β π β β+ ) |
353 |
350 352
|
rpdivcld |
β’ ( ( π β§ π β β+ ) β ( π / π ) β β+ ) |
354 |
353
|
adantlr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β ( π / π ) β β+ ) |
355 |
|
simpr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π β β ) β π β β ) |
356 |
29
|
recnd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π β ( π + 1 ) ) β β ) |
357 |
356
|
ad2antrr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π β β ) β ( π β ( π + 1 ) ) β β ) |
358 |
355 357
|
mulcld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π β β ) β ( π Β· ( π β ( π + 1 ) ) ) β β ) |
359 |
358
|
coscld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π β β ) β ( cos β ( π Β· ( π β ( π + 1 ) ) ) ) β β ) |
360 |
29
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( π β ( π + 1 ) ) β β ) |
361 |
187 360
|
remulcld |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( π Β· ( π β ( π + 1 ) ) ) β β ) |
362 |
|
abscosbd |
β’ ( ( π Β· ( π β ( π + 1 ) ) ) β β β ( abs β ( cos β ( π Β· ( π β ( π + 1 ) ) ) ) ) β€ 1 ) |
363 |
361 362
|
syl |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( abs β ( cos β ( π Β· ( π β ( π + 1 ) ) ) ) ) β€ 1 ) |
364 |
363
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π β β ) β ( abs β ( cos β ( π Β· ( π β ( π + 1 ) ) ) ) ) β€ 1 ) |
365 |
26
|
recnd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π β π ) β β ) |
366 |
365
|
ad2antrr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π β β ) β ( π β π ) β β ) |
367 |
355 366
|
mulcld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π β β ) β ( π Β· ( π β π ) ) β β ) |
368 |
367
|
coscld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π β β ) β ( cos β ( π Β· ( π β π ) ) ) β β ) |
369 |
26
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( π β π ) β β ) |
370 |
187 369
|
remulcld |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( π Β· ( π β π ) ) β β ) |
371 |
|
abscosbd |
β’ ( ( π Β· ( π β π ) ) β β β ( abs β ( cos β ( π Β· ( π β π ) ) ) ) β€ 1 ) |
372 |
370 371
|
syl |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( abs β ( cos β ( π Β· ( π β π ) ) ) ) β€ 1 ) |
373 |
372
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π β β ) β ( abs β ( cos β ( π Β· ( π β π ) ) ) ) β€ 1 ) |
374 |
|
fveq2 |
β’ ( π§ = π₯ β ( ( β D π· ) β π§ ) = ( ( β D π· ) β π₯ ) ) |
375 |
374
|
fveq2d |
β’ ( π§ = π₯ β ( abs β ( ( β D π· ) β π§ ) ) = ( abs β ( ( β D π· ) β π₯ ) ) ) |
376 |
375
|
cbvitgv |
β’ β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π§ ) ) d π§ = β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) d π₯ |
377 |
376
|
oveq2i |
β’ ( ( ( abs β ( π· β ( π β ( π + 1 ) ) ) ) + ( abs β ( π· β ( π β π ) ) ) ) + β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π§ ) ) d π§ ) = ( ( ( abs β ( π· β ( π β ( π + 1 ) ) ) ) + ( abs β ( π· β ( π β π ) ) ) ) + β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) d π₯ ) |
378 |
377
|
oveq1i |
β’ ( ( ( ( abs β ( π· β ( π β ( π + 1 ) ) ) ) + ( abs β ( π· β ( π β π ) ) ) ) + β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π§ ) ) d π§ ) / ( π / π ) ) = ( ( ( ( abs β ( π· β ( π β ( π + 1 ) ) ) ) + ( abs β ( π· β ( π β π ) ) ) ) + β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) d π₯ ) / ( π / π ) ) |
379 |
378
|
oveq1i |
β’ ( ( ( ( ( abs β ( π· β ( π β ( π + 1 ) ) ) ) + ( abs β ( π· β ( π β π ) ) ) ) + β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π§ ) ) d π§ ) / ( π / π ) ) + 1 ) = ( ( ( ( ( abs β ( π· β ( π β ( π + 1 ) ) ) ) + ( abs β ( π· β ( π β π ) ) ) ) + β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) d π₯ ) / ( π / π ) ) + 1 ) |
380 |
379
|
fveq2i |
β’ ( β β ( ( ( ( ( abs β ( π· β ( π β ( π + 1 ) ) ) ) + ( abs β ( π· β ( π β π ) ) ) ) + β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π§ ) ) d π§ ) / ( π / π ) ) + 1 ) ) = ( β β ( ( ( ( ( abs β ( π· β ( π β ( π + 1 ) ) ) ) + ( abs β ( π· β ( π β π ) ) ) ) + β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) d π₯ ) / ( π / π ) ) + 1 ) ) |
381 |
380
|
oveq1i |
β’ ( ( β β ( ( ( ( ( abs β ( π· β ( π β ( π + 1 ) ) ) ) + ( abs β ( π· β ( π β π ) ) ) ) + β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π§ ) ) d π§ ) / ( π / π ) ) + 1 ) ) + 1 ) = ( ( β β ( ( ( ( ( abs β ( π· β ( π β ( π + 1 ) ) ) ) + ( abs β ( π· β ( π β π ) ) ) ) + β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) d π₯ ) / ( π / π ) ) + 1 ) ) + 1 ) |
382 |
178 309 310 315 319 337 338 347 348 349 354 359 364 368 373 381
|
fourierdlem47 |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β β π β β β π β ( π (,) +β ) ( abs β ( ( ( ( π· β ( π β ( π + 1 ) ) ) Β· - ( ( cos β ( π Β· ( π β ( π + 1 ) ) ) ) / π ) ) β ( ( π· β ( π β π ) ) Β· - ( ( cos β ( π Β· ( π β π ) ) ) / π ) ) ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( ( β D π· ) β π₯ ) Β· - ( ( cos β ( π Β· π₯ ) ) / π ) ) d π₯ ) ) < ( π / π ) ) |
383 |
|
simplll |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π β ( π (,) +β ) ) β π ) |
384 |
|
simpllr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π β ( π (,) +β ) ) β π β ( 0 ..^ π ) ) |
385 |
|
elioore |
β’ ( π β ( π (,) +β ) β π β β ) |
386 |
385
|
adantl |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β π β β ) |
387 |
|
0red |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β 0 β β ) |
388 |
|
nnre |
β’ ( π β β β π β β ) |
389 |
388
|
adantr |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β π β β ) |
390 |
|
nngt0 |
β’ ( π β β β 0 < π ) |
391 |
390
|
adantr |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β 0 < π ) |
392 |
389
|
rexrd |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β π β β* ) |
393 |
|
pnfxr |
β’ +β β β* |
394 |
393
|
a1i |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β +β β β* ) |
395 |
|
simpr |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β π β ( π (,) +β ) ) |
396 |
|
ioogtlb |
β’ ( ( π β β* β§ +β β β* β§ π β ( π (,) +β ) ) β π < π ) |
397 |
392 394 395 396
|
syl3anc |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β π < π ) |
398 |
387 389 386 391 397
|
lttrd |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β 0 < π ) |
399 |
386 398
|
elrpd |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β π β β+ ) |
400 |
399
|
adantll |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π β ( π (,) +β ) ) β π β β+ ) |
401 |
26
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β ( π β π ) β β ) |
402 |
29
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β ( π β ( π + 1 ) ) β β ) |
403 |
72
|
ffvelcdmda |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π· β π₯ ) β β ) |
404 |
403
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π· β π₯ ) β β ) |
405 |
|
rpcn |
β’ ( π β β+ β π β β ) |
406 |
405
|
ad2antlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π β β ) |
407 |
44
|
recnd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ β β ) |
408 |
407
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ β β ) |
409 |
406 408
|
mulcld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π Β· π₯ ) β β ) |
410 |
409
|
sincld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( sin β ( π Β· π₯ ) ) β β ) |
411 |
404 410
|
mulcld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) β β ) |
412 |
401 402 411
|
itgioo |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
413 |
143
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β ( π β π ) β€ ( π β ( π + 1 ) ) ) |
414 |
72
|
feqmptd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π· = ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β¦ ( π· β π₯ ) ) ) |
415 |
|
iftrue |
β’ ( π₯ = ( π β ( π + 1 ) ) β if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) = πΏ ) |
416 |
330 415
|
eqtr4d |
β’ ( π₯ = ( π β ( π + 1 ) ) β if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) = if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) ) |
417 |
416
|
adantl |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β§ π₯ = ( π β ( π + 1 ) ) ) β if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) = if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) ) |
418 |
|
iffalse |
β’ ( Β¬ π₯ = ( π β ( π + 1 ) ) β if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) = ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) |
419 |
418
|
adantl |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) = ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) |
420 |
54
|
ad2antrr |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β ( π β π ) β β* ) |
421 |
55
|
ad2antrr |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β ( π β ( π + 1 ) ) β β* ) |
422 |
44
|
ad2antrr |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β π₯ β β ) |
423 |
26
|
ad2antrr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β ( π β π ) β β ) |
424 |
44
|
adantr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β π₯ β β ) |
425 |
57
|
adantr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β ( π β π ) β€ π₯ ) |
426 |
|
neqne |
β’ ( Β¬ π₯ = ( π β π ) β π₯ β ( π β π ) ) |
427 |
426
|
adantl |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β π₯ β ( π β π ) ) |
428 |
423 424 425 427
|
leneltd |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β ( π β π ) < π₯ ) |
429 |
428
|
adantr |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β ( π β π ) < π₯ ) |
430 |
44
|
adantr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β π₯ β β ) |
431 |
29
|
ad2antrr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β ( π β ( π + 1 ) ) β β ) |
432 |
60
|
adantr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β π₯ β€ ( π β ( π + 1 ) ) ) |
433 |
323
|
biimpi |
β’ ( ( π β ( π + 1 ) ) = π₯ β π₯ = ( π β ( π + 1 ) ) ) |
434 |
433
|
necon3bi |
β’ ( Β¬ π₯ = ( π β ( π + 1 ) ) β ( π β ( π + 1 ) ) β π₯ ) |
435 |
434
|
adantl |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β ( π β ( π + 1 ) ) β π₯ ) |
436 |
430 431 432 435
|
leneltd |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β π₯ < ( π β ( π + 1 ) ) ) |
437 |
436
|
adantlr |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β π₯ < ( π β ( π + 1 ) ) ) |
438 |
420 421 422 429 437
|
eliood |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) |
439 |
|
fvres |
β’ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) = ( πΉ β π₯ ) ) |
440 |
438 439
|
syl |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) = ( πΉ β π₯ ) ) |
441 |
|
iffalse |
β’ ( Β¬ π₯ = ( π β ( π + 1 ) ) β if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) = ( πΉ β π₯ ) ) |
442 |
441
|
eqcomd |
β’ ( Β¬ π₯ = ( π β ( π + 1 ) ) β ( πΉ β π₯ ) = if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) |
443 |
442
|
adantl |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β ( πΉ β π₯ ) = if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) |
444 |
419 440 443
|
3eqtrrd |
β’ ( ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β§ Β¬ π₯ = ( π β ( π + 1 ) ) ) β if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) = if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) ) |
445 |
417 444
|
pm2.61dan |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β§ Β¬ π₯ = ( π β π ) ) β if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) = if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) ) |
446 |
445
|
ifeq2da |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) = if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) ) ) |
447 |
446
|
mpteq2dva |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β¦ if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( πΉ β π₯ ) ) ) ) = ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β¦ if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) ) ) ) |
448 |
320 414 447
|
3eqtr3d |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β¦ ( π· β π₯ ) ) = ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β¦ if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) ) ) ) |
449 |
|
eqid |
β’ ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β¦ if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) ) ) = ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β¦ if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) ) ) |
450 |
200 449 26 29 9 10 11
|
cncfiooicc |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β¦ if ( π₯ = ( π β π ) , π
, if ( π₯ = ( π β ( π + 1 ) ) , πΏ , ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ ) ) ) ) β ( ( ( π β π ) [,] ( π β ( π + 1 ) ) ) βcnβ β ) ) |
451 |
448 450
|
eqeltrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β¦ ( π· β π₯ ) ) β ( ( ( π β π ) [,] ( π β ( π + 1 ) ) ) βcnβ β ) ) |
452 |
414 451
|
eqeltrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π· β ( ( ( π β π ) [,] ( π β ( π + 1 ) ) ) βcnβ β ) ) |
453 |
452
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β π· β ( ( ( π β π ) [,] ( π β ( π + 1 ) ) ) βcnβ β ) ) |
454 |
|
eqid |
β’ ( β D π· ) = ( β D π· ) |
455 |
136 13
|
eqeltrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( β D π· ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
456 |
455
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β ( β D π· ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
457 |
214
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β β π¦ β β β π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( abs β ( ( β D π· ) β π₯ ) ) β€ π¦ ) |
458 |
|
simpr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β π β β+ ) |
459 |
401 402 413 453 454 456 457 458
|
fourierdlem39 |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = ( ( ( ( π· β ( π β ( π + 1 ) ) ) Β· - ( ( cos β ( π Β· ( π β ( π + 1 ) ) ) ) / π ) ) β ( ( π· β ( π β π ) ) Β· - ( ( cos β ( π Β· ( π β π ) ) ) / π ) ) ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( ( β D π· ) β π₯ ) Β· - ( ( cos β ( π Β· π₯ ) ) / π ) ) d π₯ ) ) |
460 |
412 459
|
eqtr3d |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = ( ( ( ( π· β ( π β ( π + 1 ) ) ) Β· - ( ( cos β ( π Β· ( π β ( π + 1 ) ) ) ) / π ) ) β ( ( π· β ( π β π ) ) Β· - ( ( cos β ( π Β· ( π β π ) ) ) / π ) ) ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( ( β D π· ) β π₯ ) Β· - ( ( cos β ( π Β· π₯ ) ) / π ) ) d π₯ ) ) |
461 |
383 384 400 460
|
syl21anc |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π β ( π (,) +β ) ) β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = ( ( ( ( π· β ( π β ( π + 1 ) ) ) Β· - ( ( cos β ( π Β· ( π β ( π + 1 ) ) ) ) / π ) ) β ( ( π· β ( π β π ) ) Β· - ( ( cos β ( π Β· ( π β π ) ) ) / π ) ) ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( ( β D π· ) β π₯ ) Β· - ( ( cos β ( π Β· π₯ ) ) / π ) ) d π₯ ) ) |
462 |
461
|
fveq2d |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π β ( π (,) +β ) ) β ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) = ( abs β ( ( ( ( π· β ( π β ( π + 1 ) ) ) Β· - ( ( cos β ( π Β· ( π β ( π + 1 ) ) ) ) / π ) ) β ( ( π· β ( π β π ) ) Β· - ( ( cos β ( π Β· ( π β π ) ) ) / π ) ) ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( ( β D π· ) β π₯ ) Β· - ( ( cos β ( π Β· π₯ ) ) / π ) ) d π₯ ) ) ) |
463 |
462
|
breq1d |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β§ π β ( π (,) +β ) ) β ( ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β ( abs β ( ( ( ( π· β ( π β ( π + 1 ) ) ) Β· - ( ( cos β ( π Β· ( π β ( π + 1 ) ) ) ) / π ) ) β ( ( π· β ( π β π ) ) Β· - ( ( cos β ( π Β· ( π β π ) ) ) / π ) ) ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( ( β D π· ) β π₯ ) Β· - ( ( cos β ( π Β· π₯ ) ) / π ) ) d π₯ ) ) < ( π / π ) ) ) |
464 |
463
|
ralbidva |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β ) β ( β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β β π β ( π (,) +β ) ( abs β ( ( ( ( π· β ( π β ( π + 1 ) ) ) Β· - ( ( cos β ( π Β· ( π β ( π + 1 ) ) ) ) / π ) ) β ( ( π· β ( π β π ) ) Β· - ( ( cos β ( π Β· ( π β π ) ) ) / π ) ) ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( ( β D π· ) β π₯ ) Β· - ( ( cos β ( π Β· π₯ ) ) / π ) ) d π₯ ) ) < ( π / π ) ) ) |
465 |
464
|
rexbidva |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β β π β β β π β ( π (,) +β ) ( abs β ( ( ( ( π· β ( π β ( π + 1 ) ) ) Β· - ( ( cos β ( π Β· ( π β ( π + 1 ) ) ) ) / π ) ) β ( ( π· β ( π β π ) ) Β· - ( ( cos β ( π Β· ( π β π ) ) ) / π ) ) ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( ( β D π· ) β π₯ ) Β· - ( ( cos β ( π Β· π₯ ) ) / π ) ) d π₯ ) ) < ( π / π ) ) ) |
466 |
465
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β ( β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β β π β β β π β ( π (,) +β ) ( abs β ( ( ( ( π· β ( π β ( π + 1 ) ) ) Β· - ( ( cos β ( π Β· ( π β ( π + 1 ) ) ) ) / π ) ) β ( ( π· β ( π β π ) ) Β· - ( ( cos β ( π Β· ( π β π ) ) ) / π ) ) ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( ( β D π· ) β π₯ ) Β· - ( ( cos β ( π Β· π₯ ) ) / π ) ) d π₯ ) ) < ( π / π ) ) ) |
467 |
382 466
|
mpbird |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β β+ ) β β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
468 |
467
|
an32s |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
469 |
102
|
oveq1d |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) = ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) ) |
470 |
469
|
itgeq2dv |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
471 |
470
|
eqcomd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
472 |
471
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
473 |
26
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β ( π β π ) β β ) |
474 |
29
|
adantr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β ( π β ( π + 1 ) ) β β ) |
475 |
403
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π· β π₯ ) β β ) |
476 |
385
|
recnd |
β’ ( π β ( π (,) +β ) β π β β ) |
477 |
476
|
ad2antlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π β β ) |
478 |
407
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ β β ) |
479 |
477 478
|
mulcld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π Β· π₯ ) β β ) |
480 |
479
|
sincld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( sin β ( π Β· π₯ ) ) β β ) |
481 |
475 480
|
mulcld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) β β ) |
482 |
473 474 481
|
itgioo |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
483 |
69
|
adantlr |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( πΉ β π₯ ) β β ) |
484 |
483 480
|
mulcld |
β’ ( ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) β β ) |
485 |
473 474 484
|
itgioo |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β β« ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
486 |
472 482 485
|
3eqtr3d |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
487 |
486
|
fveq2d |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) = ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) ) |
488 |
487
|
breq1d |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π β ( π (,) +β ) ) β ( ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) ) |
489 |
488
|
ralbidva |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) ) |
490 |
489
|
adantlr |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) ) |
491 |
490
|
rexbidv |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( π· β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) ) |
492 |
468 491
|
mpbid |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
493 |
492
|
ralrimiva |
β’ ( ( π β§ π β β+ ) β β π β ( 0 ..^ π ) β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
494 |
493
|
ralrimiva |
β’ ( π β β π β β+ β π β ( 0 ..^ π ) β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
495 |
|
nfv |
β’ β² π ( π β§ π β β+ ) |
496 |
|
nfra1 |
β’ β² π β π β ( 0 ..^ π ) β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) |
497 |
495 496
|
nfan |
β’ β² π ( ( π β§ π β β+ ) β§ β π β ( 0 ..^ π ) β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
498 |
|
nfv |
β’ β² π ( π β§ π β β+ ) |
499 |
|
nfcv |
β’ β² π ( 0 ..^ π ) |
500 |
|
nfcv |
β’ β² π β |
501 |
|
nfra1 |
β’ β² π β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) |
502 |
500 501
|
nfrexw |
β’ β² π β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) |
503 |
499 502
|
nfralw |
β’ β² π β π β ( 0 ..^ π ) β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) |
504 |
498 503
|
nfan |
β’ β² π ( ( π β§ π β β+ ) β§ β π β ( 0 ..^ π ) β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
505 |
|
nfmpt1 |
β’ β² π ( π β ( 0 ..^ π ) β¦ inf ( { π β β β£ β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) } , β , < ) ) |
506 |
|
fzofi |
β’ ( 0 ..^ π ) β Fin |
507 |
506
|
a1i |
β’ ( ( ( π β§ π β β+ ) β§ β π β ( 0 ..^ π ) β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β ( 0 ..^ π ) β Fin ) |
508 |
|
simpr |
β’ ( ( ( π β§ π β β+ ) β§ β π β ( 0 ..^ π ) β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β β π β ( 0 ..^ π ) β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
509 |
|
eqid |
β’ { π β β β£ β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) } = { π β β β£ β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) } |
510 |
|
eqid |
β’ ( π β ( 0 ..^ π ) β¦ inf ( { π β β β£ β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) } , β , < ) ) = ( π β ( 0 ..^ π ) β¦ inf ( { π β β β£ β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) } , β , < ) ) |
511 |
|
eqid |
β’ sup ( ran ( π β ( 0 ..^ π ) β¦ inf ( { π β β β£ β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) } , β , < ) ) , β , < ) = sup ( ran ( π β ( 0 ..^ π ) β¦ inf ( { π β β β£ β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) } , β , < ) ) , β , < ) |
512 |
497 504 505 507 508 509 510 511
|
fourierdlem31 |
β’ ( ( ( π β§ π β β+ ) β§ β π β ( 0 ..^ π ) β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β β π β β β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
513 |
|
simpr |
β’ ( ( ( π β§ π β β+ ) β§ β π β β β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β β π β β β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
514 |
|
nfv |
β’ β² π ( π β§ π β β+ ) |
515 |
|
nfre1 |
β’ β² π β π β β β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) |
516 |
514 515
|
nfan |
β’ β² π ( ( π β§ π β β+ ) β§ β π β β β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
517 |
|
nfv |
β’ β² π π β β |
518 |
|
nfra1 |
β’ β² π β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) |
519 |
498 517 518
|
nf3an |
β’ β² π ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
520 |
|
simpll |
β’ ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β π ) |
521 |
|
elioore |
β’ ( π β ( π (,) +β ) β π β β ) |
522 |
521
|
adantl |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β π β β ) |
523 |
|
0red |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β 0 β β ) |
524 |
|
nnre |
β’ ( π β β β π β β ) |
525 |
524
|
adantr |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β π β β ) |
526 |
|
nngt0 |
β’ ( π β β β 0 < π ) |
527 |
526
|
adantr |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β 0 < π ) |
528 |
525
|
rexrd |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β π β β* ) |
529 |
393
|
a1i |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β +β β β* ) |
530 |
|
simpr |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β π β ( π (,) +β ) ) |
531 |
|
ioogtlb |
β’ ( ( π β β* β§ +β β β* β§ π β ( π (,) +β ) ) β π < π ) |
532 |
528 529 530 531
|
syl3anc |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β π < π ) |
533 |
523 525 522 527 532
|
lttrd |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β 0 < π ) |
534 |
522 533
|
elrpd |
β’ ( ( π β β β§ π β ( π (,) +β ) ) β π β β+ ) |
535 |
534
|
adantll |
β’ ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β π β β+ ) |
536 |
1
|
adantr |
β’ ( ( π β§ π β β+ ) β π΄ β β ) |
537 |
2
|
adantr |
β’ ( ( π β§ π β β+ ) β π΅ β β ) |
538 |
3
|
ffvelcdmda |
β’ ( ( π β§ π₯ β ( π΄ [,] π΅ ) ) β ( πΉ β π₯ ) β β ) |
539 |
538
|
adantlr |
β’ ( ( ( π β§ π β β+ ) β§ π₯ β ( π΄ [,] π΅ ) ) β ( πΉ β π₯ ) β β ) |
540 |
405
|
ad2antlr |
β’ ( ( ( π β§ π β β+ ) β§ π₯ β ( π΄ [,] π΅ ) ) β π β β ) |
541 |
21
|
sselda |
β’ ( ( π β§ π₯ β ( π΄ [,] π΅ ) ) β π₯ β β ) |
542 |
541
|
recnd |
β’ ( ( π β§ π₯ β ( π΄ [,] π΅ ) ) β π₯ β β ) |
543 |
542
|
adantlr |
β’ ( ( ( π β§ π β β+ ) β§ π₯ β ( π΄ [,] π΅ ) ) β π₯ β β ) |
544 |
540 543
|
mulcld |
β’ ( ( ( π β§ π β β+ ) β§ π₯ β ( π΄ [,] π΅ ) ) β ( π Β· π₯ ) β β ) |
545 |
544
|
sincld |
β’ ( ( ( π β§ π β β+ ) β§ π₯ β ( π΄ [,] π΅ ) ) β ( sin β ( π Β· π₯ ) ) β β ) |
546 |
539 545
|
mulcld |
β’ ( ( ( π β§ π β β+ ) β§ π₯ β ( π΄ [,] π΅ ) ) β ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) β β ) |
547 |
536 537 546
|
itgioo |
β’ ( ( π β§ π β β+ ) β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = β« ( π΄ [,] π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
548 |
6
|
eqcomd |
β’ ( π β π΄ = ( π β 0 ) ) |
549 |
7
|
eqcomd |
β’ ( π β π΅ = ( π β π ) ) |
550 |
548 549
|
oveq12d |
β’ ( π β ( π΄ [,] π΅ ) = ( ( π β 0 ) [,] ( π β π ) ) ) |
551 |
550
|
adantr |
β’ ( ( π β§ π β β+ ) β ( π΄ [,] π΅ ) = ( ( π β 0 ) [,] ( π β π ) ) ) |
552 |
551
|
itgeq1d |
β’ ( ( π β§ π β β+ ) β β« ( π΄ [,] π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = β« ( ( π β 0 ) [,] ( π β π ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
553 |
|
0zd |
β’ ( ( π β§ π β β+ ) β 0 β β€ ) |
554 |
|
nnuz |
β’ β = ( β€β₯ β 1 ) |
555 |
|
0p1e1 |
β’ ( 0 + 1 ) = 1 |
556 |
555
|
fveq2i |
β’ ( β€β₯ β ( 0 + 1 ) ) = ( β€β₯ β 1 ) |
557 |
554 556
|
eqtr4i |
β’ β = ( β€β₯ β ( 0 + 1 ) ) |
558 |
4 557
|
eleqtrdi |
β’ ( π β π β ( β€β₯ β ( 0 + 1 ) ) ) |
559 |
558
|
adantr |
β’ ( ( π β§ π β β+ ) β π β ( β€β₯ β ( 0 + 1 ) ) ) |
560 |
22
|
adantr |
β’ ( ( π β§ π β β+ ) β π : ( 0 ... π ) βΆ β ) |
561 |
8
|
adantlr |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π β π ) < ( π β ( π + 1 ) ) ) |
562 |
|
simpr |
β’ ( ( π β§ π₯ β ( ( π β 0 ) [,] ( π β π ) ) ) β π₯ β ( ( π β 0 ) [,] ( π β π ) ) ) |
563 |
550
|
eqcomd |
β’ ( π β ( ( π β 0 ) [,] ( π β π ) ) = ( π΄ [,] π΅ ) ) |
564 |
563
|
adantr |
β’ ( ( π β§ π₯ β ( ( π β 0 ) [,] ( π β π ) ) ) β ( ( π β 0 ) [,] ( π β π ) ) = ( π΄ [,] π΅ ) ) |
565 |
562 564
|
eleqtrd |
β’ ( ( π β§ π₯ β ( ( π β 0 ) [,] ( π β π ) ) ) β π₯ β ( π΄ [,] π΅ ) ) |
566 |
565
|
adantlr |
β’ ( ( ( π β§ π β β+ ) β§ π₯ β ( ( π β 0 ) [,] ( π β π ) ) ) β π₯ β ( π΄ [,] π΅ ) ) |
567 |
566 546
|
syldan |
β’ ( ( ( π β§ π β β+ ) β§ π₯ β ( ( π β 0 ) [,] ( π β π ) ) ) β ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) β β ) |
568 |
26
|
adantlr |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π β π ) β β ) |
569 |
29
|
adantlr |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π β ( π + 1 ) ) β β ) |
570 |
114 111
|
sstrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β ( π΄ [,] π΅ ) ) |
571 |
121 570
|
feqresmpt |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) = ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( πΉ β π₯ ) ) ) |
572 |
571 9
|
eqeltrrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( πΉ β π₯ ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
573 |
572
|
adantlr |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( πΉ β π₯ ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
574 |
|
sincn |
β’ sin β ( β βcnβ β ) |
575 |
574
|
a1i |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β sin β ( β βcnβ β ) ) |
576 |
185
|
a1i |
β’ ( ( π β§ π β β+ ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β β ) |
577 |
405
|
adantl |
β’ ( ( π β§ π β β+ ) β π β β ) |
578 |
189
|
a1i |
β’ ( ( π β§ π β β+ ) β β β β ) |
579 |
576 577 578
|
constcncfg |
β’ ( ( π β§ π β β+ ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ π ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
580 |
194
|
adantr |
β’ ( ( π β§ π β β+ ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ π₯ ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
581 |
579 580
|
mulcncf |
β’ ( ( π β§ π β β+ ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( π Β· π₯ ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
582 |
581
|
adantr |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( π Β· π₯ ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
583 |
575 582
|
cncfmpt1f |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( sin β ( π Β· π₯ ) ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
584 |
573 583
|
mulcncf |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) ) β ( ( ( π β π ) (,) ( π β ( π + 1 ) ) ) βcnβ β ) ) |
585 |
|
eqid |
β’ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( πΉ β π₯ ) ) = ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( πΉ β π₯ ) ) |
586 |
|
eqid |
β’ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( sin β ( π Β· π₯ ) ) ) = ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( sin β ( π Β· π₯ ) ) ) |
587 |
|
eqid |
β’ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) ) = ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) ) |
588 |
3
|
ad2antrr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β πΉ : ( π΄ [,] π΅ ) βΆ β ) |
589 |
45
|
ad2antrr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π΄ β β* ) |
590 |
47
|
ad2antrr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π΅ β β* ) |
591 |
5
|
ad2antrr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π : ( 0 ... π ) βΆ ( π΄ [,] π΅ ) ) |
592 |
|
simplr |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π β ( 0 ..^ π ) ) |
593 |
589 590 591 592 80
|
fourierdlem1 |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ β ( π΄ [,] π΅ ) ) |
594 |
588 593
|
ffvelcdmd |
β’ ( ( ( π β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( πΉ β π₯ ) β β ) |
595 |
594
|
adantllr |
β’ ( ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( πΉ β π₯ ) β β ) |
596 |
577
|
ad2antrr |
β’ ( ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π β β ) |
597 |
312
|
adantl |
β’ ( ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ β β ) |
598 |
596 597
|
mulcld |
β’ ( ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π Β· π₯ ) β β ) |
599 |
598
|
sincld |
β’ ( ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( sin β ( π Β· π₯ ) ) β β ) |
600 |
571
|
oveq1d |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) limβ ( π β ( π + 1 ) ) ) = ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( πΉ β π₯ ) ) limβ ( π β ( π + 1 ) ) ) ) |
601 |
10 600
|
eleqtrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β πΏ β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( πΉ β π₯ ) ) limβ ( π β ( π + 1 ) ) ) ) |
602 |
601
|
adantlr |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β πΏ β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( πΉ β π₯ ) ) limβ ( π β ( π + 1 ) ) ) ) |
603 |
|
rpre |
β’ ( π β β+ β π β β ) |
604 |
603
|
adantr |
β’ ( ( π β β+ β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π β β ) |
605 |
95
|
adantl |
β’ ( ( π β β+ β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β π₯ β β ) |
606 |
604 605
|
remulcld |
β’ ( ( π β β+ β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π Β· π₯ ) β β ) |
607 |
606
|
adantll |
β’ ( ( ( π β§ π β β+ ) β§ π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) β ( π Β· π₯ ) β β ) |
608 |
607
|
ad2ant2r |
β’ ( ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β§ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β§ ( π Β· π₯ ) β ( π Β· ( π β ( π + 1 ) ) ) ) ) β ( π Β· π₯ ) β β ) |
609 |
|
recn |
β’ ( π¦ β β β π¦ β β ) |
610 |
609
|
sincld |
β’ ( π¦ β β β ( sin β π¦ ) β β ) |
611 |
610
|
adantl |
β’ ( ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β§ π¦ β β ) β ( sin β π¦ ) β β ) |
612 |
|
eqid |
β’ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ π ) = ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ π ) |
613 |
|
eqid |
β’ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ π₯ ) = ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ π₯ ) |
614 |
|
eqid |
β’ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( π Β· π₯ ) ) = ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( π Β· π₯ ) ) |
615 |
185
|
a1i |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β β ) |
616 |
577
|
adantr |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β π β β ) |
617 |
569
|
recnd |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π β ( π + 1 ) ) β β ) |
618 |
612 615 616 617
|
constlimc |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β π β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ π ) limβ ( π β ( π + 1 ) ) ) ) |
619 |
615 613 617
|
idlimc |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π β ( π + 1 ) ) β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ π₯ ) limβ ( π β ( π + 1 ) ) ) ) |
620 |
612 613 614 596 597 618 619
|
mullimc |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π Β· ( π β ( π + 1 ) ) ) β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( π Β· π₯ ) ) limβ ( π β ( π + 1 ) ) ) ) |
621 |
|
eqid |
β’ ( π¦ β β β¦ ( sin β π¦ ) ) = ( π¦ β β β¦ ( sin β π¦ ) ) |
622 |
|
sinf |
β’ sin : β βΆ β |
623 |
622
|
a1i |
β’ ( β€ β sin : β βΆ β ) |
624 |
623
|
feqmptd |
β’ ( β€ β sin = ( π¦ β β β¦ ( sin β π¦ ) ) ) |
625 |
624 574
|
eqeltrrdi |
β’ ( β€ β ( π¦ β β β¦ ( sin β π¦ ) ) β ( β βcnβ β ) ) |
626 |
19
|
a1i |
β’ ( β€ β β β β ) |
627 |
|
resincl |
β’ ( π¦ β β β ( sin β π¦ ) β β ) |
628 |
627
|
adantl |
β’ ( ( β€ β§ π¦ β β ) β ( sin β π¦ ) β β ) |
629 |
621 625 626 626 628
|
cncfmptssg |
β’ ( β€ β ( π¦ β β β¦ ( sin β π¦ ) ) β ( β βcnβ β ) ) |
630 |
629
|
mptru |
β’ ( π¦ β β β¦ ( sin β π¦ ) ) β ( β βcnβ β ) |
631 |
630
|
a1i |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π¦ β β β¦ ( sin β π¦ ) ) β ( β βcnβ β ) ) |
632 |
603
|
ad2antlr |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β π β β ) |
633 |
632 569
|
remulcld |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π Β· ( π β ( π + 1 ) ) ) β β ) |
634 |
|
fveq2 |
β’ ( π¦ = ( π Β· ( π β ( π + 1 ) ) ) β ( sin β π¦ ) = ( sin β ( π Β· ( π β ( π + 1 ) ) ) ) ) |
635 |
631 633 634
|
cnmptlimc |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( sin β ( π Β· ( π β ( π + 1 ) ) ) ) β ( ( π¦ β β β¦ ( sin β π¦ ) ) limβ ( π Β· ( π β ( π + 1 ) ) ) ) ) |
636 |
|
fveq2 |
β’ ( π¦ = ( π Β· π₯ ) β ( sin β π¦ ) = ( sin β ( π Β· π₯ ) ) ) |
637 |
|
fveq2 |
β’ ( ( π Β· π₯ ) = ( π Β· ( π β ( π + 1 ) ) ) β ( sin β ( π Β· π₯ ) ) = ( sin β ( π Β· ( π β ( π + 1 ) ) ) ) ) |
638 |
637
|
ad2antll |
β’ ( ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β§ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β§ ( π Β· π₯ ) = ( π Β· ( π β ( π + 1 ) ) ) ) ) β ( sin β ( π Β· π₯ ) ) = ( sin β ( π Β· ( π β ( π + 1 ) ) ) ) ) |
639 |
608 611 620 635 636 638
|
limcco |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( sin β ( π Β· ( π β ( π + 1 ) ) ) ) β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( sin β ( π Β· π₯ ) ) ) limβ ( π β ( π + 1 ) ) ) ) |
640 |
585 586 587 595 599 602 639
|
mullimc |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( πΏ Β· ( sin β ( π Β· ( π β ( π + 1 ) ) ) ) ) β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) ) limβ ( π β ( π + 1 ) ) ) ) |
641 |
571
|
oveq1d |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β ( ( πΉ βΎ ( ( π β π ) (,) ( π β ( π + 1 ) ) ) ) limβ ( π β π ) ) = ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( πΉ β π₯ ) ) limβ ( π β π ) ) ) |
642 |
11 641
|
eleqtrd |
β’ ( ( π β§ π β ( 0 ..^ π ) ) β π
β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( πΉ β π₯ ) ) limβ ( π β π ) ) ) |
643 |
642
|
adantlr |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β π
β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( πΉ β π₯ ) ) limβ ( π β π ) ) ) |
644 |
607
|
ad2ant2r |
β’ ( ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β§ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β§ ( π Β· π₯ ) β ( π Β· ( π β π ) ) ) ) β ( π Β· π₯ ) β β ) |
645 |
568
|
recnd |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π β π ) β β ) |
646 |
612 615 616 645
|
constlimc |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β π β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ π ) limβ ( π β π ) ) ) |
647 |
615 613 645
|
idlimc |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π β π ) β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ π₯ ) limβ ( π β π ) ) ) |
648 |
612 613 614 596 597 646 647
|
mullimc |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π Β· ( π β π ) ) β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( π Β· π₯ ) ) limβ ( π β π ) ) ) |
649 |
632 568
|
remulcld |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π Β· ( π β π ) ) β β ) |
650 |
|
fveq2 |
β’ ( π¦ = ( π Β· ( π β π ) ) β ( sin β π¦ ) = ( sin β ( π Β· ( π β π ) ) ) ) |
651 |
631 649 650
|
cnmptlimc |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( sin β ( π Β· ( π β π ) ) ) β ( ( π¦ β β β¦ ( sin β π¦ ) ) limβ ( π Β· ( π β π ) ) ) ) |
652 |
|
fveq2 |
β’ ( ( π Β· π₯ ) = ( π Β· ( π β π ) ) β ( sin β ( π Β· π₯ ) ) = ( sin β ( π Β· ( π β π ) ) ) ) |
653 |
652
|
ad2antll |
β’ ( ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β§ ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β§ ( π Β· π₯ ) = ( π Β· ( π β π ) ) ) ) β ( sin β ( π Β· π₯ ) ) = ( sin β ( π Β· ( π β π ) ) ) ) |
654 |
644 611 648 651 636 653
|
limcco |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( sin β ( π Β· ( π β π ) ) ) β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( sin β ( π Β· π₯ ) ) ) limβ ( π β π ) ) ) |
655 |
585 586 587 595 599 643 654
|
mullimc |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π
Β· ( sin β ( π Β· ( π β π ) ) ) ) β ( ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) ) limβ ( π β π ) ) ) |
656 |
568 569 584 640 655
|
iblcncfioo |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) (,) ( π β ( π + 1 ) ) ) β¦ ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) ) β πΏ1 ) |
657 |
|
simpll |
β’ ( ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π β§ π β β+ ) ) |
658 |
68
|
adantllr |
β’ ( ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ β ( π΄ [,] π΅ ) ) |
659 |
657 658 546
|
syl2anc |
β’ ( ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) β β ) |
660 |
568 569 656 659
|
ibliooicc |
β’ ( ( ( π β§ π β β+ ) β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β¦ ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) ) β πΏ1 ) |
661 |
553 559 560 561 567 660
|
itgspltprt |
β’ ( ( π β§ π β β+ ) β β« ( ( π β 0 ) [,] ( π β π ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = Ξ£ π β ( 0 ..^ π ) β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
662 |
547 552 661
|
3eqtrd |
β’ ( ( π β§ π β β+ ) β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = Ξ£ π β ( 0 ..^ π ) β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
663 |
520 535 662
|
syl2anc |
β’ ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = Ξ£ π β ( 0 ..^ π ) β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
664 |
506
|
a1i |
β’ ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β ( 0 ..^ π ) β Fin ) |
665 |
69
|
adantllr |
β’ ( ( ( ( π β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( πΉ β π₯ ) β β ) |
666 |
521
|
recnd |
β’ ( π β ( π (,) +β ) β π β β ) |
667 |
666
|
adantl |
β’ ( ( π β§ π β ( π (,) +β ) ) β π β β ) |
668 |
667
|
ad2antrr |
β’ ( ( ( ( π β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π β β ) |
669 |
407
|
adantllr |
β’ ( ( ( ( π β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β π₯ β β ) |
670 |
668 669
|
mulcld |
β’ ( ( ( ( π β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( π Β· π₯ ) β β ) |
671 |
670
|
sincld |
β’ ( ( ( ( π β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( sin β ( π Β· π₯ ) ) β β ) |
672 |
665 671
|
mulcld |
β’ ( ( ( ( π β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) β β ) |
673 |
672
|
adantl3r |
β’ ( ( ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β§ π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) β ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) β β ) |
674 |
|
simplll |
β’ ( ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β π ) |
675 |
535
|
adantr |
β’ ( ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β π β β+ ) |
676 |
|
simpr |
β’ ( ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β π β ( 0 ..^ π ) ) |
677 |
674 675 676 660
|
syl21anc |
β’ ( ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β ( π₯ β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) β¦ ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) ) β πΏ1 ) |
678 |
673 677
|
itgcl |
β’ ( ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ β β ) |
679 |
664 678
|
fsumcl |
β’ ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β Ξ£ π β ( 0 ..^ π ) β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ β β ) |
680 |
663 679
|
eqeltrd |
β’ ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ β β ) |
681 |
680
|
adantllr |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β ) β§ π β ( π (,) +β ) ) β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ β β ) |
682 |
681
|
3adantl3 |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ β β ) |
683 |
682
|
abscld |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) β β ) |
684 |
678
|
abscld |
β’ ( ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) β β ) |
685 |
664 684
|
fsumrecl |
β’ ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β Ξ£ π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) β β ) |
686 |
685
|
adantllr |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β ) β§ π β ( π (,) +β ) ) β Ξ£ π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) β β ) |
687 |
686
|
3adantl3 |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β Ξ£ π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) β β ) |
688 |
|
rpre |
β’ ( π β β+ β π β β ) |
689 |
688
|
ad2antlr |
β’ ( ( ( π β§ π β β+ ) β§ π β ( π (,) +β ) ) β π β β ) |
690 |
689
|
3ad2antl1 |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β π β β ) |
691 |
663
|
fveq2d |
β’ ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) = ( abs β Ξ£ π β ( 0 ..^ π ) β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) ) |
692 |
664 678
|
fsumabs |
β’ ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β ( abs β Ξ£ π β ( 0 ..^ π ) β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) β€ Ξ£ π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) ) |
693 |
691 692
|
eqbrtrd |
β’ ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) β€ Ξ£ π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) ) |
694 |
693
|
adantllr |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β ) β§ π β ( π (,) +β ) ) β ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) β€ Ξ£ π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) ) |
695 |
694
|
3adantl3 |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) β€ Ξ£ π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) ) |
696 |
506
|
a1i |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β ( 0 ..^ π ) β Fin ) |
697 |
|
0zd |
β’ ( π β 0 β β€ ) |
698 |
4
|
nnzd |
β’ ( π β π β β€ ) |
699 |
4
|
nngt0d |
β’ ( π β 0 < π ) |
700 |
|
fzolb |
β’ ( 0 β ( 0 ..^ π ) β ( 0 β β€ β§ π β β€ β§ 0 < π ) ) |
701 |
697 698 699 700
|
syl3anbrc |
β’ ( π β 0 β ( 0 ..^ π ) ) |
702 |
|
ne0i |
β’ ( 0 β ( 0 ..^ π ) β ( 0 ..^ π ) β β
) |
703 |
701 702
|
syl |
β’ ( π β ( 0 ..^ π ) β β
) |
704 |
703
|
ad2antrr |
β’ ( ( ( π β§ π β β+ ) β§ π β ( π (,) +β ) ) β ( 0 ..^ π ) β β
) |
705 |
704
|
3ad2antl1 |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β ( 0 ..^ π ) β β
) |
706 |
|
simp1l |
β’ ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β π ) |
707 |
706
|
ad2antrr |
β’ ( ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β π ) |
708 |
|
simpll2 |
β’ ( ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β π β β ) |
709 |
707 708
|
jca |
β’ ( ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β ( π β§ π β β ) ) |
710 |
|
simplr |
β’ ( ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β π β ( π (,) +β ) ) |
711 |
|
simpr |
β’ ( ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β π β ( 0 ..^ π ) ) |
712 |
|
eleq1w |
β’ ( π = π β ( π β ( 0 ..^ π ) β π β ( 0 ..^ π ) ) ) |
713 |
712
|
anbi2d |
β’ ( π = π β ( ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) ) ) |
714 |
|
fveq2 |
β’ ( π = π β ( π β π ) = ( π β π ) ) |
715 |
|
oveq1 |
β’ ( π = π β ( π + 1 ) = ( π + 1 ) ) |
716 |
715
|
fveq2d |
β’ ( π = π β ( π β ( π + 1 ) ) = ( π β ( π + 1 ) ) ) |
717 |
714 716
|
oveq12d |
β’ ( π = π β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) = ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) |
718 |
717
|
itgeq1d |
β’ ( π = π β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
719 |
718
|
eleq1d |
β’ ( π = π β ( β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ β β β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ β β ) ) |
720 |
713 719
|
imbi12d |
β’ ( π = π β ( ( ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ β β ) β ( ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ β β ) ) ) |
721 |
720 678
|
chvarvv |
β’ ( ( ( ( π β§ π β β ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ β β ) |
722 |
709 710 711 721
|
syl21anc |
β’ ( ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ β β ) |
723 |
722
|
abscld |
β’ ( ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) β β ) |
724 |
353
|
rpred |
β’ ( ( π β§ π β β+ ) β ( π / π ) β β ) |
725 |
724
|
3ad2ant1 |
β’ ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β ( π / π ) β β ) |
726 |
725
|
ad2antrr |
β’ ( ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β ( π / π ) β β ) |
727 |
|
simpll3 |
β’ ( ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
728 |
|
rspa |
β’ ( ( β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β§ π β ( π (,) +β ) ) β β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
729 |
728
|
adantr |
β’ ( ( ( β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
730 |
718
|
fveq2d |
β’ ( π = π β ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) = ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) ) |
731 |
730
|
breq1d |
β’ ( π = π β ( ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) ) |
732 |
731
|
cbvralvw |
β’ ( β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
733 |
729 732
|
sylib |
β’ ( ( ( β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
734 |
|
rspa |
β’ ( ( β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β§ π β ( 0 ..^ π ) ) β ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
735 |
733 734
|
sylancom |
β’ ( ( ( β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
736 |
727 710 711 735
|
syl21anc |
β’ ( ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β§ π β ( 0 ..^ π ) ) β ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) |
737 |
696 705 723 726 736
|
fsumlt |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β Ξ£ π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < Ξ£ π β ( 0 ..^ π ) ( π / π ) ) |
738 |
|
fveq2 |
β’ ( π = π β ( π β π ) = ( π β π ) ) |
739 |
|
oveq1 |
β’ ( π = π β ( π + 1 ) = ( π + 1 ) ) |
740 |
739
|
fveq2d |
β’ ( π = π β ( π β ( π + 1 ) ) = ( π β ( π + 1 ) ) ) |
741 |
738 740
|
oveq12d |
β’ ( π = π β ( ( π β π ) [,] ( π β ( π + 1 ) ) ) = ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ) |
742 |
741
|
itgeq1d |
β’ ( π = π β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ = β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
743 |
742
|
fveq2d |
β’ ( π = π β ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) = ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) ) |
744 |
743
|
cbvsumv |
β’ Ξ£ π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) = Ξ£ π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) |
745 |
744
|
a1i |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β Ξ£ π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) = Ξ£ π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) ) |
746 |
353
|
rpcnd |
β’ ( ( π β§ π β β+ ) β ( π / π ) β β ) |
747 |
|
fsumconst |
β’ ( ( ( 0 ..^ π ) β Fin β§ ( π / π ) β β ) β Ξ£ π β ( 0 ..^ π ) ( π / π ) = ( ( β― β ( 0 ..^ π ) ) Β· ( π / π ) ) ) |
748 |
506 746 747
|
sylancr |
β’ ( ( π β§ π β β+ ) β Ξ£ π β ( 0 ..^ π ) ( π / π ) = ( ( β― β ( 0 ..^ π ) ) Β· ( π / π ) ) ) |
749 |
4
|
nnnn0d |
β’ ( π β π β β0 ) |
750 |
|
hashfzo0 |
β’ ( π β β0 β ( β― β ( 0 ..^ π ) ) = π ) |
751 |
749 750
|
syl |
β’ ( π β ( β― β ( 0 ..^ π ) ) = π ) |
752 |
751
|
oveq1d |
β’ ( π β ( ( β― β ( 0 ..^ π ) ) Β· ( π / π ) ) = ( π Β· ( π / π ) ) ) |
753 |
752
|
adantr |
β’ ( ( π β§ π β β+ ) β ( ( β― β ( 0 ..^ π ) ) Β· ( π / π ) ) = ( π Β· ( π / π ) ) ) |
754 |
350
|
rpcnd |
β’ ( ( π β§ π β β+ ) β π β β ) |
755 |
352
|
rpcnd |
β’ ( ( π β§ π β β+ ) β π β β ) |
756 |
352
|
rpne0d |
β’ ( ( π β§ π β β+ ) β π β 0 ) |
757 |
754 755 756
|
divcan2d |
β’ ( ( π β§ π β β+ ) β ( π Β· ( π / π ) ) = π ) |
758 |
748 753 757
|
3eqtrd |
β’ ( ( π β§ π β β+ ) β Ξ£ π β ( 0 ..^ π ) ( π / π ) = π ) |
759 |
758
|
adantr |
β’ ( ( ( π β§ π β β+ ) β§ π β ( π (,) +β ) ) β Ξ£ π β ( 0 ..^ π ) ( π / π ) = π ) |
760 |
759
|
3ad2antl1 |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β Ξ£ π β ( 0 ..^ π ) ( π / π ) = π ) |
761 |
737 745 760
|
3brtr3d |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β Ξ£ π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < π ) |
762 |
683 687 690 695 761
|
lelttrd |
β’ ( ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β§ π β ( π (,) +β ) ) β ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < π ) |
763 |
762
|
ex |
β’ ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β ( π β ( π (,) +β ) β ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < π ) ) |
764 |
519 763
|
ralrimi |
β’ ( ( ( π β§ π β β+ ) β§ π β β β§ β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β β π β ( π (,) +β ) ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < π ) |
765 |
764
|
3exp |
β’ ( ( π β§ π β β+ ) β ( π β β β ( β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β β π β ( π (,) +β ) ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < π ) ) ) |
766 |
765
|
adantr |
β’ ( ( ( π β§ π β β+ ) β§ β π β β β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β ( π β β β ( β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β β π β ( π (,) +β ) ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < π ) ) ) |
767 |
516 766
|
reximdai |
β’ ( ( ( π β§ π β β+ ) β§ β π β β β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β ( β π β β β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β β π β β β π β ( π (,) +β ) ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < π ) ) |
768 |
513 767
|
mpd |
β’ ( ( ( π β§ π β β+ ) β§ β π β β β π β ( π (,) +β ) β π β ( 0 ..^ π ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β β π β β β π β ( π (,) +β ) ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < π ) |
769 |
512 768
|
syldan |
β’ ( ( ( π β§ π β β+ ) β§ β π β ( 0 ..^ π ) β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) ) β β π β β β π β ( π (,) +β ) ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < π ) |
770 |
769
|
ex |
β’ ( ( π β§ π β β+ ) β ( β π β ( 0 ..^ π ) β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β β π β β β π β ( π (,) +β ) ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < π ) ) |
771 |
770
|
ralimdva |
β’ ( π β ( β π β β+ β π β ( 0 ..^ π ) β π β β β π β ( π (,) +β ) ( abs β β« ( ( π β π ) [,] ( π β ( π + 1 ) ) ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < ( π / π ) β β π β β+ β π β β β π β ( π (,) +β ) ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < π ) ) |
772 |
494 771
|
mpd |
β’ ( π β β π β β+ β π β β β π β ( π (,) +β ) ( abs β β« ( π΄ (,) π΅ ) ( ( πΉ β π₯ ) Β· ( sin β ( π Β· π₯ ) ) ) d π₯ ) < π ) |