Step | Hyp | Ref
| Expression |
1 | | ulmscl 25754 |
. . . 4
β’ (πΉ(βπ’βπ)πΊ β π β V) |
2 | | ulmcl 25756 |
. . . 4
β’ (πΉ(βπ’βπ)πΊ β πΊ:πβΆβ) |
3 | 1, 2 | jca 513 |
. . 3
β’ (πΉ(βπ’βπ)πΊ β (π β V β§ πΊ:πβΆβ)) |
4 | 3 | a1i 11 |
. 2
β’ (π β (πΉ(βπ’βπ)πΊ β (π β V β§ πΊ:πβΆβ))) |
5 | | ulmscl 25754 |
. . . 4
β’ ((πΉ βΎ π)(βπ’βπ)πΊ β π β V) |
6 | | ulmcl 25756 |
. . . 4
β’ ((πΉ βΎ π)(βπ’βπ)πΊ β πΊ:πβΆβ) |
7 | 5, 6 | jca 513 |
. . 3
β’ ((πΉ βΎ π)(βπ’βπ)πΊ β (π β V β§ πΊ:πβΆβ)) |
8 | 7 | a1i 11 |
. 2
β’ (π β ((πΉ βΎ π)(βπ’βπ)πΊ β (π β V β§ πΊ:πβΆβ))) |
9 | | ulmres.m |
. . . . . . . . . 10
β’ (π β π β π) |
10 | | ulmres.z |
. . . . . . . . . 10
β’ π =
(β€β₯βπ) |
11 | 9, 10 | eleqtrdi 2848 |
. . . . . . . . 9
β’ (π β π β (β€β₯βπ)) |
12 | 11 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β π β (β€β₯βπ)) |
13 | | eluzel2 12775 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β π β β€) |
14 | 12, 13 | syl 17 |
. . . . . . 7
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β π β β€) |
15 | 10 | rexuz3 15240 |
. . . . . . 7
β’ (π β β€ β
(βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π β βπ β β€ βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π)) |
16 | 14, 15 | syl 17 |
. . . . . 6
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β (βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π β βπ β β€ βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π)) |
17 | | eluzelz 12780 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β π β β€) |
18 | 12, 17 | syl 17 |
. . . . . . 7
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β π β β€) |
19 | | ulmres.w |
. . . . . . . 8
β’ π =
(β€β₯βπ) |
20 | 19 | rexuz3 15240 |
. . . . . . 7
β’ (π β β€ β
(βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π β βπ β β€ βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π)) |
21 | 18, 20 | syl 17 |
. . . . . 6
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β (βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π β βπ β β€ βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π)) |
22 | 16, 21 | bitr4d 282 |
. . . . 5
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β (βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π)) |
23 | 22 | ralbidv 3175 |
. . . 4
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β (βπ β β+
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π β βπ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π)) |
24 | | ulmres.f |
. . . . . 6
β’ (π β πΉ:πβΆ(β βm π)) |
25 | 24 | adantr 482 |
. . . . 5
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β πΉ:πβΆ(β βm π)) |
26 | | eqidd 2738 |
. . . . 5
β’ (((π β§ (π β V β§ πΊ:πβΆβ)) β§ (π β π β§ π§ β π)) β ((πΉβπ)βπ§) = ((πΉβπ)βπ§)) |
27 | | eqidd 2738 |
. . . . 5
β’ (((π β§ (π β V β§ πΊ:πβΆβ)) β§ π§ β π) β (πΊβπ§) = (πΊβπ§)) |
28 | | simprr 772 |
. . . . 5
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β πΊ:πβΆβ) |
29 | | simprl 770 |
. . . . 5
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β π β V) |
30 | 10, 14, 25, 26, 27, 28, 29 | ulm2 25760 |
. . . 4
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β (πΉ(βπ’βπ)πΊ β βπ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π)) |
31 | | uzss 12793 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β
(β€β₯βπ)) |
32 | 12, 31 | syl 17 |
. . . . . . 7
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β
(β€β₯βπ) β
(β€β₯βπ)) |
33 | 32, 19, 10 | 3sstr4g 3994 |
. . . . . 6
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β π β π) |
34 | 25, 33 | fssresd 6714 |
. . . . 5
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β (πΉ βΎ π):πβΆ(β βm π)) |
35 | | fvres 6866 |
. . . . . . 7
β’ (π β π β ((πΉ βΎ π)βπ) = (πΉβπ)) |
36 | 35 | ad2antrl 727 |
. . . . . 6
β’ (((π β§ (π β V β§ πΊ:πβΆβ)) β§ (π β π β§ π§ β π)) β ((πΉ βΎ π)βπ) = (πΉβπ)) |
37 | 36 | fveq1d 6849 |
. . . . 5
β’ (((π β§ (π β V β§ πΊ:πβΆβ)) β§ (π β π β§ π§ β π)) β (((πΉ βΎ π)βπ)βπ§) = ((πΉβπ)βπ§)) |
38 | 19, 18, 34, 37, 27, 28, 29 | ulm2 25760 |
. . . 4
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β ((πΉ βΎ π)(βπ’βπ)πΊ β βπ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π)) |
39 | 23, 30, 38 | 3bitr4d 311 |
. . 3
β’ ((π β§ (π β V β§ πΊ:πβΆβ)) β (πΉ(βπ’βπ)πΊ β (πΉ βΎ π)(βπ’βπ)πΊ)) |
40 | 39 | ex 414 |
. 2
β’ (π β ((π β V β§ πΊ:πβΆβ) β (πΉ(βπ’βπ)πΊ β (πΉ βΎ π)(βπ’βπ)πΊ))) |
41 | 4, 8, 40 | pm5.21ndd 381 |
1
β’ (π β (πΉ(βπ’βπ)πΊ β (πΉ βΎ π)(βπ’βπ)πΊ)) |