Step | Hyp | Ref
| Expression |
1 | | ulm0.m |
. . . . . . 7
β’ (π β π β β€) |
2 | | uzid 12785 |
. . . . . . 7
β’ (π β β€ β π β
(β€β₯βπ)) |
3 | 1, 2 | syl 17 |
. . . . . 6
β’ (π β π β (β€β₯βπ)) |
4 | | ulm0.z |
. . . . . 6
β’ π =
(β€β₯βπ) |
5 | 3, 4 | eleqtrrdi 2849 |
. . . . 5
β’ (π β π β π) |
6 | 5 | ne0d 4300 |
. . . 4
β’ (π β π β β
) |
7 | | ral0 4475 |
. . . . . . 7
β’
βπ§ β
β
(absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ |
8 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π = β
) β π = β
) |
9 | 8 | raleqdv 3316 |
. . . . . . 7
β’ ((π β§ π = β
) β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β βπ§ β β
(absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯)) |
10 | 7, 9 | mpbiri 258 |
. . . . . 6
β’ ((π β§ π = β
) β βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) |
11 | 10 | ralrimivw 3148 |
. . . . 5
β’ ((π β§ π = β
) β βπ β
(β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) |
12 | 11 | ralrimivw 3148 |
. . . 4
β’ ((π β§ π = β
) β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) |
13 | | r19.2z 4457 |
. . . 4
β’ ((π β β
β§
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) |
14 | 6, 12, 13 | syl2an2r 684 |
. . 3
β’ ((π β§ π = β
) β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) |
15 | 14 | ralrimivw 3148 |
. 2
β’ ((π β§ π = β
) β βπ₯ β β+
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) |
16 | 1 | adantr 482 |
. . 3
β’ ((π β§ π = β
) β π β β€) |
17 | | ulm0.f |
. . . 4
β’ (π β πΉ:πβΆ(β βm π)) |
18 | 17 | adantr 482 |
. . 3
β’ ((π β§ π = β
) β πΉ:πβΆ(β βm π)) |
19 | | eqidd 2738 |
. . 3
β’ (((π β§ π = β
) β§ (π β π β§ π§ β π)) β ((πΉβπ)βπ§) = ((πΉβπ)βπ§)) |
20 | | eqidd 2738 |
. . 3
β’ (((π β§ π = β
) β§ π§ β π) β (πΊβπ§) = (πΊβπ§)) |
21 | | ulm0.g |
. . . 4
β’ (π β πΊ:πβΆβ) |
22 | 21 | adantr 482 |
. . 3
β’ ((π β§ π = β
) β πΊ:πβΆβ) |
23 | | 0ex 5269 |
. . . 4
β’ β
β V |
24 | 8, 23 | eqeltrdi 2846 |
. . 3
β’ ((π β§ π = β
) β π β V) |
25 | 4, 16, 18, 19, 20, 22, 24 | ulm2 25760 |
. 2
β’ ((π β§ π = β
) β (πΉ(βπ’βπ)πΊ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯)) |
26 | 15, 25 | mpbird 257 |
1
β’ ((π β§ π = β
) β πΉ(βπ’βπ)πΊ) |