Step | Hyp | Ref
| Expression |
1 | | simprl 770 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β π
β
β+) |
2 | 1 | rphalfcld 13028 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β (π
/ 2) β
β+) |
3 | | simprr 772 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β π β
β+) |
4 | 2, 3 | ifcld 4575 |
. 2
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β if((π
/ 2) β€
π, (π
/ 2), π) β
β+) |
5 | 4 | rpred 13016 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β if((π
/ 2) β€
π, (π
/ 2), π) β β) |
6 | 2 | rpred 13016 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β (π
/ 2) β
β) |
7 | 1 | rpred 13016 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β π
β
β) |
8 | 3 | rpred 13016 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β π β
β) |
9 | | min1 13168 |
. . . 4
β’ (((π
/ 2) β β β§ π β β) β
if((π
/ 2) β€ π, (π
/ 2), π) β€ (π
/ 2)) |
10 | 6, 8, 9 | syl2anc 585 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β if((π
/ 2) β€
π, (π
/ 2), π) β€ (π
/ 2)) |
11 | 1 | rpgt0d 13019 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β 0 < π
) |
12 | | halfpos 12442 |
. . . . 5
β’ (π
β β β (0 <
π
β (π
/ 2) < π
)) |
13 | 7, 12 | syl 17 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β (0 < π
β
(π
/ 2) < π
)) |
14 | 11, 13 | mpbid 231 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β (π
/ 2) < π
) |
15 | 5, 6, 7, 10, 14 | lelttrd 11372 |
. 2
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β if((π
/ 2) β€
π, (π
/ 2), π) < π
) |
16 | | simpl 484 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β (π· β
(βMetβπ) β§
π β π)) |
17 | 4 | rpxrd 13017 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β if((π
/ 2) β€
π, (π
/ 2), π) β
β*) |
18 | 3 | rpxrd 13017 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β π β
β*) |
19 | | min2 13169 |
. . . 4
β’ (((π
/ 2) β β β§ π β β) β
if((π
/ 2) β€ π, (π
/ 2), π) β€ π) |
20 | 6, 8, 19 | syl2anc 585 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β if((π
/ 2) β€
π, (π
/ 2), π) β€ π) |
21 | | ssbl 23929 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (if((π
/ 2) β€ π, (π
/ 2), π) β β* β§ π β β*)
β§ if((π
/ 2) β€ π, (π
/ 2), π) β€ π) β (π(ballβπ·)if((π
/ 2) β€ π, (π
/ 2), π)) β (π(ballβπ·)π)) |
22 | 16, 17, 18, 20, 21 | syl121anc 1376 |
. 2
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β (π(ballβπ·)if((π
/ 2) β€ π, (π
/ 2), π)) β (π(ballβπ·)π)) |
23 | | breq1 5152 |
. . . 4
β’ (π₯ = if((π
/ 2) β€ π, (π
/ 2), π) β (π₯ < π
β if((π
/ 2) β€ π, (π
/ 2), π) < π
)) |
24 | | oveq2 7417 |
. . . . 5
β’ (π₯ = if((π
/ 2) β€ π, (π
/ 2), π) β (π(ballβπ·)π₯) = (π(ballβπ·)if((π
/ 2) β€ π, (π
/ 2), π))) |
25 | 24 | sseq1d 4014 |
. . . 4
β’ (π₯ = if((π
/ 2) β€ π, (π
/ 2), π) β ((π(ballβπ·)π₯) β (π(ballβπ·)π) β (π(ballβπ·)if((π
/ 2) β€ π, (π
/ 2), π)) β (π(ballβπ·)π))) |
26 | 23, 25 | anbi12d 632 |
. . 3
β’ (π₯ = if((π
/ 2) β€ π, (π
/ 2), π) β ((π₯ < π
β§ (π(ballβπ·)π₯) β (π(ballβπ·)π)) β (if((π
/ 2) β€ π, (π
/ 2), π) < π
β§ (π(ballβπ·)if((π
/ 2) β€ π, (π
/ 2), π)) β (π(ballβπ·)π)))) |
27 | 26 | rspcev 3613 |
. 2
β’
((if((π
/ 2) β€
π, (π
/ 2), π) β β+ β§
(if((π
/ 2) β€ π, (π
/ 2), π) < π
β§ (π(ballβπ·)if((π
/ 2) β€ π, (π
/ 2), π)) β (π(ballβπ·)π))) β βπ₯ β β+ (π₯ < π
β§ (π(ballβπ·)π₯) β (π(ballβπ·)π))) |
28 | 4, 15, 22, 27 | syl12anc 836 |
1
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β+ β§ π β β+))
β βπ₯ β
β+ (π₯ <
π
β§ (π(ballβπ·)π₯) β (π(ballβπ·)π))) |