Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
β’ ((π β§ π = β
) β π = β
) |
2 | | stoweid.10 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
3 | 2 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ₯ β β (π‘ β π β¦ π₯) β π΄) |
4 | | 1re 11160 |
. . . . . 6
β’ 1 β
β |
5 | | id 22 |
. . . . . . . . 9
β’ (π₯ = 1 β π₯ = 1) |
6 | 5 | mpteq2dv 5208 |
. . . . . . . 8
β’ (π₯ = 1 β (π‘ β π β¦ π₯) = (π‘ β π β¦ 1)) |
7 | 6 | eleq1d 2819 |
. . . . . . 7
β’ (π₯ = 1 β ((π‘ β π β¦ π₯) β π΄ β (π‘ β π β¦ 1) β π΄)) |
8 | 7 | rspccv 3577 |
. . . . . 6
β’
(βπ₯ β
β (π‘ β π β¦ π₯) β π΄ β (1 β β β (π‘ β π β¦ 1) β π΄)) |
9 | 3, 4, 8 | mpisyl 21 |
. . . . 5
β’ (π β (π‘ β π β¦ 1) β π΄) |
10 | 9 | adantr 482 |
. . . 4
β’ ((π β§ π = β
) β (π‘ β π β¦ 1) β π΄) |
11 | 1, 10 | stoweidlem9 44336 |
. . 3
β’ ((π β§ π = β
) β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < if(πΈ β€ (1 / 4), πΈ, (1 / 4))) |
12 | | stoweid.1 |
. . . 4
β’
β²π‘πΉ |
13 | | nfv 1918 |
. . . . 5
β’
β²ππ |
14 | | nfv 1918 |
. . . . 5
β’
β²π Β¬ π = β
|
15 | 13, 14 | nfan 1903 |
. . . 4
β’
β²π(π β§ Β¬ π = β
) |
16 | | stoweid.2 |
. . . . 5
β’
β²π‘π |
17 | | nfv 1918 |
. . . . 5
β’
β²π‘ Β¬ π = β
|
18 | 16, 17 | nfan 1903 |
. . . 4
β’
β²π‘(π β§ Β¬ π = β
) |
19 | | eqid 2733 |
. . . 4
β’ (π‘ β π β¦ ((πΉβπ‘) β inf(ran πΉ, β, < ))) = (π‘ β π β¦ ((πΉβπ‘) β inf(ran πΉ, β, < ))) |
20 | | stoweid.3 |
. . . 4
β’ πΎ = (topGenβran
(,)) |
21 | | stoweid.5 |
. . . 4
β’ π = βͺ
π½ |
22 | | stoweid.4 |
. . . . 5
β’ (π β π½ β Comp) |
23 | 22 | adantr 482 |
. . . 4
β’ ((π β§ Β¬ π = β
) β π½ β Comp) |
24 | | stoweid.6 |
. . . 4
β’ πΆ = (π½ Cn πΎ) |
25 | | stoweid.7 |
. . . . 5
β’ (π β π΄ β πΆ) |
26 | 25 | adantr 482 |
. . . 4
β’ ((π β§ Β¬ π = β
) β π΄ β πΆ) |
27 | | stoweid.8 |
. . . . 5
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
28 | 27 | 3adant1r 1178 |
. . . 4
β’ (((π β§ Β¬ π = β
) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
29 | | stoweid.9 |
. . . . 5
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
30 | 29 | 3adant1r 1178 |
. . . 4
β’ (((π β§ Β¬ π = β
) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
31 | 2 | adantlr 714 |
. . . 4
β’ (((π β§ Β¬ π = β
) β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
32 | | stoweid.11 |
. . . . 5
β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β ββ β π΄ (ββπ) β (ββπ‘)) |
33 | 32 | adantlr 714 |
. . . 4
β’ (((π β§ Β¬ π = β
) β§ (π β π β§ π‘ β π β§ π β π‘)) β ββ β π΄ (ββπ) β (ββπ‘)) |
34 | | stoweid.12 |
. . . . 5
β’ (π β πΉ β πΆ) |
35 | 34 | adantr 482 |
. . . 4
β’ ((π β§ Β¬ π = β
) β πΉ β πΆ) |
36 | | stoweid.13 |
. . . . . 6
β’ (π β πΈ β
β+) |
37 | | 4re 12242 |
. . . . . . . . 9
β’ 4 β
β |
38 | | 4pos 12265 |
. . . . . . . . 9
β’ 0 <
4 |
39 | 37, 38 | elrpii 12923 |
. . . . . . . 8
β’ 4 β
β+ |
40 | 39 | a1i 11 |
. . . . . . 7
β’ (π β 4 β
β+) |
41 | 40 | rpreccld 12972 |
. . . . . 6
β’ (π β (1 / 4) β
β+) |
42 | 36, 41 | ifcld 4533 |
. . . . 5
β’ (π β if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β
β+) |
43 | 42 | adantr 482 |
. . . 4
β’ ((π β§ Β¬ π = β
) β if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β
β+) |
44 | | neqne 2948 |
. . . . 5
β’ (Β¬
π = β
β π β β
) |
45 | 44 | adantl 483 |
. . . 4
β’ ((π β§ Β¬ π = β
) β π β β
) |
46 | 36 | rpred 12962 |
. . . . . . 7
β’ (π β πΈ β β) |
47 | | 4ne0 12266 |
. . . . . . . . 9
β’ 4 β
0 |
48 | 37, 47 | rereccli 11925 |
. . . . . . . 8
β’ (1 / 4)
β β |
49 | 48 | a1i 11 |
. . . . . . 7
β’ (π β (1 / 4) β
β) |
50 | 46, 49 | ifcld 4533 |
. . . . . 6
β’ (π β if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β β) |
51 | | 3re 12238 |
. . . . . . . 8
β’ 3 β
β |
52 | | 3ne0 12264 |
. . . . . . . 8
β’ 3 β
0 |
53 | 51, 52 | rereccli 11925 |
. . . . . . 7
β’ (1 / 3)
β β |
54 | 53 | a1i 11 |
. . . . . 6
β’ (π β (1 / 3) β
β) |
55 | 36 | rpxrd 12963 |
. . . . . . 7
β’ (π β πΈ β
β*) |
56 | 41 | rpxrd 12963 |
. . . . . . 7
β’ (π β (1 / 4) β
β*) |
57 | | xrmin2 13103 |
. . . . . . 7
β’ ((πΈ β β*
β§ (1 / 4) β β*) β if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β€ (1 / 4)) |
58 | 55, 56, 57 | syl2anc 585 |
. . . . . 6
β’ (π β if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β€ (1 / 4)) |
59 | | 3lt4 12332 |
. . . . . . . 8
β’ 3 <
4 |
60 | | 3pos 12263 |
. . . . . . . . 9
β’ 0 <
3 |
61 | 51, 37, 60, 38 | ltrecii 12076 |
. . . . . . . 8
β’ (3 < 4
β (1 / 4) < (1 / 3)) |
62 | 59, 61 | mpbi 229 |
. . . . . . 7
β’ (1 / 4)
< (1 / 3) |
63 | 62 | a1i 11 |
. . . . . 6
β’ (π β (1 / 4) < (1 /
3)) |
64 | 50, 49, 54, 58, 63 | lelttrd 11318 |
. . . . 5
β’ (π β if(πΈ β€ (1 / 4), πΈ, (1 / 4)) < (1 / 3)) |
65 | 64 | adantr 482 |
. . . 4
β’ ((π β§ Β¬ π = β
) β if(πΈ β€ (1 / 4), πΈ, (1 / 4)) < (1 / 3)) |
66 | 12, 15, 18, 19, 20, 21, 23, 24, 26, 28, 30, 31, 33, 35, 43, 45, 65 | stoweidlem62 44389 |
. . 3
β’ ((π β§ Β¬ π = β
) β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < if(πΈ β€ (1 / 4), πΈ, (1 / 4))) |
67 | 11, 66 | pm2.61dan 812 |
. 2
β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < if(πΈ β€ (1 / 4), πΈ, (1 / 4))) |
68 | | nfv 1918 |
. . . . 5
β’
β²π‘ π β π΄ |
69 | 16, 68 | nfan 1903 |
. . . 4
β’
β²π‘(π β§ π β π΄) |
70 | | xrmin1 13102 |
. . . . . . 7
β’ ((πΈ β β*
β§ (1 / 4) β β*) β if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β€ πΈ) |
71 | 55, 56, 70 | syl2anc 585 |
. . . . . 6
β’ (π β if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β€ πΈ) |
72 | 71 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β π΄) β§ π‘ β π) β if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β€ πΈ) |
73 | 25 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ π‘ β π) β π΄ β πΆ) |
74 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΄) β§ π‘ β π) β π β π΄) |
75 | 73, 74 | sseldd 3946 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄) β§ π‘ β π) β π β πΆ) |
76 | 20, 21, 24, 75 | fcnre 43318 |
. . . . . . . . . 10
β’ (((π β§ π β π΄) β§ π‘ β π) β π:πβΆβ) |
77 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π β π΄) β§ π‘ β π) β π‘ β π) |
78 | 76, 77 | jca 513 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ π‘ β π) β (π:πβΆβ β§ π‘ β π)) |
79 | | ffvelcdm 7033 |
. . . . . . . . 9
β’ ((π:πβΆβ β§ π‘ β π) β (πβπ‘) β β) |
80 | | recn 11146 |
. . . . . . . . 9
β’ ((πβπ‘) β β β (πβπ‘) β β) |
81 | 78, 79, 80 | 3syl 18 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π‘ β π) β (πβπ‘) β β) |
82 | 34 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β π΄) β§ π‘ β π) β πΉ β πΆ) |
83 | 20, 21, 24, 82 | fcnre 43318 |
. . . . . . . . . 10
β’ (((π β§ π β π΄) β§ π‘ β π) β πΉ:πβΆβ) |
84 | 83, 77 | jca 513 |
. . . . . . . . 9
β’ (((π β§ π β π΄) β§ π‘ β π) β (πΉ:πβΆβ β§ π‘ β π)) |
85 | | ffvelcdm 7033 |
. . . . . . . . 9
β’ ((πΉ:πβΆβ β§ π‘ β π) β (πΉβπ‘) β β) |
86 | | recn 11146 |
. . . . . . . . 9
β’ ((πΉβπ‘) β β β (πΉβπ‘) β β) |
87 | 84, 85, 86 | 3syl 18 |
. . . . . . . 8
β’ (((π β§ π β π΄) β§ π‘ β π) β (πΉβπ‘) β β) |
88 | 81, 87 | subcld 11517 |
. . . . . . 7
β’ (((π β§ π β π΄) β§ π‘ β π) β ((πβπ‘) β (πΉβπ‘)) β β) |
89 | 88 | abscld 15327 |
. . . . . 6
β’ (((π β§ π β π΄) β§ π‘ β π) β (absβ((πβπ‘) β (πΉβπ‘))) β β) |
90 | 4, 37, 47 | 3pm3.2i 1340 |
. . . . . . . . 9
β’ (1 β
β β§ 4 β β β§ 4 β 0) |
91 | | redivcl 11879 |
. . . . . . . . 9
β’ ((1
β β β§ 4 β β β§ 4 β 0) β (1 / 4) β
β) |
92 | 90, 91 | mp1i 13 |
. . . . . . . 8
β’ (π β (1 / 4) β
β) |
93 | 46, 92 | ifcld 4533 |
. . . . . . 7
β’ (π β if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β β) |
94 | 93 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β π΄) β§ π‘ β π) β if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β β) |
95 | 46 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β π΄) β§ π‘ β π) β πΈ β β) |
96 | | ltletr 11252 |
. . . . . 6
β’
(((absβ((πβπ‘) β (πΉβπ‘))) β β β§ if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β β β§ πΈ β β) β
(((absβ((πβπ‘) β (πΉβπ‘))) < if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β§ if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β€ πΈ) β (absβ((πβπ‘) β (πΉβπ‘))) < πΈ)) |
97 | 89, 94, 95, 96 | syl3anc 1372 |
. . . . 5
β’ (((π β§ π β π΄) β§ π‘ β π) β (((absβ((πβπ‘) β (πΉβπ‘))) < if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β§ if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β€ πΈ) β (absβ((πβπ‘) β (πΉβπ‘))) < πΈ)) |
98 | 72, 97 | mpan2d 693 |
. . . 4
β’ (((π β§ π β π΄) β§ π‘ β π) β ((absβ((πβπ‘) β (πΉβπ‘))) < if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β (absβ((πβπ‘) β (πΉβπ‘))) < πΈ)) |
99 | 69, 98 | ralimdaa 3242 |
. . 3
β’ ((π β§ π β π΄) β (βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ)) |
100 | 99 | reximdva 3162 |
. 2
β’ (π β (βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < if(πΈ β€ (1 / 4), πΈ, (1 / 4)) β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ)) |
101 | 67, 100 | mpd 15 |
1
β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ) |