| Step | Hyp | Ref
| Expression |
|---|
| 1 | | simprl 529 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β π
β
β+) |
| 2 | 1 | rphalfcld 9709 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β (π
/ 2) β
β+) |
| 3 | | simprr 531 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β π β
β+) |
| 4 | | rpmincl 11246 |
. . 3
β’ (((π
/ 2) β β+
β§ π β
β+) β inf({(π
/ 2), π}, β, < ) β
β+) |
| 5 | 2, 3, 4 | syl2anc 411 |
. 2
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β inf({(π
/ 2), π}, β, < ) β
β+) |
| 6 | 5 | rpred 9696 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β inf({(π
/ 2), π}, β, < ) β
β) |
| 7 | 2 | rpred 9696 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β (π
/ 2) β
β) |
| 8 | 1 | rpred 9696 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β π
β
β) |
| 9 | 3 | rpred 9696 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β π β
β) |
| 10 | | min1inf 11240 |
. . . 4
β’ (((π
/ 2) β β β§ π β β) β
inf({(π
/ 2), π}, β, < ) β€ (π
/ 2)) |
| 11 | 7, 9, 10 | syl2anc 411 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β inf({(π
/ 2), π}, β, < ) β€ (π
/ 2)) |
| 12 | 1 | rpgt0d 9699 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β 0 < π
) |
| 13 | | halfpos 9150 |
. . . . 5
β’ (π
β β β (0 <
π
β (π
/ 2) < π
)) |
| 14 | 8, 13 | syl 14 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β (0 < π
β
(π
/ 2) < π
)) |
| 15 | 12, 14 | mpbid 147 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β (π
/ 2) < π
) |
| 16 | 6, 7, 8, 11, 15 | lelttrd 8082 |
. 2
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β inf({(π
/ 2), π}, β, < ) < π
) |
| 17 | | simpl 109 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β (π· β
(βMetβπ) β§
π β π)) |
| 18 | 5 | rpxrd 9697 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β inf({(π
/ 2), π}, β, < ) β
β*) |
| 19 | 3 | rpxrd 9697 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β π β
β*) |
| 20 | | min2inf 11241 |
. . . 4
β’ (((π
/ 2) β β β§ π β β) β
inf({(π
/ 2), π}, β, < ) β€ π) |
| 21 | 7, 9, 20 | syl2anc 411 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β inf({(π
/ 2), π}, β, < ) β€ π) |
| 22 | | ssbl 13929 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (inf({(π
/ 2), π}, β, < ) β
β* β§ π
β β*) β§ inf({(π
/ 2), π}, β, < ) β€ π) β (π(ballβπ·)inf({(π
/ 2), π}, β, < )) β (π(ballβπ·)π)) |
| 23 | 17, 18, 19, 21, 22 | syl121anc 1243 |
. 2
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β (π(ballβπ·)inf({(π
/ 2), π}, β, < )) β (π(ballβπ·)π)) |
| 24 | | breq1 4007 |
. . . 4
β’ (π₯ = inf({(π
/ 2), π}, β, < ) β (π₯ < π
β inf({(π
/ 2), π}, β, < ) < π
)) |
| 25 | | oveq2 5883 |
. . . . 5
β’ (π₯ = inf({(π
/ 2), π}, β, < ) β (π(ballβπ·)π₯) = (π(ballβπ·)inf({(π
/ 2), π}, β, < ))) |
| 26 | 25 | sseq1d 3185 |
. . . 4
β’ (π₯ = inf({(π
/ 2), π}, β, < ) β ((π(ballβπ·)π₯) β (π(ballβπ·)π) β (π(ballβπ·)inf({(π
/ 2), π}, β, < )) β (π(ballβπ·)π))) |
| 27 | 24, 26 | anbi12d 473 |
. . 3
β’ (π₯ = inf({(π
/ 2), π}, β, < ) β ((π₯ < π
β§ (π(ballβπ·)π₯) β (π(ballβπ·)π)) β (inf({(π
/ 2), π}, β, < ) < π
β§ (π(ballβπ·)inf({(π
/ 2), π}, β, < )) β (π(ballβπ·)π)))) |
| 28 | 27 | rspcev 2842 |
. 2
β’
((inf({(π
/ 2),
π}, β, < ) β
β+ β§ (inf({(π
/ 2), π}, β, < ) < π
β§ (π(ballβπ·)inf({(π
/ 2), π}, β, < )) β (π(ballβπ·)π))) β βπ₯ β β+ (π₯ < π
β§ (π(ballβπ·)π₯) β (π(ballβπ·)π))) |
| 29 | 5, 16, 23, 28 | syl12anc 1236 |
1
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β βπ₯ β
β+ (π₯ <
π
β§ (π(ballβπ·)π₯) β (π(ballβπ·)π))) |
