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