Step | Hyp | Ref
| Expression |
1 | | fourierdlem75.xre |
. . . . 5
β’ (π β π β β) |
2 | 1 | ad2antrr 725 |
. . . 4
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β π β β) |
3 | | fourierdlem75.v |
. . . . . . . . . 10
β’ (π β π β (πβπ)) |
4 | | fourierdlem75.m |
. . . . . . . . . . 11
β’ (π β π β β) |
5 | | fourierdlem75.p |
. . . . . . . . . . . 12
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
6 | 5 | fourierdlem2 44452 |
. . . . . . . . . . 11
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
7 | 4, 6 | syl 17 |
. . . . . . . . . 10
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
8 | 3, 7 | mpbid 231 |
. . . . . . . . 9
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
9 | 8 | simpld 496 |
. . . . . . . 8
β’ (π β π β (β βm
(0...π))) |
10 | | elmapi 8795 |
. . . . . . . 8
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
11 | 9, 10 | syl 17 |
. . . . . . 7
β’ (π β π:(0...π)βΆβ) |
12 | 11 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆβ) |
13 | | fzofzp1 13680 |
. . . . . . 7
β’ (π β (0..^π) β (π + 1) β (0...π)) |
14 | 13 | adantl 483 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
15 | 12, 14 | ffvelcdmd 7042 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
16 | 15 | adantr 482 |
. . . 4
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β (πβ(π + 1)) β β) |
17 | | eqcom 2739 |
. . . . . . 7
β’ ((πβπ) = π β π = (πβπ)) |
18 | 17 | biimpi 215 |
. . . . . 6
β’ ((πβπ) = π β π = (πβπ)) |
19 | 18 | adantl 483 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β π = (πβπ)) |
20 | 8 | simprrd 773 |
. . . . . . 7
β’ (π β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
21 | 20 | r19.21bi 3233 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
22 | 21 | adantr 482 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β (πβπ) < (πβ(π + 1))) |
23 | 19, 22 | eqbrtrd 5133 |
. . . 4
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β π < (πβ(π + 1))) |
24 | | fourierdlem75.f |
. . . . . . 7
β’ (π β πΉ:ββΆβ) |
25 | 24 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β πΉ:ββΆβ) |
26 | | ioossre 13336 |
. . . . . . 7
β’ (π(,)(πβ(π + 1))) β β |
27 | 26 | a1i 11 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (π(,)(πβ(π + 1))) β β) |
28 | 25, 27 | fssresd 6715 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (πΉ βΎ (π(,)(πβ(π + 1)))):(π(,)(πβ(π + 1)))βΆβ) |
29 | 28 | adantr 482 |
. . . 4
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β (πΉ βΎ (π(,)(πβ(π + 1)))):(π(,)(πβ(π + 1)))βΆβ) |
30 | | limcresi 25287 |
. . . . . . . 8
β’ ((πΉ βΎ (π(,)+β)) limβ π) β (((πΉ βΎ (π(,)+β)) βΎ (π(,)(πβ(π + 1)))) limβ π) |
31 | | fourierdlem75.y |
. . . . . . . 8
β’ (π β π β ((πΉ βΎ (π(,)+β)) limβ π)) |
32 | 30, 31 | sselid 3946 |
. . . . . . 7
β’ (π β π β (((πΉ βΎ (π(,)+β)) βΎ (π(,)(πβ(π + 1)))) limβ π)) |
33 | 32 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β π β (((πΉ βΎ (π(,)+β)) βΎ (π(,)(πβ(π + 1)))) limβ π)) |
34 | | pnfxr 11219 |
. . . . . . . . . 10
β’ +β
β β* |
35 | 34 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β +β β
β*) |
36 | 15 | rexrd 11215 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β
β*) |
37 | 15 | ltpnfd 13052 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) < +β) |
38 | 36, 35, 37 | xrltled 13080 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β€ +β) |
39 | | iooss2 13311 |
. . . . . . . . 9
β’
((+β β β* β§ (πβ(π + 1)) β€ +β) β (π(,)(πβ(π + 1))) β (π(,)+β)) |
40 | 35, 38, 39 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (π(,)(πβ(π + 1))) β (π(,)+β)) |
41 | 40 | resabs1d 5974 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β ((πΉ βΎ (π(,)+β)) βΎ (π(,)(πβ(π + 1)))) = (πΉ βΎ (π(,)(πβ(π + 1))))) |
42 | 41 | oveq1d 7378 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (((πΉ βΎ (π(,)+β)) βΎ (π(,)(πβ(π + 1)))) limβ π) = ((πΉ βΎ (π(,)(πβ(π + 1)))) limβ π)) |
43 | 33, 42 | eleqtrd 2835 |
. . . . 5
β’ ((π β§ π β (0..^π)) β π β ((πΉ βΎ (π(,)(πβ(π + 1)))) limβ π)) |
44 | 43 | adantr 482 |
. . . 4
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β π β ((πΉ βΎ (π(,)(πβ(π + 1)))) limβ π)) |
45 | | eqid 2732 |
. . . 4
β’ (β
D (πΉ βΎ (π(,)(πβ(π + 1))))) = (β D (πΉ βΎ (π(,)(πβ(π + 1))))) |
46 | | ax-resscn 11118 |
. . . . . . . . . . 11
β’ β
β β |
47 | 46 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β
β) |
48 | 24, 47 | fssd 6692 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ) |
49 | | ssid 3970 |
. . . . . . . . . . 11
β’ β
β β |
50 | 49 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β
β) |
51 | 26 | a1i 11 |
. . . . . . . . . 10
β’ (π β (π(,)(πβ(π + 1))) β β) |
52 | | eqid 2732 |
. . . . . . . . . . 11
β’
(TopOpenββfld) =
(TopOpenββfld) |
53 | 52 | tgioo2 24204 |
. . . . . . . . . . 11
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
54 | 52, 53 | dvres 25313 |
. . . . . . . . . 10
β’
(((β β β β§ πΉ:ββΆβ) β§ (β
β β β§ (π(,)(πβ(π + 1))) β β)) β (β D
(πΉ βΎ (π(,)(πβ(π + 1))))) = ((β D πΉ) βΎ ((intβ(topGenβran
(,)))β(π(,)(πβ(π + 1)))))) |
55 | 47, 48, 50, 51, 54 | syl22anc 838 |
. . . . . . . . 9
β’ (π β (β D (πΉ βΎ (π(,)(πβ(π + 1))))) = ((β D πΉ) βΎ ((intβ(topGenβran
(,)))β(π(,)(πβ(π + 1)))))) |
56 | | fourierdlem75.g |
. . . . . . . . . . 11
β’ πΊ = (β D πΉ) |
57 | 56 | eqcomi 2741 |
. . . . . . . . . 10
β’ (β
D πΉ) = πΊ |
58 | | ioontr 43851 |
. . . . . . . . . 10
β’
((intβ(topGenβran (,)))β(π(,)(πβ(π + 1)))) = (π(,)(πβ(π + 1))) |
59 | 57, 58 | reseq12i 5941 |
. . . . . . . . 9
β’ ((β
D πΉ) βΎ
((intβ(topGenβran (,)))β(π(,)(πβ(π + 1))))) = (πΊ βΎ (π(,)(πβ(π + 1)))) |
60 | 55, 59 | eqtrdi 2788 |
. . . . . . . 8
β’ (π β (β D (πΉ βΎ (π(,)(πβ(π + 1))))) = (πΊ βΎ (π(,)(πβ(π + 1))))) |
61 | 60 | adantr 482 |
. . . . . . 7
β’ ((π β§ (πβπ) = π) β (β D (πΉ βΎ (π(,)(πβ(π + 1))))) = (πΊ βΎ (π(,)(πβ(π + 1))))) |
62 | 61 | dmeqd 5867 |
. . . . . 6
β’ ((π β§ (πβπ) = π) β dom (β D (πΉ βΎ (π(,)(πβ(π + 1))))) = dom (πΊ βΎ (π(,)(πβ(π + 1))))) |
63 | 62 | adantlr 714 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β dom (β D (πΉ βΎ (π(,)(πβ(π + 1))))) = dom (πΊ βΎ (π(,)(πβ(π + 1))))) |
64 | | fourierdlem75.gcn |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
65 | 64 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
66 | | oveq1 7370 |
. . . . . . . . . . 11
β’ ((πβπ) = π β ((πβπ)(,)(πβ(π + 1))) = (π(,)(πβ(π + 1)))) |
67 | 66 | reseq2d 5943 |
. . . . . . . . . 10
β’ ((πβπ) = π β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) = (πΊ βΎ (π(,)(πβ(π + 1))))) |
68 | 67 | feq1d 6659 |
. . . . . . . . 9
β’ ((πβπ) = π β ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ β (πΊ βΎ (π(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ)) |
69 | 68 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ β (πΊ βΎ (π(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ)) |
70 | 65, 69 | mpbid 231 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β (πΊ βΎ (π(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
71 | 66 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β ((πβπ)(,)(πβ(π + 1))) = (π(,)(πβ(π + 1)))) |
72 | 71 | feq2d 6660 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β ((πΊ βΎ (π(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ β (πΊ βΎ (π(,)(πβ(π + 1)))):(π(,)(πβ(π + 1)))βΆβ)) |
73 | 70, 72 | mpbid 231 |
. . . . . 6
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β (πΊ βΎ (π(,)(πβ(π + 1)))):(π(,)(πβ(π + 1)))βΆβ) |
74 | | fdm 6683 |
. . . . . 6
β’ ((πΊ βΎ (π(,)(πβ(π + 1)))):(π(,)(πβ(π + 1)))βΆβ β dom (πΊ βΎ (π(,)(πβ(π + 1)))) = (π(,)(πβ(π + 1)))) |
75 | 73, 74 | syl 17 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β dom (πΊ βΎ (π(,)(πβ(π + 1)))) = (π(,)(πβ(π + 1)))) |
76 | 63, 75 | eqtrd 2772 |
. . . 4
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β dom (β D (πΉ βΎ (π(,)(πβ(π + 1))))) = (π(,)(πβ(π + 1)))) |
77 | | limcresi 25287 |
. . . . . . . 8
β’ ((πΊ βΎ (π(,)+β)) limβ π) β (((πΊ βΎ (π(,)+β)) βΎ (π(,)(πβ(π + 1)))) limβ π) |
78 | | fourierdlem75.e |
. . . . . . . 8
β’ (π β πΈ β ((πΊ βΎ (π(,)+β)) limβ π)) |
79 | 77, 78 | sselid 3946 |
. . . . . . 7
β’ (π β πΈ β (((πΊ βΎ (π(,)+β)) βΎ (π(,)(πβ(π + 1)))) limβ π)) |
80 | 79 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β πΈ β (((πΊ βΎ (π(,)+β)) βΎ (π(,)(πβ(π + 1)))) limβ π)) |
81 | 40 | resabs1d 5974 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β ((πΊ βΎ (π(,)+β)) βΎ (π(,)(πβ(π + 1)))) = (πΊ βΎ (π(,)(πβ(π + 1))))) |
82 | 60 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (β D (πΉ βΎ (π(,)(πβ(π + 1))))) = (πΊ βΎ (π(,)(πβ(π + 1))))) |
83 | 81, 82 | eqtr4d 2775 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β ((πΊ βΎ (π(,)+β)) βΎ (π(,)(πβ(π + 1)))) = (β D (πΉ βΎ (π(,)(πβ(π + 1)))))) |
84 | 83 | oveq1d 7378 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (((πΊ βΎ (π(,)+β)) βΎ (π(,)(πβ(π + 1)))) limβ π) = ((β D (πΉ βΎ (π(,)(πβ(π + 1))))) limβ π)) |
85 | 80, 84 | eleqtrd 2835 |
. . . . 5
β’ ((π β§ π β (0..^π)) β πΈ β ((β D (πΉ βΎ (π(,)(πβ(π + 1))))) limβ π)) |
86 | 85 | adantr 482 |
. . . 4
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β πΈ β ((β D (πΉ βΎ (π(,)(πβ(π + 1))))) limβ π)) |
87 | | eqid 2732 |
. . . 4
β’ (π β (0(,)((πβ(π + 1)) β π)) β¦ ((((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π )) β π) / π )) = (π β (0(,)((πβ(π + 1)) β π)) β¦ ((((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π )) β π) / π )) |
88 | | oveq2 7371 |
. . . . . . 7
β’ (π₯ = π β (π + π₯) = (π + π )) |
89 | 88 | fveq2d 6852 |
. . . . . 6
β’ (π₯ = π β ((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π₯)) = ((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π ))) |
90 | 89 | oveq1d 7378 |
. . . . 5
β’ (π₯ = π β (((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π₯)) β π) = (((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π )) β π)) |
91 | 90 | cbvmptv 5224 |
. . . 4
β’ (π₯ β (0(,)((πβ(π + 1)) β π)) β¦ (((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π₯)) β π)) = (π β (0(,)((πβ(π + 1)) β π)) β¦ (((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π )) β π)) |
92 | | id 22 |
. . . . 5
β’ (π₯ = π β π₯ = π ) |
93 | 92 | cbvmptv 5224 |
. . . 4
β’ (π₯ β (0(,)((πβ(π + 1)) β π)) β¦ π₯) = (π β (0(,)((πβ(π + 1)) β π)) β¦ π ) |
94 | 2, 16, 23, 29, 44, 45, 76, 86, 87, 91, 93 | fourierdlem61 44510 |
. . 3
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β πΈ β ((π β (0(,)((πβ(π + 1)) β π)) β¦ ((((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π )) β π) / π )) limβ 0)) |
95 | | fourierdlem75.a |
. . . . 5
β’ π΄ = if((πβπ) = π, πΈ, ((π
β if((πβπ) < π, π, π)) / (πβπ))) |
96 | | iftrue 4498 |
. . . . 5
β’ ((πβπ) = π β if((πβπ) = π, πΈ, ((π
β if((πβπ) < π, π, π)) / (πβπ))) = πΈ) |
97 | 95, 96 | eqtrid 2784 |
. . . 4
β’ ((πβπ) = π β π΄ = πΈ) |
98 | 97 | adantl 483 |
. . 3
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β π΄ = πΈ) |
99 | | fourierdlem75.h |
. . . . . . 7
β’ π» = (π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) |
100 | 99 | reseq1i 5939 |
. . . . . 6
β’ (π» βΎ ((πβπ)(,)(πβ(π + 1)))) = ((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) βΎ ((πβπ)(,)(πβ(π + 1)))) |
101 | 100 | a1i 11 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β (π» βΎ ((πβπ)(,)(πβ(π + 1)))) = ((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) βΎ ((πβπ)(,)(πβ(π + 1))))) |
102 | | ioossicc 13361 |
. . . . . . . 8
β’ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)[,](πβ(π + 1))) |
103 | | pire 25853 |
. . . . . . . . . . . 12
β’ Ο
β β |
104 | 103 | renegcli 11472 |
. . . . . . . . . . 11
β’ -Ο
β β |
105 | 104 | rexri 11223 |
. . . . . . . . . 10
β’ -Ο
β β* |
106 | 105 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β -Ο β
β*) |
107 | 103 | rexri 11223 |
. . . . . . . . . 10
β’ Ο
β β* |
108 | 107 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β Ο β
β*) |
109 | 104 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π)) β -Ο β
β) |
110 | 103 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π)) β Ο β
β) |
111 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β -Ο β
β) |
112 | 111, 1 | readdcld 11194 |
. . . . . . . . . . . . . . . 16
β’ (π β (-Ο + π) β β) |
113 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β Ο β
β) |
114 | 113, 1 | readdcld 11194 |
. . . . . . . . . . . . . . . 16
β’ (π β (Ο + π) β β) |
115 | 112, 114 | iccssred 13362 |
. . . . . . . . . . . . . . 15
β’ (π β ((-Ο + π)[,](Ο + π)) β β) |
116 | 115 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π)) β ((-Ο + π)[,](Ο + π)) β β) |
117 | 5, 4, 3 | fourierdlem15 44465 |
. . . . . . . . . . . . . . 15
β’ (π β π:(0...π)βΆ((-Ο + π)[,](Ο + π))) |
118 | 117 | ffvelcdmda 7041 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π)) β (πβπ) β ((-Ο + π)[,](Ο + π))) |
119 | 116, 118 | sseldd 3949 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π)) β (πβπ) β β) |
120 | 1 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π)) β π β β) |
121 | 119, 120 | resubcld 11593 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π)) β ((πβπ) β π) β β) |
122 | 111 | recnd 11193 |
. . . . . . . . . . . . . . . 16
β’ (π β -Ο β
β) |
123 | 1 | recnd 11193 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
124 | 122, 123 | pncand 11523 |
. . . . . . . . . . . . . . 15
β’ (π β ((-Ο + π) β π) = -Ο) |
125 | 124 | eqcomd 2738 |
. . . . . . . . . . . . . 14
β’ (π β -Ο = ((-Ο + π) β π)) |
126 | 125 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π)) β -Ο = ((-Ο + π) β π)) |
127 | 112 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π)) β (-Ο + π) β β) |
128 | 114 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0...π)) β (Ο + π) β β) |
129 | | elicc2 13340 |
. . . . . . . . . . . . . . . . 17
β’ (((-Ο
+ π) β β β§
(Ο + π) β β)
β ((πβπ) β ((-Ο + π)[,](Ο + π)) β ((πβπ) β β β§ (-Ο + π) β€ (πβπ) β§ (πβπ) β€ (Ο + π)))) |
130 | 127, 128,
129 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...π)) β ((πβπ) β ((-Ο + π)[,](Ο + π)) β ((πβπ) β β β§ (-Ο + π) β€ (πβπ) β§ (πβπ) β€ (Ο + π)))) |
131 | 118, 130 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...π)) β ((πβπ) β β β§ (-Ο + π) β€ (πβπ) β§ (πβπ) β€ (Ο + π))) |
132 | 131 | simp2d 1144 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π)) β (-Ο + π) β€ (πβπ)) |
133 | 127, 119,
120, 132 | lesub1dd 11781 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π)) β ((-Ο + π) β π) β€ ((πβπ) β π)) |
134 | 126, 133 | eqbrtrd 5133 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π)) β -Ο β€ ((πβπ) β π)) |
135 | 131 | simp3d 1145 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π)) β (πβπ) β€ (Ο + π)) |
136 | 119, 128,
120, 135 | lesub1dd 11781 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π)) β ((πβπ) β π) β€ ((Ο + π) β π)) |
137 | 110 | recnd 11193 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π)) β Ο β
β) |
138 | 123 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π)) β π β β) |
139 | 137, 138 | pncand 11523 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π)) β ((Ο + π) β π) = Ο) |
140 | 136, 139 | breqtrd 5137 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π)) β ((πβπ) β π) β€ Ο) |
141 | 109, 110,
121, 134, 140 | eliccd 43844 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β ((πβπ) β π) β (-Ο[,]Ο)) |
142 | | fourierdlem75.q |
. . . . . . . . . . 11
β’ π = (π β (0...π) β¦ ((πβπ) β π)) |
143 | 141, 142 | fmptd 7068 |
. . . . . . . . . 10
β’ (π β π:(0...π)βΆ(-Ο[,]Ο)) |
144 | 143 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆ(-Ο[,]Ο)) |
145 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β π β (0..^π)) |
146 | 106, 108,
144, 145 | fourierdlem8 44458 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β ((πβπ)[,](πβ(π + 1))) β
(-Ο[,]Ο)) |
147 | 102, 146 | sstrid 3959 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β
(-Ο[,]Ο)) |
148 | 147 | resmptd 6000 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β ((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π )))) |
149 | 148 | adantr 482 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β ((π β (-Ο[,]Ο) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π )))) |
150 | | elfzofz 13599 |
. . . . . . . 8
β’ (π β (0..^π) β π β (0...π)) |
151 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β π β (0...π)) |
152 | 142 | fvmpt2 6965 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ ((πβπ) β π) β (-Ο[,]Ο)) β (πβπ) = ((πβπ) β π)) |
153 | 151, 141,
152 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β (πβπ) = ((πβπ) β π)) |
154 | 153 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ (πβπ) = π) β (πβπ) = ((πβπ) β π)) |
155 | | oveq1 7370 |
. . . . . . . . . 10
β’ ((πβπ) = π β ((πβπ) β π) = (π β π)) |
156 | 155 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ (πβπ) = π) β ((πβπ) β π) = (π β π)) |
157 | 123 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ (πβπ) = π) β π β β) |
158 | 157 | subidd 11510 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ (πβπ) = π) β (π β π) = 0) |
159 | 154, 156,
158 | 3eqtrd 2776 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ (πβπ) = π) β (πβπ) = 0) |
160 | 150, 159 | sylanl2 680 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β (πβπ) = 0) |
161 | | fveq2 6848 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ)) |
162 | 161 | oveq1d 7378 |
. . . . . . . . . . . 12
β’ (π = π β ((πβπ) β π) = ((πβπ) β π)) |
163 | 162 | cbvmptv 5224 |
. . . . . . . . . . 11
β’ (π β (0...π) β¦ ((πβπ) β π)) = (π β (0...π) β¦ ((πβπ) β π)) |
164 | 142, 163 | eqtri 2760 |
. . . . . . . . . 10
β’ π = (π β (0...π) β¦ ((πβπ) β π)) |
165 | 164 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β π = (π β (0...π) β¦ ((πβπ) β π))) |
166 | | fveq2 6848 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
167 | 166 | oveq1d 7378 |
. . . . . . . . . 10
β’ (π = (π + 1) β ((πβπ) β π) = ((πβ(π + 1)) β π)) |
168 | 167 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π = (π + 1)) β ((πβπ) β π) = ((πβ(π + 1)) β π)) |
169 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β β) |
170 | 15, 169 | resubcld 11593 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β ((πβ(π + 1)) β π) β β) |
171 | 165, 168,
14, 170 | fvmptd 6961 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) = ((πβ(π + 1)) β π)) |
172 | 171 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β (πβ(π + 1)) = ((πβ(π + 1)) β π)) |
173 | 160, 172 | oveq12d 7381 |
. . . . . 6
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β ((πβπ)(,)(πβ(π + 1))) = (0(,)((πβ(π + 1)) β π))) |
174 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β§ π = 0) β π β ((πβπ)(,)(πβ(π + 1)))) |
175 | | fourierdlem75.o |
. . . . . . . . . . . . 13
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
176 | 4 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π = 0) β π β β) |
177 | 111, 113,
1, 5, 175, 4, 3, 142 | fourierdlem14 44464 |
. . . . . . . . . . . . . 14
β’ (π β π β (πβπ)) |
178 | 177 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π = 0) β π β (πβπ)) |
179 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π = 0) β π = 0) |
180 | | fourierdlem75.x |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β ran π) |
181 | | ffn 6674 |
. . . . . . . . . . . . . . . . . . 19
β’ (π:(0...π)βΆ((-Ο + π)[,](Ο + π)) β π Fn (0...π)) |
182 | | fvelrnb 6909 |
. . . . . . . . . . . . . . . . . . 19
β’ (π Fn (0...π) β (π β ran π β βπ β (0...π)(πβπ) = π)) |
183 | 117, 181,
182 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π β ran π β βπ β (0...π)(πβπ) = π)) |
184 | 180, 183 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (π β βπ β (0...π)(πβπ) = π) |
185 | 159 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0...π)) β ((πβπ) = π β (πβπ) = 0)) |
186 | 185 | reximdva 3162 |
. . . . . . . . . . . . . . . . 17
β’ (π β (βπ β (0...π)(πβπ) = π β βπ β (0...π)(πβπ) = 0)) |
187 | 184, 186 | mpd 15 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ β (0...π)(πβπ) = 0) |
188 | 121, 142 | fmptd 7068 |
. . . . . . . . . . . . . . . . 17
β’ (π β π:(0...π)βΆβ) |
189 | | ffn 6674 |
. . . . . . . . . . . . . . . . 17
β’ (π:(0...π)βΆβ β π Fn (0...π)) |
190 | | fvelrnb 6909 |
. . . . . . . . . . . . . . . . 17
β’ (π Fn (0...π) β (0 β ran π β βπ β (0...π)(πβπ) = 0)) |
191 | 188, 189,
190 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (π β (0 β ran π β βπ β (0...π)(πβπ) = 0)) |
192 | 187, 191 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ (π β 0 β ran π) |
193 | 192 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π = 0) β 0 β ran π) |
194 | 179, 193 | eqeltrd 2833 |
. . . . . . . . . . . . 13
β’ ((π β§ π = 0) β π β ran π) |
195 | 175, 176,
178, 194 | fourierdlem12 44462 |
. . . . . . . . . . . 12
β’ (((π β§ π = 0) β§ π β (0..^π)) β Β¬ π β ((πβπ)(,)(πβ(π + 1)))) |
196 | 195 | an32s 651 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π = 0) β Β¬ π β ((πβπ)(,)(πβ(π + 1)))) |
197 | 196 | adantlr 714 |
. . . . . . . . . 10
β’ ((((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β§ π = 0) β Β¬ π β ((πβπ)(,)(πβ(π + 1)))) |
198 | 174, 197 | pm2.65da 816 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β Β¬ π = 0) |
199 | 198 | adantlr 714 |
. . . . . . . 8
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β Β¬ π = 0) |
200 | 199 | iffalsed 4503 |
. . . . . . 7
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) = (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) |
201 | 160 | eqcomd 2738 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β 0 = (πβπ)) |
202 | 201 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β 0 = (πβπ)) |
203 | | elioo3g 13304 |
. . . . . . . . . . . . . 14
β’ (π β ((πβπ)(,)(πβ(π + 1))) β (((πβπ) β β* β§ (πβ(π + 1)) β β* β§ π β β*)
β§ ((πβπ) < π β§ π < (πβ(π + 1))))) |
204 | 203 | biimpi 215 |
. . . . . . . . . . . . 13
β’ (π β ((πβπ)(,)(πβ(π + 1))) β (((πβπ) β β* β§ (πβ(π + 1)) β β* β§ π β β*)
β§ ((πβπ) < π β§ π < (πβ(π + 1))))) |
205 | 204 | simprld 771 |
. . . . . . . . . . . 12
β’ (π β ((πβπ)(,)(πβ(π + 1))) β (πβπ) < π ) |
206 | 205 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < π ) |
207 | 202, 206 | eqbrtrd 5133 |
. . . . . . . . . 10
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β 0 < π ) |
208 | 207 | iftrued 4500 |
. . . . . . . . 9
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β if(0 < π , π, π) = π) |
209 | 208 | oveq2d 7379 |
. . . . . . . 8
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((πΉβ(π + π )) β if(0 < π , π, π)) = ((πΉβ(π + π )) β π)) |
210 | 209 | oveq1d 7378 |
. . . . . . 7
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (((πΉβ(π + π )) β if(0 < π , π, π)) / π ) = (((πΉβ(π + π )) β π) / π )) |
211 | 1 | rexrd 11215 |
. . . . . . . . . . . . 13
β’ (π β π β
β*) |
212 | 211 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β
β*) |
213 | 36 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
214 | 169 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
215 | | elioore 13305 |
. . . . . . . . . . . . . 14
β’ (π β ((πβπ)(,)(πβ(π + 1))) β π β β) |
216 | 215 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
217 | 214, 216 | readdcld 11194 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β β) |
218 | 216, 207 | elrpd 12964 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β+) |
219 | 214, 218 | ltaddrpd 13000 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π < (π + π )) |
220 | 215 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
221 | 188 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆβ) |
222 | 221, 14 | ffvelcdmd 7042 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
223 | 222 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β β) |
224 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
225 | 204 | simprrd 773 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πβπ)(,)(πβ(π + 1))) β π < (πβ(π + 1))) |
226 | 225 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π < (πβ(π + 1))) |
227 | 220, 223,
224, 226 | ltadd2dd 11324 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) < (π + (πβ(π + 1)))) |
228 | 171 | oveq2d 7379 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (π + (πβ(π + 1))) = (π + ((πβ(π + 1)) β π))) |
229 | 123 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β π β β) |
230 | 15 | recnd 11193 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
231 | 229, 230 | pncan3d 11525 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (π + ((πβ(π + 1)) β π)) = (πβ(π + 1))) |
232 | 228, 231 | eqtrd 2772 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π + (πβ(π + 1))) = (πβ(π + 1))) |
233 | 232 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + (πβ(π + 1))) = (πβ(π + 1))) |
234 | 227, 233 | breqtrd 5137 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) < (πβ(π + 1))) |
235 | 234 | adantlr 714 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) < (πβ(π + 1))) |
236 | 212, 213,
217, 219, 235 | eliood 43838 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β (π(,)(πβ(π + 1)))) |
237 | | fvres 6867 |
. . . . . . . . . . 11
β’ ((π + π ) β (π(,)(πβ(π + 1))) β ((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π )) = (πΉβ(π + π ))) |
238 | 236, 237 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π )) = (πΉβ(π + π ))) |
239 | 238 | eqcomd 2738 |
. . . . . . . . 9
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) = ((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π ))) |
240 | 239 | oveq1d 7378 |
. . . . . . . 8
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((πΉβ(π + π )) β π) = (((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π )) β π)) |
241 | 240 | oveq1d 7378 |
. . . . . . 7
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (((πΉβ(π + π )) β π) / π ) = ((((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π )) β π) / π )) |
242 | 200, 210,
241 | 3eqtrd 2776 |
. . . . . 6
β’ ((((π β§ π β (0..^π)) β§ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) = ((((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π )) β π) / π )) |
243 | 173, 242 | mpteq12dva 5200 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) = (π β (0(,)((πβ(π + 1)) β π)) β¦ ((((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π )) β π) / π ))) |
244 | 101, 149,
243 | 3eqtrd 2776 |
. . . 4
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β (π» βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β (0(,)((πβ(π + 1)) β π)) β¦ ((((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π )) β π) / π ))) |
245 | 244, 160 | oveq12d 7381 |
. . 3
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β ((π» βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((π β (0(,)((πβ(π + 1)) β π)) β¦ ((((πΉ βΎ (π(,)(πβ(π + 1))))β(π + π )) β π) / π )) limβ 0)) |
246 | 94, 98, 245 | 3eltr4d 2848 |
. 2
β’ (((π β§ π β (0..^π)) β§ (πβπ) = π) β π΄ β ((π» βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
247 | | eqid 2732 |
. . . . 5
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) |
248 | | eqid 2732 |
. . . . 5
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ π ) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ π ) |
249 | | eqid 2732 |
. . . . 5
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) |
250 | 24 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β πΉ:ββΆβ) |
251 | 1 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
252 | 215 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
253 | 251, 252 | readdcld 11194 |
. . . . . . . . . 10
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β β) |
254 | 250, 253 | ffvelcdmd 7042 |
. . . . . . . . 9
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) β β) |
255 | 254 | recnd 11193 |
. . . . . . . 8
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) β β) |
256 | 255 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) β β) |
257 | 256 | 3adantl3 1169 |
. . . . . 6
β’ (((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) β β) |
258 | | limccl 25277 |
. . . . . . . . . 10
β’ ((πΉ βΎ (π(,)+β)) limβ π) β
β |
259 | 258, 31 | sselid 3946 |
. . . . . . . . 9
β’ (π β π β β) |
260 | | fourierdlem75.w |
. . . . . . . . . 10
β’ (π β π β β) |
261 | 260 | recnd 11193 |
. . . . . . . . 9
β’ (π β π β β) |
262 | 259, 261 | ifcld 4538 |
. . . . . . . 8
β’ (π β if(0 < π , π, π) β β) |
263 | 262 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β if(0 < π , π, π) β β) |
264 | 263 | 3ad2antl1 1186 |
. . . . . 6
β’ (((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β if(0 < π , π, π) β β) |
265 | 257, 264 | subcld 11522 |
. . . . 5
β’ (((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((πΉβ(π + π )) β if(0 < π , π, π)) β β) |
266 | 215 | recnd 11193 |
. . . . . . 7
β’ (π β ((πβπ)(,)(πβ(π + 1))) β π β β) |
267 | 266 | adantl 483 |
. . . . . 6
β’ (((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
268 | | velsn 4608 |
. . . . . . . 8
β’ (π β {0} β π = 0) |
269 | 198, 268 | sylnibr 329 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β Β¬ π β {0}) |
270 | 269 | 3adantl3 1169 |
. . . . . 6
β’ (((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β Β¬ π β {0}) |
271 | 267, 270 | eldifd 3925 |
. . . . 5
β’ (((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β (β β
{0})) |
272 | | eqid 2732 |
. . . . . . . . . 10
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) |
273 | | eqid 2732 |
. . . . . . . . . 10
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ π) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ π) |
274 | | eqid 2732 |
. . . . . . . . . 10
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β π)) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β π)) |
275 | 261 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
276 | | ioossre 13336 |
. . . . . . . . . . . 12
β’ ((πβπ)(,)(πβ(π + 1))) β β |
277 | 276 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β β) |
278 | 150, 119 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
279 | 278 | rexrd 11215 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβπ) β
β*) |
280 | 279 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β
β*) |
281 | 36 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
282 | 253 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β β) |
283 | | iccssre 13357 |
. . . . . . . . . . . . . . . . . . 19
β’ ((-Ο
β β β§ Ο β β) β (-Ο[,]Ο) β
β) |
284 | 104, 103,
283 | mp2an 691 |
. . . . . . . . . . . . . . . . . 18
β’
(-Ο[,]Ο) β β |
285 | 284, 46 | sstri 3957 |
. . . . . . . . . . . . . . . . 17
β’
(-Ο[,]Ο) β β |
286 | 153, 141 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0...π)) β (πβπ) β (-Ο[,]Ο)) |
287 | 150, 286 | sylan2 594 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β (πβπ) β (-Ο[,]Ο)) |
288 | 285, 287 | sselid 3946 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
289 | 229, 288 | addcomd 11367 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π + (πβπ)) = ((πβπ) + π)) |
290 | 150 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
291 | 150, 121 | sylan2 594 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β ((πβπ) β π) β β) |
292 | 142 | fvmpt2 6965 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (0...π) β§ ((πβπ) β π) β β) β (πβπ) = ((πβπ) β π)) |
293 | 290, 291,
292 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (πβπ) = ((πβπ) β π)) |
294 | 293 | oveq1d 7378 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β ((πβπ) + π) = (((πβπ) β π) + π)) |
295 | 278 | recnd 11193 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
296 | 295, 229 | npcand 11526 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (((πβπ) β π) + π) = (πβπ)) |
297 | 289, 294,
296 | 3eqtrrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβπ) = (π + (πβπ))) |
298 | 297 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) = (π + (πβπ))) |
299 | 293, 291 | eqeltrd 2833 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
300 | 299 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β β) |
301 | 205 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < π ) |
302 | 300, 220,
224, 301 | ltadd2dd 11324 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + (πβπ)) < (π + π )) |
303 | 298, 302 | eqbrtrd 5133 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < (π + π )) |
304 | 280, 281,
282, 303, 234 | eliood 43838 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β ((πβπ)(,)(πβ(π + 1)))) |
305 | | ioossre 13336 |
. . . . . . . . . . . 12
β’ ((πβπ)(,)(πβ(π + 1))) β β |
306 | 305 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β β) |
307 | 300, 301 | gtned 11300 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β (πβπ)) |
308 | | fourierdlem75.r |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
309 | 297 | oveq2d 7379 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (π + (πβπ)))) |
310 | 308, 309 | eleqtrd 2835 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (π + (πβπ)))) |
311 | 25, 169, 277, 272, 304, 306, 307, 310, 288 | fourierdlem53 44502 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π
β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) limβ (πβπ))) |
312 | | ioosscn 13337 |
. . . . . . . . . . . 12
β’ ((πβπ)(,)(πβ(π + 1))) β β |
313 | 312 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β β) |
314 | 261 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β π β β) |
315 | 273, 313,
314, 288 | constlimc 43967 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ π) limβ (πβπ))) |
316 | 272, 273,
274, 256, 275, 311, 315 | sublimc 43995 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (π
β π) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β π)) limβ (πβπ))) |
317 | 316 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ (πβπ) < π) β (π
β π) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β π)) limβ (πβπ))) |
318 | | iftrue 4498 |
. . . . . . . . . 10
β’ ((πβπ) < π β if((πβπ) < π, π, π) = π) |
319 | 318 | oveq2d 7379 |
. . . . . . . . 9
β’ ((πβπ) < π β (π
β if((πβπ) < π, π, π)) = (π
β π)) |
320 | 319 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ (πβπ) < π) β (π
β if((πβπ) < π, π, π)) = (π
β π)) |
321 | 215 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
322 | | 0red 11168 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β 0 β
β) |
323 | 222 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β β) |
324 | 225 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π < (πβ(π + 1))) |
325 | 171 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ (πβπ) < π) β (πβ(π + 1)) = ((πβ(π + 1)) β π)) |
326 | 279 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ Β¬ (πβ(π + 1)) β€ π) β (πβπ) β
β*) |
327 | 36 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ Β¬ (πβ(π + 1)) β€ π) β (πβ(π + 1)) β
β*) |
328 | 169 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ Β¬ (πβ(π + 1)) β€ π) β π β β) |
329 | | simplr 768 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ Β¬ (πβ(π + 1)) β€ π) β (πβπ) < π) |
330 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβ(π + 1)) β€ π) β Β¬ (πβ(π + 1)) β€ π) |
331 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβ(π + 1)) β€ π) β π β β) |
332 | 15 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβ(π + 1)) β€ π) β (πβ(π + 1)) β β) |
333 | 331, 332 | ltnled 11312 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβ(π + 1)) β€ π) β (π < (πβ(π + 1)) β Β¬ (πβ(π + 1)) β€ π)) |
334 | 330, 333 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβ(π + 1)) β€ π) β π < (πβ(π + 1))) |
335 | 334 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ Β¬ (πβ(π + 1)) β€ π) β π < (πβ(π + 1))) |
336 | 326, 327,
328, 329, 335 | eliood 43838 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ Β¬ (πβ(π + 1)) β€ π) β π β ((πβπ)(,)(πβ(π + 1)))) |
337 | 5, 4, 3, 180 | fourierdlem12 44462 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0..^π)) β Β¬ π β ((πβπ)(,)(πβ(π + 1)))) |
338 | 337 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ Β¬ (πβ(π + 1)) β€ π) β Β¬ π β ((πβπ)(,)(πβ(π + 1)))) |
339 | 336, 338 | condan 817 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ (πβπ) < π) β (πβ(π + 1)) β€ π) |
340 | 15 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ (πβπ) < π) β (πβ(π + 1)) β β) |
341 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ (πβπ) < π) β π β β) |
342 | 340, 341 | suble0d 11756 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ (πβπ) < π) β (((πβ(π + 1)) β π) β€ 0 β (πβ(π + 1)) β€ π)) |
343 | 339, 342 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ (πβπ) < π) β ((πβ(π + 1)) β π) β€ 0) |
344 | 325, 343 | eqbrtrd 5133 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ (πβπ) < π) β (πβ(π + 1)) β€ 0) |
345 | 344 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β€ 0) |
346 | 321, 323,
322, 324, 345 | ltletrd 11325 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π < 0) |
347 | 321, 322,
346 | ltnsymd 11314 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β Β¬ 0 < π ) |
348 | 347 | iffalsed 4503 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β if(0 < π , π, π) = π) |
349 | 348 | oveq2d 7379 |
. . . . . . . . . 10
β’ ((((π β§ π β (0..^π)) β§ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((πΉβ(π + π )) β if(0 < π , π, π)) = ((πΉβ(π + π )) β π)) |
350 | 349 | mpteq2dva 5211 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ (πβπ) < π) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β π))) |
351 | 350 | oveq1d 7378 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ (πβπ) < π) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) limβ (πβπ)) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β π)) limβ (πβπ))) |
352 | 317, 320,
351 | 3eltr4d 2848 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ (πβπ) < π) β (π
β if((πβπ) < π, π, π)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) limβ (πβπ))) |
353 | 352 | 3adantl3 1169 |
. . . . . 6
β’ (((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β§ (πβπ) < π) β (π
β if((πβπ) < π, π, π)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) limβ (πβπ))) |
354 | | eqid 2732 |
. . . . . . . . . 10
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ π) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ π) |
355 | | eqid 2732 |
. . . . . . . . . 10
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β π)) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β π)) |
356 | 259 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
357 | 259 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β π β β) |
358 | 354, 313,
357, 288 | constlimc 43967 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ π) limβ (πβπ))) |
359 | 272, 354,
355, 256, 356, 311, 358 | sublimc 43995 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (π
β π) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β π)) limβ (πβπ))) |
360 | 359 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β (π
β π) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β π)) limβ (πβπ))) |
361 | | iffalse 4501 |
. . . . . . . . . 10
β’ (Β¬
(πβπ) < π β if((πβπ) < π, π, π) = π) |
362 | 361 | oveq2d 7379 |
. . . . . . . . 9
β’ (Β¬
(πβπ) < π β (π
β if((πβπ) < π, π, π)) = (π
β π)) |
363 | 362 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β (π
β if((πβπ) < π, π, π)) = (π
β π)) |
364 | | 0red 11168 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β 0 β
β) |
365 | 299 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β β) |
366 | 215 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
367 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β π β β) |
368 | 278 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β (πβπ) β β) |
369 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β Β¬ (πβπ) < π) |
370 | 367, 368,
369 | nltled 11315 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β π β€ (πβπ)) |
371 | 368, 367 | subge0d 11755 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β (0 β€ ((πβπ) β π) β π β€ (πβπ))) |
372 | 370, 371 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β 0 β€ ((πβπ) β π)) |
373 | 293 | eqcomd 2738 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β ((πβπ) β π) = (πβπ)) |
374 | 373 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β ((πβπ) β π) = (πβπ)) |
375 | 372, 374 | breqtrd 5137 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β 0 β€ (πβπ)) |
376 | 375 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β 0 β€ (πβπ)) |
377 | 205 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < π ) |
378 | 364, 365,
366, 376, 377 | lelttrd 11323 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β 0 < π ) |
379 | 378 | iftrued 4500 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β if(0 < π , π, π) = π) |
380 | 379 | oveq2d 7379 |
. . . . . . . . . 10
β’ ((((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((πΉβ(π + π )) β if(0 < π , π, π)) = ((πΉβ(π + π )) β π)) |
381 | 380 | mpteq2dva 5211 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β π))) |
382 | 381 | oveq1d 7378 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) limβ (πβπ)) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β π)) limβ (πβπ))) |
383 | 360, 363,
382 | 3eltr4d 2848 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβπ) < π) β (π
β if((πβπ) < π, π, π)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) limβ (πβπ))) |
384 | 383 | 3adantl3 1169 |
. . . . . 6
β’ (((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β§ Β¬ (πβπ) < π) β (π
β if((πβπ) < π, π, π)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) limβ (πβπ))) |
385 | 353, 384 | pm2.61dan 812 |
. . . . 5
β’ ((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β (π
β if((πβπ) < π, π, π)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β if(0 < π , π, π))) limβ (πβπ))) |
386 | 313, 248,
288 | idlimc 43969 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (πβπ) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ π ) limβ (πβπ))) |
387 | 386 | 3adant3 1133 |
. . . . 5
β’ ((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β (πβπ) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ π ) limβ (πβπ))) |
388 | 293 | 3adant3 1133 |
. . . . . 6
β’ ((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β (πβπ) = ((πβπ) β π)) |
389 | 295 | 3adant3 1133 |
. . . . . . 7
β’ ((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β (πβπ) β β) |
390 | 229 | 3adant3 1133 |
. . . . . . 7
β’ ((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β π β β) |
391 | | neqne 2948 |
. . . . . . . 8
β’ (Β¬
(πβπ) = π β (πβπ) β π) |
392 | 391 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β (πβπ) β π) |
393 | 389, 390,
392 | subne0d 11531 |
. . . . . 6
β’ ((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β ((πβπ) β π) β 0) |
394 | 388, 393 | eqnetrd 3008 |
. . . . 5
β’ ((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β (πβπ) β 0) |
395 | 198 | 3adantl3 1169 |
. . . . . 6
β’ (((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β Β¬ π = 0) |
396 | 395 | neqned 2947 |
. . . . 5
β’ (((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β 0) |
397 | 247, 248,
249, 265, 271, 385, 387, 394, 396 | divlimc 43999 |
. . . 4
β’ ((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β ((π
β if((πβπ) < π, π, π)) / (πβπ)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) limβ (πβπ))) |
398 | | iffalse 4501 |
. . . . . 6
β’ (Β¬
(πβπ) = π β if((πβπ) = π, πΈ, ((π
β if((πβπ) < π, π, π)) / (πβπ))) = ((π
β if((πβπ) < π, π, π)) / (πβπ))) |
399 | 95, 398 | eqtrid 2784 |
. . . . 5
β’ (Β¬
(πβπ) = π β π΄ = ((π
β if((πβπ) < π, π, π)) / (πβπ))) |
400 | 399 | 3ad2ant3 1136 |
. . . 4
β’ ((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β π΄ = ((π
β if((πβπ) < π, π, π)) / (πβπ))) |
401 | | ioossre 13336 |
. . . . . . . . . . . . 13
β’ (π(,)+β) β
β |
402 | 401 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (π(,)+β) β
β) |
403 | 24, 402 | fssresd 6715 |
. . . . . . . . . . 11
β’ (π β (πΉ βΎ (π(,)+β)):(π(,)+β)βΆβ) |
404 | 401, 47 | sstrid 3959 |
. . . . . . . . . . 11
β’ (π β (π(,)+β) β
β) |
405 | 34 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β +β β
β*) |
406 | 1 | ltpnfd 13052 |
. . . . . . . . . . . 12
β’ (π β π < +β) |
407 | 52, 405, 1, 406 | lptioo1cn 43989 |
. . . . . . . . . . 11
β’ (π β π β
((limPtβ(TopOpenββfld))β(π(,)+β))) |
408 | 403, 404,
407, 31 | limcrecl 43972 |
. . . . . . . . . 10
β’ (π β π β β) |
409 | 24, 1, 408, 260, 99 | fourierdlem9 44459 |
. . . . . . . . 9
β’ (π β π»:(-Ο[,]Ο)βΆβ) |
410 | 409 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β π»:(-Ο[,]Ο)βΆβ) |
411 | 410, 147 | feqresmpt 6917 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (π» βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π»βπ ))) |
412 | 147 | sselda 3948 |
. . . . . . . . . 10
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β (-Ο[,]Ο)) |
413 | | 0cnd 11158 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β 0 β
β) |
414 | 262 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β if(0 < π , π, π) β β) |
415 | 256, 414 | subcld 11522 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((πΉβ(π + π )) β if(0 < π , π, π)) β β) |
416 | 266 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
417 | 198 | neqned 2947 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β 0) |
418 | 415, 416,
417 | divcld 11941 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (((πΉβ(π + π )) β if(0 < π , π, π)) / π ) β β) |
419 | 413, 418 | ifcld 4538 |
. . . . . . . . . 10
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) β β) |
420 | 99 | fvmpt2 6965 |
. . . . . . . . . 10
β’ ((π β (-Ο[,]Ο) β§
if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) β β) β (π»βπ ) = if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) |
421 | 412, 419,
420 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π»βπ ) = if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) |
422 | 198 | iffalsed 4503 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β if(π = 0, 0, (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) = (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) |
423 | 421, 422 | eqtrd 2772 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π»βπ ) = (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) |
424 | 423 | mpteq2dva 5211 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π»βπ )) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) |
425 | 411, 424 | eqtrd 2772 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (π» βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) |
426 | 425 | 3adant3 1133 |
. . . . 5
β’ ((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β (π» βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (((πΉβ(π + π )) β if(0 < π , π, π)) / π ))) |
427 | 426 | oveq1d 7378 |
. . . 4
β’ ((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β ((π» βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (((πΉβ(π + π )) β if(0 < π , π, π)) / π )) limβ (πβπ))) |
428 | 397, 400,
427 | 3eltr4d 2848 |
. . 3
β’ ((π β§ π β (0..^π) β§ Β¬ (πβπ) = π) β π΄ β ((π» βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
429 | 428 | 3expa 1119 |
. 2
β’ (((π β§ π β (0..^π)) β§ Β¬ (πβπ) = π) β π΄ β ((π» βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
430 | 246, 429 | pm2.61dan 812 |
1
β’ ((π β§ π β (0..^π)) β π΄ β ((π» βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |