Metamath Proof Explorer


Theorem blhalf

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 M∞MetXYXRZYballMR2YballMR2ZballMR

Proof

Step Hyp Ref Expression
1 simpll M∞MetXYXRZYballMR2M∞MetX
2 simplr M∞MetXYXRZYballMR2YX
3 simprr M∞MetXYXRZYballMR2ZYballMR2
4 simprl M∞MetXYXRZYballMR2R
5 4 rehalfcld M∞MetXYXRZYballMR2R2
6 5 rexrd M∞MetXYXRZYballMR2R2*
7 elbl M∞MetXYXR2*ZYballMR2ZXYMZ<R2
8 1 2 6 7 syl3anc M∞MetXYXRZYballMR2ZYballMR2ZXYMZ<R2
9 3 8 mpbid M∞MetXYXRZYballMR2ZXYMZ<R2
10 9 simpld M∞MetXYXRZYballMR2ZX
11 xmetcl M∞MetXYXZXYMZ*
12 1 2 10 11 syl3anc M∞MetXYXRZYballMR2YMZ*
13 9 simprd M∞MetXYXRZYballMR2YMZ<R2
14 12 6 13 xrltled M∞MetXYXRZYballMR2YMZR2
15 5 recnd M∞MetXYXRZYballMR2R2
16 4 recnd M∞MetXYXRZYballMR2R
17 16 2halvesd M∞MetXYXRZYballMR2R2+R2=R
18 15 15 17 mvlraddd M∞MetXYXRZYballMR2R2=RR2
19 14 18 breqtrd M∞MetXYXRZYballMR2YMZRR2
20 blss2 M∞MetXYXZXR2RYMZRR2YballMR2ZballMR
21 1 2 10 5 4 19 20 syl33anc M∞MetXYXRZYballMR2YballMR2ZballMR