Step | Hyp | Ref
| Expression |
1 | | 0red 11163 |
. . 3
β’ (π β 0 β
β) |
2 | | fourierdlem61.b |
. . . . 5
β’ (π β π΅ β β) |
3 | | fourierdlem61.a |
. . . . 5
β’ (π β π΄ β β) |
4 | 2, 3 | resubcld 11588 |
. . . 4
β’ (π β (π΅ β π΄) β β) |
5 | 4 | rexrd 11210 |
. . 3
β’ (π β (π΅ β π΄) β
β*) |
6 | | fourierdlem61.altb |
. . . 4
β’ (π β π΄ < π΅) |
7 | 3, 2 | posdifd 11747 |
. . . 4
β’ (π β (π΄ < π΅ β 0 < (π΅ β π΄))) |
8 | 6, 7 | mpbid 231 |
. . 3
β’ (π β 0 < (π΅ β π΄)) |
9 | | fourierdlem61.f |
. . . . . . 7
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
10 | 9 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0(,)(π΅ β π΄))) β πΉ:(π΄(,)π΅)βΆβ) |
11 | 3 | rexrd 11210 |
. . . . . . . 8
β’ (π β π΄ β
β*) |
12 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π΄ β
β*) |
13 | 2 | rexrd 11210 |
. . . . . . . 8
β’ (π β π΅ β
β*) |
14 | 13 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π΅ β
β*) |
15 | 3 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π΄ β β) |
16 | | elioore 13300 |
. . . . . . . . 9
β’ (π β (0(,)(π΅ β π΄)) β π β β) |
17 | 16 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π β β) |
18 | 15, 17 | readdcld 11189 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + π ) β β) |
19 | 3 | recnd 11188 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
20 | 19 | addid1d 11360 |
. . . . . . . . . 10
β’ (π β (π΄ + 0) = π΄) |
21 | 20 | eqcomd 2739 |
. . . . . . . . 9
β’ (π β π΄ = (π΄ + 0)) |
22 | 21 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π΄ = (π΄ + 0)) |
23 | | 0red 11163 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β 0 β
β) |
24 | | 0xr 11207 |
. . . . . . . . . . 11
β’ 0 β
β* |
25 | 24 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (0(,)(π΅ β π΄))) β 0 β
β*) |
26 | 5 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΅ β π΄) β
β*) |
27 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π β (0(,)(π΅ β π΄))) |
28 | 25, 26, 27 | ioogtlbd 43874 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β 0 < π ) |
29 | 23, 17, 15, 28 | ltadd2dd 11319 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + 0) < (π΄ + π )) |
30 | 22, 29 | eqbrtrd 5128 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π΄ < (π΄ + π )) |
31 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΅ β π΄) β β) |
32 | 25, 26, 27 | iooltubd 43868 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π < (π΅ β π΄)) |
33 | 17, 31, 15, 32 | ltadd2dd 11319 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + π ) < (π΄ + (π΅ β π΄))) |
34 | 2 | recnd 11188 |
. . . . . . . . . 10
β’ (π β π΅ β β) |
35 | 19, 34 | pncan3d 11520 |
. . . . . . . . 9
β’ (π β (π΄ + (π΅ β π΄)) = π΅) |
36 | 35 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + (π΅ β π΄)) = π΅) |
37 | 33, 36 | breqtrd 5132 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + π ) < π΅) |
38 | 12, 14, 18, 30, 37 | eliood 43822 |
. . . . . 6
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + π ) β (π΄(,)π΅)) |
39 | 10, 38 | ffvelcdmd 7037 |
. . . . 5
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (πΉβ(π΄ + π )) β β) |
40 | | ioossre 13331 |
. . . . . . . . 9
β’ (π΄(,)π΅) β β |
41 | 40 | a1i 11 |
. . . . . . . 8
β’ (π β (π΄(,)π΅) β β) |
42 | | ax-resscn 11113 |
. . . . . . . 8
β’ β
β β |
43 | 41, 42 | sstrdi 3957 |
. . . . . . 7
β’ (π β (π΄(,)π΅) β β) |
44 | | eqid 2733 |
. . . . . . . 8
β’
(TopOpenββfld) =
(TopOpenββfld) |
45 | 44, 13, 3, 6 | lptioo1cn 43973 |
. . . . . . 7
β’ (π β π΄ β
((limPtβ(TopOpenββfld))β(π΄(,)π΅))) |
46 | | fourierdlem61.y |
. . . . . . 7
β’ (π β π β (πΉ limβ π΄)) |
47 | 9, 43, 45, 46 | limcrecl 43956 |
. . . . . 6
β’ (π β π β β) |
48 | 47 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π β β) |
49 | 39, 48 | resubcld 11588 |
. . . 4
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((πΉβ(π΄ + π )) β π) β β) |
50 | | fourierdlem61.n |
. . . 4
β’ π = (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) |
51 | 49, 50 | fmptd 7063 |
. . 3
β’ (π β π:(0(,)(π΅ β π΄))βΆβ) |
52 | | fourierdlem61.d |
. . . 4
β’ π· = (π β (0(,)(π΅ β π΄)) β¦ π ) |
53 | 17, 52 | fmptd 7063 |
. . 3
β’ (π β π·:(0(,)(π΅ β π΄))βΆβ) |
54 | 50 | oveq2i 7369 |
. . . . . 6
β’ (β
D π) = (β D (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π))) |
55 | 54 | a1i 11 |
. . . . 5
β’ (π β (β D π) = (β D (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)))) |
56 | 55 | dmeqd 5862 |
. . . 4
β’ (π β dom (β D π) = dom (β D (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)))) |
57 | | reelprrecn 11148 |
. . . . . . . 8
β’ β
β {β, β} |
58 | 57 | a1i 11 |
. . . . . . 7
β’ (π β β β {β,
β}) |
59 | 39 | recnd 11188 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (πΉβ(π΄ + π )) β β) |
60 | | dvfre 25331 |
. . . . . . . . . . 11
β’ ((πΉ:(π΄(,)π΅)βΆβ β§ (π΄(,)π΅) β β) β (β D πΉ):dom (β D πΉ)βΆβ) |
61 | 9, 41, 60 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (β D πΉ):dom (β D πΉ)βΆβ) |
62 | | fourierdlem61.g |
. . . . . . . . . . . 12
β’ πΊ = (β D πΉ) |
63 | 62 | a1i 11 |
. . . . . . . . . . 11
β’ (π β πΊ = (β D πΉ)) |
64 | 63 | feq1d 6654 |
. . . . . . . . . 10
β’ (π β (πΊ:dom (β D πΉ)βΆβ β (β D πΉ):dom (β D πΉ)βΆβ)) |
65 | 61, 64 | mpbird 257 |
. . . . . . . . 9
β’ (π β πΊ:dom (β D πΉ)βΆβ) |
66 | 65 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β πΊ:dom (β D πΉ)βΆβ) |
67 | 63 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ (π β (β D πΉ) = πΊ) |
68 | 67 | dmeqd 5862 |
. . . . . . . . . . 11
β’ (π β dom (β D πΉ) = dom πΊ) |
69 | | fourierdlem61.domg |
. . . . . . . . . . 11
β’ (π β dom πΊ = (π΄(,)π΅)) |
70 | 68, 69 | eqtr2d 2774 |
. . . . . . . . . 10
β’ (π β (π΄(,)π΅) = dom (β D πΉ)) |
71 | 70 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄(,)π΅) = dom (β D πΉ)) |
72 | 38, 71 | eleqtrd 2836 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + π ) β dom (β D πΉ)) |
73 | 66, 72 | ffvelcdmd 7037 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (πΊβ(π΄ + π )) β β) |
74 | | 1red 11161 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β 1 β
β) |
75 | 9 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΉβπ₯) β β) |
76 | 75 | recnd 11188 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΉβπ₯) β β) |
77 | 70 | feq2d 6655 |
. . . . . . . . . . 11
β’ (π β (πΊ:(π΄(,)π΅)βΆβ β πΊ:dom (β D πΉ)βΆβ)) |
78 | 65, 77 | mpbird 257 |
. . . . . . . . . 10
β’ (π β πΊ:(π΄(,)π΅)βΆβ) |
79 | 78 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΊβπ₯) β β) |
80 | 19 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π΄ β β) |
81 | 19 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π΄ β β) |
82 | | 0red 11163 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β 0 β
β) |
83 | 58, 19 | dvmptc 25338 |
. . . . . . . . . . . 12
β’ (π β (β D (π β β β¦ π΄)) = (π β β β¦ 0)) |
84 | | ioossre 13331 |
. . . . . . . . . . . . 13
β’
(0(,)(π΅ β
π΄)) β
β |
85 | 84 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (0(,)(π΅ β π΄)) β β) |
86 | | tgioo4 43897 |
. . . . . . . . . . . 12
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
87 | | iooretop 24145 |
. . . . . . . . . . . . 13
β’
(0(,)(π΅ β
π΄)) β
(topGenβran (,)) |
88 | 87 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (0(,)(π΅ β π΄)) β (topGenβran
(,))) |
89 | 58, 81, 82, 83, 85, 86, 44, 88 | dvmptres 25343 |
. . . . . . . . . . 11
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ π΄)) = (π β (0(,)(π΅ β π΄)) β¦ 0)) |
90 | 17 | recnd 11188 |
. . . . . . . . . . 11
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π β β) |
91 | | recn 11146 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
92 | 91 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
93 | | 1red 11161 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β 1 β
β) |
94 | 58 | dvmptid 25337 |
. . . . . . . . . . . 12
β’ (π β (β D (π β β β¦ π )) = (π β β β¦ 1)) |
95 | 58, 92, 93, 94, 85, 86, 44, 88 | dvmptres 25343 |
. . . . . . . . . . 11
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ π )) = (π β (0(,)(π΅ β π΄)) β¦ 1)) |
96 | 58, 80, 23, 89, 90, 74, 95 | dvmptadd 25340 |
. . . . . . . . . 10
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ (π΄ + π ))) = (π β (0(,)(π΅ β π΄)) β¦ (0 + 1))) |
97 | | 0p1e1 12280 |
. . . . . . . . . . 11
β’ (0 + 1) =
1 |
98 | 97 | mpteq2i 5211 |
. . . . . . . . . 10
β’ (π β (0(,)(π΅ β π΄)) β¦ (0 + 1)) = (π β (0(,)(π΅ β π΄)) β¦ 1) |
99 | 96, 98 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ (π΄ + π ))) = (π β (0(,)(π΅ β π΄)) β¦ 1)) |
100 | 9 | feqmptd 6911 |
. . . . . . . . . . . 12
β’ (π β πΉ = (π₯ β (π΄(,)π΅) β¦ (πΉβπ₯))) |
101 | 100 | eqcomd 2739 |
. . . . . . . . . . 11
β’ (π β (π₯ β (π΄(,)π΅) β¦ (πΉβπ₯)) = πΉ) |
102 | 101 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π β (β D (π₯ β (π΄(,)π΅) β¦ (πΉβπ₯))) = (β D πΉ)) |
103 | 78 | feqmptd 6911 |
. . . . . . . . . 10
β’ (π β πΊ = (π₯ β (π΄(,)π΅) β¦ (πΊβπ₯))) |
104 | 102, 67, 103 | 3eqtrd 2777 |
. . . . . . . . 9
β’ (π β (β D (π₯ β (π΄(,)π΅) β¦ (πΉβπ₯))) = (π₯ β (π΄(,)π΅) β¦ (πΊβπ₯))) |
105 | | fveq2 6843 |
. . . . . . . . 9
β’ (π₯ = (π΄ + π ) β (πΉβπ₯) = (πΉβ(π΄ + π ))) |
106 | | fveq2 6843 |
. . . . . . . . 9
β’ (π₯ = (π΄ + π ) β (πΊβπ₯) = (πΊβ(π΄ + π ))) |
107 | 58, 58, 38, 74, 76, 79, 99, 104, 105, 106 | dvmptco 25352 |
. . . . . . . 8
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ (πΉβ(π΄ + π )))) = (π β (0(,)(π΅ β π΄)) β¦ ((πΊβ(π΄ + π )) Β· 1))) |
108 | 73 | recnd 11188 |
. . . . . . . . . 10
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (πΊβ(π΄ + π )) β β) |
109 | 108 | mulid1d 11177 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((πΊβ(π΄ + π )) Β· 1) = (πΊβ(π΄ + π ))) |
110 | 109 | mpteq2dva 5206 |
. . . . . . . 8
β’ (π β (π β (0(,)(π΅ β π΄)) β¦ ((πΊβ(π΄ + π )) Β· 1)) = (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))) |
111 | 107, 110 | eqtrd 2773 |
. . . . . . 7
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ (πΉβ(π΄ + π )))) = (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))) |
112 | | limccl 25255 |
. . . . . . . . 9
β’ (πΉ limβ π΄) β
β |
113 | 112, 46 | sselid 3943 |
. . . . . . . 8
β’ (π β π β β) |
114 | 113 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β π β β) |
115 | 113 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
116 | 58, 113 | dvmptc 25338 |
. . . . . . . 8
β’ (π β (β D (π β β β¦ π)) = (π β β β¦ 0)) |
117 | 58, 115, 82, 116, 85, 86, 44, 88 | dvmptres 25343 |
. . . . . . 7
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ π)) = (π β (0(,)(π΅ β π΄)) β¦ 0)) |
118 | 58, 59, 73, 111, 114, 23, 117 | dvmptsub 25347 |
. . . . . 6
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π))) = (π β (0(,)(π΅ β π΄)) β¦ ((πΊβ(π΄ + π )) β 0))) |
119 | 108 | subid1d 11506 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((πΊβ(π΄ + π )) β 0) = (πΊβ(π΄ + π ))) |
120 | 119 | mpteq2dva 5206 |
. . . . . 6
β’ (π β (π β (0(,)(π΅ β π΄)) β¦ ((πΊβ(π΄ + π )) β 0)) = (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))) |
121 | 118, 120 | eqtrd 2773 |
. . . . 5
β’ (π β (β D (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π))) = (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))) |
122 | 121 | dmeqd 5862 |
. . . 4
β’ (π β dom (β D (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π))) = dom (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))) |
123 | 73 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β (0(,)(π΅ β π΄))(πΊβ(π΄ + π )) β β) |
124 | | dmmptg 6195 |
. . . . 5
β’
(βπ β
(0(,)(π΅ β π΄))(πΊβ(π΄ + π )) β β β dom (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π ))) = (0(,)(π΅ β π΄))) |
125 | 123, 124 | syl 17 |
. . . 4
β’ (π β dom (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π ))) = (0(,)(π΅ β π΄))) |
126 | 56, 122, 125 | 3eqtrd 2777 |
. . 3
β’ (π β dom (β D π) = (0(,)(π΅ β π΄))) |
127 | 52 | a1i 11 |
. . . . . . 7
β’ (π β π· = (π β (0(,)(π΅ β π΄)) β¦ π )) |
128 | 127 | oveq2d 7374 |
. . . . . 6
β’ (π β (β D π·) = (β D (π β (0(,)(π΅ β π΄)) β¦ π ))) |
129 | 128, 95 | eqtrd 2773 |
. . . . 5
β’ (π β (β D π·) = (π β (0(,)(π΅ β π΄)) β¦ 1)) |
130 | 129 | dmeqd 5862 |
. . . 4
β’ (π β dom (β D π·) = dom (π β (0(,)(π΅ β π΄)) β¦ 1)) |
131 | 74 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β (0(,)(π΅ β π΄))1 β β) |
132 | | dmmptg 6195 |
. . . . 5
β’
(βπ β
(0(,)(π΅ β π΄))1 β β β dom
(π β (0(,)(π΅ β π΄)) β¦ 1) = (0(,)(π΅ β π΄))) |
133 | 131, 132 | syl 17 |
. . . 4
β’ (π β dom (π β (0(,)(π΅ β π΄)) β¦ 1) = (0(,)(π΅ β π΄))) |
134 | 130, 133 | eqtrd 2773 |
. . 3
β’ (π β dom (β D π·) = (0(,)(π΅ β π΄))) |
135 | | eqid 2733 |
. . . . 5
β’ (π β (0(,)(π΅ β π΄)) β¦ (πΉβ(π΄ + π ))) = (π β (0(,)(π΅ β π΄)) β¦ (πΉβ(π΄ + π ))) |
136 | | eqid 2733 |
. . . . 5
β’ (π β (0(,)(π΅ β π΄)) β¦ π) = (π β (0(,)(π΅ β π΄)) β¦ π) |
137 | | eqid 2733 |
. . . . 5
β’ (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) = (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) |
138 | 38 | adantrr 716 |
. . . . . 6
β’ ((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) β π΄)) β (π΄ + π ) β (π΄(,)π΅)) |
139 | | eqid 2733 |
. . . . . . . 8
β’ (π β (0(,)(π΅ β π΄)) β¦ π΄) = (π β (0(,)(π΅ β π΄)) β¦ π΄) |
140 | | eqid 2733 |
. . . . . . . 8
β’ (π β (0(,)(π΅ β π΄)) β¦ π ) = (π β (0(,)(π΅ β π΄)) β¦ π ) |
141 | | eqid 2733 |
. . . . . . . 8
β’ (π β (0(,)(π΅ β π΄)) β¦ (π΄ + π )) = (π β (0(,)(π΅ β π΄)) β¦ (π΄ + π )) |
142 | 85, 42 | sstrdi 3957 |
. . . . . . . . 9
β’ (π β (0(,)(π΅ β π΄)) β β) |
143 | 1 | recnd 11188 |
. . . . . . . . 9
β’ (π β 0 β
β) |
144 | 139, 142,
19, 143 | constlimc 43951 |
. . . . . . . 8
β’ (π β π΄ β ((π β (0(,)(π΅ β π΄)) β¦ π΄) limβ 0)) |
145 | 142, 140,
143 | idlimc 43953 |
. . . . . . . 8
β’ (π β 0 β ((π β (0(,)(π΅ β π΄)) β¦ π ) limβ 0)) |
146 | 139, 140,
141, 80, 90, 144, 145 | addlimc 43975 |
. . . . . . 7
β’ (π β (π΄ + 0) β ((π β (0(,)(π΅ β π΄)) β¦ (π΄ + π )) limβ 0)) |
147 | 21, 146 | eqeltrd 2834 |
. . . . . 6
β’ (π β π΄ β ((π β (0(,)(π΅ β π΄)) β¦ (π΄ + π )) limβ 0)) |
148 | 100 | oveq1d 7373 |
. . . . . . 7
β’ (π β (πΉ limβ π΄) = ((π₯ β (π΄(,)π΅) β¦ (πΉβπ₯)) limβ π΄)) |
149 | 46, 148 | eleqtrd 2836 |
. . . . . 6
β’ (π β π β ((π₯ β (π΄(,)π΅) β¦ (πΉβπ₯)) limβ π΄)) |
150 | | simplrr 777 |
. . . . . . 7
β’ (((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) = π΄)) β§ Β¬ (πΉβ(π΄ + π )) = π) β (π΄ + π ) = π΄) |
151 | 15, 30 | gtned 11295 |
. . . . . . . . . 10
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π΄ + π ) β π΄) |
152 | 151 | neneqd 2945 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β Β¬ (π΄ + π ) = π΄) |
153 | 152 | adantrr 716 |
. . . . . . . 8
β’ ((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) = π΄)) β Β¬ (π΄ + π ) = π΄) |
154 | 153 | adantr 482 |
. . . . . . 7
β’ (((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) = π΄)) β§ Β¬ (πΉβ(π΄ + π )) = π) β Β¬ (π΄ + π ) = π΄) |
155 | 150, 154 | condan 817 |
. . . . . 6
β’ ((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) = π΄)) β (πΉβ(π΄ + π )) = π) |
156 | 138, 76, 147, 149, 105, 155 | limcco 25273 |
. . . . 5
β’ (π β π β ((π β (0(,)(π΅ β π΄)) β¦ (πΉβ(π΄ + π ))) limβ
0)) |
157 | 136, 142,
113, 143 | constlimc 43951 |
. . . . 5
β’ (π β π β ((π β (0(,)(π΅ β π΄)) β¦ π) limβ 0)) |
158 | 135, 136,
137, 59, 114, 156, 157 | sublimc 43979 |
. . . 4
β’ (π β (π β π) β ((π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) limβ
0)) |
159 | 113 | subidd 11505 |
. . . 4
β’ (π β (π β π) = 0) |
160 | 50 | eqcomi 2742 |
. . . . . 6
β’ (π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) = π |
161 | 160 | oveq1i 7368 |
. . . . 5
β’ ((π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) limβ 0) = (π limβ
0) |
162 | 161 | a1i 11 |
. . . 4
β’ (π β ((π β (0(,)(π΅ β π΄)) β¦ ((πΉβ(π΄ + π )) β π)) limβ 0) = (π limβ
0)) |
163 | 158, 159,
162 | 3eltr3d 2848 |
. . 3
β’ (π β 0 β (π limβ
0)) |
164 | 142, 52, 143 | idlimc 43953 |
. . 3
β’ (π β 0 β (π· limβ
0)) |
165 | | lbioo 13301 |
. . . . 5
β’ Β¬ 0
β (0(,)(π΅ β
π΄)) |
166 | 165 | a1i 11 |
. . . 4
β’ (π β Β¬ 0 β (0(,)(π΅ β π΄))) |
167 | | mptresid 6005 |
. . . . . . 7
β’ ( I
βΎ (0(,)(π΅ β
π΄))) = (π β (0(,)(π΅ β π΄)) β¦ π ) |
168 | 127, 167 | eqtr4di 2791 |
. . . . . 6
β’ (π β π· = ( I βΎ (0(,)(π΅ β π΄)))) |
169 | 168 | rneqd 5894 |
. . . . 5
β’ (π β ran π· = ran ( I βΎ (0(,)(π΅ β π΄)))) |
170 | | rnresi 6028 |
. . . . 5
β’ ran ( I
βΎ (0(,)(π΅ β
π΄))) = (0(,)(π΅ β π΄)) |
171 | 169, 170 | eqtr2di 2790 |
. . . 4
β’ (π β (0(,)(π΅ β π΄)) = ran π·) |
172 | 166, 171 | neleqtrd 2856 |
. . 3
β’ (π β Β¬ 0 β ran π·) |
173 | | 0ne1 12229 |
. . . . . 6
β’ 0 β
1 |
174 | 173 | neii 2942 |
. . . . 5
β’ Β¬ 0
= 1 |
175 | | elsng 4601 |
. . . . . 6
β’ (0 β
β β (0 β {1} β 0 = 1)) |
176 | 1, 175 | syl 17 |
. . . . 5
β’ (π β (0 β {1} β 0 =
1)) |
177 | 174, 176 | mtbiri 327 |
. . . 4
β’ (π β Β¬ 0 β
{1}) |
178 | 129 | rneqd 5894 |
. . . . 5
β’ (π β ran (β D π·) = ran (π β (0(,)(π΅ β π΄)) β¦ 1)) |
179 | | eqid 2733 |
. . . . . 6
β’ (π β (0(,)(π΅ β π΄)) β¦ 1) = (π β (0(,)(π΅ β π΄)) β¦ 1) |
180 | 24 | a1i 11 |
. . . . . . . 8
β’ (π β 0 β
β*) |
181 | | ioon0 13296 |
. . . . . . . 8
β’ ((0
β β* β§ (π΅ β π΄) β β*) β
((0(,)(π΅ β π΄)) β β
β 0 <
(π΅ β π΄))) |
182 | 180, 5, 181 | syl2anc 585 |
. . . . . . 7
β’ (π β ((0(,)(π΅ β π΄)) β β
β 0 < (π΅ β π΄))) |
183 | 8, 182 | mpbird 257 |
. . . . . 6
β’ (π β (0(,)(π΅ β π΄)) β β
) |
184 | 179, 183 | rnmptc 7157 |
. . . . 5
β’ (π β ran (π β (0(,)(π΅ β π΄)) β¦ 1) = {1}) |
185 | 178, 184 | eqtr2d 2774 |
. . . 4
β’ (π β {1} = ran (β D π·)) |
186 | 177, 185 | neleqtrd 2856 |
. . 3
β’ (π β Β¬ 0 β ran
(β D π·)) |
187 | 79 | recnd 11188 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β (πΊβπ₯) β β) |
188 | | fourierdlem61.e |
. . . . . 6
β’ (π β πΈ β (πΊ limβ π΄)) |
189 | 103 | oveq1d 7373 |
. . . . . 6
β’ (π β (πΊ limβ π΄) = ((π₯ β (π΄(,)π΅) β¦ (πΊβπ₯)) limβ π΄)) |
190 | 188, 189 | eleqtrd 2836 |
. . . . 5
β’ (π β πΈ β ((π₯ β (π΄(,)π΅) β¦ (πΊβπ₯)) limβ π΄)) |
191 | | simplrr 777 |
. . . . . 6
β’ (((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) = π΄)) β§ Β¬ (πΊβ(π΄ + π )) = πΈ) β (π΄ + π ) = π΄) |
192 | 153 | adantr 482 |
. . . . . 6
β’ (((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) = π΄)) β§ Β¬ (πΊβ(π΄ + π )) = πΈ) β Β¬ (π΄ + π ) = π΄) |
193 | 191, 192 | condan 817 |
. . . . 5
β’ ((π β§ (π β (0(,)(π΅ β π΄)) β§ (π΄ + π ) = π΄)) β (πΊβ(π΄ + π )) = πΈ) |
194 | 138, 187,
147, 190, 106, 193 | limcco 25273 |
. . . 4
β’ (π β πΈ β ((π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π ))) limβ
0)) |
195 | 108 | div1d 11928 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((πΊβ(π΄ + π )) / 1) = (πΊβ(π΄ + π ))) |
196 | 54, 121 | eqtrid 2785 |
. . . . . . . . . . 11
β’ (π β (β D π) = (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))) |
197 | 196 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (β D π) = (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))) |
198 | 197 | fveq1d 6845 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((β D π)βπ ) = ((π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))βπ )) |
199 | | fvmpt4 43551 |
. . . . . . . . . 10
β’ ((π β (0(,)(π΅ β π΄)) β§ (πΊβ(π΄ + π )) β β) β ((π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))βπ ) = (πΊβ(π΄ + π ))) |
200 | 27, 73, 199 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π )))βπ ) = (πΊβ(π΄ + π ))) |
201 | 198, 200 | eqtr2d 2774 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (πΊβ(π΄ + π )) = ((β D π)βπ )) |
202 | 129 | fveq1d 6845 |
. . . . . . . . . 10
β’ (π β ((β D π·)βπ ) = ((π β (0(,)(π΅ β π΄)) β¦ 1)βπ )) |
203 | 202 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((β D π·)βπ ) = ((π β (0(,)(π΅ β π΄)) β¦ 1)βπ )) |
204 | | fvmpt4 43551 |
. . . . . . . . . 10
β’ ((π β (0(,)(π΅ β π΄)) β§ 1 β β) β ((π β (0(,)(π΅ β π΄)) β¦ 1)βπ ) = 1) |
205 | 27, 74, 204 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((π β (0(,)(π΅ β π΄)) β¦ 1)βπ ) = 1) |
206 | 203, 205 | eqtr2d 2774 |
. . . . . . . 8
β’ ((π β§ π β (0(,)(π΅ β π΄))) β 1 = ((β D π·)βπ )) |
207 | 201, 206 | oveq12d 7376 |
. . . . . . 7
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((πΊβ(π΄ + π )) / 1) = (((β D π)βπ ) / ((β D π·)βπ ))) |
208 | 195, 207 | eqtr3d 2775 |
. . . . . 6
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (πΊβ(π΄ + π )) = (((β D π)βπ ) / ((β D π·)βπ ))) |
209 | 208 | mpteq2dva 5206 |
. . . . 5
β’ (π β (π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π ))) = (π β (0(,)(π΅ β π΄)) β¦ (((β D π)βπ ) / ((β D π·)βπ )))) |
210 | 209 | oveq1d 7373 |
. . . 4
β’ (π β ((π β (0(,)(π΅ β π΄)) β¦ (πΊβ(π΄ + π ))) limβ 0) = ((π β (0(,)(π΅ β π΄)) β¦ (((β D π)βπ ) / ((β D π·)βπ ))) limβ
0)) |
211 | 194, 210 | eleqtrd 2836 |
. . 3
β’ (π β πΈ β ((π β (0(,)(π΅ β π΄)) β¦ (((β D π)βπ ) / ((β D π·)βπ ))) limβ
0)) |
212 | 1, 5, 8, 51, 53, 126, 134, 163, 164, 172, 186, 211 | lhop1 25394 |
. 2
β’ (π β πΈ β ((π β (0(,)(π΅ β π΄)) β¦ ((πβπ ) / (π·βπ ))) limβ
0)) |
213 | 50 | fvmpt2 6960 |
. . . . . . 7
β’ ((π β (0(,)(π΅ β π΄)) β§ ((πΉβ(π΄ + π )) β π) β β) β (πβπ ) = ((πΉβ(π΄ + π )) β π)) |
214 | 27, 49, 213 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (πβπ ) = ((πΉβ(π΄ + π )) β π)) |
215 | 52 | fvmpt2 6960 |
. . . . . . 7
β’ ((π β (0(,)(π΅ β π΄)) β§ π β (0(,)(π΅ β π΄))) β (π·βπ ) = π ) |
216 | 27, 27, 215 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β (0(,)(π΅ β π΄))) β (π·βπ ) = π ) |
217 | 214, 216 | oveq12d 7376 |
. . . . 5
β’ ((π β§ π β (0(,)(π΅ β π΄))) β ((πβπ ) / (π·βπ )) = (((πΉβ(π΄ + π )) β π) / π )) |
218 | 217 | mpteq2dva 5206 |
. . . 4
β’ (π β (π β (0(,)(π΅ β π΄)) β¦ ((πβπ ) / (π·βπ ))) = (π β (0(,)(π΅ β π΄)) β¦ (((πΉβ(π΄ + π )) β π) / π ))) |
219 | | fourierdlem61.h |
. . . 4
β’ π» = (π β (0(,)(π΅ β π΄)) β¦ (((πΉβ(π΄ + π )) β π) / π )) |
220 | 218, 219 | eqtr4di 2791 |
. . 3
β’ (π β (π β (0(,)(π΅ β π΄)) β¦ ((πβπ ) / (π·βπ ))) = π») |
221 | 220 | oveq1d 7373 |
. 2
β’ (π β ((π β (0(,)(π΅ β π΄)) β¦ ((πβπ ) / (π·βπ ))) limβ 0) = (π» limβ
0)) |
222 | 212, 221 | eleqtrd 2836 |
1
β’ (π β πΈ β (π» limβ 0)) |