Step | Hyp | Ref
| Expression |
1 | | fourierdlem109.a |
. . . 4
β’ (π β π΄ β β) |
2 | 1 | adantr 482 |
. . 3
β’ ((π β§ 0 < π) β π΄ β β) |
3 | | fourierdlem109.b |
. . . 4
β’ (π β π΅ β β) |
4 | 3 | adantr 482 |
. . 3
β’ ((π β§ 0 < π) β π΅ β β) |
5 | | fourierdlem109.t |
. . 3
β’ π = (π΅ β π΄) |
6 | | fourierdlem109.x |
. . . . 5
β’ (π β π β β) |
7 | 6 | adantr 482 |
. . . 4
β’ ((π β§ 0 < π) β π β β) |
8 | | simpr 486 |
. . . 4
β’ ((π β§ 0 < π) β 0 < π) |
9 | 7, 8 | elrpd 12964 |
. . 3
β’ ((π β§ 0 < π) β π β
β+) |
10 | | fourierdlem109.p |
. . 3
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
11 | | fourierdlem109.m |
. . . 4
β’ (π β π β β) |
12 | 11 | adantr 482 |
. . 3
β’ ((π β§ 0 < π) β π β β) |
13 | | fourierdlem109.q |
. . . 4
β’ (π β π β (πβπ)) |
14 | 13 | adantr 482 |
. . 3
β’ ((π β§ 0 < π) β π β (πβπ)) |
15 | | fourierdlem109.f |
. . . 4
β’ (π β πΉ:ββΆβ) |
16 | 15 | adantr 482 |
. . 3
β’ ((π β§ 0 < π) β πΉ:ββΆβ) |
17 | | fourierdlem109.fper |
. . . 4
β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
18 | 17 | adantlr 714 |
. . 3
β’ (((π β§ 0 < π) β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
19 | | fourierdlem109.fcn |
. . . 4
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
20 | 19 | adantlr 714 |
. . 3
β’ (((π β§ 0 < π) β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
21 | | fourierdlem109.r |
. . . 4
β’ ((π β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
22 | 21 | adantlr 714 |
. . 3
β’ (((π β§ 0 < π) β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
23 | | fourierdlem109.l |
. . . 4
β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
24 | 23 | adantlr 714 |
. . 3
β’ (((π β§ 0 < π) β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
25 | 2, 4, 5, 9, 10, 12, 14, 16, 18, 20, 22, 24 | fourierdlem108 44557 |
. 2
β’ ((π β§ 0 < π) β β«((π΄ β π)[,](π΅ β π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |
26 | | oveq2 7371 |
. . . . . . 7
β’ (π = 0 β (π΄ β π) = (π΄ β 0)) |
27 | 1 | recnd 11193 |
. . . . . . . 8
β’ (π β π΄ β β) |
28 | 27 | subid1d 11511 |
. . . . . . 7
β’ (π β (π΄ β 0) = π΄) |
29 | 26, 28 | sylan9eqr 2794 |
. . . . . 6
β’ ((π β§ π = 0) β (π΄ β π) = π΄) |
30 | | oveq2 7371 |
. . . . . . 7
β’ (π = 0 β (π΅ β π) = (π΅ β 0)) |
31 | 3 | recnd 11193 |
. . . . . . . 8
β’ (π β π΅ β β) |
32 | 31 | subid1d 11511 |
. . . . . . 7
β’ (π β (π΅ β 0) = π΅) |
33 | 30, 32 | sylan9eqr 2794 |
. . . . . 6
β’ ((π β§ π = 0) β (π΅ β π) = π΅) |
34 | 29, 33 | oveq12d 7381 |
. . . . 5
β’ ((π β§ π = 0) β ((π΄ β π)[,](π΅ β π)) = (π΄[,]π΅)) |
35 | 34 | itgeq1d 44300 |
. . . 4
β’ ((π β§ π = 0) β β«((π΄ β π)[,](π΅ β π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |
36 | 35 | adantlr 714 |
. . 3
β’ (((π β§ Β¬ 0 < π) β§ π = 0) β β«((π΄ β π)[,](π΅ β π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |
37 | | simpll 766 |
. . . 4
β’ (((π β§ Β¬ 0 < π) β§ Β¬ π = 0) β π) |
38 | 37, 6 | syl 17 |
. . . . 5
β’ (((π β§ Β¬ 0 < π) β§ Β¬ π = 0) β π β β) |
39 | | 0red 11168 |
. . . . 5
β’ (((π β§ Β¬ 0 < π) β§ Β¬ π = 0) β 0 β
β) |
40 | | simpr 486 |
. . . . . 6
β’ (((π β§ Β¬ 0 < π) β§ Β¬ π = 0) β Β¬ π = 0) |
41 | 40 | neqned 2947 |
. . . . 5
β’ (((π β§ Β¬ 0 < π) β§ Β¬ π = 0) β π β 0) |
42 | | simplr 768 |
. . . . 5
β’ (((π β§ Β¬ 0 < π) β§ Β¬ π = 0) β Β¬ 0 < π) |
43 | 38, 39, 41, 42 | lttri5d 43636 |
. . . 4
β’ (((π β§ Β¬ 0 < π) β§ Β¬ π = 0) β π < 0) |
44 | 6 | recnd 11193 |
. . . . . . . . . . . 12
β’ (π β π β β) |
45 | 27, 44 | subcld 11522 |
. . . . . . . . . . 11
β’ (π β (π΄ β π) β β) |
46 | 45, 44 | subnegd 11529 |
. . . . . . . . . 10
β’ (π β ((π΄ β π) β -π) = ((π΄ β π) + π)) |
47 | 27, 44 | npcand 11526 |
. . . . . . . . . 10
β’ (π β ((π΄ β π) + π) = π΄) |
48 | 46, 47 | eqtrd 2772 |
. . . . . . . . 9
β’ (π β ((π΄ β π) β -π) = π΄) |
49 | 31, 44 | subcld 11522 |
. . . . . . . . . . 11
β’ (π β (π΅ β π) β β) |
50 | 49, 44 | subnegd 11529 |
. . . . . . . . . 10
β’ (π β ((π΅ β π) β -π) = ((π΅ β π) + π)) |
51 | 31, 44 | npcand 11526 |
. . . . . . . . . 10
β’ (π β ((π΅ β π) + π) = π΅) |
52 | 50, 51 | eqtrd 2772 |
. . . . . . . . 9
β’ (π β ((π΅ β π) β -π) = π΅) |
53 | 48, 52 | oveq12d 7381 |
. . . . . . . 8
β’ (π β (((π΄ β π) β -π)[,]((π΅ β π) β -π)) = (π΄[,]π΅)) |
54 | 53 | eqcomd 2738 |
. . . . . . 7
β’ (π β (π΄[,]π΅) = (((π΄ β π) β -π)[,]((π΅ β π) β -π))) |
55 | 54 | itgeq1d 44300 |
. . . . . 6
β’ (π β β«(π΄[,]π΅)(πΉβπ₯) dπ₯ = β«(((π΄ β π) β -π)[,]((π΅ β π) β -π))(πΉβπ₯) dπ₯) |
56 | 55 | adantr 482 |
. . . . 5
β’ ((π β§ π < 0) β β«(π΄[,]π΅)(πΉβπ₯) dπ₯ = β«(((π΄ β π) β -π)[,]((π΅ β π) β -π))(πΉβπ₯) dπ₯) |
57 | 1, 6 | resubcld 11593 |
. . . . . . 7
β’ (π β (π΄ β π) β β) |
58 | 57 | adantr 482 |
. . . . . 6
β’ ((π β§ π < 0) β (π΄ β π) β β) |
59 | 3, 6 | resubcld 11593 |
. . . . . . 7
β’ (π β (π΅ β π) β β) |
60 | 59 | adantr 482 |
. . . . . 6
β’ ((π β§ π < 0) β (π΅ β π) β β) |
61 | | eqid 2732 |
. . . . . 6
β’ ((π΅ β π) β (π΄ β π)) = ((π΅ β π) β (π΄ β π)) |
62 | 6 | renegcld 11592 |
. . . . . . . 8
β’ (π β -π β β) |
63 | 62 | adantr 482 |
. . . . . . 7
β’ ((π β§ π < 0) β -π β β) |
64 | 6 | lt0neg1d 11734 |
. . . . . . . 8
β’ (π β (π < 0 β 0 < -π)) |
65 | 64 | biimpa 478 |
. . . . . . 7
β’ ((π β§ π < 0) β 0 < -π) |
66 | 63, 65 | elrpd 12964 |
. . . . . 6
β’ ((π β§ π < 0) β -π β
β+) |
67 | | fourierdlem109.o |
. . . . . . 7
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (π΄ β π) β§ (πβπ) = (π΅ β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
68 | | fveq2 6848 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ)) |
69 | | oveq1 7370 |
. . . . . . . . . . . . . 14
β’ (π = π β (π + 1) = (π + 1)) |
70 | 69 | fveq2d 6852 |
. . . . . . . . . . . . 13
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
71 | 68, 70 | breq12d 5124 |
. . . . . . . . . . . 12
β’ (π = π β ((πβπ) < (πβ(π + 1)) β (πβπ) < (πβ(π + 1)))) |
72 | 71 | cbvralvw 3224 |
. . . . . . . . . . 11
β’
(βπ β
(0..^π)(πβπ) < (πβ(π + 1)) β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
73 | 72 | anbi2i 624 |
. . . . . . . . . 10
β’ ((((πβ0) = (π΄ β π) β§ (πβπ) = (π΅ β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))) β (((πβ0) = (π΄ β π) β§ (πβπ) = (π΅ β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))) |
74 | 73 | a1i 11 |
. . . . . . . . 9
β’ (π β (β
βm (0...π))
β ((((πβ0) =
(π΄ β π) β§ (πβπ) = (π΅ β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))) β (((πβ0) = (π΄ β π) β§ (πβπ) = (π΅ β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
75 | 74 | rabbiia 3410 |
. . . . . . . 8
β’ {π β (β
βm (0...π))
β£ (((πβ0) =
(π΄ β π) β§ (πβπ) = (π΅ β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))} = {π β (β βm
(0...π)) β£ (((πβ0) = (π΄ β π) β§ (πβπ) = (π΅ β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))} |
76 | 75 | mpteq2i 5216 |
. . . . . . 7
β’ (π β β β¦ {π β (β
βm (0...π))
β£ (((πβ0) =
(π΄ β π) β§ (πβπ) = (π΅ β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (π΄ β π) β§ (πβπ) = (π΅ β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
77 | 67, 76 | eqtri 2760 |
. . . . . 6
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (π΄ β π) β§ (πβπ) = (π΅ β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
78 | 10, 11, 13 | fourierdlem11 44461 |
. . . . . . . . . . . 12
β’ (π β (π΄ β β β§ π΅ β β β§ π΄ < π΅)) |
79 | 78 | simp3d 1145 |
. . . . . . . . . . 11
β’ (π β π΄ < π΅) |
80 | 1, 3, 6, 79 | ltsub1dd 11777 |
. . . . . . . . . 10
β’ (π β (π΄ β π) < (π΅ β π)) |
81 | | fourierdlem109.h |
. . . . . . . . . 10
β’ π» = ({(π΄ β π), (π΅ β π)} βͺ {π₯ β ((π΄ β π)[,](π΅ β π)) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) |
82 | | fourierdlem109.n |
. . . . . . . . . 10
β’ π = ((β―βπ») β 1) |
83 | | fourierdlem109.16 |
. . . . . . . . . 10
β’ π = (β©ππ Isom < , < ((0...π), π»)) |
84 | 5, 10, 11, 13, 57, 59, 80, 67, 81, 82, 83 | fourierdlem54 44503 |
. . . . . . . . 9
β’ (π β ((π β β β§ π β (πβπ)) β§ π Isom < , < ((0...π), π»))) |
85 | 84 | simpld 496 |
. . . . . . . 8
β’ (π β (π β β β§ π β (πβπ))) |
86 | 85 | simpld 496 |
. . . . . . 7
β’ (π β π β β) |
87 | 86 | adantr 482 |
. . . . . 6
β’ ((π β§ π < 0) β π β β) |
88 | 85 | simprd 497 |
. . . . . . 7
β’ (π β π β (πβπ)) |
89 | 88 | adantr 482 |
. . . . . 6
β’ ((π β§ π < 0) β π β (πβπ)) |
90 | 15 | adantr 482 |
. . . . . 6
β’ ((π β§ π < 0) β πΉ:ββΆβ) |
91 | 31, 27, 44 | nnncan2d 11557 |
. . . . . . . . . . . 12
β’ (π β ((π΅ β π) β (π΄ β π)) = (π΅ β π΄)) |
92 | 91, 5 | eqtr4di 2790 |
. . . . . . . . . . 11
β’ (π β ((π΅ β π) β (π΄ β π)) = π) |
93 | 92 | oveq2d 7379 |
. . . . . . . . . 10
β’ (π β (π₯ + ((π΅ β π) β (π΄ β π))) = (π₯ + π)) |
94 | 93 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (π₯ + ((π΅ β π) β (π΄ β π))) = (π₯ + π)) |
95 | 94 | fveq2d 6852 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (πΉβ(π₯ + ((π΅ β π) β (π΄ β π)))) = (πΉβ(π₯ + π))) |
96 | 95, 17 | eqtrd 2772 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (πΉβ(π₯ + ((π΅ β π) β (π΄ β π)))) = (πΉβπ₯)) |
97 | 96 | adantlr 714 |
. . . . . 6
β’ (((π β§ π < 0) β§ π₯ β β) β (πΉβ(π₯ + ((π΅ β π) β (π΄ β π)))) = (πΉβπ₯)) |
98 | 11 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β π β β) |
99 | 13 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β π β (πβπ)) |
100 | 15 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β πΉ:ββΆβ) |
101 | 17 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
102 | 19 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
103 | 57 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (π΄ β π) β β) |
104 | 57 | rexrd 11215 |
. . . . . . . . . 10
β’ (π β (π΄ β π) β
β*) |
105 | | pnfxr 11219 |
. . . . . . . . . . 11
β’ +β
β β* |
106 | 105 | a1i 11 |
. . . . . . . . . 10
β’ (π β +β β
β*) |
107 | 59 | ltpnfd 13052 |
. . . . . . . . . 10
β’ (π β (π΅ β π) < +β) |
108 | 104, 106,
59, 80, 107 | eliood 43838 |
. . . . . . . . 9
β’ (π β (π΅ β π) β ((π΄ β π)(,)+β)) |
109 | 108 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (π΅ β π) β ((π΄ β π)(,)+β)) |
110 | | oveq1 7370 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β (π₯ + (π Β· π)) = (π¦ + (π Β· π))) |
111 | 110 | eleq1d 2818 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β ((π₯ + (π Β· π)) β ran π β (π¦ + (π Β· π)) β ran π)) |
112 | 111 | rexbidv 3172 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (βπ β β€ (π₯ + (π Β· π)) β ran π β βπ β β€ (π¦ + (π Β· π)) β ran π)) |
113 | 112 | cbvrabv 3416 |
. . . . . . . . . 10
β’ {π₯ β ((π΄ β π)[,](π΅ β π)) β£ βπ β β€ (π₯ + (π Β· π)) β ran π} = {π¦ β ((π΄ β π)[,](π΅ β π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π} |
114 | 113 | uneq2i 4126 |
. . . . . . . . 9
β’ ({(π΄ β π), (π΅ β π)} βͺ {π₯ β ((π΄ β π)[,](π΅ β π)) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) = ({(π΄ β π), (π΅ β π)} βͺ {π¦ β ((π΄ β π)[,](π΅ β π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) |
115 | 81, 114 | eqtri 2760 |
. . . . . . . 8
β’ π» = ({(π΄ β π), (π΅ β π)} βͺ {π¦ β ((π΄ β π)[,](π΅ β π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) |
116 | | fourierdlem109.17 |
. . . . . . . 8
β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
117 | | fourierdlem109.18 |
. . . . . . . 8
β’ π½ = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) |
118 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β π β (0..^π)) |
119 | | eqid 2732 |
. . . . . . . 8
β’ ((πβ(π + 1)) β (πΈβ(πβ(π + 1)))) = ((πβ(π + 1)) β (πΈβ(πβ(π + 1)))) |
120 | | eqid 2732 |
. . . . . . . 8
β’ (πΉ βΎ ((π½β(πΈβ(πβπ)))(,)(πΈβ(πβ(π + 1))))) = (πΉ βΎ ((π½β(πΈβ(πβπ)))(,)(πΈβ(πβ(π + 1))))) |
121 | | eqid 2732 |
. . . . . . . 8
β’ (π¦ β (((π½β(πΈβ(πβπ))) + ((πβ(π + 1)) β (πΈβ(πβ(π + 1)))))(,)((πΈβ(πβ(π + 1))) + ((πβ(π + 1)) β (πΈβ(πβ(π + 1)))))) β¦ ((πΉ βΎ ((π½β(πΈβ(πβπ)))(,)(πΈβ(πβ(π + 1)))))β(π¦ β ((πβ(π + 1)) β (πΈβ(πβ(π + 1))))))) = (π¦ β (((π½β(πΈβ(πβπ))) + ((πβ(π + 1)) β (πΈβ(πβ(π + 1)))))(,)((πΈβ(πβ(π + 1))) + ((πβ(π + 1)) β (πΈβ(πβ(π + 1)))))) β¦ ((πΉ βΎ ((π½β(πΈβ(πβπ)))(,)(πΈβ(πβ(π + 1)))))β(π¦ β ((πβ(π + 1)) β (πΈβ(πβ(π + 1))))))) |
122 | | fourierdlem109.19 |
. . . . . . . . 9
β’ πΌ = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ (π½β(πΈβπ₯))}, β, < )) |
123 | | fveq2 6848 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ)) |
124 | 123 | breq1d 5121 |
. . . . . . . . . . . 12
β’ (π = π β ((πβπ) β€ (π½β(πΈβπ₯)) β (πβπ) β€ (π½β(πΈβπ₯)))) |
125 | 124 | cbvrabv 3416 |
. . . . . . . . . . 11
β’ {π β (0..^π) β£ (πβπ) β€ (π½β(πΈβπ₯))} = {π β (0..^π) β£ (πβπ) β€ (π½β(πΈβπ₯))} |
126 | 125 | supeq1i 9393 |
. . . . . . . . . 10
β’
sup({π β
(0..^π) β£ (πβπ) β€ (π½β(πΈβπ₯))}, β, < ) = sup({π β (0..^π) β£ (πβπ) β€ (π½β(πΈβπ₯))}, β, < ) |
127 | 126 | mpteq2i 5216 |
. . . . . . . . 9
β’ (π₯ β β β¦
sup({π β (0..^π) β£ (πβπ) β€ (π½β(πΈβπ₯))}, β, < )) = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ (π½β(πΈβπ₯))}, β, < )) |
128 | 122, 127 | eqtri 2760 |
. . . . . . . 8
β’ πΌ = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ (π½β(πΈβπ₯))}, β, < )) |
129 | 10, 5, 98, 99, 100, 101, 102, 103, 109, 67, 115, 82, 83, 116, 117, 118, 119, 120, 121, 128 | fourierdlem90 44539 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
130 | 129 | adantlr 714 |
. . . . . 6
β’ (((π β§ π < 0) β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
131 | 21 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
132 | | eqid 2732 |
. . . . . . . 8
β’ (π β (0..^π) β¦ π
) = (π β (0..^π) β¦ π
) |
133 | 10, 5, 98, 99, 100, 101, 102, 131, 103, 109, 67, 115, 82, 83, 116, 117, 118, 119, 128, 132 | fourierdlem89 44538 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β if((π½β(πΈβ(πβπ))) = (πβ(πΌβ(πβπ))), ((π β (0..^π) β¦ π
)β(πΌβ(πβπ))), (πΉβ(π½β(πΈβ(πβπ))))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
134 | 133 | adantlr 714 |
. . . . . 6
β’ (((π β§ π < 0) β§ π β (0..^π)) β if((π½β(πΈβ(πβπ))) = (πβ(πΌβ(πβπ))), ((π β (0..^π) β¦ π
)β(πΌβ(πβπ))), (πΉβ(π½β(πΈβ(πβπ))))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
135 | 23 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
136 | | eqid 2732 |
. . . . . . . 8
β’ (π β (0..^π) β¦ πΏ) = (π β (0..^π) β¦ πΏ) |
137 | 10, 5, 98, 99, 100, 101, 102, 135, 103, 109, 67, 115, 82, 83, 116, 117, 118, 119, 128, 136 | fourierdlem91 44540 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β if((πΈβ(πβ(π + 1))) = (πβ((πΌβ(πβπ)) + 1)), ((π β (0..^π) β¦ πΏ)β(πΌβ(πβπ))), (πΉβ(πΈβ(πβ(π + 1))))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
138 | 137 | adantlr 714 |
. . . . . 6
β’ (((π β§ π < 0) β§ π β (0..^π)) β if((πΈβ(πβ(π + 1))) = (πβ((πΌβ(πβπ)) + 1)), ((π β (0..^π) β¦ πΏ)β(πΌβ(πβπ))), (πΉβ(πΈβ(πβ(π + 1))))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
139 | 58, 60, 61, 66, 77, 87, 89, 90, 97, 130, 134, 138 | fourierdlem108 44557 |
. . . . 5
β’ ((π β§ π < 0) β β«(((π΄ β π) β -π)[,]((π΅ β π) β -π))(πΉβπ₯) dπ₯ = β«((π΄ β π)[,](π΅ β π))(πΉβπ₯) dπ₯) |
140 | 56, 139 | eqtr2d 2773 |
. . . 4
β’ ((π β§ π < 0) β β«((π΄ β π)[,](π΅ β π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |
141 | 37, 43, 140 | syl2anc 585 |
. . 3
β’ (((π β§ Β¬ 0 < π) β§ Β¬ π = 0) β β«((π΄ β π)[,](π΅ β π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |
142 | 36, 141 | pm2.61dan 812 |
. 2
β’ ((π β§ Β¬ 0 < π) β β«((π΄ β π)[,](π΅ β π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |
143 | 25, 142 | pm2.61dan 812 |
1
β’ (π β β«((π΄ β π)[,](π΅ β π))(πΉβπ₯) dπ₯ = β«(π΄[,]π΅)(πΉβπ₯) dπ₯) |