Step | Hyp | Ref
| Expression |
1 | | fourierdlem47.m |
. . 3
β’ π = ((ββ((((π + π) + π) / πΈ) + 1)) + 1) |
2 | | fourierdlem47.x |
. . . . . . . . . . 11
β’ π = (absβπ΄) |
3 | | fourierdlem47.a |
. . . . . . . . . . . 12
β’ (π β π΄ β β) |
4 | 3 | abscld 15328 |
. . . . . . . . . . 11
β’ (π β (absβπ΄) β
β) |
5 | 2, 4 | eqeltrid 2842 |
. . . . . . . . . 10
β’ (π β π β β) |
6 | | fourierdlem47.y |
. . . . . . . . . . 11
β’ π = (absβπΆ) |
7 | | fourierdlem47.c |
. . . . . . . . . . . 12
β’ (π β πΆ β β) |
8 | 7 | abscld 15328 |
. . . . . . . . . . 11
β’ (π β (absβπΆ) β
β) |
9 | 6, 8 | eqeltrid 2842 |
. . . . . . . . . 10
β’ (π β π β β) |
10 | 5, 9 | readdcld 11191 |
. . . . . . . . 9
β’ (π β (π + π) β β) |
11 | | fourierdlem47.z |
. . . . . . . . . 10
β’ π = β«πΌ(absβπΉ) dπ₯ |
12 | | fourierdlem47.f |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β πΌ) β πΉ β β) |
13 | 12 | abscld 15328 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β πΌ) β (absβπΉ) β β) |
14 | | fourierdlem47.ibl |
. . . . . . . . . . . 12
β’ (π β (π₯ β πΌ β¦ πΉ) β
πΏ1) |
15 | 12, 14 | iblabs 25209 |
. . . . . . . . . . 11
β’ (π β (π₯ β πΌ β¦ (absβπΉ)) β
πΏ1) |
16 | 13, 15 | itgrecl 25178 |
. . . . . . . . . 10
β’ (π β β«πΌ(absβπΉ) dπ₯ β β) |
17 | 11, 16 | eqeltrid 2842 |
. . . . . . . . 9
β’ (π β π β β) |
18 | 10, 17 | readdcld 11191 |
. . . . . . . 8
β’ (π β ((π + π) + π) β β) |
19 | | fourierdlem47.e |
. . . . . . . . 9
β’ (π β πΈ β
β+) |
20 | 19 | rpred 12964 |
. . . . . . . 8
β’ (π β πΈ β β) |
21 | 19 | rpne0d 12969 |
. . . . . . . 8
β’ (π β πΈ β 0) |
22 | 18, 20, 21 | redivcld 11990 |
. . . . . . 7
β’ (π β (((π + π) + π) / πΈ) β β) |
23 | | 1red 11163 |
. . . . . . 7
β’ (π β 1 β
β) |
24 | 22, 23 | readdcld 11191 |
. . . . . 6
β’ (π β ((((π + π) + π) / πΈ) + 1) β β) |
25 | 24 | flcld 13710 |
. . . . 5
β’ (π β (ββ((((π + π) + π) / πΈ) + 1)) β β€) |
26 | | 0red 11165 |
. . . . . 6
β’ (π β 0 β
β) |
27 | | reflcl 13708 |
. . . . . . 7
β’
(((((π + π) + π) / πΈ) + 1) β β β
(ββ((((π +
π) + π) / πΈ) + 1)) β β) |
28 | 24, 27 | syl 17 |
. . . . . 6
β’ (π β (ββ((((π + π) + π) / πΈ) + 1)) β β) |
29 | | 0lt1 11684 |
. . . . . . 7
β’ 0 <
1 |
30 | 29 | a1i 11 |
. . . . . 6
β’ (π β 0 < 1) |
31 | 3 | absge0d 15336 |
. . . . . . . . . . . . 13
β’ (π β 0 β€ (absβπ΄)) |
32 | 31, 2 | breqtrrdi 5152 |
. . . . . . . . . . . 12
β’ (π β 0 β€ π) |
33 | 7 | absge0d 15336 |
. . . . . . . . . . . . 13
β’ (π β 0 β€ (absβπΆ)) |
34 | 33, 6 | breqtrrdi 5152 |
. . . . . . . . . . . 12
β’ (π β 0 β€ π) |
35 | 5, 9, 32, 34 | addge0d 11738 |
. . . . . . . . . . 11
β’ (π β 0 β€ (π + π)) |
36 | 12 | absge0d 15336 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β πΌ) β 0 β€ (absβπΉ)) |
37 | 15, 13, 36 | itgge0 25191 |
. . . . . . . . . . . 12
β’ (π β 0 β€ β«πΌ(absβπΉ) dπ₯) |
38 | 37, 11 | breqtrrdi 5152 |
. . . . . . . . . . 11
β’ (π β 0 β€ π) |
39 | 10, 17, 35, 38 | addge0d 11738 |
. . . . . . . . . 10
β’ (π β 0 β€ ((π + π) + π)) |
40 | 18, 19, 39 | divge0d 13004 |
. . . . . . . . 9
β’ (π β 0 β€ (((π + π) + π) / πΈ)) |
41 | | flge0nn0 13732 |
. . . . . . . . 9
β’
(((((π + π) + π) / πΈ) β β β§ 0 β€ (((π + π) + π) / πΈ)) β (ββ(((π + π) + π) / πΈ)) β
β0) |
42 | 22, 40, 41 | syl2anc 585 |
. . . . . . . 8
β’ (π β (ββ(((π + π) + π) / πΈ)) β
β0) |
43 | | nn0addge1 12466 |
. . . . . . . 8
β’ ((1
β β β§ (ββ(((π + π) + π) / πΈ)) β β0) β 1 β€
(1 + (ββ(((π +
π) + π) / πΈ)))) |
44 | 23, 42, 43 | syl2anc 585 |
. . . . . . 7
β’ (π β 1 β€ (1 +
(ββ(((π + π) + π) / πΈ)))) |
45 | | 1z 12540 |
. . . . . . . . 9
β’ 1 β
β€ |
46 | | fladdz 13737 |
. . . . . . . . 9
β’
(((((π + π) + π) / πΈ) β β β§ 1 β β€)
β (ββ((((π
+ π) + π) / πΈ) + 1)) = ((ββ(((π + π) + π) / πΈ)) + 1)) |
47 | 22, 45, 46 | sylancl 587 |
. . . . . . . 8
β’ (π β (ββ((((π + π) + π) / πΈ) + 1)) = ((ββ(((π + π) + π) / πΈ)) + 1)) |
48 | 42 | nn0cnd 12482 |
. . . . . . . . 9
β’ (π β (ββ(((π + π) + π) / πΈ)) β β) |
49 | 23 | recnd 11190 |
. . . . . . . . 9
β’ (π β 1 β
β) |
50 | 48, 49 | addcomd 11364 |
. . . . . . . 8
β’ (π β ((ββ(((π + π) + π) / πΈ)) + 1) = (1 + (ββ(((π + π) + π) / πΈ)))) |
51 | 47, 50 | eqtr2d 2778 |
. . . . . . 7
β’ (π β (1 +
(ββ(((π + π) + π) / πΈ))) = (ββ((((π + π) + π) / πΈ) + 1))) |
52 | 44, 51 | breqtrd 5136 |
. . . . . 6
β’ (π β 1 β€
(ββ((((π +
π) + π) / πΈ) + 1))) |
53 | 26, 23, 28, 30, 52 | ltletrd 11322 |
. . . . 5
β’ (π β 0 <
(ββ((((π +
π) + π) / πΈ) + 1))) |
54 | | elnnz 12516 |
. . . . 5
β’
((ββ((((π + π) + π) / πΈ) + 1)) β β β
((ββ((((π +
π) + π) / πΈ) + 1)) β β€ β§ 0 <
(ββ((((π +
π) + π) / πΈ) + 1)))) |
55 | 25, 53, 54 | sylanbrc 584 |
. . . 4
β’ (π β (ββ((((π + π) + π) / πΈ) + 1)) β β) |
56 | 55 | peano2nnd 12177 |
. . 3
β’ (π β ((ββ((((π + π) + π) / πΈ) + 1)) + 1) β
β) |
57 | 1, 56 | eqeltrid 2842 |
. 2
β’ (π β π β β) |
58 | | elioore 13301 |
. . . . 5
β’ (π β (π(,)+β) β π β β) |
59 | | fourierdlem47.iblmul |
. . . . 5
β’ ((π β§ π β β) β (π₯ β πΌ β¦ (πΉ Β· -πΊ)) β
πΏ1) |
60 | 58, 59 | sylan2 594 |
. . . 4
β’ ((π β§ π β (π(,)+β)) β (π₯ β πΌ β¦ (πΉ Β· -πΊ)) β
πΏ1) |
61 | 12 | adantlr 714 |
. . . 4
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β πΉ β β) |
62 | | simpll 766 |
. . . . 5
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β π) |
63 | | simpr 486 |
. . . . 5
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β π₯ β πΌ) |
64 | 58 | ad2antlr 726 |
. . . . . 6
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β π β β) |
65 | 64 | recnd 11190 |
. . . . 5
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β π β β) |
66 | | fourierdlem47.g |
. . . . 5
β’ (((π β§ π₯ β πΌ) β§ π β β) β πΊ β β) |
67 | 62, 63, 65, 66 | syl21anc 837 |
. . . 4
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β πΊ β β) |
68 | 3 | adantr 482 |
. . . 4
β’ ((π β§ π β (π(,)+β)) β π΄ β β) |
69 | 7 | adantr 482 |
. . . 4
β’ ((π β§ π β (π(,)+β)) β πΆ β β) |
70 | | eqid 2737 |
. . . 4
β’
(absββ«πΌ(πΉ Β· -πΊ) dπ₯) = (absββ«πΌ(πΉ Β· -πΊ) dπ₯) |
71 | 19 | adantr 482 |
. . . 4
β’ ((π β§ π β (π(,)+β)) β πΈ β
β+) |
72 | 58 | adantl 483 |
. . . 4
β’ ((π β§ π β (π(,)+β)) β π β β) |
73 | 2 | eqcomi 2746 |
. . . . . . . . . 10
β’
(absβπ΄) =
π |
74 | 6 | eqcomi 2746 |
. . . . . . . . . 10
β’
(absβπΆ) =
π |
75 | 73, 74 | oveq12i 7374 |
. . . . . . . . 9
β’
((absβπ΄) +
(absβπΆ)) = (π + π) |
76 | 75 | oveq1i 7372 |
. . . . . . . 8
β’
(((absβπ΄) +
(absβπΆ)) +
(absββ«πΌ(πΉ Β· -πΊ) dπ₯)) = ((π + π) + (absββ«πΌ(πΉ Β· -πΊ) dπ₯)) |
77 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π(,)+β)) β (absβπ΄) β
β) |
78 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π(,)+β)) β (absβπΆ) β
β) |
79 | 77, 78 | readdcld 11191 |
. . . . . . . . 9
β’ ((π β§ π β (π(,)+β)) β ((absβπ΄) + (absβπΆ)) β β) |
80 | 67 | negcld 11506 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β -πΊ β β) |
81 | 61, 80 | mulcld 11182 |
. . . . . . . . . . 11
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β (πΉ Β· -πΊ) β β) |
82 | 81, 60 | itgcl 25164 |
. . . . . . . . . 10
β’ ((π β§ π β (π(,)+β)) β β«πΌ(πΉ Β· -πΊ) dπ₯ β β) |
83 | 82 | abscld 15328 |
. . . . . . . . 9
β’ ((π β§ π β (π(,)+β)) β (absββ«πΌ(πΉ Β· -πΊ) dπ₯) β β) |
84 | 79, 83 | readdcld 11191 |
. . . . . . . 8
β’ ((π β§ π β (π(,)+β)) β (((absβπ΄) + (absβπΆ)) + (absββ«πΌ(πΉ Β· -πΊ) dπ₯)) β β) |
85 | 76, 84 | eqeltrrid 2843 |
. . . . . . 7
β’ ((π β§ π β (π(,)+β)) β ((π + π) + (absββ«πΌ(πΉ Β· -πΊ) dπ₯)) β β) |
86 | 20 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (π(,)+β)) β πΈ β β) |
87 | 21 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (π(,)+β)) β πΈ β 0) |
88 | 85, 86, 87 | redivcld 11990 |
. . . . . 6
β’ ((π β§ π β (π(,)+β)) β (((π + π) + (absββ«πΌ(πΉ Β· -πΊ) dπ₯)) / πΈ) β β) |
89 | | 1red 11163 |
. . . . . 6
β’ ((π β§ π β (π(,)+β)) β 1 β
β) |
90 | 88, 89 | readdcld 11191 |
. . . . 5
β’ ((π β§ π β (π(,)+β)) β ((((π + π) + (absββ«πΌ(πΉ Β· -πΊ) dπ₯)) / πΈ) + 1) β β) |
91 | 2, 77 | eqeltrid 2842 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π(,)+β)) β π β β) |
92 | 6, 78 | eqeltrid 2842 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π(,)+β)) β π β β) |
93 | 91, 92 | readdcld 11191 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π(,)+β)) β (π + π) β β) |
94 | 17 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π(,)+β)) β π β β) |
95 | 93, 94 | readdcld 11191 |
. . . . . . . . . . 11
β’ ((π β§ π β (π(,)+β)) β ((π + π) + π) β β) |
96 | 95, 86, 87 | redivcld 11990 |
. . . . . . . . . 10
β’ ((π β§ π β (π(,)+β)) β (((π + π) + π) / πΈ) β β) |
97 | 96, 89 | readdcld 11191 |
. . . . . . . . 9
β’ ((π β§ π β (π(,)+β)) β ((((π + π) + π) / πΈ) + 1) β β) |
98 | 97, 27 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (π(,)+β)) β
(ββ((((π +
π) + π) / πΈ) + 1)) β β) |
99 | 98, 89 | readdcld 11191 |
. . . . . . 7
β’ ((π β§ π β (π(,)+β)) β
((ββ((((π +
π) + π) / πΈ) + 1)) + 1) β
β) |
100 | 1, 99 | eqeltrid 2842 |
. . . . . 6
β’ ((π β§ π β (π(,)+β)) β π β β) |
101 | 81 | abscld 15328 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β (absβ(πΉ Β· -πΊ)) β β) |
102 | 81, 60 | iblabs 25209 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π(,)+β)) β (π₯ β πΌ β¦ (absβ(πΉ Β· -πΊ))) β
πΏ1) |
103 | 101, 102 | itgrecl 25178 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π(,)+β)) β β«πΌ(absβ(πΉ Β· -πΊ)) dπ₯ β β) |
104 | 81, 60 | itgabs 25215 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π(,)+β)) β (absββ«πΌ(πΉ Β· -πΊ) dπ₯) β€ β«πΌ(absβ(πΉ Β· -πΊ)) dπ₯) |
105 | 15 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π(,)+β)) β (π₯ β πΌ β¦ (absβπΉ)) β
πΏ1) |
106 | 61 | abscld 15328 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β (absβπΉ) β β) |
107 | 61, 80 | absmuld 15346 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β (absβ(πΉ Β· -πΊ)) = ((absβπΉ) Β· (absβ-πΊ))) |
108 | 80 | abscld 15328 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β (absβ-πΊ) β β) |
109 | | 1red 11163 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β 1 β β) |
110 | 61 | absge0d 15336 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β 0 β€ (absβπΉ)) |
111 | | recn 11148 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β π β
β) |
112 | 111, 66 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β πΌ) β§ π β β) β πΊ β β) |
113 | 112 | absnegd 15341 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β πΌ) β§ π β β) β (absβ-πΊ) = (absβπΊ)) |
114 | | fourierdlem47.absg |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β πΌ) β§ π β β) β (absβπΊ) β€ 1) |
115 | 113, 114 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β πΌ) β§ π β β) β (absβ-πΊ) β€ 1) |
116 | 62, 63, 64, 115 | syl21anc 837 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β (absβ-πΊ) β€ 1) |
117 | 108, 109,
106, 110, 116 | lemul2ad 12102 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β ((absβπΉ) Β· (absβ-πΊ)) β€ ((absβπΉ) Β· 1)) |
118 | 106 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β (absβπΉ) β β) |
119 | 118 | mulid1d 11179 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β ((absβπΉ) Β· 1) = (absβπΉ)) |
120 | 117, 119 | breqtrd 5136 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β ((absβπΉ) Β· (absβ-πΊ)) β€ (absβπΉ)) |
121 | 107, 120 | eqbrtrd 5132 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π(,)+β)) β§ π₯ β πΌ) β (absβ(πΉ Β· -πΊ)) β€ (absβπΉ)) |
122 | 102, 105,
101, 106, 121 | itgle 25190 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π(,)+β)) β β«πΌ(absβ(πΉ Β· -πΊ)) dπ₯ β€ β«πΌ(absβπΉ) dπ₯) |
123 | 122, 11 | breqtrrdi 5152 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π(,)+β)) β β«πΌ(absβ(πΉ Β· -πΊ)) dπ₯ β€ π) |
124 | 83, 103, 94, 104, 123 | letrd 11319 |
. . . . . . . . . . 11
β’ ((π β§ π β (π(,)+β)) β (absββ«πΌ(πΉ Β· -πΊ) dπ₯) β€ π) |
125 | 83, 94, 93, 124 | leadd2dd 11777 |
. . . . . . . . . 10
β’ ((π β§ π β (π(,)+β)) β ((π + π) + (absββ«πΌ(πΉ Β· -πΊ) dπ₯)) β€ ((π + π) + π)) |
126 | 85, 95, 71, 125 | lediv1dd 13022 |
. . . . . . . . 9
β’ ((π β§ π β (π(,)+β)) β (((π + π) + (absββ«πΌ(πΉ Β· -πΊ) dπ₯)) / πΈ) β€ (((π + π) + π) / πΈ)) |
127 | | flltp1 13712 |
. . . . . . . . . . 11
β’ ((((π + π) + π) / πΈ) β β β (((π + π) + π) / πΈ) < ((ββ(((π + π) + π) / πΈ)) + 1)) |
128 | 96, 127 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (π(,)+β)) β (((π + π) + π) / πΈ) < ((ββ(((π + π) + π) / πΈ)) + 1)) |
129 | 96, 45, 46 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β§ π β (π(,)+β)) β
(ββ((((π +
π) + π) / πΈ) + 1)) = ((ββ(((π + π) + π) / πΈ)) + 1)) |
130 | 128, 129 | breqtrrd 5138 |
. . . . . . . . 9
β’ ((π β§ π β (π(,)+β)) β (((π + π) + π) / πΈ) < (ββ((((π + π) + π) / πΈ) + 1))) |
131 | 88, 96, 98, 126, 130 | lelttrd 11320 |
. . . . . . . 8
β’ ((π β§ π β (π(,)+β)) β (((π + π) + (absββ«πΌ(πΉ Β· -πΊ) dπ₯)) / πΈ) < (ββ((((π + π) + π) / πΈ) + 1))) |
132 | 88, 98, 89, 131 | ltadd1dd 11773 |
. . . . . . 7
β’ ((π β§ π β (π(,)+β)) β ((((π + π) + (absββ«πΌ(πΉ Β· -πΊ) dπ₯)) / πΈ) + 1) < ((ββ((((π + π) + π) / πΈ) + 1)) + 1)) |
133 | 132, 1 | breqtrrdi 5152 |
. . . . . 6
β’ ((π β§ π β (π(,)+β)) β ((((π + π) + (absββ«πΌ(πΉ Β· -πΊ) dπ₯)) / πΈ) + 1) < π) |
134 | 100 | rexrd 11212 |
. . . . . . 7
β’ ((π β§ π β (π(,)+β)) β π β
β*) |
135 | | pnfxr 11216 |
. . . . . . . 8
β’ +β
β β* |
136 | 135 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β (π(,)+β)) β +β β
β*) |
137 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β (π(,)+β)) β π β (π(,)+β)) |
138 | | ioogtlb 43807 |
. . . . . . 7
β’ ((π β β*
β§ +β β β* β§ π β (π(,)+β)) β π < π) |
139 | 134, 136,
137, 138 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π β (π(,)+β)) β π < π) |
140 | 90, 100, 72, 133, 139 | lttrd 11323 |
. . . . 5
β’ ((π β§ π β (π(,)+β)) β ((((π + π) + (absββ«πΌ(πΉ Β· -πΊ) dπ₯)) / πΈ) + 1) < π) |
141 | 90, 72, 140 | ltled 11310 |
. . . 4
β’ ((π β§ π β (π(,)+β)) β ((((π + π) + (absββ«πΌ(πΉ Β· -πΊ) dπ₯)) / πΈ) + 1) β€ π) |
142 | 72 | recnd 11190 |
. . . . 5
β’ ((π β§ π β (π(,)+β)) β π β β) |
143 | | fourierdlem47.b |
. . . . 5
β’ ((π β§ π β β) β π΅ β β) |
144 | 142, 143 | syldan 592 |
. . . 4
β’ ((π β§ π β (π(,)+β)) β π΅ β β) |
145 | | fourierdlem47.absb |
. . . . 5
β’ ((π β§ π β β) β (absβπ΅) β€ 1) |
146 | 58, 145 | sylan2 594 |
. . . 4
β’ ((π β§ π β (π(,)+β)) β (absβπ΅) β€ 1) |
147 | | fourierdlem47.d |
. . . . 5
β’ ((π β§ π β β) β π· β β) |
148 | 142, 147 | syldan 592 |
. . . 4
β’ ((π β§ π β (π(,)+β)) β π· β β) |
149 | | fourierdlem47.absd |
. . . . 5
β’ ((π β§ π β β) β (absβπ·) β€ 1) |
150 | 58, 149 | sylan2 594 |
. . . 4
β’ ((π β§ π β (π(,)+β)) β (absβπ·) β€ 1) |
151 | 60, 61, 67, 68, 2, 69, 6, 70, 71, 72, 141, 144, 146, 148, 150 | fourierdlem30 44452 |
. . 3
β’ ((π β§ π β (π(,)+β)) β (absβ(((π΄ Β· -(π΅ / π)) β (πΆ Β· -(π· / π))) β β«πΌ(πΉ Β· -(πΊ / π)) dπ₯)) < πΈ) |
152 | 151 | ralrimiva 3144 |
. 2
β’ (π β βπ β (π(,)+β)(absβ(((π΄ Β· -(π΅ / π)) β (πΆ Β· -(π· / π))) β β«πΌ(πΉ Β· -(πΊ / π)) dπ₯)) < πΈ) |
153 | | oveq1 7369 |
. . . 4
β’ (π = π β (π(,)+β) = (π(,)+β)) |
154 | 153 | raleqdv 3316 |
. . 3
β’ (π = π β (βπ β (π(,)+β)(absβ(((π΄ Β· -(π΅ / π)) β (πΆ Β· -(π· / π))) β β«πΌ(πΉ Β· -(πΊ / π)) dπ₯)) < πΈ β βπ β (π(,)+β)(absβ(((π΄ Β· -(π΅ / π)) β (πΆ Β· -(π· / π))) β β«πΌ(πΉ Β· -(πΊ / π)) dπ₯)) < πΈ)) |
155 | 154 | rspcev 3584 |
. 2
β’ ((π β β β§
βπ β (π(,)+β)(absβ(((π΄ Β· -(π΅ / π)) β (πΆ Β· -(π· / π))) β β«πΌ(πΉ Β· -(πΊ / π)) dπ₯)) < πΈ) β βπ β β βπ β (π(,)+β)(absβ(((π΄ Β· -(π΅ / π)) β (πΆ Β· -(π· / π))) β β«πΌ(πΉ Β· -(πΊ / π)) dπ₯)) < πΈ) |
156 | 57, 152, 155 | syl2anc 585 |
1
β’ (π β βπ β β βπ β (π(,)+β)(absβ(((π΄ Β· -(π΅ / π)) β (πΆ Β· -(π· / π))) β β«πΌ(πΉ Β· -(πΊ / π)) dπ₯)) < πΈ) |