Step | Hyp | Ref
| Expression |
1 | | simpl1 1188 |
. . 3
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ (π
β β β§ π
β€ ((ππ·π) / 2))) β π· β (Metβπ)) |
2 | | metxmet 24184 |
. . 3
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
3 | 1, 2 | syl 17 |
. 2
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ (π
β β β§ π
β€ ((ππ·π) / 2))) β π· β (βMetβπ)) |
4 | | simpl2 1189 |
. 2
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ (π
β β β§ π
β€ ((ππ·π) / 2))) β π β π) |
5 | | simpl3 1190 |
. 2
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ (π
β β β§ π
β€ ((ππ·π) / 2))) β π β π) |
6 | | rexr 11259 |
. . 3
β’ (π
β β β π
β
β*) |
7 | 6 | ad2antrl 725 |
. 2
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ (π
β β β§ π
β€ ((ππ·π) / 2))) β π
β
β*) |
8 | | simprl 768 |
. . . . 5
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ (π
β β β§ π
β€ ((ππ·π) / 2))) β π
β β) |
9 | 8, 8 | rexaddd 13214 |
. . . 4
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ (π
β β β§ π
β€ ((ππ·π) / 2))) β (π
+π π
) = (π
+ π
)) |
10 | 8 | recnd 11241 |
. . . . 5
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ (π
β β β§ π
β€ ((ππ·π) / 2))) β π
β β) |
11 | 10 | 2timesd 12454 |
. . . 4
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ (π
β β β§ π
β€ ((ππ·π) / 2))) β (2 Β· π
) = (π
+ π
)) |
12 | 9, 11 | eqtr4d 2767 |
. . 3
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ (π
β β β§ π
β€ ((ππ·π) / 2))) β (π
+π π
) = (2 Β· π
)) |
13 | | id 22 |
. . . . . 6
β’ (π
β β β π
β
β) |
14 | | metcl 24182 |
. . . . . 6
β’ ((π· β (Metβπ) β§ π β π β§ π β π) β (ππ·π) β β) |
15 | | 2re 12285 |
. . . . . . . 8
β’ 2 β
β |
16 | | 2pos 12314 |
. . . . . . . 8
β’ 0 <
2 |
17 | 15, 16 | pm3.2i 470 |
. . . . . . 7
β’ (2 β
β β§ 0 < 2) |
18 | | lemuldiv2 12094 |
. . . . . . 7
β’ ((π
β β β§ (ππ·π) β β β§ (2 β β
β§ 0 < 2)) β ((2 Β· π
) β€ (ππ·π) β π
β€ ((ππ·π) / 2))) |
19 | 17, 18 | mp3an3 1446 |
. . . . . 6
β’ ((π
β β β§ (ππ·π) β β) β ((2 Β· π
) β€ (ππ·π) β π
β€ ((ππ·π) / 2))) |
20 | 13, 14, 19 | syl2anr 596 |
. . . . 5
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ π
β β) β ((2 Β· π
) β€ (ππ·π) β π
β€ ((ππ·π) / 2))) |
21 | 20 | biimprd 247 |
. . . 4
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ π
β β) β (π
β€ ((ππ·π) / 2) β (2 Β· π
) β€ (ππ·π))) |
22 | 21 | impr 454 |
. . 3
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ (π
β β β§ π
β€ ((ππ·π) / 2))) β (2 Β· π
) β€ (ππ·π)) |
23 | 12, 22 | eqbrtrd 5161 |
. 2
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ (π
β β β§ π
β€ ((ππ·π) / 2))) β (π
+π π
) β€ (ππ·π)) |
24 | | bldisj 24248 |
. 2
β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π
β β* β§ π
β β*
β§ (π
+π π
)
β€ (ππ·π))) β ((π(ballβπ·)π
) β© (π(ballβπ·)π
)) = β
) |
25 | 3, 4, 5, 7, 7, 23,
24 | syl33anc 1382 |
1
β’ (((π· β (Metβπ) β§ π β π β§ π β π) β§ (π
β β β§ π
β€ ((ππ·π) / 2))) β ((π(ballβπ·)π
) β© (π(ballβπ·)π
)) = β
) |