Step | Hyp | Ref
| Expression |
1 | | blss 23816 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π₯ β ran (ballβπ·) β§ π β π₯) β βπ β β+ (π(ballβπ·)π) β π₯) |
2 | | sstr 3956 |
. . . . . . . . 9
β’ (((π(ballβπ·)π) β π₯ β§ π₯ β π΄) β (π(ballβπ·)π) β π΄) |
3 | 2 | expcom 415 |
. . . . . . . 8
β’ (π₯ β π΄ β ((π(ballβπ·)π) β π₯ β (π(ballβπ·)π) β π΄)) |
4 | 3 | reximdv 3164 |
. . . . . . 7
β’ (π₯ β π΄ β (βπ β β+ (π(ballβπ·)π) β π₯ β βπ β β+ (π(ballβπ·)π) β π΄)) |
5 | 1, 4 | syl5com 31 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π₯ β ran (ballβπ·) β§ π β π₯) β (π₯ β π΄ β βπ β β+ (π(ballβπ·)π) β π΄)) |
6 | 5 | 3expa 1119 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π₯ β ran (ballβπ·)) β§ π β π₯) β (π₯ β π΄ β βπ β β+ (π(ballβπ·)π) β π΄)) |
7 | 6 | expimpd 455 |
. . . 4
β’ ((π· β (βMetβπ) β§ π₯ β ran (ballβπ·)) β ((π β π₯ β§ π₯ β π΄) β βπ β β+ (π(ballβπ·)π) β π΄)) |
8 | 7 | adantlr 714 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β ran (ballβπ·)) β ((π β π₯ β§ π₯ β π΄) β βπ β β+ (π(ballβπ·)π) β π΄)) |
9 | 8 | rexlimdva 3149 |
. 2
β’ ((π· β (βMetβπ) β§ π β π) β (βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄) β βπ β β+ (π(ballβπ·)π) β π΄)) |
10 | | simpll 766 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π· β (βMetβπ)) |
11 | | simplr 768 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π β π) |
12 | | rpxr 12934 |
. . . . . 6
β’ (π β β+
β π β
β*) |
13 | 12 | ad2antrl 727 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π β β*) |
14 | | blelrn 23808 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (π(ballβπ·)π) β ran (ballβπ·)) |
15 | 10, 11, 13, 14 | syl3anc 1372 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β (π(ballβπ·)π) β ran (ballβπ·)) |
16 | | simprl 770 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π β β+) |
17 | | blcntr 23804 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ π β β+) β π β (π(ballβπ·)π)) |
18 | 10, 11, 16, 17 | syl3anc 1372 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β π β (π(ballβπ·)π)) |
19 | | simprr 772 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β (π(ballβπ·)π) β π΄) |
20 | | eleq2 2822 |
. . . . . 6
β’ (π₯ = (π(ballβπ·)π) β (π β π₯ β π β (π(ballβπ·)π))) |
21 | | sseq1 3973 |
. . . . . 6
β’ (π₯ = (π(ballβπ·)π) β (π₯ β π΄ β (π(ballβπ·)π) β π΄)) |
22 | 20, 21 | anbi12d 632 |
. . . . 5
β’ (π₯ = (π(ballβπ·)π) β ((π β π₯ β§ π₯ β π΄) β (π β (π(ballβπ·)π) β§ (π(ballβπ·)π) β π΄))) |
23 | 22 | rspcev 3583 |
. . . 4
β’ (((π(ballβπ·)π) β ran (ballβπ·) β§ (π β (π(ballβπ·)π) β§ (π(ballβπ·)π) β π΄)) β βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄)) |
24 | 15, 18, 19, 23 | syl12anc 836 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β+ β§ (π(ballβπ·)π) β π΄)) β βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄)) |
25 | 24 | rexlimdvaa 3150 |
. 2
β’ ((π· β (βMetβπ) β§ π β π) β (βπ β β+ (π(ballβπ·)π) β π΄ β βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄))) |
26 | 9, 25 | impbid 211 |
1
β’ ((π· β (βMetβπ) β§ π β π) β (βπ₯ β ran (ballβπ·)(π β π₯ β§ π₯ β π΄) β βπ β β+ (π(ballβπ·)π) β π΄)) |