Step | Hyp | Ref
| Expression |
1 | | isbndx 36270 |
. . 3
β’ (π β (Bndβπ) β (π β (βMetβπ) β§ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) |
2 | 1 | anbi1i 625 |
. 2
β’ ((π β (Bndβπ) β§ π β β
) β ((π β (βMetβπ) β§ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π)) β§ π β β
)) |
3 | | anass 470 |
. 2
β’ (((π β (βMetβπ) β§ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π)) β§ π β β
) β (π β (βMetβπ) β§ (βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β§ π β β
))) |
4 | | r19.2z 4457 |
. . . . 5
β’ ((π β β
β§
βπ₯ β π βπ β β+ π = (π₯(ballβπ)π)) β βπ₯ β π βπ β β+ π = (π₯(ballβπ)π)) |
5 | 4 | ancoms 460 |
. . . 4
β’
((βπ₯ β
π βπ β β+ π = (π₯(ballβπ)π) β§ π β β
) β βπ₯ β π βπ β β+ π = (π₯(ballβπ)π)) |
6 | | oveq1 7369 |
. . . . . . . 8
β’ (π₯ = π¦ β (π₯(ballβπ)π) = (π¦(ballβπ)π)) |
7 | 6 | eqeq2d 2748 |
. . . . . . 7
β’ (π₯ = π¦ β (π = (π₯(ballβπ)π) β π = (π¦(ballβπ)π))) |
8 | | oveq2 7370 |
. . . . . . . 8
β’ (π = π β (π¦(ballβπ)π) = (π¦(ballβπ)π )) |
9 | 8 | eqeq2d 2748 |
. . . . . . 7
β’ (π = π β (π = (π¦(ballβπ)π) β π = (π¦(ballβπ)π ))) |
10 | 7, 9 | cbvrex2vw 3231 |
. . . . . 6
β’
(βπ₯ β
π βπ β β+ π = (π₯(ballβπ)π) β βπ¦ β π βπ β β+ π = (π¦(ballβπ)π )) |
11 | | 2rp 12927 |
. . . . . . . . . . . . 13
β’ 2 β
β+ |
12 | | rpmulcl 12945 |
. . . . . . . . . . . . 13
β’ ((2
β β+ β§ π β β+) β (2
Β· π ) β
β+) |
13 | 11, 12 | mpan 689 |
. . . . . . . . . . . 12
β’ (π β β+
β (2 Β· π )
β β+) |
14 | 13 | ad2antll 728 |
. . . . . . . . . . 11
β’ ((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β (2
Β· π ) β
β+) |
15 | 14 | ad2antrr 725 |
. . . . . . . . . 10
β’ ((((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β§ π₯ β π) β§ π = (π¦(ballβπ)π )) β (2 Β· π ) β
β+) |
16 | | rpcn 12932 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β+
β π β
β) |
17 | | 2cnd 12238 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β+
β 2 β β) |
18 | | 2ne0 12264 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
0 |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β+
β 2 β 0) |
20 | | divcan3 11846 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ 2 β
β β§ 2 β 0) β ((2 Β· π ) / 2) = π ) |
21 | 20 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ 2 β
β β§ 2 β 0) β π = ((2 Β· π ) / 2)) |
22 | 16, 17, 19, 21 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β+
β π = ((2 Β·
π ) / 2)) |
23 | 22 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
β’ (π β β+
β (π¦(ballβπ)π ) = (π¦(ballβπ)((2 Β· π ) / 2))) |
24 | 23 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
β’ (π β β+
β (π = (π¦(ballβπ)π ) β π = (π¦(ballβπ)((2 Β· π ) / 2)))) |
25 | 24 | biimpd 228 |
. . . . . . . . . . . . . . 15
β’ (π β β+
β (π = (π¦(ballβπ)π ) β π = (π¦(ballβπ)((2 Β· π ) / 2)))) |
26 | 25 | ad2antll 728 |
. . . . . . . . . . . . . 14
β’ ((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β (π = (π¦(ballβπ)π ) β π = (π¦(ballβπ)((2 Β· π ) / 2)))) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β§ π₯ β π) β (π = (π¦(ballβπ)π ) β π = (π¦(ballβπ)((2 Β· π ) / 2)))) |
28 | 27 | imp 408 |
. . . . . . . . . . . 12
β’ ((((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β§ π₯ β π) β§ π = (π¦(ballβπ)π )) β π = (π¦(ballβπ)((2 Β· π ) / 2))) |
29 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β§ π₯ β π) β§ π = (π¦(ballβπ)((2 Β· π ) / 2))) β π = (π¦(ballβπ)((2 Β· π ) / 2))) |
30 | | eleq2 2827 |
. . . . . . . . . . . . . . . 16
β’ (π = (π¦(ballβπ)((2 Β· π ) / 2)) β (π₯ β π β π₯ β (π¦(ballβπ)((2 Β· π ) / 2)))) |
31 | 30 | biimpac 480 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β π β§ π = (π¦(ballβπ)((2 Β· π ) / 2))) β π₯ β (π¦(ballβπ)((2 Β· π ) / 2))) |
32 | | 2re 12234 |
. . . . . . . . . . . . . . . . . . 19
β’ 2 β
β |
33 | | rpre 12930 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β+
β π β
β) |
34 | | remulcl 11143 |
. . . . . . . . . . . . . . . . . . 19
β’ ((2
β β β§ π
β β) β (2 Β· π ) β β) |
35 | 32, 33, 34 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β+
β (2 Β· π )
β β) |
36 | | blhalf 23774 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (βMetβπ) β§ π¦ β π) β§ ((2 Β· π ) β β β§ π₯ β (π¦(ballβπ)((2 Β· π ) / 2)))) β (π¦(ballβπ)((2 Β· π ) / 2)) β (π₯(ballβπ)(2 Β· π ))) |
37 | 36 | expr 458 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β (βMetβπ) β§ π¦ β π) β§ (2 Β· π ) β β) β (π₯ β (π¦(ballβπ)((2 Β· π ) / 2)) β (π¦(ballβπ)((2 Β· π ) / 2)) β (π₯(ballβπ)(2 Β· π )))) |
38 | 35, 37 | sylan2 594 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (βMetβπ) β§ π¦ β π) β§ π β β+) β (π₯ β (π¦(ballβπ)((2 Β· π ) / 2)) β (π¦(ballβπ)((2 Β· π ) / 2)) β (π₯(ballβπ)(2 Β· π )))) |
39 | 38 | anasss 468 |
. . . . . . . . . . . . . . . 16
β’ ((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β (π₯ β (π¦(ballβπ)((2 Β· π ) / 2)) β (π¦(ballβπ)((2 Β· π ) / 2)) β (π₯(ballβπ)(2 Β· π )))) |
40 | 39 | imp 408 |
. . . . . . . . . . . . . . 15
β’ (((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β§ π₯ β (π¦(ballβπ)((2 Β· π ) / 2))) β (π¦(ballβπ)((2 Β· π ) / 2)) β (π₯(ballβπ)(2 Β· π ))) |
41 | 31, 40 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ (((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β§ (π₯ β π β§ π = (π¦(ballβπ)((2 Β· π ) / 2)))) β (π¦(ballβπ)((2 Β· π ) / 2)) β (π₯(ballβπ)(2 Β· π ))) |
42 | 41 | anassrs 469 |
. . . . . . . . . . . . 13
β’ ((((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β§ π₯ β π) β§ π = (π¦(ballβπ)((2 Β· π ) / 2))) β (π¦(ballβπ)((2 Β· π ) / 2)) β (π₯(ballβπ)(2 Β· π ))) |
43 | 29, 42 | eqsstrd 3987 |
. . . . . . . . . . . 12
β’ ((((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β§ π₯ β π) β§ π = (π¦(ballβπ)((2 Β· π ) / 2))) β π β (π₯(ballβπ)(2 Β· π ))) |
44 | 28, 43 | syldan 592 |
. . . . . . . . . . 11
β’ ((((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β§ π₯ β π) β§ π = (π¦(ballβπ)π )) β π β (π₯(ballβπ)(2 Β· π ))) |
45 | 13 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π¦ β π β§ π β β+) β (2
Β· π ) β
β+) |
46 | | rpxr 12931 |
. . . . . . . . . . . . . . . 16
β’ ((2
Β· π ) β
β+ β (2 Β· π ) β
β*) |
47 | | blssm 23787 |
. . . . . . . . . . . . . . . 16
β’ ((π β (βMetβπ) β§ π₯ β π β§ (2 Β· π ) β β*) β (π₯(ballβπ)(2 Β· π )) β π) |
48 | 46, 47 | syl3an3 1166 |
. . . . . . . . . . . . . . 15
β’ ((π β (βMetβπ) β§ π₯ β π β§ (2 Β· π ) β β+) β (π₯(ballβπ)(2 Β· π )) β π) |
49 | 48 | 3expa 1119 |
. . . . . . . . . . . . . 14
β’ (((π β (βMetβπ) β§ π₯ β π) β§ (2 Β· π ) β β+) β (π₯(ballβπ)(2 Β· π )) β π) |
50 | 45, 49 | sylan2 594 |
. . . . . . . . . . . . 13
β’ (((π β (βMetβπ) β§ π₯ β π) β§ (π¦ β π β§ π β β+)) β (π₯(ballβπ)(2 Β· π )) β π) |
51 | 50 | an32s 651 |
. . . . . . . . . . . 12
β’ (((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β§ π₯ β π) β (π₯(ballβπ)(2 Β· π )) β π) |
52 | 51 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β§ π₯ β π) β§ π = (π¦(ballβπ)π )) β (π₯(ballβπ)(2 Β· π )) β π) |
53 | 44, 52 | eqssd 3966 |
. . . . . . . . . 10
β’ ((((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β§ π₯ β π) β§ π = (π¦(ballβπ)π )) β π = (π₯(ballβπ)(2 Β· π ))) |
54 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = (2 Β· π ) β (π₯(ballβπ)π) = (π₯(ballβπ)(2 Β· π ))) |
55 | 54 | rspceeqv 3600 |
. . . . . . . . . 10
β’ (((2
Β· π ) β
β+ β§ π
= (π₯(ballβπ)(2 Β· π ))) β βπ β β+ π = (π₯(ballβπ)π)) |
56 | 15, 53, 55 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β§ π₯ β π) β§ π = (π¦(ballβπ)π )) β βπ β β+ π = (π₯(ballβπ)π)) |
57 | 56 | ex 414 |
. . . . . . . 8
β’ (((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β§ π₯ β π) β (π = (π¦(ballβπ)π ) β βπ β β+ π = (π₯(ballβπ)π))) |
58 | 57 | ralrimdva 3152 |
. . . . . . 7
β’ ((π β (βMetβπ) β§ (π¦ β π β§ π β β+)) β (π = (π¦(ballβπ)π ) β βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) |
59 | 58 | rexlimdvva 3206 |
. . . . . 6
β’ (π β (βMetβπ) β (βπ¦ β π βπ β β+ π = (π¦(ballβπ)π ) β βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) |
60 | 10, 59 | biimtrid 241 |
. . . . 5
β’ (π β (βMetβπ) β (βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) |
61 | | rexn0 4473 |
. . . . . 6
β’
(βπ₯ β
π βπ β β+ π = (π₯(ballβπ)π) β π β β
) |
62 | 61 | a1i 11 |
. . . . 5
β’ (π β (βMetβπ) β (βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β π β β
)) |
63 | 60, 62 | jcad 514 |
. . . 4
β’ (π β (βMetβπ) β (βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β (βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β§ π β β
))) |
64 | 5, 63 | impbid2 225 |
. . 3
β’ (π β (βMetβπ) β ((βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β§ π β β
) β βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) |
65 | 64 | pm5.32i 576 |
. 2
β’ ((π β (βMetβπ) β§ (βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β§ π β β
)) β (π β (βMetβπ) β§ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) |
66 | 2, 3, 65 | 3bitri 297 |
1
β’ ((π β (Bndβπ) β§ π β β
) β (π β (βMetβπ) β§ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) |