Step | Hyp | Ref
| Expression |
1 | | ulm2.s |
. . 3
β’ (π β π β π) |
2 | | ulmval 25755 |
. . 3
β’ (π β π β (πΉ(βπ’βπ)πΊ β βπ β β€ (πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯))) |
3 | 1, 2 | syl 17 |
. 2
β’ (π β (πΉ(βπ’βπ)πΊ β βπ β β€ (πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯))) |
4 | | 3anan12 1097 |
. . . 4
β’ ((πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) β (πΊ:πβΆβ β§ (πΉ:(β€β₯βπ)βΆ(β
βm π) β§
βπ₯ β
β+ βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯))) |
5 | | ulm2.z |
. . . . . . . . . 10
β’ π =
(β€β₯βπ) |
6 | | ulm2.f |
. . . . . . . . . . . 12
β’ (π β πΉ:πβΆ(β βm π)) |
7 | 6 | fdmd 6684 |
. . . . . . . . . . 11
β’ (π β dom πΉ = π) |
8 | | fdm 6682 |
. . . . . . . . . . 11
β’ (πΉ:(β€β₯βπ)βΆ(β
βm π)
β dom πΉ =
(β€β₯βπ)) |
9 | 7, 8 | sylan9req 2798 |
. . . . . . . . . 10
β’ ((π β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β π =
(β€β₯βπ)) |
10 | 5, 9 | eqtr3id 2791 |
. . . . . . . . 9
β’ ((π β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β (β€β₯βπ) = (β€β₯βπ)) |
11 | | ulm2.m |
. . . . . . . . . . 11
β’ (π β π β β€) |
12 | 11 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β π β
β€) |
13 | | uz11 12795 |
. . . . . . . . . 10
β’ (π β β€ β
((β€β₯βπ) = (β€β₯βπ) β π = π)) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
β’ ((π β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β ((β€β₯βπ) = (β€β₯βπ) β π = π)) |
15 | 10, 14 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β π = π) |
16 | 15 | eqcomd 2743 |
. . . . . . 7
β’ ((π β§ πΉ:(β€β₯βπ)βΆ(β
βm π))
β π = π) |
17 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
18 | 17, 5 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π = π β (β€β₯βπ) = π) |
19 | 18 | feq2d 6659 |
. . . . . . . . 9
β’ (π = π β (πΉ:(β€β₯βπ)βΆ(β
βm π)
β πΉ:πβΆ(β βm π))) |
20 | 19 | biimparc 481 |
. . . . . . . 8
β’ ((πΉ:πβΆ(β βm π) β§ π = π) β πΉ:(β€β₯βπ)βΆ(β
βm π)) |
21 | 6, 20 | sylan 581 |
. . . . . . 7
β’ ((π β§ π = π) β πΉ:(β€β₯βπ)βΆ(β
βm π)) |
22 | 16, 21 | impbida 800 |
. . . . . 6
β’ (π β (πΉ:(β€β₯βπ)βΆ(β
βm π)
β π = π)) |
23 | 22 | anbi1d 631 |
. . . . 5
β’ (π β ((πΉ:(β€β₯βπ)βΆ(β
βm π) β§
βπ₯ β
β+ βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) β (π = π β§ βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯))) |
24 | | ulm2.g |
. . . . . 6
β’ (π β πΊ:πβΆβ) |
25 | 24 | biantrurd 534 |
. . . . 5
β’ (π β ((πΉ:(β€β₯βπ)βΆ(β
βm π) β§
βπ₯ β
β+ βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) β (πΊ:πβΆβ β§ (πΉ:(β€β₯βπ)βΆ(β
βm π) β§
βπ₯ β
β+ βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯)))) |
26 | | simp-4l 782 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π = π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β π) |
27 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π = π) β π = π) |
28 | | uzid 12785 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β€ β π β
(β€β₯βπ)) |
29 | 11, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β (β€β₯βπ)) |
30 | 29, 5 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β π) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π = π) β π β π) |
32 | 27, 31 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π = π) β π β π) |
33 | 5 | uztrn2 12789 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
34 | 32, 33 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π = π) β§ π β (β€β₯βπ)) β π β π) |
35 | 5 | uztrn2 12789 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
36 | 34, 35 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π = π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β π β π) |
37 | 36 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π = π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β π β π) |
38 | | simpr 486 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π = π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β π§ β π) |
39 | | ulm2.b |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ π§ β π)) β ((πΉβπ)βπ§) = π΅) |
40 | 26, 37, 38, 39 | syl12anc 836 |
. . . . . . . . . . . . 13
β’
(((((π β§ π = π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β ((πΉβπ)βπ§) = π΅) |
41 | | ulm2.a |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π) β (πΊβπ§) = π΄) |
42 | 26, 41 | sylancom 589 |
. . . . . . . . . . . . 13
β’
(((((π β§ π = π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β (πΊβπ§) = π΄) |
43 | 40, 42 | oveq12d 7380 |
. . . . . . . . . . . 12
β’
(((((π β§ π = π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β (((πΉβπ)βπ§) β (πΊβπ§)) = (π΅ β π΄)) |
44 | 43 | fveq2d 6851 |
. . . . . . . . . . 11
β’
(((((π β§ π = π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β (absβ(((πΉβπ)βπ§) β (πΊβπ§))) = (absβ(π΅ β π΄))) |
45 | 44 | breq1d 5120 |
. . . . . . . . . 10
β’
(((((π β§ π = π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β ((absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β (absβ(π΅ β π΄)) < π₯)) |
46 | 45 | ralbidva 3173 |
. . . . . . . . 9
β’ ((((π β§ π = π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β βπ§ β π (absβ(π΅ β π΄)) < π₯)) |
47 | 46 | ralbidva 3173 |
. . . . . . . 8
β’ (((π β§ π = π) β§ π β (β€β₯βπ)) β (βπ β
(β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯)) |
48 | 47 | rexbidva 3174 |
. . . . . . 7
β’ ((π β§ π = π) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯)) |
49 | 48 | ralbidv 3175 |
. . . . . 6
β’ ((π β§ π = π) β (βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯ β βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯)) |
50 | 49 | pm5.32da 580 |
. . . . 5
β’ (π β ((π = π β§ βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) β (π = π β§ βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯))) |
51 | 23, 25, 50 | 3bitr3d 309 |
. . . 4
β’ (π β ((πΊ:πβΆβ β§ (πΉ:(β€β₯βπ)βΆ(β
βm π) β§
βπ₯ β
β+ βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯)) β (π = π β§ βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯))) |
52 | 4, 51 | bitrid 283 |
. . 3
β’ (π β ((πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) β (π = π β§ βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯))) |
53 | 52 | rexbidv 3176 |
. 2
β’ (π β (βπ β β€ (πΉ:(β€β₯βπ)βΆ(β
βm π) β§
πΊ:πβΆβ β§ βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯) β βπ β β€ (π = π β§ βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯))) |
54 | 18 | rexeqdv 3317 |
. . . . 5
β’ (π = π β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯ β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯)) |
55 | 54 | ralbidv 3175 |
. . . 4
β’ (π = π β (βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯)) |
56 | 55 | ceqsrexv 3610 |
. . 3
β’ (π β β€ β
(βπ β β€
(π = π β§ βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯)) |
57 | 11, 56 | syl 17 |
. 2
β’ (π β (βπ β β€ (π = π β§ βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯)) |
58 | 3, 53, 57 | 3bitrd 305 |
1
β’ (π β (πΉ(βπ’βπ)πΊ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯)) |