Description: A ball of radius R / 2 is contained in a ball of radius R centered at any point inside the smaller ball. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 14-Jan-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | blhalf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpll | |
|
2 | simplr | |
|
3 | simprr | |
|
4 | simprl | |
|
5 | 4 | rehalfcld | |
6 | 5 | rexrd | |
7 | elbl | |
|
8 | 1 2 6 7 | syl3anc | |
9 | 3 8 | mpbid | |
10 | 9 | simpld | |
11 | xmetcl | |
|
12 | 1 2 10 11 | syl3anc | |
13 | 9 | simprd | |
14 | 12 6 13 | xrltled | |
15 | 5 | recnd | |
16 | 4 | recnd | |
17 | 16 | 2halvesd | |
18 | 15 15 17 | mvlraddd | |
19 | 14 18 | breqtrd | |
20 | blss2 | |
|
21 | 1 2 10 5 4 19 20 | syl33anc | |