Step | Hyp | Ref
| Expression |
1 | | fourierdlem16.f |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ) |
2 | 1 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΆ) β πΉ:ββΆβ) |
3 | | ioossre 13409 |
. . . . . . . . . . 11
β’
(-Ο(,)Ο) β β |
4 | | id 22 |
. . . . . . . . . . . 12
β’ (π₯ β πΆ β π₯ β πΆ) |
5 | | fourierdlem16.c |
. . . . . . . . . . . 12
β’ πΆ =
(-Ο(,)Ο) |
6 | 4, 5 | eleqtrdi 2838 |
. . . . . . . . . . 11
β’ (π₯ β πΆ β π₯ β (-Ο(,)Ο)) |
7 | 3, 6 | sselid 3976 |
. . . . . . . . . 10
β’ (π₯ β πΆ β π₯ β β) |
8 | 7 | adantl 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΆ) β π₯ β β) |
9 | 2, 8 | ffvelcdmd 7089 |
. . . . . . . 8
β’ ((π β§ π₯ β πΆ) β (πΉβπ₯) β β) |
10 | 9 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π₯ β πΆ) β (πΉβπ₯) β β) |
11 | | nn0re 12503 |
. . . . . . . . . . 11
β’ (π β β0
β π β
β) |
12 | 11 | adantr 480 |
. . . . . . . . . 10
β’ ((π β β0
β§ π₯ β πΆ) β π β β) |
13 | 7 | adantl 481 |
. . . . . . . . . 10
β’ ((π β β0
β§ π₯ β πΆ) β π₯ β β) |
14 | 12, 13 | remulcld 11266 |
. . . . . . . . 9
β’ ((π β β0
β§ π₯ β πΆ) β (π Β· π₯) β β) |
15 | 14 | recoscld 16112 |
. . . . . . . 8
β’ ((π β β0
β§ π₯ β πΆ) β (cosβ(π Β· π₯)) β β) |
16 | 15 | adantll 713 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π₯ β πΆ) β (cosβ(π Β· π₯)) β β) |
17 | 10, 16 | remulcld 11266 |
. . . . . 6
β’ (((π β§ π β β0) β§ π₯ β πΆ) β ((πΉβπ₯) Β· (cosβ(π Β· π₯))) β β) |
18 | | ioombl 25481 |
. . . . . . . . . . 11
β’
(-Ο(,)Ο) β dom vol |
19 | 5, 18 | eqeltri 2824 |
. . . . . . . . . 10
β’ πΆ β dom vol |
20 | 19 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β β0) β πΆ β dom
vol) |
21 | | eqidd 2728 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (cosβ(π Β· π₯))) = (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) |
22 | | eqidd 2728 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (πΉβπ₯)) = (π₯ β πΆ β¦ (πΉβπ₯))) |
23 | 20, 16, 10, 21, 22 | offval2 7699 |
. . . . . . . 8
β’ ((π β§ π β β0) β ((π₯ β πΆ β¦ (cosβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯))) = (π₯ β πΆ β¦ ((cosβ(π Β· π₯)) Β· (πΉβπ₯)))) |
24 | 16 | recnd 11264 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π₯ β πΆ) β (cosβ(π Β· π₯)) β β) |
25 | 10 | recnd 11264 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π₯ β πΆ) β (πΉβπ₯) β β) |
26 | 24, 25 | mulcomd 11257 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π₯ β πΆ) β ((cosβ(π Β· π₯)) Β· (πΉβπ₯)) = ((πΉβπ₯) Β· (cosβ(π Β· π₯)))) |
27 | 26 | mpteq2dva 5242 |
. . . . . . . 8
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ ((cosβ(π Β· π₯)) Β· (πΉβπ₯))) = (π₯ β πΆ β¦ ((πΉβπ₯) Β· (cosβ(π Β· π₯))))) |
28 | 23, 27 | eqtr2d 2768 |
. . . . . . 7
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ ((πΉβπ₯) Β· (cosβ(π Β· π₯)))) = ((π₯ β πΆ β¦ (cosβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯)))) |
29 | | coscn 26369 |
. . . . . . . . . . . 12
β’ cos
β (ββcnββ) |
30 | 29 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β0
β cos β (ββcnββ)) |
31 | 5, 3 | eqsstri 4012 |
. . . . . . . . . . . . . . 15
β’ πΆ β
β |
32 | | ax-resscn 11187 |
. . . . . . . . . . . . . . 15
β’ β
β β |
33 | 31, 32 | sstri 3987 |
. . . . . . . . . . . . . 14
β’ πΆ β
β |
34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β β0
β πΆ β
β) |
35 | 11 | recnd 11264 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β) |
36 | | ssid 4000 |
. . . . . . . . . . . . . 14
β’ β
β β |
37 | 36 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β β0
β β β β) |
38 | 34, 35, 37 | constcncfg 45183 |
. . . . . . . . . . . 12
β’ (π β β0
β (π₯ β πΆ β¦ π) β (πΆβcnββ)) |
39 | | cncfmptid 24820 |
. . . . . . . . . . . . . 14
β’ ((πΆ β β β§ β
β β) β (π₯
β πΆ β¦ π₯) β (πΆβcnββ)) |
40 | 33, 36, 39 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (π₯ β πΆ β¦ π₯) β (πΆβcnββ) |
41 | 40 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β0
β (π₯ β πΆ β¦ π₯) β (πΆβcnββ)) |
42 | 38, 41 | mulcncf 25361 |
. . . . . . . . . . 11
β’ (π β β0
β (π₯ β πΆ β¦ (π Β· π₯)) β (πΆβcnββ)) |
43 | 30, 42 | cncfmpt1f 24821 |
. . . . . . . . . 10
β’ (π β β0
β (π₯ β πΆ β¦ (cosβ(π Β· π₯))) β (πΆβcnββ)) |
44 | | cnmbf 25575 |
. . . . . . . . . 10
β’ ((πΆ β dom vol β§ (π₯ β πΆ β¦ (cosβ(π Β· π₯))) β (πΆβcnββ)) β (π₯ β πΆ β¦ (cosβ(π Β· π₯))) β MblFn) |
45 | 19, 43, 44 | sylancr 586 |
. . . . . . . . 9
β’ (π β β0
β (π₯ β πΆ β¦ (cosβ(π Β· π₯))) β MblFn) |
46 | 45 | adantl 481 |
. . . . . . . 8
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (cosβ(π Β· π₯))) β MblFn) |
47 | 1 | feqmptd 6961 |
. . . . . . . . . . . 12
β’ (π β πΉ = (π₯ β β β¦ (πΉβπ₯))) |
48 | 47 | reseq1d 5978 |
. . . . . . . . . . 11
β’ (π β (πΉ βΎ πΆ) = ((π₯ β β β¦ (πΉβπ₯)) βΎ πΆ)) |
49 | | resmpt 6035 |
. . . . . . . . . . . 12
β’ (πΆ β β β ((π₯ β β β¦ (πΉβπ₯)) βΎ πΆ) = (π₯ β πΆ β¦ (πΉβπ₯))) |
50 | 31, 49 | mp1i 13 |
. . . . . . . . . . 11
β’ (π β ((π₯ β β β¦ (πΉβπ₯)) βΎ πΆ) = (π₯ β πΆ β¦ (πΉβπ₯))) |
51 | 48, 50 | eqtr2d 2768 |
. . . . . . . . . 10
β’ (π β (π₯ β πΆ β¦ (πΉβπ₯)) = (πΉ βΎ πΆ)) |
52 | | fourierdlem16.fibl |
. . . . . . . . . 10
β’ (π β (πΉ βΎ πΆ) β
πΏ1) |
53 | 51, 52 | eqeltrd 2828 |
. . . . . . . . 9
β’ (π β (π₯ β πΆ β¦ (πΉβπ₯)) β
πΏ1) |
54 | 53 | adantr 480 |
. . . . . . . 8
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (πΉβπ₯)) β
πΏ1) |
55 | | 1re 11236 |
. . . . . . . . . 10
β’ 1 β
β |
56 | | simpr 484 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) β π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) |
57 | | nfv 1910 |
. . . . . . . . . . . . . . . 16
β’
β²π₯ π β
β0 |
58 | | nfmpt1 5250 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯(π₯ β πΆ β¦ (cosβ(π Β· π₯))) |
59 | 58 | nfdm 5947 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯dom
(π₯ β πΆ β¦ (cosβ(π Β· π₯))) |
60 | 59 | nfcri 2885 |
. . . . . . . . . . . . . . . 16
β’
β²π₯ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯))) |
61 | 57, 60 | nfan 1895 |
. . . . . . . . . . . . . . 15
β’
β²π₯(π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) |
62 | 15 | ex 412 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (π₯ β πΆ β (cosβ(π Β· π₯)) β β)) |
63 | 62 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) β (π₯ β πΆ β (cosβ(π Β· π₯)) β β)) |
64 | 61, 63 | ralrimi 3249 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) β βπ₯ β πΆ (cosβ(π Β· π₯)) β β) |
65 | | dmmptg 6240 |
. . . . . . . . . . . . . 14
β’
(βπ₯ β
πΆ (cosβ(π Β· π₯)) β β β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯))) = πΆ) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯))) = πΆ) |
67 | 56, 66 | eleqtrd 2830 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) β π¦ β πΆ) |
68 | | eqidd 2728 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π¦ β πΆ) β (π₯ β πΆ β¦ (cosβ(π Β· π₯))) = (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) |
69 | | oveq2 7422 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π¦ β (π Β· π₯) = (π Β· π¦)) |
70 | 69 | fveq2d 6895 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π¦ β (cosβ(π Β· π₯)) = (cosβ(π Β· π¦))) |
71 | 70 | adantl 481 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ π¦ β πΆ) β§ π₯ = π¦) β (cosβ(π Β· π₯)) = (cosβ(π Β· π¦))) |
72 | | simpr 484 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π¦ β πΆ) β π¦ β πΆ) |
73 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ π¦ β πΆ) β π β β) |
74 | 31, 72 | sselid 3976 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ π¦ β πΆ) β π¦ β β) |
75 | 73, 74 | remulcld 11266 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π¦ β πΆ) β (π Β· π¦) β β) |
76 | 75 | recoscld 16112 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π¦ β πΆ) β (cosβ(π Β· π¦)) β β) |
77 | 68, 71, 72, 76 | fvmptd 7006 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π¦ β πΆ) β ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦) = (cosβ(π Β· π¦))) |
78 | 77 | fveq2d 6895 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π¦ β πΆ) β (absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) = (absβ(cosβ(π Β· π¦)))) |
79 | | abscosbd 44583 |
. . . . . . . . . . . . . 14
β’ ((π Β· π¦) β β β
(absβ(cosβ(π
Β· π¦))) β€
1) |
80 | 75, 79 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π¦ β πΆ) β
(absβ(cosβ(π
Β· π¦))) β€
1) |
81 | 78, 80 | eqbrtrd 5164 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π¦ β πΆ) β (absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ 1) |
82 | 67, 81 | syldan 590 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))) β (absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ 1) |
83 | 82 | ralrimiva 3141 |
. . . . . . . . . 10
β’ (π β β0
β βπ¦ β dom
(π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ 1) |
84 | | breq2 5146 |
. . . . . . . . . . . 12
β’ (π = 1 β ((absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ π β (absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ 1)) |
85 | 84 | ralbidv 3172 |
. . . . . . . . . . 11
β’ (π = 1 β (βπ¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ π β βπ¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ 1)) |
86 | 85 | rspcev 3607 |
. . . . . . . . . 10
β’ ((1
β β β§ βπ¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ 1) β βπ β β βπ¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ π) |
87 | 55, 83, 86 | sylancr 586 |
. . . . . . . . 9
β’ (π β β0
β βπ β
β βπ¦ β
dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ π) |
88 | 87 | adantl 481 |
. . . . . . . 8
β’ ((π β§ π β β0) β
βπ β β
βπ¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ π) |
89 | | bddmulibl 25755 |
. . . . . . . 8
β’ (((π₯ β πΆ β¦ (cosβ(π Β· π₯))) β MblFn β§ (π₯ β πΆ β¦ (πΉβπ₯)) β πΏ1 β§
βπ β β
βπ¦ β dom (π₯ β πΆ β¦ (cosβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (cosβ(π Β· π₯)))βπ¦)) β€ π) β ((π₯ β πΆ β¦ (cosβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯))) β
πΏ1) |
90 | 46, 54, 88, 89 | syl3anc 1369 |
. . . . . . 7
β’ ((π β§ π β β0) β ((π₯ β πΆ β¦ (cosβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯))) β
πΏ1) |
91 | 28, 90 | eqeltrd 2828 |
. . . . . 6
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ ((πΉβπ₯) Β· (cosβ(π Β· π₯)))) β
πΏ1) |
92 | 17, 91 | itgrecl 25714 |
. . . . 5
β’ ((π β§ π β β0) β
β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ β β) |
93 | | pire 26380 |
. . . . . 6
β’ Ο
β β |
94 | 93 | a1i 11 |
. . . . 5
β’ ((π β§ π β β0) β Ο
β β) |
95 | | 0re 11238 |
. . . . . . 7
β’ 0 β
β |
96 | | pipos 26382 |
. . . . . . 7
β’ 0 <
Ο |
97 | 95, 96 | gtneii 11348 |
. . . . . 6
β’ Ο β
0 |
98 | 97 | a1i 11 |
. . . . 5
β’ ((π β§ π β β0) β Ο β
0) |
99 | 92, 94, 98 | redivcld 12064 |
. . . 4
β’ ((π β§ π β β0) β
(β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο) β β) |
100 | | fourierdlem16.a |
. . . 4
β’ π΄ = (π β β0 β¦
(β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) |
101 | 99, 100 | fmptd 7118 |
. . 3
β’ (π β π΄:β0βΆβ) |
102 | | fourierdlem16.n |
. . 3
β’ (π β π β
β0) |
103 | 101, 102 | ffvelcdmd 7089 |
. 2
β’ (π β (π΄βπ) β β) |
104 | 102 | ancli 548 |
. . 3
β’ (π β (π β§ π β
β0)) |
105 | | eleq1 2816 |
. . . . . 6
β’ (π = π β (π β β0 β π β
β0)) |
106 | 105 | anbi2d 628 |
. . . . 5
β’ (π = π β ((π β§ π β β0) β (π β§ π β
β0))) |
107 | | simpl 482 |
. . . . . . . . . 10
β’ ((π = π β§ π₯ β πΆ) β π = π) |
108 | 107 | oveq1d 7429 |
. . . . . . . . 9
β’ ((π = π β§ π₯ β πΆ) β (π Β· π₯) = (π Β· π₯)) |
109 | 108 | fveq2d 6895 |
. . . . . . . 8
β’ ((π = π β§ π₯ β πΆ) β (cosβ(π Β· π₯)) = (cosβ(π Β· π₯))) |
110 | 109 | oveq2d 7430 |
. . . . . . 7
β’ ((π = π β§ π₯ β πΆ) β ((πΉβπ₯) Β· (cosβ(π Β· π₯))) = ((πΉβπ₯) Β· (cosβ(π Β· π₯)))) |
111 | 110 | itgeq2dv 25698 |
. . . . . 6
β’ (π = π β β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ = β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯) |
112 | 111 | eleq1d 2813 |
. . . . 5
β’ (π = π β (β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ β β β β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ β β)) |
113 | 106, 112 | imbi12d 344 |
. . . 4
β’ (π = π β (((π β§ π β β0) β
β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ β β) β ((π β§ π β β0) β
β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ β β))) |
114 | 113, 92 | vtoclg 3538 |
. . 3
β’ (π β β0
β ((π β§ π β β0)
β β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ β β)) |
115 | 102, 104,
114 | sylc 65 |
. 2
β’ (π β β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ β β) |
116 | 103, 53, 115 | jca31 514 |
1
β’ (π β (((π΄βπ) β β β§ (π₯ β πΆ β¦ (πΉβπ₯)) β πΏ1) β§
β«πΆ((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ β β)) |