Step | Hyp | Ref
| Expression |
1 | | fourierdlem22.f |
. . . . . . . . . . 11
β’ (π β πΉ:ββΆβ) |
2 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΆ) β πΉ:ββΆβ) |
3 | | ioossre 13331 |
. . . . . . . . . . . 12
β’
(-Ο(,)Ο) β β |
4 | | id 22 |
. . . . . . . . . . . . 13
β’ (π₯ β πΆ β π₯ β πΆ) |
5 | | fourierdlem22.c |
. . . . . . . . . . . . 13
β’ πΆ =
(-Ο(,)Ο) |
6 | 4, 5 | eleqtrdi 2844 |
. . . . . . . . . . . 12
β’ (π₯ β πΆ β π₯ β (-Ο(,)Ο)) |
7 | 3, 6 | sselid 3943 |
. . . . . . . . . . 11
β’ (π₯ β πΆ β π₯ β β) |
8 | 7 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΆ) β π₯ β β) |
9 | 2, 8 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΆ) β (πΉβπ₯) β β) |
10 | 9 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π₯ β πΆ) β (πΉβπ₯) β β) |
11 | | nn0re 12427 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
β) |
12 | 11 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π₯ β πΆ) β π β β) |
13 | 7 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π₯ β πΆ) β π₯ β β) |
14 | 12, 13 | remulcld 11190 |
. . . . . . . . . 10
β’ ((π β β0
β§ π₯ β πΆ) β (π Β· π₯) β β) |
15 | 14 | recoscld 16031 |
. . . . . . . . 9
β’ ((π β β0
β§ π₯ β πΆ) β (cosβ(π Β· π₯)) β β) |
16 | 15 | adantll 713 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π₯ β πΆ) β (cosβ(π Β· π₯)) β β) |
17 | 10, 16 | remulcld 11190 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π₯ β πΆ) β ((πΉβπ₯) Β· (cosβ(π Β· π₯))) β β) |
18 | | ioombl 24945 |
. . . . . . . . . . . 12
β’
(-Ο(,)Ο) β dom vol |
19 | 5, 18 | eqeltri 2830 |
. . . . . . . . . . 11
β’ πΆ β dom vol |
20 | 19 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β πΆ β dom
vol) |
21 | | eqidd 2734 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (cosβ(π Β· π₯))) = (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) |
22 | | eqidd 2734 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (πΉβπ₯)) = (π₯ β πΆ β¦ (πΉβπ₯))) |
23 | 20, 16, 10, 21, 22 | offval2 7638 |
. . . . . . . . 9
β’ ((π β§ π β β0) β ((π₯ β πΆ β¦ (cosβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯))) = (π₯ β πΆ β¦ ((cosβ(π Β· π₯)) Β· (πΉβπ₯)))) |
24 | 16 | recnd 11188 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ π₯ β πΆ) β (cosβ(π Β· π₯)) β β) |
25 | 10 | recnd 11188 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ π₯ β πΆ) β (πΉβπ₯) β β) |
26 | 24, 25 | mulcomd 11181 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π₯ β πΆ) β ((cosβ(π Β· π₯)) Β· (πΉβπ₯)) = ((πΉβπ₯) Β· (cosβ(π Β· π₯)))) |
27 | 26 | mpteq2dva 5206 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ ((cosβ(π Β· π₯)) Β· (πΉβπ₯))) = (π₯ β πΆ β¦ ((πΉβπ₯) Β· (cosβ(π Β· π₯))))) |
28 | 23, 27 | eqtr2d 2774 |
. . . . . . . 8
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ ((πΉβπ₯) Β· (cosβ(π Β· π₯)))) = ((π₯ β πΆ β¦ (cosβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯)))) |
29 | | coscn 25820 |
. . . . . . . . . . . . 13
β’ cos
β (ββcnββ) |
30 | 29 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β0
β cos β (ββcnββ)) |
31 | 5, 3 | eqsstri 3979 |
. . . . . . . . . . . . . . . 16
β’ πΆ β
β |
32 | | ax-resscn 11113 |
. . . . . . . . . . . . . . . 16
β’ β
β β |
33 | 31, 32 | sstri 3954 |
. . . . . . . . . . . . . . 15
β’ πΆ β
β |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β0
β πΆ β
β) |
35 | 11 | recnd 11188 |
. . . . . . . . . . . . . 14
β’ (π β β0
β π β
β) |
36 | | ssid 3967 |
. . . . . . . . . . . . . . 15
β’ β
β β |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β0
β β β β) |
38 | 34, 35, 37 | constcncfg 44199 |
. . . . . . . . . . . . 13
β’ (π β β0
β (π₯ β πΆ β¦ π) β (πΆβcnββ)) |
39 | | cncfmptid 24292 |
. . . . . . . . . . . . . . 15
β’ ((πΆ β β β§ β
β β) β (π₯
β πΆ β¦ π₯) β (πΆβcnββ)) |
40 | 33, 36, 39 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (π₯ β πΆ β¦ π₯) β (πΆβcnββ) |
41 | 40 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β β0
β (π₯ β πΆ β¦ π₯) β (πΆβcnββ)) |
42 | 38, 41 | mulcncf 24826 |
. . . . . . . . . . . 12
β’ (π β β0
β (π₯ β πΆ β¦ (π Β· π₯)) β (πΆβcnββ)) |
43 | 30, 42 | cncfmpt1f 24293 |
. . . . . . . . . . 11
β’ (π β β0
β (π₯ β πΆ β¦ (cosβ(π Β· π₯))) β (πΆβcnββ)) |
44 | | cnmbf 25039 |
. . . . . . . . . . 11
β’ ((πΆ β dom vol β§ (π₯ β πΆ β¦ (cosβ(π Β· π₯))) β (πΆβcnββ)) β (π₯ β πΆ β¦ (cosβ(π Β· π₯))) β MblFn) |
45 | 19, 43, 44 | sylancr 588 |
. . . . . . . . . 10
β’ (π β β0
β (π₯ β πΆ β¦ (cosβ(π Β· π₯))) β MblFn) |
46 | 45 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (cosβ(π Β· π₯))) β MblFn) |
47 | 1 | feqmptd 6911 |
. . . . . . . . . . . . 13
β’ (π β πΉ = (π₯ β β β¦ (πΉβπ₯))) |
48 | 47 | reseq1d 5937 |
. . . . . . . . . . . 12
β’ (π β (πΉ βΎ πΆ) = ((π₯ β β β¦ (πΉβπ₯)) βΎ πΆ)) |
49 | | resmpt 5992 |
. . . . . . . . . . . . 13
β’ (πΆ β β β ((π₯ β β β¦ (πΉβπ₯)) βΎ πΆ) = (π₯ β πΆ β¦ (πΉβπ₯))) |
50 | 31, 49 | mp1i 13 |
. . . . . . . . . . . 12
β’ (π β ((π₯ β β β¦ (πΉβπ₯)) βΎ πΆ) = (π₯ β πΆ β¦ (πΉβπ₯))) |
51 | 48, 50 | eqtr2d 2774 |
. . . . . . . . . . 11
β’ (π β (π₯ β πΆ β¦ (πΉβπ₯)) = (πΉ βΎ πΆ)) |
52 | | fourierdlem22.fibl |
. . . . . . . . . . 11
β’ (π β (πΉ βΎ πΆ) β
πΏ1) |
53 | 51, 52 | eqeltrd 2834 |
. . . . . . . . . 10
β’ (π β (π₯ β πΆ β¦ (πΉβπ₯)) β
πΏ1) |
54 | 53 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (πΉβπ₯)) β
πΏ1) |
55 | | 1re 11160 |
. . . . . . . . . . 11
β’ 1 β
β |
56 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) β π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) |
57 | | nfv 1918 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯ π β
β0 |
58 | | nfmpt1 5214 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯(π₯ β πΆ β¦ (cosβ(π Β· π₯))) |
59 | 58 | nfdm 5907 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯dom
(π₯ β πΆ β¦ (cosβ(π Β· π₯))) |
60 | 59 | nfcri 2891 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯))) |
61 | 57, 60 | nfan 1903 |
. . . . . . . . . . . . . . . 16
β’
β²π₯(π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) |
62 | 15 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (π₯ β πΆ β (cosβ(π Β· π₯)) β β)) |
63 | 62 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) β (π₯ β πΆ β (cosβ(π Β· π₯)) β β)) |
64 | 61, 63 | ralrimi 3239 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) β βπ₯ β πΆ (cosβ(π Β· π₯)) β β) |
65 | | dmmptg 6195 |
. . . . . . . . . . . . . . 15
β’
(βπ₯ β
πΆ (cosβ(π Β· π₯)) β β β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯))) = πΆ) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯))) = πΆ) |
67 | 56, 66 | eleqtrd 2836 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) β π¦ β πΆ) |
68 | | eqidd 2734 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π¦ β πΆ) β (π₯ β πΆ β¦ (cosβ(π Β· π₯))) = (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) |
69 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β (π Β· π₯) = (π Β· π¦)) |
70 | 69 | fveq2d 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π¦ β (cosβ(π Β· π₯)) = (cosβ(π Β· π¦))) |
71 | 70 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ π¦ β πΆ) β§ π₯ = π¦) β (cosβ(π Β· π₯)) = (cosβ(π Β· π¦))) |
72 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π¦ β πΆ) β π¦ β πΆ) |
73 | 11 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β0
β§ π¦ β πΆ) β π β β) |
74 | 31, 72 | sselid 3943 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β0
β§ π¦ β πΆ) β π¦ β β) |
75 | 73, 74 | remulcld 11190 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ π¦ β πΆ) β (π Β· π¦) β β) |
76 | 75 | recoscld 16031 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π¦ β πΆ) β (cosβ(π Β· π¦)) β β) |
77 | 68, 71, 72, 76 | fvmptd 6956 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π¦ β πΆ) β ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦) = (cosβ(π Β· π¦))) |
78 | 77 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π¦ β πΆ) β (absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) = (absβ(cosβ(π Β· π¦)))) |
79 | | abscosbd 43599 |
. . . . . . . . . . . . . . 15
β’ ((π Β· π¦) β β β
(absβ(cosβ(π
Β· π¦))) β€
1) |
80 | 75, 79 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π¦ β πΆ) β
(absβ(cosβ(π
Β· π¦))) β€
1) |
81 | 78, 80 | eqbrtrd 5128 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π¦ β πΆ) β (absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ 1) |
82 | 67, 81 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) β (absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ 1) |
83 | 82 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ (π β β0
β βπ¦ β dom
(π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ 1) |
84 | | breq2 5110 |
. . . . . . . . . . . . 13
β’ (π = 1 β ((absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ π β (absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ 1)) |
85 | 84 | ralbidv 3171 |
. . . . . . . . . . . 12
β’ (π = 1 β (βπ¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ π β βπ¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ 1)) |
86 | 85 | rspcev 3580 |
. . . . . . . . . . 11
β’ ((1
β β β§ βπ¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ 1) β βπ β β βπ¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ π) |
87 | 55, 83, 86 | sylancr 588 |
. . . . . . . . . 10
β’ (π β β0
β βπ β
β βπ¦ β
dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ π) |
88 | 87 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β β0) β
βπ β β
βπ¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ π) |
89 | | bddmulibl 25219 |
. . . . . . . . 9
β’ (((π₯ β πΆ β¦ (cosβ(π Β· π₯))) β MblFn β§ (π₯ β πΆ β¦ (πΉβπ₯)) β πΏ1 β§
βπ β β
βπ¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ π) β ((π₯ β πΆ β¦ (cosβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯))) β
πΏ1) |
90 | 46, 54, 88, 89 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β β0) β ((π₯ β πΆ β¦ (cosβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯))) β
πΏ1) |
91 | 28, 90 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ ((πΉβπ₯) Β· (cosβ(π Β· π₯)))) β
πΏ1) |
92 | 17, 91 | itgrecl 25178 |
. . . . . 6
β’ ((π β§ π β β0) β
β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ β β) |
93 | | pire 25831 |
. . . . . . 7
β’ Ο
β β |
94 | 93 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β0) β Ο
β β) |
95 | | 0re 11162 |
. . . . . . . 8
β’ 0 β
β |
96 | | pipos 25833 |
. . . . . . . 8
β’ 0 <
Ο |
97 | 95, 96 | gtneii 11272 |
. . . . . . 7
β’ Ο β
0 |
98 | 97 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β0) β Ο β
0) |
99 | 92, 94, 98 | redivcld 11988 |
. . . . 5
β’ ((π β§ π β β0) β
(β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο) β β) |
100 | | fourierdlem22.a |
. . . . 5
β’ π΄ = (π β β0 β¦
(β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) |
101 | 99, 100 | fmptd 7063 |
. . . 4
β’ (π β π΄:β0βΆβ) |
102 | 101 | ffvelcdmda 7036 |
. . 3
β’ ((π β§ π β β0) β (π΄βπ) β β) |
103 | 102 | ex 414 |
. 2
β’ (π β (π β β0 β (π΄βπ) β β)) |
104 | | nnnn0 12425 |
. . . . . . 7
β’ (π β β β π β
β0) |
105 | 14 | resincld 16030 |
. . . . . . . . . 10
β’ ((π β β0
β§ π₯ β πΆ) β (sinβ(π Β· π₯)) β β) |
106 | 105 | adantll 713 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π₯ β πΆ) β (sinβ(π Β· π₯)) β β) |
107 | 10, 106 | remulcld 11190 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π₯ β πΆ) β ((πΉβπ₯) Β· (sinβ(π Β· π₯))) β β) |
108 | | eqidd 2734 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (sinβ(π Β· π₯))) = (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) |
109 | 20, 106, 10, 108, 22 | offval2 7638 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β ((π₯ β πΆ β¦ (sinβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯))) = (π₯ β πΆ β¦ ((sinβ(π Β· π₯)) Β· (πΉβπ₯)))) |
110 | 106 | recnd 11188 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ π₯ β πΆ) β (sinβ(π Β· π₯)) β β) |
111 | 110, 25 | mulcomd 11181 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ π₯ β πΆ) β ((sinβ(π Β· π₯)) Β· (πΉβπ₯)) = ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) |
112 | 111 | mpteq2dva 5206 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ ((sinβ(π Β· π₯)) Β· (πΉβπ₯))) = (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯))))) |
113 | 109, 112 | eqtr2d 2774 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) = ((π₯ β πΆ β¦ (sinβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯)))) |
114 | | sincn 25819 |
. . . . . . . . . . . . 13
β’ sin
β (ββcnββ) |
115 | 114 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β sin
β (ββcnββ)) |
116 | 42 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (π Β· π₯)) β (πΆβcnββ)) |
117 | 115, 116 | cncfmpt1f 24293 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (sinβ(π Β· π₯))) β (πΆβcnββ)) |
118 | | cnmbf 25039 |
. . . . . . . . . . 11
β’ ((πΆ β dom vol β§ (π₯ β πΆ β¦ (sinβ(π Β· π₯))) β (πΆβcnββ)) β (π₯ β πΆ β¦ (sinβ(π Β· π₯))) β MblFn) |
119 | 19, 117, 118 | sylancr 588 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (sinβ(π Β· π₯))) β MblFn) |
120 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) β π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) |
121 | | nfmpt1 5214 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯(π₯ β πΆ β¦ (sinβ(π Β· π₯))) |
122 | 121 | nfdm 5907 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯dom
(π₯ β πΆ β¦ (sinβ(π Β· π₯))) |
123 | 122 | nfcri 2891 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯))) |
124 | 57, 123 | nfan 1903 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯(π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) |
125 | 105 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (π₯ β πΆ β (sinβ(π Β· π₯)) β β)) |
126 | 125 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) β (π₯ β πΆ β (sinβ(π Β· π₯)) β β)) |
127 | 124, 126 | ralrimi 3239 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) β βπ₯ β πΆ (sinβ(π Β· π₯)) β β) |
128 | | dmmptg 6195 |
. . . . . . . . . . . . . . . 16
β’
(βπ₯ β
πΆ (sinβ(π Β· π₯)) β β β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯))) = πΆ) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯))) = πΆ) |
130 | 120, 129 | eleqtrd 2836 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) β π¦ β πΆ) |
131 | | eqidd 2734 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ π¦ β πΆ) β (π₯ β πΆ β¦ (sinβ(π Β· π₯))) = (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) |
132 | 69 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β (sinβ(π Β· π₯)) = (sinβ(π Β· π¦))) |
133 | 132 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β0
β§ π¦ β πΆ) β§ π₯ = π¦) β (sinβ(π Β· π₯)) = (sinβ(π Β· π¦))) |
134 | 75 | resincld 16030 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ π¦ β πΆ) β (sinβ(π Β· π¦)) β β) |
135 | 131, 133,
72, 134 | fvmptd 6956 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π¦ β πΆ) β ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦) = (sinβ(π Β· π¦))) |
136 | 135 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π¦ β πΆ) β (absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) = (absβ(sinβ(π Β· π¦)))) |
137 | | abssinbd 43616 |
. . . . . . . . . . . . . . . 16
β’ ((π Β· π¦) β β β
(absβ(sinβ(π
Β· π¦))) β€
1) |
138 | 75, 137 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π¦ β πΆ) β
(absβ(sinβ(π
Β· π¦))) β€
1) |
139 | 136, 138 | eqbrtrd 5128 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π¦ β πΆ) β (absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ 1) |
140 | 130, 139 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) β (absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ 1) |
141 | 140 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ (π β β0
β βπ¦ β dom
(π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ 1) |
142 | | breq2 5110 |
. . . . . . . . . . . . . 14
β’ (π = 1 β ((absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ π β (absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ 1)) |
143 | 142 | ralbidv 3171 |
. . . . . . . . . . . . 13
β’ (π = 1 β (βπ¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ π β βπ¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ 1)) |
144 | 143 | rspcev 3580 |
. . . . . . . . . . . 12
β’ ((1
β β β§ βπ¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ 1) β βπ β β βπ¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ π) |
145 | 55, 141, 144 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β β0
β βπ β
β βπ¦ β
dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ π) |
146 | 145 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β
βπ β β
βπ¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ π) |
147 | | bddmulibl 25219 |
. . . . . . . . . 10
β’ (((π₯ β πΆ β¦ (sinβ(π Β· π₯))) β MblFn β§ (π₯ β πΆ β¦ (πΉβπ₯)) β πΏ1 β§
βπ β β
βπ¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ π) β ((π₯ β πΆ β¦ (sinβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯))) β
πΏ1) |
148 | 119, 54, 146, 147 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β β0) β ((π₯ β πΆ β¦ (sinβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯))) β
πΏ1) |
149 | 113, 148 | eqeltrd 2834 |
. . . . . . . 8
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β
πΏ1) |
150 | 107, 149 | itgrecl 25178 |
. . . . . . 7
β’ ((π β§ π β β0) β
β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ β β) |
151 | 104, 150 | sylan2 594 |
. . . . . 6
β’ ((π β§ π β β) β β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ β β) |
152 | 93 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β) β Ο β
β) |
153 | 97 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β) β Ο β
0) |
154 | 151, 152,
153 | redivcld 11988 |
. . . . 5
β’ ((π β§ π β β) β (β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο) β β) |
155 | | fourierdlem22.b |
. . . . 5
β’ π΅ = (π β β β¦ (β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) |
156 | 154, 155 | fmptd 7063 |
. . . 4
β’ (π β π΅:ββΆβ) |
157 | 156 | ffvelcdmda 7036 |
. . 3
β’ ((π β§ π β β) β (π΅βπ) β β) |
158 | 157 | ex 414 |
. 2
β’ (π β (π β β β (π΅βπ) β β)) |
159 | 103, 158 | jca 513 |
1
β’ (π β ((π β β0 β (π΄βπ) β β) β§ (π β β β (π΅βπ) β β))) |