Step | Hyp | Ref
| Expression |
1 | | fourierdlem63.e |
. . . . 5
β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
2 | 1 | a1i 11 |
. . . 4
β’ (π β πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)))) |
3 | | id 22 |
. . . . . 6
β’ (π₯ = (πβ(π½ + 1)) β π₯ = (πβ(π½ + 1))) |
4 | | oveq2 7419 |
. . . . . . . . 9
β’ (π₯ = (πβ(π½ + 1)) β (π΅ β π₯) = (π΅ β (πβ(π½ + 1)))) |
5 | 4 | oveq1d 7426 |
. . . . . . . 8
β’ (π₯ = (πβ(π½ + 1)) β ((π΅ β π₯) / π) = ((π΅ β (πβ(π½ + 1))) / π)) |
6 | 5 | fveq2d 6895 |
. . . . . . 7
β’ (π₯ = (πβ(π½ + 1)) β (ββ((π΅ β π₯) / π)) = (ββ((π΅ β (πβ(π½ + 1))) / π))) |
7 | 6 | oveq1d 7426 |
. . . . . 6
β’ (π₯ = (πβ(π½ + 1)) β ((ββ((π΅ β π₯) / π)) Β· π) = ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π)) |
8 | 3, 7 | oveq12d 7429 |
. . . . 5
β’ (π₯ = (πβ(π½ + 1)) β (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) = ((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π))) |
9 | 8 | adantl 482 |
. . . 4
β’ ((π β§ π₯ = (πβ(π½ + 1))) β (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) = ((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π))) |
10 | | fourierdlem63.t |
. . . . . . . . . . 11
β’ π = (π΅ β π΄) |
11 | | fourierdlem63.p |
. . . . . . . . . . 11
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
12 | | fourierdlem63.m |
. . . . . . . . . . 11
β’ (π β π β β) |
13 | | fourierdlem63.q |
. . . . . . . . . . 11
β’ (π β π β (πβπ)) |
14 | | fourierdlem63.c |
. . . . . . . . . . 11
β’ (π β πΆ β β) |
15 | | fourierdlem63.d |
. . . . . . . . . . 11
β’ (π β π· β β) |
16 | | fourierdlem63.cltd |
. . . . . . . . . . 11
β’ (π β πΆ < π·) |
17 | | fourierdlem63.o |
. . . . . . . . . . 11
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
18 | | fourierdlem63.h |
. . . . . . . . . . 11
β’ π» = ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) |
19 | | fourierdlem63.n |
. . . . . . . . . . 11
β’ π = ((β―βπ») β 1) |
20 | | fourierdlem63.s |
. . . . . . . . . . 11
β’ π = (β©ππ Isom < , < ((0...π), π»)) |
21 | 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20 | fourierdlem54 44961 |
. . . . . . . . . 10
β’ (π β ((π β β β§ π β (πβπ)) β§ π Isom < , < ((0...π), π»))) |
22 | 21 | simpld 495 |
. . . . . . . . 9
β’ (π β (π β β β§ π β (πβπ))) |
23 | 22 | simprd 496 |
. . . . . . . 8
β’ (π β π β (πβπ)) |
24 | 22 | simpld 495 |
. . . . . . . . 9
β’ (π β π β β) |
25 | 17 | fourierdlem2 44910 |
. . . . . . . . 9
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
27 | 23, 26 | mpbid 231 |
. . . . . . 7
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = πΆ β§ (πβπ) = π·) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
28 | 27 | simpld 495 |
. . . . . 6
β’ (π β π β (β βm
(0...π))) |
29 | | elmapi 8845 |
. . . . . 6
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
30 | 28, 29 | syl 17 |
. . . . 5
β’ (π β π:(0...π)βΆβ) |
31 | | fourierdlem63.j |
. . . . . 6
β’ (π β π½ β (0..^π)) |
32 | | fzofzp1 13731 |
. . . . . 6
β’ (π½ β (0..^π) β (π½ + 1) β (0...π)) |
33 | 31, 32 | syl 17 |
. . . . 5
β’ (π β (π½ + 1) β (0...π)) |
34 | 30, 33 | ffvelcdmd 7087 |
. . . 4
β’ (π β (πβ(π½ + 1)) β β) |
35 | 11, 12, 13 | fourierdlem11 44919 |
. . . . . . . . . . 11
β’ (π β (π΄ β β β§ π΅ β β β§ π΄ < π΅)) |
36 | 35 | simp2d 1143 |
. . . . . . . . . 10
β’ (π β π΅ β β) |
37 | 36, 34 | resubcld 11644 |
. . . . . . . . 9
β’ (π β (π΅ β (πβ(π½ + 1))) β β) |
38 | 35 | simp1d 1142 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
39 | 36, 38 | resubcld 11644 |
. . . . . . . . . 10
β’ (π β (π΅ β π΄) β β) |
40 | 10, 39 | eqeltrid 2837 |
. . . . . . . . 9
β’ (π β π β β) |
41 | 35 | simp3d 1144 |
. . . . . . . . . . . 12
β’ (π β π΄ < π΅) |
42 | 38, 36 | posdifd 11803 |
. . . . . . . . . . . 12
β’ (π β (π΄ < π΅ β 0 < (π΅ β π΄))) |
43 | 41, 42 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β 0 < (π΅ β π΄)) |
44 | 43, 10 | breqtrrdi 5190 |
. . . . . . . . . 10
β’ (π β 0 < π) |
45 | 44 | gt0ne0d 11780 |
. . . . . . . . 9
β’ (π β π β 0) |
46 | 37, 40, 45 | redivcld 12044 |
. . . . . . . 8
β’ (π β ((π΅ β (πβ(π½ + 1))) / π) β β) |
47 | 46 | flcld 13765 |
. . . . . . 7
β’ (π β (ββ((π΅ β (πβ(π½ + 1))) / π)) β β€) |
48 | 47 | zred 12668 |
. . . . . 6
β’ (π β (ββ((π΅ β (πβ(π½ + 1))) / π)) β β) |
49 | 48, 40 | remulcld 11246 |
. . . . 5
β’ (π β ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π) β β) |
50 | 34, 49 | readdcld 11245 |
. . . 4
β’ (π β ((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π)) β β) |
51 | 2, 9, 34, 50 | fvmptd 7005 |
. . 3
β’ (π β (πΈβ(πβ(π½ + 1))) = ((πβ(π½ + 1)) + ((ββ((π΅ β (πβ(π½ + 1))) / π)) Β· π))) |
52 | 51, 50 | eqeltrd 2833 |
. 2
β’ (π β (πΈβ(πβ(π½ + 1))) β β) |
53 | 11 | fourierdlem2 44910 |
. . . . . . 7
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
54 | 12, 53 | syl 17 |
. . . . . 6
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
55 | 13, 54 | mpbid 231 |
. . . . 5
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
56 | 55 | simpld 495 |
. . . 4
β’ (π β π β (β βm
(0...π))) |
57 | | elmapi 8845 |
. . . 4
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
58 | 56, 57 | syl 17 |
. . 3
β’ (π β π:(0...π)βΆβ) |
59 | | fourierdlem63.k |
. . 3
β’ (π β πΎ β (0...π)) |
60 | 58, 59 | ffvelcdmd 7087 |
. 2
β’ (π β (πβπΎ) β β) |
61 | 14 | adantr 481 |
. . . . . . 7
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β πΆ β β) |
62 | 15 | adantr 481 |
. . . . . . 7
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β π· β β) |
63 | 38 | rexrd 11266 |
. . . . . . . . . . . 12
β’ (π β π΄ β
β*) |
64 | | iocssre 13406 |
. . . . . . . . . . . 12
β’ ((π΄ β β*
β§ π΅ β β)
β (π΄(,]π΅) β
β) |
65 | 63, 36, 64 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β (π΄(,]π΅) β β) |
66 | 38, 36, 41, 10, 1 | fourierdlem4 44912 |
. . . . . . . . . . . 12
β’ (π β πΈ:ββΆ(π΄(,]π΅)) |
67 | | fourierdlem63.y |
. . . . . . . . . . . . . 14
β’ (π β π β ((πβπ½)[,)(πβ(π½ + 1)))) |
68 | | elfzofz 13650 |
. . . . . . . . . . . . . . . . 17
β’ (π½ β (0..^π) β π½ β (0...π)) |
69 | 31, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π½ β (0...π)) |
70 | 30, 69 | ffvelcdmd 7087 |
. . . . . . . . . . . . . . 15
β’ (π β (πβπ½) β β) |
71 | 34 | rexrd 11266 |
. . . . . . . . . . . . . . 15
β’ (π β (πβ(π½ + 1)) β
β*) |
72 | | elico2 13390 |
. . . . . . . . . . . . . . 15
β’ (((πβπ½) β β β§ (πβ(π½ + 1)) β β*) β
(π β ((πβπ½)[,)(πβ(π½ + 1))) β (π β β β§ (πβπ½) β€ π β§ π < (πβ(π½ + 1))))) |
73 | 70, 71, 72 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ (π β (π β ((πβπ½)[,)(πβ(π½ + 1))) β (π β β β§ (πβπ½) β€ π β§ π < (πβ(π½ + 1))))) |
74 | 67, 73 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (π β (π β β β§ (πβπ½) β€ π β§ π < (πβ(π½ + 1)))) |
75 | 74 | simp1d 1142 |
. . . . . . . . . . . 12
β’ (π β π β β) |
76 | 66, 75 | ffvelcdmd 7087 |
. . . . . . . . . . 11
β’ (π β (πΈβπ) β (π΄(,]π΅)) |
77 | 65, 76 | sseldd 3983 |
. . . . . . . . . 10
β’ (π β (πΈβπ) β β) |
78 | 77, 75 | resubcld 11644 |
. . . . . . . . 9
β’ (π β ((πΈβπ) β π) β β) |
79 | 60, 78 | resubcld 11644 |
. . . . . . . 8
β’ (π β ((πβπΎ) β ((πΈβπ) β π)) β β) |
80 | 79 | adantr 481 |
. . . . . . 7
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβπΎ) β ((πΈβπ) β π)) β β) |
81 | | icossicc 13415 |
. . . . . . . . . . . . . 14
β’ ((πβπ½)[,)(πβ(π½ + 1))) β ((πβπ½)[,](πβ(π½ + 1))) |
82 | 14 | rexrd 11266 |
. . . . . . . . . . . . . . 15
β’ (π β πΆ β
β*) |
83 | 15 | rexrd 11266 |
. . . . . . . . . . . . . . 15
β’ (π β π· β
β*) |
84 | 17, 24, 23 | fourierdlem15 44923 |
. . . . . . . . . . . . . . 15
β’ (π β π:(0...π)βΆ(πΆ[,]π·)) |
85 | 82, 83, 84, 31 | fourierdlem8 44916 |
. . . . . . . . . . . . . 14
β’ (π β ((πβπ½)[,](πβ(π½ + 1))) β (πΆ[,]π·)) |
86 | 81, 85 | sstrid 3993 |
. . . . . . . . . . . . 13
β’ (π β ((πβπ½)[,)(πβ(π½ + 1))) β (πΆ[,]π·)) |
87 | 86, 67 | sseldd 3983 |
. . . . . . . . . . . 12
β’ (π β π β (πΆ[,]π·)) |
88 | | elicc2 13391 |
. . . . . . . . . . . . 13
β’ ((πΆ β β β§ π· β β) β (π β (πΆ[,]π·) β (π β β β§ πΆ β€ π β§ π β€ π·))) |
89 | 14, 15, 88 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (π β (π β (πΆ[,]π·) β (π β β β§ πΆ β€ π β§ π β€ π·))) |
90 | 87, 89 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (π β β β§ πΆ β€ π β§ π β€ π·)) |
91 | 90 | simp2d 1143 |
. . . . . . . . . 10
β’ (π β πΆ β€ π) |
92 | 60, 77 | resubcld 11644 |
. . . . . . . . . . . . 13
β’ (π β ((πβπΎ) β (πΈβπ)) β β) |
93 | | fourierdlem63.eyltqk |
. . . . . . . . . . . . . 14
β’ (π β (πΈβπ) < (πβπΎ)) |
94 | 77, 60 | posdifd 11803 |
. . . . . . . . . . . . . 14
β’ (π β ((πΈβπ) < (πβπΎ) β 0 < ((πβπΎ) β (πΈβπ)))) |
95 | 93, 94 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (π β 0 < ((πβπΎ) β (πΈβπ))) |
96 | 92, 95 | elrpd 13015 |
. . . . . . . . . . . 12
β’ (π β ((πβπΎ) β (πΈβπ)) β
β+) |
97 | 75, 96 | ltaddrpd 13051 |
. . . . . . . . . . 11
β’ (π β π < (π + ((πβπΎ) β (πΈβπ)))) |
98 | 60 | recnd 11244 |
. . . . . . . . . . . . 13
β’ (π β (πβπΎ) β β) |
99 | 77 | recnd 11244 |
. . . . . . . . . . . . 13
β’ (π β (πΈβπ) β β) |
100 | 75 | recnd 11244 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
101 | 98, 99, 100 | subsub3d 11603 |
. . . . . . . . . . . 12
β’ (π β ((πβπΎ) β ((πΈβπ) β π)) = (((πβπΎ) + π) β (πΈβπ))) |
102 | 98, 100 | addcomd 11418 |
. . . . . . . . . . . . 13
β’ (π β ((πβπΎ) + π) = (π + (πβπΎ))) |
103 | 102 | oveq1d 7426 |
. . . . . . . . . . . 12
β’ (π β (((πβπΎ) + π) β (πΈβπ)) = ((π + (πβπΎ)) β (πΈβπ))) |
104 | 100, 98, 99 | addsubassd 11593 |
. . . . . . . . . . . 12
β’ (π β ((π + (πβπΎ)) β (πΈβπ)) = (π + ((πβπΎ) β (πΈβπ)))) |
105 | 101, 103,
104 | 3eqtrrd 2777 |
. . . . . . . . . . 11
β’ (π β (π + ((πβπΎ) β (πΈβπ))) = ((πβπΎ) β ((πΈβπ) β π))) |
106 | 97, 105 | breqtrd 5174 |
. . . . . . . . . 10
β’ (π β π < ((πβπΎ) β ((πΈβπ) β π))) |
107 | 14, 75, 79, 91, 106 | lelttrd 11374 |
. . . . . . . . 9
β’ (π β πΆ < ((πβπΎ) β ((πΈβπ) β π))) |
108 | 14, 79, 107 | ltled 11364 |
. . . . . . . 8
β’ (π β πΆ β€ ((πβπΎ) β ((πΈβπ) β π))) |
109 | 108 | adantr 481 |
. . . . . . 7
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β πΆ β€ ((πβπΎ) β ((πΈβπ) β π))) |
110 | 34 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β (πβ(π½ + 1)) β β) |
111 | 60 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β (πβπΎ) β β) |
112 | 52, 34 | resubcld 11644 |
. . . . . . . . . . . 12
β’ (π β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) β β) |
113 | 112 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) β β) |
114 | 111, 113 | resubcld 11644 |
. . . . . . . . . 10
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβπΎ) β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1)))) β β) |
115 | 74 | simp3d 1144 |
. . . . . . . . . . . . . 14
β’ (π β π < (πβ(π½ + 1))) |
116 | 75, 34, 115 | ltled 11364 |
. . . . . . . . . . . . 13
β’ (π β π β€ (πβ(π½ + 1))) |
117 | 38, 36, 41, 10, 1, 75, 34, 116 | fourierdlem7 44915 |
. . . . . . . . . . . 12
β’ (π β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))) β€ ((πΈβπ) β π)) |
118 | 112, 78, 60, 117 | lesub2dd 11833 |
. . . . . . . . . . 11
β’ (π β ((πβπΎ) β ((πΈβπ) β π)) β€ ((πβπΎ) β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))))) |
119 | 118 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβπΎ) β ((πΈβπ) β π)) β€ ((πβπΎ) β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1))))) |
120 | 98 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β (πβπΎ) β β) |
121 | 52 | recnd 11244 |
. . . . . . . . . . . . . 14
β’ (π β (πΈβ(πβ(π½ + 1))) β β) |
122 | 121 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β (πΈβ(πβ(π½ + 1))) β β) |
123 | 110 | recnd 11244 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β (πβ(π½ + 1)) β β) |
124 | 120, 122,
123 | subsubd 11601 |
. . . . . . . . . . . 12
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβπΎ) β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1)))) = (((πβπΎ) β (πΈβ(πβ(π½ + 1)))) + (πβ(π½ + 1)))) |
125 | 98, 121 | subcld 11573 |
. . . . . . . . . . . . . 14
β’ (π β ((πβπΎ) β (πΈβ(πβ(π½ + 1)))) β β) |
126 | 34 | recnd 11244 |
. . . . . . . . . . . . . 14
β’ (π β (πβ(π½ + 1)) β β) |
127 | 125, 126 | addcomd 11418 |
. . . . . . . . . . . . 13
β’ (π β (((πβπΎ) β (πΈβ(πβ(π½ + 1)))) + (πβ(π½ + 1))) = ((πβ(π½ + 1)) + ((πβπΎ) β (πΈβ(πβ(π½ + 1)))))) |
128 | 127 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β (((πβπΎ) β (πΈβ(πβ(π½ + 1)))) + (πβ(π½ + 1))) = ((πβ(π½ + 1)) + ((πβπΎ) β (πΈβ(πβ(π½ + 1)))))) |
129 | 124, 128 | eqtrd 2772 |
. . . . . . . . . . 11
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβπΎ) β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1)))) = ((πβ(π½ + 1)) + ((πβπΎ) β (πΈβ(πβ(π½ + 1)))))) |
130 | | simpr 485 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β (πβπΎ) < (πΈβ(πβ(π½ + 1)))) |
131 | 52 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β (πΈβ(πβ(π½ + 1))) β β) |
132 | 111, 131 | sublt0d 11842 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β (((πβπΎ) β (πΈβ(πβ(π½ + 1)))) < 0 β (πβπΎ) < (πΈβ(πβ(π½ + 1))))) |
133 | 130, 132 | mpbird 256 |
. . . . . . . . . . . 12
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβπΎ) β (πΈβ(πβ(π½ + 1)))) < 0) |
134 | 111, 131 | resubcld 11644 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβπΎ) β (πΈβ(πβ(π½ + 1)))) β β) |
135 | | ltaddneg 11431 |
. . . . . . . . . . . . 13
β’ ((((πβπΎ) β (πΈβ(πβ(π½ + 1)))) β β β§ (πβ(π½ + 1)) β β) β (((πβπΎ) β (πΈβ(πβ(π½ + 1)))) < 0 β ((πβ(π½ + 1)) + ((πβπΎ) β (πΈβ(πβ(π½ + 1))))) < (πβ(π½ + 1)))) |
136 | 134, 110,
135 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β (((πβπΎ) β (πΈβ(πβ(π½ + 1)))) < 0 β ((πβ(π½ + 1)) + ((πβπΎ) β (πΈβ(πβ(π½ + 1))))) < (πβ(π½ + 1)))) |
137 | 133, 136 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβ(π½ + 1)) + ((πβπΎ) β (πΈβ(πβ(π½ + 1))))) < (πβ(π½ + 1))) |
138 | 129, 137 | eqbrtrd 5170 |
. . . . . . . . . 10
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβπΎ) β ((πΈβ(πβ(π½ + 1))) β (πβ(π½ + 1)))) < (πβ(π½ + 1))) |
139 | 80, 114, 110, 119, 138 | lelttrd 11374 |
. . . . . . . . 9
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβπΎ) β ((πΈβπ) β π)) < (πβ(π½ + 1))) |
140 | 84, 33 | ffvelcdmd 7087 |
. . . . . . . . . . . 12
β’ (π β (πβ(π½ + 1)) β (πΆ[,]π·)) |
141 | | elicc2 13391 |
. . . . . . . . . . . . 13
β’ ((πΆ β β β§ π· β β) β ((πβ(π½ + 1)) β (πΆ[,]π·) β ((πβ(π½ + 1)) β β β§ πΆ β€ (πβ(π½ + 1)) β§ (πβ(π½ + 1)) β€ π·))) |
142 | 14, 15, 141 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (π β ((πβ(π½ + 1)) β (πΆ[,]π·) β ((πβ(π½ + 1)) β β β§ πΆ β€ (πβ(π½ + 1)) β§ (πβ(π½ + 1)) β€ π·))) |
143 | 140, 142 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β ((πβ(π½ + 1)) β β β§ πΆ β€ (πβ(π½ + 1)) β§ (πβ(π½ + 1)) β€ π·)) |
144 | 143 | simp3d 1144 |
. . . . . . . . . 10
β’ (π β (πβ(π½ + 1)) β€ π·) |
145 | 144 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β (πβ(π½ + 1)) β€ π·) |
146 | 80, 110, 62, 139, 145 | ltletrd 11376 |
. . . . . . . 8
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβπΎ) β ((πΈβπ) β π)) < π·) |
147 | 80, 62, 146 | ltled 11364 |
. . . . . . 7
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβπΎ) β ((πΈβπ) β π)) β€ π·) |
148 | 61, 62, 80, 109, 147 | eliccd 44302 |
. . . . . 6
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβπΎ) β ((πΈβπ) β π)) β (πΆ[,]π·)) |
149 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β π₯ = π) |
150 | | oveq2 7419 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β (π΅ β π₯) = (π΅ β π)) |
151 | 150 | oveq1d 7426 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β ((π΅ β π₯) / π) = ((π΅ β π) / π)) |
152 | 151 | fveq2d 6895 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (ββ((π΅ β π₯) / π)) = (ββ((π΅ β π) / π))) |
153 | 152 | oveq1d 7426 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β ((ββ((π΅ β π₯) / π)) Β· π) = ((ββ((π΅ β π) / π)) Β· π)) |
154 | 149, 153 | oveq12d 7429 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) = (π + ((ββ((π΅ β π) / π)) Β· π))) |
155 | 154 | adantl 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ = π) β (π₯ + ((ββ((π΅ β π₯) / π)) Β· π)) = (π + ((ββ((π΅ β π) / π)) Β· π))) |
156 | 36, 75 | resubcld 11644 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΅ β π) β β) |
157 | 156, 40, 45 | redivcld 12044 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π΅ β π) / π) β β) |
158 | 157 | flcld 13765 |
. . . . . . . . . . . . . . . 16
β’ (π β (ββ((π΅ β π) / π)) β β€) |
159 | 158 | zred 12668 |
. . . . . . . . . . . . . . 15
β’ (π β (ββ((π΅ β π) / π)) β β) |
160 | 159, 40 | remulcld 11246 |
. . . . . . . . . . . . . 14
β’ (π β ((ββ((π΅ β π) / π)) Β· π) β β) |
161 | 75, 160 | readdcld 11245 |
. . . . . . . . . . . . 13
β’ (π β (π + ((ββ((π΅ β π) / π)) Β· π)) β β) |
162 | 2, 155, 75, 161 | fvmptd 7005 |
. . . . . . . . . . . 12
β’ (π β (πΈβπ) = (π + ((ββ((π΅ β π) / π)) Β· π))) |
163 | 162 | oveq1d 7426 |
. . . . . . . . . . 11
β’ (π β ((πΈβπ) β π) = ((π + ((ββ((π΅ β π) / π)) Β· π)) β π)) |
164 | 163 | oveq1d 7426 |
. . . . . . . . . 10
β’ (π β (((πΈβπ) β π) / π) = (((π + ((ββ((π΅ β π) / π)) Β· π)) β π) / π)) |
165 | 160 | recnd 11244 |
. . . . . . . . . . . 12
β’ (π β ((ββ((π΅ β π) / π)) Β· π) β β) |
166 | 100, 165 | pncan2d 11575 |
. . . . . . . . . . 11
β’ (π β ((π + ((ββ((π΅ β π) / π)) Β· π)) β π) = ((ββ((π΅ β π) / π)) Β· π)) |
167 | 166 | oveq1d 7426 |
. . . . . . . . . 10
β’ (π β (((π + ((ββ((π΅ β π) / π)) Β· π)) β π) / π) = (((ββ((π΅ β π) / π)) Β· π) / π)) |
168 | 159 | recnd 11244 |
. . . . . . . . . . 11
β’ (π β (ββ((π΅ β π) / π)) β β) |
169 | 40 | recnd 11244 |
. . . . . . . . . . 11
β’ (π β π β β) |
170 | 168, 169,
45 | divcan4d 11998 |
. . . . . . . . . 10
β’ (π β (((ββ((π΅ β π) / π)) Β· π) / π) = (ββ((π΅ β π) / π))) |
171 | 164, 167,
170 | 3eqtrd 2776 |
. . . . . . . . 9
β’ (π β (((πΈβπ) β π) / π) = (ββ((π΅ β π) / π))) |
172 | 171, 158 | eqeltrd 2833 |
. . . . . . . 8
β’ (π β (((πΈβπ) β π) / π) β β€) |
173 | 78 | recnd 11244 |
. . . . . . . . . . . 12
β’ (π β ((πΈβπ) β π) β β) |
174 | 173, 169,
45 | divcan1d 11993 |
. . . . . . . . . . 11
β’ (π β ((((πΈβπ) β π) / π) Β· π) = ((πΈβπ) β π)) |
175 | 174 | oveq2d 7427 |
. . . . . . . . . 10
β’ (π β (((πβπΎ) β ((πΈβπ) β π)) + ((((πΈβπ) β π) / π) Β· π)) = (((πβπΎ) β ((πΈβπ) β π)) + ((πΈβπ) β π))) |
176 | 98, 173 | npcand 11577 |
. . . . . . . . . 10
β’ (π β (((πβπΎ) β ((πΈβπ) β π)) + ((πΈβπ) β π)) = (πβπΎ)) |
177 | 175, 176 | eqtrd 2772 |
. . . . . . . . 9
β’ (π β (((πβπΎ) β ((πΈβπ) β π)) + ((((πΈβπ) β π) / π) Β· π)) = (πβπΎ)) |
178 | | ffun 6720 |
. . . . . . . . . . 11
β’ (π:(0...π)βΆβ β Fun π) |
179 | 58, 178 | syl 17 |
. . . . . . . . . 10
β’ (π β Fun π) |
180 | 58 | fdmd 6728 |
. . . . . . . . . . 11
β’ (π β dom π = (0...π)) |
181 | 59, 180 | eleqtrrd 2836 |
. . . . . . . . . 10
β’ (π β πΎ β dom π) |
182 | | fvelrn 7078 |
. . . . . . . . . 10
β’ ((Fun
π β§ πΎ β dom π) β (πβπΎ) β ran π) |
183 | 179, 181,
182 | syl2anc 584 |
. . . . . . . . 9
β’ (π β (πβπΎ) β ran π) |
184 | 177, 183 | eqeltrd 2833 |
. . . . . . . 8
β’ (π β (((πβπΎ) β ((πΈβπ) β π)) + ((((πΈβπ) β π) / π) Β· π)) β ran π) |
185 | | oveq1 7418 |
. . . . . . . . . . 11
β’ (π = (((πΈβπ) β π) / π) β (π Β· π) = ((((πΈβπ) β π) / π) Β· π)) |
186 | 185 | oveq2d 7427 |
. . . . . . . . . 10
β’ (π = (((πΈβπ) β π) / π) β (((πβπΎ) β ((πΈβπ) β π)) + (π Β· π)) = (((πβπΎ) β ((πΈβπ) β π)) + ((((πΈβπ) β π) / π) Β· π))) |
187 | 186 | eleq1d 2818 |
. . . . . . . . 9
β’ (π = (((πΈβπ) β π) / π) β ((((πβπΎ) β ((πΈβπ) β π)) + (π Β· π)) β ran π β (((πβπΎ) β ((πΈβπ) β π)) + ((((πΈβπ) β π) / π) Β· π)) β ran π)) |
188 | 187 | rspcev 3612 |
. . . . . . . 8
β’
(((((πΈβπ) β π) / π) β β€ β§ (((πβπΎ) β ((πΈβπ) β π)) + ((((πΈβπ) β π) / π) Β· π)) β ran π) β βπ β β€ (((πβπΎ) β ((πΈβπ) β π)) + (π Β· π)) β ran π) |
189 | 172, 184,
188 | syl2anc 584 |
. . . . . . 7
β’ (π β βπ β β€ (((πβπΎ) β ((πΈβπ) β π)) + (π Β· π)) β ran π) |
190 | 189 | adantr 481 |
. . . . . 6
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β βπ β β€ (((πβπΎ) β ((πΈβπ) β π)) + (π Β· π)) β ran π) |
191 | | oveq1 7418 |
. . . . . . . . 9
β’ (π₯ = ((πβπΎ) β ((πΈβπ) β π)) β (π₯ + (π Β· π)) = (((πβπΎ) β ((πΈβπ) β π)) + (π Β· π))) |
192 | 191 | eleq1d 2818 |
. . . . . . . 8
β’ (π₯ = ((πβπΎ) β ((πΈβπ) β π)) β ((π₯ + (π Β· π)) β ran π β (((πβπΎ) β ((πΈβπ) β π)) + (π Β· π)) β ran π)) |
193 | 192 | rexbidv 3178 |
. . . . . . 7
β’ (π₯ = ((πβπΎ) β ((πΈβπ) β π)) β (βπ β β€ (π₯ + (π Β· π)) β ran π β βπ β β€ (((πβπΎ) β ((πΈβπ) β π)) + (π Β· π)) β ran π)) |
194 | 193 | elrab 3683 |
. . . . . 6
β’ (((πβπΎ) β ((πΈβπ) β π)) β {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π} β (((πβπΎ) β ((πΈβπ) β π)) β (πΆ[,]π·) β§ βπ β β€ (((πβπΎ) β ((πΈβπ) β π)) + (π Β· π)) β ran π)) |
195 | 148, 190,
194 | sylanbrc 583 |
. . . . 5
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβπΎ) β ((πΈβπ) β π)) β {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π}) |
196 | | elun2 4177 |
. . . . 5
β’ (((πβπΎ) β ((πΈβπ) β π)) β {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π} β ((πβπΎ) β ((πΈβπ) β π)) β ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π})) |
197 | 195, 196 | syl 17 |
. . . 4
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β ((πβπΎ) β ((πΈβπ) β π)) β ({πΆ, π·} βͺ {π₯ β (πΆ[,]π·) β£ βπ β β€ (π₯ + (π Β· π)) β ran π})) |
198 | | fourierdlem63.x |
. . . 4
β’ π = ((πβπΎ) β ((πΈβπ) β π)) |
199 | 197, 198,
18 | 3eltr4g 2850 |
. . 3
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β π β π») |
200 | | elfzelz 13503 |
. . . . . . . . 9
β’ (π β (0...π) β π β β€) |
201 | 200 | ad2antlr 725 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ ((πβπ½) < (πβπ) β§ (πβπ) < (πβ(π½ + 1)))) β π β β€) |
202 | | elfzoelz 13634 |
. . . . . . . . . . 11
β’ (π½ β (0..^π) β π½ β β€) |
203 | 31, 202 | syl 17 |
. . . . . . . . . 10
β’ (π β π½ β β€) |
204 | 203 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ ((πβπ½) < (πβπ) β§ (πβπ) < (πβ(π½ + 1)))) β π½ β β€) |
205 | | simpr 485 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ (πβπ½) < (πβπ)) β (πβπ½) < (πβπ)) |
206 | 21 | simprd 496 |
. . . . . . . . . . . . 13
β’ (π β π Isom < , < ((0...π), π»)) |
207 | 206 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ (πβπ½) < (πβπ)) β π Isom < , < ((0...π), π»)) |
208 | 69 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ (πβπ½) < (πβπ)) β π½ β (0...π)) |
209 | | simplr 767 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ (πβπ½) < (πβπ)) β π β (0...π)) |
210 | | isorel 7325 |
. . . . . . . . . . . 12
β’ ((π Isom < , < ((0...π), π») β§ (π½ β (0...π) β§ π β (0...π))) β (π½ < π β (πβπ½) < (πβπ))) |
211 | 207, 208,
209, 210 | syl12anc 835 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ (πβπ½) < (πβπ)) β (π½ < π β (πβπ½) < (πβπ))) |
212 | 205, 211 | mpbird 256 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ (πβπ½) < (πβπ)) β π½ < π) |
213 | 212 | adantrr 715 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ ((πβπ½) < (πβπ) β§ (πβπ) < (πβ(π½ + 1)))) β π½ < π) |
214 | | simpr 485 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ (πβπ) < (πβ(π½ + 1))) β (πβπ) < (πβ(π½ + 1))) |
215 | 206 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ (πβπ) < (πβ(π½ + 1))) β π Isom < , < ((0...π), π»)) |
216 | | simplr 767 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ (πβπ) < (πβ(π½ + 1))) β π β (0...π)) |
217 | 33 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ (πβπ) < (πβ(π½ + 1))) β (π½ + 1) β (0...π)) |
218 | | isorel 7325 |
. . . . . . . . . . . 12
β’ ((π Isom < , < ((0...π), π») β§ (π β (0...π) β§ (π½ + 1) β (0...π))) β (π < (π½ + 1) β (πβπ) < (πβ(π½ + 1)))) |
219 | 215, 216,
217, 218 | syl12anc 835 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ (πβπ) < (πβ(π½ + 1))) β (π < (π½ + 1) β (πβπ) < (πβ(π½ + 1)))) |
220 | 214, 219 | mpbird 256 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ (πβπ) < (πβ(π½ + 1))) β π < (π½ + 1)) |
221 | 220 | adantrl 714 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ ((πβπ½) < (πβπ) β§ (πβπ) < (πβ(π½ + 1)))) β π < (π½ + 1)) |
222 | | btwnnz 12640 |
. . . . . . . . 9
β’ ((π½ β β€ β§ π½ < π β§ π < (π½ + 1)) β Β¬ π β β€) |
223 | 204, 213,
221, 222 | syl3anc 1371 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ ((πβπ½) < (πβπ) β§ (πβπ) < (πβ(π½ + 1)))) β Β¬ π β β€) |
224 | 201, 223 | pm2.65da 815 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β Β¬ ((πβπ½) < (πβπ) β§ (πβπ) < (πβ(π½ + 1)))) |
225 | 224 | adantlr 713 |
. . . . . 6
β’ (((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β§ π β (0...π)) β Β¬ ((πβπ½) < (πβπ) β§ (πβπ) < (πβ(π½ + 1)))) |
226 | 70 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ (πβπ) = π) β (πβπ½) β β) |
227 | 75 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ (πβπ) = π) β π β β) |
228 | 30 | ffvelcdmda 7086 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β (πβπ) β β) |
229 | 228 | adantr 481 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ (πβπ) = π) β (πβπ) β β) |
230 | 74 | simp2d 1143 |
. . . . . . . . . 10
β’ (π β (πβπ½) β€ π) |
231 | 230 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ (πβπ) = π) β (πβπ½) β€ π) |
232 | 106, 198 | breqtrrdi 5190 |
. . . . . . . . . . . 12
β’ (π β π < π) |
233 | 232 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ (πβπ) = π) β π < π) |
234 | | eqcom 2739 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β (πβπ) = π) |
235 | 234 | biimpri 227 |
. . . . . . . . . . . 12
β’ ((πβπ) = π β π = (πβπ)) |
236 | 235 | adantl 482 |
. . . . . . . . . . 11
β’ ((π β§ (πβπ) = π) β π = (πβπ)) |
237 | 233, 236 | breqtrd 5174 |
. . . . . . . . . 10
β’ ((π β§ (πβπ) = π) β π < (πβπ)) |
238 | 237 | adantlr 713 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ (πβπ) = π) β π < (πβπ)) |
239 | 226, 227,
229, 231, 238 | lelttrd 11374 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ (πβπ) = π) β (πβπ½) < (πβπ)) |
240 | 239 | adantllr 717 |
. . . . . . 7
β’ ((((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β§ π β (0...π)) β§ (πβπ) = π) β (πβπ½) < (πβπ)) |
241 | | simpr 485 |
. . . . . . . . 9
β’ (((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β§ (πβπ) = π) β (πβπ) = π) |
242 | 198, 139 | eqbrtrid 5183 |
. . . . . . . . . 10
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β π < (πβ(π½ + 1))) |
243 | 242 | adantr 481 |
. . . . . . . . 9
β’ (((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β§ (πβπ) = π) β π < (πβ(π½ + 1))) |
244 | 241, 243 | eqbrtrd 5170 |
. . . . . . . 8
β’ (((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β§ (πβπ) = π) β (πβπ) < (πβ(π½ + 1))) |
245 | 244 | adantlr 713 |
. . . . . . 7
β’ ((((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β§ π β (0...π)) β§ (πβπ) = π) β (πβπ) < (πβ(π½ + 1))) |
246 | 240, 245 | jca 512 |
. . . . . 6
β’ ((((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β§ π β (0...π)) β§ (πβπ) = π) β ((πβπ½) < (πβπ) β§ (πβπ) < (πβ(π½ + 1)))) |
247 | 225, 246 | mtand 814 |
. . . . 5
β’ (((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β§ π β (0...π)) β Β¬ (πβπ) = π) |
248 | 247 | nrexdv 3149 |
. . . 4
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β Β¬ βπ β (0...π)(πβπ) = π) |
249 | | isof1o 7322 |
. . . . . . . . 9
β’ (π Isom < , < ((0...π), π») β π:(0...π)β1-1-ontoβπ») |
250 | 206, 249 | syl 17 |
. . . . . . . 8
β’ (π β π:(0...π)β1-1-ontoβπ») |
251 | | f1ofo 6840 |
. . . . . . . 8
β’ (π:(0...π)β1-1-ontoβπ» β π:(0...π)βontoβπ») |
252 | 250, 251 | syl 17 |
. . . . . . 7
β’ (π β π:(0...π)βontoβπ») |
253 | | foelrn 7108 |
. . . . . . 7
β’ ((π:(0...π)βontoβπ» β§ π β π») β βπ β (0...π)π = (πβπ)) |
254 | 252, 253 | sylan 580 |
. . . . . 6
β’ ((π β§ π β π») β βπ β (0...π)π = (πβπ)) |
255 | 234 | rexbii 3094 |
. . . . . 6
β’
(βπ β
(0...π)π = (πβπ) β βπ β (0...π)(πβπ) = π) |
256 | 254, 255 | sylib 217 |
. . . . 5
β’ ((π β§ π β π») β βπ β (0...π)(πβπ) = π) |
257 | 256 | adantlr 713 |
. . . 4
β’ (((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β§ π β π») β βπ β (0...π)(πβπ) = π) |
258 | 248, 257 | mtand 814 |
. . 3
β’ ((π β§ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) β Β¬ π β π») |
259 | 199, 258 | pm2.65da 815 |
. 2
β’ (π β Β¬ (πβπΎ) < (πΈβ(πβ(π½ + 1)))) |
260 | 52, 60, 259 | nltled 11366 |
1
β’ (π β (πΈβ(πβ(π½ + 1))) β€ (πβπΎ)) |