Step | Hyp | Ref
| Expression |
1 | | fourierdlem112.23 |
. . . . 5
β’ π = (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
2 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π β (π΄βπ) = (π΄βπ)) |
3 | | oveq1 7369 |
. . . . . . . . 9
β’ (π = π β (π Β· π) = (π Β· π)) |
4 | 3 | fveq2d 6851 |
. . . . . . . 8
β’ (π = π β (cosβ(π Β· π)) = (cosβ(π Β· π))) |
5 | 2, 4 | oveq12d 7380 |
. . . . . . 7
β’ (π = π β ((π΄βπ) Β· (cosβ(π Β· π))) = ((π΄βπ) Β· (cosβ(π Β· π)))) |
6 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π β (π΅βπ) = (π΅βπ)) |
7 | 3 | fveq2d 6851 |
. . . . . . . 8
β’ (π = π β (sinβ(π Β· π)) = (sinβ(π Β· π))) |
8 | 6, 7 | oveq12d 7380 |
. . . . . . 7
β’ (π = π β ((π΅βπ) Β· (sinβ(π Β· π))) = ((π΅βπ) Β· (sinβ(π Β· π)))) |
9 | 5, 8 | oveq12d 7380 |
. . . . . 6
β’ (π = π β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
10 | 9 | cbvmptv 5223 |
. . . . 5
β’ (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
11 | 1, 10 | eqtri 2765 |
. . . 4
β’ π = (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
12 | | seqeq3 13918 |
. . . 4
β’ (π = (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β seq1( + , π) = seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))))) |
13 | 11, 12 | mp1i 13 |
. . 3
β’ (π β seq1( + , π) = seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))))) |
14 | | nnuz 12813 |
. . . . 5
β’ β =
(β€β₯β1) |
15 | | 1zzd 12541 |
. . . . 5
β’ (π β 1 β
β€) |
16 | | nfv 1918 |
. . . . . . 7
β’
β²ππ |
17 | | nfcv 2908 |
. . . . . . . 8
β’
β²πβ |
18 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π(-Ο(,)0) |
19 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π(πΉβ(π + π )) |
20 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π
Β· |
21 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π((π·βπ)βπ ) |
22 | 19, 20, 21 | nfov 7392 |
. . . . . . . . 9
β’
β²π((πΉβ(π + π )) Β· ((π·βπ)βπ )) |
23 | 18, 22 | nfitg 25155 |
. . . . . . . 8
β’
β²πβ«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ |
24 | 17, 23 | nfmpt 5217 |
. . . . . . 7
β’
β²π(π β β β¦
β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
25 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π(0(,)Ο) |
26 | 25, 22 | nfitg 25155 |
. . . . . . . 8
β’
β²πβ«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ |
27 | 17, 26 | nfmpt 5217 |
. . . . . . 7
β’
β²π(π β β β¦
β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
28 | | fourierdlem112.z |
. . . . . . . 8
β’ π = (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
29 | | fourierdlem112.a |
. . . . . . . . . . . . 13
β’ π΄ = (π β β0 β¦
(β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) |
30 | | nfmpt1 5218 |
. . . . . . . . . . . . 13
β’
β²π(π β β0 β¦
(β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) |
31 | 29, 30 | nfcxfr 2906 |
. . . . . . . . . . . 12
β’
β²ππ΄ |
32 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π0 |
33 | 31, 32 | nffv 6857 |
. . . . . . . . . . 11
β’
β²π(π΄β0) |
34 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π
/ |
35 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π2 |
36 | 33, 34, 35 | nfov 7392 |
. . . . . . . . . 10
β’
β²π((π΄β0) / 2) |
37 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π
+ |
38 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π(1...π) |
39 | 38 | nfsum1 15581 |
. . . . . . . . . 10
β’
β²πΞ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) |
40 | 36, 37, 39 | nfov 7392 |
. . . . . . . . 9
β’
β²π(((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
41 | 17, 40 | nfmpt 5217 |
. . . . . . . 8
β’
β²π(π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
42 | 28, 41 | nfcxfr 2906 |
. . . . . . 7
β’
β²ππ |
43 | | fourierdlem112.f |
. . . . . . . 8
β’ (π β πΉ:ββΆβ) |
44 | | fourierdlem112.25 |
. . . . . . . 8
β’ (π β π β β) |
45 | | eqid 2737 |
. . . . . . . 8
β’ (π β β β¦ {π β (β
βm (0...π))
β£ (((πβ0) =
(-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
46 | | picn 25832 |
. . . . . . . . . . . . 13
β’ Ο
β β |
47 | 46 | 2timesi 12298 |
. . . . . . . . . . . 12
β’ (2
Β· Ο) = (Ο + Ο) |
48 | | fourierdlem112.t |
. . . . . . . . . . . 12
β’ π = (2 Β·
Ο) |
49 | 46, 46 | subnegi 11487 |
. . . . . . . . . . . 12
β’ (Ο
β -Ο) = (Ο + Ο) |
50 | 47, 48, 49 | 3eqtr4i 2775 |
. . . . . . . . . . 11
β’ π = (Ο β
-Ο) |
51 | | fourierdlem112.p |
. . . . . . . . . . 11
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
52 | | fourierdlem112.m |
. . . . . . . . . . 11
β’ (π β π β β) |
53 | | fourierdlem112.q |
. . . . . . . . . . 11
β’ (π β π β (πβπ)) |
54 | | pire 25831 |
. . . . . . . . . . . . . 14
β’ Ο
β β |
55 | 54 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β Ο β
β) |
56 | 55 | renegcld 11589 |
. . . . . . . . . . . 12
β’ (π β -Ο β
β) |
57 | 56, 44 | readdcld 11191 |
. . . . . . . . . . 11
β’ (π β (-Ο + π) β β) |
58 | 55, 44 | readdcld 11191 |
. . . . . . . . . . 11
β’ (π β (Ο + π) β β) |
59 | | negpilt0 43588 |
. . . . . . . . . . . . . 14
β’ -Ο
< 0 |
60 | | pipos 25833 |
. . . . . . . . . . . . . 14
β’ 0 <
Ο |
61 | 54 | renegcli 11469 |
. . . . . . . . . . . . . . 15
β’ -Ο
β β |
62 | | 0re 11164 |
. . . . . . . . . . . . . . 15
β’ 0 β
β |
63 | 61, 62, 54 | lttri 11288 |
. . . . . . . . . . . . . 14
β’ ((-Ο
< 0 β§ 0 < Ο) β -Ο < Ο) |
64 | 59, 60, 63 | mp2an 691 |
. . . . . . . . . . . . 13
β’ -Ο
< Ο |
65 | 64 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β -Ο <
Ο) |
66 | 56, 55, 44, 65 | ltadd1dd 11773 |
. . . . . . . . . . 11
β’ (π β (-Ο + π) < (Ο + π)) |
67 | | oveq1 7369 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π₯ β (π¦ + (π Β· π)) = (π₯ + (π Β· π))) |
68 | 67 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (π¦ = π₯ β ((π¦ + (π Β· π)) β ran π β (π₯ + (π Β· π)) β ran π)) |
69 | 68 | rexbidv 3176 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β (βπ β β€ (π¦ + (π Β· π)) β ran π β βπ β β€ (π₯ + (π Β· π)) β ran π)) |
70 | 69 | cbvrabv 3420 |
. . . . . . . . . . . 12
β’ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π} = {π₯ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π₯ + (π Β· π)) β ran π} |
71 | 70 | uneq2i 4125 |
. . . . . . . . . . 11
β’ ({(-Ο
+ π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) = ({(-Ο + π), (Ο + π)} βͺ {π₯ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) |
72 | | fourierdlem112.n |
. . . . . . . . . . 11
β’ π = ((β―β({(-Ο +
π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1) |
73 | | fourierdlem112.v |
. . . . . . . . . . 11
β’ π = (β©ππ Isom < , < ((0...π), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}))) |
74 | 50, 51, 52, 53, 57, 58, 66, 45, 71, 72, 73 | fourierdlem54 44475 |
. . . . . . . . . 10
β’ (π β ((π β β β§ π β ((π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))})βπ)) β§ π Isom < , < ((0...π), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})))) |
75 | 74 | simpld 496 |
. . . . . . . . 9
β’ (π β (π β β β§ π β ((π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))})βπ))) |
76 | 75 | simpld 496 |
. . . . . . . 8
β’ (π β π β β) |
77 | 75 | simprd 497 |
. . . . . . . 8
β’ (π β π β ((π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))})βπ)) |
78 | | fourierdlem112.xran |
. . . . . . . 8
β’ (π β π β ran π) |
79 | 43 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β πΉ:ββΆβ) |
80 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πβπ) = (πβπ)) |
81 | | oveq1 7369 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π + 1) = (π + 1)) |
82 | 81 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
83 | 80, 82 | breq12d 5123 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πβπ) < (πβ(π + 1)) β (πβπ) < (πβ(π + 1)))) |
84 | 83 | cbvralvw 3228 |
. . . . . . . . . . . . . 14
β’
(βπ β
(0..^π)(πβπ) < (πβ(π + 1)) β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
85 | 84 | anbi2i 624 |
. . . . . . . . . . . . 13
β’ ((((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))) β (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))) |
86 | 85 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (β
βm (0...π))
β ((((πβ0) =
-Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))) β (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
87 | 86 | rabbiia 3414 |
. . . . . . . . . . 11
β’ {π β (β
βm (0...π))
β£ (((πβ0) =
-Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))} = {π β (β βm
(0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))} |
88 | 87 | mpteq2i 5215 |
. . . . . . . . . 10
β’ (π β β β¦ {π β (β
βm (0...π))
β£ (((πβ0) =
-Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
89 | 51, 88 | eqtri 2765 |
. . . . . . . . 9
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
90 | 52 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β π β β) |
91 | 53 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β π β (πβπ)) |
92 | | fourierdlem112.fper |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
93 | 92 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
94 | | eleq1w 2821 |
. . . . . . . . . . . . 13
β’ (π = π β (π β (0..^π) β π β (0..^π))) |
95 | 94 | anbi2d 630 |
. . . . . . . . . . . 12
β’ (π = π β ((π β§ π β (0..^π)) β (π β§ π β (0..^π)))) |
96 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβπ) = (πβπ)) |
97 | 81 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
98 | 96, 97 | oveq12d 7380 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πβπ)(,)(πβ(π + 1))) = ((πβπ)(,)(πβ(π + 1)))) |
99 | 98 | reseq2d 5942 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = (πΉ βΎ ((πβπ)(,)(πβ(π + 1))))) |
100 | 98 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (π = π β (((πβπ)(,)(πβ(π + 1)))βcnββ) = (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
101 | 99, 100 | eleq12d 2832 |
. . . . . . . . . . . 12
β’ (π = π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ))) |
102 | 95, 101 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = π β (((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) β ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)))) |
103 | | fourierdlem112.fcn |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
104 | 102, 103 | chvarvv 2003 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
105 | 104 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
106 | 57 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (-Ο + π) β β) |
107 | 57 | rexrd 11212 |
. . . . . . . . . . 11
β’ (π β (-Ο + π) β
β*) |
108 | | pnfxr 11216 |
. . . . . . . . . . . 12
β’ +β
β β* |
109 | 108 | a1i 11 |
. . . . . . . . . . 11
β’ (π β +β β
β*) |
110 | 58 | ltpnfd 13049 |
. . . . . . . . . . 11
β’ (π β (Ο + π) < +β) |
111 | 107, 109,
58, 66, 110 | eliood 43810 |
. . . . . . . . . 10
β’ (π β (Ο + π) β ((-Ο + π)(,)+β)) |
112 | 111 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (Ο + π) β ((-Ο + π)(,)+β)) |
113 | | id 22 |
. . . . . . . . . . 11
β’ (π β (0..^π) β π β (0..^π)) |
114 | 72 | oveq2i 7373 |
. . . . . . . . . . 11
β’
(0..^π) =
(0..^((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)) |
115 | 113, 114 | eleqtrdi 2848 |
. . . . . . . . . 10
β’ (π β (0..^π) β π β (0..^((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1))) |
116 | 115 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β π β (0..^((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1))) |
117 | 72 | oveq2i 7373 |
. . . . . . . . . . . 12
β’
(0...π) =
(0...((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)) |
118 | | isoeq4 7270 |
. . . . . . . . . . . 12
β’
((0...π) =
(0...((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)) β (π Isom < , < ((0...π), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β π Isom < , <
((0...((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})))) |
119 | 117, 118 | ax-mp 5 |
. . . . . . . . . . 11
β’ (π Isom < , < ((0...π), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β π Isom < , <
((0...((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}))) |
120 | 119 | iotabii 6486 |
. . . . . . . . . 10
β’
(β©ππ Isom < , < ((0...π), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}))) = (β©ππ Isom < , <
((0...((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}))) |
121 | 73, 120 | eqtri 2765 |
. . . . . . . . 9
β’ π = (β©ππ Isom < , <
((0...((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}))) |
122 | 79, 89, 50, 90, 91, 93, 105, 106, 112, 116, 121 | fourierdlem98 44519 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
123 | | fourierdlem112.fbd |
. . . . . . . . . 10
β’ (π β βπ€ β β βπ‘ β β (absβ(πΉβπ‘)) β€ π€) |
124 | 123 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β βπ€ β β βπ‘ β β (absβ(πΉβπ‘)) β€ π€) |
125 | | nfra1 3270 |
. . . . . . . . . . 11
β’
β²π‘βπ‘ β β (absβ(πΉβπ‘)) β€ π€ |
126 | | elioore 13301 |
. . . . . . . . . . . . 13
β’ (π‘ β ((πβπ)(,)(πβ(π + 1))) β π‘ β β) |
127 | | rspa 3234 |
. . . . . . . . . . . . 13
β’
((βπ‘ β
β (absβ(πΉβπ‘)) β€ π€ β§ π‘ β β) β (absβ(πΉβπ‘)) β€ π€) |
128 | 126, 127 | sylan2 594 |
. . . . . . . . . . . 12
β’
((βπ‘ β
β (absβ(πΉβπ‘)) β€ π€ β§ π‘ β ((πβπ)(,)(πβ(π + 1)))) β (absβ(πΉβπ‘)) β€ π€) |
129 | 128 | ex 414 |
. . . . . . . . . . 11
β’
(βπ‘ β
β (absβ(πΉβπ‘)) β€ π€ β (π‘ β ((πβπ)(,)(πβ(π + 1))) β (absβ(πΉβπ‘)) β€ π€)) |
130 | 125, 129 | ralrimi 3243 |
. . . . . . . . . 10
β’
(βπ‘ β
β (absβ(πΉβπ‘)) β€ π€ β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ‘)) β€ π€) |
131 | 130 | reximi 3088 |
. . . . . . . . 9
β’
(βπ€ β
β βπ‘ β
β (absβ(πΉβπ‘)) β€ π€ β βπ€ β β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ‘)) β€ π€) |
132 | 124, 131 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β βπ€ β β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ(πΉβπ‘)) β€ π€) |
133 | | ssid 3971 |
. . . . . . . . . . . 12
β’ β
β β |
134 | | dvfre 25331 |
. . . . . . . . . . . 12
β’ ((πΉ:ββΆβ β§
β β β) β (β D πΉ):dom (β D πΉ)βΆβ) |
135 | 43, 133, 134 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β (β D πΉ):dom (β D πΉ)βΆβ) |
136 | 135 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (β D πΉ):dom (β D πΉ)βΆβ) |
137 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (β
D πΉ) = (β D πΉ) |
138 | 54 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β Ο β
β) |
139 | 61 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β -Ο β
β) |
140 | 98 | reseq2d 5942 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) = ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))) |
141 | 140, 100 | eleq12d 2832 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ))) |
142 | 95, 141 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π = π β (((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) β ((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)))) |
143 | | fourierdlem112.fdvcn |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
144 | 142, 143 | chvarvv 2003 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
145 | 144 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
146 | | fourierdlem112.x |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
147 | 56, 146 | readdcld 11191 |
. . . . . . . . . . . . . 14
β’ (π β (-Ο + π) β β) |
148 | 147 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (-Ο + π) β β) |
149 | 147 | rexrd 11212 |
. . . . . . . . . . . . . . 15
β’ (π β (-Ο + π) β
β*) |
150 | 55, 146 | readdcld 11191 |
. . . . . . . . . . . . . . 15
β’ (π β (Ο + π) β β) |
151 | 56, 55, 146, 65 | ltadd1dd 11773 |
. . . . . . . . . . . . . . 15
β’ (π β (-Ο + π) < (Ο + π)) |
152 | 150 | ltpnfd 13049 |
. . . . . . . . . . . . . . 15
β’ (π β (Ο + π) < +β) |
153 | 149, 109,
150, 151, 152 | eliood 43810 |
. . . . . . . . . . . . . 14
β’ (π β (Ο + π) β ((-Ο + π)(,)+β)) |
154 | 153 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (Ο + π) β ((-Ο + π)(,)+β)) |
155 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = β β (π Β· π) = (β Β· π)) |
156 | 155 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = β β (π¦ + (π Β· π)) = (π¦ + (β Β· π))) |
157 | 156 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = β β ((π¦ + (π Β· π)) β ran π β (π¦ + (β Β· π)) β ran π)) |
158 | 157 | cbvrexvw 3229 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ β
β€ (π¦ + (π Β· π)) β ran π β ββ β β€ (π¦ + (β Β· π)) β ran π) |
159 | 158 | rgenw 3069 |
. . . . . . . . . . . . . . . . . 18
β’
βπ¦ β
((-Ο + π)[,](Ο +
π))(βπ β β€ (π¦ + (π Β· π)) β ran π β ββ β β€ (π¦ + (β Β· π)) β ran π) |
160 | | rabbi 3435 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ¦ β
((-Ο + π)[,](Ο +
π))(βπ β β€ (π¦ + (π Β· π)) β ran π β ββ β β€ (π¦ + (β Β· π)) β ran π) β {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π} = {π¦ β ((-Ο + π)[,](Ο + π)) β£ ββ β β€ (π¦ + (β Β· π)) β ran π}) |
161 | 159, 160 | mpbi 229 |
. . . . . . . . . . . . . . . . 17
β’ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π} = {π¦ β ((-Ο + π)[,](Ο + π)) β£ ββ β β€ (π¦ + (β Β· π)) β ran π} |
162 | 161 | uneq2i 4125 |
. . . . . . . . . . . . . . . 16
β’ ({(-Ο
+ π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) = ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ ββ β β€ (π¦ + (β Β· π)) β ran π}) |
163 | | isoeq5 7271 |
. . . . . . . . . . . . . . . 16
β’ (({(-Ο
+ π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) = ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ ββ β β€ (π¦ + (β Β· π)) β ran π}) β (π Isom < , <
((0...((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β π Isom < , <
((0...((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ ββ β β€ (π¦ + (β Β· π)) β ran π})))) |
164 | 162, 163 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ (π Isom < , <
((0...((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β π Isom < , <
((0...((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ ββ β β€ (π¦ + (β Β· π)) β ran π}))) |
165 | 164 | iotabii 6486 |
. . . . . . . . . . . . . 14
β’
(β©ππ Isom < , <
((0...((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}))) = (β©ππ Isom < , <
((0...((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ ββ β β€ (π¦ + (β Β· π)) β ran π}))) |
166 | 121, 165 | eqtri 2765 |
. . . . . . . . . . . . 13
β’ π = (β©ππ Isom < , <
((0...((β―β({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1)), ({(-Ο + π), (Ο + π)} βͺ {π¦ β ((-Ο + π)[,](Ο + π)) β£ ββ β β€ (π¦ + (β Β· π)) β ran π}))) |
167 | | eleq1w 2821 |
. . . . . . . . . . . . . . 15
β’ (π£ = π’ β (π£ β dom (β D πΉ) β π’ β dom (β D πΉ))) |
168 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π£ = π’ β ((β D πΉ)βπ£) = ((β D πΉ)βπ’)) |
169 | 167, 168 | ifbieq1d 4515 |
. . . . . . . . . . . . . 14
β’ (π£ = π’ β if(π£ β dom (β D πΉ), ((β D πΉ)βπ£), 0) = if(π’ β dom (β D πΉ), ((β D πΉ)βπ’), 0)) |
170 | 169 | cbvmptv 5223 |
. . . . . . . . . . . . 13
β’ (π£ β β β¦ if(π£ β dom (β D πΉ), ((β D πΉ)βπ£), 0)) = (π’ β β β¦ if(π’ β dom (β D πΉ), ((β D πΉ)βπ’), 0)) |
171 | 79, 137, 89, 138, 139, 50, 90, 91, 93, 145, 148, 154, 116, 166, 170 | fourierdlem97 44518 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
172 | | cncff 24272 |
. . . . . . . . . . . 12
β’
(((β D πΉ)
βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
173 | | fdm 6682 |
. . . . . . . . . . . 12
β’
(((β D πΉ)
βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ β dom ((β D
πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) = ((πβπ)(,)(πβ(π + 1)))) |
174 | 171, 172,
173 | 3syl 18 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β dom ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) = ((πβπ)(,)(πβ(π + 1)))) |
175 | | ssdmres 5965 |
. . . . . . . . . . 11
β’ (((πβπ)(,)(πβ(π + 1))) β dom (β D πΉ) β dom ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) = ((πβπ)(,)(πβ(π + 1)))) |
176 | 174, 175 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β dom (β D πΉ)) |
177 | 136, 176 | fssresd 6714 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
178 | | ax-resscn 11115 |
. . . . . . . . . . 11
β’ β
β β |
179 | 178 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β β β
β) |
180 | | cncfcdm 24277 |
. . . . . . . . . 10
β’ ((β
β β β§ ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) β (((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ)) |
181 | 179, 171,
180 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ)) |
182 | 177, 181 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β ((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
183 | | fourierdlem112.fdvbd |
. . . . . . . . . . 11
β’ (π β βπ§ β β βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§) |
184 | 183 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β βπ§ β β βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§) |
185 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²π‘(π β§ π β (0..^π)) |
186 | | nfra1 3270 |
. . . . . . . . . . . . . 14
β’
β²π‘βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§ |
187 | 185, 186 | nfan 1903 |
. . . . . . . . . . . . 13
β’
β²π‘((π β§ π β (0..^π)) β§ βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§) |
188 | | fvres 6866 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ β ((πβπ)(,)(πβ(π + 1))) β (((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘) = ((β D πΉ)βπ‘)) |
189 | 188 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π‘ β ((πβπ)(,)(πβ(π + 1)))) β (((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘) = ((β D πΉ)βπ‘)) |
190 | 189 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π‘ β ((πβπ)(,)(πβ(π + 1)))) β (absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) = (absβ((β D πΉ)βπ‘))) |
191 | 190 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (0..^π)) β§ βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§) β§ π‘ β ((πβπ)(,)(πβ(π + 1)))) β (absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) = (absβ((β D πΉ)βπ‘))) |
192 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0..^π)) β§ βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§) β§ π‘ β ((πβπ)(,)(πβ(π + 1)))) β βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§) |
193 | 176 | sselda 3949 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π‘ β ((πβπ)(,)(πβ(π + 1)))) β π‘ β dom (β D πΉ)) |
194 | 193 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0..^π)) β§ βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§) β§ π‘ β ((πβπ)(,)(πβ(π + 1)))) β π‘ β dom (β D πΉ)) |
195 | | rspa 3234 |
. . . . . . . . . . . . . . . 16
β’
((βπ‘ β
dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§ β§ π‘ β dom (β D πΉ)) β (absβ((β D πΉ)βπ‘)) β€ π§) |
196 | 192, 194,
195 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (0..^π)) β§ βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§) β§ π‘ β ((πβπ)(,)(πβ(π + 1)))) β (absβ((β D πΉ)βπ‘)) β€ π§) |
197 | 191, 196 | eqbrtrd 5132 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0..^π)) β§ βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§) β§ π‘ β ((πβπ)(,)(πβ(π + 1)))) β (absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§) |
198 | 197 | ex 414 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§) β (π‘ β ((πβπ)(,)(πβ(π + 1))) β (absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§)) |
199 | 187, 198 | ralrimi 3243 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§) β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§) |
200 | 199 | ex 414 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§ β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§)) |
201 | 200 | reximdv 3168 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (βπ§ β β βπ‘ β dom (β D πΉ)(absβ((β D πΉ)βπ‘)) β€ π§ β βπ§ β β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§)) |
202 | 184, 201 | mpd 15 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β βπ§ β β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§) |
203 | | nfra1 3270 |
. . . . . . . . . . . 12
β’
β²π‘βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§ |
204 | 188 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β ((πβπ)(,)(πβ(π + 1))) β ((β D πΉ)βπ‘) = (((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) |
205 | 204 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (π‘ β ((πβπ)(,)(πβ(π + 1))) β (absβ((β D πΉ)βπ‘)) = (absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘))) |
206 | 205 | adantl 483 |
. . . . . . . . . . . . . 14
β’
((βπ‘ β
((πβπ)(,)(πβ(π + 1)))(absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§ β§ π‘ β ((πβπ)(,)(πβ(π + 1)))) β (absβ((β D πΉ)βπ‘)) = (absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘))) |
207 | | rspa 3234 |
. . . . . . . . . . . . . 14
β’
((βπ‘ β
((πβπ)(,)(πβ(π + 1)))(absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§ β§ π‘ β ((πβπ)(,)(πβ(π + 1)))) β (absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§) |
208 | 206, 207 | eqbrtrd 5132 |
. . . . . . . . . . . . 13
β’
((βπ‘ β
((πβπ)(,)(πβ(π + 1)))(absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§ β§ π‘ β ((πβπ)(,)(πβ(π + 1)))) β (absβ((β D πΉ)βπ‘)) β€ π§) |
209 | 208 | ex 414 |
. . . . . . . . . . . 12
β’
(βπ‘ β
((πβπ)(,)(πβ(π + 1)))(absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§ β (π‘ β ((πβπ)(,)(πβ(π + 1))) β (absβ((β D πΉ)βπ‘)) β€ π§)) |
210 | 203, 209 | ralrimi 3243 |
. . . . . . . . . . 11
β’
(βπ‘ β
((πβπ)(,)(πβ(π + 1)))(absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§ β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ((β D πΉ)βπ‘)) β€ π§) |
211 | 210 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§ β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ((β D πΉ)βπ‘)) β€ π§)) |
212 | 211 | reximdv 3168 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (βπ§ β β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ(((β D πΉ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ‘)) β€ π§ β βπ§ β β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ((β D πΉ)βπ‘)) β€ π§)) |
213 | 202, 212 | mpd 15 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β βπ§ β β βπ‘ β ((πβπ)(,)(πβ(π + 1)))(absβ((β D πΉ)βπ‘)) β€ π§) |
214 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π(π β§ π β (0..^π)) |
215 | | nfcsb1v 3885 |
. . . . . . . . . . . . 13
β’
β²πβ¦π / πβ¦πΆ |
216 | 215 | nfel1 2924 |
. . . . . . . . . . . 12
β’
β²πβ¦π / πβ¦πΆ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) |
217 | 214, 216 | nfim 1900 |
. . . . . . . . . . 11
β’
β²π((π β§ π β (0..^π)) β β¦π / πβ¦πΆ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
218 | | csbeq1a 3874 |
. . . . . . . . . . . . 13
β’ (π = π β πΆ = β¦π / πβ¦πΆ) |
219 | 99, 96 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
220 | 218, 219 | eleq12d 2832 |
. . . . . . . . . . . 12
β’ (π = π β (πΆ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) β β¦π / πβ¦πΆ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)))) |
221 | 95, 220 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = π β (((π β§ π β (0..^π)) β πΆ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) β ((π β§ π β (0..^π)) β β¦π / πβ¦πΆ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))))) |
222 | | fourierdlem112.c |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β πΆ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
223 | 217, 221,
222 | chvarfv 2234 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β β¦π / πβ¦πΆ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
224 | 223 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β β¦π / πβ¦πΆ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
225 | 79, 89, 50, 90, 91, 93, 105, 224, 106, 112, 116, 121 | fourierdlem96 44517 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β if(((π β (-Ο(,]Ο) β¦ if(π = Ο, -Ο, π))β((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))β(πβπ))) = (πβ((π¦ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ ((π β (-Ο(,]Ο) β¦ if(π = Ο, -Ο, π))β((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))βπ¦))}, β, < ))β(πβπ))), ((π β (0..^π) β¦ β¦π / πβ¦πΆ)β((π¦ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ ((π β (-Ο(,]Ο) β¦ if(π = Ο, -Ο, π))β((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))βπ¦))}, β, < ))β(πβπ))), (πΉβ((π β (-Ο(,]Ο) β¦ if(π = Ο, -Ο, π))β((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))β(πβπ))))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
226 | | nfcsb1v 3885 |
. . . . . . . . . . . . 13
β’
β²πβ¦π / πβ¦π |
227 | 226 | nfel1 2924 |
. . . . . . . . . . . 12
β’
β²πβ¦π / πβ¦π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) |
228 | 214, 227 | nfim 1900 |
. . . . . . . . . . 11
β’
β²π((π β§ π β (0..^π)) β β¦π / πβ¦π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
229 | | csbeq1a 3874 |
. . . . . . . . . . . . 13
β’ (π = π β π = β¦π / πβ¦π) |
230 | 99, 97 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
231 | 229, 230 | eleq12d 2832 |
. . . . . . . . . . . 12
β’ (π = π β (π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) β β¦π / πβ¦π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))))) |
232 | 95, 231 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = π β (((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) β ((π β§ π β (0..^π)) β β¦π / πβ¦π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))))) |
233 | | fourierdlem112.u |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
234 | 228, 232,
233 | chvarfv 2234 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β β¦π / πβ¦π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
235 | 234 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β β¦π / πβ¦π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
236 | 79, 89, 50, 90, 91, 93, 105, 235, 148, 154, 116, 121 | fourierdlem99 44520 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β if(((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))β(πβ(π + 1))) = (πβ(((π¦ β β β¦ sup({β β (0..^π) β£ (πββ) β€ ((π β (-Ο(,]Ο) β¦ if(π = Ο, -Ο, π))β((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))βπ¦))}, β, < ))β(πβπ)) + 1)), ((π β (0..^π) β¦ β¦π / πβ¦π)β((π¦ β β β¦ sup({β β (0..^π) β£ (πββ) β€ ((π β (-Ο(,]Ο) β¦ if(π = Ο, -Ο, π))β((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))βπ¦))}, β, < ))β(πβπ))), (πΉβ((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))β(πβ(π + 1))))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
237 | | eqeq1 2741 |
. . . . . . . . . 10
β’ (π = π β (π = 0 β π = 0)) |
238 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π = π β (π + π) = (π + π )) |
239 | 238 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π = π β (πΉβ(π + π)) = (πΉβ(π + π ))) |
240 | | breq2 5114 |
. . . . . . . . . . . . 13
β’ (π = π β (0 < π β 0 < π )) |
241 | 240 | ifbid 4514 |
. . . . . . . . . . . 12
β’ (π = π β if(0 < π, π
, πΏ) = if(0 < π , π
, πΏ)) |
242 | 239, 241 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = π β ((πΉβ(π + π)) β if(0 < π, π
, πΏ)) = ((πΉβ(π + π )) β if(0 < π , π
, πΏ))) |
243 | | id 22 |
. . . . . . . . . . 11
β’ (π = π β π = π ) |
244 | 242, 243 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π = π β (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π) = (((πΉβ(π + π )) β if(0 < π , π
, πΏ)) / π )) |
245 | 237, 244 | ifbieq2d 4517 |
. . . . . . . . 9
β’ (π = π β if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)) = if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π
, πΏ)) / π ))) |
246 | 245 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π))) = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π
, πΏ)) / π ))) |
247 | | eqeq1 2741 |
. . . . . . . . . 10
β’ (π = π β (π = 0 β π = 0)) |
248 | | id 22 |
. . . . . . . . . . 11
β’ (π = π β π = π ) |
249 | | oveq1 7369 |
. . . . . . . . . . . . 13
β’ (π = π β (π / 2) = (π / 2)) |
250 | 249 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π = π β (sinβ(π / 2)) = (sinβ(π / 2))) |
251 | 250 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = π β (2 Β· (sinβ(π / 2))) = (2 Β·
(sinβ(π /
2)))) |
252 | 248, 251 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π = π β (π / (2 Β· (sinβ(π / 2)))) = (π / (2 Β· (sinβ(π / 2))))) |
253 | 247, 252 | ifbieq2d 4517 |
. . . . . . . . 9
β’ (π = π β if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))) = if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) |
254 | 253 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β (-Ο[,]Ο) β¦
if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) |
255 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β ((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) = ((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ )) |
256 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ) = ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ )) |
257 | 255, 256 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = π β (((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)) = (((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ ))) |
258 | 257 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ))) = (π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ ))) |
259 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = π β ((π + (1 / 2)) Β· π) = ((π + (1 / 2)) Β· π )) |
260 | 259 | fveq2d 6851 |
. . . . . . . . 9
β’ (π = π β (sinβ((π + (1 / 2)) Β· π)) = (sinβ((π + (1 / 2)) Β· π ))) |
261 | 260 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π))) = (π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π ))) |
262 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π§ = π β ((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) = ((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ )) |
263 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π§ = π β ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§) = ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ )) |
264 | 262, 263 | oveq12d 7380 |
. . . . . . . . 9
β’ (π§ = π β (((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)) = (((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ ))) |
265 | 264 | cbvmptv 5223 |
. . . . . . . 8
β’ (π§ β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ (((π β
(-Ο[,]Ο) β¦ if(π
= 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§))) = (π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ ))) |
266 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = π β (π·βπ) = (π·βπ)) |
267 | 266 | fveq1d 6849 |
. . . . . . . . . . . 12
β’ (π = π β ((π·βπ)βπ ) = ((π·βπ)βπ )) |
268 | 267 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = π β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) = ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
269 | 268 | adantr 482 |
. . . . . . . . . 10
β’ ((π = π β§ π β (-Ο(,)0)) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) = ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
270 | 269 | itgeq2dv 25162 |
. . . . . . . . 9
β’ (π = π β β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ = β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
271 | 270 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β β β¦
β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) = (π β β β¦
β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
272 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π + (1 / 2)) = (π + (1 / 2))) |
273 | 272 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((π + (1 / 2)) Β· π) = ((π + (1 / 2)) Β· π)) |
274 | 273 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (sinβ((π + (1 / 2)) Β· π)) = (sinβ((π + (1 / 2)) Β· π))) |
275 | 274 | mpteq2dv 5212 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π))) = (π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))) |
276 | 275 | fveq1d 6849 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§) = ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)) |
277 | 276 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π = π β (((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)) = (((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§))) |
278 | 277 | mpteq2dv 5212 |
. . . . . . . . . . . . 13
β’ (π = π β (π§ β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§))) = (π§ β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))) |
279 | 278 | fveq1d 6849 |
. . . . . . . . . . . 12
β’ (π = π β ((π§ β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) = ((π§ β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ )) |
280 | 279 | adantr 482 |
. . . . . . . . . . 11
β’ ((π = π β§ π β (-Ο(,)0)) β ((π§ β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ (((π β
(-Ο[,]Ο) β¦ if(π
= 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) = ((π§ β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ )) |
281 | 280 | itgeq2dv 25162 |
. . . . . . . . . 10
β’ (π = π β β«(-Ο(,)0)((π§ β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) dπ = β«(-Ο(,)0)((π§ β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) dπ ) |
282 | 281 | oveq1d 7377 |
. . . . . . . . 9
β’ (π = π β (β«(-Ο(,)0)((π§ β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) dπ / Ο) = (β«(-Ο(,)0)((π§ β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ (((π β
(-Ο[,]Ο) β¦ if(π
= 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) dπ / Ο)) |
283 | 282 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β β β¦
(β«(-Ο(,)0)((π§ β
(-Ο[,]Ο) β¦ (((π
β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) dπ / Ο)) = (π β β β¦
(β«(-Ο(,)0)((π§ β
(-Ο[,]Ο) β¦ (((π
β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) dπ / Ο)) |
284 | | fourierdlem112.r |
. . . . . . . 8
β’ (π β π
β ((πΉ βΎ (π(,)+β)) limβ π)) |
285 | | fourierdlem112.l |
. . . . . . . 8
β’ (π β πΏ β ((πΉ βΎ (-β(,)π)) limβ π)) |
286 | | fourierdlem112.e |
. . . . . . . 8
β’ (π β πΈ β (((β D πΉ) βΎ (-β(,)π)) limβ π)) |
287 | | fourierdlem112.i |
. . . . . . . 8
β’ (π β πΌ β (((β D πΉ) βΎ (π(,)+β)) limβ π)) |
288 | | fourierdlem112.d |
. . . . . . . . 9
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ /
2))))))) |
289 | | oveq1 7369 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β (π¦ mod (2 Β· Ο)) = (π mod (2 Β· Ο))) |
290 | 289 | eqeq1d 2739 |
. . . . . . . . . . . . 13
β’ (π¦ = π β ((π¦ mod (2 Β· Ο)) = 0 β (π mod (2 Β· Ο)) =
0)) |
291 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β ((π + (1 / 2)) Β· π¦) = ((π + (1 / 2)) Β· π )) |
292 | 291 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β (sinβ((π + (1 / 2)) Β· π¦)) = (sinβ((π + (1 / 2)) Β· π ))) |
293 | | oveq1 7369 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β (π¦ / 2) = (π / 2)) |
294 | 293 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β (sinβ(π¦ / 2)) = (sinβ(π / 2))) |
295 | 294 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β ((2 Β· Ο) Β·
(sinβ(π¦ / 2))) = ((2
Β· Ο) Β· (sinβ(π / 2)))) |
296 | 292, 295 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ (π¦ = π β ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ / 2)))) =
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2))))) |
297 | 290, 296 | ifbieq2d 4517 |
. . . . . . . . . . . 12
β’ (π¦ = π β if((π¦ mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· π¦)) / ((2
Β· Ο) Β· (sinβ(π¦ / 2))))) = if((π mod (2 Β· Ο)) = 0, (((2 Β·
π) + 1) / (2 Β·
Ο)), ((sinβ((π +
(1 / 2)) Β· π )) / ((2
Β· Ο) Β· (sinβ(π / 2)))))) |
298 | 297 | cbvmptv 5223 |
. . . . . . . . . . 11
β’ (π¦ β β β¦
if((π¦ mod (2 Β·
Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π¦)) / ((2 Β·
Ο) Β· (sinβ(π¦ / 2)))))) = (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2)))))) |
299 | | simpl 484 |
. . . . . . . . . . . . . . . 16
β’ ((π = π β§ π β β) β π = π) |
300 | 299 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ ((π = π β§ π β β) β (2 Β· π) = (2 Β· π)) |
301 | 300 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π β β) β ((2 Β· π) + 1) = ((2 Β· π) + 1)) |
302 | 301 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π β β) β (((2 Β· π) + 1) / (2 Β· Ο)) =
(((2 Β· π) + 1) / (2
Β· Ο))) |
303 | 299 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ ((π = π β§ π β β) β (π + (1 / 2)) = (π + (1 / 2))) |
304 | 303 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ ((π = π β§ π β β) β ((π + (1 / 2)) Β· π ) = ((π + (1 / 2)) Β· π )) |
305 | 304 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π β β) β (sinβ((π + (1 / 2)) Β· π )) = (sinβ((π + (1 / 2)) Β· π ))) |
306 | 305 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π β β) β ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π / 2)))) =
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2))))) |
307 | 302, 306 | ifeq12d 4512 |
. . . . . . . . . . . 12
β’ ((π = π β§ π β β) β if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π / 2))))) =
if((π mod (2 Β·
Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2)))))) |
308 | 307 | mpteq2dva 5210 |
. . . . . . . . . . 11
β’ (π = π β (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π / 2)))))) =
(π β β β¦
if((π mod (2 Β·
Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2))))))) |
309 | 298, 308 | eqtrid 2789 |
. . . . . . . . . 10
β’ (π = π β (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ / 2)))))) =
(π β β β¦
if((π mod (2 Β·
Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π )) / ((2 Β·
Ο) Β· (sinβ(π / 2))))))) |
310 | 309 | cbvmptv 5223 |
. . . . . . . . 9
β’ (π β β β¦ (π¦ β β β¦
if((π¦ mod (2 Β·
Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π¦)) / ((2 Β·
Ο) Β· (sinβ(π¦ / 2))))))) = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))))) |
311 | 288, 310 | eqtri 2765 |
. . . . . . . 8
β’ π· = (π β β β¦ (π β β β¦ if((π mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π )) / ((2 Β· Ο) Β·
(sinβ(π /
2))))))) |
312 | | eqid 2737 |
. . . . . . . 8
β’ ((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ))) βΎ (-Ο[,]π)) = ((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ))) βΎ (-Ο[,]π)) |
313 | | eqid 2737 |
. . . . . . . 8
β’ ({-Ο,
π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π))) = ({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π))) |
314 | | eqid 2737 |
. . . . . . . 8
β’
((β―β({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))) β 1) = ((β―β({-Ο,
π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))) β 1) |
315 | | isoeq1 7267 |
. . . . . . . . 9
β’ (π’ = π€ β (π’ Isom < , <
((0...((β―β({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))) β 1)), ({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))) β π€ Isom < , <
((0...((β―β({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))) β 1)), ({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))))) |
316 | 315 | cbviotavw 6461 |
. . . . . . . 8
β’
(β©π’π’ Isom < , <
((0...((β―β({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))) β 1)), ({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π))))) = (β©π€π€ Isom < , <
((0...((β―β({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))) β 1)), ({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π))))) |
317 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = π β (πβπ) = (πβπ)) |
318 | 317 | oveq1d 7377 |
. . . . . . . . 9
β’ (π = π β ((πβπ) β π) = ((πβπ) β π)) |
319 | 318 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β (0...π) β¦ ((πβπ) β π)) = (π β (0...π) β¦ ((πβπ) β π)) |
320 | | eqid 2737 |
. . . . . . . 8
β’
(β©π
β (0..^π)(((β©π’π’ Isom < , <
((0...((β―β({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))) β 1)), ({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))))βπ)(,)((β©π’π’ Isom < , <
((0...((β―β({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))) β 1)), ({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))))β(π + 1))) β (((π β (0...π) β¦ ((πβπ) β π))βπ)(,)((π β (0...π) β¦ ((πβπ) β π))β(π + 1)))) = (β©π β (0..^π)(((β©π’π’ Isom < , <
((0...((β―β({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))) β 1)), ({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))))βπ)(,)((β©π’π’ Isom < , <
((0...((β―β({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))) β 1)), ({-Ο, π} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (-Ο(,)π)))))β(π + 1))) β (((π β (0...π) β¦ ((πβπ) β π))βπ)(,)((π β (0...π) β¦ ((πβπ) β π))β(π + 1)))) |
321 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) = ((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ )) |
322 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π + (1 / 2)) Β· π) = ((π + (1 / 2)) Β· π )) |
323 | 322 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π = π β (sinβ((π + (1 / 2)) Β· π)) = (sinβ((π + (1 / 2)) Β· π ))) |
324 | 321, 323 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ (π = π β (((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) = (((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π )))) |
325 | 324 | cbvitgv 25157 |
. . . . . . . . . . . 12
β’
β«(π(,)0)(((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ = β«(π(,)0)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ |
326 | 325 | fveq2i 6850 |
. . . . . . . . . . 11
β’
(absββ«(π(,)0)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ) = (absββ«(π(,)0)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) |
327 | 326 | breq1i 5117 |
. . . . . . . . . 10
β’
((absββ«(π(,)0)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ) < (π / 2) β (absββ«(π(,)0)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2)) |
328 | 327 | anbi2i 624 |
. . . . . . . . 9
β’
(((((π β§ π β β+)
β§ π β (-Ο(,)0))
β§ π β β)
β§ (absββ«(π(,)0)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ) < (π / 2)) β ((((π β§ π β β+) β§ π β (-Ο(,)0)) β§ π β β) β§
(absββ«(π(,)0)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2))) |
329 | 324 | cbvitgv 25157 |
. . . . . . . . . . 11
β’
β«(-Ο(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ = β«(-Ο(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ |
330 | 329 | fveq2i 6850 |
. . . . . . . . . 10
β’
(absββ«(-Ο(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ) = (absββ«(-Ο(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) |
331 | 330 | breq1i 5117 |
. . . . . . . . 9
β’
((absββ«(-Ο(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ) < (π / 2) β (absββ«(-Ο(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2)) |
332 | 328, 331 | anbi12i 628 |
. . . . . . . 8
β’
((((((π β§ π β β+)
β§ π β (-Ο(,)0))
β§ π β β)
β§ (absββ«(π(,)0)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ) < (π / 2)) β§ (absββ«(-Ο(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ) < (π / 2)) β (((((π β§ π β β+) β§ π β (-Ο(,)0)) β§ π β β) β§
(absββ«(π(,)0)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2)) β§ (absββ«(-Ο(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2))) |
333 | 43, 44, 45, 76, 77, 78, 122, 132, 182, 213, 225, 236, 246, 254, 258, 261, 265, 271, 283, 284, 285, 286, 287, 311, 312, 313, 314, 316, 319, 320, 332 | fourierdlem103 44524 |
. . . . . . 7
β’ (π β (π β β β¦
β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) β (πΏ / 2)) |
334 | | nnex 12166 |
. . . . . . . . . 10
β’ β
β V |
335 | 334 | mptex 7178 |
. . . . . . . . 9
β’ (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) β V |
336 | 28, 335 | eqeltri 2834 |
. . . . . . . 8
β’ π β V |
337 | 336 | a1i 11 |
. . . . . . 7
β’ (π β π β V) |
338 | 268 | adantr 482 |
. . . . . . . . . 10
β’ ((π = π β§ π β (0(,)Ο)) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) = ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
339 | 338 | itgeq2dv 25162 |
. . . . . . . . 9
β’ (π = π β β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ = β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
340 | 339 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β β β¦
β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) = (π β β β¦
β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
341 | 279 | adantr 482 |
. . . . . . . . . . 11
β’ ((π = π β§ π β (0(,)Ο)) β ((π§ β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ (((π β
(-Ο[,]Ο) β¦ if(π
= 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) = ((π§ β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ )) |
342 | 341 | itgeq2dv 25162 |
. . . . . . . . . 10
β’ (π = π β β«(0(,)Ο)((π§ β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) dπ = β«(0(,)Ο)((π§ β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) dπ ) |
343 | 342 | oveq1d 7377 |
. . . . . . . . 9
β’ (π = π β (β«(0(,)Ο)((π§ β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) dπ / Ο) = (β«(0(,)Ο)((π§ β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ (((π β
(-Ο[,]Ο) β¦ if(π
= 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) dπ / Ο)) |
344 | 343 | cbvmptv 5223 |
. . . . . . . 8
β’ (π β β β¦
(β«(0(,)Ο)((π§ β
(-Ο[,]Ο) β¦ (((π
β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) dπ / Ο)) = (π β β β¦
(β«(0(,)Ο)((π§ β
(-Ο[,]Ο) β¦ (((π
β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ§) Β· ((π β (-Ο[,]Ο) β¦
(sinβ((π + (1 / 2))
Β· π)))βπ§)))βπ ) dπ / Ο)) |
345 | | eqid 2737 |
. . . . . . . 8
β’ ((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ))) βΎ (π[,]Ο)) = ((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ))) βΎ (π[,]Ο)) |
346 | | eqid 2737 |
. . . . . . . 8
β’ ({π, Ο} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (π(,)Ο))) = ({π, Ο} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (π(,)Ο))) |
347 | | eqid 2737 |
. . . . . . . 8
β’
((β―β({π,
Ο} βͺ (ran (π β
(0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))) β 1) =
((β―β({π, Ο}
βͺ (ran (π β
(0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))) β 1) |
348 | | isoeq1 7267 |
. . . . . . . . 9
β’ (π’ = π£ β (π’ Isom < , <
((0...((β―β({π,
Ο} βͺ (ran (π β
(0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))) β 1)), ({π, Ο} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))) β π£ Isom < , <
((0...((β―β({π,
Ο} βͺ (ran (π β
(0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))) β 1)), ({π, Ο} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))))) |
349 | 348 | cbviotavw 6461 |
. . . . . . . 8
β’
(β©π’π’ Isom < , <
((0...((β―β({π,
Ο} βͺ (ran (π β
(0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))) β 1)), ({π, Ο} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (π(,)Ο))))) = (β©π£π£ Isom < , <
((0...((β―β({π,
Ο} βͺ (ran (π β
(0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))) β 1)), ({π, Ο} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (π(,)Ο))))) |
350 | | eqid 2737 |
. . . . . . . 8
β’
(β©π
β (0..^π)(((β©π’π’ Isom < , <
((0...((β―β({π,
Ο} βͺ (ran (π β
(0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))) β 1)), ({π, Ο} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))))βπ)(,)((β©π’π’ Isom < , <
((0...((β―β({π,
Ο} βͺ (ran (π β
(0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))) β 1)), ({π, Ο} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))))β(π + 1))) β (((π β (0...π) β¦ ((πβπ) β π))βπ)(,)((π β (0...π) β¦ ((πβπ) β π))β(π + 1)))) = (β©π β (0..^π)(((β©π’π’ Isom < , <
((0...((β―β({π,
Ο} βͺ (ran (π β
(0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))) β 1)), ({π, Ο} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))))βπ)(,)((β©π’π’ Isom < , <
((0...((β―β({π,
Ο} βͺ (ran (π β
(0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))) β 1)), ({π, Ο} βͺ (ran (π β (0...π) β¦ ((πβπ) β π)) β© (π(,)Ο)))))β(π + 1))) β (((π β (0...π) β¦ ((πβπ) β π))βπ)(,)((π β (0...π) β¦ ((πβπ) β π))β(π + 1)))) |
351 | 324 | cbvitgv 25157 |
. . . . . . . . . . . 12
β’
β«(0(,)π)(((π β (-Ο[,]Ο) β¦
(((π β (-Ο[,]Ο)
β¦ if(π = 0, 0,
(((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ = β«(0(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ |
352 | 351 | fveq2i 6850 |
. . . . . . . . . . 11
β’
(absββ«(0(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ) = (absββ«(0(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) |
353 | 352 | breq1i 5117 |
. . . . . . . . . 10
β’
((absββ«(0(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ) < (π / 2) β (absββ«(0(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2)) |
354 | 353 | anbi2i 624 |
. . . . . . . . 9
β’
(((((π β§ π β β+)
β§ π β (0(,)Ο))
β§ π β β)
β§ (absββ«(0(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ) < (π / 2)) β ((((π β§ π β β+) β§ π β (0(,)Ο)) β§ π β β) β§
(absββ«(0(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2))) |
355 | 324 | cbvitgv 25157 |
. . . . . . . . . . 11
β’
β«(π(,)Ο)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ = β«(π(,)Ο)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ |
356 | 355 | fveq2i 6850 |
. . . . . . . . . 10
β’
(absββ«(π(,)Ο)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ) = (absββ«(π(,)Ο)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) |
357 | 356 | breq1i 5117 |
. . . . . . . . 9
β’
((absββ«(π(,)Ο)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ) < (π / 2) β (absββ«(π(,)Ο)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2)) |
358 | 354, 357 | anbi12i 628 |
. . . . . . . 8
β’
((((((π β§ π β β+)
β§ π β (0(,)Ο))
β§ π β β)
β§ (absββ«(0(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ) < (π / 2)) β§ (absββ«(π(,)Ο)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ) Β· (sinβ((π + (1 / 2)) Β· π))) dπ) < (π / 2)) β (((((π β§ π β β+) β§ π β (0(,)Ο)) β§ π β β) β§
(absββ«(0(,)π)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2)) β§ (absββ«(π(,)Ο)(((π β (-Ο[,]Ο) β¦ (((π β (-Ο[,]Ο) β¦
if(π = 0, 0, (((πΉβ(π + π)) β if(0 < π, π
, πΏ)) / π)))βπ) Β· ((π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))))βπ)))βπ ) Β· (sinβ((π + (1 / 2)) Β· π ))) dπ ) < (π / 2))) |
359 | 43, 44, 45, 76, 77, 78, 122, 132, 182, 213, 225, 236, 246, 254, 258, 261, 265, 340, 344, 284, 285, 286, 287, 311, 345, 346, 347, 349, 319, 350, 358 | fourierdlem104 44525 |
. . . . . . 7
β’ (π β (π β β β¦
β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) β (π
/ 2)) |
360 | | eqidd 2738 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π β β β¦
β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) = (π β β β¦
β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )) |
361 | 270 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π = π) β β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ = β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
362 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β) |
363 | | elioore 13301 |
. . . . . . . . . . 11
β’ (π β (-Ο(,)0) β π β
β) |
364 | 43 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β πΉ:ββΆβ) |
365 | 44 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π β β) |
366 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π β β) |
367 | 365, 366 | readdcld 11191 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π + π ) β β) |
368 | 364, 367 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΉβ(π + π )) β β) |
369 | 368 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β β) β (πΉβ(π + π )) β β) |
370 | 288 | dirkerre 44410 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β) β ((π·βπ)βπ ) β β) |
371 | 370 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β β) β ((π·βπ)βπ ) β β) |
372 | 369, 371 | remulcld 11192 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β β) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) β β) |
373 | 363, 372 | sylan2 594 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (-Ο(,)0)) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) β β) |
374 | | ioossicc 13357 |
. . . . . . . . . . . . 13
β’
(-Ο(,)0) β (-Ο[,]0) |
375 | 61 | leidi 11696 |
. . . . . . . . . . . . . 14
β’ -Ο
β€ -Ο |
376 | 62, 54, 60 | ltleii 11285 |
. . . . . . . . . . . . . 14
β’ 0 β€
Ο |
377 | | iccss 13339 |
. . . . . . . . . . . . . 14
β’ (((-Ο
β β β§ Ο β β) β§ (-Ο β€ -Ο β§ 0 β€
Ο)) β (-Ο[,]0) β (-Ο[,]Ο)) |
378 | 61, 54, 375, 376, 377 | mp4an 692 |
. . . . . . . . . . . . 13
β’
(-Ο[,]0) β (-Ο[,]Ο) |
379 | 374, 378 | sstri 3958 |
. . . . . . . . . . . 12
β’
(-Ο(,)0) β (-Ο[,]Ο) |
380 | 379 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (-Ο(,)0) β
(-Ο[,]Ο)) |
381 | | ioombl 24945 |
. . . . . . . . . . . 12
β’
(-Ο(,)0) β dom vol |
382 | 381 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (-Ο(,)0) β
dom vol) |
383 | 43 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (-Ο[,]Ο)) β πΉ:ββΆβ) |
384 | 44 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (-Ο[,]Ο)) β π β
β) |
385 | 56, 55 | iccssred 13358 |
. . . . . . . . . . . . . . . 16
β’ (π β (-Ο[,]Ο) β
β) |
386 | 385 | sselda 3949 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (-Ο[,]Ο)) β π β
β) |
387 | 384, 386 | readdcld 11191 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (-Ο[,]Ο)) β (π + π ) β β) |
388 | 383, 387 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (-Ο[,]Ο)) β (πΉβ(π + π )) β β) |
389 | 388 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (-Ο[,]Ο)) β (πΉβ(π + π )) β β) |
390 | | iccssre 13353 |
. . . . . . . . . . . . . . . 16
β’ ((-Ο
β β β§ Ο β β) β (-Ο[,]Ο) β
β) |
391 | 61, 54, 390 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’
(-Ο[,]Ο) β β |
392 | 391 | sseli 3945 |
. . . . . . . . . . . . . 14
β’ (π β (-Ο[,]Ο) β
π β
β) |
393 | 392, 370 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β (-Ο[,]Ο)) β
((π·βπ)βπ ) β β) |
394 | 393 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (-Ο[,]Ο)) β ((π·βπ)βπ ) β β) |
395 | 389, 394 | remulcld 11192 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (-Ο[,]Ο)) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) β β) |
396 | 61 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β -Ο β
β) |
397 | 54 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β Ο β
β) |
398 | 43 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β πΉ:ββΆβ) |
399 | 44 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
400 | 76 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
401 | 77 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β ((π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))})βπ)) |
402 | 122 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
403 | 225 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (0..^π)) β if(((π β (-Ο(,]Ο) β¦ if(π = Ο, -Ο, π))β((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))β(πβπ))) = (πβ((π¦ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ ((π β (-Ο(,]Ο) β¦ if(π = Ο, -Ο, π))β((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))βπ¦))}, β, < ))β(πβπ))), ((π β (0..^π) β¦ β¦π / πβ¦πΆ)β((π¦ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ ((π β (-Ο(,]Ο) β¦ if(π = Ο, -Ο, π))β((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))βπ¦))}, β, < ))β(πβπ))), (πΉβ((π β (-Ο(,]Ο) β¦ if(π = Ο, -Ο, π))β((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))β(πβπ))))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
404 | 236 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (0..^π)) β if(((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))β(πβ(π + 1))) = (πβ(((π¦ β β β¦ sup({β β (0..^π) β£ (πββ) β€ ((π β (-Ο(,]Ο) β¦ if(π = Ο, -Ο, π))β((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))βπ¦))}, β, < ))β(πβπ)) + 1)), ((π β (0..^π) β¦ β¦π / πβ¦π)β((π¦ β β β¦ sup({β β (0..^π) β£ (πββ) β€ ((π β (-Ο(,]Ο) β¦ if(π = Ο, -Ο, π))β((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))βπ¦))}, β, < ))β(πβπ))), (πΉβ((π β β β¦ (π + ((ββ((Ο β π) / π)) Β· π)))β(πβ(π + 1))))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
405 | 288 | dirkercncf 44422 |
. . . . . . . . . . . . 13
β’ (π β β β (π·βπ) β (ββcnββ)) |
406 | 405 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π·βπ) β (ββcnββ)) |
407 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π β (-Ο[,]Ο) β¦
((πΉβ(π + π )) Β· ((π·βπ)βπ ))) = (π β (-Ο[,]Ο) β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
408 | 396, 397,
398, 399, 45, 400, 401, 402, 403, 404, 319, 51, 406, 407 | fourierdlem84 44505 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π β (-Ο[,]Ο) β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) β
πΏ1) |
409 | 380, 382,
395, 408 | iblss 25185 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π β (-Ο(,)0) β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) β
πΏ1) |
410 | 373, 409 | itgcl 25164 |
. . . . . . . . 9
β’ ((π β§ π β β) β
β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ β β) |
411 | 360, 361,
362, 410 | fvmptd 6960 |
. . . . . . . 8
β’ ((π β§ π β β) β ((π β β β¦
β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )βπ) = β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
412 | 411, 410 | eqeltrd 2838 |
. . . . . . 7
β’ ((π β§ π β β) β ((π β β β¦
β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )βπ) β β) |
413 | | eqidd 2738 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π β β β¦
β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) = (π β β β¦
β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )) |
414 | 339 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π = π) β β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ = β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
415 | 43 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0(,)Ο)) β πΉ:ββΆβ) |
416 | 44 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0(,)Ο)) β π β β) |
417 | | elioore 13301 |
. . . . . . . . . . . . . . 15
β’ (π β (0(,)Ο) β π β
β) |
418 | 417 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0(,)Ο)) β π β β) |
419 | 416, 418 | readdcld 11191 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0(,)Ο)) β (π + π ) β β) |
420 | 415, 419 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0(,)Ο)) β (πΉβ(π + π )) β β) |
421 | 420 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (0(,)Ο)) β (πΉβ(π + π )) β β) |
422 | 417, 370 | sylan2 594 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β (0(,)Ο)) β
((π·βπ)βπ ) β β) |
423 | 422 | adantll 713 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (0(,)Ο)) β ((π·βπ)βπ ) β β) |
424 | 421, 423 | remulcld 11192 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (0(,)Ο)) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) β β) |
425 | | ioossicc 13357 |
. . . . . . . . . . . . 13
β’
(0(,)Ο) β (0[,]Ο) |
426 | 61, 62, 59 | ltleii 11285 |
. . . . . . . . . . . . . 14
β’ -Ο
β€ 0 |
427 | 54 | leidi 11696 |
. . . . . . . . . . . . . 14
β’ Ο β€
Ο |
428 | | iccss 13339 |
. . . . . . . . . . . . . 14
β’ (((-Ο
β β β§ Ο β β) β§ (-Ο β€ 0 β§ Ο β€
Ο)) β (0[,]Ο) β (-Ο[,]Ο)) |
429 | 61, 54, 426, 427, 428 | mp4an 692 |
. . . . . . . . . . . . 13
β’
(0[,]Ο) β (-Ο[,]Ο) |
430 | 425, 429 | sstri 3958 |
. . . . . . . . . . . 12
β’
(0(,)Ο) β (-Ο[,]Ο) |
431 | 430 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (0(,)Ο) β
(-Ο[,]Ο)) |
432 | | ioombl 24945 |
. . . . . . . . . . . 12
β’
(0(,)Ο) β dom vol |
433 | 432 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (0(,)Ο) β dom
vol) |
434 | 431, 433,
395, 408 | iblss 25185 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π β (0(,)Ο) β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) β
πΏ1) |
435 | 424, 434 | itgcl 25164 |
. . . . . . . . 9
β’ ((π β§ π β β) β
β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ β β) |
436 | 413, 414,
362, 435 | fvmptd 6960 |
. . . . . . . 8
β’ ((π β§ π β β) β ((π β β β¦
β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )βπ) = β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
437 | 436, 435 | eqeltrd 2838 |
. . . . . . 7
β’ ((π β§ π β β) β ((π β β β¦
β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )βπ) β β) |
438 | | eleq1w 2821 |
. . . . . . . . . . 11
β’ (π = π β (π β β β π β β)) |
439 | 438 | anbi2d 630 |
. . . . . . . . . 10
β’ (π = π β ((π β§ π β β) β (π β§ π β β))) |
440 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = π β (πβπ) = (πβπ)) |
441 | 270, 339 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = π β (β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ + β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) = (β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ + β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )) |
442 | 440, 441 | eqeq12d 2753 |
. . . . . . . . . 10
β’ (π = π β ((πβπ) = (β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ + β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) β (πβπ) = (β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ + β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ))) |
443 | 439, 442 | imbi12d 345 |
. . . . . . . . 9
β’ (π = π β (((π β§ π β β) β (πβπ) = (β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ + β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )) β ((π β§ π β β) β (πβπ) = (β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ + β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )))) |
444 | | oveq1 7369 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π Β· π₯) = (π Β· π₯)) |
445 | 444 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (cosβ(π Β· π₯)) = (cosβ(π Β· π₯))) |
446 | 445 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πΉβπ₯) Β· (cosβ(π Β· π₯))) = ((πΉβπ₯) Β· (cosβ(π Β· π₯)))) |
447 | 446 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π₯ β (-Ο(,)Ο)) β ((πΉβπ₯) Β· (cosβ(π Β· π₯))) = ((πΉβπ₯) Β· (cosβ(π Β· π₯)))) |
448 | 447 | itgeq2dv 25162 |
. . . . . . . . . . . . 13
β’ (π = π β β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ = β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯) |
449 | 448 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (π = π β (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο) = (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) |
450 | 449 | cbvmptv 5223 |
. . . . . . . . . . 11
β’ (π β β0
β¦ (β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) = (π β β0 β¦
(β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) |
451 | 29, 450 | eqtri 2765 |
. . . . . . . . . 10
β’ π΄ = (π β β0 β¦
(β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ / Ο)) |
452 | | fourierdlem112.b |
. . . . . . . . . . 11
β’ π΅ = (π β β β¦
(β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) |
453 | 444 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (sinβ(π Β· π₯)) = (sinβ(π Β· π₯))) |
454 | 453 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πΉβπ₯) Β· (sinβ(π Β· π₯))) = ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) |
455 | 454 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π₯ β (-Ο(,)Ο)) β ((πΉβπ₯) Β· (sinβ(π Β· π₯))) = ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) |
456 | 455 | itgeq2dv 25162 |
. . . . . . . . . . . . 13
β’ (π = π β β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ = β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯) |
457 | 456 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (π = π β (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο) = (β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) |
458 | 457 | cbvmptv 5223 |
. . . . . . . . . . 11
β’ (π β β β¦
(β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) = (π β β β¦
(β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) |
459 | 452, 458 | eqtri 2765 |
. . . . . . . . . 10
β’ π΅ = (π β β β¦
(β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ / Ο)) |
460 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π΄βπ) = (π΄βπ)) |
461 | | oveq1 7369 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π Β· π) = (π Β· π)) |
462 | 461 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (cosβ(π Β· π)) = (cosβ(π Β· π))) |
463 | 460, 462 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π΄βπ) Β· (cosβ(π Β· π))) = ((π΄βπ) Β· (cosβ(π Β· π)))) |
464 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π΅βπ) = (π΅βπ)) |
465 | 461 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (sinβ(π Β· π)) = (sinβ(π Β· π))) |
466 | 464, 465 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π΅βπ) Β· (sinβ(π Β· π))) = ((π΅βπ) Β· (sinβ(π Β· π)))) |
467 | 463, 466 | oveq12d 7380 |
. . . . . . . . . . . . . 14
β’ (π = π β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
468 | 467 | cbvsumv 15588 |
. . . . . . . . . . . . 13
β’
Ξ£π β
(1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) |
469 | 468 | oveq2i 7373 |
. . . . . . . . . . . 12
β’ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
470 | 469 | mpteq2i 5215 |
. . . . . . . . . . 11
β’ (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) = (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
471 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
β’ (π = π β (1...π) = (1...π)) |
472 | 471 | sumeq1d 15593 |
. . . . . . . . . . . . . 14
β’ (π = π β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
473 | 472 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π = π β (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
474 | 473 | cbvmptv 5223 |
. . . . . . . . . . . 12
β’ (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) = (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
475 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π΄βπ) = (π΄βπ)) |
476 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π Β· π) = (π Β· π)) |
477 | 476 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (cosβ(π Β· π)) = (cosβ(π Β· π))) |
478 | 475, 477 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π΄βπ) Β· (cosβ(π Β· π))) = ((π΄βπ) Β· (cosβ(π Β· π)))) |
479 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π΅βπ) = (π΅βπ)) |
480 | 476 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (sinβ(π Β· π)) = (sinβ(π Β· π))) |
481 | 479, 480 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π΅βπ) Β· (sinβ(π Β· π))) = ((π΅βπ) Β· (sinβ(π Β· π)))) |
482 | 478, 481 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
β’ (π = π β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
483 | 482 | cbvsumv 15588 |
. . . . . . . . . . . . . 14
β’
Ξ£π β
(1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) |
484 | 483 | oveq2i 7373 |
. . . . . . . . . . . . 13
β’ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
485 | 484 | mpteq2i 5215 |
. . . . . . . . . . . 12
β’ (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) = (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
486 | 474, 485 | eqtri 2765 |
. . . . . . . . . . 11
β’ (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) = (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
487 | 28, 470, 486 | 3eqtri 2769 |
. . . . . . . . . 10
β’ π = (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
488 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β (π + π¦) = (π + π₯)) |
489 | 488 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β (πΉβ(π + π¦)) = (πΉβ(π + π₯))) |
490 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β ((π·βπ)βπ¦) = ((π·βπ)βπ₯)) |
491 | 489, 490 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β ((πΉβ(π + π¦)) Β· ((π·βπ)βπ¦)) = ((πΉβ(π + π₯)) Β· ((π·βπ)βπ₯))) |
492 | 491 | cbvmptv 5223 |
. . . . . . . . . 10
β’ (π¦ β β β¦ ((πΉβ(π + π¦)) Β· ((π·βπ)βπ¦))) = (π₯ β β β¦ ((πΉβ(π + π₯)) Β· ((π·βπ)βπ₯))) |
493 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β β β¦ {π β (β
βm (0...π))
β£ (((πβ0) =
(-Ο β π) β§
(πβπ) = (Ο β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (-Ο β π) β§ (πβπ) = (Ο β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
494 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (πβπ) = (πβπ)) |
495 | 494 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π = π β ((πβπ) β π) = ((πβπ) β π)) |
496 | 495 | cbvmptv 5223 |
. . . . . . . . . 10
β’ (π β (0...π) β¦ ((πβπ) β π)) = (π β (0...π) β¦ ((πβπ) β π)) |
497 | 451, 459,
487, 288, 51, 52, 53, 146, 43, 92, 492, 103, 222, 233, 48, 493, 496 | fourierdlem111 44532 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβπ) = (β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ + β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )) |
498 | 443, 497 | chvarvv 2003 |
. . . . . . . 8
β’ ((π β§ π β β) β (πβπ) = (β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ + β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )) |
499 | 411, 436 | oveq12d 7380 |
. . . . . . . 8
β’ ((π β§ π β β) β (((π β β β¦
β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )βπ) + ((π β β β¦
β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )βπ)) = (β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ + β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )) |
500 | 498, 499 | eqtr4d 2780 |
. . . . . . 7
β’ ((π β§ π β β) β (πβπ) = (((π β β β¦
β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )βπ) + ((π β β β¦
β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )βπ))) |
501 | 16, 24, 27, 42, 14, 15, 333, 337, 359, 412, 437, 500 | climaddf 43930 |
. . . . . 6
β’ (π β π β ((πΏ / 2) + (π
/ 2))) |
502 | | limccl 25255 |
. . . . . . . 8
β’ ((πΉ βΎ (-β(,)π)) limβ π) β
β |
503 | 502, 285 | sselid 3947 |
. . . . . . 7
β’ (π β πΏ β β) |
504 | | limccl 25255 |
. . . . . . . 8
β’ ((πΉ βΎ (π(,)+β)) limβ π) β
β |
505 | 504, 284 | sselid 3947 |
. . . . . . 7
β’ (π β π
β β) |
506 | | 2cnd 12238 |
. . . . . . 7
β’ (π β 2 β
β) |
507 | | 2pos 12263 |
. . . . . . . . 9
β’ 0 <
2 |
508 | 507 | a1i 11 |
. . . . . . . 8
β’ (π β 0 < 2) |
509 | 508 | gt0ne0d 11726 |
. . . . . . 7
β’ (π β 2 β 0) |
510 | 503, 505,
506, 509 | divdird 11976 |
. . . . . 6
β’ (π β ((πΏ + π
) / 2) = ((πΏ / 2) + (π
/ 2))) |
511 | 501, 510 | breqtrrd 5138 |
. . . . 5
β’ (π β π β ((πΏ + π
) / 2)) |
512 | | 0nn0 12435 |
. . . . . . . 8
β’ 0 β
β0 |
513 | 43 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ 0 β
β0) β πΉ:ββΆβ) |
514 | | eqid 2737 |
. . . . . . . . . 10
β’
(-Ο(,)Ο) = (-Ο(,)Ο) |
515 | | ioossre 13332 |
. . . . . . . . . . . . . 14
β’
(-Ο(,)Ο) β β |
516 | 515 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (-Ο(,)Ο) β
β) |
517 | 43, 516 | feqresmpt 6916 |
. . . . . . . . . . . 12
β’ (π β (πΉ βΎ (-Ο(,)Ο)) = (π₯ β (-Ο(,)Ο) β¦
(πΉβπ₯))) |
518 | | ioossicc 13357 |
. . . . . . . . . . . . . 14
β’
(-Ο(,)Ο) β (-Ο[,]Ο) |
519 | 518 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (-Ο(,)Ο) β
(-Ο[,]Ο)) |
520 | | ioombl 24945 |
. . . . . . . . . . . . . 14
β’
(-Ο(,)Ο) β dom vol |
521 | 520 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (-Ο(,)Ο) β dom
vol) |
522 | 43 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (-Ο[,]Ο)) β πΉ:ββΆβ) |
523 | 385 | sselda 3949 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (-Ο[,]Ο)) β π₯ β
β) |
524 | 522, 523 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (-Ο[,]Ο)) β (πΉβπ₯) β β) |
525 | 43, 385 | feqresmpt 6916 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ βΎ (-Ο[,]Ο)) = (π₯ β (-Ο[,]Ο) β¦
(πΉβπ₯))) |
526 | 178 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β
β) |
527 | 43, 526 | fssd 6691 |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:ββΆβ) |
528 | 527, 385 | fssresd 6714 |
. . . . . . . . . . . . . . 15
β’ (π β (πΉ βΎ
(-Ο[,]Ο)):(-Ο[,]Ο)βΆβ) |
529 | | ioossicc 13357 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)[,](πβ(π + 1))) |
530 | 61 | rexri 11220 |
. . . . . . . . . . . . . . . . . . . 20
β’ -Ο
β β* |
531 | 530 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0..^π)) β -Ο β
β*) |
532 | 54 | rexri 11220 |
. . . . . . . . . . . . . . . . . . . 20
β’ Ο
β β* |
533 | 532 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0..^π)) β Ο β
β*) |
534 | 51, 52, 53 | fourierdlem15 44437 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π:(0...π)βΆ(-Ο[,]Ο)) |
535 | 534 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆ(-Ο[,]Ο)) |
536 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0..^π)) β π β (0..^π)) |
537 | 531, 533,
535, 536 | fourierdlem8 44430 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β ((πβπ)[,](πβ(π + 1))) β
(-Ο[,]Ο)) |
538 | 529, 537 | sstrid 3960 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β
(-Ο[,]Ο)) |
539 | 538 | resabs1d 5973 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β ((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) = (πΉ βΎ ((πβπ)(,)(πβ(π + 1))))) |
540 | 539, 103 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β ((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
541 | 539 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = ((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1))))) |
542 | 541 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = (((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
543 | 222, 542 | eleqtrd 2840 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β πΆ β (((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
544 | 541 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = (((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
545 | 233, 544 | eleqtrd 2840 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β π β (((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
546 | 51, 52, 53, 528, 540, 543, 545 | fourierdlem69 44490 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ βΎ (-Ο[,]Ο)) β
πΏ1) |
547 | 525, 546 | eqeltrrd 2839 |
. . . . . . . . . . . . 13
β’ (π β (π₯ β (-Ο[,]Ο) β¦ (πΉβπ₯)) β
πΏ1) |
548 | 519, 521,
524, 547 | iblss 25185 |
. . . . . . . . . . . 12
β’ (π β (π₯ β (-Ο(,)Ο) β¦ (πΉβπ₯)) β
πΏ1) |
549 | 517, 548 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ (π β (πΉ βΎ (-Ο(,)Ο)) β
πΏ1) |
550 | 549 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ 0 β
β0) β (πΉ βΎ (-Ο(,)Ο)) β
πΏ1) |
551 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ 0 β
β0) β 0 β β0) |
552 | 513, 514,
550, 29, 551 | fourierdlem16 44438 |
. . . . . . . . 9
β’ ((π β§ 0 β
β0) β (((π΄β0) β β β§ (π₯ β (-Ο(,)Ο) β¦
(πΉβπ₯)) β πΏ1) β§
β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(0 Β· π₯))) dπ₯ β β)) |
553 | 552 | simplld 767 |
. . . . . . . 8
β’ ((π β§ 0 β
β0) β (π΄β0) β β) |
554 | 512, 553 | mpan2 690 |
. . . . . . 7
β’ (π β (π΄β0) β β) |
555 | 554 | rehalfcld 12407 |
. . . . . 6
β’ (π β ((π΄β0) / 2) β
β) |
556 | 555 | recnd 11190 |
. . . . 5
β’ (π β ((π΄β0) / 2) β
β) |
557 | 334 | mptex 7178 |
. . . . . 6
β’ (π β β β¦
Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β V |
558 | 557 | a1i 11 |
. . . . 5
β’ (π β (π β β β¦ Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β V) |
559 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
560 | 555 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((π΄β0) / 2) β
β) |
561 | | fzfid 13885 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (1...π) β Fin) |
562 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...π)) β π) |
563 | | elfznn 13477 |
. . . . . . . . . . . 12
β’ (π β (1...π) β π β β) |
564 | 563 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...π)) β π β β) |
565 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π) |
566 | 362 | nnnn0d 12480 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β β0) |
567 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β β0 β π β
β0)) |
568 | 567 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π β§ π β β0) β (π β§ π β
β0))) |
569 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π΄βπ) = (π΄βπ)) |
570 | 569 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π΄βπ) β β β (π΄βπ) β β)) |
571 | 568, 570 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π = π β (((π β§ π β β0) β (π΄βπ) β β) β ((π β§ π β β0) β (π΄βπ) β β))) |
572 | 43 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β0) β πΉ:ββΆβ) |
573 | 549 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β0) β (πΉ βΎ (-Ο(,)Ο)) β
πΏ1) |
574 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β0) β π β
β0) |
575 | 572, 514,
573, 29, 574 | fourierdlem16 44438 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β0) β (((π΄βπ) β β β§ (π₯ β (-Ο(,)Ο) β¦ (πΉβπ₯)) β πΏ1) β§
β«(-Ο(,)Ο)((πΉβπ₯) Β· (cosβ(π Β· π₯))) dπ₯ β β)) |
576 | 575 | simplld 767 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β0) β (π΄βπ) β β) |
577 | 571, 576 | chvarvv 2003 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β (π΄βπ) β β) |
578 | 565, 566,
577 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (π΄βπ) β β) |
579 | 362 | nnred 12175 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π β β) |
580 | 579, 399 | remulcld 11192 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π Β· π) β β) |
581 | 580 | recoscld 16033 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (cosβ(π Β· π)) β β) |
582 | 578, 581 | remulcld 11192 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((π΄βπ) Β· (cosβ(π Β· π))) β β) |
583 | | eleq1w 2821 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π β β β π β β)) |
584 | 583 | anbi2d 630 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π β§ π β β) β (π β§ π β β))) |
585 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π΅βπ) = (π΅βπ)) |
586 | 585 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π΅βπ) β β β (π΅βπ) β β)) |
587 | 584, 586 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π = π β (((π β§ π β β) β (π΅βπ) β β) β ((π β§ π β β) β (π΅βπ) β β))) |
588 | 43 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β πΉ:ββΆβ) |
589 | 549 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (πΉ βΎ (-Ο(,)Ο)) β
πΏ1) |
590 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π β β) |
591 | 588, 514,
589, 452, 590 | fourierdlem21 44443 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (((π΅βπ) β β β§ (π₯ β (-Ο(,)Ο) β¦ ((πΉβπ₯) Β· (sinβ(π Β· π₯)))) β πΏ1) β§
β«(-Ο(,)Ο)((πΉβπ₯) Β· (sinβ(π Β· π₯))) dπ₯ β β)) |
592 | 591 | simplld 767 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π΅βπ) β β) |
593 | 587, 592 | chvarvv 2003 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (π΅βπ) β β) |
594 | 580 | resincld 16032 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (sinβ(π Β· π)) β β) |
595 | 593, 594 | remulcld 11192 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((π΅βπ) Β· (sinβ(π Β· π))) β β) |
596 | 582, 595 | readdcld 11191 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) β β) |
597 | 562, 564,
596 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (1...π)) β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) β β) |
598 | 561, 597 | fsumrecl 15626 |
. . . . . . . . 9
β’ ((π β§ π β β) β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) β β) |
599 | 560, 598 | readdcld 11191 |
. . . . . . . 8
β’ ((π β§ π β β) β (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β β) |
600 | 28 | fvmpt2 6964 |
. . . . . . . 8
β’ ((π β β β§ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β β) β (πβπ) = (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
601 | 559, 599,
600 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β β) β (πβπ) = (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
602 | 601, 599 | eqeltrd 2838 |
. . . . . 6
β’ ((π β§ π β β) β (πβπ) β β) |
603 | 602 | recnd 11190 |
. . . . 5
β’ ((π β§ π β β) β (πβπ) β β) |
604 | | eqidd 2738 |
. . . . . . 7
β’ ((π β§ π β β) β (π β β β¦ Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = (π β β β¦ Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
605 | | oveq2 7370 |
. . . . . . . . 9
β’ (π = π β (1...π) = (1...π)) |
606 | 605 | sumeq1d 15593 |
. . . . . . . 8
β’ (π = π β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
607 | 606 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β β) β§ π = π) β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
608 | | sumex 15579 |
. . . . . . . 8
β’
Ξ£π β
(1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) β V |
609 | 608 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β) β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) β V) |
610 | 604, 607,
559, 609 | fvmptd 6960 |
. . . . . 6
β’ ((π β§ π β β) β ((π β β β¦ Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))βπ) = Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
611 | 560 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ π β β) β ((π΄β0) / 2) β
β) |
612 | 598 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ π β β) β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) β β) |
613 | 611, 612 | pncan2d 11521 |
. . . . . . 7
β’ ((π β§ π β β) β ((((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β ((π΄β0) / 2)) = Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
614 | 613, 468 | eqtr2di 2794 |
. . . . . 6
β’ ((π β§ π β β) β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = ((((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β ((π΄β0) / 2))) |
615 | | ovex 7395 |
. . . . . . . . 9
β’ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β V |
616 | 28 | fvmpt2 6964 |
. . . . . . . . 9
β’ ((π β β β§ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β V) β (πβπ) = (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
617 | 559, 615,
616 | sylancl 587 |
. . . . . . . 8
β’ ((π β§ π β β) β (πβπ) = (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
618 | 617 | eqcomd 2743 |
. . . . . . 7
β’ ((π β§ π β β) β (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = (πβπ)) |
619 | 618 | oveq1d 7377 |
. . . . . 6
β’ ((π β§ π β β) β ((((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β ((π΄β0) / 2)) = ((πβπ) β ((π΄β0) / 2))) |
620 | 610, 614,
619 | 3eqtrd 2781 |
. . . . 5
β’ ((π β§ π β β) β ((π β β β¦ Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))βπ) = ((πβπ) β ((π΄β0) / 2))) |
621 | 14, 15, 511, 556, 558, 603, 620 | climsubc1 15527 |
. . . 4
β’ (π β (π β β β¦ Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β (((πΏ + π
) / 2) β ((π΄β0) / 2))) |
622 | | seqex 13915 |
. . . . . 6
β’ seq1( + ,
(π β β β¦
(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) β V |
623 | 622 | a1i 11 |
. . . . 5
β’ (π β seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) β V) |
624 | | eqidd 2738 |
. . . . . . 7
β’ ((π β§ π β β) β (π β β β¦ Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = (π β β β¦ Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
625 | | oveq2 7370 |
. . . . . . . . 9
β’ (π = π β (1...π) = (1...π)) |
626 | 625 | sumeq1d 15593 |
. . . . . . . 8
β’ (π = π β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
627 | 626 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β β) β§ π = π) β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
628 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β β) β π β β) |
629 | | fzfid 13885 |
. . . . . . . 8
β’ ((π β§ π β β) β (1...π) β Fin) |
630 | | elfznn 13477 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β π β β) |
631 | 630 | nnnn0d 12480 |
. . . . . . . . . . . 12
β’ (π β (1...π) β π β β0) |
632 | 631, 576 | sylan2 594 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (π΄βπ) β β) |
633 | 630 | nnred 12175 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β π β β) |
634 | 633 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β π β β) |
635 | 146 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β π β β) |
636 | 634, 635 | remulcld 11192 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (π Β· π) β β) |
637 | 636 | recoscld 16033 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (cosβ(π Β· π)) β β) |
638 | 632, 637 | remulcld 11192 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β ((π΄βπ) Β· (cosβ(π Β· π))) β β) |
639 | 630, 592 | sylan2 594 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (π΅βπ) β β) |
640 | 636 | resincld 16032 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (sinβ(π Β· π)) β β) |
641 | 639, 640 | remulcld 11192 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β ((π΅βπ) Β· (sinβ(π Β· π))) β β) |
642 | 638, 641 | readdcld 11191 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) β β) |
643 | 642 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (1...π)) β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) β β) |
644 | 629, 643 | fsumrecl 15626 |
. . . . . . 7
β’ ((π β§ π β β) β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) β β) |
645 | 624, 627,
628, 644 | fvmptd 6960 |
. . . . . 6
β’ ((π β§ π β β) β ((π β β β¦ Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))βπ) = Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
646 | | eleq1w 2821 |
. . . . . . . . 9
β’ (π = π β (π β β β π β β)) |
647 | 646 | anbi2d 630 |
. . . . . . . 8
β’ (π = π β ((π β§ π β β) β (π β§ π β β))) |
648 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = π β (seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))))βπ) = (seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))))βπ)) |
649 | 626, 648 | eqeq12d 2753 |
. . . . . . . 8
β’ (π = π β (Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))))βπ) β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))))βπ))) |
650 | 647, 649 | imbi12d 345 |
. . . . . . 7
β’ (π = π β (((π β§ π β β) β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))))βπ)) β ((π β§ π β β) β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))))βπ)))) |
651 | | eqidd 2738 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (1...π)) β (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
652 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (π΄βπ) = (π΄βπ)) |
653 | | oveq1 7369 |
. . . . . . . . . . . . 13
β’ (π = π β (π Β· π) = (π Β· π)) |
654 | 653 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π = π β (cosβ(π Β· π)) = (cosβ(π Β· π))) |
655 | 652, 654 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = π β ((π΄βπ) Β· (cosβ(π Β· π))) = ((π΄βπ) Β· (cosβ(π Β· π)))) |
656 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (π΅βπ) = (π΅βπ)) |
657 | 653 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π = π β (sinβ(π Β· π)) = (sinβ(π Β· π))) |
658 | 656, 657 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = π β ((π΅βπ) Β· (sinβ(π Β· π))) = ((π΅βπ) Β· (sinβ(π Β· π)))) |
659 | 655, 658 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π = π β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
660 | 659 | adantl 483 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ π β (1...π)) β§ π = π) β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
661 | | elfznn 13477 |
. . . . . . . . . 10
β’ (π β (1...π) β π β β) |
662 | 661 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (1...π)) β π β β) |
663 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (1...π)) β π) |
664 | | nnnn0 12427 |
. . . . . . . . . . . 12
β’ (π β β β π β
β0) |
665 | | nn0re 12429 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β π β
β) |
666 | 665 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β0) β π β
β) |
667 | 146 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β0) β π β
β) |
668 | 666, 667 | remulcld 11192 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β (π Β· π) β β) |
669 | 668 | recoscld 16033 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β
(cosβ(π Β·
π)) β
β) |
670 | 576, 669 | remulcld 11192 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β ((π΄βπ) Β· (cosβ(π Β· π))) β β) |
671 | 664, 670 | sylan2 594 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((π΄βπ) Β· (cosβ(π Β· π))) β β) |
672 | 664, 668 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (π Β· π) β β) |
673 | 672 | resincld 16032 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (sinβ(π Β· π)) β β) |
674 | 592, 673 | remulcld 11192 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((π΅βπ) Β· (sinβ(π Β· π))) β β) |
675 | 671, 674 | readdcld 11191 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) β β) |
676 | 663, 662,
675 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (1...π)) β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) β β) |
677 | 651, 660,
662, 676 | fvmptd 6960 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (1...π)) β ((π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))βπ) = (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
678 | 362, 14 | eleqtrdi 2848 |
. . . . . . . 8
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
679 | 676 | recnd 11190 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (1...π)) β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) β β) |
680 | 677, 678,
679 | fsumser 15622 |
. . . . . . 7
β’ ((π β§ π β β) β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))))βπ)) |
681 | 650, 680 | chvarvv 2003 |
. . . . . 6
β’ ((π β§ π β β) β Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))))βπ)) |
682 | 645, 681 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π β β) β ((π β β β¦ Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))βπ) = (seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))))βπ)) |
683 | 14, 558, 623, 15, 682 | climeq 15456 |
. . . 4
β’ (π β ((π β β β¦ Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) β (((πΏ + π
) / 2) β ((π΄β0) / 2)) β seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) β (((πΏ + π
) / 2) β ((π΄β0) / 2)))) |
684 | 621, 683 | mpbid 231 |
. . 3
β’ (π β seq1( + , (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) β (((πΏ + π
) / 2) β ((π΄β0) / 2))) |
685 | 13, 684 | eqbrtrd 5132 |
. 2
β’ (π β seq1( + , π) β (((πΏ + π
) / 2) β ((π΄β0) / 2))) |
686 | | eqidd 2738 |
. . . . . 6
β’ ((π β§ π β β) β (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = (π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
687 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = π β (π΄βπ) = (π΄βπ)) |
688 | | oveq1 7369 |
. . . . . . . . . 10
β’ (π = π β (π Β· π) = (π Β· π)) |
689 | 688 | fveq2d 6851 |
. . . . . . . . 9
β’ (π = π β (cosβ(π Β· π)) = (cosβ(π Β· π))) |
690 | 687, 689 | oveq12d 7380 |
. . . . . . . 8
β’ (π = π β ((π΄βπ) Β· (cosβ(π Β· π))) = ((π΄βπ) Β· (cosβ(π Β· π)))) |
691 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = π β (π΅βπ) = (π΅βπ)) |
692 | 688 | fveq2d 6851 |
. . . . . . . . 9
β’ (π = π β (sinβ(π Β· π)) = (sinβ(π Β· π))) |
693 | 691, 692 | oveq12d 7380 |
. . . . . . . 8
β’ (π = π β ((π΅βπ) Β· (sinβ(π Β· π))) = ((π΅βπ) Β· (sinβ(π Β· π)))) |
694 | 690, 693 | oveq12d 7380 |
. . . . . . 7
β’ (π = π β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
695 | 694 | adantl 483 |
. . . . . 6
β’ (((π β§ π β β) β§ π = π) β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
696 | 686, 695,
362, 596 | fvmptd 6960 |
. . . . 5
β’ ((π β§ π β β) β ((π β β β¦ (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))βπ) = (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) |
697 | 596 | recnd 11190 |
. . . . 5
β’ ((π β§ π β β) β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) β β) |
698 | 14, 15, 696, 697, 684 | isumclim 15649 |
. . . 4
β’ (π β Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))) = (((πΏ + π
) / 2) β ((π΄β0) / 2))) |
699 | 698 | oveq2d 7378 |
. . 3
β’ (π β (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = (((π΄β0) / 2) + (((πΏ + π
) / 2) β ((π΄β0) / 2)))) |
700 | 503, 505 | addcld 11181 |
. . . . 5
β’ (π β (πΏ + π
) β β) |
701 | 700 | halfcld 12405 |
. . . 4
β’ (π β ((πΏ + π
) / 2) β β) |
702 | 556, 701 | pncan3d 11522 |
. . 3
β’ (π β (((π΄β0) / 2) + (((πΏ + π
) / 2) β ((π΄β0) / 2))) = ((πΏ + π
) / 2)) |
703 | 699, 702 | eqtrd 2777 |
. 2
β’ (π β (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = ((πΏ + π
) / 2)) |
704 | 685, 703 | jca 513 |
1
β’ (π β (seq1( + , π) β (((πΏ + π
) / 2) β ((π΄β0) / 2)) β§ (((π΄β0) / 2) + Ξ£π β β (((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π))))) = ((πΏ + π
) / 2))) |