Step | Hyp | Ref
| Expression |
1 | | 0red 11216 |
. . 3
β’ (π β 0 β
β) |
2 | | fourierdlem61.b |
. . . . 5
β’ (π β π΅ β β) |
3 | | fourierdlem61.a |
. . . . 5
β’ (π β π΄ β β) |
4 | 2, 3 | resubcld 11641 |
. . . 4
β’ (π β (π΅ β π΄) β β) |
5 | 4 | rexrd 11263 |
. . 3
β’ (π β (π΅ β π΄) β
β*) |
6 | | fourierdlem61.altb |
. . . 4
β’ (π β π΄ < π΅) |
7 | 3, 2 | posdifd 11800 |
. . . 4
β’ (π β (π΄ < π΅ β 0 < (π΅ β π΄))) |
8 | 6, 7 | mpbid 231 |
. . 3
β’ (π β 0 < (π΅ β π΄)) |
9 | | fourierdlem61.f |
. . . . . . 7
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
10 | 9 | adantr 481 |
. . . . . 6
β’ ((π β§ π β (0(,)(π΅ β π΄))) β πΉ:(π΄(,)π΅)βΆβ) |
11 | 3 | rexrd 11263 |
. . . . . . . 8
β’ (π β π΄ β
β*) |
12 | 11 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π΄ β
β*) |
13 | 2 | rexrd 11263 |
. . . . . . . 8
β’ (π β π΅ β
β*) |
14 | 13 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π΅ β
β*) |
15 | 3 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π΄ β β) |
16 | | elioore 13353 |
. . . . . . . . 9
β’ (π β (0(,)(π΅ β π΄)) β π β β) |
17 | 16 | adantl 482 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π β β) |
18 | 15, 17 | readdcld 11242 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + π ) β β) |
19 | 3 | recnd 11241 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
20 | 19 | addridd 11413 |
. . . . . . . . . 10
β’ (π β (π΄ + 0) = π΄) |
21 | 20 | eqcomd 2738 |
. . . . . . . . 9
β’ (π β π΄ = (π΄ + 0)) |
22 | 21 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π΄ = (π΄ + 0)) |
23 | | 0red 11216 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β 0 β
β) |
24 | | 0xr 11260 |
. . . . . . . . . . 11
β’ 0 β
β* |
25 | 24 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (0(,)(π΅ β π΄))) β 0 β
β*) |
26 | 5 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΅ β π΄) β
β*) |
27 | | simpr 485 |
. . . . . . . . . 10
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π β (0(,)(π΅ β π΄))) |
28 | 25, 26, 27 | ioogtlbd 44253 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β 0 < π ) |
29 | 23, 17, 15, 28 | ltadd2dd 11372 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + 0) < (π΄ + π )) |
30 | 22, 29 | eqbrtrd 5170 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π΄ < (π΄ + π )) |
31 | 4 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΅ β π΄) β β) |
32 | 25, 26, 27 | iooltubd 44247 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π < (π΅ β π΄)) |
33 | 17, 31, 15, 32 | ltadd2dd 11372 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + π ) < (π΄ + (π΅ β π΄))) |
34 | 2 | recnd 11241 |
. . . . . . . . . 10
β’ (π β π΅ β β) |
35 | 19, 34 | pncan3d 11573 |
. . . . . . . . 9
β’ (π β (π΄ + (π΅ β π΄)) = π΅) |
36 | 35 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + (π΅ β π΄)) = π΅) |
37 | 33, 36 | breqtrd 5174 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + π ) < π΅) |
38 | 12, 14, 18, 30, 37 | eliood 44201 |
. . . . . 6
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + π ) β (π΄(,)π΅)) |
39 | 10, 38 | ffvelcdmd 7087 |
. . . . 5
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (πΉβ(π΄ + π )) β β) |
40 | | ioossre 13384 |
. . . . . . . . 9
β’ (π΄(,)π΅) β β |
41 | 40 | a1i 11 |
. . . . . . . 8
β’ (π β (π΄(,)π΅) β β) |
42 | | ax-resscn 11166 |
. . . . . . . 8
β’ β
β β |
43 | 41, 42 | sstrdi 3994 |
. . . . . . 7
β’ (π β (π΄(,)π΅) β β) |
44 | | eqid 2732 |
. . . . . . . 8
β’
(TopOpenββfld) =
(TopOpenββfld) |
45 | 44, 13, 3, 6 | lptioo1cn 44352 |
. . . . . . 7
β’ (π β π΄ β
((limPtβ(TopOpenββfld))β(π΄(,)π΅))) |
46 | | fourierdlem61.y |
. . . . . . 7
β’ (π β π β (πΉ limβ π΄)) |
47 | 9, 43, 45, 46 | limcrecl 44335 |
. . . . . 6
β’ (π β π β β) |
48 | 47 | adantr 481 |
. . . . 5
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π β β) |
49 | 39, 48 | resubcld 11641 |
. . . 4
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((πΉβ(π΄ + π )) β π) β β) |
50 | | fourierdlem61.n |
. . . 4
β’ π = (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) |
51 | 49, 50 | fmptd 7113 |
. . 3
β’ (π β π:(0(,)(π΅ β π΄))βΆβ) |
52 | | fourierdlem61.d |
. . . 4
β’ π· = (π β (0(,)(π΅ β π΄)) β¦ π ) |
53 | 17, 52 | fmptd 7113 |
. . 3
β’ (π β π·:(0(,)(π΅ β π΄))βΆβ) |
54 | 50 | oveq2i 7419 |
. . . . . 6
β’ (β
D π) = (β D (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π))) |
55 | 54 | a1i 11 |
. . . . 5
β’ (π β (β D π) = (β D (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)))) |
56 | 55 | dmeqd 5905 |
. . . 4
β’ (π β dom (β D π) = dom (β D (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)))) |
57 | | reelprrecn 11201 |
. . . . . . . 8
β’ β
β {β, β} |
58 | 57 | a1i 11 |
. . . . . . 7
β’ (π β β β {β,
β}) |
59 | 39 | recnd 11241 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (πΉβ(π΄ + π )) β β) |
60 | | dvfre 25467 |
. . . . . . . . . . 11
β’ ((πΉ:(π΄(,)π΅)βΆβ β§ (π΄(,)π΅) β β) β (β D πΉ):dom (β D πΉ)βΆβ) |
61 | 9, 41, 60 | syl2anc 584 |
. . . . . . . . . 10
β’ (π β (β D πΉ):dom (β D πΉ)βΆβ) |
62 | | fourierdlem61.g |
. . . . . . . . . . . 12
β’ πΊ = (β D πΉ) |
63 | 62 | a1i 11 |
. . . . . . . . . . 11
β’ (π β πΊ = (β D πΉ)) |
64 | 63 | feq1d 6702 |
. . . . . . . . . 10
β’ (π β (πΊ:dom (β D πΉ)βΆβ β (β D πΉ):dom (β D πΉ)βΆβ)) |
65 | 61, 64 | mpbird 256 |
. . . . . . . . 9
β’ (π β πΊ:dom (β D πΉ)βΆβ) |
66 | 65 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β πΊ:dom (β D πΉ)βΆβ) |
67 | 63 | eqcomd 2738 |
. . . . . . . . . . . 12
β’ (π β (β D πΉ) = πΊ) |
68 | 67 | dmeqd 5905 |
. . . . . . . . . . 11
β’ (π β dom (β D πΉ) = dom πΊ) |
69 | | fourierdlem61.domg |
. . . . . . . . . . 11
β’ (π β dom πΊ = (π΄(,)π΅)) |
70 | 68, 69 | eqtr2d 2773 |
. . . . . . . . . 10
β’ (π β (π΄(,)π΅) = dom (β D πΉ)) |
71 | 70 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄(,)π΅) = dom (β D πΉ)) |
72 | 38, 71 | eleqtrd 2835 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + π ) β dom (β D πΉ)) |
73 | 66, 72 | ffvelcdmd 7087 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (πΊβ(π΄ + π )) β β) |
74 | | 1red 11214 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β 1 β
β) |
75 | 9 | ffvelcdmda 7086 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΉβπ₯) β β) |
76 | 75 | recnd 11241 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΉβπ₯) β β) |
77 | 70 | feq2d 6703 |
. . . . . . . . . . 11
β’ (π β (πΊ:(π΄(,)π΅)βΆβ β πΊ:dom (β D πΉ)βΆβ)) |
78 | 65, 77 | mpbird 256 |
. . . . . . . . . 10
β’ (π β πΊ:(π΄(,)π΅)βΆβ) |
79 | 78 | ffvelcdmda 7086 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΊβπ₯) β β) |
80 | 19 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π΄ β β) |
81 | 19 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π΄ β β) |
82 | | 0red 11216 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β 0 β
β) |
83 | 58, 19 | dvmptc 25474 |
. . . . . . . . . . . 12
β’ (π β (β D (π β β β¦ π΄)) = (π β β β¦ 0)) |
84 | | ioossre 13384 |
. . . . . . . . . . . . 13
β’
(0(,)(π΅ β
π΄)) β
β |
85 | 84 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (0(,)(π΅ β π΄)) β β) |
86 | | tgioo4 44276 |
. . . . . . . . . . . 12
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
87 | | iooretop 24281 |
. . . . . . . . . . . . 13
β’
(0(,)(π΅ β
π΄)) β
(topGenβran (,)) |
88 | 87 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (0(,)(π΅ β π΄)) β (topGenβran
(,))) |
89 | 58, 81, 82, 83, 85, 86, 44, 88 | dvmptres 25479 |
. . . . . . . . . . 11
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ π΄)) = (π β (0(,)(π΅ β π΄)) β¦ 0)) |
90 | 17 | recnd 11241 |
. . . . . . . . . . 11
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π β β) |
91 | | recn 11199 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
92 | 91 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
93 | | 1red 11214 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β 1 β
β) |
94 | 58 | dvmptid 25473 |
. . . . . . . . . . . 12
β’ (π β (β D (π β β β¦ π )) = (π β β β¦ 1)) |
95 | 58, 92, 93, 94, 85, 86, 44, 88 | dvmptres 25479 |
. . . . . . . . . . 11
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ π )) = (π β (0(,)(π΅ β π΄)) β¦ 1)) |
96 | 58, 80, 23, 89, 90, 74, 95 | dvmptadd 25476 |
. . . . . . . . . 10
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ (π΄ + π ))) = (π β (0(,)(π΅ β π΄)) β¦ (0 + 1))) |
97 | | 0p1e1 12333 |
. . . . . . . . . . 11
β’ (0 + 1) =
1 |
98 | 97 | mpteq2i 5253 |
. . . . . . . . . 10
β’ (π β (0(,)(π΅ β π΄)) β¦ (0 + 1)) = (π β (0(,)(π΅ β π΄)) β¦ 1) |
99 | 96, 98 | eqtrdi 2788 |
. . . . . . . . 9
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ (π΄ + π ))) = (π β (0(,)(π΅ β π΄)) β¦ 1)) |
100 | 9 | feqmptd 6960 |
. . . . . . . . . . . 12
β’ (π β πΉ = (π₯ β (π΄(,)π΅) β¦ (πΉβπ₯))) |
101 | 100 | eqcomd 2738 |
. . . . . . . . . . 11
β’ (π β (π₯ β (π΄(,)π΅) β¦ (πΉβπ₯)) = πΉ) |
102 | 101 | oveq2d 7424 |
. . . . . . . . . 10
β’ (π β (β D (π₯ β (π΄(,)π΅) β¦ (πΉβπ₯))) = (β D πΉ)) |
103 | 78 | feqmptd 6960 |
. . . . . . . . . 10
β’ (π β πΊ = (π₯ β (π΄(,)π΅) β¦ (πΊβπ₯))) |
104 | 102, 67, 103 | 3eqtrd 2776 |
. . . . . . . . 9
β’ (π β (β D (π₯ β (π΄(,)π΅) β¦ (πΉβπ₯))) = (π₯ β (π΄(,)π΅) β¦ (πΊβπ₯))) |
105 | | fveq2 6891 |
. . . . . . . . 9
β’ (π₯ = (π΄ + π ) β (πΉβπ₯) = (πΉβ(π΄ + π ))) |
106 | | fveq2 6891 |
. . . . . . . . 9
β’ (π₯ = (π΄ + π ) β (πΊβπ₯) = (πΊβ(π΄ + π ))) |
107 | 58, 58, 38, 74, 76, 79, 99, 104, 105, 106 | dvmptco 25488 |
. . . . . . . 8
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ (πΉβ(π΄ + π )))) = (π β (0(,)(π΅ β π΄)) β¦ ((πΊβ(π΄ + π )) Β· 1))) |
108 | 73 | recnd 11241 |
. . . . . . . . . 10
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (πΊβ(π΄ + π )) β β) |
109 | 108 | mulridd 11230 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((πΊβ(π΄ + π )) Β· 1) = (πΊβ(π΄ + π ))) |
110 | 109 | mpteq2dva 5248 |
. . . . . . . 8
β’ (π β (π β (0(,)(π΅ β π΄)) β¦ ((πΊβ(π΄ + π )) Β· 1)) = (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))) |
111 | 107, 110 | eqtrd 2772 |
. . . . . . 7
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ (πΉβ(π΄ + π )))) = (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))) |
112 | | limccl 25391 |
. . . . . . . . 9
β’ (πΉ limβ π΄) β
β |
113 | 112, 46 | sselid 3980 |
. . . . . . . 8
β’ (π β π β β) |
114 | 113 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π β β) |
115 | 113 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
116 | 58, 113 | dvmptc 25474 |
. . . . . . . 8
β’ (π β (β D (π β β β¦ π)) = (π β β β¦ 0)) |
117 | 58, 115, 82, 116, 85, 86, 44, 88 | dvmptres 25479 |
. . . . . . 7
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ π)) = (π β (0(,)(π΅ β π΄)) β¦ 0)) |
118 | 58, 59, 73, 111, 114, 23, 117 | dvmptsub 25483 |
. . . . . 6
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π))) = (π β (0(,)(π΅ β π΄)) β¦ ((πΊβ(π΄ + π )) β 0))) |
119 | 108 | subid1d 11559 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((πΊβ(π΄ + π )) β 0) = (πΊβ(π΄ + π ))) |
120 | 119 | mpteq2dva 5248 |
. . . . . 6
β’ (π β (π β (0(,)(π΅ β π΄)) β¦ ((πΊβ(π΄ + π )) β 0)) = (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))) |
121 | 118, 120 | eqtrd 2772 |
. . . . 5
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π))) = (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))) |
122 | 121 | dmeqd 5905 |
. . . 4
β’ (π β dom (β D (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π))) = dom (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))) |
123 | 73 | ralrimiva 3146 |
. . . . 5
β’ (π β βπ β (0(,)(π΅ β π΄))(πΊβ(π΄ + π )) β β) |
124 | | dmmptg 6241 |
. . . . 5
β’
(βπ β
(0(,)(π΅ β π΄))(πΊβ(π΄ + π )) β β β dom (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π ))) = (0(,)(π΅ β π΄))) |
125 | 123, 124 | syl 17 |
. . . 4
β’ (π β dom (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π ))) = (0(,)(π΅ β π΄))) |
126 | 56, 122, 125 | 3eqtrd 2776 |
. . 3
β’ (π β dom (β D π) = (0(,)(π΅ β π΄))) |
127 | 52 | a1i 11 |
. . . . . . 7
β’ (π β π· = (π β (0(,)(π΅ β π΄)) β¦ π )) |
128 | 127 | oveq2d 7424 |
. . . . . 6
β’ (π β (β D π·) = (β D (π β (0(,)(π΅ β π΄)) β¦ π ))) |
129 | 128, 95 | eqtrd 2772 |
. . . . 5
β’ (π β (β D π·) = (π β (0(,)(π΅ β π΄)) β¦ 1)) |
130 | 129 | dmeqd 5905 |
. . . 4
β’ (π β dom (β D π·) = dom (π β (0(,)(π΅ β π΄)) β¦ 1)) |
131 | 74 | ralrimiva 3146 |
. . . . 5
β’ (π β βπ β (0(,)(π΅ β π΄))1 β β) |
132 | | dmmptg 6241 |
. . . . 5
β’
(βπ β
(0(,)(π΅ β π΄))1 β β β dom
(π β (0(,)(π΅ β π΄)) β¦ 1) = (0(,)(π΅ β π΄))) |
133 | 131, 132 | syl 17 |
. . . 4
β’ (π β dom (π β (0(,)(π΅ β π΄)) β¦ 1) = (0(,)(π΅ β π΄))) |
134 | 130, 133 | eqtrd 2772 |
. . 3
β’ (π β dom (β D π·) = (0(,)(π΅ β π΄))) |
135 | | eqid 2732 |
. . . . 5
β’ (π β (0(,)(π΅ β π΄)) β¦ (πΉβ(π΄ + π ))) = (π β (0(,)(π΅ β π΄)) β¦ (πΉβ(π΄ + π ))) |
136 | | eqid 2732 |
. . . . 5
β’ (π β (0(,)(π΅ β π΄)) β¦ π) = (π β (0(,)(π΅ β π΄)) β¦ π) |
137 | | eqid 2732 |
. . . . 5
β’ (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) = (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) |
138 | 38 | adantrr 715 |
. . . . . 6
β’ ((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) β π΄)) β (π΄ + π ) β (π΄(,)π΅)) |
139 | | eqid 2732 |
. . . . . . . 8
β’ (π β (0(,)(π΅ β π΄)) β¦ π΄) = (π β (0(,)(π΅ β π΄)) β¦ π΄) |
140 | | eqid 2732 |
. . . . . . . 8
β’ (π β (0(,)(π΅ β π΄)) β¦ π ) = (π β (0(,)(π΅ β π΄)) β¦ π ) |
141 | | eqid 2732 |
. . . . . . . 8
β’ (π β (0(,)(π΅ β π΄)) β¦ (π΄ + π )) = (π β (0(,)(π΅ β π΄)) β¦ (π΄ + π )) |
142 | 85, 42 | sstrdi 3994 |
. . . . . . . . 9
β’ (π β (0(,)(π΅ β π΄)) β β) |
143 | 1 | recnd 11241 |
. . . . . . . . 9
β’ (π β 0 β
β) |
144 | 139, 142,
19, 143 | constlimc 44330 |
. . . . . . . 8
β’ (π β π΄ β ((π β (0(,)(π΅ β π΄)) β¦ π΄) limβ 0)) |
145 | 142, 140,
143 | idlimc 44332 |
. . . . . . . 8
β’ (π β 0 β ((π β (0(,)(π΅ β π΄)) β¦ π ) limβ 0)) |
146 | 139, 140,
141, 80, 90, 144, 145 | addlimc 44354 |
. . . . . . 7
β’ (π β (π΄ + 0) β ((π β (0(,)(π΅ β π΄)) β¦ (π΄ + π )) limβ 0)) |
147 | 21, 146 | eqeltrd 2833 |
. . . . . 6
β’ (π β π΄ β ((π β (0(,)(π΅ β π΄)) β¦ (π΄ + π )) limβ 0)) |
148 | 100 | oveq1d 7423 |
. . . . . . 7
β’ (π β (πΉ limβ π΄) = ((π₯ β (π΄(,)π΅) β¦ (πΉβπ₯)) limβ π΄)) |
149 | 46, 148 | eleqtrd 2835 |
. . . . . 6
β’ (π β π β ((π₯ β (π΄(,)π΅) β¦ (πΉβπ₯)) limβ π΄)) |
150 | | simplrr 776 |
. . . . . . 7
β’ (((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) = π΄)) β§ Β¬ (πΉβ(π΄ + π )) = π) β (π΄ + π ) = π΄) |
151 | 15, 30 | gtned 11348 |
. . . . . . . . . 10
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + π ) β π΄) |
152 | 151 | neneqd 2945 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β Β¬ (π΄ + π ) = π΄) |
153 | 152 | adantrr 715 |
. . . . . . . 8
β’ ((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) = π΄)) β Β¬ (π΄ + π ) = π΄) |
154 | 153 | adantr 481 |
. . . . . . 7
β’ (((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) = π΄)) β§ Β¬ (πΉβ(π΄ + π )) = π) β Β¬ (π΄ + π ) = π΄) |
155 | 150, 154 | condan 816 |
. . . . . 6
β’ ((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) = π΄)) β (πΉβ(π΄ + π )) = π) |
156 | 138, 76, 147, 149, 105, 155 | limcco 25409 |
. . . . 5
β’ (π β π β ((π β (0(,)(π΅ β π΄)) β¦ (πΉβ(π΄ + π ))) limβ
0)) |
157 | 136, 142,
113, 143 | constlimc 44330 |
. . . . 5
β’ (π β π β ((π β (0(,)(π΅ β π΄)) β¦ π) limβ 0)) |
158 | 135, 136,
137, 59, 114, 156, 157 | sublimc 44358 |
. . . 4
β’ (π β (π β π) β ((π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) limβ
0)) |
159 | 113 | subidd 11558 |
. . . 4
β’ (π β (π β π) = 0) |
160 | 50 | eqcomi 2741 |
. . . . . 6
β’ (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) = π |
161 | 160 | oveq1i 7418 |
. . . . 5
β’ ((π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) limβ 0) = (π limβ
0) |
162 | 161 | a1i 11 |
. . . 4
β’ (π β ((π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) limβ 0) = (π limβ
0)) |
163 | 158, 159,
162 | 3eltr3d 2847 |
. . 3
β’ (π β 0 β (π limβ
0)) |
164 | 142, 52, 143 | idlimc 44332 |
. . 3
β’ (π β 0 β (π· limβ
0)) |
165 | | lbioo 13354 |
. . . . 5
β’ Β¬ 0
β (0(,)(π΅ β
π΄)) |
166 | 165 | a1i 11 |
. . . 4
β’ (π β Β¬ 0 β (0(,)(π΅ β π΄))) |
167 | | mptresid 6050 |
. . . . . . 7
β’ ( I
βΎ (0(,)(π΅ β
π΄))) = (π β (0(,)(π΅ β π΄)) β¦ π ) |
168 | 127, 167 | eqtr4di 2790 |
. . . . . 6
β’ (π β π· = ( I βΎ (0(,)(π΅ β π΄)))) |
169 | 168 | rneqd 5937 |
. . . . 5
β’ (π β ran π· = ran ( I βΎ (0(,)(π΅ β π΄)))) |
170 | | rnresi 6074 |
. . . . 5
β’ ran ( I
βΎ (0(,)(π΅ β
π΄))) = (0(,)(π΅ β π΄)) |
171 | 169, 170 | eqtr2di 2789 |
. . . 4
β’ (π β (0(,)(π΅ β π΄)) = ran π·) |
172 | 166, 171 | neleqtrd 2855 |
. . 3
β’ (π β Β¬ 0 β ran π·) |
173 | | 0ne1 12282 |
. . . . . 6
β’ 0 β
1 |
174 | 173 | neii 2942 |
. . . . 5
β’ Β¬ 0
= 1 |
175 | | elsng 4642 |
. . . . . 6
β’ (0 β
β β (0 β {1} β 0 = 1)) |
176 | 1, 175 | syl 17 |
. . . . 5
β’ (π β (0 β {1} β 0 =
1)) |
177 | 174, 176 | mtbiri 326 |
. . . 4
β’ (π β Β¬ 0 β
{1}) |
178 | 129 | rneqd 5937 |
. . . . 5
β’ (π β ran (β D π·) = ran (π β (0(,)(π΅ β π΄)) β¦ 1)) |
179 | | eqid 2732 |
. . . . . 6
β’ (π β (0(,)(π΅ β π΄)) β¦ 1) = (π β (0(,)(π΅ β π΄)) β¦ 1) |
180 | 24 | a1i 11 |
. . . . . . . 8
β’ (π β 0 β
β*) |
181 | | ioon0 13349 |
. . . . . . . 8
β’ ((0
β β* β§ (π΅ β π΄) β β*) β
((0(,)(π΅ β π΄)) β β
β 0 <
(π΅ β π΄))) |
182 | 180, 5, 181 | syl2anc 584 |
. . . . . . 7
β’ (π β ((0(,)(π΅ β π΄)) β β
β 0 < (π΅ β π΄))) |
183 | 8, 182 | mpbird 256 |
. . . . . 6
β’ (π β (0(,)(π΅ β π΄)) β β
) |
184 | 179, 183 | rnmptc 7207 |
. . . . 5
β’ (π β ran (π β (0(,)(π΅ β π΄)) β¦ 1) = {1}) |
185 | 178, 184 | eqtr2d 2773 |
. . . 4
β’ (π β {1} = ran (β D π·)) |
186 | 177, 185 | neleqtrd 2855 |
. . 3
β’ (π β Β¬ 0 β ran
(β D π·)) |
187 | 79 | recnd 11241 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΊβπ₯) β β) |
188 | | fourierdlem61.e |
. . . . . 6
β’ (π β πΈ β (πΊ limβ π΄)) |
189 | 103 | oveq1d 7423 |
. . . . . 6
β’ (π β (πΊ limβ π΄) = ((π₯ β (π΄(,)π΅) β¦ (πΊβπ₯)) limβ π΄)) |
190 | 188, 189 | eleqtrd 2835 |
. . . . 5
β’ (π β πΈ β ((π₯ β (π΄(,)π΅) β¦ (πΊβπ₯)) limβ π΄)) |
191 | | simplrr 776 |
. . . . . 6
β’ (((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) = π΄)) β§ Β¬ (πΊβ(π΄ + π )) = πΈ) β (π΄ + π ) = π΄) |
192 | 153 | adantr 481 |
. . . . . 6
β’ (((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) = π΄)) β§ Β¬ (πΊβ(π΄ + π )) = πΈ) β Β¬ (π΄ + π ) = π΄) |
193 | 191, 192 | condan 816 |
. . . . 5
β’ ((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) = π΄)) β (πΊβ(π΄ + π )) = πΈ) |
194 | 138, 187,
147, 190, 106, 193 | limcco 25409 |
. . . 4
β’ (π β πΈ β ((π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π ))) limβ
0)) |
195 | 108 | div1d 11981 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((πΊβ(π΄ + π )) / 1) = (πΊβ(π΄ + π ))) |
196 | 54, 121 | eqtrid 2784 |
. . . . . . . . . . 11
β’ (π β (β D π) = (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))) |
197 | 196 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (β D π) = (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))) |
198 | 197 | fveq1d 6893 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((β D π)βπ ) = ((π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))βπ )) |
199 | | fvmpt4 43931 |
. . . . . . . . . 10
β’ ((π β (0(,)(π΅ β π΄)) β§ (πΊβ(π΄ + π )) β β) β ((π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))βπ ) = (πΊβ(π΄ + π ))) |
200 | 27, 73, 199 | syl2anc 584 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))βπ ) = (πΊβ(π΄ + π ))) |
201 | 198, 200 | eqtr2d 2773 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (πΊβ(π΄ + π )) = ((β D π)βπ )) |
202 | 129 | fveq1d 6893 |
. . . . . . . . . 10
β’ (π β ((β D π·)βπ ) = ((π β (0(,)(π΅ β π΄)) β¦ 1)βπ )) |
203 | 202 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((β D π·)βπ ) = ((π β (0(,)(π΅ β π΄)) β¦ 1)βπ )) |
204 | | fvmpt4 43931 |
. . . . . . . . . 10
β’ ((π β (0(,)(π΅ β π΄)) β§ 1 β β) β ((π β (0(,)(π΅ β π΄)) β¦ 1)βπ ) = 1) |
205 | 27, 74, 204 | syl2anc 584 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((π β (0(,)(π΅ β π΄)) β¦ 1)βπ ) = 1) |
206 | 203, 205 | eqtr2d 2773 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β 1 = ((β D π·)βπ )) |
207 | 201, 206 | oveq12d 7426 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((πΊβ(π΄ + π )) / 1) = (((β D π)βπ ) / ((β D π·)βπ ))) |
208 | 195, 207 | eqtr3d 2774 |
. . . . . 6
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (πΊβ(π΄ + π )) = (((β D π)βπ ) / ((β D π·)βπ ))) |
209 | 208 | mpteq2dva 5248 |
. . . . 5
β’ (π β (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π ))) = (π β (0(,)(π΅ β π΄)) β¦ (((β D π)βπ ) / ((β D π·)βπ )))) |
210 | 209 | oveq1d 7423 |
. . . 4
β’ (π β ((π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π ))) limβ 0) = ((π β (0(,)(π΅ β π΄)) β¦ (((β D π)βπ ) / ((β D π·)βπ ))) limβ
0)) |
211 | 194, 210 | eleqtrd 2835 |
. . 3
β’ (π β πΈ β ((π β (0(,)(π΅ β π΄)) β¦ (((β D π)βπ ) / ((β D π·)βπ ))) limβ
0)) |
212 | 1, 5, 8, 51, 53, 126, 134, 163, 164, 172, 186, 211 | lhop1 25530 |
. 2
β’ (π β πΈ β ((π β (0(,)(π΅ β π΄)) β¦ ((πβπ ) / (π·βπ ))) limβ
0)) |
213 | 50 | fvmpt2 7009 |
. . . . . . 7
β’ ((π β (0(,)(π΅ β π΄)) β§ ((πΉβ(π΄ + π )) β π) β β) β (πβπ ) = ((πΉβ(π΄ + π )) β π)) |
214 | 27, 49, 213 | syl2anc 584 |
. . . . . 6
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (πβπ ) = ((πΉβ(π΄ + π )) β π)) |
215 | 52 | fvmpt2 7009 |
. . . . . . 7
β’ ((π β (0(,)(π΅ β π΄)) β§ π β (0(,)(π΅ β π΄))) β (π·βπ ) = π ) |
216 | 27, 27, 215 | syl2anc 584 |
. . . . . 6
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π·βπ ) = π ) |
217 | 214, 216 | oveq12d 7426 |
. . . . 5
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((πβπ ) / (π·βπ )) = (((πΉβ(π΄ + π )) β π) / π )) |
218 | 217 | mpteq2dva 5248 |
. . . 4
β’ (π β (π β (0(,)(π΅ β π΄)) β¦ ((πβπ ) / (π·βπ ))) = (π β (0(,)(π΅ β π΄)) β¦ (((πΉβ(π΄ + π )) β π) / π ))) |
219 | | fourierdlem61.h |
. . . 4
β’ π» = (π β (0(,)(π΅ β π΄)) β¦ (((πΉβ(π΄ + π )) β π) / π )) |
220 | 218, 219 | eqtr4di 2790 |
. . 3
β’ (π β (π β (0(,)(π΅ β π΄)) β¦ ((πβπ ) / (π·βπ ))) = π») |
221 | 220 | oveq1d 7423 |
. 2
β’ (π β ((π β (0(,)(π΅ β π΄)) β¦ ((πβπ ) / (π·βπ ))) limβ 0) = (π» limβ
0)) |
222 | 212, 221 | eleqtrd 2835 |
1
β’ (π β πΈ β (π» limβ 0)) |