Step | Hyp | Ref
| Expression |
1 | | fourierdlem11.q |
. . . . . . 7
β’ (π β π β (πβπ)) |
2 | | fourierdlem11.m |
. . . . . . . 8
β’ (π β π β β) |
3 | | fourierdlem11.p |
. . . . . . . . 9
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
4 | 3 | fourierdlem2 44436 |
. . . . . . . 8
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
5 | 2, 4 | syl 17 |
. . . . . . 7
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
6 | 1, 5 | mpbid 231 |
. . . . . 6
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
7 | 6 | simprd 497 |
. . . . 5
β’ (π β (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))) |
8 | 7 | simpld 496 |
. . . 4
β’ (π β ((πβ0) = π΄ β§ (πβπ) = π΅)) |
9 | 8 | simpld 496 |
. . 3
β’ (π β (πβ0) = π΄) |
10 | 6 | simpld 496 |
. . . . 5
β’ (π β π β (β βm
(0...π))) |
11 | | elmapi 8790 |
. . . . 5
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
12 | 10, 11 | syl 17 |
. . . 4
β’ (π β π:(0...π)βΆβ) |
13 | | 0zd 12516 |
. . . . 5
β’ (π β 0 β
β€) |
14 | 2 | nnzd 12531 |
. . . . 5
β’ (π β π β β€) |
15 | | 0red 11163 |
. . . . . 6
β’ (π β 0 β
β) |
16 | 15 | leidd 11726 |
. . . . 5
β’ (π β 0 β€ 0) |
17 | 2 | nnred 12173 |
. . . . . 6
β’ (π β π β β) |
18 | 2 | nngt0d 12207 |
. . . . . 6
β’ (π β 0 < π) |
19 | 15, 17, 18 | ltled 11308 |
. . . . 5
β’ (π β 0 β€ π) |
20 | 13, 14, 13, 16, 19 | elfzd 13438 |
. . . 4
β’ (π β 0 β (0...π)) |
21 | 12, 20 | ffvelcdmd 7037 |
. . 3
β’ (π β (πβ0) β β) |
22 | 9, 21 | eqeltrrd 2835 |
. 2
β’ (π β π΄ β β) |
23 | 8 | simprd 497 |
. . 3
β’ (π β (πβπ) = π΅) |
24 | 17 | leidd 11726 |
. . . . 5
β’ (π β π β€ π) |
25 | 13, 14, 14, 19, 24 | elfzd 13438 |
. . . 4
β’ (π β π β (0...π)) |
26 | 12, 25 | ffvelcdmd 7037 |
. . 3
β’ (π β (πβπ) β β) |
27 | 23, 26 | eqeltrrd 2835 |
. 2
β’ (π β π΅ β β) |
28 | | 1zzd 12539 |
. . . . 5
β’ (π β 1 β
β€) |
29 | | 0le1 11683 |
. . . . . 6
β’ 0 β€
1 |
30 | 29 | a1i 11 |
. . . . 5
β’ (π β 0 β€ 1) |
31 | 2 | nnge1d 12206 |
. . . . 5
β’ (π β 1 β€ π) |
32 | 13, 14, 28, 30, 31 | elfzd 13438 |
. . . 4
β’ (π β 1 β (0...π)) |
33 | 12, 32 | ffvelcdmd 7037 |
. . 3
β’ (π β (πβ1) β β) |
34 | | elfzo 13580 |
. . . . . . 7
β’ ((0
β β€ β§ 0 β β€ β§ π β β€) β (0 β (0..^π) β (0 β€ 0 β§ 0 <
π))) |
35 | 13, 13, 14, 34 | syl3anc 1372 |
. . . . . 6
β’ (π β (0 β (0..^π) β (0 β€ 0 β§ 0 <
π))) |
36 | 16, 18, 35 | mpbir2and 712 |
. . . . 5
β’ (π β 0 β (0..^π)) |
37 | | 0re 11162 |
. . . . . 6
β’ 0 β
β |
38 | | eleq1 2822 |
. . . . . . . . 9
β’ (π = 0 β (π β (0..^π) β 0 β (0..^π))) |
39 | 38 | anbi2d 630 |
. . . . . . . 8
β’ (π = 0 β ((π β§ π β (0..^π)) β (π β§ 0 β (0..^π)))) |
40 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = 0 β (πβπ) = (πβ0)) |
41 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = 0 β (π + 1) = (0 + 1)) |
42 | 41 | fveq2d 6847 |
. . . . . . . . 9
β’ (π = 0 β (πβ(π + 1)) = (πβ(0 + 1))) |
43 | 40, 42 | breq12d 5119 |
. . . . . . . 8
β’ (π = 0 β ((πβπ) < (πβ(π + 1)) β (πβ0) < (πβ(0 + 1)))) |
44 | 39, 43 | imbi12d 345 |
. . . . . . 7
β’ (π = 0 β (((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) β ((π β§ 0 β (0..^π)) β (πβ0) < (πβ(0 + 1))))) |
45 | 7 | simprd 497 |
. . . . . . . 8
β’ (π β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
46 | 45 | r19.21bi 3233 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
47 | 44, 46 | vtoclg 3524 |
. . . . . 6
β’ (0 β
β β ((π β§ 0
β (0..^π)) β
(πβ0) < (πβ(0 +
1)))) |
48 | 37, 47 | ax-mp 5 |
. . . . 5
β’ ((π β§ 0 β (0..^π)) β (πβ0) < (πβ(0 + 1))) |
49 | 36, 48 | mpdan 686 |
. . . 4
β’ (π β (πβ0) < (πβ(0 + 1))) |
50 | | 0p1e1 12280 |
. . . . . 6
β’ (0 + 1) =
1 |
51 | 50 | a1i 11 |
. . . . 5
β’ (π β (0 + 1) =
1) |
52 | 51 | fveq2d 6847 |
. . . 4
β’ (π β (πβ(0 + 1)) = (πβ1)) |
53 | 49, 9, 52 | 3brtr3d 5137 |
. . 3
β’ (π β π΄ < (πβ1)) |
54 | | nnuz 12811 |
. . . . . 6
β’ β =
(β€β₯β1) |
55 | 2, 54 | eleqtrdi 2844 |
. . . . 5
β’ (π β π β
(β€β₯β1)) |
56 | 12 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (1...π)) β π:(0...π)βΆβ) |
57 | | 0zd 12516 |
. . . . . . . 8
β’ (π β (1...π) β 0 β β€) |
58 | | elfzel2 13445 |
. . . . . . . 8
β’ (π β (1...π) β π β β€) |
59 | | elfzelz 13447 |
. . . . . . . 8
β’ (π β (1...π) β π β β€) |
60 | | 0red 11163 |
. . . . . . . . 9
β’ (π β (1...π) β 0 β β) |
61 | 59 | zred 12612 |
. . . . . . . . 9
β’ (π β (1...π) β π β β) |
62 | | 1red 11161 |
. . . . . . . . . 10
β’ (π β (1...π) β 1 β β) |
63 | | 0lt1 11682 |
. . . . . . . . . . 11
β’ 0 <
1 |
64 | 63 | a1i 11 |
. . . . . . . . . 10
β’ (π β (1...π) β 0 < 1) |
65 | | elfzle1 13450 |
. . . . . . . . . 10
β’ (π β (1...π) β 1 β€ π) |
66 | 60, 62, 61, 64, 65 | ltletrd 11320 |
. . . . . . . . 9
β’ (π β (1...π) β 0 < π) |
67 | 60, 61, 66 | ltled 11308 |
. . . . . . . 8
β’ (π β (1...π) β 0 β€ π) |
68 | | elfzle2 13451 |
. . . . . . . 8
β’ (π β (1...π) β π β€ π) |
69 | 57, 58, 59, 67, 68 | elfzd 13438 |
. . . . . . 7
β’ (π β (1...π) β π β (0...π)) |
70 | 69 | adantl 483 |
. . . . . 6
β’ ((π β§ π β (1...π)) β π β (0...π)) |
71 | 56, 70 | ffvelcdmd 7037 |
. . . . 5
β’ ((π β§ π β (1...π)) β (πβπ) β β) |
72 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (1...(π β 1))) β π:(0...π)βΆβ) |
73 | | 0zd 12516 |
. . . . . . . 8
β’ ((π β§ π β (1...(π β 1))) β 0 β
β€) |
74 | 14 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (1...(π β 1))) β π β β€) |
75 | | elfzelz 13447 |
. . . . . . . . 9
β’ (π β (1...(π β 1)) β π β β€) |
76 | 75 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (1...(π β 1))) β π β β€) |
77 | | 0red 11163 |
. . . . . . . . . 10
β’ (π β (1...(π β 1)) β 0 β
β) |
78 | 75 | zred 12612 |
. . . . . . . . . 10
β’ (π β (1...(π β 1)) β π β β) |
79 | | 1red 11161 |
. . . . . . . . . . 11
β’ (π β (1...(π β 1)) β 1 β
β) |
80 | 63 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (1...(π β 1)) β 0 <
1) |
81 | | elfzle1 13450 |
. . . . . . . . . . 11
β’ (π β (1...(π β 1)) β 1 β€ π) |
82 | 77, 79, 78, 80, 81 | ltletrd 11320 |
. . . . . . . . . 10
β’ (π β (1...(π β 1)) β 0 < π) |
83 | 77, 78, 82 | ltled 11308 |
. . . . . . . . 9
β’ (π β (1...(π β 1)) β 0 β€ π) |
84 | 83 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (1...(π β 1))) β 0 β€ π) |
85 | 78 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (1...(π β 1))) β π β β) |
86 | 17 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (1...(π β 1))) β π β β) |
87 | | peano2rem 11473 |
. . . . . . . . . . 11
β’ (π β β β (π β 1) β
β) |
88 | 86, 87 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(π β 1))) β (π β 1) β β) |
89 | | elfzle2 13451 |
. . . . . . . . . . 11
β’ (π β (1...(π β 1)) β π β€ (π β 1)) |
90 | 89 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(π β 1))) β π β€ (π β 1)) |
91 | 86 | ltm1d 12092 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(π β 1))) β (π β 1) < π) |
92 | 85, 88, 86, 90, 91 | lelttrd 11318 |
. . . . . . . . 9
β’ ((π β§ π β (1...(π β 1))) β π < π) |
93 | 85, 86, 92 | ltled 11308 |
. . . . . . . 8
β’ ((π β§ π β (1...(π β 1))) β π β€ π) |
94 | 73, 74, 76, 84, 93 | elfzd 13438 |
. . . . . . 7
β’ ((π β§ π β (1...(π β 1))) β π β (0...π)) |
95 | 72, 94 | ffvelcdmd 7037 |
. . . . . 6
β’ ((π β§ π β (1...(π β 1))) β (πβπ) β β) |
96 | 76 | peano2zd 12615 |
. . . . . . . 8
β’ ((π β§ π β (1...(π β 1))) β (π + 1) β β€) |
97 | | 0red 11163 |
. . . . . . . . 9
β’ ((π β§ π β (1...(π β 1))) β 0 β
β) |
98 | | peano2re 11333 |
. . . . . . . . . 10
β’ (π β β β (π + 1) β
β) |
99 | 85, 98 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β (1...(π β 1))) β (π + 1) β β) |
100 | | 1red 11161 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(π β 1))) β 1 β
β) |
101 | 63 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(π β 1))) β 0 <
1) |
102 | 78, 98 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (1...(π β 1)) β (π + 1) β β) |
103 | 78 | ltp1d 12090 |
. . . . . . . . . . . 12
β’ (π β (1...(π β 1)) β π < (π + 1)) |
104 | 79, 78, 102, 81, 103 | lelttrd 11318 |
. . . . . . . . . . 11
β’ (π β (1...(π β 1)) β 1 < (π + 1)) |
105 | 104 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(π β 1))) β 1 < (π + 1)) |
106 | 97, 100, 99, 101, 105 | lttrd 11321 |
. . . . . . . . 9
β’ ((π β§ π β (1...(π β 1))) β 0 < (π + 1)) |
107 | 97, 99, 106 | ltled 11308 |
. . . . . . . 8
β’ ((π β§ π β (1...(π β 1))) β 0 β€ (π + 1)) |
108 | 85, 88, 100, 90 | leadd1dd 11774 |
. . . . . . . . 9
β’ ((π β§ π β (1...(π β 1))) β (π + 1) β€ ((π β 1) + 1)) |
109 | 2 | nncnd 12174 |
. . . . . . . . . . 11
β’ (π β π β β) |
110 | | 1cnd 11155 |
. . . . . . . . . . 11
β’ (π β 1 β
β) |
111 | 109, 110 | npcand 11521 |
. . . . . . . . . 10
β’ (π β ((π β 1) + 1) = π) |
112 | 111 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (1...(π β 1))) β ((π β 1) + 1) = π) |
113 | 108, 112 | breqtrd 5132 |
. . . . . . . 8
β’ ((π β§ π β (1...(π β 1))) β (π + 1) β€ π) |
114 | 73, 74, 96, 107, 113 | elfzd 13438 |
. . . . . . 7
β’ ((π β§ π β (1...(π β 1))) β (π + 1) β (0...π)) |
115 | 72, 114 | ffvelcdmd 7037 |
. . . . . 6
β’ ((π β§ π β (1...(π β 1))) β (πβ(π + 1)) β β) |
116 | | elfzo 13580 |
. . . . . . . . 9
β’ ((π β β€ β§ 0 β
β€ β§ π β
β€) β (π β
(0..^π) β (0 β€
π β§ π < π))) |
117 | 76, 73, 74, 116 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β (1...(π β 1))) β (π β (0..^π) β (0 β€ π β§ π < π))) |
118 | 84, 92, 117 | mpbir2and 712 |
. . . . . . 7
β’ ((π β§ π β (1...(π β 1))) β π β (0..^π)) |
119 | 118, 46 | syldan 592 |
. . . . . 6
β’ ((π β§ π β (1...(π β 1))) β (πβπ) < (πβ(π + 1))) |
120 | 95, 115, 119 | ltled 11308 |
. . . . 5
β’ ((π β§ π β (1...(π β 1))) β (πβπ) β€ (πβ(π + 1))) |
121 | 55, 71, 120 | monoord 13944 |
. . . 4
β’ (π β (πβ1) β€ (πβπ)) |
122 | 121, 23 | breqtrd 5132 |
. . 3
β’ (π β (πβ1) β€ π΅) |
123 | 22, 33, 27, 53, 122 | ltletrd 11320 |
. 2
β’ (π β π΄ < π΅) |
124 | 22, 27, 123 | 3jca 1129 |
1
β’ (π β (π΄ β β β§ π΅ β β β§ π΄ < π΅)) |