Step | Hyp | Ref
| Expression |
1 | | blrn 23778 |
. . 3
β’ (π· β (βMetβπ) β (π΅ β ran (ballβπ·) β βπ¦ β π βπ β β* π΅ = (π¦(ballβπ·)π))) |
2 | | elbl 23757 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β (π β (π¦(ballβπ·)π) β (π β π β§ (π¦π·π) < π))) |
3 | | simpl1 1192 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β π· β (βMetβπ)) |
4 | | simpl2 1193 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β π¦ β π) |
5 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β π β π) |
6 | | xmetcl 23700 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π¦ β π β§ π β π) β (π¦π·π) β
β*) |
7 | 3, 4, 5, 6 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β (π¦π·π) β
β*) |
8 | | simpl3 1194 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β π β β*) |
9 | | qbtwnxr 13125 |
. . . . . . . . . . 11
β’ (((π¦π·π) β β* β§ π β β*
β§ (π¦π·π) < π) β βπ§ β β ((π¦π·π) < π§ β§ π§ < π)) |
10 | 9 | 3expia 1122 |
. . . . . . . . . 10
β’ (((π¦π·π) β β* β§ π β β*)
β ((π¦π·π) < π β βπ§ β β ((π¦π·π) < π§ β§ π§ < π))) |
11 | 7, 8, 10 | syl2anc 585 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β ((π¦π·π) < π β βπ§ β β ((π¦π·π) < π§ β§ π§ < π))) |
12 | | qre 12883 |
. . . . . . . . . . 11
β’ (π§ β β β π§ β
β) |
13 | | simpll1 1213 |
. . . . . . . . . . . . . . . 16
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β π· β (βMetβπ)) |
14 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β π β π) |
15 | | simpll2 1214 |
. . . . . . . . . . . . . . . 16
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β π¦ β π) |
16 | | xmetsym 23716 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (βMetβπ) β§ π β π β§ π¦ β π) β (ππ·π¦) = (π¦π·π)) |
17 | 13, 14, 15, 16 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (ππ·π¦) = (π¦π·π)) |
18 | | simprrl 780 |
. . . . . . . . . . . . . . 15
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (π¦π·π) < π§) |
19 | 17, 18 | eqbrtrd 5128 |
. . . . . . . . . . . . . 14
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (ππ·π¦) < π§) |
20 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β π§ β β) |
21 | | xmetcl 23700 |
. . . . . . . . . . . . . . . . . 18
β’ ((π· β (βMetβπ) β§ π β π β§ π¦ β π) β (ππ·π¦) β
β*) |
22 | 13, 14, 15, 21 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (ππ·π¦) β
β*) |
23 | | rexr 11206 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β β β π§ β
β*) |
24 | 23 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β π§ β β*) |
25 | 22, 24, 19 | xrltled 13075 |
. . . . . . . . . . . . . . . 16
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (ππ·π¦) β€ π§) |
26 | | xmetlecl 23715 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (βMetβπ) β§ (π β π β§ π¦ β π) β§ (π§ β β β§ (ππ·π¦) β€ π§)) β (ππ·π¦) β β) |
27 | 13, 14, 15, 20, 25, 26 | syl122anc 1380 |
. . . . . . . . . . . . . . 15
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (ππ·π¦) β β) |
28 | | difrp 12958 |
. . . . . . . . . . . . . . 15
β’ (((ππ·π¦) β β β§ π§ β β) β ((ππ·π¦) < π§ β (π§ β (ππ·π¦)) β
β+)) |
29 | 27, 20, 28 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β ((ππ·π¦) < π§ β (π§ β (ππ·π¦)) β
β+)) |
30 | 19, 29 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (π§ β (ππ·π¦)) β
β+) |
31 | 20, 27 | resubcld 11588 |
. . . . . . . . . . . . . . 15
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (π§ β (ππ·π¦)) β β) |
32 | 22 | xrleidd 13077 |
. . . . . . . . . . . . . . . 16
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (ππ·π¦) β€ (ππ·π¦)) |
33 | 20 | recnd 11188 |
. . . . . . . . . . . . . . . . 17
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β π§ β β) |
34 | 27 | recnd 11188 |
. . . . . . . . . . . . . . . . 17
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (ππ·π¦) β β) |
35 | 33, 34 | nncand 11522 |
. . . . . . . . . . . . . . . 16
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (π§ β (π§ β (ππ·π¦))) = (ππ·π¦)) |
36 | 32, 35 | breqtrrd 5134 |
. . . . . . . . . . . . . . 15
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (ππ·π¦) β€ (π§ β (π§ β (ππ·π¦)))) |
37 | | blss2 23773 |
. . . . . . . . . . . . . . 15
β’ (((π· β (βMetβπ) β§ π β π β§ π¦ β π) β§ ((π§ β (ππ·π¦)) β β β§ π§ β β β§ (ππ·π¦) β€ (π§ β (π§ β (ππ·π¦))))) β (π(ballβπ·)(π§ β (ππ·π¦))) β (π¦(ballβπ·)π§)) |
38 | 13, 14, 15, 31, 20, 36, 37 | syl33anc 1386 |
. . . . . . . . . . . . . 14
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (π(ballβπ·)(π§ β (ππ·π¦))) β (π¦(ballβπ·)π§)) |
39 | | simpll3 1215 |
. . . . . . . . . . . . . . 15
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β π β β*) |
40 | | simprrr 781 |
. . . . . . . . . . . . . . . 16
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β π§ < π) |
41 | 24, 39, 40 | xrltled 13075 |
. . . . . . . . . . . . . . 15
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β π§ β€ π) |
42 | | ssbl 23792 |
. . . . . . . . . . . . . . 15
β’ (((π· β (βMetβπ) β§ π¦ β π) β§ (π§ β β* β§ π β β*)
β§ π§ β€ π) β (π¦(ballβπ·)π§) β (π¦(ballβπ·)π)) |
43 | 13, 15, 24, 39, 41, 42 | syl221anc 1382 |
. . . . . . . . . . . . . 14
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (π¦(ballβπ·)π§) β (π¦(ballβπ·)π)) |
44 | 38, 43 | sstrd 3955 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β (π(ballβπ·)(π§ β (ππ·π¦))) β (π¦(ballβπ·)π)) |
45 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π§ β (ππ·π¦)) β (π(ballβπ·)π₯) = (π(ballβπ·)(π§ β (ππ·π¦)))) |
46 | 45 | sseq1d 3976 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π§ β (ππ·π¦)) β ((π(ballβπ·)π₯) β (π¦(ballβπ·)π) β (π(ballβπ·)(π§ β (ππ·π¦))) β (π¦(ballβπ·)π))) |
47 | 46 | rspcev 3580 |
. . . . . . . . . . . . 13
β’ (((π§ β (ππ·π¦)) β β+ β§ (π(ballβπ·)(π§ β (ππ·π¦))) β (π¦(ballβπ·)π)) β βπ₯ β β+ (π(ballβπ·)π₯) β (π¦(ballβπ·)π)) |
48 | 30, 44, 47 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ (π§ β β β§ ((π¦π·π) < π§ β§ π§ < π))) β βπ₯ β β+ (π(ballβπ·)π₯) β (π¦(ballβπ·)π)) |
49 | 48 | expr 458 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ π§ β β) β (((π¦π·π) < π§ β§ π§ < π) β βπ₯ β β+ (π(ballβπ·)π₯) β (π¦(ballβπ·)π))) |
50 | 12, 49 | sylan2 594 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β§ π§ β β) β (((π¦π·π) < π§ β§ π§ < π) β βπ₯ β β+ (π(ballβπ·)π₯) β (π¦(ballβπ·)π))) |
51 | 50 | rexlimdva 3149 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β (βπ§ β β ((π¦π·π) < π§ β§ π§ < π) β βπ₯ β β+ (π(ballβπ·)π₯) β (π¦(ballβπ·)π))) |
52 | 11, 51 | syld 47 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β§ π β π) β ((π¦π·π) < π β βπ₯ β β+ (π(ballβπ·)π₯) β (π¦(ballβπ·)π))) |
53 | 52 | expimpd 455 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β ((π β π β§ (π¦π·π) < π) β βπ₯ β β+ (π(ballβπ·)π₯) β (π¦(ballβπ·)π))) |
54 | 2, 53 | sylbid 239 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β (π β (π¦(ballβπ·)π) β βπ₯ β β+ (π(ballβπ·)π₯) β (π¦(ballβπ·)π))) |
55 | | eleq2 2823 |
. . . . . . 7
β’ (π΅ = (π¦(ballβπ·)π) β (π β π΅ β π β (π¦(ballβπ·)π))) |
56 | | sseq2 3971 |
. . . . . . . 8
β’ (π΅ = (π¦(ballβπ·)π) β ((π(ballβπ·)π₯) β π΅ β (π(ballβπ·)π₯) β (π¦(ballβπ·)π))) |
57 | 56 | rexbidv 3172 |
. . . . . . 7
β’ (π΅ = (π¦(ballβπ·)π) β (βπ₯ β β+ (π(ballβπ·)π₯) β π΅ β βπ₯ β β+ (π(ballβπ·)π₯) β (π¦(ballβπ·)π))) |
58 | 55, 57 | imbi12d 345 |
. . . . . 6
β’ (π΅ = (π¦(ballβπ·)π) β ((π β π΅ β βπ₯ β β+ (π(ballβπ·)π₯) β π΅) β (π β (π¦(ballβπ·)π) β βπ₯ β β+ (π(ballβπ·)π₯) β (π¦(ballβπ·)π)))) |
59 | 54, 58 | syl5ibrcom 247 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π¦ β π β§ π β β*) β (π΅ = (π¦(ballβπ·)π) β (π β π΅ β βπ₯ β β+ (π(ballβπ·)π₯) β π΅))) |
60 | 59 | 3expib 1123 |
. . . 4
β’ (π· β (βMetβπ) β ((π¦ β π β§ π β β*) β (π΅ = (π¦(ballβπ·)π) β (π β π΅ β βπ₯ β β+ (π(ballβπ·)π₯) β π΅)))) |
61 | 60 | rexlimdvv 3201 |
. . 3
β’ (π· β (βMetβπ) β (βπ¦ β π βπ β β* π΅ = (π¦(ballβπ·)π) β (π β π΅ β βπ₯ β β+ (π(ballβπ·)π₯) β π΅))) |
62 | 1, 61 | sylbid 239 |
. 2
β’ (π· β (βMetβπ) β (π΅ β ran (ballβπ·) β (π β π΅ β βπ₯ β β+ (π(ballβπ·)π₯) β π΅))) |
63 | 62 | 3imp 1112 |
1
β’ ((π· β (βMetβπ) β§ π΅ β ran (ballβπ·) β§ π β π΅) β βπ₯ β β+ (π(ballβπ·)π₯) β π΅) |