Step | Hyp | Ref
| Expression |
1 | | fourierdlem54.n |
. . 3
β’ π = ((β―βπ») β 1) |
2 | | 2z 12542 |
. . . . . 6
β’ 2 β
β€ |
3 | 2 | a1i 11 |
. . . . 5
β’ (π β 2 β
β€) |
4 | | fourierdlem54.c |
. . . . . . . . . 10
β’ (π β πΆ β β) |
5 | | prid1g 4726 |
. . . . . . . . . 10
β’ (πΆ β β β πΆ β {πΆ, π·}) |
6 | | elun1 4141 |
. . . . . . . . . 10
β’ (πΆ β {πΆ, π·} β πΆ β ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π})) |
7 | 4, 5, 6 | 3syl 18 |
. . . . . . . . 9
β’ (π β πΆ β ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π})) |
8 | | fourierdlem54.h |
. . . . . . . . 9
β’ π» = ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) |
9 | 7, 8 | eleqtrrdi 2849 |
. . . . . . . 8
β’ (π β πΆ β π») |
10 | 9 | ne0d 4300 |
. . . . . . 7
β’ (π β π» β β
) |
11 | | prfi 9273 |
. . . . . . . . . 10
β’ {πΆ, π·} β Fin |
12 | | fourierdlem54.p |
. . . . . . . . . . . . 13
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
13 | | fourierdlem54.m |
. . . . . . . . . . . . 13
β’ (π β π β β) |
14 | | fourierdlem54.q |
. . . . . . . . . . . . 13
β’ (π β π β (πβπ)) |
15 | 12, 13, 14 | fourierdlem11 44433 |
. . . . . . . . . . . 12
β’ (π β (π΄ β β β§ π΅ β β β§ π΄ < π΅)) |
16 | 15 | simp1d 1143 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
17 | 15 | simp2d 1144 |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
18 | 15 | simp3d 1145 |
. . . . . . . . . . 11
β’ (π β π΄ < π΅) |
19 | | fourierdlem54.t |
. . . . . . . . . . 11
β’ π = (π΅ β π΄) |
20 | 12, 13, 14 | fourierdlem15 44437 |
. . . . . . . . . . . 12
β’ (π β π:(0...π)βΆ(π΄[,]π΅)) |
21 | | frn 6680 |
. . . . . . . . . . . 12
β’ (π:(0...π)βΆ(π΄[,]π΅) β ran π β (π΄[,]π΅)) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
β’ (π β ran π β (π΄[,]π΅)) |
23 | 12 | fourierdlem2 44424 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
24 | 13, 23 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
25 | 14, 24 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
26 | 25 | simpld 496 |
. . . . . . . . . . . . . 14
β’ (π β π β (β βm
(0...π))) |
27 | | elmapi 8794 |
. . . . . . . . . . . . . 14
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
28 | | ffn 6673 |
. . . . . . . . . . . . . 14
β’ (π:(0...π)βΆβ β π Fn (0...π)) |
29 | 26, 27, 28 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β π Fn (0...π)) |
30 | | fzfid 13885 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β Fin) |
31 | | fnfi 9132 |
. . . . . . . . . . . . 13
β’ ((π Fn (0...π) β§ (0...π) β Fin) β π β Fin) |
32 | 29, 30, 31 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β π β Fin) |
33 | | rnfi 9286 |
. . . . . . . . . . . 12
β’ (π β Fin β ran π β Fin) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
β’ (π β ran π β Fin) |
35 | 25 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))) |
36 | 35 | simpld 496 |
. . . . . . . . . . . . 13
β’ (π β ((πβ0) = π΄ β§ (πβπ) = π΅)) |
37 | 36 | simpld 496 |
. . . . . . . . . . . 12
β’ (π β (πβ0) = π΄) |
38 | 13 | nnnn0d 12480 |
. . . . . . . . . . . . . . 15
β’ (π β π β
β0) |
39 | | nn0uz 12812 |
. . . . . . . . . . . . . . 15
β’
β0 = (β€β₯β0) |
40 | 38, 39 | eleqtrdi 2848 |
. . . . . . . . . . . . . 14
β’ (π β π β
(β€β₯β0)) |
41 | | eluzfz1 13455 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β0) β 0 β (0...π)) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β 0 β (0...π)) |
43 | | fnfvelrn 7036 |
. . . . . . . . . . . . 13
β’ ((π Fn (0...π) β§ 0 β (0...π)) β (πβ0) β ran π) |
44 | 29, 42, 43 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (πβ0) β ran π) |
45 | 37, 44 | eqeltrrd 2839 |
. . . . . . . . . . 11
β’ (π β π΄ β ran π) |
46 | 36 | simprd 497 |
. . . . . . . . . . . 12
β’ (π β (πβπ) = π΅) |
47 | | eluzfz2 13456 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β0) β π β (0...π)) |
48 | 40, 47 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β (0...π)) |
49 | | fnfvelrn 7036 |
. . . . . . . . . . . . 13
β’ ((π Fn (0...π) β§ π β (0...π)) β (πβπ) β ran π) |
50 | 29, 48, 49 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (πβπ) β ran π) |
51 | 46, 50 | eqeltrrd 2839 |
. . . . . . . . . . 11
β’ (π β π΅ β ran π) |
52 | | eqid 2737 |
. . . . . . . . . . 11
β’ (abs
β β ) = (abs β β ) |
53 | | eqid 2737 |
. . . . . . . . . . 11
β’ ((ran
π Γ ran π) β I ) = ((ran π Γ ran π) β I ) |
54 | | eqid 2737 |
. . . . . . . . . . 11
β’ ran ((abs
β β ) βΎ ((ran π Γ ran π) β I )) = ran ((abs β β )
βΎ ((ran π Γ ran
π) β I
)) |
55 | | eqid 2737 |
. . . . . . . . . . 11
β’ inf(ran
((abs β β ) βΎ ((ran π Γ ran π) β I )), β, < ) = inf(ran
((abs β β ) βΎ ((ran π Γ ran π) β I )), β, <
) |
56 | | fourierdlem54.d |
. . . . . . . . . . 11
β’ (π β π· β β) |
57 | | eqid 2737 |
. . . . . . . . . . 11
β’
(topGenβran (,)) = (topGenβran (,)) |
58 | | eqid 2737 |
. . . . . . . . . . 11
β’
((topGenβran (,)) βΎt (πΆ[,]π·)) = ((topGenβran (,))
βΎt (πΆ[,]π·)) |
59 | | oveq1 7369 |
. . . . . . . . . . . . . 14
β’ (π₯ = π€ β (π₯ + (π Β· π)) = (π€ + (π Β· π))) |
60 | 59 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π₯ = π€ β ((π₯ + (π Β· π)) β ran π β (π€ + (π Β· π)) β ran π)) |
61 | 60 | rexbidv 3176 |
. . . . . . . . . . . 12
β’ (π₯ = π€ β (βπ β β€ (π₯ + (π Β· π)) β ran π β βπ β β€ (π€ + (π Β· π)) β ran π)) |
62 | 61 | cbvrabv 3420 |
. . . . . . . . . . 11
β’ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π} = {π€ β (πΆ[,]π·) β£ βπ β β€ (π€ + (π Β· π)) β ran π} |
63 | | oveq1 7369 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π Β· π) = (π Β· π)) |
64 | 63 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π¦ + (π Β· π)) = (π¦ + (π Β· π))) |
65 | 64 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π¦ + (π Β· π)) β ran π β (π¦ + (π Β· π)) β ran π)) |
66 | 65 | anbi1d 631 |
. . . . . . . . . . . . 13
β’ (π = π β (((π¦ + (π Β· π)) β ran π β§ (π§ + (π Β· π)) β ran π) β ((π¦ + (π Β· π)) β ran π β§ (π§ + (π Β· π)) β ran π))) |
67 | | oveq1 7369 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π Β· π) = (π Β· π)) |
68 | 67 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π§ + (π Β· π)) = (π§ + (π Β· π))) |
69 | 68 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π§ + (π Β· π)) β ran π β (π§ + (π Β· π)) β ran π)) |
70 | 69 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ (π = π β (((π¦ + (π Β· π)) β ran π β§ (π§ + (π Β· π)) β ran π) β ((π¦ + (π Β· π)) β ran π β§ (π§ + (π Β· π)) β ran π))) |
71 | 66, 70 | cbvrex2vw 3231 |
. . . . . . . . . . . 12
β’
(βπ β
β€ βπ β
β€ ((π¦ + (π Β· π)) β ran π β§ (π§ + (π Β· π)) β ran π) β βπ β β€ βπ β β€ ((π¦ + (π Β· π)) β ran π β§ (π§ + (π Β· π)) β ran π)) |
72 | 71 | anbi2i 624 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β β β§ π§ β β β§ π¦ < π§)) β§ βπ β β€ βπ β β€ ((π¦ + (π Β· π)) β ran π β§ (π§ + (π Β· π)) β ran π)) β ((π β§ (π¦ β β β§ π§ β β β§ π¦ < π§)) β§ βπ β β€ βπ β β€ ((π¦ + (π Β· π)) β ran π β§ (π§ + (π Β· π)) β ran π))) |
73 | 16, 17, 18, 19, 22, 34, 45, 51, 52, 53, 54, 55, 4, 56, 57, 58, 62, 72 | fourierdlem42 44464 |
. . . . . . . . . 10
β’ (π β {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π} β Fin) |
74 | | unfi 9123 |
. . . . . . . . . 10
β’ (({πΆ, π·} β Fin β§ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π} β Fin) β ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) β Fin) |
75 | 11, 73, 74 | sylancr 588 |
. . . . . . . . 9
β’ (π β ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) β Fin) |
76 | 8, 75 | eqeltrid 2842 |
. . . . . . . 8
β’ (π β π» β Fin) |
77 | | hashnncl 14273 |
. . . . . . . 8
β’ (π» β Fin β
((β―βπ») β
β β π» β
β
)) |
78 | 76, 77 | syl 17 |
. . . . . . 7
β’ (π β ((β―βπ») β β β π» β β
)) |
79 | 10, 78 | mpbird 257 |
. . . . . 6
β’ (π β (β―βπ») β
β) |
80 | 79 | nnzd 12533 |
. . . . 5
β’ (π β (β―βπ») β
β€) |
81 | | fourierdlem54.cd |
. . . . . . . . 9
β’ (π β πΆ < π·) |
82 | 4, 81 | ltned 11298 |
. . . . . . . 8
β’ (π β πΆ β π·) |
83 | | hashprg 14302 |
. . . . . . . . 9
β’ ((πΆ β β β§ π· β β) β (πΆ β π· β (β―β{πΆ, π·}) = 2)) |
84 | 4, 56, 83 | syl2anc 585 |
. . . . . . . 8
β’ (π β (πΆ β π· β (β―β{πΆ, π·}) = 2)) |
85 | 82, 84 | mpbid 231 |
. . . . . . 7
β’ (π β (β―β{πΆ, π·}) = 2) |
86 | 85 | eqcomd 2743 |
. . . . . 6
β’ (π β 2 = (β―β{πΆ, π·})) |
87 | | ssun1 4137 |
. . . . . . . . 9
β’ {πΆ, π·} β ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) |
88 | 87 | a1i 11 |
. . . . . . . 8
β’ (π β {πΆ, π·} β ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π})) |
89 | 88, 8 | sseqtrrdi 4000 |
. . . . . . 7
β’ (π β {πΆ, π·} β π») |
90 | | hashssle 43606 |
. . . . . . 7
β’ ((π» β Fin β§ {πΆ, π·} β π») β (β―β{πΆ, π·}) β€ (β―βπ»)) |
91 | 76, 89, 90 | syl2anc 585 |
. . . . . 6
β’ (π β (β―β{πΆ, π·}) β€ (β―βπ»)) |
92 | 86, 91 | eqbrtrd 5132 |
. . . . 5
β’ (π β 2 β€
(β―βπ»)) |
93 | | eluz2 12776 |
. . . . 5
β’
((β―βπ»)
β (β€β₯β2) β (2 β β€ β§
(β―βπ») β
β€ β§ 2 β€ (β―βπ»))) |
94 | 3, 80, 92, 93 | syl3anbrc 1344 |
. . . 4
β’ (π β (β―βπ») β
(β€β₯β2)) |
95 | | uz2m1nn 12855 |
. . . 4
β’
((β―βπ»)
β (β€β₯β2) β ((β―βπ») β 1) β
β) |
96 | 94, 95 | syl 17 |
. . 3
β’ (π β ((β―βπ») β 1) β
β) |
97 | 1, 96 | eqeltrid 2842 |
. 2
β’ (π β π β β) |
98 | | prssg 4784 |
. . . . . . . . . . . . 13
β’ ((πΆ β β β§ π· β β) β ((πΆ β β β§ π· β β) β {πΆ, π·} β β)) |
99 | 4, 56, 98 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β ((πΆ β β β§ π· β β) β {πΆ, π·} β β)) |
100 | 4, 56, 99 | mpbi2and 711 |
. . . . . . . . . . 11
β’ (π β {πΆ, π·} β β) |
101 | | ssrab2 4042 |
. . . . . . . . . . . 12
β’ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π} β (πΆ[,]π·) |
102 | 4, 56 | iccssred 13358 |
. . . . . . . . . . . 12
β’ (π β (πΆ[,]π·) β β) |
103 | 101, 102 | sstrid 3960 |
. . . . . . . . . . 11
β’ (π β {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π} β β) |
104 | 100, 103 | unssd 4151 |
. . . . . . . . . 10
β’ (π β ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) β β) |
105 | 8, 104 | eqsstrid 3997 |
. . . . . . . . 9
β’ (π β π» β β) |
106 | | fourierdlem54.s |
. . . . . . . . 9
β’ π = (β©ππ Isom < , < ((0...π), π»)) |
107 | 76, 105, 106, 1 | fourierdlem36 44458 |
. . . . . . . 8
β’ (π β π Isom < , < ((0...π), π»)) |
108 | | df-isom 6510 |
. . . . . . . 8
β’ (π Isom < , < ((0...π), π») β (π:(0...π)β1-1-ontoβπ» β§ βπ₯ β (0...π)βπ¦ β (0...π)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
109 | 107, 108 | sylib 217 |
. . . . . . 7
β’ (π β (π:(0...π)β1-1-ontoβπ» β§ βπ₯ β (0...π)βπ¦ β (0...π)(π₯ < π¦ β (πβπ₯) < (πβπ¦)))) |
110 | 109 | simpld 496 |
. . . . . 6
β’ (π β π:(0...π)β1-1-ontoβπ») |
111 | | f1of 6789 |
. . . . . 6
β’ (π:(0...π)β1-1-ontoβπ» β π:(0...π)βΆπ») |
112 | 110, 111 | syl 17 |
. . . . 5
β’ (π β π:(0...π)βΆπ») |
113 | 112, 105 | fssd 6691 |
. . . 4
β’ (π β π:(0...π)βΆβ) |
114 | | reex 11149 |
. . . . 5
β’ β
β V |
115 | | ovex 7395 |
. . . . . 6
β’
(0...π) β
V |
116 | 115 | a1i 11 |
. . . . 5
β’ (π β (0...π) β V) |
117 | | elmapg 8785 |
. . . . 5
β’ ((β
β V β§ (0...π)
β V) β (π β
(β βm (0...π)) β π:(0...π)βΆβ)) |
118 | 114, 116,
117 | sylancr 588 |
. . . 4
β’ (π β (π β (β βm
(0...π)) β π:(0...π)βΆβ)) |
119 | 113, 118 | mpbird 257 |
. . 3
β’ (π β π β (β βm
(0...π))) |
120 | | df-f1o 6508 |
. . . . . . . . . . 11
β’ (π:(0...π)β1-1-ontoβπ» β (π:(0...π)β1-1βπ» β§ π:(0...π)βontoβπ»)) |
121 | 110, 120 | sylib 217 |
. . . . . . . . . 10
β’ (π β (π:(0...π)β1-1βπ» β§ π:(0...π)βontoβπ»)) |
122 | 121 | simprd 497 |
. . . . . . . . 9
β’ (π β π:(0...π)βontoβπ») |
123 | | dffo3 7057 |
. . . . . . . . 9
β’ (π:(0...π)βontoβπ» β (π:(0...π)βΆπ» β§ ββ β π» βπ¦ β (0...π)β = (πβπ¦))) |
124 | 122, 123 | sylib 217 |
. . . . . . . 8
β’ (π β (π:(0...π)βΆπ» β§ ββ β π» βπ¦ β (0...π)β = (πβπ¦))) |
125 | 124 | simprd 497 |
. . . . . . 7
β’ (π β ββ β π» βπ¦ β (0...π)β = (πβπ¦)) |
126 | | eqeq1 2741 |
. . . . . . . . . 10
β’ (β = πΆ β (β = (πβπ¦) β πΆ = (πβπ¦))) |
127 | | eqcom 2744 |
. . . . . . . . . 10
β’ (πΆ = (πβπ¦) β (πβπ¦) = πΆ) |
128 | 126, 127 | bitrdi 287 |
. . . . . . . . 9
β’ (β = πΆ β (β = (πβπ¦) β (πβπ¦) = πΆ)) |
129 | 128 | rexbidv 3176 |
. . . . . . . 8
β’ (β = πΆ β (βπ¦ β (0...π)β = (πβπ¦) β βπ¦ β (0...π)(πβπ¦) = πΆ)) |
130 | 129 | rspcv 3580 |
. . . . . . 7
β’ (πΆ β π» β (ββ β π» βπ¦ β (0...π)β = (πβπ¦) β βπ¦ β (0...π)(πβπ¦) = πΆ)) |
131 | 9, 125, 130 | sylc 65 |
. . . . . 6
β’ (π β βπ¦ β (0...π)(πβπ¦) = πΆ) |
132 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π¦ = 0 β (πβπ¦) = (πβ0)) |
133 | 132 | eqcomd 2743 |
. . . . . . . . . . . . 13
β’ (π¦ = 0 β (πβ0) = (πβπ¦)) |
134 | 133 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ (πβπ¦) = πΆ) β§ π¦ = 0) β (πβ0) = (πβπ¦)) |
135 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ (πβπ¦) = πΆ) β§ π¦ = 0) β (πβπ¦) = πΆ) |
136 | 134, 135 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ¦) = πΆ) β§ π¦ = 0) β (πβ0) = πΆ) |
137 | 4 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πβπ¦) = πΆ) β§ π¦ = 0) β πΆ β β) |
138 | 136, 137 | eqeltrd 2838 |
. . . . . . . . . 10
β’ (((π β§ (πβπ¦) = πΆ) β§ π¦ = 0) β (πβ0) β β) |
139 | 138, 136 | eqled 11265 |
. . . . . . . . 9
β’ (((π β§ (πβπ¦) = πΆ) β§ π¦ = 0) β (πβ0) β€ πΆ) |
140 | 139 | 3adantl2 1168 |
. . . . . . . 8
β’ (((π β§ π¦ β (0...π) β§ (πβπ¦) = πΆ) β§ π¦ = 0) β (πβ0) β€ πΆ) |
141 | 4 | rexrd 11212 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΆ β
β*) |
142 | 56 | rexrd 11212 |
. . . . . . . . . . . . . . . . 17
β’ (π β π· β
β*) |
143 | 4, 56, 81 | ltled 11310 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΆ β€ π·) |
144 | | lbicc2 13388 |
. . . . . . . . . . . . . . . . 17
β’ ((πΆ β β*
β§ π· β
β* β§ πΆ
β€ π·) β πΆ β (πΆ[,]π·)) |
145 | 141, 142,
143, 144 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β πΆ β (πΆ[,]π·)) |
146 | | ubicc2 13389 |
. . . . . . . . . . . . . . . . 17
β’ ((πΆ β β*
β§ π· β
β* β§ πΆ
β€ π·) β π· β (πΆ[,]π·)) |
147 | 141, 142,
143, 146 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β π· β (πΆ[,]π·)) |
148 | | prssg 4784 |
. . . . . . . . . . . . . . . . 17
β’ ((πΆ β (πΆ[,]π·) β§ π· β (πΆ[,]π·)) β ((πΆ β (πΆ[,]π·) β§ π· β (πΆ[,]π·)) β {πΆ, π·} β (πΆ[,]π·))) |
149 | 145, 147,
148 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πΆ β (πΆ[,]π·) β§ π· β (πΆ[,]π·)) β {πΆ, π·} β (πΆ[,]π·))) |
150 | 145, 147,
149 | mpbi2and 711 |
. . . . . . . . . . . . . . 15
β’ (π β {πΆ, π·} β (πΆ[,]π·)) |
151 | 101 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π} β (πΆ[,]π·)) |
152 | 150, 151 | unssd 4151 |
. . . . . . . . . . . . . 14
β’ (π β ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) β (πΆ[,]π·)) |
153 | 8, 152 | eqsstrid 3997 |
. . . . . . . . . . . . 13
β’ (π β π» β (πΆ[,]π·)) |
154 | | nnm1nn0 12461 |
. . . . . . . . . . . . . . . . . 18
β’
((β―βπ»)
β β β ((β―βπ») β 1) β
β0) |
155 | 79, 154 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((β―βπ») β 1) β
β0) |
156 | 1, 155 | eqeltrid 2842 |
. . . . . . . . . . . . . . . 16
β’ (π β π β
β0) |
157 | 156, 39 | eleqtrdi 2848 |
. . . . . . . . . . . . . . 15
β’ (π β π β
(β€β₯β0)) |
158 | | eluzfz1 13455 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β0) β 0 β (0...π)) |
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β 0 β (0...π)) |
160 | 112, 159 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ (π β (πβ0) β π») |
161 | 153, 160 | sseldd 3950 |
. . . . . . . . . . . 12
β’ (π β (πβ0) β (πΆ[,]π·)) |
162 | 102, 161 | sseldd 3950 |
. . . . . . . . . . 11
β’ (π β (πβ0) β β) |
163 | 162 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ Β¬ π¦ = 0) β (πβ0) β β) |
164 | 163 | 3ad2antl1 1186 |
. . . . . . . . 9
β’ (((π β§ π¦ β (0...π) β§ (πβπ¦) = πΆ) β§ Β¬ π¦ = 0) β (πβ0) β β) |
165 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ Β¬ π¦ = 0) β πΆ β β) |
166 | 165 | 3ad2antl1 1186 |
. . . . . . . . 9
β’ (((π β§ π¦ β (0...π) β§ (πβπ¦) = πΆ) β§ Β¬ π¦ = 0) β πΆ β β) |
167 | | elfzelz 13448 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (0...π) β π¦ β β€) |
168 | 167 | zred 12614 |
. . . . . . . . . . . . . 14
β’ (π¦ β (0...π) β π¦ β β) |
169 | 168 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π¦ β (0...π) β§ Β¬ π¦ = 0) β π¦ β β) |
170 | | elfzle1 13451 |
. . . . . . . . . . . . . 14
β’ (π¦ β (0...π) β 0 β€ π¦) |
171 | 170 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π¦ β (0...π) β§ Β¬ π¦ = 0) β 0 β€ π¦) |
172 | | neqne 2952 |
. . . . . . . . . . . . . 14
β’ (Β¬
π¦ = 0 β π¦ β 0) |
173 | 172 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π¦ β (0...π) β§ Β¬ π¦ = 0) β π¦ β 0) |
174 | 169, 171,
173 | ne0gt0d 11299 |
. . . . . . . . . . . 12
β’ ((π¦ β (0...π) β§ Β¬ π¦ = 0) β 0 < π¦) |
175 | 174 | 3ad2antl2 1187 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (0...π) β§ (πβπ¦) = πΆ) β§ Β¬ π¦ = 0) β 0 < π¦) |
176 | | simpl1 1192 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (0...π) β§ (πβπ¦) = πΆ) β§ Β¬ π¦ = 0) β π) |
177 | | simpl2 1193 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (0...π) β§ (πβπ¦) = πΆ) β§ Β¬ π¦ = 0) β π¦ β (0...π)) |
178 | 109 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β βπ₯ β (0...π)βπ¦ β (0...π)(π₯ < π¦ β (πβπ₯) < (πβπ¦))) |
179 | | breq1 5113 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = 0 β (π₯ < π¦ β 0 < π¦)) |
180 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = 0 β (πβπ₯) = (πβ0)) |
181 | 180 | breq1d 5120 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = 0 β ((πβπ₯) < (πβπ¦) β (πβ0) < (πβπ¦))) |
182 | 179, 181 | bibi12d 346 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = 0 β ((π₯ < π¦ β (πβπ₯) < (πβπ¦)) β (0 < π¦ β (πβ0) < (πβπ¦)))) |
183 | 182 | ralbidv 3175 |
. . . . . . . . . . . . . . 15
β’ (π₯ = 0 β (βπ¦ β (0...π)(π₯ < π¦ β (πβπ₯) < (πβπ¦)) β βπ¦ β (0...π)(0 < π¦ β (πβ0) < (πβπ¦)))) |
184 | 183 | rspcv 3580 |
. . . . . . . . . . . . . 14
β’ (0 β
(0...π) β
(βπ₯ β
(0...π)βπ¦ β (0...π)(π₯ < π¦ β (πβπ₯) < (πβπ¦)) β βπ¦ β (0...π)(0 < π¦ β (πβ0) < (πβπ¦)))) |
185 | 159, 178,
184 | sylc 65 |
. . . . . . . . . . . . 13
β’ (π β βπ¦ β (0...π)(0 < π¦ β (πβ0) < (πβπ¦))) |
186 | 185 | r19.21bi 3237 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (0...π)) β (0 < π¦ β (πβ0) < (πβπ¦))) |
187 | 176, 177,
186 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (0...π) β§ (πβπ¦) = πΆ) β§ Β¬ π¦ = 0) β (0 < π¦ β (πβ0) < (πβπ¦))) |
188 | 175, 187 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (0...π) β§ (πβπ¦) = πΆ) β§ Β¬ π¦ = 0) β (πβ0) < (πβπ¦)) |
189 | | simpl3 1194 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (0...π) β§ (πβπ¦) = πΆ) β§ Β¬ π¦ = 0) β (πβπ¦) = πΆ) |
190 | 188, 189 | breqtrd 5136 |
. . . . . . . . 9
β’ (((π β§ π¦ β (0...π) β§ (πβπ¦) = πΆ) β§ Β¬ π¦ = 0) β (πβ0) < πΆ) |
191 | 164, 166,
190 | ltled 11310 |
. . . . . . . 8
β’ (((π β§ π¦ β (0...π) β§ (πβπ¦) = πΆ) β§ Β¬ π¦ = 0) β (πβ0) β€ πΆ) |
192 | 140, 191 | pm2.61dan 812 |
. . . . . . 7
β’ ((π β§ π¦ β (0...π) β§ (πβπ¦) = πΆ) β (πβ0) β€ πΆ) |
193 | 192 | rexlimdv3a 3157 |
. . . . . 6
β’ (π β (βπ¦ β (0...π)(πβπ¦) = πΆ β (πβ0) β€ πΆ)) |
194 | 131, 193 | mpd 15 |
. . . . 5
β’ (π β (πβ0) β€ πΆ) |
195 | | elicc2 13336 |
. . . . . . . 8
β’ ((πΆ β β β§ π· β β) β ((πβ0) β (πΆ[,]π·) β ((πβ0) β β β§ πΆ β€ (πβ0) β§ (πβ0) β€ π·))) |
196 | 4, 56, 195 | syl2anc 585 |
. . . . . . 7
β’ (π β ((πβ0) β (πΆ[,]π·) β ((πβ0) β β β§ πΆ β€ (πβ0) β§ (πβ0) β€ π·))) |
197 | 161, 196 | mpbid 231 |
. . . . . 6
β’ (π β ((πβ0) β β β§ πΆ β€ (πβ0) β§ (πβ0) β€ π·)) |
198 | 197 | simp2d 1144 |
. . . . 5
β’ (π β πΆ β€ (πβ0)) |
199 | 162, 4 | letri3d 11304 |
. . . . 5
β’ (π β ((πβ0) = πΆ β ((πβ0) β€ πΆ β§ πΆ β€ (πβ0)))) |
200 | 194, 198,
199 | mpbir2and 712 |
. . . 4
β’ (π β (πβ0) = πΆ) |
201 | | eluzfz2 13456 |
. . . . . . . . . 10
β’ (π β
(β€β₯β0) β π β (0...π)) |
202 | 157, 201 | syl 17 |
. . . . . . . . 9
β’ (π β π β (0...π)) |
203 | 112, 202 | ffvelcdmd 7041 |
. . . . . . . 8
β’ (π β (πβπ) β π») |
204 | 153, 203 | sseldd 3950 |
. . . . . . 7
β’ (π β (πβπ) β (πΆ[,]π·)) |
205 | | elicc2 13336 |
. . . . . . . 8
β’ ((πΆ β β β§ π· β β) β ((πβπ) β (πΆ[,]π·) β ((πβπ) β β β§ πΆ β€ (πβπ) β§ (πβπ) β€ π·))) |
206 | 4, 56, 205 | syl2anc 585 |
. . . . . . 7
β’ (π β ((πβπ) β (πΆ[,]π·) β ((πβπ) β β β§ πΆ β€ (πβπ) β§ (πβπ) β€ π·))) |
207 | 204, 206 | mpbid 231 |
. . . . . 6
β’ (π β ((πβπ) β β β§ πΆ β€ (πβπ) β§ (πβπ) β€ π·)) |
208 | 207 | simp3d 1145 |
. . . . 5
β’ (π β (πβπ) β€ π·) |
209 | | prid2g 4727 |
. . . . . . . . 9
β’ (π· β β β π· β {πΆ, π·}) |
210 | | elun1 4141 |
. . . . . . . . 9
β’ (π· β {πΆ, π·} β π· β ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π})) |
211 | 56, 209, 210 | 3syl 18 |
. . . . . . . 8
β’ (π β π· β ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π})) |
212 | 211, 8 | eleqtrrdi 2849 |
. . . . . . 7
β’ (π β π· β π») |
213 | | eqeq1 2741 |
. . . . . . . . . 10
β’ (β = π· β (β = (πβπ¦) β π· = (πβπ¦))) |
214 | | eqcom 2744 |
. . . . . . . . . 10
β’ (π· = (πβπ¦) β (πβπ¦) = π·) |
215 | 213, 214 | bitrdi 287 |
. . . . . . . . 9
β’ (β = π· β (β = (πβπ¦) β (πβπ¦) = π·)) |
216 | 215 | rexbidv 3176 |
. . . . . . . 8
β’ (β = π· β (βπ¦ β (0...π)β = (πβπ¦) β βπ¦ β (0...π)(πβπ¦) = π·)) |
217 | 216 | rspcv 3580 |
. . . . . . 7
β’ (π· β π» β (ββ β π» βπ¦ β (0...π)β = (πβπ¦) β βπ¦ β (0...π)(πβπ¦) = π·)) |
218 | 212, 125,
217 | sylc 65 |
. . . . . 6
β’ (π β βπ¦ β (0...π)(πβπ¦) = π·) |
219 | 214 | biimpri 227 |
. . . . . . . . 9
β’ ((πβπ¦) = π· β π· = (πβπ¦)) |
220 | 219 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((π β§ π¦ β (0...π) β§ (πβπ¦) = π·) β π· = (πβπ¦)) |
221 | 113 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (0...π)) β (πβπ¦) β β) |
222 | 102, 204 | sseldd 3950 |
. . . . . . . . . . 11
β’ (π β (πβπ) β β) |
223 | 222 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (0...π)) β (πβπ) β β) |
224 | 168 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (0...π)) β π¦ β β) |
225 | | elfzel2 13446 |
. . . . . . . . . . . . . 14
β’ (π¦ β (0...π) β π β β€) |
226 | 225 | zred 12614 |
. . . . . . . . . . . . 13
β’ (π¦ β (0...π) β π β β) |
227 | 226 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (0...π)) β π β β) |
228 | | elfzle2 13452 |
. . . . . . . . . . . . 13
β’ (π¦ β (0...π) β π¦ β€ π) |
229 | 228 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (0...π)) β π¦ β€ π) |
230 | 224, 227,
229 | lensymd 11313 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (0...π)) β Β¬ π < π¦) |
231 | | breq1 5113 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (π₯ < π¦ β π < π¦)) |
232 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
233 | 232 | breq1d 5120 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β ((πβπ₯) < (πβπ¦) β (πβπ) < (πβπ¦))) |
234 | 231, 233 | bibi12d 346 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β ((π₯ < π¦ β (πβπ₯) < (πβπ¦)) β (π < π¦ β (πβπ) < (πβπ¦)))) |
235 | 234 | ralbidv 3175 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (βπ¦ β (0...π)(π₯ < π¦ β (πβπ₯) < (πβπ¦)) β βπ¦ β (0...π)(π < π¦ β (πβπ) < (πβπ¦)))) |
236 | 235 | rspcv 3580 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β (βπ₯ β (0...π)βπ¦ β (0...π)(π₯ < π¦ β (πβπ₯) < (πβπ¦)) β βπ¦ β (0...π)(π < π¦ β (πβπ) < (πβπ¦)))) |
237 | 202, 178,
236 | sylc 65 |
. . . . . . . . . . . 12
β’ (π β βπ¦ β (0...π)(π < π¦ β (πβπ) < (πβπ¦))) |
238 | 237 | r19.21bi 3237 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (0...π)) β (π < π¦ β (πβπ) < (πβπ¦))) |
239 | 230, 238 | mtbid 324 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (0...π)) β Β¬ (πβπ) < (πβπ¦)) |
240 | 221, 223,
239 | nltled 11312 |
. . . . . . . . 9
β’ ((π β§ π¦ β (0...π)) β (πβπ¦) β€ (πβπ)) |
241 | 240 | 3adant3 1133 |
. . . . . . . 8
β’ ((π β§ π¦ β (0...π) β§ (πβπ¦) = π·) β (πβπ¦) β€ (πβπ)) |
242 | 220, 241 | eqbrtrd 5132 |
. . . . . . 7
β’ ((π β§ π¦ β (0...π) β§ (πβπ¦) = π·) β π· β€ (πβπ)) |
243 | 242 | rexlimdv3a 3157 |
. . . . . 6
β’ (π β (βπ¦ β (0...π)(πβπ¦) = π· β π· β€ (πβπ))) |
244 | 218, 243 | mpd 15 |
. . . . 5
β’ (π β π· β€ (πβπ)) |
245 | 222, 56 | letri3d 11304 |
. . . . 5
β’ (π β ((πβπ) = π· β ((πβπ) β€ π· β§ π· β€ (πβπ)))) |
246 | 208, 244,
245 | mpbir2and 712 |
. . . 4
β’ (π β (πβπ) = π·) |
247 | | elfzoelz 13579 |
. . . . . . . . 9
β’ (π β (0..^π) β π β β€) |
248 | 247 | zred 12614 |
. . . . . . . 8
β’ (π β (0..^π) β π β β) |
249 | 248 | ltp1d 12092 |
. . . . . . 7
β’ (π β (0..^π) β π < (π + 1)) |
250 | 249 | adantl 483 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β π < (π + 1)) |
251 | 178 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β βπ₯ β (0...π)βπ¦ β (0...π)(π₯ < π¦ β (πβπ₯) < (πβπ¦))) |
252 | | elfzofz 13595 |
. . . . . . . . 9
β’ (π β (0..^π) β π β (0...π)) |
253 | 252 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
254 | | fzofzp1 13676 |
. . . . . . . . 9
β’ (π β (0..^π) β (π + 1) β (0...π)) |
255 | 254 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
256 | | breq1 5113 |
. . . . . . . . . 10
β’ (π₯ = π β (π₯ < π¦ β π < π¦)) |
257 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
258 | 257 | breq1d 5120 |
. . . . . . . . . 10
β’ (π₯ = π β ((πβπ₯) < (πβπ¦) β (πβπ) < (πβπ¦))) |
259 | 256, 258 | bibi12d 346 |
. . . . . . . . 9
β’ (π₯ = π β ((π₯ < π¦ β (πβπ₯) < (πβπ¦)) β (π < π¦ β (πβπ) < (πβπ¦)))) |
260 | | breq2 5114 |
. . . . . . . . . 10
β’ (π¦ = (π + 1) β (π < π¦ β π < (π + 1))) |
261 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π¦ = (π + 1) β (πβπ¦) = (πβ(π + 1))) |
262 | 261 | breq2d 5122 |
. . . . . . . . . 10
β’ (π¦ = (π + 1) β ((πβπ) < (πβπ¦) β (πβπ) < (πβ(π + 1)))) |
263 | 260, 262 | bibi12d 346 |
. . . . . . . . 9
β’ (π¦ = (π + 1) β ((π < π¦ β (πβπ) < (πβπ¦)) β (π < (π + 1) β (πβπ) < (πβ(π + 1))))) |
264 | 259, 263 | rspc2v 3593 |
. . . . . . . 8
β’ ((π β (0...π) β§ (π + 1) β (0...π)) β (βπ₯ β (0...π)βπ¦ β (0...π)(π₯ < π¦ β (πβπ₯) < (πβπ¦)) β (π < (π + 1) β (πβπ) < (πβ(π + 1))))) |
265 | 253, 255,
264 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (βπ₯ β (0...π)βπ¦ β (0...π)(π₯ < π¦ β (πβπ₯) < (πβπ¦)) β (π < (π + 1) β (πβπ) < (πβ(π + 1))))) |
266 | 251, 265 | mpd 15 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (π < (π + 1) β (πβπ) < (πβ(π + 1)))) |
267 | 250, 266 | mpbid 231 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
268 | 267 | ralrimiva 3144 |
. . . 4
β’ (π β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
269 | 200, 246,
268 | jca31 516 |
. . 3
β’ (π β (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))) |
270 | | fourierdlem54.o |
. . . . 5
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
271 | 270 | fourierdlem2 44424 |
. . . 4
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
272 | 97, 271 | syl 17 |
. . 3
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
273 | 119, 269,
272 | mpbir2and 712 |
. 2
β’ (π β π β (πβπ)) |
274 | 97, 273, 107 | jca31 516 |
1
β’ (π β ((π β β β§ π β (πβπ)) β§ π Isom < , < ((0...π), π»))) |