Step | Hyp | Ref
| Expression |
1 | | fourierdlem60.a |
. . . . 5
β’ (π β π΄ β β) |
2 | | fourierdlem60.b |
. . . . 5
β’ (π β π΅ β β) |
3 | 1, 2 | resubcld 11588 |
. . . 4
β’ (π β (π΄ β π΅) β β) |
4 | 3 | rexrd 11210 |
. . 3
β’ (π β (π΄ β π΅) β
β*) |
5 | | 0red 11163 |
. . 3
β’ (π β 0 β
β) |
6 | | fourierdlem60.altb |
. . . 4
β’ (π β π΄ < π΅) |
7 | 1, 2 | sublt0d 11786 |
. . . 4
β’ (π β ((π΄ β π΅) < 0 β π΄ < π΅)) |
8 | 6, 7 | mpbird 257 |
. . 3
β’ (π β (π΄ β π΅) < 0) |
9 | | fourierdlem60.f |
. . . . . . 7
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
10 | 9 | adantr 482 |
. . . . . 6
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β πΉ:(π΄(,)π΅)βΆβ) |
11 | 1 | rexrd 11210 |
. . . . . . . 8
β’ (π β π΄ β
β*) |
12 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β π΄ β
β*) |
13 | 2 | rexrd 11210 |
. . . . . . . 8
β’ (π β π΅ β
β*) |
14 | 13 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β π΅ β
β*) |
15 | 2 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β π΅ β β) |
16 | | elioore 13300 |
. . . . . . . . 9
β’ (π β ((π΄ β π΅)(,)0) β π β β) |
17 | 16 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β π β β) |
18 | 15, 17 | readdcld 11189 |
. . . . . . 7
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β (π΅ + π ) β β) |
19 | 2 | recnd 11188 |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
20 | 1 | recnd 11188 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
21 | 19, 20 | pncan3d 11520 |
. . . . . . . . . 10
β’ (π β (π΅ + (π΄ β π΅)) = π΄) |
22 | 21 | eqcomd 2739 |
. . . . . . . . 9
β’ (π β π΄ = (π΅ + (π΄ β π΅))) |
23 | 22 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β π΄ = (π΅ + (π΄ β π΅))) |
24 | 3 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β (π΄ β π΅) β β) |
25 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β (π΄ β π΅) β
β*) |
26 | | 0xr 11207 |
. . . . . . . . . . 11
β’ 0 β
β* |
27 | 26 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β 0 β
β*) |
28 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β π β ((π΄ β π΅)(,)0)) |
29 | 25, 27, 28 | ioogtlbd 43874 |
. . . . . . . . 9
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β (π΄ β π΅) < π ) |
30 | 24, 17, 15, 29 | ltadd2dd 11319 |
. . . . . . . 8
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β (π΅ + (π΄ β π΅)) < (π΅ + π )) |
31 | 23, 30 | eqbrtrd 5128 |
. . . . . . 7
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β π΄ < (π΅ + π )) |
32 | | 0red 11163 |
. . . . . . . . 9
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β 0 β
β) |
33 | 25, 27, 28 | iooltubd 43868 |
. . . . . . . . 9
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β π < 0) |
34 | 17, 32, 15, 33 | ltadd2dd 11319 |
. . . . . . . 8
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β (π΅ + π ) < (π΅ + 0)) |
35 | 19 | addid1d 11360 |
. . . . . . . . 9
β’ (π β (π΅ + 0) = π΅) |
36 | 35 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β (π΅ + 0) = π΅) |
37 | 34, 36 | breqtrd 5132 |
. . . . . . 7
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β (π΅ + π ) < π΅) |
38 | 12, 14, 18, 31, 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, 11, 2, 6 | lptioo2cn 43972 |
. . . . . . 7
β’ (π β π΅ β
((limPtβ(TopOpenββfld))β(π΄(,)π΅))) |
46 | | fourierdlem60.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 | | fourierdlem60.n |
. . . 4
β’ π = (π β ((π΄ β π΅)(,)0) β¦ ((πΉβ(π΅ + π )) β π)) |
51 | 49, 50 | fmptd 7063 |
. . 3
β’ (π β π:((π΄ β π΅)(,)0)βΆβ) |
52 | | fourierdlem60.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 | | fourierdlem60.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 | | fourierdlem60.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, 32, 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, 27, 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 | 5 | 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 | 35, 146 | eqeltrrd 2835 |
. . . . . 6
β’ (π β π΅ β ((π β ((π΄ β π΅)(,)0) β¦ (π΅ + π )) limβ 0)) |
148 | 100 | oveq1d 7373 |
. . . . . . 7
β’ (π β (πΉ limβ π΅) = ((π₯ β (π΄(,)π΅) β¦ (πΉβπ₯)) limβ π΅)) |
149 | 46, 148 | eleqtrd 2836 |
. . . . . 6
β’ (π β π β ((π₯ β (π΄(,)π΅) β¦ (πΉβπ₯)) limβ π΅)) |
150 | | simplrr 777 |
. . . . . . 7
β’ (((π β§ (π β ((π΄ β π΅)(,)0) β§ (π΅ + π ) = π΅)) β§ Β¬ (πΉβ(π΅ + π )) = π) β (π΅ + π ) = π΅) |
151 | 18, 37 | ltned 11296 |
. . . . . . . . . 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 | | ubioo 13302 |
. . . . 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 | 5, 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 | 26 | a1i 11 |
. . . . . . . 8
β’ (π β 0 β
β*) |
181 | | ioon0 13296 |
. . . . . . . 8
β’ (((π΄ β π΅) β β* β§ 0 β
β*) β (((π΄ β π΅)(,)0) β β
β (π΄ β π΅) < 0)) |
182 | 4, 180, 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 | | fourierdlem60.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 | 28, 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 | 28, 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 | 4, 5, 8, 51, 53, 126, 134, 163, 164, 172, 186, 211 | lhop2 25395 |
. 2
β’ (π β πΈ β ((π β ((π΄ β π΅)(,)0) β¦ ((πβπ ) / (π·βπ ))) limβ
0)) |
213 | 50 | fvmpt2 6960 |
. . . . . . 7
β’ ((π β ((π΄ β π΅)(,)0) β§ ((πΉβ(π΅ + π )) β π) β β) β (πβπ ) = ((πΉβ(π΅ + π )) β π)) |
214 | 28, 49, 213 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β (πβπ ) = ((πΉβ(π΅ + π )) β π)) |
215 | 52 | fvmpt2 6960 |
. . . . . . 7
β’ ((π β ((π΄ β π΅)(,)0) β§ π β ((π΄ β π΅)(,)0)) β (π·βπ ) = π ) |
216 | 28, 28, 215 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β (π·βπ ) = π ) |
217 | 214, 216 | oveq12d 7376 |
. . . . 5
β’ ((π β§ π β ((π΄ β π΅)(,)0)) β ((πβπ ) / (π·βπ )) = (((πΉβ(π΅ + π )) β π) / π )) |
218 | 217 | mpteq2dva 5206 |
. . . 4
β’ (π β (π β ((π΄ β π΅)(,)0) β¦ ((πβπ ) / (π·βπ ))) = (π β ((π΄ β π΅)(,)0) β¦ (((πΉβ(π΅ + π )) β π) / π ))) |
219 | | fourierdlem60.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)) |