Step | Hyp | Ref
| Expression |
1 | | fourierdlem91.q |
. . . . . . . . . . . 12
β’ (π β π β (πβπ)) |
2 | | fourierdlem91.m |
. . . . . . . . . . . . 13
β’ (π β π β β) |
3 | | fourierdlem91.p |
. . . . . . . . . . . . . 14
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
4 | 3 | fourierdlem2 44812 |
. . . . . . . . . . . . 13
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
5 | 2, 4 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
6 | 1, 5 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
7 | 6 | simpld 496 |
. . . . . . . . . 10
β’ (π β π β (β βm
(0...π))) |
8 | | elmapi 8840 |
. . . . . . . . . 10
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
β’ (π β π:(0...π)βΆβ) |
10 | | fzossfz 13648 |
. . . . . . . . . 10
β’
(0..^π) β
(0...π) |
11 | | fourierdlem91.t |
. . . . . . . . . . . . 13
β’ π = (π΅ β π΄) |
12 | | fourierdlem91.e |
. . . . . . . . . . . . 13
β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
13 | | fourierdlem91.J |
. . . . . . . . . . . . 13
β’ π = (π¦ β (π΄(,]π΅) β¦ if(π¦ = π΅, π΄, π¦)) |
14 | | fourierdlem91.i |
. . . . . . . . . . . . 13
β’ πΌ = (π₯ β β β¦ sup({π β (0..^π) β£ (πβπ) β€ (πβ(πΈβπ₯))}, β, < )) |
15 | 3, 2, 1, 11, 12, 13, 14 | fourierdlem37 44847 |
. . . . . . . . . . . 12
β’ (π β (πΌ:ββΆ(0..^π) β§ (π₯ β β β sup({π β (0..^π) β£ (πβπ) β€ (πβ(πΈβπ₯))}, β, < ) β {π β (0..^π) β£ (πβπ) β€ (πβ(πΈβπ₯))}))) |
16 | 15 | simpld 496 |
. . . . . . . . . . 11
β’ (π β πΌ:ββΆ(0..^π)) |
17 | | fourierdlem91.c |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΆ β β) |
18 | | fourierdlem91.d |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π· β (πΆ(,)+β)) |
19 | | elioore 13351 |
. . . . . . . . . . . . . . . . . . 19
β’ (π· β (πΆ(,)+β) β π· β β) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π· β β) |
21 | | elioo4g 13381 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π· β (πΆ(,)+β) β ((πΆ β β* β§ +β
β β* β§ π· β β) β§ (πΆ < π· β§ π· < +β))) |
22 | 18, 21 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((πΆ β β* β§ +β
β β* β§ π· β β) β§ (πΆ < π· β§ π· < +β))) |
23 | 22 | simprd 497 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πΆ < π· β§ π· < +β)) |
24 | 23 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΆ < π·) |
25 | | fourierdlem91.o |
. . . . . . . . . . . . . . . . . 18
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
26 | | oveq1 7413 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = π₯ β (π¦ + (π Β· π)) = (π₯ + (π Β· π))) |
27 | 26 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = π₯ β ((π¦ + (π Β· π)) β ran π β (π₯ + (π Β· π)) β ran π)) |
28 | 27 | rexbidv 3179 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π₯ β (βπ β β€ (π¦ + (π Β· π)) β ran π β βπ β β€ (π₯ + (π Β· π)) β ran π)) |
29 | 28 | cbvrabv 3443 |
. . . . . . . . . . . . . . . . . . 19
β’ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π} = {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π} |
30 | 29 | uneq2i 4160 |
. . . . . . . . . . . . . . . . . 18
β’ ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) = ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) |
31 | | fourierdlem91.n |
. . . . . . . . . . . . . . . . . . 19
β’ π = ((β―βπ») β 1) |
32 | | fourierdlem91.h |
. . . . . . . . . . . . . . . . . . . . 21
β’ π» = ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) |
33 | 32 | fveq2i 6892 |
. . . . . . . . . . . . . . . . . . . 20
β’
(β―βπ») =
(β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) |
34 | 33 | oveq1i 7416 |
. . . . . . . . . . . . . . . . . . 19
β’
((β―βπ»)
β 1) = ((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1) |
35 | 31, 34 | eqtri 2761 |
. . . . . . . . . . . . . . . . . 18
β’ π = ((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1) |
36 | | fourierdlem91.s |
. . . . . . . . . . . . . . . . . . 19
β’ π = (β©ππ Isom < , < ((0...π), π»)) |
37 | | isoeq5 7315 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π» = ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) β (π Isom < , < ((0...π), π») β π Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})))) |
38 | 32, 37 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π Isom < , < ((0...π), π») β π Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}))) |
39 | 38 | iotabii 6526 |
. . . . . . . . . . . . . . . . . . 19
β’
(β©ππ Isom < , < ((0...π), π»)) = (β©ππ Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}))) |
40 | 36, 39 | eqtri 2761 |
. . . . . . . . . . . . . . . . . 18
β’ π = (β©ππ Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}))) |
41 | 11, 3, 2, 1, 17, 20, 24, 25, 30, 35, 40 | fourierdlem54 44863 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π β β β§ π β (πβπ)) β§ π Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})))) |
42 | 41 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β β β§ π β (πβπ))) |
43 | 42 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ (π β π β (πβπ)) |
44 | 42 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
45 | 25 | fourierdlem2 44812 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
47 | 43, 46 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
48 | 47 | simpld 496 |
. . . . . . . . . . . . 13
β’ (π β π β (β βm
(0...π))) |
49 | | elmapi 8840 |
. . . . . . . . . . . . 13
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π:(0...π)βΆβ) |
51 | | fourierdlem91.17 |
. . . . . . . . . . . . 13
β’ (π β π½ β (0..^π)) |
52 | | elfzofz 13645 |
. . . . . . . . . . . . 13
β’ (π½ β (0..^π) β π½ β (0...π)) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π½ β (0...π)) |
54 | 50, 53 | ffvelcdmd 7085 |
. . . . . . . . . . 11
β’ (π β (πβπ½) β β) |
55 | 16, 54 | ffvelcdmd 7085 |
. . . . . . . . . 10
β’ (π β (πΌβ(πβπ½)) β (0..^π)) |
56 | 10, 55 | sselid 3980 |
. . . . . . . . 9
β’ (π β (πΌβ(πβπ½)) β (0...π)) |
57 | 9, 56 | ffvelcdmd 7085 |
. . . . . . . 8
β’ (π β (πβ(πΌβ(πβπ½))) β β) |
58 | 57 | rexrd 11261 |
. . . . . . 7
β’ (π β (πβ(πΌβ(πβπ½))) β
β*) |
59 | 58 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ (πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1))) β (πβ(πΌβ(πβπ½))) β
β*) |
60 | | fzofzp1 13726 |
. . . . . . . . . 10
β’ ((πΌβ(πβπ½)) β (0..^π) β ((πΌβ(πβπ½)) + 1) β (0...π)) |
61 | 55, 60 | syl 17 |
. . . . . . . . 9
β’ (π β ((πΌβ(πβπ½)) + 1) β (0...π)) |
62 | 9, 61 | ffvelcdmd 7085 |
. . . . . . . 8
β’ (π β (πβ((πΌβ(πβπ½)) + 1)) β β) |
63 | 62 | rexrd 11261 |
. . . . . . 7
β’ (π β (πβ((πΌβ(πβπ½)) + 1)) β
β*) |
64 | 63 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ (πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1))) β (πβ((πΌβ(πβπ½)) + 1)) β
β*) |
65 | 3, 2, 1 | fourierdlem11 44821 |
. . . . . . . . . . 11
β’ (π β (π΄ β β β§ π΅ β β β§ π΄ < π΅)) |
66 | 65 | simp1d 1143 |
. . . . . . . . . 10
β’ (π β π΄ β β) |
67 | 66 | rexrd 11261 |
. . . . . . . . 9
β’ (π β π΄ β
β*) |
68 | 65 | simp2d 1144 |
. . . . . . . . 9
β’ (π β π΅ β β) |
69 | | iocssre 13401 |
. . . . . . . . 9
β’ ((π΄ β β*
β§ π΅ β β)
β (π΄(,]π΅) β
β) |
70 | 67, 68, 69 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π΄(,]π΅) β β) |
71 | 65 | simp3d 1145 |
. . . . . . . . . 10
β’ (π β π΄ < π΅) |
72 | 66, 68, 71, 11, 12 | fourierdlem4 44814 |
. . . . . . . . 9
β’ (π β πΈ:ββΆ(π΄(,]π΅)) |
73 | | fzofzp1 13726 |
. . . . . . . . . . 11
β’ (π½ β (0..^π) β (π½ + 1) β (0...π)) |
74 | 51, 73 | syl 17 |
. . . . . . . . . 10
β’ (π β (π½ + 1) β (0...π)) |
75 | 50, 74 | ffvelcdmd 7085 |
. . . . . . . . 9
β’ (π β (πβ(π½ + 1)) β β) |
76 | 72, 75 | ffvelcdmd 7085 |
. . . . . . . 8
β’ (π β (πΈβ(πβ(π½ + 1))) β (π΄(,]π΅)) |
77 | 70, 76 | sseldd 3983 |
. . . . . . 7
β’ (π β (πΈβ(πβ(π½ + 1))) β β) |
78 | 77 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ (πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1))) β (πΈβ(πβ(π½ + 1))) β β) |
79 | 66, 68 | iccssred 13408 |
. . . . . . . . 9
β’ (π β (π΄[,]π΅) β β) |
80 | 66, 68, 71, 13 | fourierdlem17 44827 |
. . . . . . . . . 10
β’ (π β π:(π΄(,]π΅)βΆ(π΄[,]π΅)) |
81 | 72, 54 | ffvelcdmd 7085 |
. . . . . . . . . 10
β’ (π β (πΈβ(πβπ½)) β (π΄(,]π΅)) |
82 | 80, 81 | ffvelcdmd 7085 |
. . . . . . . . 9
β’ (π β (πβ(πΈβ(πβπ½))) β (π΄[,]π΅)) |
83 | 79, 82 | sseldd 3983 |
. . . . . . . 8
β’ (π β (πβ(πΈβ(πβπ½))) β β) |
84 | 47 | simprrd 773 |
. . . . . . . . . . . . . 14
β’ (π β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
85 | | fveq2 6889 |
. . . . . . . . . . . . . . . 16
β’ (π = π½ β (πβπ) = (πβπ½)) |
86 | | oveq1 7413 |
. . . . . . . . . . . . . . . . 17
β’ (π = π½ β (π + 1) = (π½ + 1)) |
87 | 86 | fveq2d 6893 |
. . . . . . . . . . . . . . . 16
β’ (π = π½ β (πβ(π + 1)) = (πβ(π½ + 1))) |
88 | 85, 87 | breq12d 5161 |
. . . . . . . . . . . . . . 15
β’ (π = π½ β ((πβπ) < (πβ(π + 1)) β (πβπ½) < (πβ(π½ + 1)))) |
89 | 88 | rspccva 3612 |
. . . . . . . . . . . . . 14
β’
((βπ β
(0..^π)(πβπ) < (πβ(π + 1)) β§ π½ β (0..^π)) β (πβπ½) < (πβ(π½ + 1))) |
90 | 84, 51, 89 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (πβπ½) < (πβ(π½ + 1))) |
91 | 54, 75 | posdifd 11798 |
. . . . . . . . . . . . 13
β’ (π β ((πβπ½) < (πβ(π½ + 1)) β 0 < ((πβ(π½ + 1)) β (πβπ½)))) |
92 | 90, 91 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β 0 < ((πβ(π½ + 1)) β (πβπ½))) |
93 | | eleq1 2822 |
. . . . . . . . . . . . . . . . 17
β’ (π = π½ β (π β (0..^π) β π½ β (0..^π))) |
94 | 93 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’ (π = π½ β ((π β§ π β (0..^π)) β (π β§ π½ β (0..^π)))) |
95 | | oveq1 7413 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π½ β (π + 1) = (π½ + 1)) |
96 | 95 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π½ β (πβ(π + 1)) = (πβ(π½ + 1))) |
97 | 96 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π½ β (πΈβ(πβ(π + 1))) = (πΈβ(πβ(π½ + 1)))) |
98 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π½ β (πβπ) = (πβπ½)) |
99 | 98 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π½ β (πΈβ(πβπ)) = (πΈβ(πβπ½))) |
100 | 99 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π½ β (πβ(πΈβ(πβπ))) = (πβ(πΈβ(πβπ½)))) |
101 | 97, 100 | oveq12d 7424 |
. . . . . . . . . . . . . . . . 17
β’ (π = π½ β ((πΈβ(πβ(π + 1))) β (πβ(πΈβ(πβπ)))) = ((πΈβ(πβ(π½ + 1))) β (πβ(πΈβ(πβπ½))))) |
102 | 96, 98 | oveq12d 7424 |
. . . . . . . . . . . . . . . . 17
β’ (π = π½ β ((πβ(π + 1)) β (πβπ)) = ((πβ(π½ + 1)) β (πβπ½))) |
103 | 101, 102 | eqeq12d 2749 |
. . . . . . . . . . . . . . . 16
β’ (π = π½ β (((πΈβ(πβ(π + 1))) β (πβ(πΈβ(πβπ)))) = ((πβ(π + 1)) β (πβπ)) β ((πΈβ(πβ(π½ + 1))) β (πβ(πΈβ(πβπ½)))) = ((πβ(π½ + 1)) β (πβπ½)))) |
104 | 94, 103 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π = π½ β (((π β§ π β (0..^π)) β ((πΈβ(πβ(π + 1))) β (πβ(πΈβ(πβπ)))) = ((πβ(π + 1)) β (πβπ))) β ((π β§ π½ β (0..^π)) β ((πΈβ(πβ(π½ + 1))) β (πβ(πΈβ(πβπ½)))) = ((πβ(π½ + 1)) β (πβπ½))))) |
105 | 11 | oveq2i 7417 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π Β· π) = (π Β· (π΅ β π΄)) |
106 | 105 | oveq2i 7417 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ + (π Β· π)) = (π¦ + (π Β· (π΅ β π΄))) |
107 | 106 | eleq1i 2825 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π¦ + (π Β· π)) β ran π β (π¦ + (π Β· (π΅ β π΄))) β ran π) |
108 | 107 | rexbii 3095 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ β
β€ (π¦ + (π Β· π)) β ran π β βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π) |
109 | 108 | rgenw 3066 |
. . . . . . . . . . . . . . . . . . . . 21
β’
βπ¦ β
(πΆ[,]π·)(βπ β β€ (π¦ + (π Β· π)) β ran π β βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π) |
110 | | rabbi 3463 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ¦ β
(πΆ[,]π·)(βπ β β€ (π¦ + (π Β· π)) β ran π β βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π) β {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π} = {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π}) |
111 | 109, 110 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . 20
β’ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π} = {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π} |
112 | 111 | uneq2i 4160 |
. . . . . . . . . . . . . . . . . . 19
β’ ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) = ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π}) |
113 | 112 | fveq2i 6892 |
. . . . . . . . . . . . . . . . . 18
β’
(β―β({πΆ,
π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) = (β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π})) |
114 | 113 | oveq1i 7416 |
. . . . . . . . . . . . . . . . 17
β’
((β―β({πΆ,
π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β 1) = ((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π})) β 1) |
115 | 35, 114 | eqtri 2761 |
. . . . . . . . . . . . . . . 16
β’ π = ((β―β({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π})) β 1) |
116 | | isoeq5 7315 |
. . . . . . . . . . . . . . . . . . 19
β’ (({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}) = ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π}) β (π Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β π Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π})))) |
117 | 112, 116 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’ (π Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π})) β π Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π}))) |
118 | 117 | iotabii 6526 |
. . . . . . . . . . . . . . . . 17
β’
(β©ππ Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· π)) β ran π}))) = (β©ππ Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π}))) |
119 | 40, 118 | eqtri 2761 |
. . . . . . . . . . . . . . . 16
β’ π = (β©ππ Isom < , < ((0...π), ({πΆ, π·} βͺ {π¦ β (πΆ[,]π·) β£ βπ β β€ (π¦ + (π Β· (π΅ β π΄))) β ran π}))) |
120 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) + (π΅ β (πΈβ(πβπ)))) = ((πβπ) + (π΅ β (πΈβ(πβπ)))) |
121 | 3, 11, 2, 1, 17, 18, 25, 115, 119, 12, 13, 120 | fourierdlem65 44874 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β ((πΈβ(πβ(π + 1))) β (πβ(πΈβ(πβπ)))) = ((πβ(π + 1)) β (πβπ))) |
122 | 104, 121 | vtoclg 3557 |
. . . . . . . . . . . . . 14
β’ (π½ β (0..^π) β ((π β§ π½ β (0..^π)) β ((πΈβ(πβ(π½ + 1))) β (πβ(πΈβ(πβπ½)))) = ((πβ(π½ + 1)) β (πβπ½)))) |
123 | 122 | anabsi7 670 |
. . . . . . . . . . . . 13
β’ ((π β§ π½ β (0..^π)) β ((πΈβ(πβ(π½ + 1))) β (πβ(πΈβ(πβπ½)))) = ((πβ(π½ + 1)) β (πβπ½))) |
124 | 51, 123 | mpdan 686 |
. . . . . . . . . . . 12
β’ (π β ((πΈβ(πβ(π½ + 1))) β (πβ(πΈβ(πβπ½)))) = ((πβ(π½ + 1)) β (πβπ½))) |
125 | 92, 124 | breqtrrd 5176 |
. . . . . . . . . . 11
β’ (π β 0 < ((πΈβ(πβ(π½ + 1))) β (πβ(πΈβ(πβπ½))))) |
126 | 83, 77 | posdifd 11798 |
. . . . . . . . . . 11
β’ (π β ((πβ(πΈβ(πβπ½))) < (πΈβ(πβ(π½ + 1))) β 0 < ((πΈβ(πβ(π½ + 1))) β (πβ(πΈβ(πβπ½)))))) |
127 | 125, 126 | mpbird 257 |
. . . . . . . . . 10
β’ (π β (πβ(πΈβ(πβπ½))) < (πΈβ(πβ(π½ + 1)))) |
128 | 100, 97 | oveq12d 7424 |
. . . . . . . . . . . . . . 15
β’ (π = π½ β ((πβ(πΈβ(πβπ)))(,)(πΈβ(πβ(π + 1)))) = ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) |
129 | 98 | fveq2d 6893 |
. . . . . . . . . . . . . . . . 17
β’ (π = π½ β (πΌβ(πβπ)) = (πΌβ(πβπ½))) |
130 | 129 | fveq2d 6893 |
. . . . . . . . . . . . . . . 16
β’ (π = π½ β (πβ(πΌβ(πβπ))) = (πβ(πΌβ(πβπ½)))) |
131 | 129 | oveq1d 7421 |
. . . . . . . . . . . . . . . . 17
β’ (π = π½ β ((πΌβ(πβπ)) + 1) = ((πΌβ(πβπ½)) + 1)) |
132 | 131 | fveq2d 6893 |
. . . . . . . . . . . . . . . 16
β’ (π = π½ β (πβ((πΌβ(πβπ)) + 1)) = (πβ((πΌβ(πβπ½)) + 1))) |
133 | 130, 132 | oveq12d 7424 |
. . . . . . . . . . . . . . 15
β’ (π = π½ β ((πβ(πΌβ(πβπ)))(,)(πβ((πΌβ(πβπ)) + 1))) = ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) |
134 | 128, 133 | sseq12d 4015 |
. . . . . . . . . . . . . 14
β’ (π = π½ β (((πβ(πΈβ(πβπ)))(,)(πΈβ(πβ(π + 1)))) β ((πβ(πΌβ(πβπ)))(,)(πβ((πΌβ(πβπ)) + 1))) β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))) |
135 | 94, 134 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π = π½ β (((π β§ π β (0..^π)) β ((πβ(πΈβ(πβπ)))(,)(πΈβ(πβ(π + 1)))) β ((πβ(πΌβ(πβπ)))(,)(πβ((πΌβ(πβπ)) + 1)))) β ((π β§ π½ β (0..^π)) β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))))) |
136 | 32, 30 | eqtri 2761 |
. . . . . . . . . . . . . 14
β’ π» = ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) |
137 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ ((πβπ) + if(((πβ(π + 1)) β (πβπ)) < ((πβ1) β π΄), (((πβ(π + 1)) β (πβπ)) / 2), (((πβ1) β π΄) / 2))) = ((πβπ) + if(((πβ(π + 1)) β (πβπ)) < ((πβ1) β π΄), (((πβ(π + 1)) β (πβπ)) / 2), (((πβ1) β π΄) / 2))) |
138 | 11, 3, 2, 1, 17, 20, 24, 25, 136, 31, 36, 12, 13, 137, 14 | fourierdlem79 44888 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((πβ(πΈβ(πβπ)))(,)(πΈβ(πβ(π + 1)))) β ((πβ(πΌβ(πβπ)))(,)(πβ((πΌβ(πβπ)) + 1)))) |
139 | 135, 138 | vtoclg 3557 |
. . . . . . . . . . . 12
β’ (π½ β (0..^π) β ((π β§ π½ β (0..^π)) β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))) |
140 | 139 | anabsi7 670 |
. . . . . . . . . . 11
β’ ((π β§ π½ β (0..^π)) β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) |
141 | 51, 140 | mpdan 686 |
. . . . . . . . . 10
β’ (π β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) |
142 | 57, 62, 83, 77, 127, 141 | fourierdlem10 44820 |
. . . . . . . . 9
β’ (π β ((πβ(πΌβ(πβπ½))) β€ (πβ(πΈβ(πβπ½))) β§ (πΈβ(πβ(π½ + 1))) β€ (πβ((πΌβ(πβπ½)) + 1)))) |
143 | 142 | simpld 496 |
. . . . . . . 8
β’ (π β (πβ(πΌβ(πβπ½))) β€ (πβ(πΈβ(πβπ½)))) |
144 | 57, 83, 77, 143, 127 | lelttrd 11369 |
. . . . . . 7
β’ (π β (πβ(πΌβ(πβπ½))) < (πΈβ(πβ(π½ + 1)))) |
145 | 144 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ (πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1))) β (πβ(πΌβ(πβπ½))) < (πΈβ(πβ(π½ + 1)))) |
146 | 62 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ (πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1))) β (πβ((πΌβ(πβπ½)) + 1)) β β) |
147 | 142 | simprd 497 |
. . . . . . . 8
β’ (π β (πΈβ(πβ(π½ + 1))) β€ (πβ((πΌβ(πβπ½)) + 1))) |
148 | 147 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ (πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1))) β (πΈβ(πβ(π½ + 1))) β€ (πβ((πΌβ(πβπ½)) + 1))) |
149 | | neqne 2949 |
. . . . . . . . 9
β’ (Β¬
(πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1)) β (πΈβ(πβ(π½ + 1))) β (πβ((πΌβ(πβπ½)) + 1))) |
150 | 149 | necomd 2997 |
. . . . . . . 8
β’ (Β¬
(πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1)) β (πβ((πΌβ(πβπ½)) + 1)) β (πΈβ(πβ(π½ + 1)))) |
151 | 150 | adantl 483 |
. . . . . . 7
β’ ((π β§ Β¬ (πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1))) β (πβ((πΌβ(πβπ½)) + 1)) β (πΈβ(πβ(π½ + 1)))) |
152 | 78, 146, 148, 151 | leneltd 11365 |
. . . . . 6
β’ ((π β§ Β¬ (πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1))) β (πΈβ(πβ(π½ + 1))) < (πβ((πΌβ(πβπ½)) + 1))) |
153 | 59, 64, 78, 145, 152 | eliood 44198 |
. . . . 5
β’ ((π β§ Β¬ (πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1))) β (πΈβ(πβ(π½ + 1))) β ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) |
154 | | fvres 6908 |
. . . . 5
β’ ((πΈβ(πβ(π½ + 1))) β ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))) β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))β(πΈβ(πβ(π½ + 1)))) = (πΉβ(πΈβ(πβ(π½ + 1))))) |
155 | 153, 154 | syl 17 |
. . . 4
β’ ((π β§ Β¬ (πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1))) β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))β(πΈβ(πβ(π½ + 1)))) = (πΉβ(πΈβ(πβ(π½ + 1))))) |
156 | 155 | eqcomd 2739 |
. . 3
β’ ((π β§ Β¬ (πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1))) β (πΉβ(πΈβ(πβ(π½ + 1)))) = ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))β(πΈβ(πβ(π½ + 1))))) |
157 | 156 | ifeq2da 4560 |
. 2
β’ (π β if((πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1)), (πβ(πΌβ(πβπ½))), (πΉβ(πΈβ(πβ(π½ + 1))))) = if((πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1)), (πβ(πΌβ(πβπ½))), ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))β(πΈβ(πβ(π½ + 1)))))) |
158 | | fourierdlem91.f |
. . . . . 6
β’ (π β πΉ:ββΆβ) |
159 | | fdm 6724 |
. . . . . . . 8
β’ (πΉ:ββΆβ β
dom πΉ =
β) |
160 | 158, 159 | syl 17 |
. . . . . . 7
β’ (π β dom πΉ = β) |
161 | 160 | feq2d 6701 |
. . . . . 6
β’ (π β (πΉ:dom πΉβΆβ β πΉ:ββΆβ)) |
162 | 158, 161 | mpbird 257 |
. . . . 5
β’ (π β πΉ:dom πΉβΆβ) |
163 | | ioosscn 13383 |
. . . . . 6
β’ ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β β |
164 | 163 | a1i 11 |
. . . . 5
β’ (π β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β β) |
165 | | ioossre 13382 |
. . . . . 6
β’ ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β β |
166 | 165, 160 | sseqtrrid 4035 |
. . . . 5
β’ (π β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β dom πΉ) |
167 | | fourierdlem91.u |
. . . . . . 7
β’ π = ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))) |
168 | 75, 77 | resubcld 11639 |
. . . . . . 7
β’ (π β ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))) β β) |
169 | 167, 168 | eqeltrid 2838 |
. . . . . 6
β’ (π β π β β) |
170 | 169 | recnd 11239 |
. . . . 5
β’ (π β π β β) |
171 | | eqid 2733 |
. . . . 5
β’ {π₯ β β β£
βπ¦ β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))π₯ = (π¦ + π)} = {π₯ β β β£ βπ¦ β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))π₯ = (π¦ + π)} |
172 | 83, 77, 169 | iooshift 44222 |
. . . . . 6
β’ (π β (((πβ(πΈβ(πβπ½))) + π)(,)((πΈβ(πβ(π½ + 1))) + π)) = {π₯ β β β£ βπ¦ β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))π₯ = (π¦ + π)}) |
173 | | ioossre 13382 |
. . . . . . 7
β’ (((πβ(πΈβ(πβπ½))) + π)(,)((πΈβ(πβ(π½ + 1))) + π)) β β |
174 | 173, 160 | sseqtrrid 4035 |
. . . . . 6
β’ (π β (((πβ(πΈβ(πβπ½))) + π)(,)((πΈβ(πβ(π½ + 1))) + π)) β dom πΉ) |
175 | 172, 174 | eqsstrrd 4021 |
. . . . 5
β’ (π β {π₯ β β β£ βπ¦ β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))π₯ = (π¦ + π)} β dom πΉ) |
176 | | elioore 13351 |
. . . . . 6
β’ (π¦ β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))) β π¦ β β) |
177 | 68, 66 | resubcld 11639 |
. . . . . . . . . . . . . 14
β’ (π β (π΅ β π΄) β β) |
178 | 11, 177 | eqeltrid 2838 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
179 | 178 | recnd 11239 |
. . . . . . . . . . . 12
β’ (π β π β β) |
180 | 66, 68 | posdifd 11798 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄ < π΅ β 0 < (π΅ β π΄))) |
181 | 71, 180 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (π β 0 < (π΅ β π΄)) |
182 | 181, 11 | breqtrrdi 5190 |
. . . . . . . . . . . . 13
β’ (π β 0 < π) |
183 | 182 | gt0ne0d 11775 |
. . . . . . . . . . . 12
β’ (π β π β 0) |
184 | 170, 179,
183 | divcan1d 11988 |
. . . . . . . . . . 11
β’ (π β ((π / π) Β· π) = π) |
185 | 184 | eqcomd 2739 |
. . . . . . . . . 10
β’ (π β π = ((π / π) Β· π)) |
186 | 185 | oveq2d 7422 |
. . . . . . . . 9
β’ (π β (π¦ + π) = (π¦ + ((π / π) Β· π))) |
187 | 186 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β (π¦ + π) = (π¦ + ((π / π) Β· π))) |
188 | 187 | fveq2d 6893 |
. . . . . . 7
β’ ((π β§ π¦ β β) β (πΉβ(π¦ + π)) = (πΉβ(π¦ + ((π / π) Β· π)))) |
189 | 158 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β πΉ:ββΆβ) |
190 | 178 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β π β β) |
191 | 77 | recnd 11239 |
. . . . . . . . . . . . . 14
β’ (π β (πΈβ(πβ(π½ + 1))) β β) |
192 | 75 | recnd 11239 |
. . . . . . . . . . . . . 14
β’ (π β (πβ(π½ + 1)) β β) |
193 | 191, 192 | negsubdi2d 11584 |
. . . . . . . . . . . . 13
β’ (π β -((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) = ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) |
194 | 193 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ (π β ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))) = -((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1)))) |
195 | 194 | oveq1d 7421 |
. . . . . . . . . . 11
β’ (π β (((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))) / π) = (-((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π)) |
196 | 167 | oveq1i 7416 |
. . . . . . . . . . . 12
β’ (π / π) = (((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))) / π) |
197 | 196 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π / π) = (((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))) / π)) |
198 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)))) |
199 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = (πβ(π½ + 1)) β π₯ = (πβ(π½ + 1))) |
200 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = (πβ(π½ + 1)) β (π΅ β π₯) = (π΅ β (πβ(π½ + 1)))) |
201 | 200 | oveq1d 7421 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = (πβ(π½ + 1)) β ((π΅ β π₯) / π) = ((π΅ β (πβ(π½ + 1))) / π)) |
202 | 201 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = (πβ(π½ + 1)) β (ββ((π΅ β π₯) / π)) = (ββ((π΅ β (πβ(π½ + 1))) / π))) |
203 | 202 | oveq1d 7421 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = (πβ(π½ + 1)) β ((ββ((π΅ β π₯) / π)) Β· π) = ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π)) |
204 | 199, 203 | oveq12d 7424 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = (πβ(π½ + 1)) β (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) = ((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π))) |
205 | 204 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ = (πβ(π½ + 1))) β (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) = ((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π))) |
206 | 68, 75 | resubcld 11639 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π΅ β (πβ(π½ + 1))) β β) |
207 | 206, 178,
183 | redivcld 12039 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π΅ β (πβ(π½ + 1))) / π) β β) |
208 | 207 | flcld 13760 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (ββ((π΅ β (πβ(π½ + 1))) / π)) β β€) |
209 | 208 | zred 12663 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (ββ((π΅ β (πβ(π½ + 1))) / π)) β β) |
210 | 209, 178 | remulcld 11241 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π) β β) |
211 | 75, 210 | readdcld 11240 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π)) β β) |
212 | 198, 205,
75, 211 | fvmptd 7003 |
. . . . . . . . . . . . . . 15
β’ (π β (πΈβ(πβ(π½ + 1))) = ((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π))) |
213 | 212 | oveq1d 7421 |
. . . . . . . . . . . . . 14
β’ (π β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) = (((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π)) β (πβ(π½ + 1)))) |
214 | 208 | zcnd 12664 |
. . . . . . . . . . . . . . . 16
β’ (π β (ββ((π΅ β (πβ(π½ + 1))) / π)) β β) |
215 | 214, 179 | mulcld 11231 |
. . . . . . . . . . . . . . 15
β’ (π β ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π) β β) |
216 | 192, 215 | pncan2d 11570 |
. . . . . . . . . . . . . 14
β’ (π β (((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π)) β (πβ(π½ + 1))) = ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π)) |
217 | 213, 216 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (π β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) = ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π)) |
218 | 217, 215 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’ (π β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) β β) |
219 | 218, 179,
183 | divnegd 12000 |
. . . . . . . . . . 11
β’ (π β -(((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) = (-((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π)) |
220 | 195, 197,
219 | 3eqtr4d 2783 |
. . . . . . . . . 10
β’ (π β (π / π) = -(((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π)) |
221 | 217 | oveq1d 7421 |
. . . . . . . . . . . . 13
β’ (π β (((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) = (((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π) / π)) |
222 | 214, 179,
183 | divcan4d 11993 |
. . . . . . . . . . . . 13
β’ (π β (((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π) / π) = (ββ((π΅ β (πβ(π½ + 1))) / π))) |
223 | 221, 222 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β (((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) = (ββ((π΅ β (πβ(π½ + 1))) / π))) |
224 | 223, 208 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ (π β (((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) β β€) |
225 | 224 | znegcld 12665 |
. . . . . . . . . 10
β’ (π β -(((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) / π) β β€) |
226 | 220, 225 | eqeltrd 2834 |
. . . . . . . . 9
β’ (π β (π / π) β β€) |
227 | 226 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β (π / π) β β€) |
228 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β π¦ β β) |
229 | | fourierdlem91.6 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
230 | 229 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π¦ β β) β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
231 | 189, 190,
227, 228, 230 | fperiodmul 44001 |
. . . . . . 7
β’ ((π β§ π¦ β β) β (πΉβ(π¦ + ((π / π) Β· π))) = (πΉβπ¦)) |
232 | 188, 231 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π¦ β β) β (πΉβ(π¦ + π)) = (πΉβπ¦)) |
233 | 176, 232 | sylan2 594 |
. . . . 5
β’ ((π β§ π¦ β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) β (πΉβ(π¦ + π)) = (πΉβπ¦)) |
234 | 6 | simprrd 773 |
. . . . . . . 8
β’ (π β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
235 | | fveq2 6889 |
. . . . . . . . . 10
β’ (π = (πΌβ(πβπ½)) β (πβπ) = (πβ(πΌβ(πβπ½)))) |
236 | | oveq1 7413 |
. . . . . . . . . . 11
β’ (π = (πΌβ(πβπ½)) β (π + 1) = ((πΌβ(πβπ½)) + 1)) |
237 | 236 | fveq2d 6893 |
. . . . . . . . . 10
β’ (π = (πΌβ(πβπ½)) β (πβ(π + 1)) = (πβ((πΌβ(πβπ½)) + 1))) |
238 | 235, 237 | breq12d 5161 |
. . . . . . . . 9
β’ (π = (πΌβ(πβπ½)) β ((πβπ) < (πβ(π + 1)) β (πβ(πΌβ(πβπ½))) < (πβ((πΌβ(πβπ½)) + 1)))) |
239 | 238 | rspccva 3612 |
. . . . . . . 8
β’
((βπ β
(0..^π)(πβπ) < (πβ(π + 1)) β§ (πΌβ(πβπ½)) β (0..^π)) β (πβ(πΌβ(πβπ½))) < (πβ((πΌβ(πβπ½)) + 1))) |
240 | 234, 55, 239 | syl2anc 585 |
. . . . . . 7
β’ (π β (πβ(πΌβ(πβπ½))) < (πβ((πΌβ(πβπ½)) + 1))) |
241 | 55 | ancli 550 |
. . . . . . . 8
β’ (π β (π β§ (πΌβ(πβπ½)) β (0..^π))) |
242 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π = (πΌβ(πβπ½)) β (π β (0..^π) β (πΌβ(πβπ½)) β (0..^π))) |
243 | 242 | anbi2d 630 |
. . . . . . . . . 10
β’ (π = (πΌβ(πβπ½)) β ((π β§ π β (0..^π)) β (π β§ (πΌβ(πβπ½)) β (0..^π)))) |
244 | 235, 237 | oveq12d 7424 |
. . . . . . . . . . . 12
β’ (π = (πΌβ(πβπ½)) β ((πβπ)(,)(πβ(π + 1))) = ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) |
245 | 244 | reseq2d 5980 |
. . . . . . . . . . 11
β’ (π = (πΌβ(πβπ½)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = (πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))) |
246 | 244 | oveq1d 7421 |
. . . . . . . . . . 11
β’ (π = (πΌβ(πβπ½)) β (((πβπ)(,)(πβ(π + 1)))βcnββ) = (((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))βcnββ)) |
247 | 245, 246 | eleq12d 2828 |
. . . . . . . . . 10
β’ (π = (πΌβ(πβπ½)) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ) β (πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) β (((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))βcnββ))) |
248 | 243, 247 | imbi12d 345 |
. . . . . . . . 9
β’ (π = (πΌβ(πβπ½)) β (((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) β ((π β§ (πΌβ(πβπ½)) β (0..^π)) β (πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) β (((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))βcnββ)))) |
249 | | fourierdlem91.fcn |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
250 | 248, 249 | vtoclg 3557 |
. . . . . . . 8
β’ ((πΌβ(πβπ½)) β (0..^π) β ((π β§ (πΌβ(πβπ½)) β (0..^π)) β (πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) β (((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))βcnββ))) |
251 | 55, 241, 250 | sylc 65 |
. . . . . . 7
β’ (π β (πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) β (((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))βcnββ)) |
252 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π(π β§ (πΌβ(πβπ½)) β (0..^π)) |
253 | | fourierdlem91.w |
. . . . . . . . . . . . 13
β’ π = (π β (0..^π) β¦ πΏ) |
254 | | nfmpt1 5256 |
. . . . . . . . . . . . 13
β’
β²π(π β (0..^π) β¦ πΏ) |
255 | 253, 254 | nfcxfr 2902 |
. . . . . . . . . . . 12
β’
β²ππ |
256 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π(πΌβ(πβπ½)) |
257 | 255, 256 | nffv 6899 |
. . . . . . . . . . 11
β’
β²π(πβ(πΌβ(πβπ½))) |
258 | 257 | nfel1 2920 |
. . . . . . . . . 10
β’
β²π(πβ(πΌβ(πβπ½))) β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) limβ (πβ((πΌβ(πβπ½)) + 1))) |
259 | 252, 258 | nfim 1900 |
. . . . . . . . 9
β’
β²π((π β§ (πΌβ(πβπ½)) β (0..^π)) β (πβ(πΌβ(πβπ½))) β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) limβ (πβ((πΌβ(πβπ½)) + 1)))) |
260 | 243 | biimpar 479 |
. . . . . . . . . . . . . 14
β’ ((π = (πΌβ(πβπ½)) β§ (π β§ (πΌβ(πβπ½)) β (0..^π))) β (π β§ π β (0..^π))) |
261 | 260 | 3adant2 1132 |
. . . . . . . . . . . . 13
β’ ((π = (πΌβ(πβπ½)) β§ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) β§ (π β§ (πΌβ(πβπ½)) β (0..^π))) β (π β§ π β (0..^π))) |
262 | | fourierdlem91.l |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
263 | 261, 262 | syl 17 |
. . . . . . . . . . . 12
β’ ((π = (πΌβ(πβπ½)) β§ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) β§ (π β§ (πΌβ(πβπ½)) β (0..^π))) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
264 | | fveq2 6889 |
. . . . . . . . . . . . . . . 16
β’ (π = (πΌβ(πβπ½)) β (πβπ) = (πβ(πΌβ(πβπ½)))) |
265 | 264 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ (π = (πΌβ(πβπ½)) β (πβ(πΌβ(πβπ½))) = (πβπ)) |
266 | 265 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π = (πΌβ(πβπ½)) β§ (π β§ (πΌβ(πβπ½)) β (0..^π))) β (πβ(πΌβ(πβπ½))) = (πβπ)) |
267 | 260 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ ((π = (πΌβ(πβπ½)) β§ (π β§ (πΌβ(πβπ½)) β (0..^π))) β π β (0..^π)) |
268 | | elex 3493 |
. . . . . . . . . . . . . . . 16
β’ (πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) β πΏ β V) |
269 | 260, 262,
268 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ ((π = (πΌβ(πβπ½)) β§ (π β§ (πΌβ(πβπ½)) β (0..^π))) β πΏ β V) |
270 | 253 | fvmpt2 7007 |
. . . . . . . . . . . . . . 15
β’ ((π β (0..^π) β§ πΏ β V) β (πβπ) = πΏ) |
271 | 267, 269,
270 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π = (πΌβ(πβπ½)) β§ (π β§ (πΌβ(πβπ½)) β (0..^π))) β (πβπ) = πΏ) |
272 | 266, 271 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π = (πΌβ(πβπ½)) β§ (π β§ (πΌβ(πβπ½)) β (0..^π))) β (πβ(πΌβ(πβπ½))) = πΏ) |
273 | 272 | 3adant2 1132 |
. . . . . . . . . . . 12
β’ ((π = (πΌβ(πβπ½)) β§ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) β§ (π β§ (πΌβ(πβπ½)) β (0..^π))) β (πβ(πΌβ(πβπ½))) = πΏ) |
274 | 245, 237 | oveq12d 7424 |
. . . . . . . . . . . . . 14
β’ (π = (πΌβ(πβπ½)) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) limβ (πβ((πΌβ(πβπ½)) + 1)))) |
275 | 274 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ (π = (πΌβ(πβπ½)) β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) limβ (πβ((πΌβ(πβπ½)) + 1))) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
276 | 275 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’ ((π = (πΌβ(πβπ½)) β§ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) β§ (π β§ (πΌβ(πβπ½)) β (0..^π))) β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) limβ (πβ((πΌβ(πβπ½)) + 1))) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
277 | 263, 273,
276 | 3eltr4d 2849 |
. . . . . . . . . . 11
β’ ((π = (πΌβ(πβπ½)) β§ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) β§ (π β§ (πΌβ(πβπ½)) β (0..^π))) β (πβ(πΌβ(πβπ½))) β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) limβ (πβ((πΌβ(πβπ½)) + 1)))) |
278 | 277 | 3exp 1120 |
. . . . . . . . . 10
β’ (π = (πΌβ(πβπ½)) β (((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) β ((π β§ (πΌβ(πβπ½)) β (0..^π)) β (πβ(πΌβ(πβπ½))) β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) limβ (πβ((πΌβ(πβπ½)) + 1)))))) |
279 | 262 | 2a1i 12 |
. . . . . . . . . 10
β’ (π = (πΌβ(πβπ½)) β (((π β§ (πΌβ(πβπ½)) β (0..^π)) β (πβ(πΌβ(πβπ½))) β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) limβ (πβ((πΌβ(πβπ½)) + 1)))) β ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))))) |
280 | 278, 279 | impbid 211 |
. . . . . . . . 9
β’ (π = (πΌβ(πβπ½)) β (((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) β ((π β§ (πΌβ(πβπ½)) β (0..^π)) β (πβ(πΌβ(πβπ½))) β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) limβ (πβ((πΌβ(πβπ½)) + 1)))))) |
281 | 259, 280,
262 | vtoclg1f 3556 |
. . . . . . . 8
β’ ((πΌβ(πβπ½)) β (0..^π) β ((π β§ (πΌβ(πβπ½)) β (0..^π)) β (πβ(πΌβ(πβπ½))) β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) limβ (πβ((πΌβ(πβπ½)) + 1))))) |
282 | 55, 241, 281 | sylc 65 |
. . . . . . 7
β’ (π β (πβ(πΌβ(πβπ½))) β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) limβ (πβ((πΌβ(πβπ½)) + 1)))) |
283 | | eqid 2733 |
. . . . . . 7
β’ if((πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1)), (πβ(πΌβ(πβπ½))), ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))β(πΈβ(πβ(π½ + 1))))) = if((πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1)), (πβ(πΌβ(πβπ½))), ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))β(πΈβ(πβ(π½ + 1))))) |
284 | | eqid 2733 |
. . . . . . 7
β’
((TopOpenββfld) βΎt (((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))) βͺ {(πβ((πΌβ(πβπ½)) + 1))})) =
((TopOpenββfld) βΎt (((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))) βͺ {(πβ((πΌβ(πβπ½)) + 1))})) |
285 | 57, 62, 240, 251, 282, 83, 77, 127, 141, 283, 284 | fourierdlem33 44843 |
. . . . . 6
β’ (π β if((πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1)), (πβ(πΌβ(πβπ½))), ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))β(πΈβ(πβ(π½ + 1))))) β (((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) βΎ ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) limβ (πΈβ(πβ(π½ + 1))))) |
286 | 141 | resabs1d 6011 |
. . . . . . 7
β’ (π β ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) βΎ ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) = (πΉ βΎ ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1)))))) |
287 | 286 | oveq1d 7421 |
. . . . . 6
β’ (π β (((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1)))) βΎ ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) limβ (πΈβ(πβ(π½ + 1)))) = ((πΉ βΎ ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) limβ (πΈβ(πβ(π½ + 1))))) |
288 | 285, 287 | eleqtrd 2836 |
. . . . 5
β’ (π β if((πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1)), (πβ(πΌβ(πβπ½))), ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))β(πΈβ(πβ(π½ + 1))))) β ((πΉ βΎ ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))) limβ (πΈβ(πβ(π½ + 1))))) |
289 | 162, 164,
166, 170, 171, 175, 233, 288 | limcperiod 44331 |
. . . 4
β’ (π β if((πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1)), (πβ(πΌβ(πβπ½))), ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))β(πΈβ(πβ(π½ + 1))))) β ((πΉ βΎ {π₯ β β β£ βπ¦ β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))π₯ = (π¦ + π)}) limβ ((πΈβ(πβ(π½ + 1))) + π))) |
290 | 167 | oveq2i 7417 |
. . . . . 6
β’ ((πΈβ(πβ(π½ + 1))) + π) = ((πΈβ(πβ(π½ + 1))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) |
291 | 191, 192 | pncan3d 11571 |
. . . . . 6
β’ (π β ((πΈβ(πβ(π½ + 1))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) = (πβ(π½ + 1))) |
292 | 290, 291 | eqtrid 2785 |
. . . . 5
β’ (π β ((πΈβ(πβ(π½ + 1))) + π) = (πβ(π½ + 1))) |
293 | 292 | oveq2d 7422 |
. . . 4
β’ (π β ((πΉ βΎ {π₯ β β β£ βπ¦ β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))π₯ = (π¦ + π)}) limβ ((πΈβ(πβ(π½ + 1))) + π)) = ((πΉ βΎ {π₯ β β β£ βπ¦ β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))π₯ = (π¦ + π)}) limβ (πβ(π½ + 1)))) |
294 | 289, 293 | eleqtrd 2836 |
. . 3
β’ (π β if((πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1)), (πβ(πΌβ(πβπ½))), ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))β(πΈβ(πβ(π½ + 1))))) β ((πΉ βΎ {π₯ β β β£ βπ¦ β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))π₯ = (π¦ + π)}) limβ (πβ(π½ + 1)))) |
295 | 167 | oveq2i 7417 |
. . . . . . . . 9
β’ ((πβ(πΈβ(πβπ½))) + π) = ((πβ(πΈβ(πβπ½))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) |
296 | 295 | a1i 11 |
. . . . . . . 8
β’ (π β ((πβ(πΈβ(πβπ½))) + π) = ((πβ(πΈβ(πβπ½))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))))) |
297 | 17, 20 | iccssred 13408 |
. . . . . . . . . . . . . . 15
β’ (π β (πΆ[,]π·) β β) |
298 | | ax-resscn 11164 |
. . . . . . . . . . . . . . 15
β’ β
β β |
299 | 297, 298 | sstrdi 3994 |
. . . . . . . . . . . . . 14
β’ (π β (πΆ[,]π·) β β) |
300 | 25, 44, 43 | fourierdlem15 44825 |
. . . . . . . . . . . . . . 15
β’ (π β π:(0...π)βΆ(πΆ[,]π·)) |
301 | 300, 53 | ffvelcdmd 7085 |
. . . . . . . . . . . . . 14
β’ (π β (πβπ½) β (πΆ[,]π·)) |
302 | 299, 301 | sseldd 3983 |
. . . . . . . . . . . . 13
β’ (π β (πβπ½) β β) |
303 | 192, 302 | subcld 11568 |
. . . . . . . . . . . 12
β’ (π β ((πβ(π½ + 1)) β (πβπ½)) β β) |
304 | 83 | recnd 11239 |
. . . . . . . . . . . 12
β’ (π β (πβ(πΈβ(πβπ½))) β β) |
305 | 191, 303,
304 | subsub23d 43984 |
. . . . . . . . . . 11
β’ (π β (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) = (πβ(πΈβ(πβπ½))) β ((πΈβ(πβ(π½ + 1))) β (πβ(πΈβ(πβπ½)))) = ((πβ(π½ + 1)) β (πβπ½)))) |
306 | 124, 305 | mpbird 257 |
. . . . . . . . . 10
β’ (π β ((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) = (πβ(πΈβ(πβπ½)))) |
307 | 306 | eqcomd 2739 |
. . . . . . . . 9
β’ (π β (πβ(πΈβ(πβπ½))) = ((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½)))) |
308 | 307 | oveq1d 7421 |
. . . . . . . 8
β’ (π β ((πβ(πΈβ(πβπ½))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) = (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1)))))) |
309 | 191, 303 | subcld 11568 |
. . . . . . . . . 10
β’ (π β ((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) β β) |
310 | 309, 192,
191 | addsub12d 11591 |
. . . . . . . . 9
β’ (π β (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) = ((πβ(π½ + 1)) + (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) β (πΈβ(πβ(π½ + 1)))))) |
311 | 191, 303,
191 | sub32d 11600 |
. . . . . . . . . . 11
β’ (π β (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) β (πΈβ(πβ(π½ + 1)))) = (((πΈβ(πβ(π½ + 1))) β (πΈβ(πβ(π½ + 1)))) β ((πβ(π½ + 1)) β (πβπ½)))) |
312 | 191 | subidd 11556 |
. . . . . . . . . . . 12
β’ (π β ((πΈβ(πβ(π½ + 1))) β (πΈβ(πβ(π½ + 1)))) = 0) |
313 | 312 | oveq1d 7421 |
. . . . . . . . . . 11
β’ (π β (((πΈβ(πβ(π½ + 1))) β (πΈβ(πβ(π½ + 1)))) β ((πβ(π½ + 1)) β (πβπ½))) = (0 β ((πβ(π½ + 1)) β (πβπ½)))) |
314 | | df-neg 11444 |
. . . . . . . . . . . 12
β’ -((πβ(π½ + 1)) β (πβπ½)) = (0 β ((πβ(π½ + 1)) β (πβπ½))) |
315 | 192, 302 | negsubdi2d 11584 |
. . . . . . . . . . . 12
β’ (π β -((πβ(π½ + 1)) β (πβπ½)) = ((πβπ½) β (πβ(π½ + 1)))) |
316 | 314, 315 | eqtr3id 2787 |
. . . . . . . . . . 11
β’ (π β (0 β ((πβ(π½ + 1)) β (πβπ½))) = ((πβπ½) β (πβ(π½ + 1)))) |
317 | 311, 313,
316 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (π β (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) β (πΈβ(πβ(π½ + 1)))) = ((πβπ½) β (πβ(π½ + 1)))) |
318 | 317 | oveq2d 7422 |
. . . . . . . . 9
β’ (π β ((πβ(π½ + 1)) + (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) β (πΈβ(πβ(π½ + 1))))) = ((πβ(π½ + 1)) + ((πβπ½) β (πβ(π½ + 1))))) |
319 | 192, 302 | pncan3d 11571 |
. . . . . . . . 9
β’ (π β ((πβ(π½ + 1)) + ((πβπ½) β (πβ(π½ + 1)))) = (πβπ½)) |
320 | 310, 318,
319 | 3eqtrd 2777 |
. . . . . . . 8
β’ (π β (((πΈβ(πβ(π½ + 1))) β ((πβ(π½ + 1)) β (πβπ½))) + ((πβ(π½ + 1)) β (πΈβ(πβ(π½ + 1))))) = (πβπ½)) |
321 | 296, 308,
320 | 3eqtrd 2777 |
. . . . . . 7
β’ (π β ((πβ(πΈβ(πβπ½))) + π) = (πβπ½)) |
322 | 321, 292 | oveq12d 7424 |
. . . . . 6
β’ (π β (((πβ(πΈβ(πβπ½))) + π)(,)((πΈβ(πβ(π½ + 1))) + π)) = ((πβπ½)(,)(πβ(π½ + 1)))) |
323 | 172, 322 | eqtr3d 2775 |
. . . . 5
β’ (π β {π₯ β β β£ βπ¦ β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))π₯ = (π¦ + π)} = ((πβπ½)(,)(πβ(π½ + 1)))) |
324 | 323 | reseq2d 5980 |
. . . 4
β’ (π β (πΉ βΎ {π₯ β β β£ βπ¦ β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))π₯ = (π¦ + π)}) = (πΉ βΎ ((πβπ½)(,)(πβ(π½ + 1))))) |
325 | 324 | oveq1d 7421 |
. . 3
β’ (π β ((πΉ βΎ {π₯ β β β£ βπ¦ β ((πβ(πΈβ(πβπ½)))(,)(πΈβ(πβ(π½ + 1))))π₯ = (π¦ + π)}) limβ (πβ(π½ + 1))) = ((πΉ βΎ ((πβπ½)(,)(πβ(π½ + 1)))) limβ (πβ(π½ + 1)))) |
326 | 294, 325 | eleqtrd 2836 |
. 2
β’ (π β if((πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1)), (πβ(πΌβ(πβπ½))), ((πΉ βΎ ((πβ(πΌβ(πβπ½)))(,)(πβ((πΌβ(πβπ½)) + 1))))β(πΈβ(πβ(π½ + 1))))) β ((πΉ βΎ ((πβπ½)(,)(πβ(π½ + 1)))) limβ (πβ(π½ + 1)))) |
327 | 157, 326 | eqeltrd 2834 |
1
β’ (π β if((πΈβ(πβ(π½ + 1))) = (πβ((πΌβ(πβπ½)) + 1)), (πβ(πΌβ(πβπ½))), (πΉβ(πΈβ(πβ(π½ + 1))))) β ((πΉ βΎ ((πβπ½)(,)(πβ(π½ + 1)))) limβ (πβ(π½ + 1)))) |