Step | Hyp | Ref
| Expression |
1 | | nnnn0 12425 |
. . . . . 6
β’ (π β β β π β
β0) |
2 | | fourierdlem21.f |
. . . . . . . . . . 11
β’ (π β πΉ:ββΆβ) |
3 | 2 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΆ) β πΉ:ββΆβ) |
4 | | ioossre 13331 |
. . . . . . . . . . . 12
β’
(-Ο(,)Ο) β β |
5 | | id 22 |
. . . . . . . . . . . . 13
β’ (π₯ β πΆ β π₯ β πΆ) |
6 | | fourierdlem21.c |
. . . . . . . . . . . . 13
β’ πΆ =
(-Ο(,)Ο) |
7 | 5, 6 | eleqtrdi 2844 |
. . . . . . . . . . . 12
β’ (π₯ β πΆ β π₯ β (-Ο(,)Ο)) |
8 | 4, 7 | sselid 3943 |
. . . . . . . . . . 11
β’ (π₯ β πΆ β π₯ β β) |
9 | 8 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΆ) β π₯ β β) |
10 | 3, 9 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΆ) β (πΉβπ₯) β β) |
11 | 10 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π₯ β πΆ) β (πΉβπ₯) β β) |
12 | | nn0re 12427 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
β) |
13 | 12 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π₯ β πΆ) β π β β) |
14 | 8 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π₯ β πΆ) β π₯ β β) |
15 | 13, 14 | remulcld 11190 |
. . . . . . . . . 10
β’ ((π β β0
β§ π₯ β πΆ) β (π Β· π₯) β β) |
16 | 15 | resincld 16030 |
. . . . . . . . 9
β’ ((π β β0
β§ π₯ β πΆ) β (sinβ(π Β· π₯)) β β) |
17 | 16 | adantll 713 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π₯ β πΆ) β (sinβ(π Β· π₯)) β β) |
18 | 11, 17 | remulcld 11190 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π₯ β πΆ) β ((πΉβπ₯) Β· (sinβ(π Β· π₯))) β β) |
19 | | ioombl 24945 |
. . . . . . . . . . . 12
β’
(-Ο(,)Ο) β dom vol |
20 | 6, 19 | eqeltri 2830 |
. . . . . . . . . . 11
β’ πΆ β dom vol |
21 | 20 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β πΆ β dom
vol) |
22 | | eqidd 2734 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (sinβ(π Β· π₯))) = (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) |
23 | | eqidd 2734 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (πΉβπ₯)) = (π₯ β πΆ β¦ (πΉβπ₯))) |
24 | 21, 17, 11, 22, 23 | offval2 7638 |
. . . . . . . . 9
β’ ((π β§ π β β0) β ((π₯ β πΆ β¦ (sinβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯))) = (π₯ β πΆ β¦ ((sinβ(π Β· π₯)) Β· (πΉβπ₯)))) |
25 | 17 | recnd 11188 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ π₯ β πΆ) β (sinβ(π Β· π₯)) β β) |
26 | 11 | recnd 11188 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ π₯ β πΆ) β (πΉβπ₯) β β) |
27 | 25, 26 | mulcomd 11181 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π₯ β πΆ) β ((sinβ(π Β· π₯)) Β· (πΉβπ₯)) = ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) |
28 | 27 | mpteq2dva 5206 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ ((sinβ(π Β· π₯)) Β· (πΉβπ₯))) = (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯))))) |
29 | 24, 28 | eqtr2d 2774 |
. . . . . . . 8
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) = ((π₯ β πΆ β¦ (sinβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯)))) |
30 | | sincn 25819 |
. . . . . . . . . . . 12
β’ sin
β (ββcnββ) |
31 | 30 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β sin
β (ββcnββ)) |
32 | 6, 4 | eqsstri 3979 |
. . . . . . . . . . . . . . . 16
β’ πΆ β
β |
33 | | ax-resscn 11113 |
. . . . . . . . . . . . . . . 16
β’ β
β β |
34 | 32, 33 | sstri 3954 |
. . . . . . . . . . . . . . 15
β’ πΆ β
β |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β0
β πΆ β
β) |
36 | 12 | recnd 11188 |
. . . . . . . . . . . . . 14
β’ (π β β0
β π β
β) |
37 | | ssid 3967 |
. . . . . . . . . . . . . . 15
β’ β
β β |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β0
β β β β) |
39 | 35, 36, 38 | constcncfg 44199 |
. . . . . . . . . . . . 13
β’ (π β β0
β (π₯ β πΆ β¦ π) β (πΆβcnββ)) |
40 | 35, 38 | idcncfg 44200 |
. . . . . . . . . . . . 13
β’ (π β β0
β (π₯ β πΆ β¦ π₯) β (πΆβcnββ)) |
41 | 39, 40 | mulcncf 24826 |
. . . . . . . . . . . 12
β’ (π β β0
β (π₯ β πΆ β¦ (π Β· π₯)) β (πΆβcnββ)) |
42 | 41 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (π Β· π₯)) β (πΆβcnββ)) |
43 | 31, 42 | cncfmpt1f 24293 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (sinβ(π Β· π₯))) β (πΆβcnββ)) |
44 | | cnmbf 25039 |
. . . . . . . . . 10
β’ ((πΆ β dom vol β§ (π₯ β πΆ β¦ (sinβ(π Β· π₯))) β (πΆβcnββ)) β (π₯ β πΆ β¦ (sinβ(π Β· π₯))) β MblFn) |
45 | 20, 43, 44 | sylancr 588 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (sinβ(π Β· π₯))) β MblFn) |
46 | 2 | feqmptd 6911 |
. . . . . . . . . . . . 13
β’ (π β πΉ = (π₯ β β β¦ (πΉβπ₯))) |
47 | 46 | reseq1d 5937 |
. . . . . . . . . . . 12
β’ (π β (πΉ βΎ πΆ) = ((π₯ β β β¦ (πΉβπ₯)) βΎ πΆ)) |
48 | | resmpt 5992 |
. . . . . . . . . . . . 13
β’ (πΆ β β β ((π₯ β β β¦ (πΉβπ₯)) βΎ πΆ) = (π₯ β πΆ β¦ (πΉβπ₯))) |
49 | 32, 48 | mp1i 13 |
. . . . . . . . . . . 12
β’ (π β ((π₯ β β β¦ (πΉβπ₯)) βΎ πΆ) = (π₯ β πΆ β¦ (πΉβπ₯))) |
50 | 47, 49 | eqtr2d 2774 |
. . . . . . . . . . 11
β’ (π β (π₯ β πΆ β¦ (πΉβπ₯)) = (πΉ βΎ πΆ)) |
51 | | fourierdlem21.fibl |
. . . . . . . . . . 11
β’ (π β (πΉ βΎ πΆ) β
πΏ1) |
52 | 50, 51 | eqeltrd 2834 |
. . . . . . . . . 10
β’ (π β (π₯ β πΆ β¦ (πΉβπ₯)) β
πΏ1) |
53 | 52 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ (πΉβπ₯)) β
πΏ1) |
54 | | 1re 11160 |
. . . . . . . . . . 11
β’ 1 β
β |
55 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) β π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) |
56 | | nfv 1918 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯ π β
β0 |
57 | | nfmpt1 5214 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯(π₯ β πΆ β¦ (sinβ(π Β· π₯))) |
58 | 57 | nfdm 5907 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯dom
(π₯ β πΆ β¦ (sinβ(π Β· π₯))) |
59 | 58 | nfcri 2891 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯))) |
60 | 56, 59 | nfan 1903 |
. . . . . . . . . . . . . . . 16
β’
β²π₯(π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) |
61 | 16 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (π₯ β πΆ β (sinβ(π Β· π₯)) β β)) |
62 | 61 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) β (π₯ β πΆ β (sinβ(π Β· π₯)) β β)) |
63 | 60, 62 | ralrimi 3239 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) β βπ₯ β πΆ (sinβ(π Β· π₯)) β β) |
64 | | dmmptg 6195 |
. . . . . . . . . . . . . . 15
β’
(βπ₯ β
πΆ (sinβ(π Β· π₯)) β β β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯))) = πΆ) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯))) = πΆ) |
66 | 55, 65 | eleqtrd 2836 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) β π¦ β πΆ) |
67 | | eqidd 2734 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π¦ β πΆ) β (π₯ β πΆ β¦ (sinβ(π Β· π₯))) = (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) |
68 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β (π Β· π₯) = (π Β· π¦)) |
69 | 68 | fveq2d 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π¦ β (sinβ(π Β· π₯)) = (sinβ(π Β· π¦))) |
70 | 69 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ π¦ β πΆ) β§ π₯ = π¦) β (sinβ(π Β· π₯)) = (sinβ(π Β· π¦))) |
71 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π¦ β πΆ) β π¦ β πΆ) |
72 | 12 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β0
β§ π¦ β πΆ) β π β β) |
73 | 32, 71 | sselid 3943 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β0
β§ π¦ β πΆ) β π¦ β β) |
74 | 72, 73 | remulcld 11190 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ π¦ β πΆ) β (π Β· π¦) β β) |
75 | 74 | resincld 16030 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π¦ β πΆ) β (sinβ(π Β· π¦)) β β) |
76 | 67, 70, 71, 75 | fvmptd 6956 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π¦ β πΆ) β ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦) = (sinβ(π Β· π¦))) |
77 | 76 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π¦ β πΆ) β (absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) = (absβ(sinβ(π Β· π¦)))) |
78 | | abssinbd 43616 |
. . . . . . . . . . . . . . 15
β’ ((π Β· π¦) β β β
(absβ(sinβ(π
Β· π¦))) β€
1) |
79 | 74, 78 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π¦ β πΆ) β
(absβ(sinβ(π
Β· π¦))) β€
1) |
80 | 77, 79 | eqbrtrd 5128 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π¦ β πΆ) β (absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ 1) |
81 | 66, 80 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))) β (absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ 1) |
82 | 81 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ (π β β0
β βπ¦ β dom
(π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ 1) |
83 | | breq2 5110 |
. . . . . . . . . . . . 13
β’ (π = 1 β ((absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ π β (absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ 1)) |
84 | 83 | ralbidv 3171 |
. . . . . . . . . . . 12
β’ (π = 1 β (βπ¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ π β βπ¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ 1)) |
85 | 84 | rspcev 3580 |
. . . . . . . . . . 11
β’ ((1
β β β§ βπ¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ 1) β βπ β β βπ¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ π) |
86 | 54, 82, 85 | sylancr 588 |
. . . . . . . . . 10
β’ (π β β0
β βπ β
β βπ¦ β
dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ π) |
87 | 86 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β β0) β
βπ β β
βπ¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ π) |
88 | | bddmulibl 25219 |
. . . . . . . . 9
β’ (((π₯ β πΆ β¦ (sinβ(π Β· π₯))) β MblFn β§ (π₯ β πΆ β¦ (πΉβπ₯)) β πΏ1 β§
βπ β β
βπ¦ β dom (π₯ β πΆ β¦ (sinβ(π Β· π₯)))(absβ((π₯ β πΆ β¦ (sinβ(π Β· π₯)))βπ¦)) β€ π) β ((π₯ β πΆ β¦ (sinβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯))) β
πΏ1) |
89 | 45, 53, 87, 88 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β β0) β ((π₯ β πΆ β¦ (sinβ(π Β· π₯))) βf Β· (π₯ β πΆ β¦ (πΉβπ₯))) β
πΏ1) |
90 | 29, 89 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β
πΏ1) |
91 | 18, 90 | itgrecl 25178 |
. . . . . 6
β’ ((π β§ π β β0) β
β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ β β) |
92 | 1, 91 | sylan2 594 |
. . . . 5
β’ ((π β§ π β β) β β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ β β) |
93 | | pire 25831 |
. . . . . 6
β’ Ο
β β |
94 | 93 | a1i 11 |
. . . . 5
β’ ((π β§ π β β) β Ο β
β) |
95 | | 0re 11162 |
. . . . . . 7
β’ 0 β
β |
96 | | pipos 25833 |
. . . . . . 7
β’ 0 <
Ο |
97 | 95, 96 | gtneii 11272 |
. . . . . 6
β’ Ο β
0 |
98 | 97 | a1i 11 |
. . . . 5
β’ ((π β§ π β β) β Ο β
0) |
99 | 92, 94, 98 | redivcld 11988 |
. . . 4
β’ ((π β§ π β β) β (β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο) β β) |
100 | | fourierdlem21.b |
. . . 4
β’ π΅ = (π β β β¦ (β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) |
101 | 99, 100 | fmptd 7063 |
. . 3
β’ (π β π΅:ββΆβ) |
102 | | fourierdlem21.n |
. . 3
β’ (π β π β β) |
103 | 101, 102 | ffvelcdmd 7037 |
. 2
β’ (π β (π΅βπ) β β) |
104 | 102 | nnnn0d 12478 |
. . 3
β’ (π β π β
β0) |
105 | | eleq1 2822 |
. . . . . . 7
β’ (π = π β (π β β0 β π β
β0)) |
106 | 105 | anbi2d 630 |
. . . . . 6
β’ (π = π β ((π β§ π β β0) β (π β§ π β
β0))) |
107 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π = π β§ π₯ β πΆ) β π = π) |
108 | 107 | oveq1d 7373 |
. . . . . . . . . 10
β’ ((π = π β§ π₯ β πΆ) β (π Β· π₯) = (π Β· π₯)) |
109 | 108 | fveq2d 6847 |
. . . . . . . . 9
β’ ((π = π β§ π₯ β πΆ) β (sinβ(π Β· π₯)) = (sinβ(π Β· π₯))) |
110 | 109 | oveq2d 7374 |
. . . . . . . 8
β’ ((π = π β§ π₯ β πΆ) β ((πΉβπ₯) Β· (sinβ(π Β· π₯))) = ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) |
111 | 110 | mpteq2dva 5206 |
. . . . . . 7
β’ (π = π β (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) = (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯))))) |
112 | 111 | eleq1d 2819 |
. . . . . 6
β’ (π = π β ((π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β πΏ1 β
(π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β
πΏ1)) |
113 | 106, 112 | imbi12d 345 |
. . . . 5
β’ (π = π β (((π β§ π β β0) β (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β πΏ1) β
((π β§ π β β0) β (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β
πΏ1))) |
114 | 113, 90 | vtoclg 3524 |
. . . 4
β’ (π β β0
β ((π β§ π β β0)
β (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β
πΏ1)) |
115 | 114 | anabsi7 670 |
. . 3
β’ ((π β§ π β β0) β (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β
πΏ1) |
116 | 104, 115 | mpdan 686 |
. 2
β’ (π β (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β
πΏ1) |
117 | 102 | ancli 550 |
. . 3
β’ (π β (π β§ π β β)) |
118 | | eleq1 2822 |
. . . . . 6
β’ (π = π β (π β β β π β β)) |
119 | 118 | anbi2d 630 |
. . . . 5
β’ (π = π β ((π β§ π β β) β (π β§ π β β))) |
120 | 110 | itgeq2dv 25162 |
. . . . . 6
β’ (π = π β β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ = β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯) |
121 | 120 | eleq1d 2819 |
. . . . 5
β’ (π = π β (β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ β β β β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ β β)) |
122 | 119, 121 | imbi12d 345 |
. . . 4
β’ (π = π β (((π β§ π β β) β β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ β β) β ((π β§ π β β) β β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ β β))) |
123 | 122, 92 | vtoclg 3524 |
. . 3
β’ (π β β β ((π β§ π β β) β β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ β β)) |
124 | 102, 117,
123 | sylc 65 |
. 2
β’ (π β β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ β β) |
125 | 103, 116,
124 | jca31 516 |
1
β’ (π β (((π΅βπ) β β β§ (π₯ β πΆ β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β πΏ1) β§
β«πΆ((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ β β)) |