Step | Hyp | Ref
| Expression |
1 | | reelprrecn 11202 |
. . . 4
β’ β
β {β, β} |
2 | 1 | a1i 11 |
. . 3
β’ (π β β β {β,
β}) |
3 | | fourierdlem28.x |
. . . . . . 7
β’ (π β π β β) |
4 | | fourierdlem28.a |
. . . . . . 7
β’ (π β π΄ β β) |
5 | 3, 4 | readdcld 11243 |
. . . . . 6
β’ (π β (π + π΄) β β) |
6 | 5 | rexrd 11264 |
. . . . 5
β’ (π β (π + π΄) β
β*) |
7 | 6 | adantr 482 |
. . . 4
β’ ((π β§ π β (π΄(,)π΅)) β (π + π΄) β
β*) |
8 | | fourierdlem28.3b |
. . . . . . 7
β’ (π β π΅ β β) |
9 | 3, 8 | readdcld 11243 |
. . . . . 6
β’ (π β (π + π΅) β β) |
10 | 9 | rexrd 11264 |
. . . . 5
β’ (π β (π + π΅) β
β*) |
11 | 10 | adantr 482 |
. . . 4
β’ ((π β§ π β (π΄(,)π΅)) β (π + π΅) β
β*) |
12 | 3 | adantr 482 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
13 | | elioore 13354 |
. . . . . 6
β’ (π β (π΄(,)π΅) β π β β) |
14 | 13 | adantl 483 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
15 | 12, 14 | readdcld 11243 |
. . . 4
β’ ((π β§ π β (π΄(,)π΅)) β (π + π ) β β) |
16 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β π΄ β β) |
17 | 16 | rexrd 11264 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β π΄ β
β*) |
18 | 8 | rexrd 11264 |
. . . . . . 7
β’ (π β π΅ β
β*) |
19 | 18 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β π΅ β
β*) |
20 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β π β (π΄(,)π΅)) |
21 | | ioogtlb 44208 |
. . . . . 6
β’ ((π΄ β β*
β§ π΅ β
β* β§ π
β (π΄(,)π΅)) β π΄ < π ) |
22 | 17, 19, 20, 21 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β π΄ < π ) |
23 | 16, 14, 12, 22 | ltadd2dd 11373 |
. . . 4
β’ ((π β§ π β (π΄(,)π΅)) β (π + π΄) < (π + π )) |
24 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β π΅ β β) |
25 | | iooltub 44223 |
. . . . . 6
β’ ((π΄ β β*
β§ π΅ β
β* β§ π
β (π΄(,)π΅)) β π < π΅) |
26 | 17, 19, 20, 25 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β π < π΅) |
27 | 14, 24, 12, 26 | ltadd2dd 11373 |
. . . 4
β’ ((π β§ π β (π΄(,)π΅)) β (π + π ) < (π + π΅)) |
28 | 7, 11, 15, 23, 27 | eliood 44211 |
. . 3
β’ ((π β§ π β (π΄(,)π΅)) β (π + π ) β ((π + π΄)(,)(π + π΅))) |
29 | | 1red 11215 |
. . 3
β’ ((π β§ π β (π΄(,)π΅)) β 1 β β) |
30 | | fourierdlem28.1 |
. . . . . 6
β’ (π β πΉ:ββΆβ) |
31 | 30 | adantr 482 |
. . . . 5
β’ ((π β§ π¦ β ((π + π΄)(,)(π + π΅))) β πΉ:ββΆβ) |
32 | | elioore 13354 |
. . . . . 6
β’ (π¦ β ((π + π΄)(,)(π + π΅)) β π¦ β β) |
33 | 32 | adantl 483 |
. . . . 5
β’ ((π β§ π¦ β ((π + π΄)(,)(π + π΅))) β π¦ β β) |
34 | 31, 33 | ffvelcdmd 7088 |
. . . 4
β’ ((π β§ π¦ β ((π + π΄)(,)(π + π΅))) β (πΉβπ¦) β β) |
35 | 34 | recnd 11242 |
. . 3
β’ ((π β§ π¦ β ((π + π΄)(,)(π + π΅))) β (πΉβπ¦) β β) |
36 | | fourierdlem28.df |
. . . 4
β’ (π β π·:((π + π΄)(,)(π + π΅))βΆβ) |
37 | 36 | ffvelcdmda 7087 |
. . 3
β’ ((π β§ π¦ β ((π + π΄)(,)(π + π΅))) β (π·βπ¦) β β) |
38 | 12 | recnd 11242 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
39 | | 0red 11217 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β 0 β β) |
40 | | iooretop 24282 |
. . . . . . . 8
β’ (π΄(,)π΅) β (topGenβran
(,)) |
41 | | eqid 2733 |
. . . . . . . . 9
β’
(TopOpenββfld) =
(TopOpenββfld) |
42 | 41 | tgioo2 24319 |
. . . . . . . 8
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
43 | 40, 42 | eleqtri 2832 |
. . . . . . 7
β’ (π΄(,)π΅) β
((TopOpenββfld) βΎt
β) |
44 | 43 | a1i 11 |
. . . . . 6
β’ (π β (π΄(,)π΅) β
((TopOpenββfld) βΎt
β)) |
45 | 3 | recnd 11242 |
. . . . . 6
β’ (π β π β β) |
46 | 2, 44, 45 | dvmptconst 44631 |
. . . . 5
β’ (π β (β D (π β (π΄(,)π΅) β¦ π)) = (π β (π΄(,)π΅) β¦ 0)) |
47 | 14 | recnd 11242 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
48 | 2, 44 | dvmptidg 44633 |
. . . . 5
β’ (π β (β D (π β (π΄(,)π΅) β¦ π )) = (π β (π΄(,)π΅) β¦ 1)) |
49 | 2, 38, 39, 46, 47, 29, 48 | dvmptadd 25477 |
. . . 4
β’ (π β (β D (π β (π΄(,)π΅) β¦ (π + π ))) = (π β (π΄(,)π΅) β¦ (0 + 1))) |
50 | | 0p1e1 12334 |
. . . . . 6
β’ (0 + 1) =
1 |
51 | 50 | a1i 11 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β (0 + 1) = 1) |
52 | 51 | mpteq2dva 5249 |
. . . 4
β’ (π β (π β (π΄(,)π΅) β¦ (0 + 1)) = (π β (π΄(,)π΅) β¦ 1)) |
53 | 49, 52 | eqtrd 2773 |
. . 3
β’ (π β (β D (π β (π΄(,)π΅) β¦ (π + π ))) = (π β (π΄(,)π΅) β¦ 1)) |
54 | 30 | feqmptd 6961 |
. . . . . . 7
β’ (π β πΉ = (π¦ β β β¦ (πΉβπ¦))) |
55 | 54 | reseq1d 5981 |
. . . . . 6
β’ (π β (πΉ βΎ ((π + π΄)(,)(π + π΅))) = ((π¦ β β β¦ (πΉβπ¦)) βΎ ((π + π΄)(,)(π + π΅)))) |
56 | | ioossre 13385 |
. . . . . . . 8
β’ ((π + π΄)(,)(π + π΅)) β β |
57 | 56 | a1i 11 |
. . . . . . 7
β’ (π β ((π + π΄)(,)(π + π΅)) β β) |
58 | 57 | resmptd 6041 |
. . . . . 6
β’ (π β ((π¦ β β β¦ (πΉβπ¦)) βΎ ((π + π΄)(,)(π + π΅))) = (π¦ β ((π + π΄)(,)(π + π΅)) β¦ (πΉβπ¦))) |
59 | 55, 58 | eqtr2d 2774 |
. . . . 5
β’ (π β (π¦ β ((π + π΄)(,)(π + π΅)) β¦ (πΉβπ¦)) = (πΉ βΎ ((π + π΄)(,)(π + π΅)))) |
60 | 59 | oveq2d 7425 |
. . . 4
β’ (π β (β D (π¦ β ((π + π΄)(,)(π + π΅)) β¦ (πΉβπ¦))) = (β D (πΉ βΎ ((π + π΄)(,)(π + π΅))))) |
61 | | fourierdlem28.d |
. . . . . 6
β’ π· = (β D (πΉ βΎ ((π + π΄)(,)(π + π΅)))) |
62 | 61 | eqcomi 2742 |
. . . . 5
β’ (β
D (πΉ βΎ ((π + π΄)(,)(π + π΅)))) = π· |
63 | 62 | a1i 11 |
. . . 4
β’ (π β (β D (πΉ βΎ ((π + π΄)(,)(π + π΅)))) = π·) |
64 | 36 | feqmptd 6961 |
. . . 4
β’ (π β π· = (π¦ β ((π + π΄)(,)(π + π΅)) β¦ (π·βπ¦))) |
65 | 60, 63, 64 | 3eqtrd 2777 |
. . 3
β’ (π β (β D (π¦ β ((π + π΄)(,)(π + π΅)) β¦ (πΉβπ¦))) = (π¦ β ((π + π΄)(,)(π + π΅)) β¦ (π·βπ¦))) |
66 | | fveq2 6892 |
. . 3
β’ (π¦ = (π + π ) β (πΉβπ¦) = (πΉβ(π + π ))) |
67 | | fveq2 6892 |
. . 3
β’ (π¦ = (π + π ) β (π·βπ¦) = (π·β(π + π ))) |
68 | 2, 2, 28, 29, 35, 37, 53, 65, 66, 67 | dvmptco 25489 |
. 2
β’ (π β (β D (π β (π΄(,)π΅) β¦ (πΉβ(π + π )))) = (π β (π΄(,)π΅) β¦ ((π·β(π + π )) Β· 1))) |
69 | 36 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β π·:((π + π΄)(,)(π + π΅))βΆβ) |
70 | 69, 28 | ffvelcdmd 7088 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β (π·β(π + π )) β β) |
71 | 70 | recnd 11242 |
. . . 4
β’ ((π β§ π β (π΄(,)π΅)) β (π·β(π + π )) β β) |
72 | 71 | mulridd 11231 |
. . 3
β’ ((π β§ π β (π΄(,)π΅)) β ((π·β(π + π )) Β· 1) = (π·β(π + π ))) |
73 | 72 | mpteq2dva 5249 |
. 2
β’ (π β (π β (π΄(,)π΅) β¦ ((π·β(π + π )) Β· 1)) = (π β (π΄(,)π΅) β¦ (π·β(π + π )))) |
74 | 68, 73 | eqtrd 2773 |
1
β’ (π β (β D (π β (π΄(,)π΅) β¦ (πΉβ(π + π )))) = (π β (π΄(,)π΅) β¦ (π·β(π + π )))) |