Step | Hyp | Ref
| Expression |
1 | | stoweidlem61.1 |
. . 3
β’
β²π‘πΉ |
2 | | stoweidlem61.2 |
. . 3
β’
β²π‘π |
3 | | stoweidlem61.3 |
. . 3
β’ πΎ = (topGenβran
(,)) |
4 | | stoweidlem61.5 |
. . 3
β’ π = βͺ
π½ |
5 | | stoweidlem61.7 |
. . 3
β’ πΆ = (π½ Cn πΎ) |
6 | | eqid 2733 |
. . 3
β’ (π β (0...π) β¦ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) = (π β (0...π) β¦ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) |
7 | | eqid 2733 |
. . 3
β’ (π β (0...π) β¦ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) = (π β (0...π) β¦ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) |
8 | | stoweidlem61.4 |
. . 3
β’ (π β π½ β Comp) |
9 | | stoweidlem61.6 |
. . 3
β’ (π β π β β
) |
10 | | stoweidlem61.8 |
. . 3
β’ (π β π΄ β πΆ) |
11 | | stoweidlem61.9 |
. . 3
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
12 | | stoweidlem61.10 |
. . 3
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
13 | | stoweidlem61.11 |
. . 3
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
14 | | stoweidlem61.12 |
. . 3
β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) |
15 | | stoweidlem61.13 |
. . 3
β’ (π β πΉ β πΆ) |
16 | | stoweidlem61.14 |
. . 3
β’ (π β βπ‘ β π 0 β€ (πΉβπ‘)) |
17 | | stoweidlem61.15 |
. . 3
β’ (π β πΈ β
β+) |
18 | | stoweidlem61.16 |
. . 3
β’ (π β πΈ < (1 / 3)) |
19 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18 | stoweidlem60 44387 |
. 2
β’ (π β βπ β π΄ βπ‘ β π βπ β β ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘)))) |
20 | | nfv 1918 |
. . . . 5
β’
β²π‘ π β π΄ |
21 | 2, 20 | nfan 1903 |
. . . 4
β’
β²π‘(π β§ π β π΄) |
22 | 17 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β π΄) β§ π‘ β π) β πΈ β
β+) |
23 | 3, 4, 5, 15 | fcnre 43318 |
. . . . . . 7
β’ (π β πΉ:πβΆβ) |
24 | 23 | ffvelcdmda 7036 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πΉβπ‘) β β) |
25 | 24 | adantlr 714 |
. . . . 5
β’ (((π β§ π β π΄) β§ π‘ β π) β (πΉβπ‘) β β) |
26 | 10 | sselda 3945 |
. . . . . . 7
β’ ((π β§ π β π΄) β π β πΆ) |
27 | 3, 4, 5, 26 | fcnre 43318 |
. . . . . 6
β’ ((π β§ π β π΄) β π:πβΆβ) |
28 | 27 | ffvelcdmda 7036 |
. . . . 5
β’ (((π β§ π β π΄) β§ π‘ β π) β (πβπ‘) β β) |
29 | | simpll1 1213 |
. . . . . . 7
β’ ((((πΈ β β+
β§ (πΉβπ‘) β β β§ (πβπ‘) β β) β§ π β β) β§ ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘)))) β πΈ β
β+) |
30 | | simpll2 1214 |
. . . . . . 7
β’ ((((πΈ β β+
β§ (πΉβπ‘) β β β§ (πβπ‘) β β) β§ π β β) β§ ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘)))) β (πΉβπ‘) β β) |
31 | | simpll3 1215 |
. . . . . . 7
β’ ((((πΈ β β+
β§ (πΉβπ‘) β β β§ (πβπ‘) β β) β§ π β β) β§ ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘)))) β (πβπ‘) β β) |
32 | | simplr 768 |
. . . . . . 7
β’ ((((πΈ β β+
β§ (πΉβπ‘) β β β§ (πβπ‘) β β) β§ π β β) β§ ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘)))) β π β β) |
33 | | simprll 778 |
. . . . . . 7
β’ ((((πΈ β β+
β§ (πΉβπ‘) β β β§ (πβπ‘) β β) β§ π β β) β§ ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘)))) β ((π β (4 / 3)) Β· πΈ) < (πΉβπ‘)) |
34 | | simprlr 779 |
. . . . . . 7
β’ ((((πΈ β β+
β§ (πΉβπ‘) β β β§ (πβπ‘) β β) β§ π β β) β§ ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘)))) β (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) |
35 | | simprrr 781 |
. . . . . . 7
β’ ((((πΈ β β+
β§ (πΉβπ‘) β β β§ (πβπ‘) β β) β§ π β β) β§ ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘)))) β ((π β (4 / 3)) Β· πΈ) < (πβπ‘)) |
36 | | simprrl 780 |
. . . . . . 7
β’ ((((πΈ β β+
β§ (πΉβπ‘) β β β§ (πβπ‘) β β) β§ π β β) β§ ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘)))) β (πβπ‘) < ((π + (1 / 3)) Β· πΈ)) |
37 | 29, 30, 31, 32, 33, 34, 35, 36 | stoweidlem13 44340 |
. . . . . 6
β’ ((((πΈ β β+
β§ (πΉβπ‘) β β β§ (πβπ‘) β β) β§ π β β) β§ ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘)))) β (absβ((πβπ‘) β (πΉβπ‘))) < (2 Β· πΈ)) |
38 | 37 | rexlimdva2 3151 |
. . . . 5
β’ ((πΈ β β+
β§ (πΉβπ‘) β β β§ (πβπ‘) β β) β (βπ β β ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘))) β (absβ((πβπ‘) β (πΉβπ‘))) < (2 Β· πΈ))) |
39 | 22, 25, 28, 38 | syl3anc 1372 |
. . . 4
β’ (((π β§ π β π΄) β§ π‘ β π) β (βπ β β ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘))) β (absβ((πβπ‘) β (πΉβπ‘))) < (2 Β· πΈ))) |
40 | 21, 39 | ralimdaa 3242 |
. . 3
β’ ((π β§ π β π΄) β (βπ‘ β π βπ β β ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘))) β βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < (2 Β· πΈ))) |
41 | 40 | reximdva 3162 |
. 2
β’ (π β (βπ β π΄ βπ‘ β π βπ β β ((((π β (4 / 3)) Β· πΈ) < (πΉβπ‘) β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) β§ ((πβπ‘) < ((π + (1 / 3)) Β· πΈ) β§ ((π β (4 / 3)) Β· πΈ) < (πβπ‘))) β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < (2 Β· πΈ))) |
42 | 19, 41 | mpd 15 |
1
β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < (2 Β· πΈ)) |