Step | Hyp | Ref
| Expression |
1 | | simp1 1133 |
. . . . 5
β’ ((π β (βMetβπ) β§ π β π β§ π
β β) β π β (βMetβπ)) |
2 | | rexr 11259 |
. . . . . 6
β’ (π
β β β π
β
β*) |
3 | | blssm 24268 |
. . . . . 6
β’ ((π β (βMetβπ) β§ π β π β§ π
β β*) β (π(ballβπ)π
) β π) |
4 | 2, 3 | syl3an3 1162 |
. . . . 5
β’ ((π β (βMetβπ) β§ π β π β§ π
β β) β (π(ballβπ)π
) β π) |
5 | | xmetres2 24211 |
. . . . 5
β’ ((π β (βMetβπ) β§ (π(ballβπ)π
) β π) β (π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))) β (βMetβ(π(ballβπ)π
))) |
6 | 1, 4, 5 | syl2anc 583 |
. . . 4
β’ ((π β (βMetβπ) β§ π β π β§ π
β β) β (π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))) β (βMetβ(π(ballβπ)π
))) |
7 | 6 | adantr 480 |
. . 3
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) = β
) β (π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))) β (βMetβ(π(ballβπ)π
))) |
8 | | rzal 4501 |
. . . 4
β’ ((π(ballβπ)π
) = β
β βπ₯ β (π(ballβπ)π
)βπ β β+ (π(ballβπ)π
) = (π₯(ballβ(π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))))π)) |
9 | 8 | adantl 481 |
. . 3
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) = β
) β βπ₯ β (π(ballβπ)π
)βπ β β+ (π(ballβπ)π
) = (π₯(ballβ(π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))))π)) |
10 | | isbndx 37153 |
. . 3
β’ ((π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))) β (Bndβ(π(ballβπ)π
)) β ((π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))) β (βMetβ(π(ballβπ)π
)) β§ βπ₯ β (π(ballβπ)π
)βπ β β+ (π(ballβπ)π
) = (π₯(ballβ(π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))))π))) |
11 | 7, 9, 10 | sylanbrc 582 |
. 2
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) = β
) β (π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))) β (Bndβ(π(ballβπ)π
))) |
12 | 6 | adantr 480 |
. . . 4
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) β β
) β (π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))) β (βMetβ(π(ballβπ)π
))) |
13 | 1 | adantr 480 |
. . . . . 6
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) β β
) β π β (βMetβπ)) |
14 | | simpl2 1189 |
. . . . . 6
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) β β
) β π β π) |
15 | | simpl3 1190 |
. . . . . . 7
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) β β
) β π
β β) |
16 | | xbln0 24264 |
. . . . . . . . 9
β’ ((π β (βMetβπ) β§ π β π β§ π
β β*) β ((π(ballβπ)π
) β β
β 0 < π
)) |
17 | 2, 16 | syl3an3 1162 |
. . . . . . . 8
β’ ((π β (βMetβπ) β§ π β π β§ π
β β) β ((π(ballβπ)π
) β β
β 0 < π
)) |
18 | 17 | biimpa 476 |
. . . . . . 7
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) β β
) β 0 < π
) |
19 | 15, 18 | elrpd 13014 |
. . . . . 6
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) β β
) β π
β
β+) |
20 | | blcntr 24263 |
. . . . . 6
β’ ((π β (βMetβπ) β§ π β π β§ π
β β+) β π β (π(ballβπ)π
)) |
21 | 13, 14, 19, 20 | syl3anc 1368 |
. . . . 5
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) β β
) β π β (π(ballβπ)π
)) |
22 | 14, 21 | elind 4187 |
. . . . . . 7
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) β β
) β π β (π β© (π(ballβπ)π
))) |
23 | 15 | rexrd 11263 |
. . . . . . 7
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) β β
) β π
β
β*) |
24 | | eqid 2724 |
. . . . . . . 8
β’ (π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))) = (π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))) |
25 | 24 | blres 24281 |
. . . . . . 7
β’ ((π β (βMetβπ) β§ π β (π β© (π(ballβπ)π
)) β§ π
β β*) β (π(ballβ(π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))))π
) = ((π(ballβπ)π
) β© (π(ballβπ)π
))) |
26 | 13, 22, 23, 25 | syl3anc 1368 |
. . . . . 6
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) β β
) β (π(ballβ(π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))))π
) = ((π(ballβπ)π
) β© (π(ballβπ)π
))) |
27 | | inidm 4211 |
. . . . . 6
β’ ((π(ballβπ)π
) β© (π(ballβπ)π
)) = (π(ballβπ)π
) |
28 | 26, 27 | eqtr2di 2781 |
. . . . 5
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) β β
) β (π(ballβπ)π
) = (π(ballβ(π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))))π
)) |
29 | | rspceov 7449 |
. . . . 5
β’ ((π β (π(ballβπ)π
) β§ π
β β+ β§ (π(ballβπ)π
) = (π(ballβ(π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))))π
)) β βπ₯ β (π(ballβπ)π
)βπ β β+ (π(ballβπ)π
) = (π₯(ballβ(π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))))π)) |
30 | 21, 19, 28, 29 | syl3anc 1368 |
. . . 4
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) β β
) β βπ₯ β (π(ballβπ)π
)βπ β β+ (π(ballβπ)π
) = (π₯(ballβ(π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))))π)) |
31 | | isbnd2 37154 |
. . . 4
β’ (((π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))) β (Bndβ(π(ballβπ)π
)) β§ (π(ballβπ)π
) β β
) β ((π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))) β (βMetβ(π(ballβπ)π
)) β§ βπ₯ β (π(ballβπ)π
)βπ β β+ (π(ballβπ)π
) = (π₯(ballβ(π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))))π))) |
32 | 12, 30, 31 | sylanbrc 582 |
. . 3
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) β β
) β ((π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))) β (Bndβ(π(ballβπ)π
)) β§ (π(ballβπ)π
) β β
)) |
33 | 32 | simpld 494 |
. 2
β’ (((π β (βMetβπ) β§ π β π β§ π
β β) β§ (π(ballβπ)π
) β β
) β (π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))) β (Bndβ(π(ballβπ)π
))) |
34 | 11, 33 | pm2.61dane 3021 |
1
β’ ((π β (βMetβπ) β§ π β π β§ π
β β) β (π βΎ ((π(ballβπ)π
) Γ (π(ballβπ)π
))) β (Bndβ(π(ballβπ)π
))) |