Step | Hyp | Ref
| Expression |
1 | | fourierdlem47.m |
. . 3
โข ๐ = ((โโ((((๐ + ๐) + ๐) / ๐ธ) + 1)) + 1) |
2 | | fourierdlem47.x |
. . . . . . . . . . 11
โข ๐ = (absโ๐ด) |
3 | | fourierdlem47.a |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โ) |
4 | 3 | abscld 15388 |
. . . . . . . . . . 11
โข (๐ โ (absโ๐ด) โ
โ) |
5 | 2, 4 | eqeltrid 2836 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
6 | | fourierdlem47.y |
. . . . . . . . . . 11
โข ๐ = (absโ๐ถ) |
7 | | fourierdlem47.c |
. . . . . . . . . . . 12
โข (๐ โ ๐ถ โ โ) |
8 | 7 | abscld 15388 |
. . . . . . . . . . 11
โข (๐ โ (absโ๐ถ) โ
โ) |
9 | 6, 8 | eqeltrid 2836 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
10 | 5, 9 | readdcld 11248 |
. . . . . . . . 9
โข (๐ โ (๐ + ๐) โ โ) |
11 | | fourierdlem47.z |
. . . . . . . . . 10
โข ๐ = โซ๐ผ(absโ๐น) d๐ฅ |
12 | | fourierdlem47.f |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ผ) โ ๐น โ โ) |
13 | 12 | abscld 15388 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ผ) โ (absโ๐น) โ โ) |
14 | | fourierdlem47.ibl |
. . . . . . . . . . . 12
โข (๐ โ (๐ฅ โ ๐ผ โฆ ๐น) โ
๐ฟ1) |
15 | 12, 14 | iblabs 25579 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ ๐ผ โฆ (absโ๐น)) โ
๐ฟ1) |
16 | 13, 15 | itgrecl 25548 |
. . . . . . . . . 10
โข (๐ โ โซ๐ผ(absโ๐น) d๐ฅ โ โ) |
17 | 11, 16 | eqeltrid 2836 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
18 | 10, 17 | readdcld 11248 |
. . . . . . . 8
โข (๐ โ ((๐ + ๐) + ๐) โ โ) |
19 | | fourierdlem47.e |
. . . . . . . . 9
โข (๐ โ ๐ธ โ
โ+) |
20 | 19 | rpred 13021 |
. . . . . . . 8
โข (๐ โ ๐ธ โ โ) |
21 | 19 | rpne0d 13026 |
. . . . . . . 8
โข (๐ โ ๐ธ โ 0) |
22 | 18, 20, 21 | redivcld 12047 |
. . . . . . 7
โข (๐ โ (((๐ + ๐) + ๐) / ๐ธ) โ โ) |
23 | | 1red 11220 |
. . . . . . 7
โข (๐ โ 1 โ
โ) |
24 | 22, 23 | readdcld 11248 |
. . . . . 6
โข (๐ โ ((((๐ + ๐) + ๐) / ๐ธ) + 1) โ โ) |
25 | 24 | flcld 13768 |
. . . . 5
โข (๐ โ (โโ((((๐ + ๐) + ๐) / ๐ธ) + 1)) โ โค) |
26 | | 0red 11222 |
. . . . . 6
โข (๐ โ 0 โ
โ) |
27 | | reflcl 13766 |
. . . . . . 7
โข
(((((๐ + ๐) + ๐) / ๐ธ) + 1) โ โ โ
(โโ((((๐ +
๐) + ๐) / ๐ธ) + 1)) โ โ) |
28 | 24, 27 | syl 17 |
. . . . . 6
โข (๐ โ (โโ((((๐ + ๐) + ๐) / ๐ธ) + 1)) โ โ) |
29 | | 0lt1 11741 |
. . . . . . 7
โข 0 <
1 |
30 | 29 | a1i 11 |
. . . . . 6
โข (๐ โ 0 < 1) |
31 | 3 | absge0d 15396 |
. . . . . . . . . . . . 13
โข (๐ โ 0 โค (absโ๐ด)) |
32 | 31, 2 | breqtrrdi 5190 |
. . . . . . . . . . . 12
โข (๐ โ 0 โค ๐) |
33 | 7 | absge0d 15396 |
. . . . . . . . . . . . 13
โข (๐ โ 0 โค (absโ๐ถ)) |
34 | 33, 6 | breqtrrdi 5190 |
. . . . . . . . . . . 12
โข (๐ โ 0 โค ๐) |
35 | 5, 9, 32, 34 | addge0d 11795 |
. . . . . . . . . . 11
โข (๐ โ 0 โค (๐ + ๐)) |
36 | 12 | absge0d 15396 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ผ) โ 0 โค (absโ๐น)) |
37 | 15, 13, 36 | itgge0 25561 |
. . . . . . . . . . . 12
โข (๐ โ 0 โค โซ๐ผ(absโ๐น) d๐ฅ) |
38 | 37, 11 | breqtrrdi 5190 |
. . . . . . . . . . 11
โข (๐ โ 0 โค ๐) |
39 | 10, 17, 35, 38 | addge0d 11795 |
. . . . . . . . . 10
โข (๐ โ 0 โค ((๐ + ๐) + ๐)) |
40 | 18, 19, 39 | divge0d 13061 |
. . . . . . . . 9
โข (๐ โ 0 โค (((๐ + ๐) + ๐) / ๐ธ)) |
41 | | flge0nn0 13790 |
. . . . . . . . 9
โข
(((((๐ + ๐) + ๐) / ๐ธ) โ โ โง 0 โค (((๐ + ๐) + ๐) / ๐ธ)) โ (โโ(((๐ + ๐) + ๐) / ๐ธ)) โ
โ0) |
42 | 22, 40, 41 | syl2anc 583 |
. . . . . . . 8
โข (๐ โ (โโ(((๐ + ๐) + ๐) / ๐ธ)) โ
โ0) |
43 | | nn0addge1 12523 |
. . . . . . . 8
โข ((1
โ โ โง (โโ(((๐ + ๐) + ๐) / ๐ธ)) โ โ0) โ 1 โค
(1 + (โโ(((๐ +
๐) + ๐) / ๐ธ)))) |
44 | 23, 42, 43 | syl2anc 583 |
. . . . . . 7
โข (๐ โ 1 โค (1 +
(โโ(((๐ + ๐) + ๐) / ๐ธ)))) |
45 | | 1z 12597 |
. . . . . . . . 9
โข 1 โ
โค |
46 | | fladdz 13795 |
. . . . . . . . 9
โข
(((((๐ + ๐) + ๐) / ๐ธ) โ โ โง 1 โ โค)
โ (โโ((((๐
+ ๐) + ๐) / ๐ธ) + 1)) = ((โโ(((๐ + ๐) + ๐) / ๐ธ)) + 1)) |
47 | 22, 45, 46 | sylancl 585 |
. . . . . . . 8
โข (๐ โ (โโ((((๐ + ๐) + ๐) / ๐ธ) + 1)) = ((โโ(((๐ + ๐) + ๐) / ๐ธ)) + 1)) |
48 | 42 | nn0cnd 12539 |
. . . . . . . . 9
โข (๐ โ (โโ(((๐ + ๐) + ๐) / ๐ธ)) โ โ) |
49 | 23 | recnd 11247 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
50 | 48, 49 | addcomd 11421 |
. . . . . . . 8
โข (๐ โ ((โโ(((๐ + ๐) + ๐) / ๐ธ)) + 1) = (1 + (โโ(((๐ + ๐) + ๐) / ๐ธ)))) |
51 | 47, 50 | eqtr2d 2772 |
. . . . . . 7
โข (๐ โ (1 +
(โโ(((๐ + ๐) + ๐) / ๐ธ))) = (โโ((((๐ + ๐) + ๐) / ๐ธ) + 1))) |
52 | 44, 51 | breqtrd 5174 |
. . . . . 6
โข (๐ โ 1 โค
(โโ((((๐ +
๐) + ๐) / ๐ธ) + 1))) |
53 | 26, 23, 28, 30, 52 | ltletrd 11379 |
. . . . 5
โข (๐ โ 0 <
(โโ((((๐ +
๐) + ๐) / ๐ธ) + 1))) |
54 | | elnnz 12573 |
. . . . 5
โข
((โโ((((๐ + ๐) + ๐) / ๐ธ) + 1)) โ โ โ
((โโ((((๐ +
๐) + ๐) / ๐ธ) + 1)) โ โค โง 0 <
(โโ((((๐ +
๐) + ๐) / ๐ธ) + 1)))) |
55 | 25, 53, 54 | sylanbrc 582 |
. . . 4
โข (๐ โ (โโ((((๐ + ๐) + ๐) / ๐ธ) + 1)) โ โ) |
56 | 55 | peano2nnd 12234 |
. . 3
โข (๐ โ ((โโ((((๐ + ๐) + ๐) / ๐ธ) + 1)) + 1) โ
โ) |
57 | 1, 56 | eqeltrid 2836 |
. 2
โข (๐ โ ๐ โ โ) |
58 | | elioore 13359 |
. . . . 5
โข (๐ โ (๐(,)+โ) โ ๐ โ โ) |
59 | | fourierdlem47.iblmul |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (๐ฅ โ ๐ผ โฆ (๐น ยท -๐บ)) โ
๐ฟ1) |
60 | 58, 59 | sylan2 592 |
. . . 4
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (๐ฅ โ ๐ผ โฆ (๐น ยท -๐บ)) โ
๐ฟ1) |
61 | 12 | adantlr 712 |
. . . 4
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ ๐น โ โ) |
62 | | simpll 764 |
. . . . 5
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ ๐) |
63 | | simpr 484 |
. . . . 5
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ ๐ฅ โ ๐ผ) |
64 | 58 | ad2antlr 724 |
. . . . . 6
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ ๐ โ โ) |
65 | 64 | recnd 11247 |
. . . . 5
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ ๐ โ โ) |
66 | | fourierdlem47.g |
. . . . 5
โข (((๐ โง ๐ฅ โ ๐ผ) โง ๐ โ โ) โ ๐บ โ โ) |
67 | 62, 63, 65, 66 | syl21anc 835 |
. . . 4
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ ๐บ โ โ) |
68 | 3 | adantr 480 |
. . . 4
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ด โ โ) |
69 | 7 | adantr 480 |
. . . 4
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ถ โ โ) |
70 | | eqid 2731 |
. . . 4
โข
(absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ) = (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ) |
71 | 19 | adantr 480 |
. . . 4
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ธ โ
โ+) |
72 | 58 | adantl 481 |
. . . 4
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ โ โ) |
73 | 2 | eqcomi 2740 |
. . . . . . . . . 10
โข
(absโ๐ด) =
๐ |
74 | 6 | eqcomi 2740 |
. . . . . . . . . 10
โข
(absโ๐ถ) =
๐ |
75 | 73, 74 | oveq12i 7424 |
. . . . . . . . 9
โข
((absโ๐ด) +
(absโ๐ถ)) = (๐ + ๐) |
76 | 75 | oveq1i 7422 |
. . . . . . . 8
โข
(((absโ๐ด) +
(absโ๐ถ)) +
(absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) = ((๐ + ๐) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) |
77 | 4 | adantr 480 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (absโ๐ด) โ
โ) |
78 | 8 | adantr 480 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (absโ๐ถ) โ
โ) |
79 | 77, 78 | readdcld 11248 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ((absโ๐ด) + (absโ๐ถ)) โ โ) |
80 | 67 | negcld 11563 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ -๐บ โ โ) |
81 | 61, 80 | mulcld 11239 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ (๐น ยท -๐บ) โ โ) |
82 | 81, 60 | itgcl 25534 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (๐(,)+โ)) โ โซ๐ผ(๐น ยท -๐บ) d๐ฅ โ โ) |
83 | 82 | abscld 15388 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ) โ โ) |
84 | 79, 83 | readdcld 11248 |
. . . . . . . 8
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (((absโ๐ด) + (absโ๐ถ)) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) โ โ) |
85 | 76, 84 | eqeltrrid 2837 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ((๐ + ๐) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) โ โ) |
86 | 20 | adantr 480 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ธ โ โ) |
87 | 21 | adantr 480 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ธ โ 0) |
88 | 85, 86, 87 | redivcld 12047 |
. . . . . 6
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (((๐ + ๐) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐ธ) โ โ) |
89 | | 1red 11220 |
. . . . . 6
โข ((๐ โง ๐ โ (๐(,)+โ)) โ 1 โ
โ) |
90 | 88, 89 | readdcld 11248 |
. . . . 5
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ((((๐ + ๐) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐ธ) + 1) โ โ) |
91 | 2, 77 | eqeltrid 2836 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ โ โ) |
92 | 6, 78 | eqeltrid 2836 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ โ โ) |
93 | 91, 92 | readdcld 11248 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (๐ + ๐) โ โ) |
94 | 17 | adantr 480 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ โ โ) |
95 | 93, 94 | readdcld 11248 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ((๐ + ๐) + ๐) โ โ) |
96 | 95, 86, 87 | redivcld 12047 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (((๐ + ๐) + ๐) / ๐ธ) โ โ) |
97 | 96, 89 | readdcld 11248 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ((((๐ + ๐) + ๐) / ๐ธ) + 1) โ โ) |
98 | 97, 27 | syl 17 |
. . . . . . . 8
โข ((๐ โง ๐ โ (๐(,)+โ)) โ
(โโ((((๐ +
๐) + ๐) / ๐ธ) + 1)) โ โ) |
99 | 98, 89 | readdcld 11248 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐(,)+โ)) โ
((โโ((((๐ +
๐) + ๐) / ๐ธ) + 1)) + 1) โ
โ) |
100 | 1, 99 | eqeltrid 2836 |
. . . . . 6
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ โ โ) |
101 | 81 | abscld 15388 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ (absโ(๐น ยท -๐บ)) โ โ) |
102 | 81, 60 | iblabs 25579 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (๐ฅ โ ๐ผ โฆ (absโ(๐น ยท -๐บ))) โ
๐ฟ1) |
103 | 101, 102 | itgrecl 25548 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (๐(,)+โ)) โ โซ๐ผ(absโ(๐น ยท -๐บ)) d๐ฅ โ โ) |
104 | 81, 60 | itgabs 25585 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ) โค โซ๐ผ(absโ(๐น ยท -๐บ)) d๐ฅ) |
105 | 15 | adantr 480 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (๐ฅ โ ๐ผ โฆ (absโ๐น)) โ
๐ฟ1) |
106 | 61 | abscld 15388 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ (absโ๐น) โ โ) |
107 | 61, 80 | absmuld 15406 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ (absโ(๐น ยท -๐บ)) = ((absโ๐น) ยท (absโ-๐บ))) |
108 | 80 | abscld 15388 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ (absโ-๐บ) โ โ) |
109 | | 1red 11220 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ 1 โ โ) |
110 | 61 | absge0d 15396 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ 0 โค (absโ๐น)) |
111 | | recn 11204 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ ๐ โ
โ) |
112 | 111, 66 | sylan2 592 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ฅ โ ๐ผ) โง ๐ โ โ) โ ๐บ โ โ) |
113 | 112 | absnegd 15401 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ฅ โ ๐ผ) โง ๐ โ โ) โ (absโ-๐บ) = (absโ๐บ)) |
114 | | fourierdlem47.absg |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ฅ โ ๐ผ) โง ๐ โ โ) โ (absโ๐บ) โค 1) |
115 | 113, 114 | eqbrtrd 5170 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ฅ โ ๐ผ) โง ๐ โ โ) โ (absโ-๐บ) โค 1) |
116 | 62, 63, 64, 115 | syl21anc 835 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ (absโ-๐บ) โค 1) |
117 | 108, 109,
106, 110, 116 | lemul2ad 12159 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ ((absโ๐น) ยท (absโ-๐บ)) โค ((absโ๐น) ยท 1)) |
118 | 106 | recnd 11247 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ (absโ๐น) โ โ) |
119 | 118 | mulridd 11236 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ ((absโ๐น) ยท 1) = (absโ๐น)) |
120 | 117, 119 | breqtrd 5174 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ ((absโ๐น) ยท (absโ-๐บ)) โค (absโ๐น)) |
121 | 107, 120 | eqbrtrd 5170 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (๐(,)+โ)) โง ๐ฅ โ ๐ผ) โ (absโ(๐น ยท -๐บ)) โค (absโ๐น)) |
122 | 102, 105,
101, 106, 121 | itgle 25560 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (๐(,)+โ)) โ โซ๐ผ(absโ(๐น ยท -๐บ)) d๐ฅ โค โซ๐ผ(absโ๐น) d๐ฅ) |
123 | 122, 11 | breqtrrdi 5190 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (๐(,)+โ)) โ โซ๐ผ(absโ(๐น ยท -๐บ)) d๐ฅ โค ๐) |
124 | 83, 103, 94, 104, 123 | letrd 11376 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ) โค ๐) |
125 | 83, 94, 93, 124 | leadd2dd 11834 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ((๐ + ๐) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) โค ((๐ + ๐) + ๐)) |
126 | 85, 95, 71, 125 | lediv1dd 13079 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (((๐ + ๐) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐ธ) โค (((๐ + ๐) + ๐) / ๐ธ)) |
127 | | flltp1 13770 |
. . . . . . . . . . 11
โข ((((๐ + ๐) + ๐) / ๐ธ) โ โ โ (((๐ + ๐) + ๐) / ๐ธ) < ((โโ(((๐ + ๐) + ๐) / ๐ธ)) + 1)) |
128 | 96, 127 | syl 17 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (((๐ + ๐) + ๐) / ๐ธ) < ((โโ(((๐ + ๐) + ๐) / ๐ธ)) + 1)) |
129 | 96, 45, 46 | sylancl 585 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (๐(,)+โ)) โ
(โโ((((๐ +
๐) + ๐) / ๐ธ) + 1)) = ((โโ(((๐ + ๐) + ๐) / ๐ธ)) + 1)) |
130 | 128, 129 | breqtrrd 5176 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (((๐ + ๐) + ๐) / ๐ธ) < (โโ((((๐ + ๐) + ๐) / ๐ธ) + 1))) |
131 | 88, 96, 98, 126, 130 | lelttrd 11377 |
. . . . . . . 8
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (((๐ + ๐) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐ธ) < (โโ((((๐ + ๐) + ๐) / ๐ธ) + 1))) |
132 | 88, 98, 89, 131 | ltadd1dd 11830 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ((((๐ + ๐) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐ธ) + 1) < ((โโ((((๐ + ๐) + ๐) / ๐ธ) + 1)) + 1)) |
133 | 132, 1 | breqtrrdi 5190 |
. . . . . 6
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ((((๐ + ๐) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐ธ) + 1) < ๐) |
134 | 100 | rexrd 11269 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ โ
โ*) |
135 | | pnfxr 11273 |
. . . . . . . 8
โข +โ
โ โ* |
136 | 135 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐(,)+โ)) โ +โ โ
โ*) |
137 | | simpr 484 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ โ (๐(,)+โ)) |
138 | | ioogtlb 44507 |
. . . . . . 7
โข ((๐ โ โ*
โง +โ โ โ* โง ๐ โ (๐(,)+โ)) โ ๐ < ๐) |
139 | 134, 136,
137, 138 | syl3anc 1370 |
. . . . . 6
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ < ๐) |
140 | 90, 100, 72, 133, 139 | lttrd 11380 |
. . . . 5
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ((((๐ + ๐) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐ธ) + 1) < ๐) |
141 | 90, 72, 140 | ltled 11367 |
. . . 4
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ((((๐ + ๐) + (absโโซ๐ผ(๐น ยท -๐บ) d๐ฅ)) / ๐ธ) + 1) โค ๐) |
142 | 72 | recnd 11247 |
. . . . 5
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ โ โ) |
143 | | fourierdlem47.b |
. . . . 5
โข ((๐ โง ๐ โ โ) โ ๐ต โ โ) |
144 | 142, 143 | syldan 590 |
. . . 4
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ต โ โ) |
145 | | fourierdlem47.absb |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (absโ๐ต) โค 1) |
146 | 58, 145 | sylan2 592 |
. . . 4
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (absโ๐ต) โค 1) |
147 | | fourierdlem47.d |
. . . . 5
โข ((๐ โง ๐ โ โ) โ ๐ท โ โ) |
148 | 142, 147 | syldan 590 |
. . . 4
โข ((๐ โง ๐ โ (๐(,)+โ)) โ ๐ท โ โ) |
149 | | fourierdlem47.absd |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (absโ๐ท) โค 1) |
150 | 58, 149 | sylan2 592 |
. . . 4
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (absโ๐ท) โค 1) |
151 | 60, 61, 67, 68, 2, 69, 6, 70, 71, 72, 141, 144, 146, 148, 150 | fourierdlem30 45152 |
. . 3
โข ((๐ โง ๐ โ (๐(,)+โ)) โ (absโ(((๐ด ยท -(๐ต / ๐)) โ (๐ถ ยท -(๐ท / ๐))) โ โซ๐ผ(๐น ยท -(๐บ / ๐)) d๐ฅ)) < ๐ธ) |
152 | 151 | ralrimiva 3145 |
. 2
โข (๐ โ โ๐ โ (๐(,)+โ)(absโ(((๐ด ยท -(๐ต / ๐)) โ (๐ถ ยท -(๐ท / ๐))) โ โซ๐ผ(๐น ยท -(๐บ / ๐)) d๐ฅ)) < ๐ธ) |
153 | | oveq1 7419 |
. . . 4
โข (๐ = ๐ โ (๐(,)+โ) = (๐(,)+โ)) |
154 | 153 | raleqdv 3324 |
. . 3
โข (๐ = ๐ โ (โ๐ โ (๐(,)+โ)(absโ(((๐ด ยท -(๐ต / ๐)) โ (๐ถ ยท -(๐ท / ๐))) โ โซ๐ผ(๐น ยท -(๐บ / ๐)) d๐ฅ)) < ๐ธ โ โ๐ โ (๐(,)+โ)(absโ(((๐ด ยท -(๐ต / ๐)) โ (๐ถ ยท -(๐ท / ๐))) โ โซ๐ผ(๐น ยท -(๐บ / ๐)) d๐ฅ)) < ๐ธ)) |
155 | 154 | rspcev 3612 |
. 2
โข ((๐ โ โ โง
โ๐ โ (๐(,)+โ)(absโ(((๐ด ยท -(๐ต / ๐)) โ (๐ถ ยท -(๐ท / ๐))) โ โซ๐ผ(๐น ยท -(๐บ / ๐)) d๐ฅ)) < ๐ธ) โ โ๐ โ โ โ๐ โ (๐(,)+โ)(absโ(((๐ด ยท -(๐ต / ๐)) โ (๐ถ ยท -(๐ท / ๐))) โ โซ๐ผ(๐น ยท -(๐บ / ๐)) d๐ฅ)) < ๐ธ) |
156 | 57, 152, 155 | syl2anc 583 |
1
โข (๐ โ โ๐ โ โ โ๐ โ (๐(,)+โ)(absโ(((๐ด ยท -(๐ต / ๐)) โ (๐ถ ยท -(๐ท / ๐))) โ โซ๐ผ(๐น ยท -(๐บ / ๐)) d๐ฅ)) < ๐ธ) |