Step | Hyp | Ref
| Expression |
1 | | fourierdlem90.p |
. . . . . . 7
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
2 | | fourierdlem90.m |
. . . . . . 7
β’ (π β π β β) |
3 | | fourierdlem90.q |
. . . . . . 7
β’ (π β π β (πβπ)) |
4 | 1, 2, 3 | fourierdlem11 44449 |
. . . . . 6
β’ (π β (π΄ β β β§ π΅ β β β§ π΄ < π΅)) |
5 | 4 | simp1d 1143 |
. . . . 5
β’ (π β π΄ β β) |
6 | 4 | simp2d 1144 |
. . . . 5
β’ (π β π΅ β β) |
7 | 5, 6 | iccssred 13360 |
. . . 4
β’ (π β (π΄[,]π΅) β β) |
8 | 4 | simp3d 1145 |
. . . . . 6
β’ (π β π΄ < π΅) |
9 | | fourierdlem90.J |
. . . . . 6
β’ πΏ = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) |
10 | 5, 6, 8, 9 | fourierdlem17 44455 |
. . . . 5
β’ (π β πΏ:(π΄(,]π΅)βΆ(π΄[,]π΅)) |
11 | | fourierdlem90.t |
. . . . . . 7
β’ π = (π΅ β π΄) |
12 | | fourierdlem90.e |
. . . . . . 7
β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
13 | 5, 6, 8, 11, 12 | fourierdlem4 44442 |
. . . . . 6
β’ (π β πΈ:ββΆ(π΄(,]π΅)) |
14 | | fourierdlem90.c |
. . . . . . . . . . . . 13
β’ (π β πΆ β β) |
15 | | fourierdlem90.d |
. . . . . . . . . . . . . 14
β’ (π β π· β (πΆ(,)+β)) |
16 | | elioore 13303 |
. . . . . . . . . . . . . 14
β’ (π· β (πΆ(,)+β) β π· β β) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π· β β) |
18 | | elioo4g 13333 |
. . . . . . . . . . . . . . . 16
β’ (π· β (πΆ(,)+β) β ((πΆ β β* β§ +β
β β* β§ π· β β) β§ (πΆ < π· β§ π· < +β))) |
19 | 15, 18 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (π β ((πΆ β β* β§ +β
β β* β§ π· β β) β§ (πΆ < π· β§ π· < +β))) |
20 | 19 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β (πΆ < π· β§ π· < +β)) |
21 | 20 | simpld 496 |
. . . . . . . . . . . . 13
β’ (π β πΆ < π·) |
22 | | fourierdlem90.o |
. . . . . . . . . . . . 13
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
23 | | fourierdlem90.h |
. . . . . . . . . . . . 13
β’ π» = ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) |
24 | | fourierdlem90.n |
. . . . . . . . . . . . 13
β’ π = ((β―βπ») β 1) |
25 | | fourierdlem90.s |
. . . . . . . . . . . . 13
β’ π = (β©ππ Isom < , < ((0...π), π»)) |
26 | 11, 1, 2, 3, 14, 17, 21, 22, 23, 24, 25 | fourierdlem54 44491 |
. . . . . . . . . . . 12
β’ (π β ((π β β β§ π β (πβπ)) β§ π Isom < , < ((0...π), π»))) |
27 | 26 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (π β β β§ π β (πβπ))) |
28 | 27 | simprd 497 |
. . . . . . . . . 10
β’ (π β π β (πβπ)) |
29 | 27 | simpld 496 |
. . . . . . . . . . 11
β’ (π β π β β) |
30 | 22 | fourierdlem2 44440 |
. . . . . . . . . . 11
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
31 | 29, 30 | syl 17 |
. . . . . . . . . 10
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
32 | 28, 31 | mpbid 231 |
. . . . . . . . 9
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
33 | 32 | simpld 496 |
. . . . . . . 8
β’ (π β π β (β βm
(0...π))) |
34 | | elmapi 8793 |
. . . . . . . 8
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
35 | 33, 34 | syl 17 |
. . . . . . 7
β’ (π β π:(0...π)βΆβ) |
36 | | fourierdlem90.17 |
. . . . . . . 8
β’ (π β π½ β (0..^π)) |
37 | | elfzofz 13597 |
. . . . . . . 8
β’ (π½ β (0..^π) β π½ β (0...π)) |
38 | 36, 37 | syl 17 |
. . . . . . 7
β’ (π β π½ β (0...π)) |
39 | 35, 38 | ffvelcdmd 7040 |
. . . . . 6
β’ (π β (πβπ½) β β) |
40 | 13, 39 | ffvelcdmd 7040 |
. . . . 5
β’ (π β (πΈβ(πβπ½)) β (π΄(,]π΅)) |
41 | 10, 40 | ffvelcdmd 7040 |
. . . 4
β’ (π β (πΏβ(πΈβ(πβπ½))) β (π΄[,]π΅)) |
42 | 7, 41 | sseldd 3949 |
. . 3
β’ (π β (πΏβ(πΈβ(πβπ½))) β β) |
43 | 5 | rexrd 11213 |
. . . . 5
β’ (π β π΄ β
β*) |
44 | | iocssre 13353 |
. . . . 5
β’ ((π΄ β β*
β§ π΅ β β)
β (π΄(,]π΅) β
β) |
45 | 43, 6, 44 | syl2anc 585 |
. . . 4
β’ (π β (π΄(,]π΅) β β) |
46 | | fzofzp1 13678 |
. . . . . . 7
β’ (π½ β (0..^π) β (π½ + 1) β (0...π)) |
47 | 36, 46 | syl 17 |
. . . . . 6
β’ (π β (π½ + 1) β (0...π)) |
48 | 35, 47 | ffvelcdmd 7040 |
. . . . 5
β’ (π β (πβ(π½ + 1)) β β) |
49 | 13, 48 | ffvelcdmd 7040 |
. . . 4
β’ (π β (πΈβ(πβ(π½ + 1))) β (π΄(,]π΅)) |
50 | 45, 49 | sseldd 3949 |
. . 3
β’ (π β (πΈβ(πβ(π½ + 1))) β β) |
51 | | eqid 2733 |
. . 3
β’ ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) = ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) |
52 | | fourierdlem90.u |
. . . 4
β’ π = ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))) |
53 | 48, 50 | resubcld 11591 |
. . . 4
β’ (π β ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))) β β) |
54 | 52, 53 | eqeltrid 2838 |
. . 3
β’ (π β π β β) |
55 | | eqid 2733 |
. . 3
β’ (((πΏβ(πΈβ(πβπ½))) + π)(,)((πΈβ(πβ(π½ + 1))) + π)) = (((πΏβ(πΈβ(πβπ½))) + π)(,)((πΈβ(πβ(π½ + 1))) + π)) |
56 | | fourierdlem90.g |
. . . 4
β’ πΊ = (πΉ βΎ ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) |
57 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π = π½ β (π β (0..^π) β π½ β (0..^π))) |
58 | 57 | anbi2d 630 |
. . . . . . . . . . 11
β’ (π = π½ β ((π β§ π β (0..^π)) β (π β§ π½ β (0..^π)))) |
59 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π = π½ β (πβπ) = (πβπ½)) |
60 | 59 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’ (π = π½ β (πΈβ(πβπ)) = (πΈβ(πβπ½))) |
61 | 60 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (π = π½ β (πΏβ(πΈβ(πβπ))) = (πΏβ(πΈβ(πβπ½)))) |
62 | | oveq1 7368 |
. . . . . . . . . . . . . . 15
β’ (π = π½ β (π + 1) = (π½ + 1)) |
63 | 62 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’ (π = π½ β (πβ(π + 1)) = (πβ(π½ + 1))) |
64 | 63 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (π = π½ β (πΈβ(πβ(π + 1))) = (πΈβ(πβ(π½ + 1)))) |
65 | 61, 64 | oveq12d 7379 |
. . . . . . . . . . . 12
β’ (π = π½ β ((πΏβ(πΈβ(πβπ)))(,)(πΈβ(πβ(π + 1)))) = ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) |
66 | 59 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’ (π = π½ β (πΌβ(πβπ)) = (πΌβ(πβπ½))) |
67 | 66 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (π = π½ β (πβ(πΌβ(πβπ))) = (πβ(πΌβ(πβπ½)))) |
68 | 66 | oveq1d 7376 |
. . . . . . . . . . . . . 14
β’ (π = π½ β ((πΌβ(πβπ)) + 1) = ((πΌβ(πβπ½)) + 1)) |
69 | 68 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (π = π½ β (πβ((πΌβ(πβπ)) + 1)) = (πβ((πΌβ(πβπ½)) + 1))) |
70 | 67, 69 | oveq12d 7379 |
. . . . . . . . . . . 12
β’ (π = π½ β ((πβ(πΌβ(πβπ)))(,)(πβ((πΌβ(πβπ)) + 1))) = ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) |
71 | 65, 70 | sseq12d 3981 |
. . . . . . . . . . 11
β’ (π = π½ β (((πΏβ(πΈβ(πβπ)))(,)(πΈβ(πβ(π + 1)))) β ((πβ(πΌβ(πβπ)))(,)(πβ((πΌβ(πβπ)) + 1))) β ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))) |
72 | 58, 71 | imbi12d 345 |
. . . . . . . . . 10
β’ (π = π½ β (((π β§ π β (0..^π)) β ((πΏβ(πΈβ(πβπ)))(,)(πΈβ(πβ(π + 1)))) β ((πβ(πΌβ(πβπ)))(,)(πβ((πΌβ(πβπ)) + 1)))) β ((π β§ π½ β (0..^π)) β ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))))) |
73 | 11 | oveq2i 7372 |
. . . . . . . . . . . . . . . . . . 19
β’ (π Β· π) = (π Β· (π΅ β π΄)) |
74 | 73 | oveq2i 7372 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ + (π Β· π)) = (π¦ + (π Β· (π΅ β π΄))) |
75 | 74 | eleq1i 2825 |
. . . . . . . . . . . . . . . . 17
β’ ((π¦ + (π Β· π)) β ran π β (π¦ + (π Β· (π΅ β π΄))) β ran π) |
76 | 75 | rexbii 3094 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
β€ (π¦ + (π Β· π)) β ran π β βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π) |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (πΆ[,]π·) β (βπ β β€ (π¦ + (π Β· π)) β ran π β βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π)) |
78 | 77 | rabbiia 3410 |
. . . . . . . . . . . . . 14
β’ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π} = {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π} |
79 | 78 | uneq2i 4124 |
. . . . . . . . . . . . 13
β’ ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) = ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π}) |
80 | 23, 79 | eqtri 2761 |
. . . . . . . . . . . 12
β’ π» = ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π}) |
81 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π₯ β π¦ = π₯) |
82 | 11 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΅ β π΄) = π |
83 | 82 | oveq2i 7372 |
. . . . . . . . . . . . . . . . . 18
β’ (π Β· (π΅ β π΄)) = (π Β· π) |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π₯ β (π Β· (π΅ β π΄)) = (π Β· π)) |
85 | 81, 84 | oveq12d 7379 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π₯ β (π¦ + (π Β· (π΅ β π΄))) = (π₯ + (π Β· π))) |
86 | 85 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π₯ β ((π¦ + (π Β· (π΅ β π΄))) β ran π β (π₯ + (π Β· π)) β ran π)) |
87 | 86 | rexbidv 3172 |
. . . . . . . . . . . . . 14
β’ (π¦ = π₯ β (βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π β βπ β β€ (π₯ + (π Β· π)) β ran π)) |
88 | 87 | cbvrabv 3416 |
. . . . . . . . . . . . 13
β’ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π} = {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π} |
89 | 88 | uneq2i 4124 |
. . . . . . . . . . . 12
β’ ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π}) = ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) |
90 | 80, 89 | eqtri 2761 |
. . . . . . . . . . 11
β’ π» = ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) |
91 | | eqid 2733 |
. . . . . . . . . . 11
β’ ((πβπ) + if(((πβ(π + 1)) β (πβπ)) < ((πβ1) β π΄), (((πβ(π + 1)) β (πβπ)) / 2), (((πβ1) β π΄) / 2))) = ((πβπ) + if(((πβ(π + 1)) β (πβπ)) < ((πβ1) β π΄), (((πβ(π + 1)) β (πβπ)) / 2), (((πβ1) β π΄) / 2))) |
92 | | fourierdlem90.i |
. . . . . . . . . . 11
β’ πΌ = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ (πΏβ(πΈβπ₯))}, β, < )) |
93 | 11, 1, 2, 3, 14, 17, 21, 22, 90, 24, 25, 12, 9, 91, 92 | fourierdlem79 44516 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β ((πΏβ(πΈβ(πβπ)))(,)(πΈβ(πβ(π + 1)))) β ((πβ(πΌβ(πβπ)))(,)(πβ((πΌβ(πβπ)) + 1)))) |
94 | 72, 93 | vtoclg 3527 |
. . . . . . . . 9
β’ (π½ β (0..^π) β ((π β§ π½ β (0..^π)) β ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))) |
95 | 94 | anabsi7 670 |
. . . . . . . 8
β’ ((π β§ π½ β (0..^π)) β ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) |
96 | 36, 95 | mpdan 686 |
. . . . . . 7
β’ (π β ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) |
97 | 96 | resabs1d 5972 |
. . . . . 6
β’ (π β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) βΎ ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) = (πΉ βΎ ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))))) |
98 | 97 | eqcomd 2739 |
. . . . 5
β’ (π β (πΉ βΎ ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) = ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) βΎ ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))))) |
99 | 1, 2, 3, 11, 12, 9, 92 | fourierdlem37 44475 |
. . . . . . . . 9
β’ (π β (πΌ:ββΆ(0..^π) β§ (π₯ β β β sup({π β (0..^π) β£ (πβπ) β€ (πΏβ(πΈβπ₯))}, β, < ) β {π β (0..^π) β£ (πβπ) β€ (πΏβ(πΈβπ₯))}))) |
100 | 99 | simpld 496 |
. . . . . . . 8
β’ (π β πΌ:ββΆ(0..^π)) |
101 | 100, 39 | ffvelcdmd 7040 |
. . . . . . 7
β’ (π β (πΌβ(πβπ½)) β (0..^π)) |
102 | 101 | ancli 550 |
. . . . . . 7
β’ (π β (π β§ (πΌβ(πβπ½)) β (0..^π))) |
103 | | eleq1 2822 |
. . . . . . . . . 10
β’ (π = (πΌβ(πβπ½)) β (π β (0..^π) β (πΌβ(πβπ½)) β (0..^π))) |
104 | 103 | anbi2d 630 |
. . . . . . . . 9
β’ (π = (πΌβ(πβπ½)) β ((π β§ π β (0..^π)) β (π β§ (πΌβ(πβπ½)) β (0..^π)))) |
105 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π = (πΌβ(πβπ½)) β (πβπ) = (πβ(πΌβ(πβπ½)))) |
106 | | oveq1 7368 |
. . . . . . . . . . . . 13
β’ (π = (πΌβ(πβπ½)) β (π + 1) = ((πΌβ(πβπ½)) + 1)) |
107 | 106 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ (π = (πΌβ(πβπ½)) β (πβ(π + 1)) = (πβ((πΌβ(πβπ½)) + 1))) |
108 | 105, 107 | oveq12d 7379 |
. . . . . . . . . . 11
β’ (π = (πΌβ(πβπ½)) β ((πβπ)(,)(πβ(π + 1))) = ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) |
109 | 108 | reseq2d 5941 |
. . . . . . . . . 10
β’ (π = (πΌβ(πβπ½)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = (πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))) |
110 | 108 | oveq1d 7376 |
. . . . . . . . . 10
β’ (π = (πΌβ(πβπ½)) β (((πβπ)(,)(πβ(π + 1)))βcnββ) = (((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))βcnββ)) |
111 | 109, 110 | eleq12d 2828 |
. . . . . . . . 9
β’ (π = (πΌβ(πβπ½)) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ) β (πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) β (((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))βcnββ))) |
112 | 104, 111 | imbi12d 345 |
. . . . . . . 8
β’ (π = (πΌβ(πβπ½)) β (((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) β ((π β§ (πΌβ(πβπ½)) β (0..^π)) β (πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) β (((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))βcnββ)))) |
113 | | fourierdlem90.fcn |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
114 | 112, 113 | vtoclg 3527 |
. . . . . . 7
β’ ((πΌβ(πβπ½)) β (0..^π) β ((π β§ (πΌβ(πβπ½)) β (0..^π)) β (πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) β (((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))βcnββ))) |
115 | 101, 102,
114 | sylc 65 |
. . . . . 6
β’ (π β (πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) β (((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))βcnββ)) |
116 | | rescncf 24283 |
. . . . . 6
β’ (((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))) β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) β (((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))βcnββ) β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) βΎ ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) β (((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))βcnββ))) |
117 | 96, 115, 116 | sylc 65 |
. . . . 5
β’ (π β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) βΎ ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) β (((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))βcnββ)) |
118 | 98, 117 | eqeltrd 2834 |
. . . 4
β’ (π β (πΉ βΎ ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) β (((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))βcnββ)) |
119 | 56, 118 | eqeltrid 2838 |
. . 3
β’ (π β πΊ β (((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))βcnββ)) |
120 | | fourierdlem90.r |
. . 3
β’ π
= (π¦ β (((πΏβ(πΈβ(πβπ½))) + π)(,)((πΈβ(πβ(π½ + 1))) + π)) β¦ (πΊβ(π¦ β π))) |
121 | 42, 50, 51, 54, 55, 119, 120 | cncfshiftioo 44223 |
. 2
β’ (π β π
β ((((πΏβ(πΈβ(πβπ½))) + π)(,)((πΈβ(πβ(π½ + 1))) + π))βcnββ)) |
122 | 120 | a1i 11 |
. . 3
β’ (π β π
= (π¦ β (((πΏβ(πΈβ(πβπ½))) + π)(,)((πΈβ(πβ(π½ + 1))) + π)) β¦ (πΊβ(π¦ β π)))) |
123 | 52 | oveq2i 7372 |
. . . . . . 7
β’ ((πΏβ(πΈβ(πβπ½))) + π) = ((πΏβ(πΈβ(πβπ½))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) |
124 | 123 | a1i 11 |
. . . . . 6
β’ (π β ((πΏβ(πΈβ(πβπ½))) + π) = ((πΏβ(πΈβ(πβπ½))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))))) |
125 | 64, 61 | oveq12d 7379 |
. . . . . . . . . . . . . 14
β’ (π = π½ β ((πΈβ(πβ(π + 1))) β (πΏβ(πΈβ(πβπ)))) = ((πΈβ(πβ(π½ + 1))) β (πΏβ(πΈβ(πβπ½))))) |
126 | 63, 59 | oveq12d 7379 |
. . . . . . . . . . . . . 14
β’ (π = π½ β ((πβ(π + 1)) β (πβπ)) = ((πβ(π½ + 1)) β (πβπ½))) |
127 | 125, 126 | eqeq12d 2749 |
. . . . . . . . . . . . 13
β’ (π = π½ β (((πΈβ(πβ(π + 1))) β (πΏβ(πΈβ(πβπ)))) = ((πβ(π + 1)) β (πβπ)) β ((πΈβ(πβ(π½ + 1))) β (πΏβ(πΈβ(πβπ½)))) = ((πβ(π½ + 1)) β (πβπ½)))) |
128 | 58, 127 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π = π½ β (((π β§ π β (0..^π)) β ((πΈβ(πβ(π + 1))) β (πΏβ(πΈβ(πβπ)))) = ((πβ(π + 1)) β (πβπ))) β ((π β§ π½ β (0..^π)) β ((πΈβ(πβ(π½ + 1))) β (πΏβ(πΈβ(πβπ½)))) = ((πβ(π½ + 1)) β (πβπ½))))) |
129 | 80 | fveq2i 6849 |
. . . . . . . . . . . . . . 15
β’
(β―βπ») =
(β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π})) |
130 | 129 | oveq1i 7371 |
. . . . . . . . . . . . . 14
β’
((β―βπ»)
β 1) = ((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π})) β 1) |
131 | 24, 130 | eqtri 2761 |
. . . . . . . . . . . . 13
β’ π = ((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π})) β 1) |
132 | | isoeq5 7270 |
. . . . . . . . . . . . . . . 16
β’ (π» = ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π}) β (π Isom < , < ((0...π), π») β π Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π})))) |
133 | 80, 132 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ (π Isom < , < ((0...π), π») β π Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π}))) |
134 | 133 | iotabii 6485 |
. . . . . . . . . . . . . 14
β’
(β©ππ Isom < , < ((0...π), π»)) = (β©ππ Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π}))) |
135 | 25, 134 | eqtri 2761 |
. . . . . . . . . . . . 13
β’ π = (β©ππ Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π}))) |
136 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ ((πβπ) + (π΅ β (πΈβ(πβπ)))) = ((πβπ) + (π΅ β (πΈβ(πβπ)))) |
137 | 1, 11, 2, 3, 14, 15, 22, 131, 135, 12, 9, 136 | fourierdlem65 44502 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β ((πΈβ(πβ(π + 1))) β (πΏβ(πΈβ(πβπ)))) = ((πβ(π + 1)) β (πβπ))) |
138 | 128, 137 | vtoclg 3527 |
. . . . . . . . . . 11
β’ (π½ β (0..^π) β ((π β§ π½ β (0..^π)) β ((πΈβ(πβ(π½ + 1))) β (πΏβ(πΈβ(πβπ½)))) = ((πβ(π½ + 1)) β (πβπ½)))) |
139 | 138 | anabsi7 670 |
. . . . . . . . . 10
β’ ((π β§ π½ β (0..^π)) β ((πΈβ(πβ(π½ + 1))) β (πΏβ(πΈβ(πβπ½)))) = ((πβ(π½ + 1)) β (πβπ½))) |
140 | 36, 139 | mpdan 686 |
. . . . . . . . 9
β’ (π β ((πΈβ(πβ(π½ + 1))) β (πΏβ(πΈβ(πβπ½)))) = ((πβ(π½ + 1)) β (πβπ½))) |
141 | 50 | recnd 11191 |
. . . . . . . . . 10
β’ (π β (πΈβ(πβ(π½ + 1))) β β) |
142 | 48 | recnd 11191 |
. . . . . . . . . . 11
β’ (π β (πβ(π½ + 1)) β β) |
143 | 14, 17 | iccssred 13360 |
. . . . . . . . . . . . 13
β’ (π β (πΆ[,]π·) β β) |
144 | | ax-resscn 11116 |
. . . . . . . . . . . . 13
β’ β
β β |
145 | 143, 144 | sstrdi 3960 |
. . . . . . . . . . . 12
β’ (π β (πΆ[,]π·) β β) |
146 | 22, 29, 28 | fourierdlem15 44453 |
. . . . . . . . . . . . 13
β’ (π β π:(0...π)βΆ(πΆ[,]π·)) |
147 | 146, 38 | ffvelcdmd 7040 |
. . . . . . . . . . . 12
β’ (π β (πβπ½) β (πΆ[,]π·)) |
148 | 145, 147 | sseldd 3949 |
. . . . . . . . . . 11
β’ (π β (πβπ½) β β) |
149 | 142, 148 | subcld 11520 |
. . . . . . . . . 10
β’ (π β ((πβ(π½ + 1)) β (πβπ½)) β β) |
150 | 42 | recnd 11191 |
. . . . . . . . . 10
β’ (π β (πΏβ(πΈβ(πβπ½))) β β) |
151 | 141, 149,
150 | subsub23d 43612 |
. . . . . . . . 9
β’ (π β (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) = (πΏβ(πΈβ(πβπ½))) β ((πΈβ(πβ(π½ + 1))) β (πΏβ(πΈβ(πβπ½)))) = ((πβ(π½ + 1)) β (πβπ½)))) |
152 | 140, 151 | mpbird 257 |
. . . . . . . 8
β’ (π β ((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) = (πΏβ(πΈβ(πβπ½)))) |
153 | 152 | eqcomd 2739 |
. . . . . . 7
β’ (π β (πΏβ(πΈβ(πβπ½))) = ((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½)))) |
154 | 153 | oveq1d 7376 |
. . . . . 6
β’ (π β ((πΏβ(πΈβ(πβπ½))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) = (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))))) |
155 | 141, 149 | subcld 11520 |
. . . . . . . 8
β’ (π β ((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) β β) |
156 | 155, 142,
141 | addsub12d 11543 |
. . . . . . 7
β’ (π β (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) = ((πβ(π½ + 1)) + (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) β (πΈβ(πβ(π½ + 1)))))) |
157 | 141, 149,
141 | sub32d 11552 |
. . . . . . . . 9
β’ (π β (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) β (πΈβ(πβ(π½ + 1)))) = (((πΈβ(πβ(π½ + 1))) β (πΈβ(πβ(π½ + 1)))) β ((πβ(π½ + 1)) β (πβπ½)))) |
158 | 141 | subidd 11508 |
. . . . . . . . . 10
β’ (π β ((πΈβ(πβ(π½ + 1))) β (πΈβ(πβ(π½ + 1)))) = 0) |
159 | 158 | oveq1d 7376 |
. . . . . . . . 9
β’ (π β (((πΈβ(πβ(π½ + 1))) β (πΈβ(πβ(π½ + 1)))) β ((πβ(π½ + 1)) β (πβπ½))) = (0 β ((πβ(π½ + 1)) β (πβπ½)))) |
160 | | df-neg 11396 |
. . . . . . . . . 10
β’ -((πβ(π½ + 1)) β (πβπ½)) = (0 β ((πβ(π½ + 1)) β (πβπ½))) |
161 | 142, 148 | negsubdi2d 11536 |
. . . . . . . . . 10
β’ (π β -((πβ(π½ + 1)) β (πβπ½)) = ((πβπ½) β (πβ(π½ + 1)))) |
162 | 160, 161 | eqtr3id 2787 |
. . . . . . . . 9
β’ (π β (0 β ((πβ(π½ + 1)) β (πβπ½))) = ((πβπ½) β (πβ(π½ + 1)))) |
163 | 157, 159,
162 | 3eqtrd 2777 |
. . . . . . . 8
β’ (π β (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) β (πΈβ(πβ(π½ + 1)))) = ((πβπ½) β (πβ(π½ + 1)))) |
164 | 163 | oveq2d 7377 |
. . . . . . 7
β’ (π β ((πβ(π½ + 1)) + (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) β (πΈβ(πβ(π½ + 1))))) = ((πβ(π½ + 1)) + ((πβπ½) β (πβ(π½ + 1))))) |
165 | 142, 148 | pncan3d 11523 |
. . . . . . 7
β’ (π β ((πβ(π½ + 1)) + ((πβπ½) β (πβ(π½ + 1)))) = (πβπ½)) |
166 | 156, 164,
165 | 3eqtrd 2777 |
. . . . . 6
β’ (π β (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) = (πβπ½)) |
167 | 124, 154,
166 | 3eqtrd 2777 |
. . . . 5
β’ (π β ((πΏβ(πΈβ(πβπ½))) + π) = (πβπ½)) |
168 | 52 | oveq2i 7372 |
. . . . . 6
β’ ((πΈβ(πβ(π½ + 1))) + π) = ((πΈβ(πβ(π½ + 1))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) |
169 | 141, 142 | pncan3d 11523 |
. . . . . 6
β’ (π β ((πΈβ(πβ(π½ + 1))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) = (πβ(π½ + 1))) |
170 | 168, 169 | eqtrid 2785 |
. . . . 5
β’ (π β ((πΈβ(πβ(π½ + 1))) + π) = (πβ(π½ + 1))) |
171 | 167, 170 | oveq12d 7379 |
. . . 4
β’ (π β (((πΏβ(πΈβ(πβπ½))) + π)(,)((πΈβ(πβ(π½ + 1))) + π)) = ((πβπ½)(,)(πβ(π½ + 1)))) |
172 | 171 | mpteq1d 5204 |
. . 3
β’ (π β (π¦ β (((πΏβ(πΈβ(πβπ½))) + π)(,)((πΈβ(πβ(π½ + 1))) + π)) β¦ (πΊβ(π¦ β π))) = (π¦ β ((πβπ½)(,)(πβ(π½ + 1))) β¦ (πΊβ(π¦ β π)))) |
173 | | fourierdlem90.f |
. . . . . 6
β’ (π β πΉ:ββΆβ) |
174 | 173 | feqmptd 6914 |
. . . . 5
β’ (π β πΉ = (π¦ β β β¦ (πΉβπ¦))) |
175 | 174 | reseq1d 5940 |
. . . 4
β’ (π β (πΉ βΎ ((πβπ½)(,)(πβ(π½ + 1)))) = ((π¦ β β β¦ (πΉβπ¦)) βΎ ((πβπ½)(,)(πβ(π½ + 1))))) |
176 | | ioossre 13334 |
. . . . . 6
β’ ((πβπ½)(,)(πβ(π½ + 1))) β β |
177 | 176 | a1i 11 |
. . . . 5
β’ (π β ((πβπ½)(,)(πβ(π½ + 1))) β β) |
178 | 177 | resmptd 5998 |
. . . 4
β’ (π β ((π¦ β β β¦ (πΉβπ¦)) βΎ ((πβπ½)(,)(πβ(π½ + 1)))) = (π¦ β ((πβπ½)(,)(πβ(π½ + 1))) β¦ (πΉβπ¦))) |
179 | 56 | fveq1i 6847 |
. . . . . . 7
β’ (πΊβ(π¦ β π)) = ((πΉ βΎ ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))))β(π¦ β π)) |
180 | 179 | a1i 11 |
. . . . . 6
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πΊβ(π¦ β π)) = ((πΉ βΎ ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))))β(π¦ β π))) |
181 | 42 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πΏβ(πΈβ(πβπ½))) β β) |
182 | 181 | rexrd 11213 |
. . . . . . . 8
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πΏβ(πΈβ(πβπ½))) β
β*) |
183 | 50 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πΈβ(πβ(π½ + 1))) β β) |
184 | 183 | rexrd 11213 |
. . . . . . . 8
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πΈβ(πβ(π½ + 1))) β
β*) |
185 | 177 | sselda 3948 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β π¦ β β) |
186 | 54 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β π β β) |
187 | 185, 186 | resubcld 11591 |
. . . . . . . 8
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (π¦ β π) β β) |
188 | 39 | rexrd 11213 |
. . . . . . . . . . . 12
β’ (π β (πβπ½) β
β*) |
189 | 188 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πβπ½) β
β*) |
190 | 48 | rexrd 11213 |
. . . . . . . . . . . 12
β’ (π β (πβ(π½ + 1)) β
β*) |
191 | 190 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πβ(π½ + 1)) β
β*) |
192 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) |
193 | | ioogtlb 43823 |
. . . . . . . . . . 11
β’ (((πβπ½) β β* β§ (πβ(π½ + 1)) β β* β§
π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πβπ½) < π¦) |
194 | 189, 191,
192, 193 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πβπ½) < π¦) |
195 | 167 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β ((πΏβ(πΈβ(πβπ½))) + π) = (πβπ½)) |
196 | 185 | recnd 11191 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β π¦ β β) |
197 | 186 | recnd 11191 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β π β β) |
198 | 196, 197 | npcand 11524 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β ((π¦ β π) + π) = π¦) |
199 | 194, 195,
198 | 3brtr4d 5141 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β ((πΏβ(πΈβ(πβπ½))) + π) < ((π¦ β π) + π)) |
200 | 181, 187,
186 | ltadd1d 11756 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β ((πΏβ(πΈβ(πβπ½))) < (π¦ β π) β ((πΏβ(πΈβ(πβπ½))) + π) < ((π¦ β π) + π))) |
201 | 199, 200 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πΏβ(πΈβ(πβπ½))) < (π¦ β π)) |
202 | | iooltub 43838 |
. . . . . . . . . . 11
β’ (((πβπ½) β β* β§ (πβ(π½ + 1)) β β* β§
π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β π¦ < (πβ(π½ + 1))) |
203 | 189, 191,
192, 202 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β π¦ < (πβ(π½ + 1))) |
204 | 170 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β ((πΈβ(πβ(π½ + 1))) + π) = (πβ(π½ + 1))) |
205 | 203, 198,
204 | 3brtr4d 5141 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β ((π¦ β π) + π) < ((πΈβ(πβ(π½ + 1))) + π)) |
206 | 187, 183,
186 | ltadd1d 11756 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β ((π¦ β π) < (πΈβ(πβ(π½ + 1))) β ((π¦ β π) + π) < ((πΈβ(πβ(π½ + 1))) + π))) |
207 | 205, 206 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (π¦ β π) < (πΈβ(πβ(π½ + 1)))) |
208 | 182, 184,
187, 201, 207 | eliood 43826 |
. . . . . . 7
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (π¦ β π) β ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) |
209 | | fvres 6865 |
. . . . . . 7
β’ ((π¦ β π) β ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β ((πΉ βΎ ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))))β(π¦ β π)) = (πΉβ(π¦ β π))) |
210 | 208, 209 | syl 17 |
. . . . . 6
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β ((πΉ βΎ ((πΏβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))))β(π¦ β π)) = (πΉβ(π¦ β π))) |
211 | 52 | oveq2i 7372 |
. . . . . . . . . 10
β’ (π¦ β π) = (π¦ β ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) |
212 | 211 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (π¦ β π) = (π¦ β ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))))) |
213 | 142 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πβ(π½ + 1)) β β) |
214 | 141 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πΈβ(πβ(π½ + 1))) β β) |
215 | 196, 213,
214 | subsub2d 11549 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (π¦ β ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) = (π¦ + ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))))) |
216 | 214, 213 | subcld 11520 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) β β) |
217 | 6, 5 | resubcld 11591 |
. . . . . . . . . . . . . . 15
β’ (π β (π΅ β π΄) β β) |
218 | 11, 217 | eqeltrid 2838 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
219 | 218 | recnd 11191 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
220 | 219 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β π β β) |
221 | 5, 6 | posdifd 11750 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΄ < π΅ β 0 < (π΅ β π΄))) |
222 | 8, 221 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (π β 0 < (π΅ β π΄)) |
223 | 222, 11 | breqtrrdi 5151 |
. . . . . . . . . . . . . 14
β’ (π β 0 < π) |
224 | 223 | gt0ne0d 11727 |
. . . . . . . . . . . . 13
β’ (π β π β 0) |
225 | 224 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β π β 0) |
226 | 216, 220,
225 | divcan1d 11940 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β ((((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) Β· π) = ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1)))) |
227 | 226 | eqcomd 2739 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) = ((((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) Β· π)) |
228 | 227 | oveq2d 7377 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (π¦ + ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1)))) = (π¦ + ((((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) Β· π))) |
229 | 212, 215,
228 | 3eqtrd 2777 |
. . . . . . . 8
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (π¦ β π) = (π¦ + ((((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) Β· π))) |
230 | 229 | fveq2d 6850 |
. . . . . . 7
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πΉβ(π¦ β π)) = (πΉβ(π¦ + ((((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) Β· π)))) |
231 | 173 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β πΉ:ββΆβ) |
232 | 218 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β π β β) |
233 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)))) |
234 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = (πβ(π½ + 1)) β π₯ = (πβ(π½ + 1))) |
235 | | oveq2 7369 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = (πβ(π½ + 1)) β (π΅ β π₯) = (π΅ β (πβ(π½ + 1)))) |
236 | 235 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = (πβ(π½ + 1)) β ((π΅ β π₯) / π) = ((π΅ β (πβ(π½ + 1))) / π)) |
237 | 236 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = (πβ(π½ + 1)) β (ββ((π΅ β π₯) / π)) = (ββ((π΅ β (πβ(π½ + 1))) / π))) |
238 | 237 | oveq1d 7376 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = (πβ(π½ + 1)) β ((ββ((π΅ β π₯) / π)) Β· π) = ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π)) |
239 | 234, 238 | oveq12d 7379 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = (πβ(π½ + 1)) β (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) = ((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π))) |
240 | 239 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ = (πβ(π½ + 1))) β (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) = ((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π))) |
241 | 6, 48 | resubcld 11591 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π΅ β (πβ(π½ + 1))) β β) |
242 | 241, 218,
224 | redivcld 11991 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π΅ β (πβ(π½ + 1))) / π) β β) |
243 | 242 | flcld 13712 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (ββ((π΅ β (πβ(π½ + 1))) / π)) β β€) |
244 | 243 | zred 12615 |
. . . . . . . . . . . . . . . . 17
β’ (π β (ββ((π΅ β (πβ(π½ + 1))) / π)) β β) |
245 | 244, 218 | remulcld 11193 |
. . . . . . . . . . . . . . . 16
β’ (π β ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π) β β) |
246 | 48, 245 | readdcld 11192 |
. . . . . . . . . . . . . . 15
β’ (π β ((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π)) β β) |
247 | 233, 240,
48, 246 | fvmptd 6959 |
. . . . . . . . . . . . . 14
β’ (π β (πΈβ(πβ(π½ + 1))) = ((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π))) |
248 | 247 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’ (π β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) = (((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π)) β (πβ(π½ + 1)))) |
249 | 244 | recnd 11191 |
. . . . . . . . . . . . . . 15
β’ (π β (ββ((π΅ β (πβ(π½ + 1))) / π)) β β) |
250 | 249, 219 | mulcld 11183 |
. . . . . . . . . . . . . 14
β’ (π β ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π) β β) |
251 | 142, 250 | pncan2d 11522 |
. . . . . . . . . . . . 13
β’ (π β (((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π)) β (πβ(π½ + 1))) = ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π)) |
252 | 248, 251 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) = ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π)) |
253 | 252 | oveq1d 7376 |
. . . . . . . . . . 11
β’ (π β (((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) = (((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π) / π)) |
254 | 249, 219,
224 | divcan4d 11945 |
. . . . . . . . . . 11
β’ (π β (((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π) / π) = (ββ((π΅ β (πβ(π½ + 1))) / π))) |
255 | 253, 254 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π β (((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) = (ββ((π΅ β (πβ(π½ + 1))) / π))) |
256 | 255, 243 | eqeltrd 2834 |
. . . . . . . . 9
β’ (π β (((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) β β€) |
257 | 256 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) β β€) |
258 | | fourierdlem90.6 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
259 | 258 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
260 | 231, 232,
257, 185, 259 | fperiodmul 43629 |
. . . . . . 7
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πΉβ(π¦ + ((((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) Β· π))) = (πΉβπ¦)) |
261 | 230, 260 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πΉβ(π¦ β π)) = (πΉβπ¦)) |
262 | 180, 210,
261 | 3eqtrrd 2778 |
. . . . 5
β’ ((π β§ π¦ β ((πβπ½)(,)(πβ(π½ + 1)))) β (πΉβπ¦) = (πΊβ(π¦ β π))) |
263 | 262 | mpteq2dva 5209 |
. . . 4
β’ (π β (π¦ β ((πβπ½)(,)(πβ(π½ + 1))) β¦ (πΉβπ¦)) = (π¦ β ((πβπ½)(,)(πβ(π½ + 1))) β¦ (πΊβ(π¦ β π)))) |
264 | 175, 178,
263 | 3eqtrrd 2778 |
. . 3
β’ (π β (π¦ β ((πβπ½)(,)(πβ(π½ + 1))) β¦ (πΊβ(π¦ β π))) = (πΉ βΎ ((πβπ½)(,)(πβ(π½ + 1))))) |
265 | 122, 172,
264 | 3eqtrd 2777 |
. 2
β’ (π β π
= (πΉ βΎ ((πβπ½)(,)(πβ(π½ + 1))))) |
266 | 171 | oveq1d 7376 |
. 2
β’ (π β ((((πΏβ(πΈβ(πβπ½))) + π)(,)((πΈβ(πβ(π½ + 1))) + π))βcnββ) = (((πβπ½)(,)(πβ(π½ + 1)))βcnββ)) |
267 | 121, 265,
266 | 3eltr3d 2848 |
1
β’ (π β (πΉ βΎ ((πβπ½)(,)(πβ(π½ + 1)))) β (((πβπ½)(,)(πβ(π½ + 1)))βcnββ)) |