Step |
Hyp |
Ref |
Expression |
1 |
|
simpl1 |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ R <_ ( ( P D Q ) / 2 ) ) ) -> D e. ( Met ` X ) ) |
2 |
|
metxmet |
|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) ) |
3 |
1 2
|
syl |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ R <_ ( ( P D Q ) / 2 ) ) ) -> D e. ( *Met ` X ) ) |
4 |
|
simpl2 |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ R <_ ( ( P D Q ) / 2 ) ) ) -> P e. X ) |
5 |
|
simpl3 |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ R <_ ( ( P D Q ) / 2 ) ) ) -> Q e. X ) |
6 |
|
rexr |
|- ( R e. RR -> R e. RR* ) |
7 |
6
|
ad2antrl |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ R <_ ( ( P D Q ) / 2 ) ) ) -> R e. RR* ) |
8 |
|
simprl |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ R <_ ( ( P D Q ) / 2 ) ) ) -> R e. RR ) |
9 |
8 8
|
rexaddd |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ R <_ ( ( P D Q ) / 2 ) ) ) -> ( R +e R ) = ( R + R ) ) |
10 |
8
|
recnd |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ R <_ ( ( P D Q ) / 2 ) ) ) -> R e. CC ) |
11 |
10
|
2timesd |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ R <_ ( ( P D Q ) / 2 ) ) ) -> ( 2 x. R ) = ( R + R ) ) |
12 |
9 11
|
eqtr4d |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ R <_ ( ( P D Q ) / 2 ) ) ) -> ( R +e R ) = ( 2 x. R ) ) |
13 |
|
id |
|- ( R e. RR -> R e. RR ) |
14 |
|
metcl |
|- ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) -> ( P D Q ) e. RR ) |
15 |
|
2re |
|- 2 e. RR |
16 |
|
2pos |
|- 0 < 2 |
17 |
15 16
|
pm3.2i |
|- ( 2 e. RR /\ 0 < 2 ) |
18 |
|
lemuldiv2 |
|- ( ( R e. RR /\ ( P D Q ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. R ) <_ ( P D Q ) <-> R <_ ( ( P D Q ) / 2 ) ) ) |
19 |
17 18
|
mp3an3 |
|- ( ( R e. RR /\ ( P D Q ) e. RR ) -> ( ( 2 x. R ) <_ ( P D Q ) <-> R <_ ( ( P D Q ) / 2 ) ) ) |
20 |
13 14 19
|
syl2anr |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ R e. RR ) -> ( ( 2 x. R ) <_ ( P D Q ) <-> R <_ ( ( P D Q ) / 2 ) ) ) |
21 |
20
|
biimprd |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ R e. RR ) -> ( R <_ ( ( P D Q ) / 2 ) -> ( 2 x. R ) <_ ( P D Q ) ) ) |
22 |
21
|
impr |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ R <_ ( ( P D Q ) / 2 ) ) ) -> ( 2 x. R ) <_ ( P D Q ) ) |
23 |
12 22
|
eqbrtrd |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ R <_ ( ( P D Q ) / 2 ) ) ) -> ( R +e R ) <_ ( P D Q ) ) |
24 |
|
bldisj |
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ R e. RR* /\ ( R +e R ) <_ ( P D Q ) ) ) -> ( ( P ( ball ` D ) R ) i^i ( Q ( ball ` D ) R ) ) = (/) ) |
25 |
3 4 5 7 7 23 24
|
syl33anc |
|- ( ( ( D e. ( Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ R <_ ( ( P D Q ) / 2 ) ) ) -> ( ( P ( ball ` D ) R ) i^i ( Q ( ball ` D ) R ) ) = (/) ) |